what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | jhendrix@galois.com
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Expr.Builder

Contents

- ExprBuilder
- Specialized representations
- configuration options
- Expr
  - AppExpr
  - NonceAppExpr
  - Type abbreviations
- App
- NonceApp
- Bound Variable information
- Symbolic Function
- SymbolVarBimap
- IdxCache
- Flags
- BV Or Set
- Re-exports

Description

This module defines the canonical implementation of the solver interface from What4.Interface. Type ``ExprBuilder` t st` is an instance of the classes `IsExprBuilder` and `IsSymExprBuilder`.

Notes regarding concurrency: The expression builder datatype contains a number of mutable storage locations. These are designed so they may reasonably be used in a multithreaded context. In particular, nonce values are generated atomically, and other IORefs used in this module are modified or written atomically, so modifications should propagate in the expected sequentially-consistent ways. Of course, threads may still clobber state others have set (e.g., the current program location) so the potential for truly multithreaded use is somewhat limited. Consider the `exprBuilderFreshConfig` or `exprBuilderSplitConfig` operations if this is a concern.

Synopsis

- data ExprBuilder t (st :: Type -> Type) (fs :: Type)
- newExprBuilder :: FloatModeRepr fm -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
- getSymbolVarBimap :: ExprBuilder t st fs -> IO (SymbolVarBimap t)
- sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
- sbNonceExpr :: ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp)
- curProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc
- unaryThreshold :: Getter (ExprBuilder t st fs) (OptionSetting BaseIntegerType)
- cacheStartSize :: Getter (ExprBuilder t st fs) (OptionSetting BaseIntegerType)
- userState :: Lens' (ExprBuilder t st fs) (st t)
- exprCounter :: Getter (ExprBuilder t st fs) (NonceGenerator IO t)
- startCaching :: ExprBuilder t st fs -> IO ()
- stopCaching :: ExprBuilder t st fs -> IO ()
- exprBuilderSplitConfig :: ExprBuilder t st fs -> IO (ExprBuilder t st fs)
- exprBuilderFreshConfig :: ExprBuilder t st fs -> IO (ExprBuilder t st fs)
- bvUnary :: 1 <= w => ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
- intSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingInteger -> IO (IntegerExpr t)
- realSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingReal -> IO (RealExpr t)
- bvSum :: ExprBuilder t st fs -> WeightedSum (Expr t) (SemiRingBV flv w) -> IO (BVExpr t w)
- scalarMul :: ExprBuilder t st fs -> SemiRingRepr sr -> Coefficient sr -> Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
- unaryThresholdOption :: ConfigOption BaseIntegerType
- cacheStartSizeOption :: ConfigOption BaseIntegerType
- cacheTerms :: ConfigOption BaseBoolType
- data Expr t (tp :: BaseType) where
  - SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr)
  - BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
  - FloatExpr :: !(FloatPrecisionRepr fpp) -> !BigFloat -> !ProgramLoc -> Expr t (BaseFloatType fpp)
  - 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
- asApp :: Expr t tp -> Maybe (App (Expr t) tp)
- asNonceApp :: Expr t tp -> Maybe (NonceApp t (Expr t) tp)
- iteSize :: Expr t tp -> Integer
- exprLoc :: Expr t tp -> ProgramLoc
- ppExpr :: Expr t tp -> Doc ann
- ppExprTop :: Expr t tp -> Doc ann
- exprMaybeId :: Expr t tp -> Maybe (Nonce t tp)
- asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
- asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
- data Polarity
  - = Positive
  - | Negative
- negatePolarity :: Polarity -> Polarity
- 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 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
- type BoolExpr t = Expr t BaseBoolType
- type IntegerExpr t = Expr t BaseIntegerType
- type RealExpr t = Expr t BaseRealType
- type FloatExpr t fpp = Expr t (BaseFloatType fpp)
- type BVExpr t n = Expr t (BaseBVType n)
- type CplxExpr t = Expr t BaseComplexType
- type StringExpr t si = Expr t (BaseStringType si)
- 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
  - 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
  - RealSpecialFunction :: !(SpecialFunction args) -> !(SpecialFnArgs e BaseRealType args) -> 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)
  - 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)
  - 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
  - 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
  - FloatSpecialFunction :: !(FloatPrecisionRepr fpp) -> !(SpecialFunction args) -> !(SpecialFnArgs e (BaseFloatType fpp) args) -> App e (BaseFloatType fpp)
  - 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
  - CopyArray :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseArrayType (SingleCtx (BaseBVType w)) a)
  - SetArray :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e a) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseArrayType (SingleCtx (BaseBVType w)) a)
  - EqualArrayRange :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
  - IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType
  - RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType
  - 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 BaseIntegerType) -> App e BaseIntegerType
  - StringSubstring :: !(StringInfoRepr si) -> !(e (BaseStringType si)) -> !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e (BaseStringType si)
  - StringAppend :: !(StringInfoRepr si) -> !(StringSeq e si) -> App e (BaseStringType si)
  - StringLength :: !(e (BaseStringType si)) -> App e BaseIntegerType
  - StructCtor :: !(Assignment BaseTypeRepr flds) -> !(Assignment e flds) -> App e (BaseStructType flds)
  - StructField :: !(e (BaseStructType flds)) -> !(Index flds tp) -> !(BaseTypeRepr tp) -> App e tp
