What4.Interface

Defines interface between the simulator and terms that are sent to the SAT or SMT solver. The simulator can use a richer set of types, but the symbolic values must be representable by types supported by this interface.

A solver backend is defined in terms of a type parameter sym, which is the type that tracks whatever state or context is needed by that particular backend. To instantiate the solver interface, one must provide several type family definitions and class instances for sym:

type SymExpr sym :: BaseType -> *

Type of symbolic expressions.

type BoundVar sym :: BaseType -> *

Representation of bound variables in symbolic expressions.

type SymFn sym :: Ctx BaseType -> BaseType -> *

Representation of symbolic functions.

instance IsExprBuilder sym

Functions for building expressions of various types.

instance IsSymExprBuilder sym

Functions for building expressions with bound variables and quantifiers.

instance IsExpr (SymExpr sym)

Recognizers for various kinds of literal expressions.

instance OrdF (SymExpr sym)

instance TestEquality (SymExpr sym)

instance HashableF (SymExpr sym)

The canonical implementation of these interface classes is found in What4.Expr.Builder.

Interface classes

Type Families

type family SymExpr (sym :: Type) :: BaseType -> Type

The class for expressions.

Instances

type SymExpr (ExprBuilder t st fs)

Defined in What4.Expr.Builder

type SymExpr (ExprBuilder t st fs) = Expr t

type family BoundVar (sym :: Type) :: BaseType -> Type

Type of bound variable associated with symbolic state.

This type is used by some methods in class IsSymExprBuilder.

Instances

type BoundVar (ExprBuilder t st fs)

Defined in What4.Expr.Builder

type BoundVar (ExprBuilder t st fs) = ExprBoundVar t

type family SymFn sym :: Ctx BaseType -> BaseType -> Type

A function that can be applied to symbolic arguments.

This type is used by some methods in classes IsExprBuilder and IsSymExprBuilder.

Instances

type SymFn (ExprBuilder t st fs)

Defined in What4.Expr.Builder

type SymFn (ExprBuilder t st fs) = ExprSymFn t

type family SymAnnotation (sym :: Type) :: BaseType -> Type

Type used to uniquely identify expressions that have been annotated.

Instances

type SymAnnotation (ExprBuilder t st fs)

Defined in What4.Expr.Builder

type SymAnnotation (ExprBuilder t st fs) = Nonce t :: BaseType -> Type

Expression recognizers

class HasAbsValue e => IsExpr e where

This class provides operations for recognizing when symbolic expressions represent concrete values, extracting the type from an expression, and for providing pretty-printed representations of an expression.

Minimal complete definition

integerBounds, asFloat, rationalBounds, unsignedBVBounds, signedBVBounds, asAffineVar, exprType, printSymExpr

Methods

asConstantPred :: e BaseBoolType -> Maybe Bool

Evaluate if predicate is constant.

asInteger :: e BaseIntegerType -> Maybe Integer

Return integer if this is a constant integer.

integerBounds :: e BaseIntegerType -> ValueRange Integer

Return any bounding information we have about the term

asRational :: e BaseRealType -> Maybe Rational

Return rational if this is a constant value.

asFloat :: e (BaseFloatType fpp) -> Maybe BigFloat

Return floating-point value if this is a constant

rationalBounds :: e BaseRealType -> ValueRange Rational

Return any bounding information we have about the term

asComplex :: e BaseComplexType -> Maybe (Complex Rational)

Return complex if this is a constant value.

asBV :: e (BaseBVType w) -> Maybe (BV w)

Return a bitvector if this is a constant bitvector.

unsignedBVBounds :: 1 <= w => e (BaseBVType w) -> Maybe (Integer, Integer)

If we have bounds information about the term, return unsigned upper and lower bounds as integers

signedBVBounds :: 1 <= w => e (BaseBVType w) -> Maybe (Integer, Integer)

If we have bounds information about the term, return signed upper and lower bounds as integers

asAffineVar :: e tp -> Maybe (ConcreteVal tp, e tp, ConcreteVal tp)

If this expression syntactically represents an "affine" form, return its components. When asAffineVar x = Just (c,r,o), then we have x == c*r + o.

asString :: e (BaseStringType si) -> Maybe (StringLiteral si)

Return the string value if this is a constant string

stringInfo :: e (BaseStringType si) -> StringInfoRepr si

Return the representation of the string info for a string-typed term.

asConstantArray :: e (BaseArrayType idx bt) -> Maybe (e bt)

Return the unique element value if this is a constant array, such as one made with constantArray.

asStruct :: e (BaseStructType flds) -> Maybe (Assignment e flds)

Return the struct fields if this is a concrete struct.

exprType :: e tp -> BaseTypeRepr tp

Get type of expression.

bvWidth :: e (BaseBVType w) -> NatRepr w

Get the width of a bitvector

floatPrecision :: e (BaseFloatType fpp) -> FloatPrecisionRepr fpp

Get the precision of a floating-point expression

printSymExpr :: e tp -> Doc ann

Print a sym expression for debugging or display purposes.

Instances

IsExpr (Expr t)

Defined in What4.Expr.App

Methods

asConstantPred :: Expr t BaseBoolType -> Maybe Bool

asInteger :: Expr t BaseIntegerType -> Maybe Integer

integerBounds :: Expr t BaseIntegerType -> ValueRange Integer

asRational :: Expr t BaseRealType -> Maybe Rational

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

rationalBounds :: Expr t BaseRealType -> ValueRange Rational

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

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

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

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

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

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

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

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

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

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

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

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

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

class IsSymFn fn where

A class for extracting type representatives from symbolic functions

Methods

fnArgTypes :: fn args ret -> Assignment BaseTypeRepr args

Get the argument types of a function.

fnReturnType :: fn args ret -> BaseTypeRepr ret

Get the return type of a function.

Instances

IsSymFn (ExprSymFn t)

Defined in What4.Expr.App

Methods

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

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

data UnfoldPolicy

Describes when we unfold the body of defined functions.

Constructors

NeverUnfold

What4 will not unfold the body of functions when applied to arguments

AlwaysUnfold

The function will be unfolded into its definition whenever it is applied to arguments

UnfoldConcrete

The function will be unfolded into its definition only if all the provided arguments are concrete.

Instances

Eq UnfoldPolicy

Defined in What4.Interface

Methods

(==) :: UnfoldPolicy -> UnfoldPolicy -> Bool

(/=) :: UnfoldPolicy -> UnfoldPolicy -> Bool

Ord UnfoldPolicy

Defined in What4.Interface

Methods

compare :: UnfoldPolicy -> UnfoldPolicy -> Ordering

(<) :: UnfoldPolicy -> UnfoldPolicy -> Bool

(<=) :: UnfoldPolicy -> UnfoldPolicy -> Bool

(>) :: UnfoldPolicy -> UnfoldPolicy -> Bool

(>=) :: UnfoldPolicy -> UnfoldPolicy -> Bool

max :: UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy

min :: UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy

Show UnfoldPolicy

Defined in What4.Interface

Methods

showsPrec :: Int -> UnfoldPolicy -> ShowS

show :: UnfoldPolicy -> String

showList :: [UnfoldPolicy] -> ShowS

shouldUnfold :: IsExpr e => UnfoldPolicy -> Assignment e args -> Bool

Evaluates an UnfoldPolicy on a collection of arguments.

IsExprBuilder

class (IsExpr (SymExpr sym), HashableF (SymExpr sym), TestEquality (SymAnnotation sym), OrdF (SymAnnotation sym), HashableF (SymAnnotation sym)) => IsExprBuilder sym where

This class allows the simulator to build symbolic expressions.

Methods of this class refer to type families SymExpr sym and SymFn sym.

Note: Some methods in this class represent operations that are partial functions on their domain (e.g., division by 0). Such functions will have documentation strings indicating that they are undefined under some conditions. When partial functions are applied outside their defined domains, they will silently produce an unspecified value of the expected type. The unspecified value returned as the result of an undefined function is _not_ guaranteed to be equivalant to a free constant, and no guarantees are made about what properties such values will satisfy.

Minimal complete definition

getConfiguration, setSolverLogListener, getSolverLogListener, logSolverEvent, getCurrentProgramLoc, setCurrentProgramLoc, annotateTerm, getAnnotation, truePred, falsePred, notPred, andPred, orPred, xorPred, eqPred, itePred, intLit, intNeg, intAdd, intMul, intIte, intEq, intLe, intAbs, intDiv, intMod, intDivisible, bvLit, bvConcat, bvSelect, bvNeg, bvAdd, bvMul, bvUdiv, bvUrem, bvSdiv, bvSrem, testBitBV, bvIte, bvEq, bvUlt, bvSlt, bvIsNonzero, bvShl, bvLshr, bvAshr, bvRol, bvRor, bvZext, bvSext, bvAndBits, bvOrBits, bvXorBits, bvNotBits, bvFill, bvPopcount, bvCountLeadingZeros, bvCountTrailingZeros, mkStruct, structField, structIte, constantArray, arrayFromFn, arrayMap, arrayUpdate, arrayLookup, arrayIte, arrayEq, arrayTrueOnEntries, integerToReal, bvToInteger, sbvToInteger, predToBV, realRound, realRoundEven, realFloor, realCeil, integerToBV, realToInteger, stringEmpty, stringLit, stringEq, stringIte, stringConcat, stringContains, stringIsPrefixOf, stringIsSuffixOf, stringIndexOf, stringLength, stringSubstring, realZero, realLit, realEq, realLe, realIte, realNeg, realAdd, realMul, realDiv, isInteger, realSqrt, realAtan2, realPi, realLog, realExp, realSin, realCos, realSinh, realCosh, floatPZero, floatNZero, floatNaN, floatPInf, floatNInf, floatLit, floatNeg, floatAbs, floatSqrt, floatAdd, floatSub, floatMul, floatDiv, floatRem, floatMin, floatMax, floatFMA, floatEq, floatNe, floatFpEq, floatLe, floatLt, floatGe, floatGt, floatIsNaN, floatIsInf, floatIsZero, floatIsPos, floatIsNeg, floatIsSubnorm, floatIsNorm, floatIte, floatCast, floatRound, floatFromBinary, floatToBinary, bvToFloat, sbvToFloat, realToFloat, floatToBV, floatToSBV, floatToReal, mkComplex, getRealPart, getImagPart, cplxGetParts

Methods

getConfiguration :: sym -> Config

Retrieve the configuration object corresponding to this solver interface.

setSolverLogListener :: sym -> Maybe (SolverEvent -> IO ()) -> IO ()

Install an action that will be invoked before and after calls to backend solvers. This action is primarily intended to be used for logging/profiling/debugging purposes. Passing Nothing to this function disables logging.

getSolverLogListener :: sym -> IO (Maybe (SolverEvent -> IO ()))

Get the currently-installed solver log listener, if one has been installed.

logSolverEvent :: sym -> SolverEvent -> IO ()

