what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2014-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.Interface

Description

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.

Synopsis

Interface classes

Type Families

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

The class for expressions.

Instances

Instances details
type SymExpr (ExprBuilder t st fs) Source # 
Instance details

Defined in What4.Expr.Builder

type SymExpr (ExprBuilder t st fs) = Expr t

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

Type of bound variable associated with symbolic state.

This type is used by some methods in class IsSymExprBuilder.

Instances

Instances details
type BoundVar (ExprBuilder t st fs) Source # 
Instance details

Defined in What4.Expr.Builder

type BoundVar (ExprBuilder t st fs) = ExprBoundVar t

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

A function that can be applied to symbolic arguments.

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

Instances

Instances details
type SymFn (ExprBuilder t st fs) Source # 
Instance details

Defined in What4.Expr.Builder

type SymFn (ExprBuilder t st fs) = ExprSymFn t

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

Type used to uniquely identify expressions that have been annotated.

Instances

Instances details
type SymAnnotation (ExprBuilder t st fs) Source # 
Instance details

Defined in What4.Expr.Builder

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

Expression recognizers

class HasAbsValue e => IsExpr e where Source #

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.

Methods

asConstantPred :: e BaseBoolType -> Maybe Bool Source #

Evaluate if predicate is constant.

asInteger :: e BaseIntegerType -> Maybe Integer Source #

Return integer if this is a constant integer.

integerBounds :: e BaseIntegerType -> ValueRange Integer Source #

Return any bounding information we have about the term

asRational :: e BaseRealType -> Maybe Rational Source #

Return rational if this is a constant value.

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

Return floating-point value if this is a constant

rationalBounds :: e BaseRealType -> ValueRange Rational Source #

Return any bounding information we have about the term

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

Return complex if this is a constant value.

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

Return a bitvector if this is a constant bitvector.

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

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

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

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

Return the string value if this is a constant string

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

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

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

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

Return the struct fields if this is a concrete struct.

exprType :: e tp -> BaseTypeRepr tp Source #

Get type of expression.

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

Get the width of a bitvector

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

Get the precision of a floating-point expression

printSymExpr :: e tp -> Doc ann Source #

Print a sym expression for debugging or display purposes.

Instances

Instances details
IsExpr (Expr t) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

class IsSymFn fn where Source #

A class for extracting type representatives from symbolic functions

Methods

fnArgTypes :: fn args ret -> Assignment BaseTypeRepr args Source #

Get the argument types of a function.

fnReturnType :: fn args ret -> BaseTypeRepr ret Source #

Get the return type of a function.

Instances

Instances details
IsSymFn (ExprSymFn t) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

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

data UnfoldPolicy Source #

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.

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

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

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

Retrieve the configuration object corresponding to this solver interface.

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

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

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

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

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

getStatistics :: sym -> IO Statistics Source #

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

Get current location of program for term creation purposes.

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

Set current location of program for term creation purposes.

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

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

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

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

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

Constant true predicate

falsePred :: sym -> Pred sym Source #

Constant false predicate

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

Boolean negation

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

Boolean conjunction

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

Boolean disjunction

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

Boolean implication

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

Exclusive-or operation

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

Equality of boolean values

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

If-then-else on a predicate.

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

Create an integer literal.

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

Negate an integer.

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

Add two integers.

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

Subtract one integer from another.

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

Multiply one integer by another.

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

Return the minimum value of two integers.

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

Return the maximum value of two integers.

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

If-then-else applied to integers.

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

Integer equality.

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

Integer less-than-or-equal.

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

Integer less-than.

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

Compute the absolute value of an integer.

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

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

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

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

Create a bitvector with the given width and value.

bvConcat Source #

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

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

2's complement negation.

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

Add two bitvectors.

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

Subtract one bitvector from another.

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

Multiply one bitvector by another.

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

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

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

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

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

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

Return true if bitvector is negative.

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

If-then-else applied to bitvectors.

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

Return true if bitvectors are equal.

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

Return true if bitvectors are distinct.

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

Unsigned less-than.

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

Unsigned less-than-or-equal.

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

Unsigned greater-than-or-equal.

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

Unsigned greater-than.

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

Signed less-than.

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

Signed greater-than.

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

Signed less-than-or-equal.

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

Signed greater-than-or-equal.

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

returns true if the given bitvector is non-zero.

bvShl Source #

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

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

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

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

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

Zero-extend a bitvector.

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

Sign-extend a bitvector.

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

Truncate a bitvector.

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

Bitwise logical and.

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

Bitwise logical or.

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

Bitwise logical exclusive or.

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

Bitwise complement.

bvSet Source #

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

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

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

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

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

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

Return the number of 1 bits in the input.

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

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

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

Unsigned add with overflow bit.

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

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

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

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

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

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

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

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

Compute the signed multiply of two values with overflow bit.

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

Create a struct from an assignment of expressions.

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

Get the value of a specific field in a struct.

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

Check if two structs are equal.

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

Take the if-then-else of two structures.

constantArray Source #

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

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

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

Update an array at a specific location.

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

