Copyright	(c) Galois Inc 2015-2020
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Safe Haskell	None
Language	Haskell2010

What4.Expr

Contents

Expression builder
Flags
Type abbreviations
Expression datatypes
Logic theories
Ground evaluation

Description

The module reexports the most commonly used types and operations of the What4 expression representation.

Synopsis

data ExprBuilder t (st :: Type -> Type) (fs :: Type)
newExprBuilder :: FloatModeRepr fm -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
data FloatMode
data FloatModeRepr :: FloatMode -> Type where
- FloatIEEERepr :: FloatModeRepr FloatIEEE
- FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted
- FloatRealRepr :: FloatModeRepr FloatReal
type FloatIEEE = FloatIEEE
type FloatUninterpreted = FloatUninterpreted
type FloatReal = FloatReal
data Flags (fi :: FloatMode)
type BoolExpr t = Expr t BaseBoolType
type NatExpr t = Expr t BaseNatType
type IntegerExpr t = Expr t BaseIntegerType
type RealExpr t = Expr t BaseRealType
type BVExpr t n = Expr t (BaseBVType n)
type CplxExpr t = Expr t BaseComplexType
type StringExpr t si = Expr t (BaseStringType si)
data Expr t (tp :: BaseType) where
- SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr)
- BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
- StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si)
- AppExpr :: !(AppExpr t tp) -> Expr t tp
- NonceAppExpr :: !(NonceAppExpr t tp) -> Expr t tp
- BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp
exprLoc :: Expr t tp -> ProgramLoc
ppExpr :: Expr t tp -> Doc
data AppExpr t (tp :: BaseType)
appExprId :: AppExpr t tp -> Nonce t tp
appExprLoc :: AppExpr t tp -> ProgramLoc
appExprApp :: AppExpr t tp -> App (Expr t) tp
data App (e :: BaseType -> Type) (tp :: BaseType) where
- BaseIte :: !(BaseTypeRepr tp) -> !Integer -> !(e BaseBoolType) -> !(e tp) -> !(e tp) -> App e tp
- BaseEq :: !(BaseTypeRepr tp) -> !(e tp) -> !(e tp) -> App e BaseBoolType
- NotPred :: !(e BaseBoolType) -> App e BaseBoolType
- ConjPred :: !(BoolMap e) -> App e BaseBoolType
- SemiRingSum :: !(WeightedSum e sr) -> App e (SemiRingBase sr)
- SemiRingProd :: !(SemiRingProduct e sr) -> App e (SemiRingBase sr)
- SemiRingLe :: !(OrderedSemiRingRepr sr) -> !(e (SemiRingBase sr)) -> !(e (SemiRingBase sr)) -> App e BaseBoolType
- RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType
- NatDiv :: !(e BaseNatType) -> !(e BaseNatType) -> App e BaseNatType
- NatMod :: !(e BaseNatType) -> !(e BaseNatType) -> App e BaseNatType
- IntDiv :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
- IntMod :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
- IntAbs :: !(e BaseIntegerType) -> App e BaseIntegerType
- IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType
- RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
- RealSqrt :: !(e BaseRealType) -> App e BaseRealType
- Pi :: App e BaseRealType
- RealSin :: !(e BaseRealType) -> App e BaseRealType
- RealCos :: !(e BaseRealType) -> App e BaseRealType
- RealATan2 :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
- RealSinh :: !(e BaseRealType) -> App e BaseRealType
- RealCosh :: !(e BaseRealType) -> App e BaseRealType
- RealExp :: !(e BaseRealType) -> App e BaseRealType
- RealLog :: !(e BaseRealType) -> App e BaseRealType
- BVTestBit :: 1 <= w => !Natural -> !(e (BaseBVType w)) -> App e BaseBoolType
- BVSlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
- BVUlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
- BVOrBits :: 1 <= w => !(NatRepr w) -> !(BVOrSet e w) -> App e (BaseBVType w)
- BVUnaryTerm :: 1 <= n => !(UnaryBV (e BaseBoolType) n) -> App e (BaseBVType n)
- BVConcat :: (1 <= u, 1 <= v, 1 <= (u + v)) => !(NatRepr (u + v)) -> !(e (BaseBVType u)) -> !(e (BaseBVType v)) -> App e (BaseBVType (u + v))
- BVSelect :: (1 <= n, (idx + n) <= w) => !(NatRepr idx) -> !(NatRepr n) -> !(e (BaseBVType w)) -> App e (BaseBVType n)
- BVFill :: 1 <= w => !(NatRepr w) -> !(e BaseBoolType) -> App e (BaseBVType w)
- BVUdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVUrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVSdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVSrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVShl :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVLshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVAshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVRol :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVRor :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVZext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r)
- BVSext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r)
- BVPopcount :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVCountTrailingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVCountLeadingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- FloatPZero :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatNZero :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatNaN :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatPInf :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatNInf :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatNeg :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatAbs :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatSqrt :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatAdd :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatSub :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatMul :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatDiv :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatRem :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatMin :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatMax :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatFMA :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatFpEq :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatFpNe :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatLe :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatLt :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsNaN :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsInf :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsZero :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsPos :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsNeg :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsSubnorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsNorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatCast :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp')) -> App e (BaseFloatType fpp)
- FloatRound :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatFromBinary :: (2 <= eb, 2 <= sb) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseBVType (eb + sb))) -> App e (BaseFloatType (FloatingPointPrecision eb sb))
- FloatToBinary :: (2 <= eb, 2 <= sb, 1 <= (eb + sb)) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseFloatType (FloatingPointPrecision eb sb))) -> App e (BaseBVType (eb + sb))
- BVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp)
- SBVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp)
- RealToFloat :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e BaseRealType) -> App e (BaseFloatType fpp)
- FloatToBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w)
- FloatToSBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w)
- FloatToReal :: !(e (BaseFloatType fpp)) -> App e BaseRealType
- ArrayMap :: !(Assignment BaseTypeRepr (i ::> itp)) -> !(BaseTypeRepr tp) -> !(ArrayUpdateMap e (i ::> itp) tp) -> !(e (BaseArrayType (i ::> itp) tp)) -> App e (BaseArrayType (i ::> itp) tp)
- ConstantArray :: !(Assignment BaseTypeRepr (i ::> tp)) -> !(BaseTypeRepr b) -> !(e b) -> App e (BaseArrayType (i ::> tp) b)
- UpdateArray :: !(BaseTypeRepr b) -> !(Assignment BaseTypeRepr (i ::> tp)) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> !(e b) -> App e (BaseArrayType (i ::> tp) b)
- SelectArray :: !(BaseTypeRepr b) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> App e b
- NatToInteger :: !(e BaseNatType) -> App e BaseIntegerType
- IntegerToNat :: !(e BaseIntegerType) -> App e BaseNatType
- IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType
- RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType
- BVToNat :: 1 <= w => !(e (BaseBVType w)) -> App e BaseNatType
- BVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
- SBVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
- IntegerToBV :: 1 <= w => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)
- RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
- RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType
- FloorReal :: !(e BaseRealType) -> App e BaseIntegerType
- CeilReal :: !(e BaseRealType) -> App e BaseIntegerType
- Cplx :: !(Complex (e BaseRealType)) -> App e BaseComplexType
- RealPart :: !(e BaseComplexType) -> App e BaseRealType
- ImagPart :: !(e BaseComplexType) -> App e BaseRealType
- StringContains :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIsPrefixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIsSuffixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIndexOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> !(e BaseNatType) -> App e BaseIntegerType
- StringSubstring :: !(StringInfoRepr si) -> !(e (BaseStringType si)) -> !(e BaseNatType) -> !(e BaseNatType) -> App e (BaseStringType si)
- StringAppend :: !(StringInfoRepr si) -> !(StringSeq e si) -> App e (BaseStringType si)
- StringLength :: !(e (BaseStringType si)) -> App e BaseNatType
- StructCtor :: !(Assignment BaseTypeRepr flds) -> !(Assignment e flds) -> App e (BaseStructType flds)
- StructField :: !(e (BaseStructType flds)) -> !(Index flds tp) -> !(BaseTypeRepr tp) -> App e tp
data NonceAppExpr t (tp :: BaseType)
nonceExprId :: NonceAppExpr t tp -> Nonce t tp
nonceExprLoc :: NonceAppExpr t tp -> ProgramLoc
nonceExprApp :: NonceAppExpr t tp -> NonceApp t (Expr t) tp
data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where
- Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp
- Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
- Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
- ArrayFromFn :: !(ExprSymFn t e (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret)
- MapOverArrays :: !(ExprSymFn t e (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r)
- ArrayTrueOnEntries :: !(ExprSymFn t e (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType
- FnApp :: !(ExprSymFn t e args ret) -> !(Assignment e args) -> NonceApp t e ret
data ExprBoundVar t (tp :: BaseType)
bvarId :: ExprBoundVar t tp -> Nonce t tp
bvarLoc :: ExprBoundVar t tp -> ProgramLoc
bvarName :: ExprBoundVar t tp -> SolverSymbol
bvarKind :: ExprBoundVar t tp -> VarKind
data VarKind
- = QuantifierVarKind
- | LatchVarKind
- | UninterpVarKind
boundVars :: Expr t tp -> ST s (BoundVarMap s t)
data ExprSymFn t e (args :: Ctx BaseType) (ret :: BaseType) = ExprSymFn {
- symFnId :: !(Nonce t (args ::> ret))
- symFnName :: !SolverSymbol
- symFnInfo :: !(SymFnInfo t e args ret)
- symFnLoc :: !ProgramLoc
}
data SymFnInfo t e (args :: Ctx BaseType) (ret :: BaseType)
- = UninterpFnInfo !(Assignment BaseTypeRepr args) !(BaseTypeRepr ret)
- | DefinedFnInfo !(Assignment (ExprBoundVar t) args) !(e ret) !UnfoldPolicy
- | MatlabSolverFnInfo !(MatlabSolverFn e args ret) !(Assignment (ExprBoundVar t) args) !(e ret)
symFnArgTypes :: ExprSymFn t e args ret -> Assignment BaseTypeRepr args
symFnReturnType :: IsExpr e => ExprSymFn t e args ret -> BaseTypeRepr ret
type family Coefficient (sr :: SemiRing) :: Type where ...
data SemiRing
data BVFlavor
data SemiRingRepr (sr :: SemiRing) where
- SemiRingNatRepr :: SemiRingRepr SemiRingNat
- SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger
- SemiRingRealRepr :: SemiRingRepr SemiRingReal
- SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)
data BVFlavorRepr (fv :: BVFlavor) where
- BVArithRepr :: BVFlavorRepr BVArith
- BVBitsRepr :: BVFlavorRepr BVBits
data OrderedSemiRingRepr (sr :: SemiRing) where
- OrderedSemiRingNatRepr :: OrderedSemiRingRepr SemiRingNat
- OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger
- OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal
data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing)
data UnaryBV p (n :: Nat)
data AppTheory
- = BoolTheory
- | LinearArithTheory
- | NonlinearArithTheory
- | ComputableArithTheory
- | BitvectorTheory
- | QuantifierTheory
- | StringTheory
- | FloatingPointTheory
- | ArrayTheory
- | StructTheory
- | FnTheory
quantTheory :: NonceApp t (Expr t) tp -> AppTheory
appTheory :: App (Expr t) tp -> AppTheory
type family GroundValue (tp :: BaseType) where ...
newtype GroundValueWrapper tp = GVW {
- unGVW :: GroundValue tp
}
data GroundArray idx b
- = ArrayMapping (Assignment GroundValueWrapper idx -> IO (GroundValue b))
- | ArrayConcrete (GroundValue b) (Map (Assignment IndexLit idx) (GroundValue b))
lookupArray :: Assignment BaseTypeRepr idx -> GroundArray idx b -> Assignment GroundValueWrapper idx -> IO (GroundValue b)
newtype GroundEvalFn t = GroundEvalFn {
- groundEval :: forall tp. Expr t tp -> IO (GroundValue tp)
}
type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)

Expression builder

data ExprBuilder t (st :: Type -> Type) (fs :: Type) Source #

Cache for storing dag terms. Parameter t is a phantom type brand used to track nonces.

Instances

IsSymExprBuilder (ExprBuilder t st fs) Source #
Instance details Defined in What4.Expr.Builder Methods freshConstant :: ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source # freshLatch :: ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source # freshBoundedBV :: 1 <= w => ExprBuilder t st fs -> SolverSymbol -> NatRepr w -> Maybe Natural -> Maybe Natural -> IO (SymBV (ExprBuilder t st fs) w) Source # freshBoundedSBV :: 1 <= w => ExprBuilder t st fs -> SolverSymbol -> NatRepr w -> Maybe Integer -> Maybe Integer -> IO (SymBV (ExprBuilder t st fs) w) Source # freshBoundedNat :: ExprBuilder t st fs -> SolverSymbol -> Maybe Natural -> Maybe Natural -> IO (SymNat (ExprBuilder t st fs)) Source # freshBoundedInt :: ExprBuilder t st fs -> SolverSymbol -> Maybe Integer -> Maybe Integer -> IO (SymInteger (ExprBuilder t st fs)) Source # freshBoundedReal :: ExprBuilder t st fs -> SolverSymbol -> Maybe Rational -> Maybe Rational -> IO (SymReal (ExprBuilder t st fs)) Source # freshBoundVar :: ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar (ExprBuilder t st fs) tp) Source # varExpr :: ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> SymExpr (ExprBuilder t st fs) tp Source # forallPred :: ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # existsPred :: ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # definedFn :: ExprBuilder t st fs -> SolverSymbol -> Assignment (BoundVar (ExprBuilder t st fs)) args -> SymExpr (ExprBuilder t st fs) ret -> UnfoldPolicy -> IO (SymFn (ExprBuilder t st fs) args ret) Source # inlineDefineFun :: CurryAssignmentClass args => ExprBuilder t st fs -> SolverSymbol -> Assignment BaseTypeRepr args -> UnfoldPolicy -> CurryAssignment args (SymExpr (ExprBuilder t st fs)) (IO (SymExpr (ExprBuilder t st fs) ret)) -> IO (SymFn (ExprBuilder t st fs) args ret) Source # freshTotalUninterpFn :: ExprBuilder t st fs -> SolverSymbol -> Assignment BaseTypeRepr args -> BaseTypeRepr ret -> IO (SymFn (ExprBuilder t st fs) args ret) Source # applySymFn :: ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) args ret -> Assignment (SymExpr (ExprBuilder t st fs)) args -> IO (SymExpr (ExprBuilder t st fs) ret) Source #
IsExprBuilder (ExprBuilder t st fs) Source #
Instance details Defined in What4.Expr.Builder Methods getConfiguration :: ExprBuilder t st fs -> Config Source # setSolverLogListener :: ExprBuilder t st fs -> Maybe (SolverEvent -> IO ()) -> IO () Source # getSolverLogListener :: ExprBuilder t st fs -> IO (Maybe (SolverEvent -> IO ())) Source # logSolverEvent :: ExprBuilder t st fs -> SolverEvent -> IO () Source # getStatistics :: ExprBuilder t st fs -> IO Statistics Source # getCurrentProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc Source # setCurrentProgramLoc :: ExprBuilder t st fs -> ProgramLoc -> IO () Source # isEq :: ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> SymExpr (ExprBuilder t st fs) tp -> IO (Pred (ExprBuilder t st fs)) Source # baseTypeIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymExpr (ExprBuilder t st fs) tp -> SymExpr (ExprBuilder t st fs) tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source # annotateTerm :: ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> IO (SymAnnotation (ExprBuilder t st fs) tp, SymExpr (ExprBuilder t st fs) tp) Source # truePred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) Source # falsePred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) Source # notPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # andPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # orPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # impliesPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # xorPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # eqPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # itePred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # natLit :: ExprBuilder t st fs -> Natural -> IO (SymNat (ExprBuilder t st fs)) Source # natAdd :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (SymNat (ExprBuilder t st fs)) Source # natSub :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (SymNat (ExprBuilder t st fs)) Source # natMul :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (SymNat (ExprBuilder t st fs)) Source # natDiv :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (SymNat (ExprBuilder t st fs)) Source # natMod :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (SymNat (ExprBuilder t st fs)) Source # natIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (SymNat (ExprBuilder t st fs)) Source # natEq :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # natLe :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # natLt :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # intLit :: ExprBuilder t st fs -> Integer -> IO (SymInteger (ExprBuilder t st fs)) Source # intNeg :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # intAdd :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # intSub :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # intMul :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # intIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # intEq :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # intLe :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # intLt :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # intAbs :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # intDiv :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # intMod :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # intDivisible :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> Natural -> IO (Pred (ExprBuilder t st fs)) Source # bvLit :: 1 <= w => ExprBuilder t st fs -> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvConcat :: (1 <= u, 1 <= v) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) u -> SymBV (ExprBuilder t st fs) v -> IO (SymBV (ExprBuilder t st fs) (u + v)) Source # bvSelect :: (1 <= n, (idx + n) <= w) => ExprBuilder t st fs -> NatRepr idx -> NatRepr n -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) n) Source # bvNeg :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvAdd :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvSub :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvMul :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvUdiv :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvUrem :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvSdiv :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvSrem :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # testBitBV :: 1 <= w => ExprBuilder t st fs -> Natural -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvIsNeg :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvIte :: 1 <= w => ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvEq :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvNe :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvUlt :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvUle :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvUge :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvUgt :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvSlt :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvSgt :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvSle :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvSge :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvIsNonzero :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source # bvShl :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvLshr :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvAshr :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvRol :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvRor :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvZext :: (1 <= u, (u + 1) <= r) => ExprBuilder t st fs -> NatRepr r -> SymBV (ExprBuilder t st fs) u -> IO (SymBV (ExprBuilder t st fs) r) Source # bvSext :: (1 <= u, (u + 1) <= r) => ExprBuilder t st fs -> NatRepr r -> SymBV (ExprBuilder t st fs) u -> IO (SymBV (ExprBuilder t st fs) r) Source # bvTrunc :: (1 <= r, (r + 1) <= w) => ExprBuilder t st fs -> NatRepr r -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) r) Source # bvAndBits :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvOrBits :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvXorBits :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvNotBits :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvSet :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> Natural -> Pred (ExprBuilder t st fs) -> IO (SymBV (ExprBuilder t st fs) w) Source # bvFill :: 1 <= w => ExprBuilder t st fs -> NatRepr w -> Pred (ExprBuilder t st fs) -> IO (SymBV (ExprBuilder t st fs) w) Source # minUnsignedBV :: 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # maxUnsignedBV :: 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # maxSignedBV :: 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # minSignedBV :: 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvPopcount :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvCountLeadingZeros :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # bvCountTrailingZeros :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source # addUnsignedOF :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w) Source # addSignedOF :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w) Source # subUnsignedOF :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w) Source # subSignedOF :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w) Source # carrylessMultiply :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) (w + w)) Source # unsignedWideMultiplyBV :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w, SymBV (ExprBuilder t st fs) w) Source # mulUnsignedOF :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w) Source # signedWideMultiplyBV :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w, SymBV (ExprBuilder t st fs) w) Source # mulSignedOF :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w) Source # mkStruct :: ExprBuilder t st fs -> Assignment (SymExpr (ExprBuilder t st fs)) flds -> IO (SymStruct (ExprBuilder t st fs) flds) Source # structField :: ExprBuilder t st fs -> SymStruct (ExprBuilder t st fs) flds -> Index flds tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source # structEq :: ExprBuilder t st fs -> SymStruct (ExprBuilder t st fs) flds -> SymStruct (ExprBuilder t st fs) flds -> IO (Pred (ExprBuilder t st fs)) Source # structIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymStruct (ExprBuilder t st fs) flds -> SymStruct (ExprBuilder t st fs) flds -> IO (SymStruct (ExprBuilder t st fs) flds) Source # constantArray :: ExprBuilder t st fs -> Assignment BaseTypeRepr (idx ::> tp) -> SymExpr (ExprBuilder t st fs) b -> IO (SymArray (ExprBuilder t st fs) (idx ::> tp) b) Source # arrayFromFn :: ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) (idx ::> itp) ret -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) ret) Source # arrayMap :: ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) (ctx ::> d) r -> Assignment (ArrayResultWrapper (SymExpr (ExprBuilder t st fs)) (idx ::> itp)) (ctx ::> d) -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) r) Source # arrayUpdate :: ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (idx ::> tp) b -> Assignment (SymExpr (ExprBuilder t st fs)) (idx ::> tp) -> SymExpr (ExprBuilder t st fs) b -> IO (SymArray (ExprBuilder t st fs) (idx ::> tp) b) Source # arrayLookup :: ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (idx ::> tp) b -> Assignment (SymExpr (ExprBuilder t st fs)) (idx ::> tp) -> IO (SymExpr (ExprBuilder t st fs) b) Source # arrayFromMap :: ExprBuilder t st fs -> Assignment BaseTypeRepr (idx ::> itp) -> ArrayUpdateMap (SymExpr (ExprBuilder t st fs)) (idx ::> itp) tp -> SymExpr (ExprBuilder t st fs) tp -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) tp) Source # arrayUpdateAtIdxLits :: ExprBuilder t st fs -> ArrayUpdateMap (SymExpr (ExprBuilder t st fs)) (idx ::> itp) tp -> SymArray (ExprBuilder t st fs) (idx ::> itp) tp -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) tp) Source # arrayIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymArray (ExprBuilder t st fs) idx b -> SymArray (ExprBuilder t st fs) idx b -> IO (SymArray (ExprBuilder t st fs) idx b) Source # arrayEq :: ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) idx b -> SymArray (ExprBuilder t st fs) idx b -> IO (Pred (ExprBuilder t st fs)) Source # allTrueEntries :: ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) idx BaseBoolType -> IO (Pred (ExprBuilder t st fs)) Source # arrayTrueOnEntries :: ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) (idx ::> itp) BaseBoolType -> SymArray (ExprBuilder t st fs) (idx ::> itp) BaseBoolType -> IO (Pred (ExprBuilder t st fs)) Source # natToInteger :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # integerToReal :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # bvToNat :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymNat (ExprBuilder t st fs)) Source # bvToInteger :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymInteger (ExprBuilder t st fs)) Source # sbvToInteger :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymInteger (ExprBuilder t st fs)) Source # predToBV :: 1 <= w => ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # natToReal :: ExprBuilder t st fs -> SymNat (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # uintToReal :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymReal (ExprBuilder t st fs)) Source # sbvToReal :: 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymReal (ExprBuilder t st fs)) Source # realRound :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # realRoundEven :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # realFloor :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # realCeil :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # realTrunc :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # integerToBV :: 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # integerToNat :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> IO (SymNat (ExprBuilder t st fs)) Source # realToInteger :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # realToNat :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymNat (ExprBuilder t st fs)) Source # realToBV :: 1 <= w => ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # realToSBV :: 1 <= w => ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # clampedIntToSBV :: 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # clampedIntToBV :: 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source # intSetWidth :: (1 <= m, 1 <= n) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) m -> NatRepr n -> IO (SymBV (ExprBuilder t st fs) n) Source # uintSetWidth :: (1 <= m, 1 <= n) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) m -> NatRepr n -> IO (SymBV (ExprBuilder t st fs) n) Source # intToUInt :: (1 <= m, 1 <= n) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) m -> NatRepr n -> IO (SymBV (ExprBuilder t st fs) n) Source # uintToInt :: (1 <= m, 1 <= n) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) m -> NatRepr n -> IO (SymBV (ExprBuilder t st fs) n) Source # stringEmpty :: ExprBuilder t st fs -> StringInfoRepr si -> IO (SymString (ExprBuilder t st fs) si) Source # stringLit :: ExprBuilder t st fs -> StringLiteral si -> IO (SymString (ExprBuilder t st fs) si) Source # stringEq :: ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs)) Source # stringIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (SymString (ExprBuilder t st fs) si) Source # stringConcat :: ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (SymString (ExprBuilder t st fs) si) Source # stringContains :: ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs)) Source # stringIsPrefixOf :: ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs)) Source # stringIsSuffixOf :: ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs)) Source # stringIndexOf :: ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> SymNat (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source # stringLength :: ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> IO (SymNat (ExprBuilder t st fs)) Source # stringSubstring :: ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymNat (ExprBuilder t st fs) -> SymNat (ExprBuilder t st fs) -> IO (SymString (ExprBuilder t st fs) si) Source # realZero :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) Source # realLit :: ExprBuilder t st fs -> Rational -> IO (SymReal (ExprBuilder t st fs)) Source # sciLit :: ExprBuilder t st fs -> Scientific -> IO (SymReal (ExprBuilder t st fs)) Source # realEq :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # realNe :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # realLe :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # realLt :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # realGe :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # realGt :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # realIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realNeg :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realAdd :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realMul :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realSub :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realSq :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realDiv :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realMod :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # isInteger :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # realIsNonNeg :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # realSqrt :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realAtan2 :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realPi :: ExprBuilder t st fs -> IO (SymReal (ExprBuilder t st fs)) Source # realLog :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realExp :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realSin :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realCos :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realTan :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realSinh :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realCosh :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realTanh :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realAbs :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # realHypot :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # floatPZero :: ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatNZero :: ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatNaN :: ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatPInf :: ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatNInf :: ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatLit :: ExprBuilder t st fs -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatNeg :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatAbs :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatSqrt :: ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatAdd :: ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatSub :: ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatMul :: ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatDiv :: ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatRem :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatMin :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatMax :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatFMA :: ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatEq :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatNe :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatFpEq :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatFpNe :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatLe :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatLt :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatGe :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatGt :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatIsNaN :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatIsInf :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatIsZero :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatIsPos :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatIsNeg :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatIsSubnorm :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatIsNorm :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source # floatIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatCast :: ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp' -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatRound :: ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatFromBinary :: (2 <= eb, 2 <= sb) => ExprBuilder t st fs -> FloatPrecisionRepr (FloatingPointPrecision eb sb) -> SymBV (ExprBuilder t st fs) (eb + sb) -> IO (SymFloat (ExprBuilder t st fs) (FloatingPointPrecision eb sb)) Source # floatToBinary :: (2 <= eb, 2 <= sb) => ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) (FloatingPointPrecision eb sb) -> IO (SymBV (ExprBuilder t st fs) (eb + sb)) Source # bvToFloat :: 1 <= w => ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV (ExprBuilder t st fs) w -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # sbvToFloat :: 1 <= w => ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV (ExprBuilder t st fs) w -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # realToFloat :: ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymReal (ExprBuilder t st fs) -> IO (SymFloat (ExprBuilder t st fs) fpp) Source # floatToBV :: 1 <= w => ExprBuilder t st fs -> NatRepr w -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymBV (ExprBuilder t st fs) w) Source # floatToSBV :: 1 <= w => ExprBuilder t st fs -> NatRepr w -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymBV (ExprBuilder t st fs) w) Source # floatToReal :: ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymReal (ExprBuilder t st fs)) Source # mkComplex :: ExprBuilder t st fs -> Complex (SymReal (ExprBuilder t st fs)) -> IO (SymCplx (ExprBuilder t st fs)) Source # getRealPart :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # getImagPart :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # cplxGetParts :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (Complex (SymReal (ExprBuilder t st fs))) Source # mkComplexLit :: ExprBuilder t st fs -> Complex Rational -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxFromReal :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxNeg :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxAdd :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxSub :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxMul :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxMag :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source # cplxSqrt :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxSin :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxCos :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxTan :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxHypot :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxRound :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxFloor :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxCeil :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxConj :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxExp :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs)) Source # cplxEq :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source # cplxNe :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source #
IsInterpretedFloatExprBuilder (ExprBuilder t st fs) => IsInterpretedFloatSymExprBuilder (ExprBuilder t st fs) Source #
Instance details Defined in What4.Expr.Builder Methods freshFloatConstant :: ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi)) Source # freshFloatLatch :: ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi)) Source # freshFloatBoundVar :: ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (BoundVar (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi)) Source #
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatIEEE) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatIEEE) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatIEEE) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatNe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatLe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatLt :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatGe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatGt :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIte :: ExprBuilder t st (Flags FloatIEEE) -> Pred (ExprBuilder t st (Flags FloatIEEE)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatIEEE)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatIEEE)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatIEEE)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatIEEE)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi) Source #
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpreted)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatUninterpreted) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatUninterpreted) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatUninterpreted) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatNe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatLe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatLt :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatGe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatGt :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIte :: ExprBuilder t st (Flags FloatUninterpreted) -> Pred (ExprBuilder t st (Flags FloatUninterpreted)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatUninterpreted)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatReal)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatReal) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatReal) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatReal) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatNe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatLe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatLt :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatGe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatGt :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIte :: ExprBuilder t st (Flags FloatReal) -> Pred (ExprBuilder t st (Flags FloatReal)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatReal)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatReal)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatReal)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatReal)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatReal))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi) Source #
MatlabSymbolicArrayBuilder (ExprBuilder t st fs) Source #
Instance details Defined in What4.Expr.Builder Methods mkMatlabSolverFn :: ExprBuilder t st fs -> MatlabSolverFn (SymExpr (ExprBuilder t st fs)) args ret -> IO (SymFn (ExprBuilder t st fs) args ret) Source #
type SymFn (ExprBuilder t st fs) Source #
Instance details Defined in What4.Expr.Builder type SymFn (ExprBuilder t st fs) = ExprSymFn t (Expr t)
type SymAnnotation (ExprBuilder t st fs) Source #
Instance details Defined in What4.Expr.Builder type SymAnnotation (ExprBuilder t st fs) = (Nonce t :: BaseType -> Type)
type BoundVar (ExprBuilder t st fs) Source #
Instance details Defined in What4.Expr.Builder type BoundVar (ExprBuilder t st fs) = ExprBoundVar t
type SymExpr (ExprBuilder t st fs) Source #
Instance details Defined in What4.Expr.Builder type SymExpr (ExprBuilder t st fs) = Expr t
type SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi = BaseFloatType (FloatInfoToPrecision fi)
type SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi = BaseBVType (FloatInfoToBitWidth fi)
type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi = BaseRealType

