Copyright | (c) Galois Inc 2015-2020 |
---|---|
License | BSD3 |
Maintainer | jhendrix@galois.com |
Safe Haskell | None |
Language | Haskell2010 |
This module defines the canonical implementation of the solver interface
from What4.Interface. Type
is
an instance of the classes ExprBuilder
t stIsExprBuilder
and IsSymExprBuilder
.
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
- sbStateManager :: ExprBuilder t st fs -> IORef (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)
- natSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingNat -> IO (NatExpr t)
- 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
- 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
- ppExprTop :: Expr t tp -> Doc
- 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 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 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
- 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 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
- 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 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
- data SymbolVarBimap t
- data SymbolBinding t
- = VarSymbolBinding !(ExprBoundVar t tp)
- | FnSymbolBinding !(ExprSymFn t (Expr 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
- NatIndexLit :: !Natural -> IndexLit BaseNatType
- 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
:: 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)) |
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.
sbStateManager :: ExprBuilder t st fs -> IORef (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
natSum :: ExprBuilder t st fs -> WeightedSum (Expr t) SemiRingNat -> IO (NatExpr t) Source #
Evaluate a weighted sum of natural number values.
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
instantiates the type family Expr
t
.SymExpr
(ExprBuilder
t st)
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
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 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 #
App
data App (e :: BaseType -> Type) (tp :: BaseType) where Source #
Type
encodes the top-level application of an 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.
Instances
FoldableFC App Source # | |
Defined in What4.Expr.App 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 |
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.
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 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 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 # | |
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
instantiates the type family
ExprBoundVar
t
.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
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.
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 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
instantiates the type family ExprSymFn
t (Expr t)
.SymFn
(ExprBuilder
t st)
ExprSymFn | |
|
Instances
IsExpr e => IsSymFn (ExprSymFn t e) Source # | |
Defined in What4.Expr.App 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.
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 #
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.
VarSymbolBinding !(ExprBoundVar t tp) | Solver |
FnSymbolBinding !(ExprSymFn t (Expr t) args ret) |
Instances
Eq (SymbolBinding t) Source # | |
Defined in What4.Expr.Builder (==) :: SymbolBinding t -> SymbolBinding t -> Bool # (/=) :: SymbolBinding t -> SymbolBinding t -> Bool # | |
Ord (SymbolBinding t) Source # | |
Defined in What4.Expr.Builder 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 testEquality :: FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) # | |
ShowF FloatModeRepr Source # | |
Defined in What4.Expr.Builder 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 | |
KnownRepr FloatModeRepr FloatUninterpreted Source # | |
Defined in What4.Expr.Builder | |
KnownRepr FloatModeRepr FloatIEEE Source # | |
Defined in What4.Expr.Builder |
data FloatModeRepr :: FloatMode -> Type where Source #
FloatIEEERepr :: FloatModeRepr FloatIEEE | |
FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted | |
FloatRealRepr :: FloatModeRepr FloatReal |
Instances
TestEquality FloatModeRepr Source # | |
Defined in What4.Expr.Builder testEquality :: FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) # | |
ShowF FloatModeRepr Source # | |
Defined in What4.Expr.Builder 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 | |
KnownRepr FloatModeRepr FloatUninterpreted Source # | |
Defined in What4.Expr.Builder | |
KnownRepr FloatModeRepr FloatIEEE Source # | |
Defined in What4.Expr.Builder | |
Show (FloatModeRepr fm) Source # | |
Defined in What4.Expr.Builder showsPrec :: Int -> FloatModeRepr fm -> ShowS # show :: FloatModeRepr fm -> String # showList :: [FloatModeRepr fm] -> ShowS # |
type FloatUninterpreted = FloatUninterpreted Source #
data Flags (fi :: FloatMode) Source #