Provide the given event to the currently installed solver log listener, if any.

getStatistics :: sym -> IO Statistics

Get statistics on execution from the initialization of the symbolic interface to this point. May return zeros if gathering statistics isn't supported.

getCurrentProgramLoc :: sym -> IO ProgramLoc

Get current location of program for term creation purposes.

setCurrentProgramLoc :: sym -> ProgramLoc -> IO ()

Set current location of program for term creation purposes.

isEq :: sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)

Return true if two expressions are equal. The default implementation dispatches eqPred, bvEq, natEq, intEq, realEq, cplxEq, structEq, or arrayEq, depending on the type.

baseTypeIte :: sym -> Pred sym -> SymExpr sym tp -> SymExpr sym tp -> IO (SymExpr sym tp)

Take the if-then-else of two expressions. The default implementation dispatches itePred, bvIte, natIte, intIte, realIte, cplxIte, structIte, or arrayIte, depending on the type.

annotateTerm :: sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)

Given a symbolic expression, annotate it with a unique identifier that can be used to maintain a connection with the given term. The SymAnnotation is intended to be used as the key in a hash table or map to additional data can be maintained alongside the terms. The returned SymExpr has the same semantics as the argument, but has embedded in it the SymAnnotation value so that it can be used later during term traversals.

Note, the returned annotation is not necessarily fresh; if an already-annotated term is passed in, the same annotation value will be returned.

getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)

Project an annotation from an expression

It should be the case that using getAnnotation on a term returned by annotateTerm returns the same annotation that annotateTerm did.

truePred :: sym -> Pred sym

Constant true predicate

falsePred :: sym -> Pred sym

Constant false predicate

notPred :: sym -> Pred sym -> IO (Pred sym)

Boolean negation

andPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

Boolean conjunction

orPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

Boolean disjunction

impliesPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

Boolean implication

xorPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

Exclusive-or operation

eqPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)

Equality of boolean values

itePred :: sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)

If-then-else on a predicate.

intLit :: sym -> Integer -> IO (SymInteger sym)

Create an integer literal.

intNeg :: sym -> SymInteger sym -> IO (SymInteger sym)

Negate an integer.

intAdd :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

Add two integers.

intSub :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

Subtract one integer from another.

intMul :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

Multiply one integer by another.

intMin :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

Return the minimum value of two integers.

intMax :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

Return the maximum value of two integers.

intIte :: sym -> Pred sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

If-then-else applied to integers.

intEq :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)

Integer equality.

intLe :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)

Integer less-than-or-equal.

intLt :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)

Integer less-than.

intAbs :: sym -> SymInteger sym -> IO (SymInteger sym)

Compute the absolute value of an integer.

intDiv :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

intDiv x y computes the integer division of x by y. This division is interpreted the same way as the SMT-Lib integer theory, which states that div and mod are the unique Euclidean division operations satisfying the following for all y /= 0:

• y * (div x y) + (mod x y) == x

•  0 <= mod x y < abs y

The value of intDiv x y is undefined when y = 0.

Integer division requires nonlinear support whenever the divisor is not a constant.

Note: div x y is floor (x/y) when y is positive (regardless of sign of x) and ceiling (x/y) when y is negative. This is neither of the more common "round toward zero" nor "round toward -inf" definitions.

Some useful theorems that are true of this division/modulus pair:

• mod x y == mod x (- y) == mod x (abs y)

• div x (-y) == -(div x y)

intMod :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)

intMod x y computes the integer modulus of x by y. See intDiv for more details.

The value of intMod x y is undefined when y = 0.

Integer modulus requires nonlinear support whenever the divisor is not a constant.

intDivisible :: sym -> SymInteger sym -> Natural -> IO (Pred sym)

intDivisible x k is true whenever x is an integer divisible by the known natural number k. In other words `divisible x k` holds if there exists an integer z such that `x = k*z`.

bvLit :: 1 <= w => sym -> NatRepr w -> BV w -> IO (SymBV sym w)

Create a bitvector with the given width and value.

bvConcat

Arguments

:: (1 <= u, 1 <= v)

=> sym

-> SymBV sym u

most significant bits

-> SymBV sym v

least significant bits

-> IO (SymBV sym (u + v))

Concatenate two bitvectors.

bvSelect

Arguments

:: forall idx n w. (1 <= n, (idx + n) <= w)

=> sym

-> NatRepr idx

Starting index, from 0 as least significant bit

-> NatRepr n

Number of bits to take

-> SymBV sym w

Bitvector to select from

-> IO (SymBV sym n)

Select a subsequence from a bitvector.

bvNeg :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)

2's complement negation.

bvAdd :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Add two bitvectors.

bvSub :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Subtract one bitvector from another.

bvMul :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Multiply one bitvector by another.

bvUdiv :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Unsigned bitvector division.

The result of bvUdiv x y is undefined when y is zero, but is otherwise equal to floor( x / y ).

bvUrem :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Unsigned bitvector remainder.

The result of bvUrem x y is undefined when y is zero, but is otherwise equal to x - (bvUdiv x y) * y.

bvSdiv :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Signed bitvector division. The result is truncated to zero.

The result of bvSdiv x y is undefined when y is zero, but is equal to floor(x/y) when x and y have the same sign, and equal to ceiling(x/y) when x and y have opposite signs.

NOTE! However, that there is a corner case when dividing MIN_INT by -1, in which case an overflow condition occurs, and the result is instead MIN_INT.

bvSrem :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Signed bitvector remainder.

The result of bvSrem x y is undefined when y is zero, but is otherwise equal to x - (bvSdiv x y) * y.

testBitBV

Arguments

:: 1 <= w

=> sym

-> Natural

Index of bit (0 is the least significant bit)

-> SymBV sym w

-> IO (Pred sym)

Returns true if the corresponding bit in the bitvector is set.

bvIsNeg :: 1 <= w => sym -> SymBV sym w -> IO (Pred sym)

Return true if bitvector is negative.

bvIte :: 1 <= w => sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

If-then-else applied to bitvectors.

bvEq :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Return true if bitvectors are equal.

bvNe :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Return true if bitvectors are distinct.

bvUlt :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Unsigned less-than.

bvUle :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Unsigned less-than-or-equal.

bvUge :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Unsigned greater-than-or-equal.

bvUgt :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Unsigned greater-than.

bvSlt :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Signed less-than.

bvSgt :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Signed greater-than.

bvSle :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Signed less-than-or-equal.

bvSge :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)

Signed greater-than-or-equal.

bvIsNonzero :: 1 <= w => sym -> SymBV sym w -> IO (Pred sym)

returns true if the given bitvector is non-zero.

bvShl

Arguments

:: 1 <= w

=> sym

-> SymBV sym w

Shift this

-> SymBV sym w

Amount to shift by

-> IO (SymBV sym w)

Left shift. The shift amount is treated as an unsigned value.

bvLshr

Arguments

:: 1 <= w

=> sym

-> SymBV sym w

Shift this

-> SymBV sym w

Amount to shift by

-> IO (SymBV sym w)

Logical right shift. The shift amount is treated as an unsigned value.

bvAshr

Arguments

:: 1 <= w

=> sym

-> SymBV sym w

Shift this

-> SymBV sym w

Amount to shift by

-> IO (SymBV sym w)

Arithmetic right shift. The shift amount is treated as an unsigned value.

bvRol

Arguments

:: 1 <= w

=> sym

-> SymBV sym w

bitvector to rotate

-> SymBV sym w

amount to rotate by

-> IO (SymBV sym w)

Rotate left. The rotate amount is treated as an unsigned value.

bvRor

Arguments

:: 1 <= w

=> sym

-> SymBV sym w

bitvector to rotate

-> SymBV sym w

amount to rotate by

-> IO (SymBV sym w)

Rotate right. The rotate amount is treated as an unsigned value.

bvZext :: (1 <= u, (u + 1) <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)

Zero-extend a bitvector.

bvSext :: (1 <= u, (u + 1) <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)

Sign-extend a bitvector.

bvTrunc :: (1 <= r, (r + 1) <= w) => sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)

Truncate a bitvector.

bvAndBits :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Bitwise logical and.

bvOrBits :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Bitwise logical or.

bvXorBits :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)

Bitwise logical exclusive or.

bvNotBits :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)

Bitwise complement.

bvSet

Arguments

:: forall w. 1 <= w

=> sym

Symbolic interface

-> SymBV sym w

Bitvector to update

-> Natural

0-based index to set

-> Pred sym

Predicate to set.

-> IO (SymBV sym w)

bvSet sym v i p returns a bitvector v' where bit i of v' is set to p, and the bits at the other indices are the same as in v.

bvFill

Arguments

:: forall w. 1 <= w

=> sym

symbolic interface

-> NatRepr w

output bitvector width

-> Pred sym

predicate to fill the bitvector with

-> IO (SymBV sym w)

bvFill sym w p returns a bitvector w-bits long where every bit is given by the boolean value of p.

minUnsignedBV :: 1 <= w => sym -> NatRepr w -> IO (SymBV sym w)

Return the bitvector of the desired width with all 0 bits; this is the minimum unsigned integer.

maxUnsignedBV :: 1 <= w => sym -> NatRepr w -> IO (SymBV sym w)

Return the bitvector of the desired width with all bits set; this is the maximum unsigned integer.

maxSignedBV :: 1 <= w => sym -> NatRepr w -> IO (SymBV sym w)

Return the bitvector representing the largest 2's complement signed integer of the given width. This consists of all bits set except the MSB.

minSignedBV :: 1 <= w => sym -> NatRepr w -> IO (SymBV sym w)

Return the bitvector representing the smallest 2's complement signed integer of the given width. This consists of all 0 bits except the MSB, which is set.

bvPopcount :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)

Return the number of 1 bits in the input.

bvCountLeadingZeros :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)

Return the number of consecutive 0 bits in the input, starting from the most significant bit position. If the input is zero, all bits are counted as leading.

bvCountTrailingZeros :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)

Return the number of consecutive 0 bits in the input, starting from the least significant bit position. If the input is zero, all bits are counted as leading.

addUnsignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)

Unsigned add with overflow bit.

addSignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)

Signed add with overflow bit. Overflow is true if positive + positive = negative, or if negative + negative = positive.

subUnsignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)

Unsigned subtract with overflow bit. Overflow is true if x < y.

subSignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)

Signed subtract with overflow bit. Overflow is true if positive - negative = negative, or if negative - positive = positive.

carrylessMultiply :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))

Compute the carry-less multiply of the two input bitvectors. This operation is essentially the same as a standard multiply, except that the partial addends are simply XOR'd together instead of using a standard adder. This operation is useful for computing on GF(2^n) polynomials.

unsignedWideMultiplyBV :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)

unsignedWideMultiplyBV sym x y multiplies two unsigned w bit numbers x and y.

It returns a pair containing the top w bits as the first element, and the lower w bits as the second element.

mulUnsignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)

Compute the unsigned multiply of two values with overflow bit.

signedWideMultiplyBV :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)

signedWideMultiplyBV sym x y multiplies two signed w bit numbers x and y.

It returns a pair containing the top w bits as the first element, and the lower w bits as the second element.

mulSignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)

Compute the signed multiply of two values with overflow bit.

mkStruct :: sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)

Create a struct from an assignment of expressions.

structField :: sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)

Get the value of a specific field in a struct.

structEq :: forall flds. sym -> SymStruct sym flds -> SymStruct sym flds -> IO (Pred sym)

Check if two structs are equal.

structIte :: sym -> Pred sym -> SymStruct sym flds -> SymStruct sym flds -> IO (SymStruct sym flds)

Take the if-then-else of two structures.

constantArray

Arguments

:: sym

-> Assignment BaseTypeRepr (idx ::> tp)

Index type

-> SymExpr sym b

Constant

-> IO (SymArray sym (idx ::> tp) b)

Create an array where each element has the same value.

arrayFromFn :: sym -> SymFn sym (idx ::> itp) ret -> IO (SymArray sym (idx ::> itp) ret)

Create an array from an arbitrary symbolic function.

Arrays created this way can typically not be compared for equality when provided to backend solvers.

arrayMap :: sym -> SymFn sym (ctx ::> d) r -> Assignment (ArrayResultWrapper (SymExpr sym) (idx ::> itp)) (ctx ::> d) -> IO (SymArray sym (idx ::> itp) r)

Create an array by mapping a function over one or more existing arrays.

arrayUpdate :: sym -> SymArray sym (idx ::> tp) b -> Assignment (SymExpr sym) (idx ::> tp) -> SymExpr sym b -> IO (SymArray sym (idx ::> tp) b)

Update an array at a specific location.

arrayLookup :: sym -> SymArray sym (idx ::> tp) b -> Assignment (SymExpr sym) (idx ::> tp) -> IO (SymExpr sym b)

Return element in array.

arrayFromMap

Arguments

:: sym

-> Assignment BaseTypeRepr (idx ::> itp)

Types for indices

-> ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp

Value for known indices.

-> SymExpr sym tp

Value for other entries.

-> IO (SymArray sym (idx ::> itp) tp)

Create an array from a map of concrete indices to values.

This is implemented, but designed to be overridden for efficiency.

arrayUpdateAtIdxLits

Arguments

:: sym

-> ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp

Value for known indices.

-> SymArray sym (idx ::> itp) tp

Value for existing array.

-> IO (SymArray sym (idx ::> itp) tp)

Update an array at specific concrete indices.

This is implemented, but designed to be overriden for efficiency.

arrayIte :: sym -> Pred sym -> SymArray sym idx b -> SymArray sym idx b -> IO (SymArray sym idx b)

If-then-else applied to arrays.

arrayEq :: sym -> SymArray sym idx b -> SymArray sym idx b -> IO (Pred sym)

Return true if two arrays are equal.

Note that in the backend, arrays do not have a fixed number of elements, so this equality requires that arrays are equal on all elements.

allTrueEntries :: sym -> SymArray sym idx BaseBoolType -> IO (Pred sym)

Return true if all entries in the array are true.

arrayTrueOnEntries

Arguments

:: sym

-> SymFn sym (idx ::> itp) BaseBoolType

Predicate that indicates if array should be true.

-> SymArray sym (idx ::> itp) BaseBoolType

-> IO (Pred sym)

Return true if the array has the value true at every index satisfying the given predicate.

integerToReal :: sym -> SymInteger sym -> IO (SymReal sym)

Convert an integer to a real number.

bvToInteger :: 1 <= w => sym -> SymBV sym w -> IO (SymInteger sym)

Return the unsigned value of the given bitvector as an integer.

sbvToInteger :: 1 <= w => sym -> SymBV sym w -> IO (SymInteger sym)

Return the signed value of the given bitvector as an integer.

predToBV :: 1 <= w => sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)

Return 1 if the predicate is true; 0 otherwise.

uintToReal :: 1 <= w => sym -> SymBV sym w -> IO (SymReal sym)

Convert an unsigned bitvector to a real number.

sbvToReal :: 1 <= w => sym -> SymBV sym w -> IO (SymReal sym)

Convert an signed bitvector to a real number.

realRound :: sym -> SymReal sym -> IO (SymInteger sym)

Round a real number to an integer.

Numbers are rounded to the nearest integer, with rounding away from zero when two integers are equidistant (e.g., 1.5 rounds to 2).

realRoundEven :: sym -> SymReal sym -> IO (SymInteger sym)

Round a real number to an integer.

Numbers are rounded to the nearest integer, with rounding toward even values when two integers are equidistant (e.g., 2.5 rounds to 2).

realFloor :: sym -> SymReal sym -> IO (SymInteger sym)

Round down to the nearest integer that is at most this value.

realCeil :: sym -> SymReal sym -> IO (SymInteger sym)

Round up to the nearest integer that is at least this value.

realTrunc :: sym -> SymReal sym -> IO (SymInteger sym)

Round toward zero. This is floor(x) when x is positive and celing(x) when x is negative.

integerToBV :: 1 <= w => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)

Convert an integer to a bitvector. The result is the unique bitvector whose value (signed or unsigned) is congruent to the input integer, modulo 2^w.

This operation has the following properties:

• bvToInteger (integerToBv x w) == mod x (2^w)

• bvToInteger (integerToBV x w) == x when 0 <= x < 2^w.

• sbvToInteger (integerToBV x w) == mod (x + 2^(w-1)) (2^w) - 2^(w-1)

• sbvToInteger (integerToBV x w) == x when -2^(w-1) <= x < 2^(w-1)
• integerToBV (bvToInteger y) w == y when y is a SymBV sym w
• integerToBV (sbvToInteger y) w == y when y is a SymBV sym w

realToInteger :: sym -> SymReal sym -> IO (SymInteger sym)

Convert a real number to an integer.

The result is undefined if the given real number does not represent an integer.

realToBV :: 1 <= w => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)

Convert a real number to an unsigned bitvector.

Numbers are rounded to the nearest representable number, with rounding away from zero when two integers are equidistant (e.g., 1.5 rounds to 2). When the real is negative the result is zero.

realToSBV :: 1 <= w => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)

Convert a real number to a signed bitvector.

Numbers are rounded to the nearest representable number, with rounding away from zero when two integers are equidistant (e.g., 1.5 rounds to 2).

clampedIntToSBV :: 1 <= w => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)

Convert an integer to the nearest signed bitvector.

Numbers are rounded to the nearest representable number.

clampedIntToBV :: 1 <= w => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)

Convert an integer to the nearest unsigned bitvector.

Numbers are rounded to the nearest representable number.

intSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)

Convert a signed bitvector to the nearest signed bitvector with the given width. If the resulting width is smaller, this clamps the value to min-int or max-int when necessary.

uintSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)

Convert an unsigned bitvector to the nearest unsigned bitvector with the given width (clamp on overflow).

intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)

Convert an signed bitvector to the nearest unsigned bitvector with the given width (clamp on overflow).

uintToInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)

Convert an unsigned bitvector to the nearest signed bitvector with the given width (clamp on overflow).

stringEmpty :: sym -> StringInfoRepr si -> IO (SymString sym si)

Create an empty string literal

stringLit :: sym -> StringLiteral si -> IO (SymString sym si)

Create a concrete string literal

stringEq :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)

Check the equality of two strings

stringIte :: sym -> Pred sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)

If-then-else on strings

stringConcat :: sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)

Concatenate two strings

stringContains :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)

Test if the first string contains the second string as a substring

stringIsPrefixOf :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)

Test if the first string is a prefix of the second string

stringIsSuffixOf :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)

Test if the first string is a suffix of the second string

stringIndexOf :: sym -> SymString sym si -> SymString sym si -> SymInteger sym -> IO (SymInteger sym)

Return the first position at which the second string can be found as a substring in the first string, starting from the given index. If no such position exists, return a negative value.

stringLength :: sym -> SymString sym si -> IO (SymInteger sym)

Compute the length of a string

stringSubstring :: sym -> SymString sym si -> SymInteger sym -> SymInteger sym -> IO (SymString sym si)

stringSubstring s off len extracts the substring of s starting at index off and having length len. The result of this operation is undefined if off and len do not specify a valid substring of s; in particular, we must have 0 <= off, 0 <= len and off+len <= length(s)@.

realZero :: sym -> SymReal sym

Return real number 0.

realLit :: sym -> Rational -> IO (SymReal sym)

Create a constant real literal.

sciLit :: sym -> Scientific -> IO (SymReal sym)

Make a real literal from a scientific value. May be overridden if we want to avoid the overhead of converting scientific value to rational.

realEq :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)

Check equality of two real numbers.

realNe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)

Check non-equality of two real numbers.

realLe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)

Check <= on two real numbers.

realLt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)

Check < on two real numbers.

realGe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)

Check >= on two real numbers.

realGt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)

Check > on two real numbers.

realIte :: sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

If-then-else on real numbers.

realMin :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

Return the minimum of two real numbers.

realMax :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

Return the maxmimum of two real numbers.

realNeg :: sym -> SymReal sym -> IO (SymReal sym)

Negate a real number.

realAdd :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

Add two real numbers.

realMul :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

Multiply two real numbers.

realSub :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

Subtract one real from another.

realSq :: sym -> SymReal sym -> IO (SymReal sym)

realSq sym x returns x * x.

realDiv :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

realDiv sym x y returns term equivalent to x/y.

The result is undefined when y is zero.

realMod :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

realMod x y returns the value of x - y * floor(x / y) when y is not zero and x when y is zero.

isInteger :: sym -> SymReal sym -> IO (Pred sym)

Predicate that holds if the real number is an exact integer.

realIsNonNeg :: sym -> SymReal sym -> IO (Pred sym)

Return true if the real is non-negative.

realSqrt :: sym -> SymReal sym -> IO (SymReal sym)

realSqrt sym x returns sqrt(x). Result is undefined if x is negative.

realAtan2 :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

realAtan2 sym y x returns the arctangent of y/x with a range of -pi to pi; this corresponds to the angle between the positive x-axis and the line from the origin (x,y).

When x is 0 this returns pi/2 * sgn y.

When x and y are both zero, this function is undefined.

realPi :: sym -> IO (SymReal sym)

Return value denoting pi.

realLog :: sym -> SymReal sym -> IO (SymReal sym)

Natural logarithm. realLog x is undefined for x <= 0.

realExp :: sym -> SymReal sym -> IO (SymReal sym)

Natural exponentiation

realSin :: sym -> SymReal sym -> IO (SymReal sym)

Sine trig function

realCos :: sym -> SymReal sym -> IO (SymReal sym)

Cosine trig function

realTan :: sym -> SymReal sym -> IO (SymReal sym)