Return element in array.

arrayFromMap Source #

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

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

If-then-else applied to arrays.

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

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

Return true if all entries in the array are true.

arrayTrueOnEntries Source #

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

Convert an integer to a real number.

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

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

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

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

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

Return 1 if the predicate is true; 0 otherwise.

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

Convert an unsigned bitvector to a real number.

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

Convert an signed bitvector to a real number.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Create an empty string literal

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

Create a concrete string literal

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

Check the equality of two strings

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

If-then-else on strings

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

Concatenate two strings

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

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

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

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

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

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

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

Compute the length of a string

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

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

Return real number 0.

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

Create a constant real literal.

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

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

Check equality of two real numbers.

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

Check non-equality of two real numbers.

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

Check <= on two real numbers.

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

Check < on two real numbers.

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

Check >= on two real numbers.

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

Check > on two real numbers.

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

If-then-else on real numbers.

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

Return the minimum of two real numbers.

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

Return the maxmimum of two real numbers.

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

Negate a real number.

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

Add two real numbers.

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

Multiply two real numbers.

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

Subtract one real from another.

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

realSq sym x returns x * x.

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

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

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

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

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

Return true if the real is non-negative.

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

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

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

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

Return value denoting pi.

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

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

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

Natural exponentiation

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

Sine trig function

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

Cosine trig function

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

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

Hyperbolic sine

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

Hyperbolic cosine

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

Hyperbolic tangent

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

Return absolute value of the real number.

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

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

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

Return floating point number +0.

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

Return floating point number -0.

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

Return floating point NaN.

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

Return floating point +infinity.

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

Return floating point -infinity.

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

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

Create a floating point literal from a BigFloat value.

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

Negate a floating point number.

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

Return the absolute value of a floating point number.

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

Compute the square root of a floating point number.

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

Add two floating point numbers.

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

Subtract two floating point numbers.

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

Multiply two floating point numbers.

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

Divide two floating point numbers.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Test if a floating-point value is NaN.

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

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

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

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

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

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

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

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

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

Test if a floating-point value is subnormal.

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

Test if a floating-point value is normal.

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

If-then-else on floating point numbers.

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

Change the precision of a floating point number.

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

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

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

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

Convert a unsigned bitvector to a floating point number.

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

Convert a signed bitvector to a floating point number.

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

Convert a real number to a floating point number.

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

Convert a floating point number to a unsigned bitvector.

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

Convert a floating point number to a signed bitvector.

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

Convert a floating point number to a real number.

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

Create a complex from cartesian coordinates.

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

getRealPart x returns the real part of x.

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

getImagPart x returns the imaginary part of x.

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

Convert a complex number into the real and imaginary part.

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

Create a constant complex literal.

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

Create a complex from a real value.

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

If-then-else on complex values.

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

Negate a complex number.

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

Add two complex numbers together.

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

Subtract one complex number from another.

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

Multiply two complex numbers together.

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

Compute the magnitude of a complex number.

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

Return the principal square root of a complex number.

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

Compute sine of a complex number.

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

Compute cosine of a complex number.

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

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

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

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

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

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

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

conjReal x returns the complex conjugate of the input.

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

Returns exponential of a complex number.

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

Check equality of two complex numbers.

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

Check non-equality of two complex numbers.

Instances

Instances details
IsExprBuilder (ExprBuilder t st fs) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

getConfiguration :: ExprBuilder t st fs -> Config Source #

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

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

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

getStatistics :: ExprBuilder t st fs -> IO Statistics Source #

getCurrentProgramLoc :: ExprBuilder t st fs -> IO ProgramLoc Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Methods

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

Create a fresh top-level uninterpreted constant.

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

Create a fresh latch variable.

freshBoundedBV Source #

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

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

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

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

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

Return an expression that references the bound variable.

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

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

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

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

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

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

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

Instances details
IsSymExprBuilder (ExprBuilder t st fs) Source # 
Instance details

Defined in What4.Expr.Builder

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

data SolverEvent Source #

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.

Instances

Instances details
Show SolverEvent Source # 
Instance details

Defined in What4.Interface

Generic SolverEvent Source # 
Instance details

Defined in What4.Interface

Associated Types

type Rep SolverEvent :: Type -> Type #

type Rep SolverEvent Source # 
Instance details

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

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

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

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

Swap the order of the bits in a bitvector.

Floating-point rounding modes

data RoundingMode Source #

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

Instances details
Enum RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Eq RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Ord RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Show RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Generic RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Associated Types

type Rep RoundingMode :: Type -> Type #

Hashable RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode Source # 
Instance details

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

Statistics gathered on a running expression builder. See getStatistics.

Constructors

Statistics 

Fields

Instances

Instances details
Show Statistics Source # 
Instance details

Defined in What4.Interface

Type Aliases

type Pred sym = SymExpr sym BaseBoolType Source #

Symbolic boolean values, AKA predicates.

type SymInteger sym = SymExpr sym BaseIntegerType Source #

Symbolic integers.

type SymReal sym = SymExpr sym BaseRealType Source #

