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

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

What4.Expr

Contents

- Expression builder
- Flags
- Type abbreviations
- Expression datatypes
  - App expressions
  - NonceApp expressions
  - Bound variables
  - Symbolic functions
  - Semirings
  - Unary BV
- Logic theories
- Ground evaluation

Description

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

Synopsis

- data ExprBuilder t (st :: Type -> Type) (fs :: Type)
- newExprBuilder :: FloatModeRepr fm -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
- startCaching :: ExprBuilder t st fs -> IO ()
- stopCaching :: ExprBuilder t st fs -> IO ()
- userState :: Lens' (ExprBuilder t st fs) (st t)
- exprCounter :: Getter (ExprBuilder t st fs) (NonceGenerator IO t)
- curProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc
- unaryThreshold :: Getter (ExprBuilder t st fs) (OptionSetting BaseIntegerType)
- cacheStartSize :: Getter (ExprBuilder t st fs) (OptionSetting BaseIntegerType)
- exprBuilderSplitConfig :: ExprBuilder t st fs -> IO (ExprBuilder t st fs)
- exprBuilderFreshConfig :: ExprBuilder t st fs -> IO (ExprBuilder t st fs)
- data EmptyExprBuilderState t = EmptyExprBuilderState
- data FloatMode
- data FloatModeRepr :: FloatMode -> Type where
  - FloatIEEERepr :: FloatModeRepr FloatIEEE
  - FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted
  - FloatRealRepr :: FloatModeRepr FloatReal
- type FloatIEEE = 'FloatIEEE
- type FloatUninterpreted = 'FloatUninterpreted
- type FloatReal = 'FloatReal
- data Flags (fi :: FloatMode)
- type BoolExpr t = Expr t BaseBoolType
- type IntegerExpr t = Expr t BaseIntegerType
- type RealExpr t = Expr t BaseRealType
- type BVExpr t n = Expr t (BaseBVType n)
- type CplxExpr t = Expr t BaseComplexType
- type StringExpr t si = Expr t (BaseStringType si)
- data Expr t (tp :: BaseType) where
  - SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr)
  - BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
  - 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
- exprLoc :: Expr t tp -> ProgramLoc
- ppExpr :: Expr t tp -> Doc ann
- data AppExpr t (tp :: BaseType)
- appExprId :: AppExpr t tp -> Nonce t tp
- appExprLoc :: AppExpr t tp -> ProgramLoc
- appExprApp :: AppExpr t tp -> App (Expr t) tp
- data App (e :: BaseType -> Type) (tp :: BaseType) where
  - BaseIte :: !(BaseTypeRepr tp) -> !Integer -> !(e BaseBoolType) -> !(e tp) -> !(e tp) -> App e tp
  - BaseEq :: !(BaseTypeRepr tp) -> !(e tp) -> !(e tp) -> App e BaseBoolType
  - NotPred :: !(e BaseBoolType) -> App e BaseBoolType
  - ConjPred :: !(BoolMap e) -> App e BaseBoolType
  - SemiRingSum :: !(WeightedSum e sr) -> App e (SemiRingBase sr)
  - SemiRingProd :: !(SemiRingProduct e sr) -> App e (SemiRingBase sr)
  - SemiRingLe :: !(OrderedSemiRingRepr sr) -> !(e (SemiRingBase sr)) -> !(e (SemiRingBase sr)) -> App e BaseBoolType
  - RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType
  - 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