Tangent trig function. realTan x is undefined when cos x = 0, i.e., when x = pi/2 + k*pi for some integer k.

realSinh :: sym -> SymReal sym -> IO (SymReal sym)

Hyperbolic sine

realCosh :: sym -> SymReal sym -> IO (SymReal sym)

Hyperbolic cosine

realTanh :: sym -> SymReal sym -> IO (SymReal sym)

Hyperbolic tangent

realAbs :: sym -> SymReal sym -> IO (SymReal sym)

Return absolute value of the real number.

realHypot :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)

realHypot x y returns sqrt(x^2 + y^2).

floatPZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

Return floating point number +0.

floatNZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

Return floating point number -0.

floatNaN :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

Return floating point NaN.

floatPInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

Return floating point +infinity.

floatNInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)

Return floating point -infinity.

floatLitRational :: sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)

Create a floating point literal from a rational literal. The rational value will be rounded if necessary using the "round to nearest even" rounding mode.

floatLit :: sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)

Create a floating point literal from a BigFloat value.

floatNeg :: sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Negate a floating point number.

floatAbs :: sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Return the absolute value of a floating point number.

floatSqrt :: sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Compute the square root of a floating point number.

floatAdd :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Add two floating point numbers.

floatSub :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Subtract two floating point numbers.

floatMul :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Multiply two floating point numbers.

floatDiv :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Divide two floating point numbers.

floatRem :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Compute the reminder: x - y * n, where n in Z is nearest to x / y (breaking ties to even values of n).

floatMin :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Return the minimum of two floating point numbers. If one argument is NaN, return the other argument. If the arguments are equal when compared as floating-point values, one of the two will be returned, but it is unspecified which; this underspecification can (only) be observed with zeros of different signs.

floatMax :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Return the maximum of two floating point numbers. If one argument is NaN, return the other argument. If the arguments are equal when compared as floating-point values, one of the two will be returned, but it is unspecified which; this underspecification can (only) be observed with zeros of different signs.

floatFMA :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Compute the fused multiplication and addition: (x * y) + z.

floatEq :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check logical equality of two floating point numbers.

NOTE! This does NOT accurately represent the equality test on floating point values typically found in programming languages. See floatFpEq instead.

floatNe :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check logical non-equality of two floating point numbers.

NOTE! This does NOT accurately represent the non-equality test on floating point values typically found in programming languages. See floatFpEq instead.

floatFpEq :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check IEEE-754 equality of two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not equal to itself! Moreover, positive and negative 0 will compare equal, despite having different bit patterns.

This test is most appropriate for interpreting the equality tests of typical languages using floating point. Moreover, not-equal tests are usually the negation of this test, rather than the floatFpNe test below.

floatFpApart :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check IEEE-754 apartness of two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not apart from any other value! Moreover, positive and negative 0 will not compare apart, despite having different bit patterns. Note that x is apart from y iff x < y or x > y.

This test usually does NOT correspond to the not-equal tests found in programming languages. Instead, one generally takes the logical negation of the floatFpEq test.

floatFpUnordered :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check if two floating point numbers are "unordered". This happens precicely when one or both of the inputs is NaN.

floatLe :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check IEEE-754 <= on two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not less-than-or-equal-to any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns.

floatLt :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check IEEE-754 < on two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not less-than any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns.

floatGe :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check IEEE-754 >= on two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not greater-than-or-equal-to any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns.

floatGt :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)

Check IEEE-754 > on two floating point numbers.

NOTE! This test returns false if either value is NaN; in particular NaN is not greater-than any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns.

floatIsNaN :: sym -> SymFloat sym fpp -> IO (Pred sym)

Test if a floating-point value is NaN.

floatIsInf :: sym -> SymFloat sym fpp -> IO (Pred sym)

Test if a floating-point value is (positive or negative) infinity.

floatIsZero :: sym -> SymFloat sym fpp -> IO (Pred sym)

Test if a floating-point value is (positive or negative) zero.

floatIsPos :: sym -> SymFloat sym fpp -> IO (Pred sym)

Test if a floating-point value is positive. NOTE! NaN is considered neither positive nor negative.

floatIsNeg :: sym -> SymFloat sym fpp -> IO (Pred sym)

Test if a floating-point value is negative. NOTE! NaN is considered neither positive nor negative.

floatIsSubnorm :: sym -> SymFloat sym fpp -> IO (Pred sym)

Test if a floating-point value is subnormal.

floatIsNorm :: sym -> SymFloat sym fpp -> IO (Pred sym)

Test if a floating-point value is normal.

floatIte :: sym -> Pred sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)

If-then-else on floating point numbers.

floatCast :: sym -> FloatPrecisionRepr fpp -> RoundingMode -> SymFloat sym fpp' -> IO (SymFloat sym fpp)

Change the precision of a floating point number.

floatRound :: sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)

Round a floating point number to an integral value.

floatFromBinary :: (2 <= eb, 2 <= sb) => sym -> FloatPrecisionRepr (FloatingPointPrecision eb sb) -> SymBV sym (eb + sb) -> IO (SymFloat sym (FloatingPointPrecision eb sb))

Convert from binary representation in IEEE 754-2008 format to floating point.

floatToBinary :: (2 <= eb, 2 <= sb) => sym -> SymFloat sym (FloatingPointPrecision eb sb) -> IO (SymBV sym (eb + sb))

Convert from floating point from to the binary representation in IEEE 754-2008 format.

NOTE! NaN has multiple representations, i.e. all bit patterns where the exponent is 0b1..1 and the significant is not 0b0..0. This functions returns the representation of positive "quiet" NaN, i.e. the bit pattern where the sign is 0b0, the exponent is 0b1..1, and the significant is 0b10..0.

bvToFloat :: 1 <= w => sym -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV sym w -> IO (SymFloat sym fpp)

Convert a unsigned bitvector to a floating point number.

sbvToFloat :: 1 <= w => sym -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV sym w -> IO (SymFloat sym fpp)

Convert a signed bitvector to a floating point number.

realToFloat :: sym -> FloatPrecisionRepr fpp -> RoundingMode -> SymReal sym -> IO (SymFloat sym fpp)

Convert a real number to a floating point number.

floatToBV :: 1 <= w => sym -> NatRepr w -> RoundingMode -> SymFloat sym fpp -> IO (SymBV sym w)

Convert a floating point number to a unsigned bitvector.

floatToSBV :: 1 <= w => sym -> NatRepr w -> RoundingMode -> SymFloat sym fpp -> IO (SymBV sym w)

Convert a floating point number to a signed bitvector.

floatToReal :: sym -> SymFloat sym fpp -> IO (SymReal sym)

Convert a floating point number to a real number.

mkComplex :: sym -> Complex (SymReal sym) -> IO (SymCplx sym)

Create a complex from cartesian coordinates.

getRealPart :: sym -> SymCplx sym -> IO (SymReal sym)

getRealPart x returns the real part of x.

getImagPart :: sym -> SymCplx sym -> IO (SymReal sym)

getImagPart x returns the imaginary part of x.

cplxGetParts :: sym -> SymCplx sym -> IO (Complex (SymReal sym))

Convert a complex number into the real and imaginary part.

mkComplexLit :: sym -> Complex Rational -> IO (SymCplx sym)

Create a constant complex literal.

cplxFromReal :: sym -> SymReal sym -> IO (SymCplx sym)

Create a complex from a real value.

cplxIte :: sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)

If-then-else on complex values.

cplxNeg :: sym -> SymCplx sym -> IO (SymCplx sym)

Negate a complex number.

cplxAdd :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)

Add two complex numbers together.

cplxSub :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)

Subtract one complex number from another.

cplxMul :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)

Multiply two complex numbers together.

cplxMag :: sym -> SymCplx sym -> IO (SymReal sym)

Compute the magnitude of a complex number.

cplxSqrt :: sym -> SymCplx sym -> IO (SymCplx sym)

Return the principal square root of a complex number.

cplxSin :: sym -> SymCplx sym -> IO (SymCplx sym)

Compute sine of a complex number.

cplxCos :: sym -> SymCplx sym -> IO (SymCplx sym)

Compute cosine of a complex number.

cplxTan :: sym -> SymCplx sym -> IO (SymCplx sym)

Compute tangent of a complex number. cplxTan x is undefined when cplxCos x is 0, which occurs only along the real line in the same conditions where realCos x is 0.

cplxHypot :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)

hypotCplx x y returns sqrt(abs(x)^2 + abs(y)^2).

cplxRound :: sym -> SymCplx sym -> IO (SymCplx sym)

roundCplx x rounds complex number to nearest integer. Numbers with a fractional part of 0.5 are rounded away from 0. Imaginary and real parts are rounded independently.

cplxFloor :: sym -> SymCplx sym -> IO (SymCplx sym)

cplxFloor x rounds to nearest integer less than or equal to x. Imaginary and real parts are rounded independently.

cplxCeil :: sym -> SymCplx sym -> IO (SymCplx sym)

cplxCeil x rounds to nearest integer greater than or equal to x. Imaginary and real parts are rounded independently.

cplxConj :: sym -> SymCplx sym -> IO (SymCplx sym)

conjReal x returns the complex conjugate of the input.

cplxExp :: sym -> SymCplx sym -> IO (SymCplx sym)

Returns exponential of a complex number.

cplxEq :: sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)

Check equality of two complex numbers.

cplxNe :: sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)

Check non-equality of two complex numbers.

Instances

IsExprBuilder (ExprBuilder t st fs)

Defined in What4.Expr.Builder

Methods

getConfiguration :: ExprBuilder t st fs -> Config

setSolverLogListener :: ExprBuilder t st fs -> Maybe (SolverEvent -> IO ()) -> IO ()

getSolverLogListener :: ExprBuilder t st fs -> IO (Maybe (SolverEvent -> IO ()))

logSolverEvent :: ExprBuilder t st fs -> SolverEvent -> IO ()

getStatistics :: ExprBuilder t st fs -> IO Statistics

getCurrentProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc

setCurrentProgramLoc :: ExprBuilder t st fs -> ProgramLoc -> IO ()

isEq :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> SymExpr (ExprBuilder t st fs) tp -> IO (Pred (ExprBuilder t st fs))

baseTypeIte :: forall (tp :: BaseType). ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymExpr (ExprBuilder t st fs) tp -> SymExpr (ExprBuilder t st fs) tp -> IO (SymExpr (ExprBuilder t st fs) tp)

annotateTerm :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> IO (SymAnnotation (ExprBuilder t st fs) tp, SymExpr (ExprBuilder t st fs) tp)

getAnnotation :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> Maybe (SymAnnotation (ExprBuilder t st fs) tp)

truePred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs)

falsePred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs)

notPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

andPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

orPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

impliesPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

xorPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

eqPred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

itePred :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