- traverseApp :: (Applicative m, OrdF f, Eq (f BaseBoolType), HashableF f, HasAbsValue f) => (forall tp. e tp -> m (f tp)) -> App e utp -> m (App f utp)
- appType :: App e tp -> BaseTypeRepr 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 (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret)
  - MapOverArrays :: !(ExprSymFn t (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r)
  - ArrayTrueOnEntries :: !(ExprSymFn t (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType
  - FnApp :: !(ExprSymFn t args ret) -> !(Assignment e args) -> NonceApp t e ret
- nonceAppType :: IsExpr e => NonceApp t e tp -> BaseTypeRepr tp
- data ExprBoundVar t (tp :: BaseType)
- bvarId :: ExprBoundVar t tp -> Nonce t tp
- bvarLoc :: ExprBoundVar t tp -> ProgramLoc
- bvarName :: ExprBoundVar t tp -> SolverSymbol
- bvarType :: ExprBoundVar t tp -> BaseTypeRepr tp
- bvarKind :: ExprBoundVar t tp -> VarKind
- bvarAbstractValue :: ExprBoundVar t tp -> Maybe (AbstractValue tp)
- data VarKind
  - = QuantifierVarKind
  - | LatchVarKind
  - | UninterpVarKind
- boundVars :: Expr t tp -> ST s (BoundVarMap s t)
- ppBoundVar :: ExprBoundVar t tp -> String
- evalBoundVars :: ExprBuilder t st fs -> Expr t ret -> Assignment (ExprBoundVar t) args -> Assignment (Expr t) args -> IO (Expr t ret)
- data ExprSymFn t (args :: Ctx BaseType) (ret :: BaseType) = ExprSymFn {
  - symFnId :: !(Nonce t (args ::> ret))
  - symFnName :: !SolverSymbol
  - symFnInfo :: !(SymFnInfo t args ret)
  - symFnLoc :: !ProgramLoc
  }
- data SymFnInfo t (args :: Ctx BaseType) (ret :: BaseType)
  - = UninterpFnInfo !(Assignment BaseTypeRepr args) !(BaseTypeRepr ret)
  - | DefinedFnInfo !(Assignment (ExprBoundVar t) args) !(Expr t ret) !UnfoldPolicy
  - | MatlabSolverFnInfo !(MatlabSolverFn (Expr t) args ret) !(Assignment (ExprBoundVar t) args) !(Expr t ret)
- symFnArgTypes :: ExprSymFn t args ret -> Assignment BaseTypeRepr args
- symFnReturnType :: ExprSymFn t args ret -> BaseTypeRepr ret
- data SomeExprSymFn t = forall args ret. SomeExprSymFn (ExprSymFn t args ret)
- data ExprSymFnWrapper t c = forall a r.c ~ (a ::> r) => ExprSymFnWrapper (ExprSymFn t a r)
- data SymbolVarBimap t
- data SymbolBinding t
  - = forall tp. VarSymbolBinding !(ExprBoundVar t tp)
  - | forall args ret. FnSymbolBinding !(ExprSymFn t args ret)
- emptySymbolVarBimap :: SymbolVarBimap t
- lookupBindingOfSymbol :: SolverSymbol -> SymbolVarBimap t -> Maybe (SymbolBinding t)
- lookupSymbolOfBinding :: SymbolBinding t -> SymbolVarBimap t -> Maybe SolverSymbol
- data IdxCache t (f :: BaseType -> Type)
- newIdxCache :: MonadIO m => m (IdxCache t f)
- lookupIdx :: MonadIO m => IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
- lookupIdxValue :: MonadIO m => IdxCache t f -> Expr t tp -> m (Maybe (f tp))
- insertIdxValue :: MonadIO m => IdxCache t f -> Nonce t tp -> f tp -> m ()
- deleteIdxValue :: MonadIO m => IdxCache t f -> Nonce t (tp :: BaseType) -> m ()
- clearIdxCache :: MonadIO m => IdxCache t f -> m ()
- idxCacheEval :: MonadIO m => IdxCache t f -> Expr t tp -> m (f tp) -> m (f tp)
- idxCacheEval' :: MonadIO m => IdxCache t f -> Nonce t tp -> m (f tp) -> m (f tp)
- 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)
- data BVOrSet e w
- bvOrToList :: BVOrSet e w -> [e (BaseBVType w)]
- bvOrSingleton :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w
- bvOrInsert :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w
- bvOrUnion :: OrdF e => BVOrSet e w -> BVOrSet e w -> BVOrSet e w
- bvOrAbs :: (OrdF e, 1 <= w) => NatRepr w -> BVOrSet e w -> BVDomain w
- traverseBVOrSet :: (HashableF f, HasAbsValue f, OrdF f, Applicative m) => (forall tp. e tp -> m (f tp)) -> BVOrSet e w -> m (BVOrSet f w)
- type family SymExpr (sym :: Type) :: BaseType -> Type
- bvWidth :: IsExpr e => e (BaseBVType w) -> NatRepr w
- exprType :: IsExpr e => e tp -> BaseTypeRepr tp
- data IndexLit idx where
  - IntIndexLit :: !Integer -> IndexLit BaseIntegerType
  - BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w)
- newtype ArrayResultWrapper f idx tp = ArrayResultWrapper {
  - unwrapArrayResult :: f (BaseArrayType idx tp)
  }

# ExprBuilder

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

Instances details

MatlabSymbolicArrayBuilder (ExprBuilder t st fs) Source # |
Instance details Defined in What4.Expr.Builder Methods mkMatlabSolverFn :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprBuilder t st fs -> MatlabSolverFn (SymExpr (ExprBuilder t st fs)) args ret -> IO (SymFn (ExprBuilder t st fs) args 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 :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> SymExpr (ExprBuilder t st fs) tp -> IO (Pred (ExprBuilder t st fs)) Source #

baseTypeIte :: forall (tp :: BaseType). 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 :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> IO (SymAnnotation (ExprBuilder t st fs) tp, SymExpr (ExprBuilder t st fs) tp) Source #

getAnnotation :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> Maybe (SymAnnotation (ExprBuilder t st fs) tp) Source #

getUnannotatedTerm :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> Maybe (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 #

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 #

intMin :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source #

intMax :: 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 :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvConcat :: forall (u :: Natural) (v :: Natural). (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 :: forall (idx :: Natural) (n :: Natural) (w :: Natural). (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 :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvAdd :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> Natural -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source #

bvIsNeg :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source #

bvIte :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source #

bvShl :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (u :: Natural) (r :: Natural). (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 :: forall (u :: Natural) (r :: Natural). (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 :: forall (r :: Natural) (w :: Natural). (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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvSet :: forall (w :: Natural). 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 :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> NatRepr w -> Pred (ExprBuilder t st fs) -> IO (SymBV (ExprBuilder t st fs) w) Source #

minUnsignedBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

maxUnsignedBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

maxSignedBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

minSignedBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvPopcount :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvCountLeadingZeros :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvCountTrailingZeros :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source #

addUnsignedOF :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (flds :: Ctx BaseType). ExprBuilder t st fs -> Assignment (SymExpr (ExprBuilder t st fs)) flds -> IO (SymStruct (ExprBuilder t st fs) flds) Source #

structField :: forall (flds :: Ctx BaseType) (tp :: BaseType). ExprBuilder t st fs -> SymStruct (ExprBuilder t st fs) flds -> Index flds tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source #

structEq :: forall (flds :: Ctx BaseType). ExprBuilder t st fs -> SymStruct (ExprBuilder t st fs) flds -> SymStruct (ExprBuilder t st fs) flds -> IO (Pred (ExprBuilder t st fs)) Source #

structIte :: forall (flds :: Ctx BaseType). 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 :: forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType). 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 :: forall (idx :: Ctx BaseType) (itp :: BaseType) (ret :: BaseType). ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) (idx ::> itp) ret -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) ret) Source #

arrayMap :: forall (ctx :: Ctx BaseType) (d :: BaseType) (r :: BaseType) (idx :: Ctx BaseType) (itp :: BaseType). 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 :: forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType). 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 :: forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType). 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 #

arrayCopy :: forall (w :: Natural) (a :: BaseType). 1 <= w => ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a) Source #

arraySet :: forall (w :: Natural) (a :: BaseType). 1 <= w => ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymExpr (ExprBuilder t st fs) a -> SymBV (ExprBuilder t st fs) w -> IO (SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a) Source #

arrayRangeEq :: forall (w :: Natural) (a :: BaseType). 1 <= w => ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source #

arrayFromMap :: forall (idx :: Ctx BaseType) (itp :: BaseType) (tp :: BaseType). 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 :: forall (idx :: Ctx BaseType) (itp :: BaseType) (tp :: BaseType). 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 :: forall (idx :: Ctx BaseType) (b :: BaseType). 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 :: forall (idx :: Ctx BaseType) (b :: BaseType). 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 :: forall (idx :: Ctx BaseType). ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) idx BaseBoolType -> IO (Pred (ExprBuilder t st fs)) Source #