newExprBuilder Source #

Arguments

:: FloatModeRepr fm	Float interpretation mode (i.e., how are floats translated for the solver).
-> st t	Current state for simple builder.
-> NonceGenerator IO t	Nonce generator for names
-> IO (ExprBuilder t st (Flags fm))

Flags

data FloatMode Source #

Mode flag for how floating-point values should be interpreted.

Instances

TestEquality FloatModeRepr Source #
Instance details Defined in What4.Expr.Builder Methods testEquality :: FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) #
ShowF FloatModeRepr Source #
Instance details Defined in What4.Expr.Builder Methods withShow :: p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) -> a) -> a # showF :: FloatModeRepr tp -> String # showsPrecF :: Int -> FloatModeRepr tp -> String -> String #
KnownRepr FloatModeRepr FloatReal Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatReal #
KnownRepr FloatModeRepr FloatUninterpreted Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatUninterpreted #
KnownRepr FloatModeRepr FloatIEEE Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatIEEE #

data FloatModeRepr :: FloatMode -> Type where Source #

Constructors

FloatIEEERepr :: FloatModeRepr FloatIEEE
FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted
FloatRealRepr :: FloatModeRepr FloatReal

Instances

TestEquality FloatModeRepr Source #
Instance details Defined in What4.Expr.Builder Methods testEquality :: FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) #
ShowF FloatModeRepr Source #
Instance details Defined in What4.Expr.Builder Methods withShow :: p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) -> a) -> a # showF :: FloatModeRepr tp -> String # showsPrecF :: Int -> FloatModeRepr tp -> String -> String #
KnownRepr FloatModeRepr FloatReal Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatReal #
KnownRepr FloatModeRepr FloatUninterpreted Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatUninterpreted #
KnownRepr FloatModeRepr FloatIEEE Source #
Instance details Defined in What4.Expr.Builder Methods knownRepr :: FloatModeRepr FloatIEEE #
Show (FloatModeRepr fm) Source #
Instance details Defined in What4.Expr.Builder Methods showsPrec :: Int -> FloatModeRepr fm -> ShowS # show :: FloatModeRepr fm -> String # showList :: [FloatModeRepr fm] -> ShowS #