intLit :: ExprBuilder t st fs -> Integer -> IO (SymInteger (ExprBuilder t st fs))

intNeg :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intAdd :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intSub :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intMul :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intMin :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intMax :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intEq :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

intLe :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

intLt :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

intAbs :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intDiv :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intMod :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

intDivisible :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> Natural -> IO (Pred (ExprBuilder t st fs))

bvLit :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w)

bvConcat :: forall (u :: Nat) (v :: Nat). (1 <= u, 1 <= v) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) u -> SymBV (ExprBuilder t st fs) v -> IO (SymBV (ExprBuilder t st fs) (u + v))

bvSelect :: forall (idx :: Nat) (n :: Nat) (w :: Nat). (1 <= n, (idx + n) <= w) => ExprBuilder t st fs -> NatRepr idx -> NatRepr n -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) n)

bvNeg :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvAdd :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvSub :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvMul :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvUdiv :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvUrem :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvSdiv :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvSrem :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

testBitBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> Natural -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvIsNeg :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvIte :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvEq :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvNe :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvUlt :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvUle :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvUge :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvUgt :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvSlt :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvSgt :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvSle :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvSge :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvIsNonzero :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs))

bvShl :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvLshr :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvAshr :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvRol :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvRor :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvZext :: forall (u :: Nat) (r :: Nat). (1 <= u, (u + 1) <= r) => ExprBuilder t st fs -> NatRepr r -> SymBV (ExprBuilder t st fs) u -> IO (SymBV (ExprBuilder t st fs) r)

bvSext :: forall (u :: Nat) (r :: Nat). (1 <= u, (u + 1) <= r) => ExprBuilder t st fs -> NatRepr r -> SymBV (ExprBuilder t st fs) u -> IO (SymBV (ExprBuilder t st fs) r)

bvTrunc :: forall (r :: Nat) (w :: Nat). (1 <= r, (r + 1) <= w) => ExprBuilder t st fs -> NatRepr r -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) r)

bvAndBits :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvOrBits :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvXorBits :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvNotBits :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvSet :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> Natural -> Pred (ExprBuilder t st fs) -> IO (SymBV (ExprBuilder t st fs) w)

bvFill :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> NatRepr w -> Pred (ExprBuilder t st fs) -> IO (SymBV (ExprBuilder t st fs) w)

minUnsignedBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

maxUnsignedBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

maxSignedBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

minSignedBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

bvPopcount :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvCountLeadingZeros :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

bvCountTrailingZeros :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w)

addUnsignedOF :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w)

addSignedOF :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w)

subUnsignedOF :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w)

subSignedOF :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w)

carrylessMultiply :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) (w + w))

unsignedWideMultiplyBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w, SymBV (ExprBuilder t st fs) w)

mulUnsignedOF :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w)

signedWideMultiplyBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w, SymBV (ExprBuilder t st fs) w)

mulSignedOF :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs), SymBV (ExprBuilder t st fs) w)

mkStruct :: forall (flds :: Ctx BaseType). ExprBuilder t st fs -> Assignment (SymExpr (ExprBuilder t st fs)) flds -> IO (SymStruct (ExprBuilder t st fs) flds)

structField :: forall (flds :: Ctx BaseType) (tp :: BaseType). ExprBuilder t st fs -> SymStruct (ExprBuilder t st fs) flds -> Index flds tp -> IO (SymExpr (ExprBuilder t st fs) tp)

structEq :: forall (flds :: Ctx BaseType). ExprBuilder t st fs -> SymStruct (ExprBuilder t st fs) flds -> SymStruct (ExprBuilder t st fs) flds -> IO (Pred (ExprBuilder t st fs))

structIte :: forall (flds :: Ctx BaseType). ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymStruct (ExprBuilder t st fs) flds -> SymStruct (ExprBuilder t st fs) flds -> IO (SymStruct (ExprBuilder t st fs) flds)

constantArray :: forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType). ExprBuilder t st fs -> Assignment BaseTypeRepr (idx ::> tp) -> SymExpr (ExprBuilder t st fs) b -> IO (SymArray (ExprBuilder t st fs) (idx ::> tp) b)

arrayFromFn :: forall (idx :: Ctx BaseType) (itp :: BaseType) (ret :: BaseType). ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) (idx ::> itp) ret -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) ret)

arrayMap :: forall (ctx :: Ctx BaseType) (d :: BaseType) (r :: BaseType) (idx :: Ctx BaseType) (itp :: BaseType). ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) (ctx ::> d) r -> Assignment (ArrayResultWrapper (SymExpr (ExprBuilder t st fs)) (idx ::> itp)) (ctx ::> d) -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) r)

arrayUpdate :: forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType). ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (idx ::> tp) b -> Assignment (SymExpr (ExprBuilder t st fs)) (idx ::> tp) -> SymExpr (ExprBuilder t st fs) b -> IO (SymArray (ExprBuilder t st fs) (idx ::> tp) b)

arrayLookup :: forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType). ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (idx ::> tp) b -> Assignment (SymExpr (ExprBuilder t st fs)) (idx ::> tp) -> IO (SymExpr (ExprBuilder t st fs) b)

arrayFromMap :: forall (idx :: Ctx BaseType) (itp :: BaseType) (tp :: BaseType). ExprBuilder t st fs -> Assignment BaseTypeRepr (idx ::> itp) -> ArrayUpdateMap (SymExpr (ExprBuilder t st fs)) (idx ::> itp) tp -> SymExpr (ExprBuilder t st fs) tp -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) tp)

arrayUpdateAtIdxLits :: forall (idx :: Ctx BaseType) (itp :: BaseType) (tp :: BaseType). ExprBuilder t st fs -> ArrayUpdateMap (SymExpr (ExprBuilder t st fs)) (idx ::> itp) tp -> SymArray (ExprBuilder t st fs) (idx ::> itp) tp -> IO (SymArray (ExprBuilder t st fs) (idx ::> itp) tp)

arrayIte :: forall (idx :: Ctx BaseType) (b :: BaseType). ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymArray (ExprBuilder t st fs) idx b -> SymArray (ExprBuilder t st fs) idx b -> IO (SymArray (ExprBuilder t st fs) idx b)

arrayEq :: forall (idx :: Ctx BaseType) (b :: BaseType). ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) idx b -> SymArray (ExprBuilder t st fs) idx b -> IO (Pred (ExprBuilder t st fs))

allTrueEntries :: forall (idx :: Ctx BaseType). ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) idx BaseBoolType -> IO (Pred (ExprBuilder t st fs))

arrayTrueOnEntries :: forall (idx :: Ctx BaseType) (itp :: BaseType). ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) (idx ::> itp) BaseBoolType -> SymArray (ExprBuilder t st fs) (idx ::> itp) BaseBoolType -> IO (Pred (ExprBuilder t st fs))

integerToReal :: ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

bvToInteger :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymInteger (ExprBuilder t st fs))

sbvToInteger :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymInteger (ExprBuilder t st fs))

predToBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

uintToReal :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymReal (ExprBuilder t st fs))

sbvToReal :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymReal (ExprBuilder t st fs))

realRound :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

realRoundEven :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

realFloor :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

realCeil :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

realTrunc :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

integerToBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

realToInteger :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

realToBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

realToSBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

clampedIntToSBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

clampedIntToBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SymInteger (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w)

intSetWidth :: forall (m :: Nat) (n :: Nat). (1 <= m, 1 <= n) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) m -> NatRepr n -> IO (SymBV (ExprBuilder t st fs) n)

uintSetWidth :: forall (m :: Nat) (n :: Nat). (1 <= m, 1 <= n) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) m -> NatRepr n -> IO (SymBV (ExprBuilder t st fs) n)

intToUInt :: forall (m :: Nat) (n :: Nat). (1 <= m, 1 <= n) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) m -> NatRepr n -> IO (SymBV (ExprBuilder t st fs) n)

uintToInt :: forall (m :: Nat) (n :: Nat). (1 <= m, 1 <= n) => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) m -> NatRepr n -> IO (SymBV (ExprBuilder t st fs) n)

stringEmpty :: forall (si :: StringInfo). ExprBuilder t st fs -> StringInfoRepr si -> IO (SymString (ExprBuilder t st fs) si)

stringLit :: forall (si :: StringInfo). ExprBuilder t st fs -> StringLiteral si -> IO (SymString (ExprBuilder t st fs) si)

stringEq :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs))

stringIte :: forall (si :: StringInfo). ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (SymString (ExprBuilder t st fs) si)

stringConcat :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (SymString (ExprBuilder t st fs) si)

stringContains :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs))

stringIsPrefixOf :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs))

stringIsSuffixOf :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> IO (Pred (ExprBuilder t st fs))

stringIndexOf :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymString (ExprBuilder t st fs) si -> SymInteger (ExprBuilder t st fs) -> IO (SymInteger (ExprBuilder t st fs))

stringLength :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> IO (SymInteger (ExprBuilder t st fs))

stringSubstring :: forall (si :: StringInfo). ExprBuilder t st fs -> SymString (ExprBuilder t st fs) si -> SymInteger (ExprBuilder t st fs) -> SymInteger (ExprBuilder t st fs) -> IO (SymString (ExprBuilder t st fs) si)

realZero :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs)

realLit :: ExprBuilder t st fs -> Rational -> IO (SymReal (ExprBuilder t st fs))

sciLit :: ExprBuilder t st fs -> Scientific -> IO (SymReal (ExprBuilder t st fs))

realEq :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

realNe :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

realLe :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

realLt :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

realGe :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

realGt :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

realIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realMin :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realMax :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realNeg :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realAdd :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realMul :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realSub :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realSq :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realDiv :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realMod :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

isInteger :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

realIsNonNeg :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

realSqrt :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realAtan2 :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realPi :: ExprBuilder t st fs -> IO (SymReal (ExprBuilder t st fs))

realLog :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realExp :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realSin :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realCos :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realTan :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realSinh :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realCosh :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realTanh :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realAbs :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

realHypot :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

floatPZero :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatNZero :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatNaN :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatPInf :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatNInf :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatLitRational :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatLit :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatNeg :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatAbs :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatSqrt :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatAdd :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatSub :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatMul :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatDiv :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatRem :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatMin :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatMax :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatFMA :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatEq :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatNe :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatFpEq :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatFpApart :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatFpUnordered :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatLe :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatLt :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatGe :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatGt :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatIsNaN :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatIsInf :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatIsZero :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatIsPos :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatIsNeg :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatIsSubnorm :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatIsNorm :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (Pred (ExprBuilder t st fs))

