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

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

What4.Expr.App

Description

This module defines datastructures that encode the basic syntax formers used in What4.ExprBuilder.

Synopsis

- data NonceAppExpr t (tp :: BaseType) = NonceAppExprCtor {
  - nonceExprId :: !(Nonce t tp)
  - nonceExprLoc :: !ProgramLoc
  - nonceExprApp :: !(NonceApp t (Expr t) tp)
  - nonceExprAbsValue :: !(AbstractValue tp)
  }
- data AppExpr t (tp :: BaseType) = AppExprCtor {
  - appExprId :: !(Nonce t tp)
  - appExprLoc :: !ProgramLoc
  - appExprApp :: !(App (Expr t) tp)
  - appExprAbsValue :: !(AbstractValue tp)
  }
- 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
- data BVOrNote w = BVOrNote !IncrHash !(BVDomain w)
- newtype BVOrSet e w = BVOrSet (AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ())
- data App (e :: BaseType -> Type) (tp :: BaseType) where
  - BaseIte :: !(BaseTypeRepr tp) -> !Integer -> !(e BaseBoolType) -> !(e tp) -> !(e tp) -> App e tp
  - BaseEq :: !(BaseTypeRepr tp) -> !(e tp) -> !(e tp) -> App e BaseBoolType
  - NotPred :: !(e BaseBoolType) -> App e BaseBoolType
  - ConjPred :: !(BoolMap e) -> App e BaseBoolType
  - SemiRingSum :: !(WeightedSum e sr) -> App e (SemiRingBase sr)
  - SemiRingProd :: !(SemiRingProduct e sr) -> App e (SemiRingBase sr)
  - SemiRingLe :: !(OrderedSemiRingRepr sr) -> !(e (SemiRingBase sr)) -> !(e (SemiRingBase sr)) -> App e BaseBoolType
  - RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType
  - IntDiv :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
  - IntMod :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType
  - IntAbs :: !(e BaseIntegerType) -> App e BaseIntegerType
  - IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType
  - RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
  - RealSqrt :: !(e BaseRealType) -> App e BaseRealType
  - RealSpecialFunction :: !(SpecialFunction args) -> !(SpecialFnArgs e BaseRealType args) -> App e BaseRealType
  - BVTestBit :: 1 <= w => !Natural -> !(e (BaseBVType w)) -> App e BaseBoolType
  - BVSlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
  - BVUlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
  - BVOrBits :: 1 <= w => !(NatRepr w) -> !(BVOrSet e w) -> App e (BaseBVType w)
  - BVUnaryTerm :: 1 <= n => !(UnaryBV (e BaseBoolType) n) -> App e (BaseBVType n)
  - BVConcat :: (1 <= u, 1 <= v, 1 <= (u + v)) => !(NatRepr (u + v)) -> !(e (BaseBVType u)) -> !(e (BaseBVType v)) -> App e (BaseBVType (u + v))
  - BVSelect :: (1 <= n, (idx + n) <= w) => !(NatRepr idx) -> !(NatRepr n) -> !(e (BaseBVType w)) -> App e (BaseBVType n)
  - BVFill :: 1 <= w => !(NatRepr w) -> !(e BaseBoolType) -> App e (BaseBVType w)
  - BVUdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVUrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVSdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVSrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVShl :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVLshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVAshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVRol :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVRor :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVZext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r)
  - BVSext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r)
  - BVPopcount :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVCountTrailingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - BVCountLeadingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w)
  - FloatNeg :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatAbs :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatSqrt :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatAdd :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatSub :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatMul :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatDiv :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatRem :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatFMA :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatFpEq :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatLe :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatLt :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatIsNaN :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatIsInf :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatIsZero :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatIsPos :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatIsNeg :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatIsSubnorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatIsNorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  - FloatCast :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp')) -> App e (BaseFloatType fpp)
  - FloatRound :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp)
  - FloatFromBinary :: (2 <= eb, 2 <= sb) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseBVType (eb + sb))) -> App e (BaseFloatType (FloatingPointPrecision eb sb))
  - FloatToBinary :: (2 <= eb, 2 <= sb, 1 <= (eb + sb)) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseFloatType (FloatingPointPrecision eb sb))) -> App e (BaseBVType (eb + sb))
  - BVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp)
  - SBVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp)
  - RealToFloat :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e BaseRealType) -> App e (BaseFloatType fpp)
  - FloatToBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w)
  - FloatToSBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w)
  - FloatToReal :: !(e (BaseFloatType fpp)) -> App e BaseRealType
  - FloatSpecialFunction :: !(FloatPrecisionRepr fpp) -> !(SpecialFunction args) -> !(SpecialFnArgs e (BaseFloatType fpp) args) -> App e (BaseFloatType fpp)
  - ArrayMap :: !(Assignment BaseTypeRepr (i ::> itp)) -> !(BaseTypeRepr tp) -> !(ArrayUpdateMap e (i ::> itp) tp) -> !(e (BaseArrayType (i ::> itp) tp)) -> App e (BaseArrayType (i ::> itp) tp)
  - ConstantArray :: !(Assignment BaseTypeRepr (i ::> tp)) -> !(BaseTypeRepr b) -> !(e b) -> App e (BaseArrayType (i ::> tp) b)
  - UpdateArray :: !(BaseTypeRepr b) -> !(Assignment BaseTypeRepr (i ::> tp)) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> !(e b) -> App e (BaseArrayType (i ::> tp) b)
  - SelectArray :: !(BaseTypeRepr b) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> App e b
  - CopyArray :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseArrayType (SingleCtx (BaseBVType w)) a)
  - SetArray :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e a) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseArrayType (SingleCtx (BaseBVType w)) a)
  - EqualArrayRange :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType
  - IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType
  - RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType
  - BVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
  - SBVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType
  - IntegerToBV :: 1 <= w => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)
  - RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
  - RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType
  - FloorReal :: !(e BaseRealType) -> App e BaseIntegerType
  - CeilReal :: !(e BaseRealType) -> App e BaseIntegerType
  - Cplx :: !(Complex (e BaseRealType)) -> App e BaseComplexType
  - RealPart :: !(e BaseComplexType) -> App e BaseRealType
  - ImagPart :: !(e BaseComplexType) -> App e BaseRealType
  - StringContains :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
  - StringIsPrefixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
  - StringIsSuffixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType
  - StringIndexOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> !(e BaseIntegerType) -> App e BaseIntegerType
  - StringSubstring :: !(StringInfoRepr si) -> !(e (BaseStringType si)) -> !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e (BaseStringType si)
  - StringAppend :: !(StringInfoRepr si) -> !(StringSeq e si) -> App e (BaseStringType si)
  - StringLength :: !(e (BaseStringType si)) -> App e BaseIntegerType
  - StructCtor :: !(Assignment BaseTypeRepr flds) -> !(Assignment e flds) -> App e (BaseStructType flds)
  - StructField :: !(e (BaseStructType flds)) -> !(Index flds tp) -> !(BaseTypeRepr tp) -> App e tp