- data NonceAppExpr t (tp :: BaseType)
- nonceExprId :: NonceAppExpr t tp -> Nonce t tp
- nonceExprLoc :: NonceAppExpr t tp -> ProgramLoc
- nonceExprApp :: NonceAppExpr t tp -> NonceApp t (Expr t) tp
- data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where
  - Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp
  - Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
  - Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
  - ArrayFromFn :: !(ExprSymFn t (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
- data ExprBoundVar t (tp :: BaseType)
- bvarId :: ExprBoundVar t tp -> Nonce t tp
- bvarLoc :: ExprBoundVar t tp -> ProgramLoc
- bvarName :: ExprBoundVar t tp -> SolverSymbol
- bvarKind :: ExprBoundVar t tp -> VarKind
- data VarKind
  - = QuantifierVarKind
  - | LatchVarKind
  - | UninterpVarKind
- boundVars :: Expr t tp -> ST s (BoundVarMap s t)
- data ExprSymFn t (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
- type family Coefficient (sr :: SemiRing) :: Type where ...
- data SemiRing
- data BVFlavor
- data SemiRingRepr (sr :: SemiRing) where
  - SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger
  - SemiRingRealRepr :: SemiRingRepr SemiRingReal
  - SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)
- data BVFlavorRepr (fv :: BVFlavor) where
  - BVArithRepr :: BVFlavorRepr BVArith
  - BVBitsRepr :: BVFlavorRepr BVBits
- data OrderedSemiRingRepr (sr :: SemiRing) where
  - OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger
  - OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal
- data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing)
- data UnaryBV p (n :: Nat)
- data AppTheory
  - = BoolTheory
  - | LinearArithTheory
  - | NonlinearArithTheory
  - | ComputableArithTheory
  - | BitvectorTheory
  - | QuantifierTheory
  - | StringTheory
  - | FloatingPointTheory
  - | ArrayTheory
  - | StructTheory
  - | FnTheory
- quantTheory :: NonceApp t (Expr t) tp -> AppTheory
- appTheory :: App (Expr t) tp -> AppTheory
- type family GroundValue (tp :: BaseType) where ...
- newtype GroundValueWrapper tp = GVW {
  - unGVW :: GroundValue tp
  }
- data GroundArray idx b
  - = ArrayMapping (Assignment GroundValueWrapper idx -> IO (GroundValue b))
  - | ArrayConcrete (GroundValue b) (Map (Assignment IndexLit idx) (GroundValue b))
- lookupArray :: Assignment BaseTypeRepr idx -> GroundArray idx b -> Assignment GroundValueWrapper idx -> IO (GroundValue b)
- newtype GroundEvalFn t = GroundEvalFn {
  - groundEval :: forall tp. Expr t tp -> IO (GroundValue tp)
  }
- type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)

# Expression builder

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

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

#### Instances

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)) |

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.

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

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

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 #

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.

data EmptyExprBuilderState t Source #

A "dummy" data type that can be used for the user state field of an `ExprBuilder` when there is no other interesting state to track.

Constructors

EmptyExprBuilderState |

# 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)

# Type abbreviations

type BoolExpr t = Expr t BaseBoolType Source #

type IntegerExpr t = Expr t BaseIntegerType Source #

type RealExpr t = Expr t BaseRealType Source #

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

type CplxExpr t = Expr t BaseComplexType Source #

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

# Expression datatypes

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

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

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

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

Constructors

SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr) |
BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType |
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 #

exprLoc :: Expr t tp -> ProgramLoc Source #

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

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

## App expressions

data AppExpr t (tp :: BaseType) Source #

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

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

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

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

appExprLoc :: AppExpr t tp -> ProgramLoc Source #

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

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

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

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

Constructors

BaseIte :: !(BaseTypeRepr tp) -> !Integer -> !(e BaseBoolType) -> !(e tp) -> !(e tp) -> App e tp |
BaseEq :: !(BaseTypeRepr tp) -> !(e tp) -> !(e tp) -> App e BaseBoolType |
NotPred :: !(e BaseBoolType) -> App e BaseBoolType |
ConjPred :: !(BoolMap e) -> App e BaseBoolType |
SemiRingSum :: !(WeightedSum e sr) -> App e (SemiRingBase sr) |
SemiRingProd :: !(SemiRingProduct e sr) -> App e (SemiRingBase sr) |
SemiRingLe :: !(OrderedSemiRingRepr sr) -> !(e (SemiRingBase sr)) -> !(e (SemiRingBase sr)) -> App e BaseBoolType |
RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType |
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 #

## NonceApp expressions

data NonceAppExpr t (tp :: BaseType) Source #

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

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

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

