what4-1.7.1.0: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2020
LicenseBSD3
Maintainerjhendrix@galois.com
Safe HaskellNone
LanguageHaskell2010

What4.Expr.App

Description

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

Synopsis

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

Instances

Instances details
TestEquality (NonceAppExpr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: forall (a :: BaseType) (b :: BaseType). NonceAppExpr t a -> NonceAppExpr t b -> Maybe (a :~: b) #

OrdF (NonceAppExpr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

Eq (NonceAppExpr t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

Ord (NonceAppExpr t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

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

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

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 :: forall (sr :: SemiRing) t. !(SemiRingRepr sr) -> !(Coefficient sr) -> !ProgramLoc -> Expr t (SemiRingBase sr) 
BoolExpr :: forall t. !Bool -> !ProgramLoc -> Expr t 'BaseBoolType 
FloatExpr :: forall (fpp :: FloatPrecision) t. !(FloatPrecisionRepr fpp) -> !BigFloat -> !ProgramLoc -> Expr t ('BaseFloatType fpp) 
StringExpr :: forall (si :: StringInfo) t. !(StringLiteral si) -> !ProgramLoc -> Expr t ('BaseStringType si) 
AppExpr :: forall t (tp :: BaseType). !(AppExpr t tp) -> Expr t tp 
NonceAppExpr :: forall t (tp :: BaseType). !(NonceAppExpr t tp) -> Expr t tp 
BoundVarExpr :: forall t (tp :: BaseType). !(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 :: BaseType) (b :: BaseType). Expr t a -> Expr t b -> Maybe (a :~: b) #

HashableF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> Expr t tp -> Int #

hashF :: forall (tp :: BaseType). Expr t tp -> Int #

OrdF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

ShowF (Expr t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

withShow :: forall p q (tp :: BaseType) a. p (Expr t) -> q tp -> (Show (Expr t tp) => a) -> a #

showF :: forall (tp :: BaseType). Expr t tp -> String #

showsPrecF :: forall (tp :: BaseType). Int -> Expr t tp -> String -> String #

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 #

show :: Expr t tp -> String #

showList :: [Expr t tp] -> ShowS #

Eq (Expr t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

(==) :: Expr t tp -> Expr t tp -> Bool #

(/=) :: Expr t tp -> Expr t tp -> Bool #

Ord (Expr t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

compare :: Expr t tp -> Expr t tp -> Ordering #

(<) :: Expr t tp -> Expr t tp -> Bool #

(<=) :: Expr t tp -> Expr t tp -> Bool #

(>) :: Expr t tp -> Expr t tp -> Bool #

(>=) :: Expr t tp -> Expr t tp -> Bool #

max :: Expr t tp -> Expr t tp -> Expr t tp #

min :: Expr t tp -> Expr t tp -> Expr t tp #

Hashable (Expr t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSalt :: Int -> Expr t tp -> Int #

hash :: Expr t tp -> Int #

Pretty (Expr t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

pretty :: Expr t tp -> Doc ann #

prettyList :: [Expr t tp] -> Doc ann #

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

polyEq :: Expr t x -> Expr t y -> Bool #

data BVOrNote (w :: Nat) 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 #

sconcat :: NonEmpty (BVOrNote w) -> BVOrNote w #

stimes :: Integral b => b -> BVOrNote w -> BVOrNote w #

newtype BVOrSet (e :: BaseType -> Type) (w :: Nat) 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 #

(/=) :: BVOrSet e w -> BVOrSet e w -> Bool #

OrdF e => Hashable (BVOrSet e w) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSalt :: Int -> BVOrSet e w -> Int #

hash :: BVOrSet e w -> Int #

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

foldrFC :: (forall (x :: BaseType). f x -> b -> b) -> forall (x :: BaseType). b -> App f x -> b #

foldlFC :: forall f b. (forall (x :: BaseType). b -> f x -> b) -> forall (x :: BaseType). b -> App f x -> b #

foldrFC' :: (forall (x :: BaseType). f x -> b -> b) -> forall (x :: BaseType). b -> App f x -> b #

foldlFC' :: forall f b. (forall (x :: BaseType). b -> f x -> b) -> forall (x :: BaseType). b -> App f x -> b #

toListFC :: (forall (x :: BaseType). f x -> a) -> forall (x :: BaseType). App f x -> [a] #

(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 :: BaseType) (b :: BaseType). App e a -> App e b -> Maybe (a :~: b) #

(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 :: BaseType). Int -> App e tp -> Int #

hashF :: forall (tp :: BaseType). App e tp -> Int #

ShowF e => Show (App e u) Source # 
Instance details

Defined in What4.Expr.App

Methods

showsPrec :: Int -> App e u -> ShowS #

show :: App e u -> String #

showList :: [App e u] -> ShowS #

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

(/=) :: App e tp -> App e tp -> Bool #

ShowF e => Pretty (App e u) Source # 
Instance details

Defined in What4.Expr.App

Methods

pretty :: App e u -> Doc ann #

prettyList :: [App e u] -> Doc ann #

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

Instances

Instances details
TestEquality (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: forall (a :: BaseType) (b :: BaseType). ExprBoundVar t a -> ExprBoundVar t b -> Maybe (a :~: b) #

HashableF (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> ExprBoundVar t tp -> Int #

hashF :: forall (tp :: BaseType). ExprBoundVar t tp -> Int #

OrdF (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

ShowF (ExprBoundVar t :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

withShow :: forall p q (tp :: BaseType) a. p (ExprBoundVar t) -> q tp -> (Show (ExprBoundVar t tp) => a) -> a #

showF :: forall (tp :: BaseType). ExprBoundVar t tp -> String #

showsPrecF :: forall (tp :: BaseType). Int -> ExprBoundVar t tp -> String -> String #

Show (ExprBoundVar t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

showsPrec :: Int -> ExprBoundVar t tp -> ShowS #

show :: ExprBoundVar t tp -> String #

showList :: [ExprBoundVar t tp] -> ShowS #

Eq (ExprBoundVar t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

Ord (ExprBoundVar t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

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

Hashable (ExprBoundVar t tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSalt :: Int -> ExprBoundVar t tp -> Int #

hash :: ExprBoundVar t tp -> Int #

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 :: forall (tp :: BaseType) t (e :: BaseType -> Type). !(BaseTypeRepr tp) -> !(Nonce t tp) -> !(e tp) -> NonceApp t e tp 
Forall :: forall t (tp1 :: BaseType) (e :: BaseType -> Type). !(ExprBoundVar t tp1) -> !(e BaseBoolType) -> NonceApp t e 'BaseBoolType 
Exists :: forall t (tp1 :: BaseType) (e :: BaseType -> Type). !(ExprBoundVar t tp1) -> !(e BaseBoolType) -> NonceApp t e 'BaseBoolType 
ArrayFromFn :: forall t (idx :: Ctx BaseType) (itp :: BaseType) (ret :: BaseType) (e :: BaseType -> Type). !(ExprSymFn t (idx ::> itp) ret) -> NonceApp t e ('BaseArrayType (idx ::> itp) ret) 
MapOverArrays :: forall t (ctx :: Ctx BaseType) (d :: BaseType) (r :: BaseType) (idx :: Ctx BaseType) (itp :: BaseType) (e :: BaseType -> Type). !(ExprSymFn t (ctx ::> d) r) -> !(Assignment BaseTypeRepr (idx ::> itp)) -> !(Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)) -> NonceApp t e ('BaseArrayType (idx ::> itp) r) 
ArrayTrueOnEntries :: forall t (idx :: Ctx BaseType) (itp :: BaseType) (e :: BaseType -> Type). !(ExprSymFn t (idx ::> itp) BaseBoolType) -> !(e (BaseArrayType (idx ::> itp) BaseBoolType)) -> NonceApp t e 'BaseBoolType 
FnApp :: forall t (args :: Ctx BaseType) (tp :: BaseType) (e :: BaseType -> Type). !(ExprSymFn t args tp) -> !(Assignment e args) -> NonceApp t e tp 

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 :: BaseType). f x -> m) -> forall (x :: BaseType). NonceApp t f x -> m #

foldrFC :: (forall (x :: BaseType). f x -> b -> b) -> forall (x :: BaseType). b -> NonceApp t f x -> b #

foldlFC :: forall f b. (forall (x :: BaseType). b -> f x -> b) -> forall (x :: BaseType). b -> NonceApp t f x -> b #

foldrFC' :: (forall (x :: BaseType). f x -> b -> b) -> forall (x :: BaseType). b -> NonceApp t f x -> b #

foldlFC' :: forall f b. (forall (x :: BaseType). b -> f x -> b) -> forall (x :: BaseType). b -> NonceApp t f x -> b #

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

FunctorFC (NonceApp t :: (BaseType -> Type) -> BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

fmapFC :: (forall (x :: BaseType). f x -> g x) -> forall (x :: BaseType). NonceApp t f x -> NonceApp t g x #

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 :: BaseType). f x -> m (g x)) -> forall (x :: BaseType). NonceApp t f x -> m (NonceApp t g x) #

TestEquality e => TestEquality (NonceApp t e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

testEquality :: forall (a :: BaseType) (b :: BaseType). NonceApp t e a -> NonceApp t e b -> Maybe (a :~: b) #

(HashableF e, TestEquality e) => HashableF (NonceApp t e :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: BaseType). Int -> NonceApp t e tp -> Int #

hashF :: forall (tp :: BaseType). NonceApp t e tp -> Int #

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 #

(/=) :: NonceApp t e tp -> NonceApp t e tp -> Bool #

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

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 #

show :: ExprSymFn t args ret -> String #

showList :: [ExprSymFn t args ret] -> ShowS #

Eq (ExprSymFn t args tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

(==) :: ExprSymFn t args tp -> ExprSymFn t args tp -> Bool #

(/=) :: ExprSymFn t args tp -> ExprSymFn t args tp -> Bool #

Hashable (ExprSymFn t args tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSalt :: Int -> ExprSymFn t args tp -> Int #

hash :: ExprSymFn t args tp -> Int #

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 :: k) (b :: k). Dummy a -> Dummy b -> Maybe (a :~: b) #

EqF (Dummy :: k -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

eqF :: forall (a :: k). Dummy a -> Dummy a -> Bool #

HashableF (Dummy :: k -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSaltF :: forall (tp :: k). Int -> Dummy tp -> Int #

hashF :: forall (tp :: k). Dummy tp -> Int #

OrdF (Dummy :: k -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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 #

(/=) :: Dummy tp -> Dummy tp -> Bool #

Ord (Dummy tp) Source # 
Instance details

Defined in What4.Expr.App

Methods

compare :: Dummy tp -> Dummy tp -> Ordering #

(<) :: Dummy tp -> Dummy tp -> Bool #

(<=) :: Dummy tp -> Dummy tp -> Bool #

(>) :: Dummy tp -> Dummy tp -> Bool #

(>=) :: Dummy tp -> Dummy tp -> Bool #

max :: Dummy tp -> Dummy tp -> Dummy tp #

min :: Dummy tp -> Dummy tp -> Dummy tp #

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

appEqF :: forall (e :: BaseType -> Type) (x :: BaseType) (y :: BaseType). (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 :: forall (e :: BaseType -> Type) (s :: BaseType). (OrdF e, HashableF e, HasAbsValue e, Hashable (e BaseBoolType), Hashable (e BaseRealType)) => Int -> App e s -> Int Source #

Hash an an application.

isNonLinearApp :: forall (e :: BaseType -> Type) (tp :: BaseType). 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 :: forall m e f (idx :: Ctx BaseType) (itp :: BaseType) (c :: BaseType). Functor m => (forall (tp :: BaseType). e tp -> m (f tp)) -> ArrayResultWrapper e (idx ::> itp) c -> m (ArrayResultWrapper f (idx ::> itp) c) Source #

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

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

Destructor for the AppExpr constructor.

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

Destructor for the NonceAppExpr constructor.

exprLoc :: forall t (tp :: BaseType). Expr t tp -> ProgramLoc Source #

mkExpr :: forall t (tp :: BaseType). 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 :: FloatPrecision) = Expr t (BaseFloatType fpp) Source #

type BVExpr t (n :: Nat) = 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 :: StringInfo) = Expr t (BaseStringType si) Source #

iteSize :: forall t (tp :: BaseType). Expr t tp -> Integer Source #

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

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

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

data SemiRingView t (sr :: SemiRing) 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 :: forall (sr :: SemiRing) t. SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr Source #

asWeightedSum :: forall t (sr :: SemiRing). 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 :: forall t (tp :: BaseType). Expr t tp -> AbstractValue tp Source #

Get abstract value associated with element.

compareExpr :: forall t (x :: BaseType) (y :: BaseType). Expr t x -> Expr t y -> OrderingF x y Source #

sameTerm :: forall t (a :: BaseType) (b :: BaseType). 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 
Instance details

Defined in What4.Expr.App

type Rep PPIndex = D1 ('MetaData "PPIndex" "What4.Expr.App" "what4-1.7.1.0-6kQTtE7QElt3pWV2ufmv7F" '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)))

Methods

from :: PPIndex -> Rep PPIndex x #

to :: Rep PPIndex x -> PPIndex #

Eq PPIndex Source # 
Instance details

Defined in What4.Expr.App

Methods

(==) :: PPIndex -> PPIndex -> Bool #

(/=) :: PPIndex -> PPIndex -> Bool #

Ord PPIndex Source # 
Instance details

Defined in What4.Expr.App

Methods

compare :: PPIndex -> PPIndex -> Ordering #

(<) :: PPIndex -> PPIndex -> Bool #

(<=) :: PPIndex -> PPIndex -> Bool #

(>) :: PPIndex -> PPIndex -> Bool #

(>=) :: PPIndex -> PPIndex -> Bool #

max :: PPIndex -> PPIndex -> PPIndex #

min :: PPIndex -> PPIndex -> PPIndex #

Hashable PPIndex Source # 
Instance details

Defined in What4.Expr.App

Methods

hashWithSalt :: Int -> PPIndex -> Int #

hash :: PPIndex -> Int #

type Rep PPIndex Source # 
Instance details

Defined in What4.Expr.App

type Rep PPIndex = D1 ('MetaData "PPIndex" "What4.Expr.App" "what4-1.7.1.0-6kQTtE7QElt3pWV2ufmv7F" '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 :: forall t (tp :: BaseType). 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 :: BaseType) 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 :: forall t (tp :: BaseType) s. Expr t tp -> ST s (BoundVarMap s t) Source #

boundVars' :: forall s t (tp :: BaseType). 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

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

defaultPPExprOpts :: PPExprOpts Source #

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

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

ppExprTop :: forall t (tp :: BaseType) ann. 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 :: BaseType) s ann. Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann) Source #

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

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

asMatlabSolverFn :: forall t (args :: Ctx BaseType) (ret :: BaseType). ExprSymFn t args ret -> Maybe (MatlabSolverFn (Expr t) args ret) Source #

Return solver function associated with ExprSymFn if any.

testExprSymFnEq :: forall t (a1 :: Ctx BaseType) (r1 :: BaseType) (a2 :: Ctx BaseType) (r2 :: BaseType). ExprSymFn t a1 r1 -> ExprSymFn t a2 r2 -> Maybe ((a1 ::> r1) :~: (a2 ::> r2)) Source #

traverseBVOrSet :: forall f m e (w :: Nat). (HashableF f, HasAbsValue f, OrdF f, Applicative m) => (forall (tp :: BaseType). e tp -> m (f tp)) -> BVOrSet e w -> m (BVOrSet f w) Source #

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

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

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

bvOrUnion :: forall (e :: BaseType -> Type) (w :: Nat). OrdF e => BVOrSet e w -> BVOrSet e w -> BVOrSet e w Source #

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

bvOrAbs :: forall (e :: BaseType -> Type) (w :: Natural). (OrdF e, 1 <= w) => NatRepr w -> BVOrSet e w -> BVDomain w Source #

nonceAppType :: forall (e :: BaseType -> Type) t (tp :: BaseType). IsExpr e => NonceApp t e tp -> BaseTypeRepr tp Source #

appType :: forall (e :: BaseType -> Type) (tp :: BaseType). App e tp -> BaseTypeRepr tp Source #

unconstrainedAbsValue :: forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp Source #

Return an unconstrained abstract value.

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

Return abstract domain associated with a nonce app

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

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

ppVar :: forall t (tp :: BaseType). String -> SolverSymbol -> Nonce t tp -> BaseTypeRepr tp -> String Source #

ppBoundVar :: forall t (tp :: BaseType). ExprBoundVar t tp -> String Source #

ppVarTypeCode :: forall (tp :: BaseType). 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 :: forall (e :: BaseType -> Type) (tp :: BaseType). e tp -> PrettyArg e 
PrettyText :: forall (e :: BaseType -> Type). Text -> PrettyArg e 
PrettyFunc :: forall (e :: BaseType -> Type). Text -> [PrettyArg e] -> PrettyArg e 

exprPrettyArg :: forall e (tp :: BaseType). e tp -> PrettyArg e Source #

exprPrettyIndices :: forall (e :: BaseType -> Type) (ctx :: Ctx BaseType). Assignment e ctx -> [PrettyArg e] Source #

stringPrettyArg :: forall (e :: BaseType -> Type). String -> PrettyArg e Source #

showPrettyArg :: forall a (e :: BaseType -> Type). Show a => a -> PrettyArg e Source #

type PrettyApp (e :: BaseType -> Type) = (Text, [PrettyArg e]) Source #

prettyApp :: forall (e :: BaseType -> Type). Text -> [PrettyArg e] -> PrettyApp e Source #

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

ppApp' :: forall (e :: BaseType -> Type) (u :: BaseType). App e u -> PrettyApp e Source #