| Copyright | (c) Galois Inc 2015-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Expr
Contents
Description
The module reexports the most commonly used types and operations of the What4 expression representation.
Synopsis
- data ExprBuilder t (st :: Type -> Type) (fs :: Type)
- newExprBuilder :: FloatModeRepr fm -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
- data FloatMode
- data FloatModeRepr :: FloatMode -> Type where
- type FloatIEEE = FloatIEEE
- type FloatUninterpreted = FloatUninterpreted
- type FloatReal = FloatReal
- data Flags (fi :: FloatMode)
- type BoolExpr t = Expr t BaseBoolType
- type NatExpr t = Expr t BaseNatType
- type IntegerExpr t = Expr t BaseIntegerType
- type RealExpr t = Expr t BaseRealType
- type BVExpr t n = Expr t (BaseBVType n)
- type CplxExpr t = Expr t BaseComplexType
- type StringExpr t si = Expr t (BaseStringType si)
- data Expr t (tp :: BaseType) where
- SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr)
- BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
- StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si)
- AppExpr :: !(AppExpr t tp) -> Expr t tp
- NonceAppExpr :: !(NonceAppExpr t tp) -> Expr t tp
- BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp
- exprLoc :: Expr t tp -> ProgramLoc
- ppExpr :: Expr t tp -> Doc
- data AppExpr t (tp :: BaseType)
- appExprId :: AppExpr t tp -> Nonce t tp
- appExprLoc :: AppExpr t tp -> ProgramLoc
- appExprApp :: AppExpr t tp -> App (Expr t) tp
- data App (e :: BaseType -> Type) (tp :: BaseType) where
- BaseIte :: !(BaseTypeRepr tp) -> !Integer -> !(e BaseBoolType) -> !(e tp) -> !(e tp) -> App e tp
- BaseEq :: !(BaseTypeRepr tp) -> !(e tp) -> !(e tp) -> App e BaseBoolType
- NotPred :: !(e BaseBoolType) -> App e BaseBoolType
- ConjPred :: !(BoolMap e) -> App e BaseBoolType
- SemiRingSum :: !(WeightedSum e sr) -> App e (SemiRingBase sr)
- SemiRingProd :: !(SemiRingProduct e sr) -> App e (SemiRingBase sr)
- SemiRingLe :: !(OrderedSemiRingRepr sr) -> !(e (SemiRingBase sr)) -> !(e (SemiRingBase sr)) -> App e BaseBoolType
- RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType
- NatDiv :: !(e BaseNatType) -> !(e BaseNatType) -> App e BaseNatType
- NatMod :: !(e BaseNatType) -> !(e BaseNatType) -> App e BaseNatType
- IntDiv :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
- IntMod :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
- IntAbs :: !(e BaseIntegerType) -> App e BaseIntegerType
- IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType
- RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
- RealSqrt :: !(e BaseRealType) -> App e BaseRealType
- Pi :: App e BaseRealType
- RealSin :: !(e BaseRealType) -> App e BaseRealType
- RealCos :: !(e BaseRealType) -> App e BaseRealType
- RealATan2 :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
- RealSinh :: !(e BaseRealType) -> App e BaseRealType
- RealCosh :: !(e BaseRealType) -> App e BaseRealType
- RealExp :: !(e BaseRealType) -> App e BaseRealType
- RealLog :: !(e BaseRealType) -> App e BaseRealType
- BVTestBit :: 1 <= w => !Natural -> !(e (BaseBVType w)) -> App e BaseBoolType
- BVSlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
- BVUlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
- BVOrBits :: 1 <= w => !(NatRepr w) -> !(BVOrSet e w) -> App e (BaseBVType w)
- BVUnaryTerm :: 1 <= n => !(UnaryBV (e BaseBoolType) n) -> App e (BaseBVType n)
- BVConcat :: (1 <= u, 1 <= v, 1 <= (u + v)) => !(NatRepr (u + v)) -> !(e (BaseBVType u)) -> !(e (BaseBVType v)) -> App e (BaseBVType (u + v))
- BVSelect :: (1 <= n, (idx + n) <= w) => !(NatRepr idx) -> !(NatRepr n) -> !(e (BaseBVType w)) -> App e (BaseBVType n)
- BVFill :: 1 <= w => !(NatRepr w) -> !(e BaseBoolType) -> App e (BaseBVType w)
- BVUdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVUrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVSdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVSrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVShl :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVLshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVAshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVRol :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVRor :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVZext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r)
- BVSext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r)
- BVPopcount :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVCountTrailingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- BVCountLeadingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
- FloatPZero :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatNZero :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatNaN :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatPInf :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatNInf :: !(FloatPrecisionRepr fpp) -> App e (BaseFloatType fpp)
- FloatNeg :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatAbs :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatSqrt :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatAdd :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatSub :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatMul :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatDiv :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatRem :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatMin :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatMax :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatFMA :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatFpEq :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatFpNe :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatLe :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatLt :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsNaN :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsInf :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsZero :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsPos :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsNeg :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsSubnorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatIsNorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
- FloatCast :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp')) -> App e (BaseFloatType fpp)
- FloatRound :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
- FloatFromBinary :: (2 <= eb, 2 <= sb) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseBVType (eb + sb))) -> App e (BaseFloatType (FloatingPointPrecision eb sb))
- FloatToBinary :: (2 <= eb, 2 <= sb, 1 <= (eb + sb)) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseFloatType (FloatingPointPrecision eb sb))) -> App e (BaseBVType (eb + sb))
- BVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp)
- SBVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp)
- RealToFloat :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e BaseRealType) -> App e (BaseFloatType fpp)
- FloatToBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w)
- FloatToSBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w)
- FloatToReal :: !(e (BaseFloatType fpp)) -> App e BaseRealType
- ArrayMap :: !(Assignment BaseTypeRepr (i ::> itp)) -> !(BaseTypeRepr tp) -> !(ArrayUpdateMap e (i ::> itp) tp) -> !(e (BaseArrayType (i ::> itp) tp)) -> App e (BaseArrayType (i ::> itp) tp)
- ConstantArray :: !(Assignment BaseTypeRepr (i ::> tp)) -> !(BaseTypeRepr b) -> !(e b) -> App e (BaseArrayType (i ::> tp) b)
- UpdateArray :: !(BaseTypeRepr b) -> !(Assignment BaseTypeRepr (i ::> tp)) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> !(e b) -> App e (BaseArrayType (i ::> tp) b)
- SelectArray :: !(BaseTypeRepr b) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> App e b
- NatToInteger :: !(e BaseNatType) -> App e BaseIntegerType
- IntegerToNat :: !(e BaseIntegerType) -> App e BaseNatType
- IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType
- RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType
- BVToNat :: 1 <= w => !(e (BaseBVType w)) -> App e BaseNatType
- BVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
- SBVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
- IntegerToBV :: 1 <= w => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)
- RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
- RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType
- FloorReal :: !(e BaseRealType) -> App e BaseIntegerType
- CeilReal :: !(e BaseRealType) -> App e BaseIntegerType
- Cplx :: !(Complex (e BaseRealType)) -> App e BaseComplexType
- RealPart :: !(e BaseComplexType) -> App e BaseRealType
- ImagPart :: !(e BaseComplexType) -> App e BaseRealType
- StringContains :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIsPrefixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIsSuffixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIndexOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> !(e BaseNatType) -> App e BaseIntegerType
- StringSubstring :: !(StringInfoRepr si) -> !(e (BaseStringType si)) -> !(e BaseNatType) -> !(e BaseNatType) -> App e (BaseStringType si)
- StringAppend :: !(StringInfoRepr si) -> !(StringSeq e si) -> App e (BaseStringType si)
- StringLength :: !(e (BaseStringType si)) -> App e BaseNatType
- StructCtor :: !(Assignment BaseTypeRepr flds) -> !(Assignment e flds) -> App e (BaseStructType flds)
- StructField :: !(e (BaseStructType flds)) -> !(Index flds tp) -> !(BaseTypeRepr tp) -> App e tp
- data NonceAppExpr t (tp :: BaseType)
- nonceExprId :: NonceAppExpr t tp -> Nonce t tp
- nonceExprLoc :: NonceAppExpr t tp -> ProgramLoc
- nonceExprApp :: NonceAppExpr t tp -> NonceApp t (Expr t) tp
- data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where
- Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp
- Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
- Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
- ArrayFromFn :: !(ExprSymFn t e (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret)
- MapOverArrays :: !(ExprSymFn t e (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r)
- ArrayTrueOnEntries :: !(ExprSymFn t e (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType
- FnApp :: !(ExprSymFn t e args ret) -> !(Assignment e args) -> NonceApp t e ret
- data ExprBoundVar t (tp :: BaseType)
- bvarId :: ExprBoundVar t tp -> Nonce t tp
- bvarLoc :: ExprBoundVar t tp -> ProgramLoc
- bvarName :: ExprBoundVar t tp -> SolverSymbol
- bvarKind :: ExprBoundVar t tp -> VarKind
- data VarKind
- boundVars :: Expr t tp -> ST s (BoundVarMap s t)
- data ExprSymFn t e (args :: Ctx BaseType) (ret :: BaseType) = ExprSymFn {
- symFnId :: !(Nonce t (args ::> ret))
- symFnName :: !SolverSymbol
- symFnInfo :: !(SymFnInfo t e args ret)
- symFnLoc :: !ProgramLoc
- data SymFnInfo t e (args :: Ctx BaseType) (ret :: BaseType)
- = UninterpFnInfo !(Assignment BaseTypeRepr args) !(BaseTypeRepr ret)
- | DefinedFnInfo !(Assignment (ExprBoundVar t) args) !(e ret) !UnfoldPolicy
- | MatlabSolverFnInfo !(MatlabSolverFn e args ret) !(Assignment (ExprBoundVar t) args) !(e ret)
- symFnArgTypes :: ExprSymFn t e args ret -> Assignment BaseTypeRepr args
- symFnReturnType :: IsExpr e => ExprSymFn t e args ret -> BaseTypeRepr ret
- type family Coefficient (sr :: SemiRing) :: Type where ...
- data SemiRing
- data BVFlavor
- data SemiRingRepr (sr :: SemiRing) where
- SemiRingNatRepr :: SemiRingRepr SemiRingNat
- SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger
- SemiRingRealRepr :: SemiRingRepr SemiRingReal
- SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)
- data BVFlavorRepr (fv :: BVFlavor) where
- data OrderedSemiRingRepr (sr :: SemiRing) where
- data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing)
- data UnaryBV p (n :: Nat)
- data AppTheory
- 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
Arguments
| :: FloatModeRepr fm | Float interpretation mode (i.e., how are floats translated for the solver). |
| -> st t | Current state for simple builder. |
| -> NonceGenerator IO t | Nonce generator for names |
| -> IO (ExprBuilder t st (Flags fm)) |
Flags
Mode flag for how floating-point values should be interpreted.
Instances
| TestEquality FloatModeRepr Source # | |
Defined in What4.Expr.Builder Methods testEquality :: FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) # | |
| ShowF FloatModeRepr Source # | |
Defined in What4.Expr.Builder Methods withShow :: p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) -> a) -> a # showF :: FloatModeRepr tp -> String # showsPrecF :: Int -> FloatModeRepr tp -> String -> String # | |
| KnownRepr FloatModeRepr FloatReal Source # | |
Defined in What4.Expr.Builder Methods | |
| KnownRepr FloatModeRepr FloatUninterpreted Source # | |
Defined in What4.Expr.Builder Methods | |
| KnownRepr FloatModeRepr FloatIEEE Source # | |
Defined in What4.Expr.Builder Methods | |
data FloatModeRepr :: FloatMode -> Type where Source #
Constructors
| FloatIEEERepr :: FloatModeRepr FloatIEEE | |
| FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted | |
| FloatRealRepr :: FloatModeRepr FloatReal |
Instances
| TestEquality FloatModeRepr Source # | |
Defined in What4.Expr.Builder Methods testEquality :: FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) # | |
| ShowF FloatModeRepr Source # | |
Defined in What4.Expr.Builder Methods withShow :: p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) -> a) -> a # showF :: FloatModeRepr tp -> String # showsPrecF :: Int -> FloatModeRepr tp -> String -> String # | |
| KnownRepr FloatModeRepr FloatReal Source # | |
Defined in What4.Expr.Builder Methods | |
| KnownRepr FloatModeRepr FloatUninterpreted Source # | |
Defined in What4.Expr.Builder Methods | |
| KnownRepr FloatModeRepr FloatIEEE Source # | |
Defined in What4.Expr.Builder Methods | |
| Show (FloatModeRepr fm) Source # | |
Defined in What4.Expr.Builder Methods showsPrec :: Int -> FloatModeRepr fm -> ShowS # show :: FloatModeRepr fm -> String # showList :: [FloatModeRepr fm] -> ShowS # | |
type FloatUninterpreted = FloatUninterpreted Source #
data Flags (fi :: FloatMode) Source #
Instances
Type abbreviations
type BoolExpr t = Expr t BaseBoolType Source #
type NatExpr t = Expr t BaseNatType Source #
type IntegerExpr t = Expr t BaseIntegerType Source #
type RealExpr t = Expr t BaseRealType Source #
type BVExpr t n = Expr t (BaseBVType n) Source #
type CplxExpr t = Expr t BaseComplexType Source #
type StringExpr t si = Expr t (BaseStringType si) Source #
Expression datatypes
data Expr t (tp :: BaseType) where Source #
The main ExprBuilder expression datastructure. The non-trivial Expr
values constructed by this module are uniquely identified by a
nonce value that is used to explicitly represent sub-term sharing.
When traversing the structure of an Expr it is usually very important
to memoize computations based on the values of these identifiers to avoid
exponential blowups due to shared term structure.
Type parameter t is a phantom type brand used to relate nonces to
a specific nonce generator (similar to the s parameter of the
ST monad). The type index tp of kind BaseType indicates the
type of the values denoted by the given expression.
Type Expr tSymExpr
(ExprBuilder t st)
Constructors
| SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr) | |
| BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType | |
| StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si) | |
| AppExpr :: !(AppExpr t tp) -> Expr t tp | |
| NonceAppExpr :: !(NonceAppExpr t tp) -> Expr t tp | |
| BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp |
Instances
exprLoc :: Expr t tp -> ProgramLoc Source #
App expressions
appExprLoc :: AppExpr t tp -> ProgramLoc Source #
data App (e :: BaseType -> Type) (tp :: BaseType) where Source #
Type App e tpExpr
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
Instances
| FoldableFC App Source # | |
Defined in What4.Expr.App Methods foldMapFC :: Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). App f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App f x -> b # foldlFC :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App f x -> b # foldlFC' :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). App f x -> [a] # | |
| (Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => TestEquality (App e :: BaseType -> Type) Source # | |
Defined in What4.Expr.App | |
| (OrdF e, HashableF e, HasAbsValue e, Hashable (e BaseBoolType), Hashable (e BaseRealType)) => HashableF (App e :: BaseType -> Type) Source # | |
Defined in What4.Expr.App | |
| (Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => Eq (App e tp) Source # | |
| ShowF e => Show (App e u) Source # | |
| ShowF e => Pretty (App e u) Source # | |
Defined in What4.Expr.App | |
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
nonceExprId :: NonceAppExpr t tp -> Nonce t tp Source #
nonceExprLoc :: NonceAppExpr t tp -> ProgramLoc Source #
nonceExprApp :: NonceAppExpr t tp -> NonceApp t (Expr t) tp Source #
data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where Source #
Type NonceApp t e tp encodes the top-level application of an
Expr. It includes expression forms that bind variables (contrast
with App).
Parameter t is a phantom type brand used to track nonces.
Parameter e is used everywhere a recursive sub-expression would
go. Uses of the NonceApp type will tie the knot through this
parameter. Parameter tp indicates the type of the expression.
Constructors
| Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp | |
| Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType | |
| Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType | |
| ArrayFromFn :: !(ExprSymFn t e (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret) | |
| MapOverArrays :: !(ExprSymFn t e (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r) | |
| ArrayTrueOnEntries :: !(ExprSymFn t e (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType | |
| FnApp :: !(ExprSymFn t e args ret) -> !(Assignment e args) -> NonceApp t e ret |
Instances
| FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # | |
Defined in What4.Expr.App | |
| FoldableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # | |
Defined in What4.Expr.App Methods foldMapFC :: Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). NonceApp t f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> NonceApp t f x -> b # foldlFC :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> NonceApp t f x -> b # foldlFC' :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> NonceApp t f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). NonceApp t f x -> [a] # | |
| TraversableFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # | |
Defined in What4.Expr.App Methods traverseFC :: Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). NonceApp t f x -> m (NonceApp t g x) # | |
| TestEquality e => TestEquality (NonceApp t e :: BaseType -> Type) Source # | |
Defined in What4.Expr.App | |
| HashableF e => HashableF (NonceApp t e :: BaseType -> Type) Source # | |
Defined in What4.Expr.App | |
| TestEquality e => Eq (NonceApp t e tp) 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 tBoundVar (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
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 #
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 |
Symbolic functions
data ExprSymFn t e (args :: Ctx BaseType) (ret :: BaseType) Source #
This represents a symbolic function in the simulator.
Parameter t is a phantom type brand used to track nonces.
Parameter e is used everywhere a recursive sub-expression would
go. The args and ret parameters define the types of arguments
and the return type of the function.
Type ExprSymFn t (Expr t)SymFn
(ExprBuilder t st)
Constructors
| ExprSymFn | |
Fields
| |
Instances
| IsExpr e => IsSymFn (ExprSymFn t e) Source # | |
Defined in What4.Expr.App Methods fnArgTypes :: ExprSymFn t e args ret -> Assignment BaseTypeRepr args Source # fnReturnType :: ExprSymFn t e args ret -> BaseTypeRepr ret Source # | |
| Show (ExprSymFn t e args ret) Source # | |
| Hashable (ExprSymFn t e args tp) Source # | |
Defined in What4.Expr.App | |
data SymFnInfo t e (args :: Ctx BaseType) (ret :: BaseType) Source #
This describes information about an undefined or defined function.
Parameter t is a phantom type brand used to track nonces.
Parameter e is used everywhere a recursive sub-expression would
go. The args and ret parameters define the types of arguments
and the return type of the function.
Constructors
| UninterpFnInfo !(Assignment BaseTypeRepr args) !(BaseTypeRepr ret) | Information about the argument type and return type of an uninterpreted function. |
| DefinedFnInfo !(Assignment (ExprBoundVar t) args) !(e ret) !UnfoldPolicy | Information about a defined function. Includes bound variables and an expression associated to a defined function, as well as a policy for when to unfold the body. |
| MatlabSolverFnInfo !(MatlabSolverFn e args ret) !(Assignment (ExprBoundVar t) args) !(e ret) | This is a function that corresponds to a matlab solver function. It includes the definition as a ExprBuilder expr to enable export to other solvers. |
symFnArgTypes :: ExprSymFn t e args ret -> Assignment BaseTypeRepr args Source #
symFnReturnType :: IsExpr e => ExprSymFn t e args ret -> BaseTypeRepr ret Source #
Semirings
type family Coefficient (sr :: SemiRing) :: Type where ... Source #
The constant values in the semiring.
Equations
| Coefficient SemiRingNat = Natural | |
| Coefficient SemiRingInteger = Integer | |
| Coefficient SemiRingReal = Rational | |
| Coefficient (SemiRingBV fv w) = BV w |
Data-kind representing the semirings What4 supports.
Instances
Data-kind indicating the two flavors of bitvector semirings. The ordinary arithmetic semiring consists of addition and multiplication, and the "bits" semiring consists of bitwise xor and bitwise and.
Instances
| TestEquality BVFlavorRepr Source # | |
Defined in What4.SemiRing Methods testEquality :: BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) # | |
| OrdF BVFlavorRepr Source # | |
Defined in What4.SemiRing Methods compareF :: BVFlavorRepr x -> BVFlavorRepr y -> OrderingF x y # leqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # ltF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # geqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # gtF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # | |
| HashableF BVFlavorRepr Source # | |
Defined in What4.SemiRing | |
data SemiRingRepr (sr :: SemiRing) where Source #
Constructors
| SemiRingNatRepr :: SemiRingRepr SemiRingNat | |
| SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger | |
| SemiRingRealRepr :: SemiRingRepr SemiRingReal | |
| SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w) |
Instances
| TestEquality SemiRingRepr Source # | |
Defined in What4.SemiRing Methods testEquality :: SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) # | |
| OrdF SemiRingRepr Source # | |
Defined in What4.SemiRing Methods compareF :: SemiRingRepr x -> SemiRingRepr y -> OrderingF x y # leqF :: SemiRingRepr x -> SemiRingRepr y -> Bool # ltF :: SemiRingRepr x -> SemiRingRepr y -> Bool # geqF :: SemiRingRepr x -> SemiRingRepr y -> Bool # gtF :: SemiRingRepr x -> SemiRingRepr y -> Bool # | |
| HashableF SemiRingRepr Source # | |
Defined in What4.SemiRing | |
| Hashable (SemiRingRepr sr) Source # | |
Defined in What4.SemiRing | |
data BVFlavorRepr (fv :: BVFlavor) where Source #
Constructors
| BVArithRepr :: BVFlavorRepr BVArith | |
| BVBitsRepr :: BVFlavorRepr BVBits |
Instances
| TestEquality BVFlavorRepr Source # | |
Defined in What4.SemiRing Methods testEquality :: BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) # | |
| OrdF BVFlavorRepr Source # | |
Defined in What4.SemiRing Methods compareF :: BVFlavorRepr x -> BVFlavorRepr y -> OrderingF x y # leqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # ltF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # geqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # gtF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # | |
| HashableF BVFlavorRepr Source # | |
Defined in What4.SemiRing | |
| Hashable (BVFlavorRepr fv) Source # | |
Defined in What4.SemiRing | |
data OrderedSemiRingRepr (sr :: SemiRing) where Source #
The subset of semirings that are equipped with an appropriate (order-respecting) total order.
Constructors
| OrderedSemiRingNatRepr :: OrderedSemiRingRepr SemiRingNat | |
| OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger | |
| OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal |
Instances
| TestEquality OrderedSemiRingRepr Source # | |
Defined in What4.SemiRing Methods testEquality :: OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) # | |
| OrdF OrderedSemiRingRepr Source # | |
Defined in What4.SemiRing Methods compareF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> OrderingF x y # leqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # ltF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # geqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # gtF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # | |
| HashableF OrderedSemiRingRepr Source # | |
Defined in What4.SemiRing Methods hashWithSaltF :: Int -> OrderedSemiRingRepr tp -> Int # hashF :: OrderedSemiRingRepr tp -> Int # | |
| Hashable (OrderedSemiRingRepr sr) Source # | |
Defined in What4.SemiRing Methods hashWithSalt :: Int -> OrderedSemiRingRepr sr -> Int # hash :: OrderedSemiRingRepr sr -> Int # | |
data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing) Source #
A weighted sum of semiring values. Mathematically, this represents an affine operation on the underlying expressions.
Instances
| OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source # | |
Defined in What4.Expr.WeightedSum Methods testEquality :: WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) # | |
| OrdF f => Hashable (WeightedSum f sr) Source # | |
Defined in What4.Expr.WeightedSum | |
Unary BV
data UnaryBV p (n :: Nat) Source #
A unary bitvector encoding where the map contains predicates
such as u^.unaryBVMap^.at i holds iff the value represented by u
is less than or equal to i.
The map stored in the representation should always have a single element, and the largest integer stored in the map should be associated with a predicate representing "true". This means that if the map contains only a single binding, then it represents a constant.
Instances
| Eq p => TestEquality (UnaryBV p :: Nat -> Type) Source # | |
Defined in What4.Expr.UnaryBV | |
| Hashable p => Hashable (UnaryBV p n) Source # | |
Defined in What4.Expr.UnaryBV | |
Logic theories
The theory that a symbol belongs to.
Constructors
| BoolTheory | |
| LinearArithTheory | |
| NonlinearArithTheory | |
| ComputableArithTheory | |
| BitvectorTheory | |
| QuantifierTheory | |
| StringTheory | |
| FloatingPointTheory | |
| ArrayTheory | |
| StructTheory | Theory attributed to structs (equivalent to records in CVC4/Z3, tuples in Yices) |
| FnTheory | Theory attributed application functions. |
Instances
| Eq AppTheory Source # | |
| Ord AppTheory Source # | |
Ground evaluation
type family GroundValue (tp :: BaseType) where ... Source #
Equations
| GroundValue BaseBoolType = Bool | |
| GroundValue BaseNatType = Natural | |
| GroundValue BaseIntegerType = Integer | |
| GroundValue BaseRealType = Rational | |
| GroundValue (BaseBVType w) = BV w | |
| GroundValue (BaseFloatType fpp) = BV (FloatPrecisionBits fpp) | |
| GroundValue BaseComplexType = Complex Rational | |
| GroundValue (BaseStringType si) = StringLiteral si | |
| GroundValue (BaseArrayType idx b) = GroundArray idx b | |
| GroundValue (BaseStructType ctx) = Assignment GroundValueWrapper ctx |
newtype GroundValueWrapper tp Source #
A newtype wrapper around ground value for use in a cache.
Constructors
| GVW | |
Fields
| |
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
| |