type FloatIEEE = FloatIEEE Source #

type FloatUninterpreted = FloatUninterpreted Source #

type FloatReal = FloatReal Source #

data Flags (fi :: FloatMode) Source #

Instances

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatIEEE) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatIEEE) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatIEEE) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatNe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatLe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatLt :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatGe :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatGt :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatIte :: ExprBuilder t st (Flags FloatIEEE) -> Pred (ExprBuilder t st (Flags FloatIEEE)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatIEEE)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatIEEE)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatIEEE)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatIEEE)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatIEEE) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatIEEE)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatIEEE))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi) Source #
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpreted)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatUninterpreted) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatUninterpreted) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatUninterpreted) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatNe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatLe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatLt :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatGe :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatGt :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatIte :: ExprBuilder t st (Flags FloatUninterpreted) -> Pred (ExprBuilder t st (Flags FloatUninterpreted)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatUninterpreted)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatUninterpreted) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatUninterpreted)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatUninterpreted))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatReal)) Source #
Instance details Defined in What4.Expr.Builder Methods iFloatPZero :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNZero :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNaN :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatPInf :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatNInf :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatLit :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatLitSingle :: ExprBuilder t st (Flags FloatReal) -> Float -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) SingleFloat) Source # iFloatLitDouble :: ExprBuilder t st (Flags FloatReal) -> Double -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) DoubleFloat) Source # iFloatLitLongDouble :: ExprBuilder t st (Flags FloatReal) -> X86_80Val -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) X86_80Float) Source # iFloatNeg :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatAbs :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatSqrt :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatAdd :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatSub :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMul :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatDiv :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatRem :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMin :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatMax :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatFMA :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatEq :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatNe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatFpEq :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatFpNe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatLe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatLt :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatGe :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatGt :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNaN :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsInf :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsZero :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsPos :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNeg :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsSubnorm :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIsNorm :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source # iFloatIte :: ExprBuilder t st (Flags FloatReal) -> Pred (ExprBuilder t st (Flags FloatReal)) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatCast :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi' -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatRound :: ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatFromBinary :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SymBV (ExprBuilder t st (Flags FloatReal)) (FloatInfoToBitWidth fi) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatToBinary :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) (FloatInfoToBitWidth fi)) Source # iBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatReal)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iSBVToFloat :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymBV (ExprBuilder t st (Flags FloatReal)) w -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iRealToFloat :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatReal)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source # iFloatToBV :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) w) Source # iFloatToSBV :: 1 <= w => ExprBuilder t st (Flags FloatReal) -> NatRepr w -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymBV (ExprBuilder t st (Flags FloatReal)) w) Source # iFloatToReal :: ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatReal))) Source # iFloatBaseTypeRepr :: ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi) Source #
type SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi = BaseFloatType (FloatInfoToPrecision fi)
type SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi = BaseBVType (FloatInfoToBitWidth fi)
type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi Source #
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi = BaseRealType