arrayTrueOnEntries :: forall (idx :: Ctx BaseType) (itp :: BaseType). 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 #

integerToReal :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source #

bvToInteger :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymInteger (ExprBuilder t st fs)) Source #

sbvToInteger :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymInteger (ExprBuilder t st fs)) Source #

predToBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

uintToReal :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymReal (ExprBuilder t st fs)) Source #

sbvToReal :: forall (w :: Natural). 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 :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

realToInteger :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source #

realToBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

realToSBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

clampedIntToSBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

clampedIntToBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

intSetWidth :: forall (m :: Natural) (n :: Natural). (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 :: forall (m :: Natural) (n :: Natural). (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 :: forall (m :: Natural) (n :: Natural). (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 :: forall (m :: Natural) (n :: Natural). (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 :: forall (si :: StringInfo). ExprBuilder t st fs -> StringInfoRepr si -> IO (SymString (ExprBuilder t st fs) si) Source #

stringLit :: forall (si :: StringInfo). ExprBuilder t st fs -> StringLiteral si -> IO (SymString (ExprBuilder t st fs) si) Source #

stringEq :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs)) Source #

stringIte :: forall (si :: StringInfo). 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 :: forall (si :: StringInfo). 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 :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs)) Source #

stringIsPrefixOf :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs)) Source #

stringIsSuffixOf :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs)) Source #

stringIndexOf :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs)) Source #

stringLength :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> IO (SymInteger (ExprBuilder t st fs)) Source #

stringSubstring :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymInteger (ExprBuilder t st fs) -> SymInteger (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 #

realMin :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source #

realMax :: 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 #

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 #

realAtan2 :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source #

realSpecialFunction :: forall (args :: Ctx Type). ExprBuilder t st fs -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st fs)) BaseRealType) args -> IO (SymReal (ExprBuilder t st fs)) Source #

realSpecialFunction0 :: ExprBuilder t st fs -> SpecialFunction EmptyCtx -> IO (SymReal (ExprBuilder t st fs)) Source #

realSpecialFunction1 :: ExprBuilder t st fs -> SpecialFunction (EmptyCtx ::> R) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source #

realSpecialFunction2 :: ExprBuilder t st fs -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source #

floatPZero :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatNZero :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatNaN :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatPInf :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatNInf :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatLitRational :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatLit :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatNeg :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatAbs :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatSqrt :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatAdd :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatNe :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatFpEq :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatFpApart :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatFpUnordered :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatLe :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatLt :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatGe :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatGt :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatIsNaN :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatIsInf :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatIsZero :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatIsPos :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatIsNeg :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatIsSubnorm :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatIsNorm :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs)) Source #

floatIte :: forall (fpp :: FloatPrecision). 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 :: forall (fpp :: FloatPrecision) (fpp' :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp' -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatRound :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatFromBinary :: forall (eb :: Natural) (sb :: Natural). (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 :: forall (eb :: Natural) (sb :: Natural). (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 :: forall (w :: Natural) (fpp :: FloatPrecision). 1 <= w => ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV (ExprBuilder t st fs) w -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

sbvToFloat :: forall (w :: Natural) (fpp :: FloatPrecision). 1 <= w => ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV (ExprBuilder t st fs) w -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

realToFloat :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymReal (ExprBuilder t st fs) -> IO (SymFloat (ExprBuilder t st fs) fpp) Source #

floatToBV :: forall (w :: Natural) (fpp :: FloatPrecision). 1 <= w => ExprBuilder t st fs -> NatRepr w -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymBV (ExprBuilder t st fs) w) Source #

floatToSBV :: forall (w :: Natural) (fpp :: FloatPrecision). 1 <= w => ExprBuilder t st fs -> NatRepr w -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymBV (ExprBuilder t st fs) w) Source #

floatToReal :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymReal (ExprBuilder t st fs)) Source #

floatSpecialFunction :: forall (fpp :: FloatPrecision) (args :: Ctx Type). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st fs)) (BaseFloatType fpp)) args -> IO (SymFloat (ExprBuilder t st fs) fpp) 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 #

IsSymExprBuilder (ExprBuilder t st fs) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

freshConstant :: forall (tp :: BaseType). ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source #

freshLatch :: forall (tp :: BaseType). ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source #

freshBoundedBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SolverSymbol -> NatRepr w -> Maybe Natural -> Maybe Natural -> IO (SymBV (ExprBuilder t st fs) w) Source #

freshBoundedSBV :: forall (w :: Natural). 1 <= w => ExprBuilder t st fs -> SolverSymbol -> NatRepr w -> Maybe Integer -> Maybe Integer -> IO (SymBV (ExprBuilder t st fs) w) 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 #

exprUninterpConstants :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> Set (Some (BoundVar (ExprBuilder t st fs))) Source #

freshBoundVar :: forall (tp :: BaseType). ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar (ExprBuilder t st fs) tp) Source #

varExpr :: forall (tp :: BaseType). ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> SymExpr (ExprBuilder t st fs) tp Source #

forallPred :: forall (tp :: BaseType). ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source #

existsPred :: forall (tp :: BaseType). ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs)) Source #

definedFn :: forall (args :: Ctx BaseType) (ret :: BaseType). 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 :: forall (args :: Ctx BaseType) (ret :: BaseType). 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 :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprBuilder t st fs -> SolverSymbol -> Assignment BaseTypeRepr args -> BaseTypeRepr ret -> IO (SymFn (ExprBuilder t st fs) args ret) Source #

applySymFn :: forall (args :: Ctx BaseType) (ret :: BaseType). 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 #

substituteBoundVars :: forall (tp :: BaseType). ExprBuilder t st fs -> MapF (BoundVar (ExprBuilder t st fs)) (SymExpr (ExprBuilder t st fs)) -> SymExpr (ExprBuilder t st fs) tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source #

substituteSymFns :: forall (tp :: BaseType). ExprBuilder t st fs -> MapF (SymFnWrapper (ExprBuilder t st fs)) (SymFnWrapper (ExprBuilder t st fs)) -> SymExpr (ExprBuilder t st fs) tp -> IO (SymExpr (ExprBuilder t st fs) tp) Source #

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE)) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatLitRational :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatAdd :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 #