floatIte :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymFloat (ExprBuilder t st fs) fpp -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatCast :: forall (fpp :: FloatPrecision) (fpp' :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp' -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatRound :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatFromBinary :: forall (eb :: Nat) (sb :: Nat). (2 <= eb, 2 <= sb) => ExprBuilder t st fs -> FloatPrecisionRepr (FloatingPointPrecision eb sb) -> SymBV (ExprBuilder t st fs) (eb + sb) -> IO (SymFloat (ExprBuilder t st fs) (FloatingPointPrecision eb sb))

floatToBinary :: forall (eb :: Nat) (sb :: Nat). (2 <= eb, 2 <= sb) => ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) (FloatingPointPrecision eb sb) -> IO (SymBV (ExprBuilder t st fs) (eb + sb))

bvToFloat :: forall (w :: Nat) (fpp :: FloatPrecision). 1 <= w => ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV (ExprBuilder t st fs) w -> IO (SymFloat (ExprBuilder t st fs) fpp)

sbvToFloat :: forall (w :: Nat) (fpp :: FloatPrecision). 1 <= w => ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV (ExprBuilder t st fs) w -> IO (SymFloat (ExprBuilder t st fs) fpp)

realToFloat :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> RoundingMode -> SymReal (ExprBuilder t st fs) -> IO (SymFloat (ExprBuilder t st fs) fpp)

floatToBV :: forall (w :: Nat) (fpp :: FloatPrecision). 1 <= w => ExprBuilder t st fs -> NatRepr w -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymBV (ExprBuilder t st fs) w)

floatToSBV :: forall (w :: Nat) (fpp :: FloatPrecision). 1 <= w => ExprBuilder t st fs -> NatRepr w -> RoundingMode -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymBV (ExprBuilder t st fs) w)

floatToReal :: forall (fpp :: FloatPrecision). ExprBuilder t st fs -> SymFloat (ExprBuilder t st fs) fpp -> IO (SymReal (ExprBuilder t st fs))

mkComplex :: ExprBuilder t st fs -> Complex (SymReal (ExprBuilder t st fs)) -> IO (SymCplx (ExprBuilder t st fs))

getRealPart :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

getImagPart :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

cplxGetParts :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (Complex (SymReal (ExprBuilder t st fs)))

mkComplexLit :: ExprBuilder t st fs -> Complex Rational -> IO (SymCplx (ExprBuilder t st fs))

cplxFromReal :: ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxIte :: ExprBuilder t st fs -> Pred (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxNeg :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxAdd :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxSub :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxMul :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxMag :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs))

cplxSqrt :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxSin :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxCos :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxTan :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxHypot :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxRound :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxFloor :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxCeil :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxConj :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxExp :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> IO (SymCplx (ExprBuilder t st fs))

cplxEq :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

cplxNe :: ExprBuilder t st fs -> SymCplx (ExprBuilder t st fs) -> SymCplx (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

class (IsExprBuilder sym, IsSymFn (SymFn sym), OrdF (SymExpr sym)) => IsSymExprBuilder sym where

This extends the interface for building expressions with operations for creating new symbolic constants and functions.

Minimal complete definition

freshConstant, freshLatch, freshBoundedBV, freshBoundedSBV, freshBoundedInt, freshBoundedReal, freshBoundVar, varExpr, forallPred, existsPred, definedFn, freshTotalUninterpFn, applySymFn

Methods

freshConstant :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)

Create a fresh top-level uninterpreted constant.

freshLatch :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)

Create a fresh latch variable.

freshBoundedBV

Arguments

:: 1 <= w

=> sym

-> SolverSymbol

-> NatRepr w

-> Maybe Natural

lower bound

-> Maybe Natural

upper bound

-> IO (SymBV sym w)

Create a fresh bitvector value with optional lower and upper bounds (which bound the unsigned value of the bitvector). If provided, the bounds are inclusive. If inconsistent or out-of-range bounds are given, an InvalidRange exception will be thrown.

freshBoundedSBV

Arguments

:: 1 <= w

=> sym

-> SolverSymbol

-> NatRepr w

-> Maybe Integer

lower bound

-> Maybe Integer

upper bound

-> IO (SymBV sym w)

Create a fresh bitvector value with optional lower and upper bounds (which bound the signed value of the bitvector). If provided, the bounds are inclusive. If inconsistent or out-of-range bounds are given, an InvalidRange exception will be thrown.

freshBoundedInt

Arguments

:: sym

-> SolverSymbol

-> Maybe Integer

lower bound

-> Maybe Integer

upper bound

-> IO (SymInteger sym)

Create a fresh integer constant with optional lower and upper bounds. If provided, the bounds are inclusive. If inconsistent bounds are given, an InvalidRange exception will be thrown.

freshBoundedReal

Arguments

:: sym

-> SolverSymbol

-> Maybe Rational

lower bound

-> Maybe Rational

upper bound

-> IO (SymReal sym)

Create a fresh real constant with optional lower and upper bounds. If provided, the bounds are inclusive. If inconsistent bounds are given, an InvalidRange exception will be thrown.

freshBoundVar :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)

Creates a bound variable.

This will be treated as a free constant when appearing inside asserted expressions. These are intended to be bound using quantifiers or symbolic functions.

varExpr :: sym -> BoundVar sym tp -> SymExpr sym tp

Return an expression that references the bound variable.

forallPred :: sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)

forallPred sym v e returns an expression that represents forall v . e. Throws a user error if bound var has already been used in a quantifier.

existsPred :: sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)

existsPred sym v e returns an expression that represents exists v . e. Throws a user error if bound var has already been used in a quantifier.

definedFn

Arguments

:: sym

Symbolic interface

-> SolverSymbol

The name to give a function (need not be unique)

-> Assignment (BoundVar sym) args

Bound variables to use as arguments for function.

-> SymExpr sym ret

Operation defining result of defined function.

-> UnfoldPolicy

Policy for unfolding on applications

-> IO (SymFn sym args ret)

Return a function defined by an expression over bound variables. The predicate argument allows the user to specify when an application of the function should be unfolded and evaluated, e.g. to perform constant folding.

inlineDefineFun

Arguments

:: CurryAssignmentClass args

=> sym

Symbolic interface

-> SolverSymbol

The name to give a function (need not be unique)

-> Assignment BaseTypeRepr args

Type signature for the arguments

-> UnfoldPolicy

Policy for unfolding on applications

-> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))

Operation defining result of defined function.

-> IO (SymFn sym args ret)

Return a function defined by Haskell computation over symbolic expressions.

freshTotalUninterpFn

Arguments

:: forall args ret. sym

Symbolic interface

-> SolverSymbol

The name to give a function (need not be unique)

-> Assignment BaseTypeRepr args

Types of arguments expected by function

-> BaseTypeRepr ret

Return type of function

-> IO (SymFn sym args ret)

Create a new uninterpreted function.

applySymFn

Arguments

:: sym

Symbolic interface

-> SymFn sym args ret

Function to call

-> Assignment (SymExpr sym) args

Arguments to function

-> IO (SymExpr sym ret)

Apply a set of arguments to a symbolic function.

Instances

IsSymExprBuilder (ExprBuilder t st fs)

Defined in What4.Expr.Builder

Methods

freshConstant :: forall (tp :: BaseType). ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr (ExprBuilder t st fs) tp)

freshLatch :: forall (tp :: BaseType). ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr (ExprBuilder t st fs) tp)

freshBoundedBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SolverSymbol -> NatRepr w -> Maybe Natural -> Maybe Natural -> IO (SymBV (ExprBuilder t st fs) w)

freshBoundedSBV :: forall (w :: Nat). 1 <= w => ExprBuilder t st fs -> SolverSymbol -> NatRepr w -> Maybe Integer -> Maybe Integer -> IO (SymBV (ExprBuilder t st fs) w)

freshBoundedInt :: ExprBuilder t st fs -> SolverSymbol -> Maybe Integer -> Maybe Integer -> IO (SymInteger (ExprBuilder t st fs))

freshBoundedReal :: ExprBuilder t st fs -> SolverSymbol -> Maybe Rational -> Maybe Rational -> IO (SymReal (ExprBuilder t st fs))

freshBoundVar :: forall (tp :: BaseType). ExprBuilder t st fs -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar (ExprBuilder t st fs) tp)

varExpr :: forall (tp :: BaseType). ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> SymExpr (ExprBuilder t st fs) tp

forallPred :: forall (tp :: BaseType). ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

existsPred :: forall (tp :: BaseType). ExprBuilder t st fs -> BoundVar (ExprBuilder t st fs) tp -> Pred (ExprBuilder t st fs) -> IO (Pred (ExprBuilder t st fs))

definedFn :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprBuilder t st fs -> SolverSymbol -> Assignment (BoundVar (ExprBuilder t st fs)) args -> SymExpr (ExprBuilder t st fs) ret -> UnfoldPolicy -> IO (SymFn (ExprBuilder t st fs) args ret)

inlineDefineFun :: forall (args :: Ctx BaseType) (ret :: BaseType). CurryAssignmentClass args => ExprBuilder t st fs -> SolverSymbol -> Assignment BaseTypeRepr args -> UnfoldPolicy -> CurryAssignment args (SymExpr (ExprBuilder t st fs)) (IO (SymExpr (ExprBuilder t st fs) ret)) -> IO (SymFn (ExprBuilder t st fs) args ret)

freshTotalUninterpFn :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprBuilder t st fs -> SolverSymbol -> Assignment BaseTypeRepr args -> BaseTypeRepr ret -> IO (SymFn (ExprBuilder t st fs) args ret)

applySymFn :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprBuilder t st fs -> SymFn (ExprBuilder t st fs) args ret -> Assignment (SymExpr (ExprBuilder t st fs)) args -> IO (SymExpr (ExprBuilder t st fs) ret)

data SolverEvent

This datatype describes events that involve interacting with solvers. A SolverEvent will be provided to the action installed via setSolverLogListener whenever an interesting event occurs.

Constructors

SolverStartSATQuery

Fields

• satQuerySolverName :: !String
• satQueryReason :: !String

SolverEndSATQuery

Fields

• satQueryResult :: !(SatResult () ())
• satQueryError :: !(Maybe String)

Instances

Show SolverEvent

Defined in What4.Interface

Methods

showsPrec :: Int -> SolverEvent -> ShowS

show :: SolverEvent -> String

showList :: [SolverEvent] -> ShowS

Generic SolverEvent

Defined in What4.Interface

Associated Types

type Rep SolverEvent :: Type -> Type

Methods

from :: SolverEvent -> Rep SolverEvent x

to :: Rep SolverEvent x -> SolverEvent

type Rep SolverEvent

Defined in What4.Interface

type Rep SolverEvent = D1 ('MetaData "SolverEvent" "What4.Interface" "what4-1.1-F6JmVDCUG2e4tsAmUzrLc2" 'False) (C1 ('MetaCons "SolverStartSATQuery" 'PrefixI 'True) (S1 ('MetaSel ('Just "satQuerySolverName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String) :*: S1 ('MetaSel ('Just "satQueryReason") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String)) :+: C1 ('MetaCons "SolverEndSATQuery" 'PrefixI 'True) (S1 ('MetaSel ('Just "satQueryResult") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SatResult () ())) :*: S1 ('MetaSel ('Just "satQueryError") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe String))))