Symbolic real numbers.

type SymFloat sym fpp = SymExpr sym (BaseFloatType fpp) Source #

Symbolic floating point numbers.

type SymString sym si = SymExpr sym (BaseStringType si) Source #

Symbolic strings.

type SymCplx sym = SymExpr sym BaseComplexType Source #

Symbolic complex numbers.

type SymStruct sym flds = SymExpr sym (BaseStructType flds) Source #

Symbolic structures.

type SymBV sym n = SymExpr sym (BaseBVType n) Source #

Symbolic bitvectors.

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

Symbolic arrays.

Natural numbers

data SymNat sym Source #

Symbolic natural numbers.

Instances

Instances details
TestEquality (SymExpr sym) => Eq (SymNat sym) Source # 
Instance details

Defined in What4.Interface

Methods

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

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

OrdF (SymExpr sym) => Ord (SymNat sym) Source # 
Instance details

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) Source # 
Instance details

Defined in What4.Interface

Methods

hashWithSalt :: Int -> SymNat sym -> Int #

hash :: SymNat sym -> Int #

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

Return nat if this is a constant natural number.

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

A natural number literal.

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

Add two natural numbers.

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

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

Multiply one number by another.

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

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

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

If-then-else applied to natural numbers.

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

Equality predicate for natural numbers.

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

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

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

natLt sym x y returns true if x < y.

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

Convert a natural number to an integer.

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

Convert the unsigned value of a bitvector to a natural.

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

Convert a natural number to a real number.

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

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

Convert a real number to a natural number.

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

freshBoundedNat Source #

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

Create a fresh natural number constant.

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

Array utility types

data IndexLit idx where Source #

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

Constructors

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

Instances

Instances details
TestEquality IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

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

OrdF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

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

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

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

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

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

ShowF IndexLit Source # 
Instance details

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 Source # 
Instance details

Defined in What4.IndexLit

Methods

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

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

Eq (IndexLit tp) Source # 
Instance details

Defined in What4.IndexLit

Methods

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

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

Show (IndexLit tp) Source # 
Instance details

Defined in What4.IndexLit

Methods

showsPrec :: Int -> IndexLit tp -> ShowS #

show :: IndexLit tp -> String #

showList :: [IndexLit tp] -> ShowS #

Hashable (IndexLit tp) Source # 
Instance details

Defined in What4.IndexLit

Methods

hashWithSalt :: Int -> IndexLit tp -> Int #

hash :: IndexLit tp -> Int #

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

Create a literal from an IndexLit.

newtype ArrayResultWrapper f idx tp Source #

Constructors

ArrayResultWrapper 

Fields

Instances

Instances details
TestEquality f => TestEquality (ArrayResultWrapper f idx :: BaseType -> Type) Source # 
Instance details

Defined in What4.Interface

Methods

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

HashableF e => HashableF (ArrayResultWrapper e idx :: BaseType -> Type) Source # 
Instance details

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

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

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

Create a literal symbolic value from a concrete value.

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

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

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

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

Return value as a constant integer if it exists.

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

Return value as a constant integer if it exists.

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

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

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

SymEncoder

data SymEncoder sym v tp Source #

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

Constructors

SymEncoder 

Fields

Utility combinators

Boolean operations

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

Return predicate equivalent to a Boolean.

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

Compute the conjunction of a sequence of predicates.

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

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

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

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

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

Return 1 if the predicate is true; 0 otherwise.

Complex number operations

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

Divide one number by another.

cplxDiv x y is undefined when y is 0.

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

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

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

Create a value from a rational.

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

Create a value from an integer.

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

Return predicate that holds if value is non-zero.

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

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

Indexing

muxRange Source #

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

This exception is thrown if the user requests to make a bounded variable, but gives incoherent or out-of-range bounds.

Reexports

class HasAbsValue f Source #

A utility class for values that contain abstract values

Minimal complete definition

getAbsValue

Instances

Instances details
HasAbsValue (Expr t) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

HasAbsValue (Dummy :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp Source #

data SolverSymbol Source #

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.

emptySymbol :: SolverSymbol Source #

Return the empty symbol.

userSymbol :: String -> Either SolverSymbolError SolverSymbol Source #

This returns either a user symbol or the empty symbol if the string is empty.

safeSymbol :: String -> SolverSymbol Source #

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

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

Instances

Instances details
TestEquality StringLiteral Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

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

OrdF StringLiteral Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in What4.Utils.StringLiteral

Methods

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

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

Eq (StringLiteral si) Source # 
Instance details

Defined in What4.Utils.StringLiteral

Ord (StringLiteral si) Source # 
Instance details

Defined in What4.Utils.StringLiteral

Show (StringLiteral si) Source # 
Instance details

Defined in What4.Utils.StringLiteral

IsString (StringLiteral Unicode) Source # 
Instance details

Defined in What4.Utils.StringLiteral

Semigroup (StringLiteral si) Source # 
Instance details

Defined in What4.Utils.StringLiteral

Hashable (StringLiteral si) Source # 
Instance details

Defined in What4.Utils.StringLiteral