iFloatFpApart :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIte :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo) (fi' :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatFromBinary :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatIEEE)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatIEEE))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatReal)) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatLitRational :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatAdd :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 #

iFloatFpApart :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIte :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo) (fi' :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatFromBinary :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatReal)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatReal))) Source #

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatReal))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi) Source #

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpreted)) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatLitRational :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatAdd :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 #

iFloatFpApart :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIte :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo) (fi' :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatFromBinary :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatUninterpreted)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatUninterpreted))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

IsInterpretedFloatExprBuilder (ExprBuilder t st fs) => IsInterpretedFloatSymExprBuilder (ExprBuilder t st fs) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

freshFloatConstant :: forall (fi :: FloatInfo). ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi)) Source #

freshFloatLatch :: forall (fi :: FloatInfo). ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (SymExpr (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi)) Source #

freshFloatBoundVar :: forall (fi :: FloatInfo). ExprBuilder t st fs -> SolverSymbol -> FloatInfoRepr fi -> IO (BoundVar (ExprBuilder t st fs) (SymInterpretedFloatType (ExprBuilder t st fs) fi)) Source #

type BoundVar (ExprBuilder t st fs) Source # |
Instance details Defined in What4.Expr.Builder type BoundVar (ExprBuilder t st fs) = ExprBoundVar 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 SymExpr (ExprBuilder t st fs) Source # |
Instance details Defined in What4.Expr.Builder type SymExpr (ExprBuilder t st fs) = Expr t
type SymFn (ExprBuilder t st fs) Source # |
Instance details Defined in What4.Expr.Builder type SymFn (ExprBuilder t st fs) = ExprSymFn 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 FloatReal)) fi Source # |
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi = BaseRealType
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)

newExprBuilder Source #

Arguments

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

getSymbolVarBimap :: ExprBuilder t st fs -> IO (SymbolVarBimap t) Source #

Get current variable bindings.

sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp) Source #

sbNonceExpr :: ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp) Source #

Create an element from a nonce app.

curProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc Source #

unaryThreshold :: Getter (ExprBuilder t st fs) (OptionSetting BaseIntegerType) Source #

cacheStartSize :: Getter (ExprBuilder t st fs) (OptionSetting BaseIntegerType) Source #

userState :: Lens' (ExprBuilder t st fs) (st t) Source #

exprCounter :: Getter (ExprBuilder t st fs) (NonceGenerator IO t) Source #

startCaching :: ExprBuilder t st fs -> IO () Source #

Restart caching applications in backend (clears cache if it is currently caching).

stopCaching :: ExprBuilder t st fs -> IO () Source #

Stop caching applications in backend.

exprBuilderSplitConfig :: ExprBuilder t st fs -> IO (ExprBuilder t st fs) Source #

Return a new expr builder where the configuration object has been "split" using the `splitConfig` operation. The returned sym will share any preexisting options with the input sym, but any new options added with `extendConfig` will not be shared. This may be useful if the expression builder needs to be shared across threads, or sequentially for separate use cases. Note, however, that hash consing settings, solver loggers and the current program location will be shared.

exprBuilderFreshConfig :: ExprBuilder t st fs -> IO (ExprBuilder t st fs) Source #

Return a new expr builder where all configuration settings have been isolated from the original. The `Config` object of the output expr builder will have only the default options that are installed via `newExprBuilder`, and configuration changes to either expr builder will not be visible to the other. This includes caching settings, the current program location, and installed solver loggers.

# Specialized representations

bvUnary :: 1 <= w => ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w) Source #

intSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingInteger -> IO (IntegerExpr t) Source #

Evaluate a weighted sum of integer values.

realSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingReal -> IO (RealExpr t) Source #

Evaluate a weighted sum of real values.

bvSum :: ExprBuilder t st fs -> WeightedSum (Expr t) (SemiRingBV flv w) -> IO (BVExpr t w) Source #

scalarMul :: ExprBuilder t st fs -> SemiRingRepr sr -> Coefficient sr -> Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr)) Source #

# configuration options

unaryThresholdOption :: ConfigOption BaseIntegerType Source #

Maximum number of values in unary bitvector encoding.

This option is named "backend.unary_threshold"

cacheStartSizeOption :: ConfigOption BaseIntegerType Source #

Starting size for element cache when caching is enabled. The default value is 100000 elements.

This option is named "backend.cache_start_size"

cacheTerms :: ConfigOption BaseBoolType Source #

Indicates if we should cache terms. When enabled, hash-consing is used to find and deduplicate common subexpressions. Toggling this option from disabled to enabled will allocate a new hash table; toggling it from enabled to disabled will discard the current hash table. The default value for this option is `False`.

This option is named "use_cache"

# Expr

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 |
FloatExpr :: !(FloatPrecisionRepr fpp) -> !BigFloat -> !ProgramLoc -> Expr t (BaseFloatType fpp) |
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

Instances details

TestEquality (Expr t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: k) (b :: k). Expr t a -> Expr t b -> Maybe (a :~: b) Source #
HashableF (Expr t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: k). Int -> Expr t tp -> Int Source # hashF :: forall (tp :: k). Expr t tp -> Int Source #
OrdF (Expr t :: BaseType -> Type) Source # |

Instance details

Defined in What4.Expr.App

Methods

compareF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> Bool Source #

ltF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> Bool Source #

geqF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> Bool Source #

gtF :: forall (x :: k) (y :: k). Expr t x -> Expr t y -> Bool Source #