Bitvector operations

bvJoinVector :: forall sym n w. (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> Vector n (SymBV sym w) -> IO (SymBV sym (n * w))

Join a Vector of smaller bitvectors. The vector is interpreted in big endian order; that is, with most significant bitvector first.

bvSplitVector :: forall sym n w. (IsExprBuilder sym, 1 <= w, 1 <= n) => sym -> NatRepr n -> NatRepr w -> SymBV sym (n * w) -> IO (Vector n (SymBV sym w))

Split a bitvector to a Vector of smaller bitvectors. The returned vector is in big endian order; that is, with most significant bitvector first.

bvSwap

Arguments

:: forall sym n. (1 <= n, IsExprBuilder sym)

=> sym

Symbolic interface

-> NatRepr n

-> SymBV sym (n * 8)

Bitvector to swap around

-> IO (SymBV sym (n * 8))

Implement LLVM's "bswap" intrinsic

See <https://llvm.org/docs/LangRef.html#llvm-bswap-intrinsics the LLVM bswap documentation.>

This is the implementation in SawCore:

llvmBSwap :: (n :: Nat) -> bitvector (mulNat n 8) -> bitvector (mulNat n 8);
llvmBSwap n x = join n 8 Bool (reverse n (bitvector 8) (split n 8 Bool x));

bvBitreverse :: forall sym w. (1 <= w, IsExprBuilder sym) => sym -> SymBV sym w -> IO (SymBV sym w)

Swap the order of the bits in a bitvector.

Floating-point rounding modes

data RoundingMode

Rounding modes for IEEE-754 floating point operations.

Constructors

RNE

Round to nearest even.

RNA

Round to nearest away.

RTP

Round toward plus Infinity.

RTN

Round toward minus Infinity.

RTZ

Round toward zero.

Instances

Enum RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

succ :: RoundingMode -> RoundingMode

pred :: RoundingMode -> RoundingMode

toEnum :: Int -> RoundingMode

fromEnum :: RoundingMode -> Int

enumFrom :: RoundingMode -> [RoundingMode]

enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]

enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]

enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]

Eq RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

(==) :: RoundingMode -> RoundingMode -> Bool

(/=) :: RoundingMode -> RoundingMode -> Bool

Ord RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

compare :: RoundingMode -> RoundingMode -> Ordering

(<) :: RoundingMode -> RoundingMode -> Bool

(<=) :: RoundingMode -> RoundingMode -> Bool

(>) :: RoundingMode -> RoundingMode -> Bool

(>=) :: RoundingMode -> RoundingMode -> Bool

max :: RoundingMode -> RoundingMode -> RoundingMode

min :: RoundingMode -> RoundingMode -> RoundingMode

Show RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

showsPrec :: Int -> RoundingMode -> ShowS

show :: RoundingMode -> String

showList :: [RoundingMode] -> ShowS

Generic RoundingMode

Defined in What4.Utils.FloatHelpers

Associated Types

type Rep RoundingMode :: Type -> Type

Methods

from :: RoundingMode -> Rep RoundingMode x

to :: Rep RoundingMode x -> RoundingMode

Hashable RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

hashWithSalt :: Int -> RoundingMode -> Int

hash :: RoundingMode -> Int

type Rep RoundingMode

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.1-F6JmVDCUG2e4tsAmUzrLc2" 'False) ((C1 ('MetaCons "RNE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RNA" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTP" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RTN" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RTZ" 'PrefixI 'False) (U1 :: Type -> Type))))

Run-time statistics

data Statistics

Statistics gathered on a running expression builder. See getStatistics.

Constructors

Statistics

Fields

• statAllocs :: !Integer

  The number of times an expression node has been allocated.

• statNonLinearOps :: !Integer

  The number of non-linear operations, such as multiplications, that have occurred.

Instances

Show Statistics

Defined in What4.Interface

Methods

showsPrec :: Int -> Statistics -> ShowS

show :: Statistics -> String

showList :: [Statistics] -> ShowS

zeroStatistics :: Statistics

Type Aliases

type Pred sym = SymExpr sym BaseBoolType

Symbolic boolean values, AKA predicates.

type SymInteger sym = SymExpr sym BaseIntegerType

Symbolic integers.

type SymReal sym = SymExpr sym BaseRealType

Symbolic real numbers.

type SymFloat sym fpp = SymExpr sym (BaseFloatType fpp)

Symbolic floating point numbers.

type SymString sym si = SymExpr sym (BaseStringType si)

Symbolic strings.

type SymCplx sym = SymExpr sym BaseComplexType

Symbolic complex numbers.

type SymStruct sym flds = SymExpr sym (BaseStructType flds)

Symbolic structures.

type SymBV sym n = SymExpr sym (BaseBVType n)

Symbolic bitvectors.

type SymArray sym idx b = SymExpr sym (BaseArrayType idx b)

Symbolic arrays.

Natural numbers

data SymNat sym

Symbolic natural numbers.

Instances

TestEquality (SymExpr sym) => Eq (SymNat sym)

Defined in What4.Interface

Methods

(==) :: SymNat sym -> SymNat sym -> Bool

(/=) :: SymNat sym -> SymNat sym -> Bool

OrdF (SymExpr sym) => Ord (SymNat sym)

Defined in What4.Interface

Methods

compare :: SymNat sym -> SymNat sym -> Ordering

(<) :: SymNat sym -> SymNat sym -> Bool

(<=) :: SymNat sym -> SymNat sym -> Bool

(>) :: SymNat sym -> SymNat sym -> Bool

(>=) :: SymNat sym -> SymNat sym -> Bool

max :: SymNat sym -> SymNat sym -> SymNat sym

min :: SymNat sym -> SymNat sym -> SymNat sym

HashableF (SymExpr sym) => Hashable (SymNat sym)

Defined in What4.Interface

Methods

hashWithSalt :: Int -> SymNat sym -> Int

hash :: SymNat sym -> Int

asNat :: IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural

Return nat if this is a constant natural number.

natLit :: IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)

A natural number literal.

natAdd :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)

Add two natural numbers.

natSub :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)

Subtract one number from another.

The result is 0 if the subtraction would otherwise be negative.

natMul :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)

Multiply one number by another.

natDiv :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)

natDiv sym x y performs division on naturals.

The result is undefined if y equals 0.

natDiv and natMod satisfy the property that given

  d <- natDiv sym x y
  m <- natMod sym x y

and y > 0, we have that y * d + m = x and m < y.

natMod :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)

natMod sym x y returns x mod y.

See natDiv for a description of the properties the return value is expected to satisfy.

natIte :: IsExprBuilder sym => sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)

If-then-else applied to natural numbers.

natEq :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)

Equality predicate for natural numbers.

natLe :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)

natLe sym x y returns true if x <= y.

natLt :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)

natLt sym x y returns true if x < y.

natToInteger :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymInteger sym)

Convert a natural number to an integer.

bvToNat :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymNat sym)

Convert the unsigned value of a bitvector to a natural.

natToReal :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymReal sym)

Convert a natural number to a real number.

integerToNat :: IsExprBuilder sym => sym -> SymInteger sym -> IO (SymNat sym)

Convert an integer to a natural number.

For negative integers, the result is clamped to 0.

realToNat :: IsExprBuilder sym => sym -> SymReal sym -> IO (SymNat sym)

Convert a real number to a natural number.

The result is undefined if the given real number does not represent a natural number.

freshBoundedNat

Arguments

:: IsSymExprBuilder sym

=> sym

-> SolverSymbol

-> Maybe Natural

lower bound

-> Maybe Natural

upper bound

-> IO (SymNat sym)

Create a fresh natural number constant with optional lower and upper bounds. If provided, the bounds are inclusive. If inconsistent bounds are given, an InvalidRange exception will be thrown.

freshNat :: IsSymExprBuilder sym => sym -> SolverSymbol -> IO (SymNat sym)

Create a fresh natural number constant.

printSymNat :: IsExpr (SymExpr sym) => SymNat sym -> Doc ann

Array utility types

data IndexLit idx where

This represents a concrete index value, and is used for creating arrays.

Constructors

IntIndexLit :: !Integer -> IndexLit BaseIntegerType

BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w)

Instances

TestEquality IndexLit

Defined in What4.IndexLit

Methods

testEquality :: forall (a :: k) (b :: k). IndexLit a -> IndexLit b -> Maybe (a :~: b)

OrdF IndexLit

Defined in What4.IndexLit

Methods

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

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

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

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

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

ShowF IndexLit

Defined in What4.IndexLit

Methods

withShow :: forall p q (tp :: k) a. p IndexLit -> q tp -> (Show (IndexLit tp) => a) -> a

showF :: forall (tp :: k). IndexLit tp -> String

showsPrecF :: forall (tp :: k). Int -> IndexLit tp -> String -> String

HashableF IndexLit

Defined in What4.IndexLit

Methods

hashWithSaltF :: forall (tp :: k). Int -> IndexLit tp -> Int

hashF :: forall (tp :: k). IndexLit tp -> Int

Eq (IndexLit tp)

Defined in What4.IndexLit

Methods

(==) :: IndexLit tp -> IndexLit tp -> Bool

(/=) :: IndexLit tp -> IndexLit tp -> Bool

Show (IndexLit tp)

Defined in What4.IndexLit

Methods

showsPrec :: Int -> IndexLit tp -> ShowS

show :: IndexLit tp -> String

showList :: [IndexLit tp] -> ShowS

Hashable (IndexLit tp)

Defined in What4.IndexLit

Methods

hashWithSalt :: Int -> IndexLit tp -> Int

hash :: IndexLit tp -> Int

indexLit :: IsExprBuilder sym => sym -> IndexLit idx -> IO (SymExpr sym idx)

Create a literal from an IndexLit.

newtype ArrayResultWrapper f idx tp

Constructors

ArrayResultWrapper

Fields

• unwrapArrayResult :: f (BaseArrayType idx tp)

Instances

TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type)

Defined in What4.Interface

Methods

testEquality :: forall (a :: k) (b :: k). ArrayResultWrapper f idx a -> ArrayResultWrapper f idx b -> Maybe (a :~: b)

HashableF e => HashableF (ArrayResultWrapper e idx :: BaseType -> Type)

Defined in What4.Interface

Methods

hashWithSaltF :: forall (tp :: k). Int -> ArrayResultWrapper e idx tp -> Int

hashF :: forall (tp :: k). ArrayResultWrapper e idx tp -> Int

Concrete values

asConcrete :: IsExpr e => e tp -> Maybe (ConcreteVal tp)

Return a concrete representation of a value, if it is concrete.

concreteToSym :: IsExprBuilder sym => sym -> ConcreteVal tp -> IO (SymExpr sym tp)

Create a literal symbolic value from a concrete value.

