| Copyright | (c) Galois Inc 2015-2020 |
|---|---|
| License | BSD3 |
| Maintainer | jhendrix@galois.com |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Expr.Builder
Description
This module defines the canonical implementation of the solver interface
from What4.Interface. Type ExprBuilder t stIsExprBuilder and IsSymExprBuilder.
Notes regarding concurrency: The expression builder datatype contains a number of mutable storage locations. These are designed so they may reasonably be used in a multithreaded context. In particular, nonce values are generated atomically, and other IORefs used in this module are modified or written atomically, so modifications should propagate in the expected sequentially-consistent ways. Of course, threads may still clobber state others have set (e.g., the current program location) so the potential for truly multithreaded use is somewhat limited.
Synopsis
- data ExprBuilder t (st :: Type -> Type) (fs :: Type)
- newExprBuilder :: FloatModeRepr fm -> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
- getSymbolVarBimap :: ExprBuilder t st fs -> IO (SymbolVarBimap t)
- sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
- sbNonceExpr :: ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp)
- curProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc
- sbUnaryThreshold :: ExprBuilder t st fs -> OptionSetting BaseIntegerType
- sbCacheStartSize :: ExprBuilder t st fs -> OptionSetting BaseIntegerType
- sbBVDomainRangeLimit :: ExprBuilder t st fs -> OptionSetting BaseIntegerType
- sbUserState :: ExprBuilder t st fs -> st t
- exprCounter :: ExprBuilder t st fs -> NonceGenerator IO t
- startCaching :: ExprBuilder t st fs -> IO ()
- stopCaching :: ExprBuilder t st fs -> IO ()
- bvUnary :: 1 <= w => ExprBuilder t st fs -> UnaryBV (BoolExpr t) w -> IO (BVExpr t w)
- intSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingInteger -> IO (IntegerExpr t)
- realSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingReal -> IO (RealExpr t)
- bvSum :: ExprBuilder t st fs -> WeightedSum (Expr t) (SemiRingBV flv w) -> IO (BVExpr t w)
- scalarMul :: ExprBuilder t st fs -> SemiRingRepr sr -> Coefficient sr -> Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr))
- unaryThresholdOption :: ConfigOption BaseIntegerType
- bvdomainRangeLimitOption :: ConfigOption BaseIntegerType
- cacheStartSizeOption :: ConfigOption BaseIntegerType
- cacheTerms :: ConfigOption BaseBoolType
- data Expr t (tp :: BaseType) where
- SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr)
- BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
- FloatExpr :: !(FloatPrecisionRepr fpp) -> !BigFloat -> !ProgramLoc -> Expr t (BaseFloatType fpp)
- StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si)
- AppExpr :: !(AppExpr t tp) -> Expr t tp
- NonceAppExpr :: !(NonceAppExpr t tp) -> Expr t tp
- BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp
- asApp :: Expr t tp -> Maybe (App (Expr t) tp)
- asNonceApp :: Expr t tp -> Maybe (NonceApp t (Expr t) tp)
- iteSize :: Expr t tp -> Integer
- exprLoc :: Expr t tp -> ProgramLoc
- ppExpr :: Expr t tp -> Doc ann
- ppExprTop :: Expr t tp -> Doc ann
- exprMaybeId :: Expr t tp -> Maybe (Nonce t tp)
- asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
- asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
- data Polarity
- negatePolarity :: Polarity -> Polarity
- data AppExpr t (tp :: BaseType)
- appExprId :: AppExpr t tp -> Nonce t tp
- appExprLoc :: AppExpr t tp -> ProgramLoc
- appExprApp :: AppExpr t tp -> App (Expr t) tp
- data NonceAppExpr t (tp :: BaseType)
- nonceExprId :: NonceAppExpr t tp -> Nonce t tp
- nonceExprLoc :: NonceAppExpr t tp -> ProgramLoc
- nonceExprApp :: NonceAppExpr t tp -> NonceApp t (Expr t) tp
- type BoolExpr t = Expr t BaseBoolType
- type IntegerExpr t = Expr t BaseIntegerType
- type RealExpr t = Expr t BaseRealType
- type FloatExpr t fpp = Expr t (BaseFloatType fpp)
- type BVExpr t n = Expr t (BaseBVType n)
- type CplxExpr t = Expr t BaseComplexType
- type StringExpr t si = Expr t (BaseStringType si)
- data App (e :: BaseType -> Type) (tp :: BaseType) where
- BaseIte :: !(BaseTypeRepr tp) -> !Integer -> !(e BaseBoolType) -> !(e tp) -> !(e tp) -> App e tp
- BaseEq :: !(BaseTypeRepr tp) -> !(e tp) -> !(e tp) -> App e BaseBoolType
- NotPred :: !(e BaseBoolType) -> App e BaseBoolType
- ConjPred :: !(BoolMap e) -> App e BaseBoolType
- SemiRingSum :: !(WeightedSum e sr) -> App e (SemiRingBase sr)
- SemiRingProd :: !(SemiRingProduct e sr) -> App e (SemiRingBase sr)
- SemiRingLe :: !(OrderedSemiRingRepr sr) -> !(e (SemiRingBase sr)) -> !(e (SemiRingBase sr)) -> App e BaseBoolType
- RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType
- IntDiv :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
- IntMod :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
- IntAbs :: !(e BaseIntegerType) -> App e BaseIntegerType
- IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType
- RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
- RealSqrt :: !(e BaseRealType) -> App e BaseRealType
- 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)
- 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
- 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
- IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType
- RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType
- BVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
- SBVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
- IntegerToBV :: 1 <= w => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)
- RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
- RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType
- FloorReal :: !(e BaseRealType) -> App e BaseIntegerType
- CeilReal :: !(e BaseRealType) -> App e BaseIntegerType
- Cplx :: !(Complex (e BaseRealType)) -> App e BaseComplexType
- RealPart :: !(e BaseComplexType) -> App e BaseRealType
- ImagPart :: !(e BaseComplexType) -> App e BaseRealType
- StringContains :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIsPrefixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIsSuffixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
- StringIndexOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> !(e BaseIntegerType) -> App e BaseIntegerType
- StringSubstring :: !(StringInfoRepr si) -> !(e (BaseStringType si)) -> !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e (BaseStringType si)
- StringAppend :: !(StringInfoRepr si) -> !(StringSeq e si) -> App e (BaseStringType si)
- StringLength :: !(e (BaseStringType si)) -> App e BaseIntegerType
- StructCtor :: !(Assignment BaseTypeRepr flds) -> !(Assignment e flds) -> App e (BaseStructType flds)
- StructField :: !(e (BaseStructType flds)) -> !(Index flds tp) -> !(BaseTypeRepr tp) -> App e tp
- traverseApp :: (Applicative m, OrdF f, Eq (f BaseBoolType), HashableF f, HasAbsValue f) => (forall tp. e tp -> m (f tp)) -> App e utp -> m (App f utp)
- appType :: App e tp -> BaseTypeRepr tp
- data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where
- Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp
- Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
- Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
- ArrayFromFn :: !(ExprSymFn t (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret)
- MapOverArrays :: !(ExprSymFn t (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r)
- ArrayTrueOnEntries :: !(ExprSymFn t (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType
- FnApp :: !(ExprSymFn t args ret) -> !(Assignment e args) -> NonceApp t e ret
- nonceAppType :: IsExpr e => NonceApp t e tp -> BaseTypeRepr tp
- data ExprBoundVar t (tp :: BaseType)
- bvarId :: ExprBoundVar t tp -> Nonce t tp
- bvarLoc :: ExprBoundVar t tp -> ProgramLoc
- bvarName :: ExprBoundVar t tp -> SolverSymbol
- bvarType :: ExprBoundVar t tp -> BaseTypeRepr tp
- bvarKind :: ExprBoundVar t tp -> VarKind
- bvarAbstractValue :: ExprBoundVar t tp -> Maybe (AbstractValue tp)
- data VarKind
- boundVars :: Expr t tp -> ST s (BoundVarMap s t)
- ppBoundVar :: ExprBoundVar t tp -> String
- evalBoundVars :: ExprBuilder t st fs -> Expr t ret -> Assignment (ExprBoundVar t) args -> Assignment (Expr t) args -> IO (Expr t ret)
- data ExprSymFn t (args :: Ctx BaseType) (ret :: BaseType) = ExprSymFn {
- symFnId :: !(Nonce t (args ::> ret))
- symFnName :: !SolverSymbol
- symFnInfo :: !(SymFnInfo t args ret)
- symFnLoc :: !ProgramLoc
- data SymFnInfo t (args :: Ctx BaseType) (ret :: BaseType)
- = UninterpFnInfo !(Assignment BaseTypeRepr args) !(BaseTypeRepr ret)
- | DefinedFnInfo !(Assignment (ExprBoundVar t) args) !(Expr t ret) !UnfoldPolicy
- | MatlabSolverFnInfo !(MatlabSolverFn (Expr t) args ret) !(Assignment (ExprBoundVar t) args) !(Expr t ret)
- symFnArgTypes :: ExprSymFn t args ret -> Assignment BaseTypeRepr args
- symFnReturnType :: ExprSymFn t args ret -> BaseTypeRepr ret
- data SymbolVarBimap t
- data SymbolBinding t
- = forall tp. VarSymbolBinding !(ExprBoundVar t tp)
- | forall args ret. FnSymbolBinding !(ExprSymFn t args ret)
- emptySymbolVarBimap :: SymbolVarBimap t
- lookupBindingOfSymbol :: SolverSymbol -> SymbolVarBimap t -> Maybe (SymbolBinding t)
- lookupSymbolOfBinding :: SymbolBinding t -> SymbolVarBimap t -> Maybe SolverSymbol
- data IdxCache t (f :: BaseType -> Type)
- newIdxCache :: MonadIO m => m (IdxCache t f)
- lookupIdx :: MonadIO m => IdxCache t f -> Nonce t tp -> m (Maybe (f tp))
- lookupIdxValue :: MonadIO m => IdxCache t f -> Expr t tp -> m (Maybe (f tp))
- insertIdxValue :: MonadIO m => IdxCache t f -> Nonce t tp -> f tp -> m ()
- deleteIdxValue :: MonadIO m => IdxCache t f -> Nonce t (tp :: BaseType) -> m ()
- clearIdxCache :: MonadIO m => IdxCache t f -> m ()
- idxCacheEval :: MonadIO m => IdxCache t f -> Expr t tp -> m (f tp) -> m (f tp)
- idxCacheEval' :: MonadIO m => IdxCache t f -> Nonce t tp -> m (f tp) -> m (f tp)
- data FloatMode
- data FloatModeRepr :: FloatMode -> Type where
- type FloatIEEE = 'FloatIEEE
- type FloatUninterpreted = 'FloatUninterpreted
- type FloatReal = 'FloatReal
- data Flags (fi :: FloatMode)
- data BVOrSet e w
- bvOrToList :: BVOrSet e w -> [e (BaseBVType w)]
- bvOrSingleton :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w
- bvOrInsert :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w
- bvOrUnion :: OrdF e => BVOrSet e w -> BVOrSet e w -> BVOrSet e w
- bvOrAbs :: (OrdF e, 1 <= w) => NatRepr w -> BVOrSet e w -> BVDomain w
- traverseBVOrSet :: (HashableF f, HasAbsValue f, OrdF f, Applicative m) => (forall tp. e tp -> m (f tp)) -> BVOrSet e w -> m (BVOrSet f w)
- type family SymExpr (sym :: Type) :: BaseType -> Type
- bvWidth :: IsExpr e => e (BaseBVType w) -> NatRepr w
- exprType :: IsExpr e => e tp -> BaseTypeRepr tp
- data IndexLit idx where
- IntIndexLit :: !Integer -> IndexLit BaseIntegerType
- BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w)
- newtype ArrayResultWrapper f idx tp = ArrayResultWrapper {
- unwrapArrayResult :: f (BaseArrayType idx tp)
ExprBuilder
data ExprBuilder t (st :: Type -> Type) (fs :: Type) Source #
Cache for storing dag terms.
Parameter t is a phantom type brand used to track nonces.
Instances
Arguments
| :: FloatModeRepr fm | Float interpretation mode (i.e., how are floats translated for the solver). |
| -> st t | Initial state for the expression builder |
| -> NonceGenerator IO t | Nonce generator for names |
| -> IO (ExprBuilder t st (Flags fm)) |
getSymbolVarBimap :: ExprBuilder t st fs -> IO (SymbolVarBimap t) Source #
Get current variable bindings.
sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp) Source #
sbNonceExpr :: ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp) Source #
Create an element from a nonce app.
curProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc Source #
sbUnaryThreshold :: ExprBuilder t st fs -> OptionSetting BaseIntegerType Source #
The maximum number of distinct values a term may have and use the unary representation.
sbCacheStartSize :: ExprBuilder t st fs -> OptionSetting BaseIntegerType Source #
The starting size when building a new cache
sbBVDomainRangeLimit :: ExprBuilder t st fs -> OptionSetting BaseIntegerType Source #
The maximum number of distinct ranges in a BVDomain expression.
sbUserState :: ExprBuilder t st fs -> st t Source #
Additional state maintained by the state manager
exprCounter :: ExprBuilder t st fs -> NonceGenerator IO t Source #
Counter to generate new unique identifiers for elements and functions.
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.
Specialized representations
intSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingInteger -> IO (IntegerExpr t) Source #
Evaluate a weighted sum of integer values.
realSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingReal -> IO (RealExpr t) Source #
Evaluate a weighted sum of real values.
bvSum :: ExprBuilder t st fs -> WeightedSum (Expr t) (SemiRingBV flv w) -> IO (BVExpr t w) Source #
scalarMul :: ExprBuilder t st fs -> SemiRingRepr sr -> Coefficient sr -> Expr t (SemiRingBase sr) -> IO (Expr t (SemiRingBase sr)) Source #
configuration options
unaryThresholdOption :: ConfigOption BaseIntegerType Source #
Maximum number of values in unary bitvector encoding.
This option is named "backend.unary_threshold"
bvdomainRangeLimitOption :: ConfigOption BaseIntegerType Source #
Maximum number of ranges in bitvector abstract domains.
This option is named "backend.bvdomain_range_limit"
cacheStartSizeOption :: ConfigOption BaseIntegerType Source #
Starting size for element cache when caching is enabled.
This option is named "backend.cache_start_size"
cacheTerms :: ConfigOption BaseBoolType Source #
Indicates if we should cache terms. When enabled, hash-consing is used to find and deduplicate common subexpressions.
This option is named "use_cache"
Expr
data Expr t (tp :: BaseType) where Source #
The main ExprBuilder expression datastructure. The non-trivial Expr
values constructed by this module are uniquely identified by a
nonce value that is used to explicitly represent sub-term sharing.
When traversing the structure of an Expr it is usually very important
to memoize computations based on the values of these identifiers to avoid
exponential blowups due to shared term structure.
Type parameter t is a phantom type brand used to relate nonces to
a specific nonce generator (similar to the s parameter of the
ST monad). The type index tp of kind BaseType indicates the
type of the values denoted by the given expression.
Type Expr tSymExpr
(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
asNonceApp :: Expr t tp -> Maybe (NonceApp t (Expr t) tp) Source #
Destructor for the NonceAppExpr constructor.
exprLoc :: Expr t tp -> ProgramLoc Source #
asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)] Source #
asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)] Source #
Describes the occurrence of a variable or expression, whether it is negated or not.
negatePolarity :: Polarity -> Polarity Source #
Swap a polarity value
AppExpr
appExprLoc :: AppExpr t tp -> ProgramLoc Source #
NonceAppExpr
data NonceAppExpr t (tp :: BaseType) Source #
This type represents Expr values that were built from a
NonceApp.
Parameter t is a phantom type brand used to track nonces.
Selector functions are provided to destruct NonceAppExpr values,
but the constructor is kept hidden. The preferred way to construct
an Expr from a NonceApp is to use sbNonceExpr.
Instances
nonceExprId :: NonceAppExpr t tp -> Nonce t tp Source #
nonceExprLoc :: NonceAppExpr t tp -> ProgramLoc Source #
nonceExprApp :: NonceAppExpr t tp -> NonceApp t (Expr t) tp Source #
Type abbreviations
type BoolExpr t = Expr t BaseBoolType Source #
type IntegerExpr t = Expr t BaseIntegerType Source #
type RealExpr t = Expr t BaseRealType Source #
type FloatExpr t fpp = Expr t (BaseFloatType fpp) Source #
type BVExpr t n = Expr t (BaseBVType n) Source #
type CplxExpr t = Expr t BaseComplexType Source #
type StringExpr t si = Expr t (BaseStringType si) Source #
App
data App (e :: BaseType -> Type) (tp :: BaseType) where Source #
Type App e 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 :: forall f m. 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 f b. (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 f b. (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 | |
traverseApp :: (Applicative m, OrdF f, Eq (f BaseBoolType), HashableF f, HasAbsValue f) => (forall tp. e tp -> m (f tp)) -> App e utp -> m (App f utp) Source #
appType :: App e tp -> BaseTypeRepr tp Source #
NonceApp
data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where Source #
Type NonceApp t e tp encodes the top-level application of an
Expr. It includes expression forms that bind variables (contrast
with App).
Parameter t is a phantom type brand used to track nonces.
Parameter e is used everywhere a recursive sub-expression would
go. Uses of the NonceApp type will tie the knot through this
parameter. Parameter tp indicates the type of the expression.
Constructors
| Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp | |
| Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType | |
| Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType | |
| ArrayFromFn :: !(ExprSymFn t (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret) | |
| MapOverArrays :: !(ExprSymFn t (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r) | |
| ArrayTrueOnEntries :: !(ExprSymFn t (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType | |
| FnApp :: !(ExprSymFn t args ret) -> !(Assignment e args) -> NonceApp t e ret |
Instances
| 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 :: forall f m. 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 f b. (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 f b. (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 :: 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) # | |
| 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 # | |
nonceAppType :: IsExpr e => NonceApp t e tp -> BaseTypeRepr tp Source #
Bound Variable information
data ExprBoundVar t (tp :: BaseType) Source #
Information about bound variables.
Parameter t is a phantom type brand used to track nonces.
Type ExprBoundVar 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 #
bvarType :: ExprBoundVar t tp -> BaseTypeRepr tp Source #
bvarKind :: ExprBoundVar t tp -> VarKind Source #
bvarAbstractValue :: ExprBoundVar t tp -> Maybe (AbstractValue tp) 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 |
ppBoundVar :: ExprBoundVar t tp -> String Source #
evalBoundVars :: ExprBuilder t st fs -> Expr t ret -> Assignment (ExprBoundVar t) args -> Assignment (Expr t) args -> IO (Expr t ret) Source #
This evaluates the term with the given bound variables rebound to the given arguments.
The algorithm works by traversing the subterms in the term in a bottom-up fashion while using a hash-table to memoize results for shared subterms. The hash-table is pre-populated so that the bound variables map to the element, so we do not need any extra map lookup when checking to see if a variable is bound.
NOTE: This function assumes that variables in the substitution are not
themselves bound in the term (e.g. in a function definition or quantifier).
If this is not respected, then evalBoundVars will call fail with an
error message.
Symbolic Function
data ExprSymFn t (args :: Ctx BaseType) (ret :: BaseType) Source #
This represents a symbolic function in the simulator.
Parameter t is a phantom type brand used to track nonces.
The args and ret parameters define the types of arguments
and the return type of the function.
Type ExprSymFn t (Expr t)SymFn
(ExprBuilder t st)
Constructors
| ExprSymFn | |
Fields
| |
Instances
| IsSymFn (ExprSymFn t) Source # | |
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 # | |
| Show (ExprSymFn t args ret) Source # | |
| Hashable (ExprSymFn t args tp) Source # | |
Defined in What4.Expr.App | |
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 #
SymbolVarBimap
data SymbolVarBimap t Source #
A bijective map between vars and their canonical name for printing
purposes.
Parameter t is a phantom type brand used to track nonces.
data SymbolBinding t Source #
This describes what a given SolverSymbol is associated with.
Parameter t is a phantom type brand used to track nonces.
Constructors
| forall tp. VarSymbolBinding !(ExprBoundVar t tp) | Solver |
| forall args ret. FnSymbolBinding !(ExprSymFn t args ret) |
Instances
| Eq (SymbolBinding t) Source # | |
Defined in What4.Expr.Builder Methods (==) :: SymbolBinding t -> SymbolBinding t -> Bool # (/=) :: SymbolBinding t -> SymbolBinding t -> Bool # | |
| Ord (SymbolBinding t) Source # | |
Defined in What4.Expr.Builder Methods compare :: SymbolBinding t -> SymbolBinding t -> Ordering # (<) :: SymbolBinding t -> SymbolBinding t -> Bool # (<=) :: SymbolBinding t -> SymbolBinding t -> Bool # (>) :: SymbolBinding t -> SymbolBinding t -> Bool # (>=) :: SymbolBinding t -> SymbolBinding t -> Bool # max :: SymbolBinding t -> SymbolBinding t -> SymbolBinding t # min :: SymbolBinding t -> SymbolBinding t -> SymbolBinding t # | |
emptySymbolVarBimap :: SymbolVarBimap t Source #
Empty symbol var bimap
lookupBindingOfSymbol :: SolverSymbol -> SymbolVarBimap t -> Maybe (SymbolBinding t) Source #
lookupSymbolOfBinding :: SymbolBinding t -> SymbolVarBimap t -> Maybe SolverSymbol Source #
IdxCache
data IdxCache t (f :: BaseType -> Type) Source #
An IdxCache is used to map expressions with type Expr t tp to
values with a corresponding type f tp. It is a mutable map using
an IO hash table. Parameter t is a phantom type brand used to
track nonces.
newIdxCache :: MonadIO m => m (IdxCache t f) Source #
Create a new IdxCache
lookupIdxValue :: MonadIO m => IdxCache t f -> Expr t tp -> m (Maybe (f tp)) Source #
Return the value associated to the expr in the index.
insertIdxValue :: MonadIO m => IdxCache t f -> Nonce t tp -> f tp -> m () Source #
Bind the value to the given expr in the index.
deleteIdxValue :: MonadIO m => IdxCache t f -> Nonce t (tp :: BaseType) -> m () Source #
Remove a value from the IdxCache
clearIdxCache :: MonadIO m => IdxCache t f -> m () Source #
Remove all values from the IdxCache
idxCacheEval :: MonadIO m => IdxCache t f -> Expr t tp -> m (f tp) -> m (f tp) Source #
Implements a cached evaluated using the given element. Given an element this function returns the value of the element if bound, and otherwise calls the evaluation function, stores the result in the cache, and returns the value.
idxCacheEval' :: MonadIO m => IdxCache t f -> Nonce t tp -> m (f tp) -> m (f tp) Source #
Implements a cached evaluated using the given element. Given an element this function returns the value of the element if bound, and otherwise calls the evaluation function, stores the result in the cache, and returns the value.
Flags
Mode flag for how floating-point values should be interpreted.
Instances
| TestEquality FloatModeRepr Source # | |
Defined in What4.Expr.Builder Methods testEquality :: forall (a :: k) (b :: k). FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) # | |
| ShowF FloatModeRepr Source # | |
Defined in What4.Expr.Builder Methods withShow :: forall p q (tp :: k) a. p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) => a) -> a # showF :: forall (tp :: k). FloatModeRepr tp -> String # showsPrecF :: forall (tp :: k). 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 :: forall (a :: k) (b :: k). FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) # | |
| ShowF FloatModeRepr Source # | |
Defined in What4.Expr.Builder Methods withShow :: forall p q (tp :: k) a. p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) => a) -> a # showF :: forall (tp :: k). FloatModeRepr tp -> String # showsPrecF :: forall (tp :: k). 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
BV Or Set
bvOrToList :: BVOrSet e w -> [e (BaseBVType w)] Source #
bvOrSingleton :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w Source #
bvOrInsert :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w Source #
traverseBVOrSet :: (HashableF f, HasAbsValue f, OrdF f, Applicative m) => (forall tp. e tp -> m (f tp)) -> BVOrSet e w -> m (BVOrSet f w) Source #
Re-exports
type family SymExpr (sym :: Type) :: BaseType -> Type Source #
The class for expressions.
Instances
| type SymExpr (ExprBuilder t st fs) Source # | |
Defined in What4.Expr.Builder | |
exprType :: IsExpr e => e tp -> BaseTypeRepr tp Source #
Get type of expression.
data IndexLit idx where Source #
This represents a concrete index value, and is used for creating arrays.
Constructors
| IntIndexLit :: !Integer -> IndexLit BaseIntegerType | |
| BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w) |
Instances
| TestEquality IndexLit Source # | |
Defined in What4.IndexLit | |
| OrdF IndexLit Source # | |
Defined in What4.IndexLit Methods compareF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool # ltF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool # geqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool # gtF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool # | |
| ShowF IndexLit Source # | |
| HashableF IndexLit Source # | |
Defined in What4.IndexLit | |
| Eq (IndexLit tp) Source # | |
| Show (IndexLit tp) Source # | |
| Hashable (IndexLit tp) Source # | |
Defined in What4.IndexLit | |
newtype ArrayResultWrapper f idx tp Source #
Constructors
| ArrayResultWrapper | |
Fields
| |
Instances
| TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type) Source # | |
Defined in What4.Interface Methods testEquality :: forall (a :: k) (b :: k). ArrayResultWrapper f idx a -> ArrayResultWrapper f idx b -> Maybe (a :~: b) # | |
| HashableF e => HashableF (ArrayResultWrapper e idx :: BaseType -> Type) Source # | |
Defined in What4.Interface Methods hashWithSaltF :: forall (tp :: k). Int -> ArrayResultWrapper e idx tp -> Int # hashF :: forall (tp :: k). ArrayResultWrapper e idx tp -> Int # | |