ShowF (Expr t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods withShow :: forall p q (tp :: k) a. p (Expr t) -> q tp -> (Show (Expr t tp) => a) -> a Source # showF :: forall (tp :: k). Expr t tp -> String Source # showsPrecF :: forall (tp :: k). Int -> Expr t tp -> String -> String Source #
IsExpr (Expr t) Source # |

Instance details

Defined in What4.Expr.App

Methods

asConstantPred :: Expr t BaseBoolType -> Maybe Bool Source #

asInteger :: Expr t BaseIntegerType -> Maybe Integer Source #

integerBounds :: Expr t BaseIntegerType -> ValueRange Integer Source #

asRational :: Expr t BaseRealType -> Maybe Rational Source #

asFloat :: forall (fpp :: FloatPrecision). Expr t (BaseFloatType fpp) -> Maybe BigFloat Source #

rationalBounds :: Expr t BaseRealType -> ValueRange Rational Source #

asComplex :: Expr t BaseComplexType -> Maybe (Complex Rational) Source #

asBV :: forall (w :: Nat). Expr t (BaseBVType w) -> Maybe (BV w) Source #

unsignedBVBounds :: forall (w :: Natural). 1 <= w => Expr t (BaseBVType w) -> Maybe (Integer, Integer) Source #

signedBVBounds :: forall (w :: Natural). 1 <= w => Expr t (BaseBVType w) -> Maybe (Integer, Integer) Source #

asAffineVar :: forall (tp :: BaseType). Expr t tp -> Maybe (ConcreteVal tp, Expr t tp, ConcreteVal tp) Source #

asString :: forall (si :: StringInfo). Expr t (BaseStringType si) -> Maybe (StringLiteral si) Source #

stringInfo :: forall (si :: StringInfo). Expr t (BaseStringType si) -> StringInfoRepr si Source #

asConstantArray :: forall (idx :: Ctx BaseType) (bt :: BaseType). Expr t (BaseArrayType idx bt) -> Maybe (Expr t bt) Source #

asStruct :: forall (flds :: Ctx BaseType). Expr t (BaseStructType flds) -> Maybe (Assignment (Expr t) flds) Source #

exprType :: forall (tp :: BaseType). Expr t tp -> BaseTypeRepr tp Source #

bvWidth :: forall (w :: Nat). Expr t (BaseBVType w) -> NatRepr w Source #

floatPrecision :: forall (fpp :: FloatPrecision). Expr t (BaseFloatType fpp) -> FloatPrecisionRepr fpp Source #

printSymExpr :: forall (tp :: BaseType) ann. Expr t tp -> Doc ann Source #

unsafeSetAbstractValue :: forall (tp :: BaseType). AbstractValue tp -> Expr t tp -> Expr t tp Source #

HasAbsValue (Expr t) Source # |
Instance details Defined in What4.Expr.App Methods getAbsValue :: forall (tp :: BaseType). Expr t tp -> AbstractValue tp Source #
Show (Expr t tp) Source # |
Instance details Defined in What4.Expr.App Methods showsPrec :: Int -> Expr t tp -> ShowS Source # show :: Expr t tp -> String Source # showList :: [Expr t tp] -> ShowS Source #
Eq (Expr t tp) Source # |
Instance details Defined in What4.Expr.App Methods (==) :: Expr t tp -> Expr t tp -> Bool Source # (/=) :: Expr t tp -> Expr t tp -> Bool Source #
Ord (Expr t tp) Source # |
Instance details Defined in What4.Expr.App Methods compare :: Expr t tp -> Expr t tp -> Ordering Source # (<) :: Expr t tp -> Expr t tp -> Bool Source # (<=) :: Expr t tp -> Expr t tp -> Bool Source # (>) :: Expr t tp -> Expr t tp -> Bool Source # (>=) :: Expr t tp -> Expr t tp -> Bool Source # max :: Expr t tp -> Expr t tp -> Expr t tp Source # min :: Expr t tp -> Expr t tp -> Expr t tp Source #
Hashable (Expr t tp) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSalt :: Int -> Expr t tp -> Int Source # hash :: Expr t tp -> Int Source #
Pretty (Expr t tp) Source # |
Instance details Defined in What4.Expr.App Methods pretty :: Expr t tp -> Doc ann Source # prettyList :: [Expr t tp] -> Doc ann Source #
PolyEq (Expr t x) (Expr t y) Source # |
Instance details Defined in What4.Expr.App Methods polyEqF :: Expr t x -> Expr t y -> Maybe (Expr t x :~: Expr t y) Source # polyEq :: Expr t x -> Expr t y -> Bool Source #

asApp :: Expr t tp -> Maybe (App (Expr t) tp) Source #

Destructor for the `AppExpr` constructor.

asNonceApp :: Expr t tp -> Maybe (NonceApp t (Expr t) tp) Source #

Destructor for the `NonceAppExpr` constructor.

iteSize :: Expr t tp -> Integer Source #

exprLoc :: Expr t tp -> ProgramLoc Source #

ppExpr :: Expr t tp -> Doc ann Source #

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

ppExprTop :: Expr t tp -> Doc ann Source #

Pretty print the top part of an element.

exprMaybeId :: Expr t tp -> Maybe (Nonce t tp) Source #

asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)] Source #

asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)] Source #

data Polarity Source #

Describes the occurrence of a variable or expression, whether it is negated or not.

Constructors

Positive |
Negative |

#### Instances

Instances details

Show Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods showsPrec :: Int -> Polarity -> ShowS Source # show :: Polarity -> String Source # showList :: [Polarity] -> ShowS Source #
Eq Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods (==) :: Polarity -> Polarity -> Bool Source # (/=) :: Polarity -> Polarity -> Bool Source #
Ord Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods compare :: Polarity -> Polarity -> Ordering Source # (<) :: Polarity -> Polarity -> Bool Source # (<=) :: Polarity -> Polarity -> Bool Source # (>) :: Polarity -> Polarity -> Bool Source # (>=) :: Polarity -> Polarity -> Bool Source # max :: Polarity -> Polarity -> Polarity Source # min :: Polarity -> Polarity -> Polarity Source #
Hashable Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods hashWithSalt :: Int -> Polarity -> Int Source # hash :: Polarity -> Int Source #

negatePolarity :: Polarity -> Polarity Source #

Swap a polarity value

## AppExpr

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 #

## NonceAppExpr

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

Instances details

TestEquality (NonceAppExpr t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: k) (b :: k). NonceAppExpr t a -> NonceAppExpr t b -> Maybe (a :~: b) Source #
OrdF (NonceAppExpr t :: BaseType -> Type) Source # |

Instance details

Defined in What4.Expr.App

Methods

compareF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> Bool Source #

ltF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> Bool Source #

geqF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> Bool Source #

gtF :: forall (x :: k) (y :: k). NonceAppExpr t x -> NonceAppExpr t y -> Bool Source #

Eq (NonceAppExpr t tp) Source # |
Instance details Defined in What4.Expr.App Methods (==) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool Source # (/=) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool Source #
Ord (NonceAppExpr t tp) Source # |

Instance details

Defined in What4.Expr.App

Methods

compare :: NonceAppExpr t tp -> NonceAppExpr t tp -> Ordering Source #

(<) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool Source #

(<=) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool Source #

(>) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool Source #

(>=) :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool Source #

max :: NonceAppExpr t tp -> NonceAppExpr t tp -> NonceAppExpr t tp Source #

min :: NonceAppExpr t tp -> NonceAppExpr t tp -> NonceAppExpr t tp Source #

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

nonceExprLoc :: NonceAppExpr t tp -> ProgramLoc Source #

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

## Type abbreviations

type BoolExpr t = Expr t BaseBoolType Source #

type IntegerExpr t = Expr t BaseIntegerType Source #

type RealExpr t = Expr t BaseRealType Source #

type FloatExpr t fpp = Expr t (BaseFloatType fpp) 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 #