Type abbreviations

type BoolExpr t = Expr t BaseBoolType Source #

type NatExpr t = Expr t BaseNatType Source #

type IntegerExpr t = Expr t BaseIntegerType Source #

type RealExpr t = Expr t BaseRealType Source #

type BVExpr t n = Expr t (BaseBVType n) Source #

type CplxExpr t = Expr t BaseComplexType Source #

type StringExpr t si = Expr t (BaseStringType si) Source #

Expression datatypes

data Expr t (tp :: BaseType) where Source #

The main ExprBuilder expression datastructure. The non-trivial Expr values constructed by this module are uniquely identified by a nonce value that is used to explicitly represent sub-term sharing. When traversing the structure of an Expr it is usually very important to memoize computations based on the values of these identifiers to avoid exponential blowups due to shared term structure.

Type parameter t is a phantom type brand used to relate nonces to a specific nonce generator (similar to the s parameter of the ST monad). The type index tp of kind BaseType indicates the type of the values denoted by the given expression.

Type Expr t instantiates the type family SymExpr (ExprBuilder t st).

Constructors

SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr)
BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si)
AppExpr :: !(AppExpr t tp) -> Expr t tp
NonceAppExpr :: !(NonceAppExpr t tp) -> Expr t tp
BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp

Instances

TestEquality (Expr t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.Builder Methods testEquality :: Expr t a -> Expr t b -> Maybe (a :~: b) #
OrdF (Expr t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.Builder Methods compareF :: Expr t x -> Expr t y -> OrderingF x y # leqF :: Expr t x -> Expr t y -> Bool # ltF :: Expr t x -> Expr t y -> Bool # geqF :: Expr t x -> Expr t y -> Bool # gtF :: Expr t x -> Expr t y -> Bool #
ShowF (Expr t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.Builder Methods withShow :: p (Expr t) -> q tp -> (Show (Expr t tp) -> a) -> a # showF :: Expr t tp -> String # showsPrecF :: Int -> Expr t tp -> String -> String #
HashableF (Expr t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.Builder Methods hashWithSaltF :: Int -> Expr t tp -> Int # hashF :: Expr t tp -> Int #
HasAbsValue (Expr t) Source #
Instance details Defined in What4.Expr.Builder Methods getAbsValue :: Expr t tp -> AbstractValue tp Source #
IsExpr (Expr t) Source #
Instance details Defined in What4.Expr.Builder Methods asConstantPred :: Expr t BaseBoolType -> Maybe Bool Source # asNat :: Expr t BaseNatType -> Maybe Natural Source # natBounds :: Expr t BaseNatType -> NatValueRange Source # asInteger :: Expr t BaseIntegerType -> Maybe Integer Source # integerBounds :: Expr t BaseIntegerType -> ValueRange Integer Source # asRational :: Expr t BaseRealType -> Maybe Rational Source # rationalBounds :: Expr t BaseRealType -> ValueRange Rational Source # asComplex :: Expr t BaseComplexType -> Maybe (Complex Rational) Source # asBV :: Expr t (BaseBVType w) -> Maybe (BV w) Source # unsignedBVBounds :: 1 <= w => Expr t (BaseBVType w) -> Maybe (Integer, Integer) Source # signedBVBounds :: 1 <= w => Expr t (BaseBVType w) -> Maybe (Integer, Integer) Source # asAffineVar :: Expr t tp -> Maybe (ConcreteVal tp, Expr t tp, ConcreteVal tp) Source # asString :: Expr t (BaseStringType si) -> Maybe (StringLiteral si) Source # stringInfo :: Expr t (BaseStringType si) -> StringInfoRepr si Source # asConstantArray :: Expr t (BaseArrayType idx bt) -> Maybe (Expr t bt) Source # asStruct :: Expr t (BaseStructType flds) -> Maybe (Assignment (Expr t) flds) Source # exprType :: Expr t tp -> BaseTypeRepr tp Source # bvWidth :: Expr t (BaseBVType w) -> NatRepr w Source # printSymExpr :: Expr t tp -> Doc Source #
Eq (Expr t tp) Source #
Instance details Defined in What4.Expr.Builder Methods (==) :: Expr t tp -> Expr t tp -> Bool # (/=) :: Expr t tp -> Expr t tp -> Bool #
Ord (Expr t tp) Source #
Instance details Defined in What4.Expr.Builder Methods compare :: Expr t tp -> Expr t tp -> Ordering # (<) :: Expr t tp -> Expr t tp -> Bool # (<=) :: Expr t tp -> Expr t tp -> Bool # (>) :: Expr t tp -> Expr t tp -> Bool # (>=) :: Expr t tp -> Expr t tp -> Bool # max :: Expr t tp -> Expr t tp -> Expr t tp # min :: Expr t tp -> Expr t tp -> Expr t tp #
Show (Expr t tp) Source #
Instance details Defined in What4.Expr.Builder Methods showsPrec :: Int -> Expr t tp -> ShowS # show :: Expr t tp -> String # showList :: [Expr t tp] -> ShowS #
Pretty (Expr t tp) Source #
Instance details Defined in What4.Expr.Builder Methods pretty :: Expr t tp -> Doc # prettyList :: [Expr t tp] -> Doc #
Hashable (Expr t tp) Source #
Instance details Defined in What4.Expr.Builder Methods hashWithSalt :: Int -> Expr t tp -> Int # hash :: Expr t tp -> Int #
PolyEq (Expr t x) (Expr t y) Source #
Instance details Defined in What4.Expr.Builder Methods polyEqF :: Expr t x -> Expr t y -> Maybe (Expr t x :~: Expr t y) # polyEq :: Expr t x -> Expr t y -> Bool #

exprLoc :: Expr t tp -> ProgramLoc Source #

ppExpr :: Expr t tp -> Doc Source #

Pretty print an Expr using let bindings to create the term.

App expressions

data AppExpr t (tp :: BaseType) Source #

This type represents Expr values that were built from an App.

Parameter t is a phantom type brand used to track nonces.

Selector functions are provided to destruct AppExpr values, but the constructor is kept hidden. The preferred way to construct an Expr from an App is to use sbMakeExpr.

appExprId :: AppExpr t tp -> Nonce t tp Source #

appExprLoc :: AppExpr t tp -> ProgramLoc Source #

appExprApp :: AppExpr t tp -> App (Expr t) tp Source #

data App (e :: BaseType -> Type) (tp :: BaseType) where Source #

Type App e tp encodes the top-level application of an Expr expression. It includes first-order expression forms that do not bind variables (contrast with NonceApp).

Parameter e is used everywhere a recursive sub-expression would go. Uses of the App type will tie the knot through this parameter. Parameter tp indicates the type of the expression.

Constructors

BaseIte :: !(BaseTypeRepr tp) -> !Integer -> !(e BaseBoolType) -> !(e tp) -> !(e tp) -> App e tp
BaseEq :: !(BaseTypeRepr tp) -> !(e tp) -> !(e tp) -> App e BaseBoolType
NotPred :: !(e BaseBoolType) -> App e BaseBoolType
ConjPred :: !(BoolMap e) -> App e BaseBoolType
SemiRingSum :: !(WeightedSum e sr) -> App e (SemiRingBase sr)
SemiRingProd :: !(SemiRingProduct e sr) -> App e (SemiRingBase sr)
SemiRingLe :: !(OrderedSemiRingRepr sr) -> !(e (SemiRingBase sr)) -> !(e (SemiRingBase sr)) -> App e BaseBoolType
RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType
NatDiv :: !(e BaseNatType) -> !(e BaseNatType) -> App e BaseNatType
NatMod :: !(e BaseNatType) -> !(e BaseNatType) -> App e BaseNatType
IntDiv :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
IntMod :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
IntAbs :: !(e BaseIntegerType) -> App e BaseIntegerType
IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType
RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
RealSqrt :: !(e BaseRealType) -> App e BaseRealType
Pi :: App e BaseRealType
RealSin :: !(e BaseRealType) -> App e BaseRealType
RealCos :: !(e BaseRealType) -> App e BaseRealType
RealATan2 :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
RealSinh :: !(e BaseRealType) -> App e BaseRealType
RealCosh :: !(e BaseRealType) -> App e BaseRealType
RealExp :: !(e BaseRealType) -> App e BaseRealType
RealLog :: !(e BaseRealType) -> App e BaseRealType
BVTestBit :: 1 <= w => !Natural -> !(e (BaseBVType w)) -> App e BaseBoolType
BVSlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
BVUlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
BVOrBits :: 1 <= w => !(NatRepr w) -> !(BVOrSet e w) -> App e (BaseBVType w)
BVUnaryTerm :: 1 <= n => !(UnaryBV (e BaseBoolType) n) -> App e (BaseBVType n)
BVConcat :: (1 <= u, 1 <= v, 1 <= (u + v)) => !(NatRepr (u + v)) -> !(e (BaseBVType u)) -> !(e (BaseBVType v)) -> App e (BaseBVType (u + v))
BVSelect :: (1 <= n, (idx + n) <= w) => !(NatRepr idx) -> !(NatRepr n) -> !(e (BaseBVType w)) -> App e (BaseBVType n)
BVFill :: 1 <= w => !(NatRepr w) -> !(e BaseBoolType) -> App e (BaseBVType w)
BVUdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVUrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVSdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVSrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVShl :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVLshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVAshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVRol :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVRor :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVZext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r)
BVSext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r)
BVPopcount :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVCountTrailingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
BVCountLeadingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
FloatPZero :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
FloatNZero :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
FloatNaN :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
FloatPInf :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
FloatNInf :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
FloatNeg :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatAbs :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatSqrt :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatAdd :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatSub :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatMul :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatDiv :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatRem :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatMin :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatMax :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatFMA :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatFpEq :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatFpNe :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatLe :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatLt :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatIsNaN :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatIsInf :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatIsZero :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatIsPos :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatIsNeg :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatIsSubnorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatIsNorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
FloatCast :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp')) -> App e (BaseFloatType fpp)
FloatRound :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
FloatFromBinary :: (2 <= eb, 2 <= sb) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseBVType (eb + sb))) -> App e (BaseFloatType (FloatingPointPrecision eb sb))
FloatToBinary :: (2 <= eb, 2 <= sb, 1 <= (eb + sb)) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseFloatType (FloatingPointPrecision eb sb))) -> App e (BaseBVType (eb + sb))
BVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp)
SBVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp)
RealToFloat :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e BaseRealType) -> App e (BaseFloatType fpp)
FloatToBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w)
FloatToSBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w)
FloatToReal :: !(e (BaseFloatType fpp)) -> App e BaseRealType
ArrayMap :: !(Assignment BaseTypeRepr (i ::> itp)) -> !(BaseTypeRepr tp) -> !(ArrayUpdateMap e (i ::> itp) tp) -> !(e (BaseArrayType (i ::> itp) tp)) -> App e (BaseArrayType (i ::> itp) tp)
ConstantArray :: !(Assignment BaseTypeRepr (i ::> tp)) -> !(BaseTypeRepr b) -> !(e b) -> App e (BaseArrayType (i ::> tp) b)
UpdateArray :: !(BaseTypeRepr b) -> !(Assignment BaseTypeRepr (i ::> tp)) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> !(e b) -> App e (BaseArrayType (i ::> tp) b)
SelectArray :: !(BaseTypeRepr b) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> App e b
NatToInteger :: !(e BaseNatType) -> App e BaseIntegerType
IntegerToNat :: !(e BaseIntegerType) -> App e BaseNatType
IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType
RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType
BVToNat :: 1 <= w => !(e (BaseBVType w)) -> App e BaseNatType
BVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
SBVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
IntegerToBV :: 1 <= w => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)
RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType
FloorReal :: !(e BaseRealType) -> App e BaseIntegerType
CeilReal :: !(e BaseRealType) -> App e BaseIntegerType
Cplx :: !(Complex (e BaseRealType)) -> App e BaseComplexType
RealPart :: !(e BaseComplexType) -> App e BaseRealType
ImagPart :: !(e BaseComplexType) -> App e BaseRealType
StringContains :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
StringIsPrefixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
StringIsSuffixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
StringIndexOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> !(e BaseNatType) -> App e BaseIntegerType
StringSubstring :: !(StringInfoRepr si) -> !(e (BaseStringType si)) -> !(e BaseNatType) -> !(e BaseNatType) -> App e (BaseStringType si)
StringAppend :: !(StringInfoRepr si) -> !(StringSeq e si) -> App e (BaseStringType si)
StringLength :: !(e (BaseStringType si)) -> App e BaseNatType
StructCtor :: !(Assignment BaseTypeRepr flds) -> !(Assignment e flds) -> App e (BaseStructType flds)
StructField :: !(e (BaseStructType flds)) -> !(Index flds tp) -> !(BaseTypeRepr tp) -> App e tp