#### Instances

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 #

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 #

## Bound variables

data ExprBoundVar t (tp :: BaseType) Source #

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

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

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

#### Instances

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 #

bvarKind :: ExprBoundVar t tp -> VarKind Source #

data VarKind Source #

The Kind of a bound variable.

Constructors

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

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

## Symbolic functions

data ExprSymFn t (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 #

## Semirings

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

The constant values in the semiring.

Equations

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

data SemiRing Source #

Data-kind representing the semirings What4 supports.

#### Instances

Instances details

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

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

OrdF SemiRingRepr Source # |

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

OrdF f => TestEquality (SemiRingProduct f :: SemiRing -> Type) Source # |
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: forall (a :: k) (b :: k). SemiRingProduct f a -> SemiRingProduct f b -> Maybe (a :~: b) Source #
OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source # |
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: forall (a :: k) (b :: k). WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) Source #

data BVFlavor Source #

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

#### Instances

Instances details

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

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

data SemiRingRepr (sr :: SemiRing) where Source #

Constructors

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

#### Instances

Instances details

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

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (SemiRingRepr sr) Source # |
Instance details Defined in What4.SemiRing Methods (==) :: SemiRingRepr sr -> SemiRingRepr sr -> Bool Source # (/=) :: SemiRingRepr sr -> SemiRingRepr sr -> Bool Source #
Hashable (SemiRingRepr sr) Source # |
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> SemiRingRepr sr -> Int Source # hash :: SemiRingRepr sr -> Int Source #

data BVFlavorRepr (fv :: BVFlavor) where Source #

Constructors

BVArithRepr :: BVFlavorRepr BVArith |
BVBitsRepr :: BVFlavorRepr BVBits |

#### Instances

Instances details

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

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (BVFlavorRepr fv) Source # |
Instance details Defined in What4.SemiRing Methods (==) :: BVFlavorRepr fv -> BVFlavorRepr fv -> Bool Source # (/=) :: BVFlavorRepr fv -> BVFlavorRepr fv -> Bool Source #
Hashable (BVFlavorRepr fv) Source # |
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> BVFlavorRepr fv -> Int Source # hash :: BVFlavorRepr fv -> Int Source #

data OrderedSemiRingRepr (sr :: SemiRing) where Source #

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

Constructors

OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger |
OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal |

#### Instances

Instances details

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

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (OrderedSemiRingRepr sr) Source # |
Instance details Defined in What4.SemiRing Methods (==) :: OrderedSemiRingRepr sr -> OrderedSemiRingRepr sr -> Bool Source # (/=) :: OrderedSemiRingRepr sr -> OrderedSemiRingRepr sr -> Bool Source #
Hashable (OrderedSemiRingRepr sr) Source # |
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> OrderedSemiRingRepr sr -> Int Source # hash :: OrderedSemiRingRepr sr -> Int Source #

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

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

#### Instances

Instances details

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

## Unary BV

data UnaryBV p (n :: Nat) Source #

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

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

#### Instances

Instances details

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

# Logic theories

data AppTheory Source #

The theory that a symbol belongs to.

Constructors

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

#### Instances

Instances details

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

Instance details

Defined in What4.Expr.AppTheory

Methods

compare :: AppTheory -> AppTheory -> Ordering Source #

(<) :: AppTheory -> AppTheory -> Bool Source #

(<=) :: AppTheory -> AppTheory -> Bool Source #

(>) :: AppTheory -> AppTheory -> Bool Source #

(>=) :: AppTheory -> AppTheory -> Bool Source #

max :: AppTheory -> AppTheory -> AppTheory Source #

min :: AppTheory -> AppTheory -> AppTheory Source #

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

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

# Ground evaluation

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

Equations

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

newtype GroundValueWrapper tp Source #

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

Constructors

GVW |

Fields

- unGVW :: GroundValue tp

data GroundArray idx b Source #

A representation of a ground-value array.

Constructors

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

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

Look up an index in an ground array.

newtype GroundEvalFn t Source #

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

Constructors

GroundEvalFn |

Fields

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

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

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