# App

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 |
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 |
RealSpecialFunction :: !(SpecialFunction args) -> !(SpecialFnArgs e BaseRealType args) -> 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) |
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) |
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 |
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 |
FloatSpecialFunction :: !(FloatPrecisionRepr fpp) -> !(SpecialFunction args) -> !(SpecialFnArgs e (BaseFloatType fpp) args) -> App e (BaseFloatType fpp) |
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 |
CopyArray :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseArrayType (SingleCtx (BaseBVType w)) a) |
SetArray :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e a) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseArrayType (SingleCtx (BaseBVType w)) a) |
EqualArrayRange :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType |
IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType |
RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType |
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 BaseIntegerType) -> App e BaseIntegerType |
StringSubstring :: !(StringInfoRepr si) -> !(e (BaseStringType si)) -> !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e (BaseStringType si) |
StringAppend :: !(StringInfoRepr si) -> !(StringSeq e si) -> App e (BaseStringType si) |
StringLength :: !(e (BaseStringType si)) -> App e BaseIntegerType |
StructCtor :: !(Assignment BaseTypeRepr flds) -> !(Assignment e flds) -> App e (BaseStructType flds) |
StructField :: !(e (BaseStructType flds)) -> !(Index flds tp) -> !(BaseTypeRepr tp) -> App e tp |

#### Instances

Instances details

FoldableFC App Source # |

Instance details

Defined in What4.Expr.App

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). App f x -> m Source #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App f x -> b Source #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b Source #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App f x -> b Source #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b Source #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). App f x -> [a] Source #