- data VarKind
  - = QuantifierVarKind
  - | LatchVarKind
  - | UninterpVarKind
- data ExprBoundVar t (tp :: BaseType) = BVar {
  - bvarId :: !(Nonce t tp)
  - bvarLoc :: !ProgramLoc
  - bvarName :: !SolverSymbol
  - bvarType :: !(BaseTypeRepr tp)
  - bvarKind :: !VarKind
  - bvarAbstractValue :: !(Maybe (AbstractValue tp))
  }
- data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where
  - Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp
  - Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
  - Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType
  - ArrayFromFn :: !(ExprSymFn t (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret)
  - MapOverArrays :: !(ExprSymFn t (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r)
  - ArrayTrueOnEntries :: !(ExprSymFn t (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType
  - FnApp :: !(ExprSymFn t args ret) -> !(Assignment e args) -> NonceApp t e ret
- data 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)
- data ExprSymFn t (args :: Ctx BaseType) (ret :: BaseType) = ExprSymFn {
  - symFnId :: !(Nonce t (args ::> ret))
  - symFnName :: !SolverSymbol
  - symFnInfo :: !(SymFnInfo t args ret)
  - symFnLoc :: !ProgramLoc
  }
- data Dummy (tp :: k)
- 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)
- appEqF :: (Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => App e x -> App e y -> Maybe (x :~: y)
- hashApp :: (OrdF e, HashableF e, HasAbsValue e, Hashable (e BaseBoolType), Hashable (e BaseRealType)) => Int -> App e s -> Int
- isNonLinearApp :: App e tp -> Bool
- traverseArrayResultWrapper :: Functor m => (forall tp. e tp -> m (f tp)) -> ArrayResultWrapper e (idx ::> itp) c -> m (ArrayResultWrapper f (idx ::> itp) c)
- traverseArrayResultWrapperAssignment :: Applicative m => (forall tp. e tp -> m (f tp)) -> Assignment (ArrayResultWrapper e (idx ::> itp)) c -> m (Assignment (ArrayResultWrapper f (idx ::> itp)) c)
- asApp :: Expr t tp -> Maybe (App (Expr t) tp)
- asNonceApp :: Expr t tp -> Maybe (NonceApp t (Expr t) tp)
- exprLoc :: Expr t tp -> ProgramLoc
- mkExpr :: Nonce t tp -> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
- type BoolExpr t = Expr t BaseBoolType
- type FloatExpr t fpp = Expr t (BaseFloatType fpp)
- type BVExpr t n = Expr t (BaseBVType n)
- type IntegerExpr t = Expr t BaseIntegerType
- type RealExpr t = Expr t BaseRealType
- type CplxExpr t = Expr t BaseComplexType
- type StringExpr t si = Expr t (BaseStringType si)
- iteSize :: Expr t tp -> Integer
- asSemiRingLit :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
- asSemiRingSum :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
- asSemiRingProd :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> Maybe (SemiRingProduct (Expr t) sr)
- data SemiRingView t sr
  - = SR_Constant !(Coefficient sr)
  - | SR_Sum !(WeightedSum (Expr t) sr)
  - | SR_Prod !(SemiRingProduct (Expr t) sr)
  - | SR_General
- viewSemiRing :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
- asWeightedSum :: HashableF (Expr t) => SemiRingRepr sr -> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
- asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
- asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
- asPosAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
- asNegAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
- exprAbsValue :: Expr t tp -> AbstractValue tp
- compareExpr :: Expr t x -> Expr t y -> OrderingF x y
- sameTerm :: Expr t a -> Expr t b -> Maybe (a :~: b)
- data PPIndex
  - = ExprPPIndex !Word64
  - | RatPPIndex !Rational
- countOccurrences :: Expr t tp -> Map PPIndex Int
- type OccurrenceTable s = HashTable s PPIndex Int
- incOccurrence :: OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
- countOccurrences' :: forall t tp s. OccurrenceTable s -> Expr t tp -> ST s ()
- type BoundVarMap s t = HashTable s PPIndex (Set (Some (ExprBoundVar t)))
- cache :: (Eq k, Hashable k) => HashTable s k r -> k -> ST s r -> ST s r
- boundVars :: Expr t tp -> ST s (BoundVarMap s t)
- boundVars' :: BoundVarMap s t -> Expr t tp -> ST s (Set (Some (ExprBoundVar t)))
- data AppPPExpr ann = APE {
  - apeIndex :: !PPIndex
  - apeLoc :: !ProgramLoc
  - apeName :: !Text
  - apeExprs :: ![PPExpr ann]
  - apeLength :: !Int
  }
- data PPExpr ann
  - = FixedPPExpr !(Doc ann) ![Doc ann] !Int
  - | AppPPExpr !(AppPPExpr ann)
- apeDoc :: AppPPExpr ann -> (Doc ann, [Doc ann])
- textPPExpr :: Text -> PPExpr ann
- stringPPExpr :: String -> PPExpr ann
- ppExprLength :: PPExpr ann -> Int
- parenIf :: Bool -> Doc ann -> [Doc ann] -> Doc ann
- ppExprDoc :: Bool -> PPExpr ann -> Doc ann
- data PPExprOpts = PPExprOpts {
  - ppExpr_maxWidth :: Int
  - ppExpr_useDecimal :: Bool
  }
- defaultPPExprOpts :: PPExprOpts
- ppExpr :: Expr t tp -> Doc ann
- ppExprTop :: Expr t tp -> Doc ann
- type SplitPPExprList ann = Maybe ([PPExpr ann], AppPPExpr ann, [PPExpr ann])
- findExprToRemove :: [PPExpr ann] -> SplitPPExprList ann
- ppExpr' :: forall t tp s ann. Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann)
- symFnArgTypes :: ExprSymFn t args ret -> Assignment BaseTypeRepr args
- symFnReturnType :: ExprSymFn t args ret -> BaseTypeRepr ret
- asMatlabSolverFn :: ExprSymFn t args ret -> Maybe (MatlabSolverFn (Expr t) args ret)
- testExprSymFnEq :: ExprSymFn t a1 r1 -> ExprSymFn t a2 r2 -> Maybe ((a1 ::> r1) :~: (a2 ::> r2))
- traverseBVOrSet :: (HashableF f, HasAbsValue f, OrdF f, Applicative m) => (forall tp. e tp -> m (f tp)) -> BVOrSet e w -> m (BVOrSet f w)
- bvOrInsert :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w
- bvOrSingleton :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w
- bvOrContains :: OrdF e => e (BaseBVType w) -> BVOrSet e w -> Bool
- bvOrUnion :: OrdF e => BVOrSet e w -> BVOrSet e w -> BVOrSet e w
- bvOrToList :: BVOrSet e w -> [e (BaseBVType w)]
- bvOrAbs :: (OrdF e, 1 <= w) => NatRepr w -> BVOrSet e w -> BVDomain w
- nonceAppType :: IsExpr e => NonceApp t e tp -> BaseTypeRepr tp
- appType :: App e tp -> BaseTypeRepr tp
- unconstrainedAbsValue :: BaseTypeRepr tp -> AbstractValue tp
- quantAbsEval :: IsExpr e => (forall u. e u -> AbstractValue u) -> NonceApp t e tp -> AbstractValue tp
- abstractEval :: (IsExpr e, HashableF e, OrdF e) => (forall u. e u -> AbstractValue u) -> App e tp -> AbstractValue tp
- reduceApp :: IsExprBuilder sym => sym -> (forall w. 1 <= w => sym -> UnaryBV (Pred sym) w -> IO (SymExpr sym (BaseBVType w))) -> App (SymExpr sym) tp -> IO (SymExpr sym tp)
- ppVar :: String -> SolverSymbol -> Nonce t tp -> BaseTypeRepr tp -> String
- ppBoundVar :: ExprBoundVar t tp -> String
- ppVarTypeCode :: BaseTypeRepr tp -> String
- data PrettyArg (e :: BaseType -> Type) where
  - PrettyArg :: e tp -> PrettyArg e
  - PrettyText :: Text -> PrettyArg e
  - PrettyFunc :: Text -> [PrettyArg e] -> PrettyArg e
- exprPrettyArg :: e tp -> PrettyArg e
- exprPrettyIndices :: Assignment e ctx -> [PrettyArg e]
- stringPrettyArg :: String -> PrettyArg e
- showPrettyArg :: Show a => a -> PrettyArg e
- type PrettyApp e = (Text, [PrettyArg e])
- prettyApp :: Text -> [PrettyArg e] -> PrettyApp e
- ppNonceApp :: forall m t e tp. Applicative m => (forall ctx r. ExprSymFn t ctx r -> m (PrettyArg e)) -> NonceApp t e tp -> m (PrettyApp e)
- ppApp' :: forall e u. App e u -> PrettyApp e

# Documentation

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`.

Constructors

NonceAppExprCtor |

Fields

- nonceExprId :: !(Nonce t tp)
- nonceExprLoc :: !ProgramLoc
- nonceExprApp :: !(NonceApp t (Expr t) tp)
- nonceExprAbsValue :: !(AbstractValue tp)

#### Instances

Instances details

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

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

data AppExpr t (tp :: BaseType) Source #

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

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

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

Constructors

AppExprCtor |

Fields

- appExprId :: !(Nonce t tp)
- appExprLoc :: !ProgramLoc
- appExprApp :: !(App (Expr t) tp)
- appExprAbsValue :: !(AbstractValue tp)

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

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

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

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

Constructors

SemiRingLiteral :: !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr) |
BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType |
FloatExpr :: !(FloatPrecisionRepr fpp) -> !BigFloat -> !ProgramLoc -> Expr t (BaseFloatType fpp) |
StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si) |
AppExpr :: !(AppExpr t tp) -> Expr t tp |
NonceAppExpr :: !(NonceAppExpr t tp) -> Expr t tp |
BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp |

#### Instances

Instances details

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

data BVOrNote w Source #

Constructors

BVOrNote !IncrHash !(BVDomain w) |

#### Instances

Instances details

Semigroup (BVOrNote w) Source # |
Instance details Defined in What4.Expr.App Methods (<>) :: BVOrNote w -> BVOrNote w -> BVOrNote w Source # sconcat :: NonEmpty (BVOrNote w) -> BVOrNote w Source # stimes :: Integral b => b -> BVOrNote w -> BVOrNote w Source #

newtype BVOrSet e w Source #

Constructors

BVOrSet (AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()) |

#### Instances

Instances details

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

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

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

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

Constructors

BaseIte :: !(BaseTypeRepr tp) -> !Integer -> !(e BaseBoolType) -> !(e tp) -> !(e tp) -> App e tp |
BaseEq :: !(BaseTypeRepr tp) -> !(e tp) -> !(e tp) -> App e BaseBoolType |
NotPred :: !(e BaseBoolType) -> App e BaseBoolType |
ConjPred :: !(BoolMap e) -> App e BaseBoolType |
SemiRingSum :: !(WeightedSum e sr) -> App e (SemiRingBase sr) |
SemiRingProd :: !(SemiRingProduct e sr) -> App e (SemiRingBase sr) |
SemiRingLe :: !(OrderedSemiRingRepr sr) -> !(e (SemiRingBase sr)) -> !(e (SemiRingBase sr)) -> App e BaseBoolType |
RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType |
IntDiv :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType |
IntMod :: !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e BaseIntegerType |
IntAbs :: !(e BaseIntegerType) -> App e BaseIntegerType |
IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType |
RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType |
RealSqrt :: !(e BaseRealType) -> App e BaseRealType |
RealSpecialFunction :: !(SpecialFunction args) -> !(SpecialFnArgs e BaseRealType args) -> App e BaseRealType |
BVTestBit :: 1 <= w => !Natural -> !(e (BaseBVType w)) -> App e BaseBoolType |
BVSlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType |
BVUlt :: 1 <= w => !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType |
BVOrBits :: 1 <= w => !(NatRepr w) -> !(BVOrSet e w) -> App e (BaseBVType w) |
BVUnaryTerm :: 1 <= n => !(UnaryBV (e BaseBoolType) n) -> App e (BaseBVType n) |
BVConcat :: (1 <= u, 1 <= v, 1 <= (u + v)) => !(NatRepr (u + v)) -> !(e (BaseBVType u)) -> !(e (BaseBVType v)) -> App e (BaseBVType (u + v)) |
BVSelect :: (1 <= n, (idx + n) <= w) => !(NatRepr idx) -> !(NatRepr n) -> !(e (BaseBVType w)) -> App e (BaseBVType n) |
BVFill :: 1 <= w => !(NatRepr w) -> !(e BaseBoolType) -> App e (BaseBVType w) |
BVUdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVUrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVSdiv :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVSrem :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVShl :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVLshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVAshr :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVRol :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVRor :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVZext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r) |
BVSext :: (1 <= w, (w + 1) <= r, 1 <= r) => !(NatRepr r) -> !(e (BaseBVType w)) -> App e (BaseBVType r) |
BVPopcount :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVCountTrailingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
BVCountLeadingZeros :: 1 <= w => !(NatRepr w) -> !(e (BaseBVType w)) -> App e (BaseBVType w) |
FloatNeg :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatAbs :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatSqrt :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatAdd :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatSub :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatMul :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatDiv :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatRem :: !(FloatPrecisionRepr fpp) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatFMA :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatFpEq :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatLe :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatLt :: !(e (BaseFloatType fpp)) -> !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatIsNaN :: !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatIsInf :: !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatIsZero :: !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatIsPos :: !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatIsNeg :: !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatIsSubnorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatIsNorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType |
FloatCast :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp')) -> App e (BaseFloatType fpp) |
FloatRound :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseFloatType fpp) |
FloatFromBinary :: (2 <= eb, 2 <= sb) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseBVType (eb + sb))) -> App e (BaseFloatType (FloatingPointPrecision eb sb)) |
FloatToBinary :: (2 <= eb, 2 <= sb, 1 <= (eb + sb)) => !(FloatPrecisionRepr (FloatingPointPrecision eb sb)) -> !(e (BaseFloatType (FloatingPointPrecision eb sb))) -> App e (BaseBVType (eb + sb)) |
BVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp) |
SBVToFloat :: 1 <= w => !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e (BaseBVType w)) -> App e (BaseFloatType fpp) |
RealToFloat :: !(FloatPrecisionRepr fpp) -> !RoundingMode -> !(e BaseRealType) -> App e (BaseFloatType fpp) |
FloatToBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w) |
FloatToSBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(e (BaseFloatType fpp)) -> App e (BaseBVType w) |
FloatToReal :: !(e (BaseFloatType fpp)) -> App e BaseRealType |
FloatSpecialFunction :: !(FloatPrecisionRepr fpp) -> !(SpecialFunction args) -> !(SpecialFnArgs e (BaseFloatType fpp) args) -> App e (BaseFloatType fpp) |
ArrayMap :: !(Assignment BaseTypeRepr (i ::> itp)) -> !(BaseTypeRepr tp) -> !(ArrayUpdateMap e (i ::> itp) tp) -> !(e (BaseArrayType (i ::> itp) tp)) -> App e (BaseArrayType (i ::> itp) tp) |
ConstantArray :: !(Assignment BaseTypeRepr (i ::> tp)) -> !(BaseTypeRepr b) -> !(e b) -> App e (BaseArrayType (i ::> tp) b) |
UpdateArray :: !(BaseTypeRepr b) -> !(Assignment BaseTypeRepr (i ::> tp)) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> !(e b) -> App e (BaseArrayType (i ::> tp) b) |
SelectArray :: !(BaseTypeRepr b) -> !(e (BaseArrayType (i ::> tp) b)) -> !(Assignment e (i ::> tp)) -> App e b |
CopyArray :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseArrayType (SingleCtx (BaseBVType w)) a) |
SetArray :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e a) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e (BaseArrayType (SingleCtx (BaseBVType w)) a) |
EqualArrayRange :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr a) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseArrayType (SingleCtx (BaseBVType w)) a)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> !(e (BaseBVType w)) -> App e BaseBoolType |
IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType |
RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType |
BVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType |
SBVToInteger :: 1 <= w => !(e (BaseBVType w)) -> App e BaseIntegerType |
IntegerToBV :: 1 <= w => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w) |
RoundReal :: !(e BaseRealType) -> App e BaseIntegerType |
RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType |
FloorReal :: !(e BaseRealType) -> App e BaseIntegerType |
CeilReal :: !(e BaseRealType) -> App e BaseIntegerType |
Cplx :: !(Complex (e BaseRealType)) -> App e BaseComplexType |
RealPart :: !(e BaseComplexType) -> App e BaseRealType |
ImagPart :: !(e BaseComplexType) -> App e BaseRealType |
StringContains :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType |
StringIsPrefixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType |
StringIsSuffixOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> App e BaseBoolType |
StringIndexOf :: !(e (BaseStringType si)) -> !(e (BaseStringType si)) -> !(e BaseIntegerType) -> App e BaseIntegerType |
StringSubstring :: !(StringInfoRepr si) -> !(e (BaseStringType si)) -> !(e BaseIntegerType) -> !(e BaseIntegerType) -> App e (BaseStringType si) |
StringAppend :: !(StringInfoRepr si) -> !(StringSeq e si) -> App e (BaseStringType si) |
StringLength :: !(e (BaseStringType si)) -> App e BaseIntegerType |
StructCtor :: !(Assignment BaseTypeRepr flds) -> !(Assignment e flds) -> App e (BaseStructType flds) |
StructField :: !(e (BaseStructType flds)) -> !(Index flds tp) -> !(BaseTypeRepr tp) -> App e tp |

#### Instances

Instances details

FoldableFC App Source # |

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

(Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => TestEquality (App e :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods testEquality :: forall (a :: k) (b :: k). App e a -> App e b -> Maybe (a :~: b) Source #
(OrdF e, HashableF e, HasAbsValue e, Hashable (e BaseBoolType), Hashable (e BaseRealType)) => HashableF (App e :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods hashWithSaltF :: forall (tp :: k). Int -> App e tp -> Int Source # hashF :: forall (tp :: k). App e tp -> Int Source #
ShowF e => Show (App e u) Source # |
Instance details Defined in What4.Expr.App Methods showsPrec :: Int -> App e u -> ShowS Source # show :: App e u -> String Source # showList :: [App e u] -> ShowS Source #
(Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => Eq (App e tp) Source # |
Instance details Defined in What4.Expr.App Methods (==) :: App e tp -> App e tp -> Bool Source # (/=) :: App e tp -> App e tp -> Bool Source #
ShowF e => Pretty (App e u) Source # |
Instance details Defined in What4.Expr.App Methods pretty :: App e u -> Doc ann Source # prettyList :: [App e u] -> Doc ann Source #

data VarKind Source #

The Kind of a bound variable.

Constructors

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

data ExprBoundVar t (tp :: BaseType) Source #

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

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

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

Constructors

BVar |

Fields

- bvarId :: !(Nonce t tp)
- bvarLoc :: !ProgramLoc
- bvarName :: !SolverSymbol
- bvarType :: !(BaseTypeRepr tp)
- bvarKind :: !VarKind
- bvarAbstractValue :: !(Maybe (AbstractValue tp))

#### Instances

Instances details

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

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

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

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

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

Parameter `t` is a phantom type brand used to track nonces. Parameter `e` is used everywhere a recursive sub-expression would go. Uses of the `NonceApp` type will tie the knot through this parameter. Parameter `tp` indicates the type of the expression.

Constructors

Annotation :: !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp |
Forall :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType |
Exists :: !(ExprBoundVar t tp) -> !(e BaseBoolType) -> NonceApp t e BaseBoolType |
ArrayFromFn :: !(ExprSymFn t (idx ::> itp) ret) -> NonceApp t e (BaseArrayType (idx ::> itp) ret) |
MapOverArrays :: !(ExprSymFn t (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e (BaseArrayType (idx ::> itp) r) |
ArrayTrueOnEntries :: !(ExprSymFn t (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e BaseBoolType |
FnApp :: !(ExprSymFn t args ret) -> !(Assignment e args) -> NonceApp t e ret |

#### Instances

Instances details

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

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

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

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.

data ExprSymFn t (args :: Ctx BaseType) (ret :: BaseType) Source #

This represents a symbolic function in the simulator. Parameter `t` is a phantom type brand used to track nonces. The `args` and `ret` parameters define the types of arguments and the return type of the function.

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

Constructors

ExprSymFn |

Fields

- symFnId :: !(Nonce t (args ::> ret))
- symFnName :: !SolverSymbol
- symFnInfo :: !(SymFnInfo t args ret)
- symFnLoc :: !ProgramLoc

#### Instances

Instances details

IsSymFn (ExprSymFn t) Source # |

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

data Dummy (tp :: k) Source #

Used to implement foldMapFc from traversal.

#### Instances

Instances details

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

Instance details

Defined in What4.Expr.App

Methods

compareF :: forall (x :: k0) (y :: k0). Dummy x -> Dummy y -> OrderingF x y Source #

leqF :: forall (x :: k0) (y :: k0). Dummy x -> Dummy y -> Bool Source #

ltF :: forall (x :: k0) (y :: k0). Dummy x -> Dummy y -> Bool Source #

geqF :: forall (x :: k0) (y :: k0). Dummy x -> Dummy y -> Bool Source #

gtF :: forall (x :: k0) (y :: k0). Dummy x -> Dummy y -> Bool Source #

HasAbsValue (Dummy :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp Source #
Eq (Dummy tp) Source # |
Instance details Defined in What4.Expr.App Methods (==) :: Dummy tp -> Dummy tp -> Bool Source # (/=) :: Dummy tp -> Dummy tp -> Bool Source #
Ord (Dummy tp) Source # |
Instance details Defined in What4.Expr.App Methods compare :: Dummy tp -> Dummy tp -> Ordering Source # (<) :: Dummy tp -> Dummy tp -> Bool Source # (<=) :: Dummy tp -> Dummy tp -> Bool Source # (>) :: Dummy tp -> Dummy tp -> Bool Source # (>=) :: Dummy tp -> Dummy tp -> Bool Source # max :: Dummy tp -> Dummy tp -> Dummy tp Source # min :: Dummy tp -> Dummy tp -> Dummy tp Source #

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

appEqF :: (Eq (e BaseBoolType), Eq (e BaseRealType), HashableF e, HasAbsValue e, OrdF e) => App e x -> App e y -> Maybe (x :~: y) Source #

Check if two applications are equal.

hashApp :: (OrdF e, HashableF e, HasAbsValue e, Hashable (e BaseBoolType), Hashable (e BaseRealType)) => Int -> App e s -> Int Source #

Hash an an application.

isNonLinearApp :: App e tp -> Bool Source #

Return `true` if an app represents a non-linear operation. Controls whether the non-linear counter ticks upward in the `Statistics`.

traverseArrayResultWrapper :: Functor m => (forall tp. e tp -> m (f tp)) -> ArrayResultWrapper e (idx ::> itp) c -> m (ArrayResultWrapper f (idx ::> itp) c) Source #

traverseArrayResultWrapperAssignment :: Applicative m => (forall tp. e tp -> m (f tp)) -> Assignment (ArrayResultWrapper e (idx ::> itp)) c -> m (Assignment (ArrayResultWrapper f (idx ::> itp)) c) Source #

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

Destructor for the `AppExpr` constructor.

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

Destructor for the `NonceAppExpr` constructor.

exprLoc :: Expr t tp -> ProgramLoc Source #

mkExpr :: Nonce t tp -> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp Source #

type BoolExpr t = Expr t BaseBoolType Source #

type FloatExpr t fpp = Expr t (BaseFloatType fpp) Source #

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

type IntegerExpr t = Expr t BaseIntegerType Source #

type RealExpr t = Expr t BaseRealType Source #

type CplxExpr t = Expr t BaseComplexType Source #

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

iteSize :: Expr t tp -> Integer Source #

asSemiRingLit :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr) Source #

asSemiRingSum :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr) Source #

asSemiRingProd :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> Maybe (SemiRingProduct (Expr t) sr) Source #

data SemiRingView t sr Source #

This privides a view of a semiring expr as a weighted sum of values.

Constructors

SR_Constant !(Coefficient sr) |
SR_Sum !(WeightedSum (Expr t) sr) |
SR_Prod !(SemiRingProduct (Expr t) sr) |
SR_General |

viewSemiRing :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr Source #

asWeightedSum :: HashableF (Expr t) => SemiRingRepr sr -> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr Source #

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

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

asPosAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity) Source #

asNegAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity) Source #

exprAbsValue :: Expr t tp -> AbstractValue tp Source #

Get abstract value associated with element.

compareExpr :: Expr t x -> Expr t y -> OrderingF x y Source #

sameTerm :: Expr t a -> Expr t b -> Maybe (a :~: b) Source #

A slightly more aggressive syntactic equality check than testEquality, `sameTerm` will recurse through a small collection of known syntax formers.

data PPIndex Source #

Constructors

ExprPPIndex !Word64 |
RatPPIndex !Rational |

#### Instances

Instances details

Generic PPIndex Source # |
Instance details Defined in What4.Expr.App Associated Types type Rep PPIndex :: Type -> Type Source # Methods from :: PPIndex -> Rep PPIndex x Source # to :: Rep PPIndex x -> PPIndex Source #
Eq PPIndex Source # |
Instance details Defined in What4.Expr.App Methods (==) :: PPIndex -> PPIndex -> Bool Source # (/=) :: PPIndex -> PPIndex -> Bool Source #
Ord PPIndex Source # |
Instance details Defined in What4.Expr.App Methods compare :: PPIndex -> PPIndex -> Ordering Source # (<) :: PPIndex -> PPIndex -> Bool Source # (<=) :: PPIndex -> PPIndex -> Bool Source # (>) :: PPIndex -> PPIndex -> Bool Source # (>=) :: PPIndex -> PPIndex -> Bool Source # max :: PPIndex -> PPIndex -> PPIndex Source # min :: PPIndex -> PPIndex -> PPIndex Source #
Hashable PPIndex Source # |
Instance details Defined in What4.Expr.App Methods hashWithSalt :: Int -> PPIndex -> Int Source # hash :: PPIndex -> Int Source #
type Rep PPIndex Source # |

Instance details

Defined in What4.Expr.App

type Rep PPIndex = D1 ('MetaData "PPIndex" "What4.Expr.App" "what4-1.5.1-96RHnAoFm39CNNNDj0F3kd" 'False) (C1 ('MetaCons "ExprPPIndex" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64)) :+: C1 ('MetaCons "RatPPIndex" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Rational)))

countOccurrences :: Expr t tp -> Map PPIndex Int Source #

type OccurrenceTable s = HashTable s PPIndex Int Source #

incOccurrence :: OccurrenceTable s -> PPIndex -> ST s () -> ST s () Source #

countOccurrences' :: forall t tp s. OccurrenceTable s -> Expr t tp -> ST s () Source #

type BoundVarMap s t = HashTable s PPIndex (Set (Some (ExprBoundVar t))) Source #

cache :: (Eq k, Hashable k) => HashTable s k r -> k -> ST s r -> ST s r Source #

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

boundVars' :: BoundVarMap s t -> Expr t tp -> ST s (Set (Some (ExprBoundVar t))) Source #

data AppPPExpr ann Source #

`AppPPExpr` represents a an application, and it may be let bound.

Constructors

APE |

Fields

- apeIndex :: !PPIndex
- apeLoc :: !ProgramLoc
- apeName :: !Text
- apeExprs :: ![PPExpr ann]
- apeLength :: !Int

  Length of AppPPExpr not including parenthesis.

data PPExpr ann Source #

Constructors

FixedPPExpr !(Doc ann) ![Doc ann] !Int | A fixed doc with length.
AppPPExpr !(AppPPExpr ann) | A doc that can be let bound.

apeDoc :: AppPPExpr ann -> (Doc ann, [Doc ann]) Source #

Pretty print a AppPPExpr

textPPExpr :: Text -> PPExpr ann Source #

stringPPExpr :: String -> PPExpr ann Source #

ppExprLength :: PPExpr ann -> Int Source #

Get length of Expr including parens.

parenIf :: Bool -> Doc ann -> [Doc ann] -> Doc ann Source #

ppExprDoc :: Bool -> PPExpr ann -> Doc ann Source #

Pretty print PPExpr

data PPExprOpts Source #

Constructors

PPExprOpts |

Fields

- ppExpr_maxWidth :: Int
- ppExpr_useDecimal :: Bool

defaultPPExprOpts :: PPExprOpts Source #

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

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

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

Pretty print the top part of an element.

type SplitPPExprList ann = Maybe ([PPExpr ann], AppPPExpr ann, [PPExpr ann]) Source #

Contains the elements before, the index, doc, and width and the elements after.

findExprToRemove :: [PPExpr ann] -> SplitPPExprList ann Source #

ppExpr' :: forall t tp s ann. Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann) Source #

symFnArgTypes :: ExprSymFn t args ret -> Assignment BaseTypeRepr args Source #

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

asMatlabSolverFn :: ExprSymFn t args ret -> Maybe (MatlabSolverFn (Expr t) args ret) Source #

Return solver function associated with ExprSymFn if any.

testExprSymFnEq :: ExprSymFn t a1 r1 -> ExprSymFn t a2 r2 -> Maybe ((a1 ::> r1) :~: (a2 ::> r2)) 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 #

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

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

bvOrContains :: OrdF e => e (BaseBVType w) -> BVOrSet e w -> Bool Source #

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

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

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

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

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

unconstrainedAbsValue :: BaseTypeRepr tp -> AbstractValue tp Source #

Return an unconstrained abstract value.

quantAbsEval :: IsExpr e => (forall u. e u -> AbstractValue u) -> NonceApp t e tp -> AbstractValue tp Source #

Return abstract domain associated with a nonce app

abstractEval :: (IsExpr e, HashableF e, OrdF e) => (forall u. e u -> AbstractValue u) -> App e tp -> AbstractValue tp Source #

reduceApp :: IsExprBuilder sym => sym -> (forall w. 1 <= w => sym -> UnaryBV (Pred sym) w -> IO (SymExpr sym (BaseBVType w))) -> App (SymExpr sym) tp -> IO (SymExpr sym tp) Source #

ppVar :: String -> SolverSymbol -> Nonce t tp -> BaseTypeRepr tp -> String Source #

ppBoundVar :: ExprBoundVar t tp -> String Source #

ppVarTypeCode :: BaseTypeRepr tp -> String Source #

Pretty print a code to identify the type of constant.

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

Either a argument or text or text

Constructors

PrettyArg :: e tp -> PrettyArg e |
PrettyText :: Text -> PrettyArg e |
PrettyFunc :: Text -> [PrettyArg e] -> PrettyArg e |

exprPrettyArg :: e tp -> PrettyArg e Source #

exprPrettyIndices :: Assignment e ctx -> [PrettyArg e] Source #

stringPrettyArg :: String -> PrettyArg e Source #

showPrettyArg :: Show a => a -> PrettyArg e Source #

type PrettyApp e = (Text, [PrettyArg e]) Source #

prettyApp :: Text -> [PrettyArg e] -> PrettyApp e Source #

ppNonceApp :: forall m t e tp. Applicative m => (forall ctx r. ExprSymFn t ctx r -> m (PrettyArg e)) -> NonceApp t e tp -> m (PrettyApp e) Source #

ppApp' :: forall e u. App e u -> PrettyApp e Source #