Instances

FoldableFC App Source #
Instance details Defined in What4.Expr.App Methods foldMapFC :: Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). App f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App f x -> b # foldlFC :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App f x -> b # foldlFC' :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). App f x -> [a] #
(Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => TestEquality (App e :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods testEquality :: App e a -> App e b -> Maybe (a :~: b) #
(OrdF e, HashableF e, HasAbsValue e, Hashable (e BaseBoolType), Hashable (e BaseRealType)) => HashableF (App e :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: Int -> App e tp -> Int # hashF :: App e tp -> Int #
(Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => Eq (App e tp) Source #
Instance details Defined in What4.Expr.App Methods (==) :: App e tp -> App e tp -> Bool # (/=) :: App e tp -> App e tp -> Bool #
ShowF e => Show (App e u) Source #
Instance details Defined in What4.Expr.App Methods showsPrec :: Int -> App e u -> ShowS # show :: App e u -> String # showList :: [App e u] -> ShowS #
ShowF e => Pretty (App e u) Source #
Instance details Defined in What4.Expr.App Methods pretty :: App e u -> Doc # prettyList :: [App e u] -> Doc #

NonceApp expressions

data NonceAppExpr t (tp :: BaseType) Source #

This type represents Expr values that were built from a NonceApp.

Parameter t is a phantom type brand used to track nonces.

Selector functions are provided to destruct NonceAppExpr values, but the constructor is kept hidden. The preferred way to construct an Expr from a NonceApp is to use sbNonceExpr.

Instances

TestEquality (NonceAppExpr t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.Builder Methods testEquality :: NonceAppExpr t a -> NonceAppExpr t b -> Maybe (a :~: b) #
OrdF (NonceAppExpr t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.Builder Methods compareF :: NonceAppExpr t x -> NonceAppExpr t y -> OrderingF x y # leqF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool # ltF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool # geqF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool # gtF :: NonceAppExpr t x -> NonceAppExpr t y -> Bool #
Eq (NonceAppExpr t tp) Source #
Instance details Defined in What4.Expr.Builder Methods (==) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool # (/=) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool #
Ord (NonceAppExpr t tp) Source #
Instance details Defined in What4.Expr.Builder Methods compare :: NonceAppExpr t tp -> NonceAppExpr t tp -> Ordering # (<) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool # (<=) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool # (>) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool # (>=) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool # max :: NonceAppExpr t tp -> NonceAppExpr t tp -> NonceAppExpr t tp # min :: NonceAppExpr t tp -> NonceAppExpr t tp -> NonceAppExpr t tp #

nonceExprId :: NonceAppExpr t tp -> Nonce t tp Source #

nonceExprLoc :: NonceAppExpr t tp -> ProgramLoc Source #

nonceExprApp :: NonceAppExpr t tp -> NonceApp t (Expr t) tp Source #

data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where Source #

Type NonceApp t e tp encodes the top-level application of an Expr. It includes expression forms that bind variables (contrast with App).

Parameter t is a phantom type brand used to track nonces. Parameter e is used everywhere a recursive sub-expression would go. Uses of the NonceApp type will tie the knot through this parameter. Parameter tp indicates the type of the expression.

Constructors

Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp
Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
ArrayFromFn :: !(ExprSymFn t e (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret)
MapOverArrays :: !(ExprSymFn t e (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r)
ArrayTrueOnEntries :: !(ExprSymFn t e (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType
FnApp :: !(ExprSymFn t e args ret) -> !(Assignment e args) -> NonceApp t e ret

Instances

FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). NonceApp t f x -> NonceApp t g x #
FoldableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods foldMapFC :: Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). NonceApp t f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> NonceApp t f x -> b # foldlFC :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> NonceApp t f x -> b # foldlFC' :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). NonceApp t f x -> [a] #
TraversableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods traverseFC :: Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). NonceApp t f x -> m (NonceApp t g x) #
TestEquality e => TestEquality (NonceApp t e :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods testEquality :: NonceApp t e a -> NonceApp t e b -> Maybe (a :~: b) #
HashableF e => HashableF (NonceApp t e :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: Int -> NonceApp t e tp -> Int # hashF :: NonceApp t e tp -> Int #
TestEquality e => Eq (NonceApp t e tp) Source #
Instance details Defined in What4.Expr.App Methods (==) :: NonceApp t e tp -> NonceApp t e tp -> Bool # (/=) :: NonceApp t e tp -> NonceApp t e tp -> Bool #

Bound variables

data ExprBoundVar t (tp :: BaseType) Source #

Information about bound variables. Parameter t is a phantom type brand used to track nonces.

Type ExprBoundVar t instantiates the type family BoundVar (ExprBuilder t st).

Selector functions are provided to destruct ExprBoundVar values, but the constructor is kept hidden. The preferred way to construct a ExprBoundVar is to use freshBoundVar.

Instances

TestEquality (ExprBoundVar t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods testEquality :: ExprBoundVar t a -> ExprBoundVar t b -> Maybe (a :~: b) #
OrdF (ExprBoundVar t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods compareF :: ExprBoundVar t x -> ExprBoundVar t y -> OrderingF x y # leqF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool # ltF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool # geqF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool # gtF :: ExprBoundVar t x -> ExprBoundVar t y -> Bool #
ShowF (ExprBoundVar t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods withShow :: p (ExprBoundVar t) -> q tp -> (Show (ExprBoundVar t tp) -> a) -> a # showF :: ExprBoundVar t tp -> String # showsPrecF :: Int -> ExprBoundVar t tp -> String -> String #
HashableF (ExprBoundVar t :: BaseType -> Type) Source #
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: Int -> ExprBoundVar t tp -> Int # hashF :: ExprBoundVar t tp -> Int #
Eq (ExprBoundVar t tp) Source #
Instance details Defined in What4.Expr.App Methods (==) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool # (/=) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool #
Ord (ExprBoundVar t tp) Source #
Instance details Defined in What4.Expr.App Methods compare :: ExprBoundVar t tp -> ExprBoundVar t tp -> Ordering # (<) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool # (<=) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool # (>) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool # (>=) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool # max :: ExprBoundVar t tp -> ExprBoundVar t tp -> ExprBoundVar t tp # min :: ExprBoundVar t tp -> ExprBoundVar t tp -> ExprBoundVar t tp #
Show (ExprBoundVar t tp) Source #
Instance details Defined in What4.Expr.App Methods showsPrec :: Int -> ExprBoundVar t tp -> ShowS # show :: ExprBoundVar t tp -> String # showList :: [ExprBoundVar t tp] -> ShowS #
Hashable (ExprBoundVar t tp) Source #
Instance details Defined in What4.Expr.App Methods hashWithSalt :: Int -> ExprBoundVar t tp -> Int # hash :: ExprBoundVar t tp -> Int #

bvarId :: ExprBoundVar t tp -> Nonce t tp Source #

bvarLoc :: ExprBoundVar t tp -> ProgramLoc Source #

bvarName :: ExprBoundVar t tp -> SolverSymbol Source #

bvarKind :: ExprBoundVar t tp -> VarKind Source #

data VarKind Source #

The Kind of a bound variable.

Constructors

QuantifierVarKind	A variable appearing in a quantifier.
LatchVarKind	A variable appearing as a latch input.
UninterpVarKind	A variable appearing in a uninterpreted constant

boundVars :: Expr t tp -> ST s (BoundVarMap s t) Source #

Symbolic functions

data ExprSymFn t e (args :: Ctx BaseType) (ret :: BaseType) Source #

This represents a symbolic function in the simulator. Parameter t is a phantom type brand used to track nonces. Parameter e is used everywhere a recursive sub-expression would go. The args and ret parameters define the types of arguments and the return type of the function.

Type ExprSymFn t (Expr t) instantiates the type family SymFn (ExprBuilder t st).

Constructors

ExprSymFn
Fields symFnId :: !(Nonce t (args ::> ret)) symFnName :: !SolverSymbol symFnInfo :: !(SymFnInfo t e args ret) symFnLoc :: !ProgramLoc

Instances

IsExpr e => IsSymFn (ExprSymFn t e) Source #
Instance details Defined in What4.Expr.App Methods fnArgTypes :: ExprSymFn t e args ret -> Assignment BaseTypeRepr args Source # fnReturnType :: ExprSymFn t e args ret -> BaseTypeRepr ret Source #
Show (ExprSymFn t e args ret) Source #
Instance details Defined in What4.Expr.App Methods showsPrec :: Int -> ExprSymFn t e args ret -> ShowS # show :: ExprSymFn t e args ret -> String # showList :: [ExprSymFn t e args ret] -> ShowS #
Hashable (ExprSymFn t e args tp) Source #
Instance details Defined in What4.Expr.App Methods hashWithSalt :: Int -> ExprSymFn t e args tp -> Int # hash :: ExprSymFn t e args tp -> Int #

data SymFnInfo t e (args :: Ctx BaseType) (ret :: BaseType) Source #

This describes information about an undefined or defined function. Parameter t is a phantom type brand used to track nonces. Parameter e is used everywhere a recursive sub-expression would go. The args and ret parameters define the types of arguments and the return type of the function.

Constructors

UninterpFnInfo !(Assignment BaseTypeRepr args) !(BaseTypeRepr ret)	Information about the argument type and return type of an uninterpreted function.
DefinedFnInfo !(Assignment (ExprBoundVar t) args) !(e ret) !UnfoldPolicy	Information about a defined function. Includes bound variables and an expression associated to a defined function, as well as a policy for when to unfold the body.
MatlabSolverFnInfo !(MatlabSolverFn e args ret) !(Assignment (ExprBoundVar t) args) !(e ret)	This is a function that corresponds to a matlab solver function. It includes the definition as a ExprBuilder expr to enable export to other solvers.

symFnArgTypes :: ExprSymFn t e args ret -> Assignment BaseTypeRepr args Source #

symFnReturnType :: IsExpr e => ExprSymFn t e args ret -> BaseTypeRepr ret Source #

Semirings

type family Coefficient (sr :: SemiRing) :: Type where ... Source #

The constant values in the semiring.

Equations

Coefficient SemiRingNat = Natural
Coefficient SemiRingInteger = Integer
Coefficient SemiRingReal = Rational
Coefficient (SemiRingBV fv w) = BV w

data SemiRing Source #

Data-kind representing the semirings What4 supports.

Instances

TestEquality OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) #
TestEquality SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) #
OrdF OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> OrderingF x y # leqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # ltF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # geqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # gtF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #
OrdF SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: SemiRingRepr x -> SemiRingRepr y -> OrderingF x y # leqF :: SemiRingRepr x -> SemiRingRepr y -> Bool # ltF :: SemiRingRepr x -> SemiRingRepr y -> Bool # geqF :: SemiRingRepr x -> SemiRingRepr y -> Bool # gtF :: SemiRingRepr x -> SemiRingRepr y -> Bool #
HashableF OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: Int -> OrderedSemiRingRepr tp -> Int # hashF :: OrderedSemiRingRepr tp -> Int #
HashableF SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: Int -> SemiRingRepr tp -> Int # hashF :: SemiRingRepr tp -> Int #
OrdF f => TestEquality (SemiRingProduct f :: SemiRing -> Type) Source #
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: SemiRingProduct f a -> SemiRingProduct f b -> Maybe (a :~: b) #
OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source #
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) #

data BVFlavor Source #

Data-kind indicating the two flavors of bitvector semirings. The ordinary arithmetic semiring consists of addition and multiplication, and the "bits" semiring consists of bitwise xor and bitwise and.

Instances

TestEquality BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) #
OrdF BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: BVFlavorRepr x -> BVFlavorRepr y -> OrderingF x y # leqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # ltF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # geqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # gtF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool #
HashableF BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: Int -> BVFlavorRepr tp -> Int # hashF :: BVFlavorRepr tp -> Int #

data SemiRingRepr (sr :: SemiRing) where Source #

Constructors

SemiRingNatRepr :: SemiRingRepr SemiRingNat
SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger
SemiRingRealRepr :: SemiRingRepr SemiRingReal
SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)

Instances

TestEquality SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) #
OrdF SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: SemiRingRepr x -> SemiRingRepr y -> OrderingF x y # leqF :: SemiRingRepr x -> SemiRingRepr y -> Bool # ltF :: SemiRingRepr x -> SemiRingRepr y -> Bool # geqF :: SemiRingRepr x -> SemiRingRepr y -> Bool # gtF :: SemiRingRepr x -> SemiRingRepr y -> Bool #
HashableF SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: Int -> SemiRingRepr tp -> Int # hashF :: SemiRingRepr tp -> Int #
Hashable (SemiRingRepr sr) Source #
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> SemiRingRepr sr -> Int # hash :: SemiRingRepr sr -> Int #

data BVFlavorRepr (fv :: BVFlavor) where Source #

Constructors

BVArithRepr :: BVFlavorRepr BVArith
BVBitsRepr :: BVFlavorRepr BVBits

Instances

TestEquality BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) #
OrdF BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: BVFlavorRepr x -> BVFlavorRepr y -> OrderingF x y # leqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # ltF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # geqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # gtF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool #
HashableF BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: Int -> BVFlavorRepr tp -> Int # hashF :: BVFlavorRepr tp -> Int #
Hashable (BVFlavorRepr fv) Source #
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> BVFlavorRepr fv -> Int # hash :: BVFlavorRepr fv -> Int #

data OrderedSemiRingRepr (sr :: SemiRing) where Source #

The subset of semirings that are equipped with an appropriate (order-respecting) total order.

Constructors

OrderedSemiRingNatRepr :: OrderedSemiRingRepr SemiRingNat
OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger
OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal

Instances

TestEquality OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) #
OrdF OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> OrderingF x y # leqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # ltF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # geqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # gtF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #
HashableF OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: Int -> OrderedSemiRingRepr tp -> Int # hashF :: OrderedSemiRingRepr tp -> Int #
Hashable (OrderedSemiRingRepr sr) Source #
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> OrderedSemiRingRepr sr -> Int # hash :: OrderedSemiRingRepr sr -> Int #

data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing) Source #

A weighted sum of semiring values. Mathematically, this represents an affine operation on the underlying expressions.

Instances

OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source #
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) #
OrdF f => Hashable (WeightedSum f sr) Source #
Instance details Defined in What4.Expr.WeightedSum Methods hashWithSalt :: Int -> WeightedSum f sr -> Int # hash :: WeightedSum f sr -> Int #

Unary BV

data UnaryBV p (n :: Nat) Source #

A unary bitvector encoding where the map contains predicates such as u^.unaryBVMap^.at i holds iff the value represented by u is less than or equal to i.

The map stored in the representation should always have a single element, and the largest integer stored in the map should be associated with a predicate representing "true". This means that if the map contains only a single binding, then it represents a constant.

Instances

Eq p => TestEquality (UnaryBV p :: Nat -> Type) Source #
Instance details Defined in What4.Expr.UnaryBV Methods testEquality :: UnaryBV p a -> UnaryBV p b -> Maybe (a :~: b) #
Hashable p => Hashable (UnaryBV p n) Source #
Instance details Defined in What4.Expr.UnaryBV Methods hashWithSalt :: Int -> UnaryBV p n -> Int # hash :: UnaryBV p n -> Int #

Logic theories

data AppTheory Source #

The theory that a symbol belongs to.

Constructors

BoolTheory
LinearArithTheory
NonlinearArithTheory
ComputableArithTheory
BitvectorTheory
QuantifierTheory
StringTheory
FloatingPointTheory
ArrayTheory
StructTheory	Theory attributed to structs (equivalent to records in CVC4/Z3, tuples in Yices)
FnTheory	Theory attributed application functions.

Instances

Eq AppTheory Source #
Instance details Defined in What4.Expr.AppTheory Methods (==) :: AppTheory -> AppTheory -> Bool # (/=) :: AppTheory -> AppTheory -> Bool #
Ord AppTheory Source #
Instance details Defined in What4.Expr.AppTheory Methods compare :: AppTheory -> AppTheory -> Ordering # (<) :: AppTheory -> AppTheory -> Bool # (<=) :: AppTheory -> AppTheory -> Bool # (>) :: AppTheory -> AppTheory -> Bool # (>=) :: AppTheory -> AppTheory -> Bool # max :: AppTheory -> AppTheory -> AppTheory # min :: AppTheory -> AppTheory -> AppTheory #

quantTheory :: NonceApp t (Expr t) tp -> AppTheory Source #

appTheory :: App (Expr t) tp -> AppTheory Source #

Ground evaluation

type family GroundValue (tp :: BaseType) where ... Source #

Equations

GroundValue BaseBoolType = Bool
GroundValue BaseNatType = Natural
GroundValue BaseIntegerType = Integer
GroundValue BaseRealType = Rational
GroundValue (BaseBVType w) = BV w
GroundValue (BaseFloatType fpp) = BV (FloatPrecisionBits fpp)
GroundValue BaseComplexType = Complex Rational
GroundValue (BaseStringType si) = StringLiteral si
GroundValue (BaseArrayType idx b) = GroundArray idx b
GroundValue (BaseStructType ctx) = Assignment GroundValueWrapper ctx

newtype GroundValueWrapper tp Source #

A newtype wrapper around ground value for use in a cache.

Constructors

GVW
Fields unGVW :: GroundValue tp

data GroundArray idx b Source #

A representation of a ground-value array.

Constructors

ArrayMapping (Assignment GroundValueWrapper idx -> IO (GroundValue b))	Lookup function for querying by index
ArrayConcrete (GroundValue b) (Map (Assignment IndexLit idx) (GroundValue b))	Default value and finite map of particular indices

lookupArray :: Assignment BaseTypeRepr idx -> GroundArray idx b -> Assignment GroundValueWrapper idx -> IO (GroundValue b) Source #

Look up an index in an ground array.

newtype GroundEvalFn t Source #

A function that calculates ground values for elements. Clients of solvers should use the groundEval function for computing values in models.

Constructors

GroundEvalFn
Fields groundEval :: forall tp. Expr t tp -> IO (GroundValue tp)

type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational) Source #

Function that calculates upper and lower bounds for real-valued elements. This type is used for solvers (e.g., dReal) that give only approximate solutions.