(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 :: forall (a :: k) (b :: k). App e a -> App e b -> Maybe (a :~: b) Source #
(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 :: forall (tp :: k). Int -> App e tp -> Int Source # hashF :: forall (tp :: k). App e tp -> Int Source #
ShowF e => Show (App e u) Source # |
Instance details Defined in What4.Expr.App Methods showsPrec :: Int -> App e u -> ShowS Source # show :: App e u -> String Source # showList :: [App e u] -> ShowS Source #
(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 Source # (/=) :: App e tp -> App e tp -> Bool Source #
ShowF e => Pretty (App e u) Source # |
Instance details Defined in What4.Expr.App Methods pretty :: App e u -> Doc ann Source # prettyList :: [App e u] -> Doc ann Source #

traverseApp :: (Applicative m, OrdF f, Eq (f BaseBoolType), HashableF f, HasAbsValue f) => (forall tp. e tp -> m (f tp)) -> App e utp -> m (App f utp) Source #

appType :: App e tp -> BaseTypeRepr tp Source #

# NonceApp

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 (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret) |
MapOverArrays :: !(ExprSymFn t (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r) |
ArrayTrueOnEntries :: !(ExprSymFn t (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType |
FnApp :: !(ExprSymFn t args ret) -> !(Assignment e args) -> NonceApp t e ret |

#### Instances

Instances details

FoldableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # |

Instance details

Defined in What4.Expr.App

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). NonceApp t f x -> m Source #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> NonceApp t f x -> b Source #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b Source #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> NonceApp t f x -> b Source #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b Source #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). NonceApp t f x -> [a] Source #

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 Source #
TraversableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). NonceApp t f x -> m (NonceApp t g x) Source #
TestEquality e => TestEquality (NonceApp t e :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: k) (b :: k). NonceApp t e a -> NonceApp t e b -> Maybe (a :~: b) Source #
(HashableF e, TestEquality e) => HashableF (NonceApp t e :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: k). Int -> NonceApp t e tp -> Int Source # hashF :: forall (tp :: k). NonceApp t e tp -> Int Source #
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 Source # (/=) :: NonceApp t e tp -> NonceApp t e tp -> Bool Source #

nonceAppType :: IsExpr e => NonceApp t e tp -> BaseTypeRepr tp Source #

# Bound Variable information

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

Instances details

TestEquality (ExprBoundVar t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: k) (b :: k). ExprBoundVar t a -> ExprBoundVar t b -> Maybe (a :~: b) Source #
HashableF (ExprBoundVar t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: k). Int -> ExprBoundVar t tp -> Int Source # hashF :: forall (tp :: k). ExprBoundVar t tp -> Int Source #
OrdF (ExprBoundVar t :: BaseType -> Type) Source # |

Instance details

Defined in What4.Expr.App

Methods

compareF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> Bool Source #

ltF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> Bool Source #

geqF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> Bool Source #

gtF :: forall (x :: k) (y :: k). ExprBoundVar t x -> ExprBoundVar t y -> Bool Source #

ShowF (ExprBoundVar t :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods withShow :: forall p q (tp :: k) a. p (ExprBoundVar t) -> q tp -> (Show (ExprBoundVar t tp) => a) -> a Source # showF :: forall (tp :: k). ExprBoundVar t tp -> String Source # showsPrecF :: forall (tp :: k). Int -> ExprBoundVar t tp -> String -> String Source #
Show (ExprBoundVar t tp) Source # |
Instance details Defined in What4.Expr.App Methods showsPrec :: Int -> ExprBoundVar t tp -> ShowS Source # show :: ExprBoundVar t tp -> String Source # showList :: [ExprBoundVar t tp] -> ShowS Source #
Eq (ExprBoundVar t tp) Source # |
Instance details Defined in What4.Expr.App Methods (==) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool Source # (/=) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool Source #
Ord (ExprBoundVar t tp) Source # |

Instance details

Defined in What4.Expr.App

Methods

compare :: ExprBoundVar t tp -> ExprBoundVar t tp -> Ordering Source #

(<) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool Source #

(<=) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool Source #

(>) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool Source #

(>=) :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool Source #

max :: ExprBoundVar t tp -> ExprBoundVar t tp -> ExprBoundVar t tp Source #

min :: ExprBoundVar t tp -> ExprBoundVar t tp -> ExprBoundVar t tp Source #

Hashable (ExprBoundVar t tp) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSalt :: Int -> ExprBoundVar t tp -> Int Source # hash :: ExprBoundVar t tp -> Int Source #

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

bvarLoc :: ExprBoundVar t tp -> ProgramLoc Source #

bvarName :: ExprBoundVar t tp -> SolverSymbol Source #

bvarType :: ExprBoundVar t tp -> BaseTypeRepr tp Source #

bvarKind :: ExprBoundVar t tp -> VarKind Source #

bvarAbstractValue :: ExprBoundVar t tp -> Maybe (AbstractValue tp) 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 #

ppBoundVar :: ExprBoundVar t tp -> String Source #

evalBoundVars :: ExprBuilder t st fs -> Expr t ret -> Assignment (ExprBoundVar t) args -> Assignment (Expr t) args -> IO (Expr t ret) Source #

This evaluates the term with the given bound variables rebound to the given arguments.

The algorithm works by traversing the subterms in the term in a bottom-up fashion while using a hash-table to memoize results for shared subterms. The hash-table is pre-populated so that the bound variables map to the element, so we do not need any extra map lookup when checking to see if a variable is bound.

NOTE: This function assumes that variables in the substitution are not themselves bound in the term (e.g. in a function definition or quantifier). If this is not respected, then `evalBoundVars` will call `fail` with an error message.

# Symbolic Function

data ExprSymFn t (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. 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 args ret)
- symFnLoc :: !ProgramLoc

#### Instances

Instances details

IsSymFn (ExprSymFn t) Source # |

Instance details

Defined in What4.Expr.App

Methods

fnArgTypes :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprSymFn t args ret -> Assignment BaseTypeRepr args Source #

fnReturnType :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprSymFn t args ret -> BaseTypeRepr ret Source #

fnTestEquality :: forall (args1 :: Ctx BaseType) (ret1 :: BaseType) (args2 :: Ctx BaseType) (ret2 :: BaseType). ExprSymFn t args1 ret1 -> ExprSymFn t args2 ret2 -> Maybe ((args1 ::> ret1) :~: (args2 ::> ret2)) Source #

fnCompare :: forall (args1 :: Ctx BaseType) (ret1 :: BaseType) (args2 :: Ctx BaseType) (ret2 :: BaseType). ExprSymFn t args1 ret1 -> ExprSymFn t args2 ret2 -> OrderingF (args1 ::> ret1) (args2 ::> ret2) Source #

Show (ExprSymFn t args ret) Source # |
Instance details Defined in What4.Expr.App Methods showsPrec :: Int -> ExprSymFn t args ret -> ShowS Source # show :: ExprSymFn t args ret -> String Source # showList :: [ExprSymFn t args ret] -> ShowS Source #
Eq (ExprSymFn t args tp) Source # |
Instance details Defined in What4.Expr.App Methods (==) :: ExprSymFn t args tp -> ExprSymFn t args tp -> Bool Source # (/=) :: ExprSymFn t args tp -> ExprSymFn t args tp -> Bool Source #
Hashable (ExprSymFn t args tp) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSalt :: Int -> ExprSymFn t args tp -> Int Source # hash :: ExprSymFn t args tp -> Int Source #

data SymFnInfo t (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. 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) !(Expr t 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 (Expr t) args ret) !(Assignment (ExprBoundVar t) args) !(Expr t 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 args ret -> Assignment BaseTypeRepr args Source #

symFnReturnType :: ExprSymFn t args ret -> BaseTypeRepr ret Source #

data SomeExprSymFn t Source #

Constructors

forall args ret. SomeExprSymFn (ExprSymFn t args ret) |

#### Instances

Instances details

Show (SomeExprSymFn t) Source # |
Instance details Defined in What4.Expr.Builder Methods showsPrec :: Int -> SomeExprSymFn t -> ShowS Source # show :: SomeExprSymFn t -> String Source # showList :: [SomeExprSymFn t] -> ShowS Source #
Eq (SomeExprSymFn t) Source # |
Instance details Defined in What4.Expr.Builder Methods (==) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source # (/=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #
Ord (SomeExprSymFn t) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

compare :: SomeExprSymFn t -> SomeExprSymFn t -> Ordering Source #

(<) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #

(<=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #

(>) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #

(>=) :: SomeExprSymFn t -> SomeExprSymFn t -> Bool Source #

max :: SomeExprSymFn t -> SomeExprSymFn t -> SomeExprSymFn t Source #

min :: SomeExprSymFn t -> SomeExprSymFn t -> SomeExprSymFn t Source #

data ExprSymFnWrapper t c Source #

Constructors

forall a r.c ~ (a ::> r) => ExprSymFnWrapper (ExprSymFn t a r) |

# SymbolVarBimap

data SymbolVarBimap t Source #

A bijective map between vars and their canonical name for printing purposes. Parameter `t` is a phantom type brand used to track nonces.

data SymbolBinding t Source #

This describes what a given SolverSymbol is associated with. Parameter `t` is a phantom type brand used to track nonces.

Constructors

forall tp. VarSymbolBinding !(ExprBoundVar t tp) | Solver
forall args ret. FnSymbolBinding !(ExprSymFn t args ret) |

#### Instances

Instances details

Eq (SymbolBinding t) Source # |
Instance details Defined in What4.Expr.Builder Methods (==) :: SymbolBinding t -> SymbolBinding t -> Bool Source # (/=) :: SymbolBinding t -> SymbolBinding t -> Bool Source #
Ord (SymbolBinding t) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

compare :: SymbolBinding t -> SymbolBinding t -> Ordering Source #

(<) :: SymbolBinding t -> SymbolBinding t -> Bool Source #

(<=) :: SymbolBinding t -> SymbolBinding t -> Bool Source #

(>) :: SymbolBinding t -> SymbolBinding t -> Bool Source #

(>=) :: SymbolBinding t -> SymbolBinding t -> Bool Source #

max :: SymbolBinding t -> SymbolBinding t -> SymbolBinding t Source #

min :: SymbolBinding t -> SymbolBinding t -> SymbolBinding t Source #

emptySymbolVarBimap :: SymbolVarBimap t Source #

Empty symbol var bimap

lookupBindingOfSymbol :: SolverSymbol -> SymbolVarBimap t -> Maybe (SymbolBinding t) Source #

lookupSymbolOfBinding :: SymbolBinding t -> SymbolVarBimap t -> Maybe SolverSymbol Source #

# IdxCache

data IdxCache t (f :: BaseType -> Type) Source #

An IdxCache is used to map expressions with type `Expr t tp` to values with a corresponding type `f tp`. It is a mutable map using an `IO` hash table. Parameter `t` is a phantom type brand used to track nonces.

newIdxCache :: MonadIO m => m (IdxCache t f) Source #

Create a new IdxCache

lookupIdx :: MonadIO m => IdxCache t f -> Nonce t tp -> m (Maybe (f tp)) Source #

lookupIdxValue :: MonadIO m => IdxCache t f -> Expr t tp -> m (Maybe (f tp)) Source #

Return the value associated to the expr in the index.

insertIdxValue :: MonadIO m => IdxCache t f -> Nonce t tp -> f tp -> m () Source #

Bind the value to the given expr in the index.

deleteIdxValue :: MonadIO m => IdxCache t f -> Nonce t (tp :: BaseType) -> m () Source #

Remove a value from the IdxCache

clearIdxCache :: MonadIO m => IdxCache t f -> m () Source #

Remove all values from the IdxCache

idxCacheEval :: MonadIO m => IdxCache t f -> Expr t tp -> m (f tp) -> m (f tp) Source #

Implements a cached evaluated using the given element. Given an element this function returns the value of the element if bound, and otherwise calls the evaluation function, stores the result in the cache, and returns the value.

idxCacheEval' :: MonadIO m => IdxCache t f -> Nonce t tp -> m (f tp) -> m (f tp) Source #

Implements a cached evaluated using the given element. Given an element this function returns the value of the element if bound, and otherwise calls the evaluation function, stores the result in the cache, and returns the value.

# Flags

data FloatMode Source #

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

#### Instances

Instances details

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

data FloatModeRepr :: FloatMode -> Type where Source #

Constructors

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

#### Instances

Instances details

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

type FloatIEEE = 'FloatIEEE Source #

In this mode "interpreted" floating-point values are treated as bit-precise IEEE-754 floats.

type FloatUninterpreted = 'FloatUninterpreted Source #

In this mode "interpreted" floating-point values are treated as bitvectors of the appropriate width, and all operations on them are translated as uninterpreted functions.

type FloatReal = 'FloatReal Source #

In this mode "interpreted" floating-point values are treated as real-number values, to the extent possible. Expressions that would result in infinities or NaN will yield unspecified values in this mode, or directly produce runtime errors.

data Flags (fi :: FloatMode) Source #

#### Instances

Instances details

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatIEEE)) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatLitRational :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatAdd :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 #

iFloatFpApart :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (Pred (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatIte :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo) (fi' :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatFromBinary :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatIEEE)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatIEEE))) Source #

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatIEEE))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatIEEE) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatIEEE)) fi) Source #

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatReal)) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatLitRational :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatAdd :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 #