baseIsConcrete :: forall e bt. IsExpr e => e bt -> Bool

This returns true if the value corresponds to a concrete value.

baseDefaultValue :: forall sym bt. IsExprBuilder sym => sym -> BaseTypeRepr bt -> IO (SymExpr sym bt)

Return some default value for each base type. For numeric types, this is 0; for booleans, false; for strings, the empty string. Structs are filled with default values for every field, default arrays are constant arrays of default values.

realExprAsInteger :: (IsExpr e, MonadFail m) => e BaseRealType -> m Integer

Return value as a constant integer if it exists.

rationalAsInteger :: MonadFail m => Rational -> m Integer

Return value as a constant integer if it exists.

cplxExprAsRational :: (MonadFail m, IsExpr e) => e BaseComplexType -> m Rational

Extract the value of a complex expression, which is assumed to be a constant real number. Fail if the number has nonzero imaginary component, or if it is not a constant.

cplxExprAsInteger :: (MonadFail m, IsExpr e) => e BaseComplexType -> m Integer

Return a complex value as a constant integer if it exists.

SymEncoder

data SymEncoder sym v tp

This provides an interface for converting between Haskell values and a solver representation.

Constructors

SymEncoder

Fields

• symEncoderType :: !(BaseTypeRepr tp)
• symFromExpr :: !(sym -> SymExpr sym tp -> IO v)
• symToExpr :: !(sym -> v -> IO (SymExpr sym tp))

Utility combinators

Boolean operations

backendPred :: IsExprBuilder sym => sym -> Bool -> Pred sym

Return predicate equivalent to a Boolean.

andAllOf :: IsExprBuilder sym => sym -> Fold s (Pred sym) -> s -> IO (Pred sym)

Compute the conjunction of a sequence of predicates.

orOneOf :: IsExprBuilder sym => sym -> Fold s (Pred sym) -> s -> IO (Pred sym)

Compute the disjunction of a sequence of predicates.

itePredM :: (IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m) => sym -> Pred sym -> m (Pred sym) -> m (Pred sym) -> m (Pred sym)

Perform an ite on a predicate lazily.

iteM :: IsExprBuilder sym => (sym -> Pred sym -> v -> v -> IO v) -> sym -> Pred sym -> IO v -> IO v -> IO v

A utility combinator for combining actions that build terms with ifthenelse. If the given predicate is concretely true or false only the corresponding "then" or "else" action is run; otherwise both actions are run and combined with the given "ite" action.

iteList :: IsExprBuilder sym => (sym -> Pred sym -> v -> v -> IO v) -> sym -> [(IO (Pred sym), IO v)] -> IO v -> IO v

An iterated sequence of ifthenelse operations. The list of predicates and "then" results is constructed as-needed. The "default" value represents the result of the expression if none of the predicates in the given list is true.

predToReal :: IsExprBuilder sym => sym -> Pred sym -> IO (SymReal sym)

Return 1 if the predicate is true; 0 otherwise.

Complex number operations

cplxDiv :: IsExprBuilder sym => sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)

Divide one number by another.

cplxDiv x y is undefined when y is 0.

cplxLog :: IsExprBuilder sym => sym -> SymCplx sym -> IO (SymCplx sym)

Returns the principal logarithm of the input value.

cplxLog x is undefined when x is 0, and has a cut discontinuity along the negative real line.

cplxLogBase

Arguments

:: IsExprBuilder sym

=> Rational

Base for the logarithm

-> sym

-> SymCplx sym

-> IO (SymCplx sym)

Returns logarithm of input at a given base.

cplxLogBase b x is undefined when x is 0.

mkRational :: IsExprBuilder sym => sym -> Rational -> IO (SymCplx sym)

Create a value from a rational.

mkReal :: (IsExprBuilder sym, Real a) => sym -> a -> IO (SymCplx sym)

Create a value from an integer.

isNonZero :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)

Return predicate that holds if value is non-zero.

isReal :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)

Return predicate that holds if imaginary part of number is zero.

Indexing

muxRange

Arguments

:: (IsExpr e, Monad m)

=> (Natural -> m (e BaseBoolType))

Returns predicate that holds if we have found the value we are looking for. It is assumed that the predicate must hold for a unique integer in the range.

-> (e BaseBoolType -> a -> a -> m a)

Ite function

-> (Natural -> m a)

Function for concrete values

-> Natural

Lower bound (inclusive)

-> Natural

Upper bound (inclusive)

-> m a

This function is used for selecting a value from among potential values in a range.

muxRange p ite f l h returns an expression denoting the value obtained from the value f i where i is the smallest value in the range [l..h] such that p i is true. If p i is true for no such value, then this returns the value f h.

Exceptions

data InvalidRange where

This exception is thrown if the user requests to make a bounded variable, but gives incoherent or out-of-range bounds.

Constructors

InvalidRange :: BaseTypeRepr bt -> Maybe (ConcreteValue bt) -> Maybe (ConcreteValue bt) -> InvalidRange

Instances

Show InvalidRange

Defined in What4.Interface

Methods

showsPrec :: Int -> InvalidRange -> ShowS

show :: InvalidRange -> String

showList :: [InvalidRange] -> ShowS

Exception InvalidRange

Defined in What4.Interface

Methods

toException :: InvalidRange -> SomeException

fromException :: SomeException -> Maybe InvalidRange

displayException :: InvalidRange -> String

Reexports

module Data.Parameterized.NatRepr

module What4.BaseTypes

class HasAbsValue f

A utility class for values that contain abstract values

Minimal complete definition

getAbsValue

Instances

HasAbsValue (Expr t)

Defined in What4.Expr.App

Methods

getAbsValue :: forall (tp :: BaseType). Expr t tp -> AbstractValue tp

HasAbsValue (Dummy :: BaseType -> Type)

Defined in What4.Expr.App

Methods

getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp

data SolverSymbol

This represents a name known to the solver.

We have three types of symbols:

• The empty symbol
• A user symbol
• A system symbol

A user symbol should consist of a letter followed by any combination of letters, digits, and underscore characters. It also cannot be a reserved word in Yices or SMTLIB.

A system symbol should start with a letter followed by any number of letter, digit, underscore or an exclamation mark characters. It must contain at least one exclamation mark to distinguish itself from user symbols.

Instances

Eq SolverSymbol

Defined in What4.Symbol

Methods

(==) :: SolverSymbol -> SolverSymbol -> Bool

(/=) :: SolverSymbol -> SolverSymbol -> Bool

Ord SolverSymbol

Defined in What4.Symbol

Methods

compare :: SolverSymbol -> SolverSymbol -> Ordering

(<) :: SolverSymbol -> SolverSymbol -> Bool

(<=) :: SolverSymbol -> SolverSymbol -> Bool

(>) :: SolverSymbol -> SolverSymbol -> Bool

(>=) :: SolverSymbol -> SolverSymbol -> Bool

max :: SolverSymbol -> SolverSymbol -> SolverSymbol

min :: SolverSymbol -> SolverSymbol -> SolverSymbol

Show SolverSymbol

Defined in What4.Symbol

Methods

showsPrec :: Int -> SolverSymbol -> ShowS

show :: SolverSymbol -> String

showList :: [SolverSymbol] -> ShowS

Hashable SolverSymbol

Defined in What4.Symbol

Methods

hashWithSalt :: Int -> SolverSymbol -> Int

hash :: SolverSymbol -> Int

emptySymbol :: SolverSymbol

Return the empty symbol.

userSymbol :: String -> Either SolverSymbolError SolverSymbol

This returns either a user symbol or the empty symbol if the string is empty.

safeSymbol :: String -> SolverSymbol

Attempts to create a user symbol from the given string. If this fails for some reason, the string is Z-encoded into a system symbol instead with the prefix "zenc!".

data ValueRange tp

Describes a range of values in a totally ordered set.

Constructors

SingleRange !tp

Indicates that range denotes a single value

MultiRange !(ValueBound tp) !(ValueBound tp)

Indicates that the number is somewhere between the given upper and lower bound.

data StringLiteral (si :: StringInfo) :: Type where

Constructors

UnicodeLiteral :: !Text -> StringLiteral Unicode

Char8Literal :: !ByteString -> StringLiteral Char8

Char16Literal :: !Word16String -> StringLiteral Char16

Instances

TestEquality StringLiteral

Defined in What4.Utils.StringLiteral

Methods

testEquality :: forall (a :: k) (b :: k). StringLiteral a -> StringLiteral b -> Maybe (a :~: b)

OrdF StringLiteral

Defined in What4.Utils.StringLiteral

Methods

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

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

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

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

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

ShowF StringLiteral

Defined in What4.Utils.StringLiteral

Methods

withShow :: forall p q (tp :: k) a. p StringLiteral -> q tp -> (Show (StringLiteral tp) => a) -> a

showF :: forall (tp :: k). StringLiteral tp -> String

showsPrecF :: forall (tp :: k). Int -> StringLiteral tp -> String -> String

HashableF StringLiteral

Defined in What4.Utils.StringLiteral

Methods

hashWithSaltF :: forall (tp :: k). Int -> StringLiteral tp -> Int

hashF :: forall (tp :: k). StringLiteral tp -> Int

Eq (StringLiteral si)

Defined in What4.Utils.StringLiteral

Methods

(==) :: StringLiteral si -> StringLiteral si -> Bool

(/=) :: StringLiteral si -> StringLiteral si -> Bool

Ord (StringLiteral si)

Defined in What4.Utils.StringLiteral

Methods

compare :: StringLiteral si -> StringLiteral si -> Ordering

(<) :: StringLiteral si -> StringLiteral si -> Bool

(<=) :: StringLiteral si -> StringLiteral si -> Bool

(>) :: StringLiteral si -> StringLiteral si -> Bool

(>=) :: StringLiteral si -> StringLiteral si -> Bool

max :: StringLiteral si -> StringLiteral si -> StringLiteral si

min :: StringLiteral si -> StringLiteral si -> StringLiteral si

Show (StringLiteral si)

Defined in What4.Utils.StringLiteral

Methods

showsPrec :: Int -> StringLiteral si -> ShowS

show :: StringLiteral si -> String

showList :: [StringLiteral si] -> ShowS

IsString (StringLiteral Unicode)

Defined in What4.Utils.StringLiteral

Methods

fromString :: String -> StringLiteral Unicode

Semigroup (StringLiteral si)

Defined in What4.Utils.StringLiteral

Methods

(<>) :: StringLiteral si -> StringLiteral si -> StringLiteral si

sconcat :: NonEmpty (StringLiteral si) -> StringLiteral si

stimes :: Integral b => b -> StringLiteral si -> StringLiteral si

Hashable (StringLiteral si)

Defined in What4.Utils.StringLiteral

Methods

hashWithSalt :: Int -> StringLiteral si -> Int

hash :: StringLiteral si -> Int

stringLiteralInfo :: StringLiteral si -> StringInfoRepr si