iFloatFpApart :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (Pred (ExprBuilder t st (Flags FloatReal))) Source #

iFloatIte :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo) (fi' :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatFromBinary :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatReal)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatReal))) Source #

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatReal))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatReal)) fi) Source #

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatReal) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi) Source #

IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags FloatUninterpreted)) Source # |

Instance details

Defined in What4.Expr.Builder

Methods

iFloatPZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatNZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatNaN :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatPInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatNInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatLitRational :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatAbs :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatSqrt :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatAdd :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 #

iFloatFpApart :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsInf :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsZero :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsPos :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsNeg :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsSubnorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIsNorm :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (Pred (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatIte :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo) (fi' :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> RoundingMode -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatFromBinary :: forall (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> RoundingMode -> SymReal (ExprBuilder t st (Flags FloatUninterpreted)) -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatToBV :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (w :: Natural) (fi :: FloatInfo). 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 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymReal (ExprBuilder t st (Flags FloatUninterpreted))) Source #

iFloatSpecialFunction :: forall (fi :: FloatInfo) (args :: Ctx Type). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st (Flags FloatUninterpreted))) (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) fi)) args -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatSpecialFunction0 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction EmptyCtx -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatSpecialFunction1 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction (EmptyCtx ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatSpecialFunction2 :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi -> IO (SymInterpretedFloat (ExprBuilder t st (Flags FloatUninterpreted)) fi) Source #

iFloatBaseTypeRepr :: forall (fi :: FloatInfo). ExprBuilder t st (Flags FloatUninterpreted) -> FloatInfoRepr fi -> BaseTypeRepr (SymInterpretedFloatType (ExprBuilder t st (Flags FloatUninterpreted)) 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 FloatReal)) fi Source # |
Instance details Defined in What4.Expr.Builder type SymInterpretedFloatType (ExprBuilder t st (Flags FloatReal)) fi = BaseRealType
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)

# BV Or Set

data BVOrSet e w Source #

#### Instances

Instances details

(OrdF e, TestEquality e) => Eq (BVOrSet e w) Source # |
Instance details Defined in What4.Expr.App Methods (==) :: BVOrSet e w -> BVOrSet e w -> Bool Source # (/=) :: BVOrSet e w -> BVOrSet e w -> Bool Source #
OrdF e => Hashable (BVOrSet e w) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSalt :: Int -> BVOrSet e w -> Int Source # hash :: BVOrSet e w -> Int Source #

bvOrToList :: BVOrSet e w -> [e (BaseBVType w)] Source #

bvOrSingleton :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w Source #

bvOrInsert :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w Source #

bvOrUnion :: OrdF e => BVOrSet e w -> BVOrSet e w -> BVOrSet e w Source #

bvOrAbs :: (OrdF e, 1 <= w) => NatRepr w -> BVOrSet e w -> BVDomain w Source #

traverseBVOrSet :: (HashableF f, HasAbsValue f, OrdF f, Applicative m) => (forall tp. e tp -> m (f tp)) -> BVOrSet e w -> m (BVOrSet f w) Source #

# Re-exports

type family SymExpr (sym :: Type) :: BaseType -> Type Source #

The class for expressions.

#### Instances

Instances details

type SymExpr (ExprBuilder t st fs) Source # |
Instance details Defined in What4.Expr.Builder type SymExpr (ExprBuilder t st fs) = Expr t

bvWidth :: IsExpr e => e (BaseBVType w) -> NatRepr w Source #

Get the width of a bitvector

exprType :: IsExpr e => e tp -> BaseTypeRepr tp Source #

Get type of expression.

data IndexLit idx where Source #

This represents a concrete index value, and is used for creating arrays.

Constructors

IntIndexLit :: !Integer -> IndexLit BaseIntegerType |
BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w) |

#### Instances

Instances details

TestEquality IndexLit Source # |
Instance details Defined in What4.IndexLit Methods testEquality :: forall (a :: k) (b :: k). IndexLit a -> IndexLit b -> Maybe (a :~: b) Source #
HashableF IndexLit Source # |
Instance details Defined in What4.IndexLit Methods hashWithSaltF :: forall (tp :: k). Int -> IndexLit tp -> Int Source # hashF :: forall (tp :: k). IndexLit tp -> Int Source #
OrdF IndexLit Source # |

Instance details

Defined in What4.IndexLit

Methods

compareF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool Source #

ltF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool Source #

geqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool Source #

gtF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool Source #

ShowF IndexLit Source # |
Instance details Defined in What4.IndexLit Methods withShow :: forall p q (tp :: k) a. p IndexLit -> q tp -> (Show (IndexLit tp) => a) -> a Source # showF :: forall (tp :: k). IndexLit tp -> String Source # showsPrecF :: forall (tp :: k). Int -> IndexLit tp -> String -> String Source #
Show (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods showsPrec :: Int -> IndexLit tp -> ShowS Source # show :: IndexLit tp -> String Source # showList :: [IndexLit tp] -> ShowS Source #
Eq (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods (==) :: IndexLit tp -> IndexLit tp -> Bool Source # (/=) :: IndexLit tp -> IndexLit tp -> Bool Source #
Hashable (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods hashWithSalt :: Int -> IndexLit tp -> Int Source # hash :: IndexLit tp -> Int Source #

newtype ArrayResultWrapper f idx tp Source #

Constructors

ArrayResultWrapper |

Fields

- unwrapArrayResult :: f (BaseArrayType idx tp)

#### Instances

Instances details

TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type) Source # |
Instance details Defined in What4.Interface Methods testEquality :: forall (a :: k) (b :: k). ArrayResultWrapper f idx a -> ArrayResultWrapper f idx b -> Maybe (a :~: b) Source #
HashableF e => HashableF (ArrayResultWrapper e idx :: BaseType -> Type) Source # |
Instance details Defined in What4.Interface Methods hashWithSaltF :: forall (tp :: k). Int -> ArrayResultWrapper e idx tp -> Int Source # hashF :: forall (tp :: k). ArrayResultWrapper e idx tp -> Int Source #