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

Copyright | (c) Galois Inc 2014-2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Interface

Contents

- Interface classes
  - Type Families
  - Expression recognizers
  - IsExprBuilder
  - Bitvector operations
  - Floating-point rounding modes
  - Run-time statistics
- Type Aliases
- Natural numbers
- Array utility types
- Concrete values
- SymEncoder
- Utility combinators
  - Boolean operations
  - Complex number operations
  - Indexing
- Exceptions
- Reexports

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)`
`instance `OrdF` (`BoundVar` sym)`
`instance `TestEquality` (`BoundVar` sym)`
`instance `HashableF` (`BoundVar` sym)`

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

Synopsis

- type family SymExpr (sym :: Type) :: BaseType -> Type
- type family BoundVar (sym :: Type) :: BaseType -> Type
- type family SymFn sym :: Ctx BaseType -> BaseType -> Type
- type family SymAnnotation (sym :: Type) :: BaseType -> Type
- class HasAbsValue e => IsExpr e where
  - asConstantPred :: e BaseBoolType -> Maybe Bool
  - asInteger :: e BaseIntegerType -> Maybe Integer
  - integerBounds :: e BaseIntegerType -> ValueRange Integer
  - asRational :: e BaseRealType -> Maybe Rational
  - asFloat :: e (BaseFloatType fpp) -> Maybe BigFloat
  - rationalBounds :: e BaseRealType -> ValueRange Rational
  - asComplex :: e BaseComplexType -> Maybe (Complex Rational)
  - asBV :: e (BaseBVType w) -> Maybe (BV w)
  - unsignedBVBounds :: 1 <= w => e (BaseBVType w) -> Maybe (Integer, Integer)
  - signedBVBounds :: 1 <= w => e (BaseBVType w) -> Maybe (Integer, Integer)
  - asAffineVar :: e tp -> Maybe (ConcreteVal tp, e tp, ConcreteVal tp)
  - asString :: e (BaseStringType si) -> Maybe (StringLiteral si)
  - stringInfo :: e (BaseStringType si) -> StringInfoRepr si
  - asConstantArray :: e (BaseArrayType idx bt) -> Maybe (e bt)
  - asStruct :: e (BaseStructType flds) -> Maybe (Assignment e flds)
  - exprType :: e tp -> BaseTypeRepr tp
  - bvWidth :: e (BaseBVType w) -> NatRepr w
  - floatPrecision :: e (BaseFloatType fpp) -> FloatPrecisionRepr fpp
  - printSymExpr :: e tp -> Doc ann
  - unsafeSetAbstractValue :: AbstractValue tp -> e tp -> e tp
- class IsSymFn (fn :: Ctx BaseType -> BaseType -> Type) where
  - fnArgTypes :: fn args ret -> Assignment BaseTypeRepr args
  - fnReturnType :: fn args ret -> BaseTypeRepr ret
  - fnTestEquality :: fn args1 ret1 -> fn args2 ret2 -> Maybe ((args1 ::> ret1) :~: (args2 ::> ret2))
  - fnCompare :: fn args1 ret1 -> fn args2 ret2 -> OrderingF (args1 ::> ret1) (args2 ::> ret2)
- data SomeSymFn sym = forall args ret. SomeSymFn (SymFn sym args ret)
- data SymFnWrapper sym ctx where
  - SymFnWrapper :: forall sym args ret. SymFn sym args ret -> SymFnWrapper sym (args ::> ret)
- data UnfoldPolicy
  - = NeverUnfold
  - | AlwaysUnfold
  - | UnfoldConcrete
- shouldUnfold :: IsExpr e => UnfoldPolicy -> Assignment e args -> Bool
- class (IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym), TestEquality (SymAnnotation sym), OrdF (SymAnnotation sym), HashableF (SymAnnotation sym)) => IsExprBuilder sym where
  - getConfiguration :: sym -> Config
  - setSolverLogListener :: sym -> Maybe (SolverEvent -> IO ()) -> IO ()
  - getSolverLogListener :: sym -> IO (Maybe (SolverEvent -> IO ()))
  - logSolverEvent :: sym -> SolverEvent -> IO ()
  - getStatistics :: sym -> IO Statistics
  - getCurrentProgramLoc :: sym -> IO ProgramLoc
  - setCurrentProgramLoc :: sym -> ProgramLoc -> IO ()
  - isEq :: sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
  - baseTypeIte :: sym -> Pred sym -> SymExpr sym tp -> SymExpr sym tp -> IO (SymExpr sym tp)
  - annotateTerm :: sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
  - getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)
  - getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp)
  - truePred :: sym -> Pred sym
  - falsePred :: sym -> Pred sym
  - notPred :: sym -> Pred sym -> IO (Pred sym)
  - andPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
  - orPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
  - impliesPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
  - xorPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
  - eqPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
  - itePred :: sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
  - intLit :: sym -> Integer -> IO (SymInteger sym)
  - intNeg :: sym -> SymInteger sym -> IO (SymInteger sym)
  - intAdd :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  - intSub :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  - intMul :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  - intMin :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  - intMax :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  - intIte :: sym -> Pred sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  - intEq :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
  - intLe :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
  - intLt :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
  - intAbs :: sym -> SymInteger sym -> IO (SymInteger sym)
  - intDiv :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  - intMod :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
  - intDivisible :: sym -> SymInteger sym -> Natural -> IO (Pred sym)
  - bvLit :: 1 <= w => sym -> NatRepr w -> BV w -> IO (SymBV sym w)
  - bvConcat :: (1 <= u, 1 <= v) => sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
  - bvSelect :: forall idx n w. (1 <= n, (idx + n) <= w) => sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
  - bvNeg :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)
  - bvAdd :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvSub :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvMul :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvUdiv :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvUrem :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvSdiv :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvSrem :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - testBitBV :: 1 <= w => sym -> Natural -> SymBV sym w -> IO (Pred sym)
  - bvIsNeg :: 1 <= w => sym -> SymBV sym w -> IO (Pred sym)
  - bvIte :: 1 <= w => sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvEq :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvNe :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvUlt :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvUle :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvUge :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvUgt :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvSlt :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvSgt :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvSle :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvSge :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - bvIsNonzero :: 1 <= w => sym -> SymBV sym w -> IO (Pred sym)
  - bvShl :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvLshr :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvAshr :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvRol :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvRor :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvZext :: (1 <= u, (u + 1) <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
  - bvSext :: (1 <= u, (u + 1) <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
  - bvTrunc :: (1 <= r, (r + 1) <= w) => sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
  - bvAndBits :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvOrBits :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvXorBits :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
  - bvNotBits :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)
  - bvSet :: forall w. 1 <= w => sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
  - bvFill :: forall w. 1 <= w => sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
  - minUnsignedBV :: 1 <= w => sym -> NatRepr w -> IO (SymBV sym w)
  - maxUnsignedBV :: 1 <= w => sym -> NatRepr w -> IO (SymBV sym w)
  - maxSignedBV :: 1 <= w => sym -> NatRepr w -> IO (SymBV sym w)
  - minSignedBV :: 1 <= w => sym -> NatRepr w -> IO (SymBV sym w)
  - bvPopcount :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)
  - bvCountLeadingZeros :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)
  - bvCountTrailingZeros :: 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)
  - addUnsignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
  - addSignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
  - subUnsignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
  - subSignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
  - carrylessMultiply :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym (w + w))
  - unsignedWideMultiplyBV :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
  - mulUnsignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
  - signedWideMultiplyBV :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w, SymBV sym w)
  - mulSignedOF :: 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
  - mkStruct :: sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
  - structField :: sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
  - structEq :: forall flds. sym -> SymStruct sym flds -> SymStruct sym flds -> IO (Pred sym)
  - structIte :: sym -> Pred sym -> SymStruct sym flds -> SymStruct sym flds -> IO (SymStruct sym flds)
  - constantArray :: sym -> Assignment BaseTypeRepr (idx ::> tp) -> SymExpr sym b -> IO (SymArray sym (idx ::> tp) b)
  - arrayFromFn :: sym -> SymFn sym (idx ::> itp) ret -> IO (SymArray sym (idx ::> itp) ret)
  - arrayMap :: sym -> SymFn sym (ctx ::> d) r -> Assignment (ArrayResultWrapper (SymExpr sym) (idx ::> itp)) (ctx ::> d) -> IO (SymArray sym (idx ::> itp) r)
  - arrayUpdate :: sym -> SymArray sym (idx ::> tp) b -> Assignment (SymExpr sym) (idx ::> tp) -> SymExpr sym b -> IO (SymArray sym (idx ::> tp) b)
  - arrayLookup :: sym -> SymArray sym (idx ::> tp) b -> Assignment (SymExpr sym) (idx ::> tp) -> IO (SymExpr sym b)
  - arrayCopy :: 1 <= w => sym -> SymArray sym (SingleCtx (BaseBVType w)) a -> SymBV sym w -> SymArray sym (SingleCtx (BaseBVType w)) a -> SymBV sym w -> SymBV sym w -> IO (SymArray sym (SingleCtx (BaseBVType w)) a)
  - arraySet :: 1 <= w => sym -> SymArray sym (SingleCtx (BaseBVType w)) a -> SymBV sym w -> SymExpr sym a -> SymBV sym w -> IO (SymArray sym (SingleCtx (BaseBVType w)) a)
  - arrayRangeEq :: 1 <= w => sym -> SymArray sym (SingleCtx (BaseBVType w)) a -> SymBV sym w -> SymArray sym (SingleCtx (BaseBVType w)) a -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
  - arrayFromMap :: sym -> Assignment BaseTypeRepr (idx ::> itp) -> ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp -> SymExpr sym tp -> IO (SymArray sym (idx ::> itp) tp)
  - arrayUpdateAtIdxLits :: sym -> ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp -> SymArray sym (idx ::> itp) tp -> IO (SymArray sym (idx ::> itp) tp)
  - arrayIte :: sym -> Pred sym -> SymArray sym idx b -> SymArray sym idx b -> IO (SymArray sym idx b)
  - arrayEq :: sym -> SymArray sym idx b -> SymArray sym idx b -> IO (Pred sym)
  - allTrueEntries :: sym -> SymArray sym idx BaseBoolType -> IO (Pred sym)
  - arrayTrueOnEntries :: sym -> SymFn sym (idx ::> itp) BaseBoolType -> SymArray sym (idx ::> itp) BaseBoolType -> IO (Pred sym)
  - integerToReal :: sym -> SymInteger sym -> IO (SymReal sym)
  - bvToInteger :: 1 <= w => sym -> SymBV sym w -> IO (SymInteger sym)
  - sbvToInteger :: 1 <= w => sym -> SymBV sym w -> IO (SymInteger sym)
  - predToBV :: 1 <= w => sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
  - uintToReal :: 1 <= w => sym -> SymBV sym w -> IO (SymReal sym)
  - sbvToReal :: 1 <= w => sym -> SymBV sym w -> IO (SymReal sym)
  - realRound :: sym -> SymReal sym -> IO (SymInteger sym)
  - realRoundEven :: sym -> SymReal sym -> IO (SymInteger sym)
  - realFloor :: sym -> SymReal sym -> IO (SymInteger sym)
  - realCeil :: sym -> SymReal sym -> IO (SymInteger sym)
  - realTrunc :: sym -> SymReal sym -> IO (SymInteger sym)
  - integerToBV :: 1 <= w => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
  - realToInteger :: sym -> SymReal sym -> IO (SymInteger sym)
  - realToBV :: 1 <= w => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
  - realToSBV :: 1 <= w => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
  - clampedIntToSBV :: 1 <= w => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
  - clampedIntToBV :: 1 <= w => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
  - intSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
  - uintSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
  - intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
  - uintToInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
  - stringEmpty :: sym -> StringInfoRepr si -> IO (SymString sym si)
  - stringLit :: sym -> StringLiteral si -> IO (SymString sym si)
  - stringEq :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
  - stringIte :: sym -> Pred sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)
  - stringConcat :: sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)
  - stringContains :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
  - stringIsPrefixOf :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
  - stringIsSuffixOf :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
  - stringIndexOf :: sym -> SymString sym si -> SymString sym si -> SymInteger sym -> IO (SymInteger sym)
  - stringLength :: sym -> SymString sym si -> IO (SymInteger sym)
  - stringSubstring :: sym -> SymString sym si -> SymInteger sym -> SymInteger sym -> IO (SymString sym si)
  - realZero :: sym -> SymReal sym
  - realLit :: sym -> Rational -> IO (SymReal sym)
  - sciLit :: sym -> Scientific -> IO (SymReal sym)
  - realEq :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  - realNe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  - realLe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  - realLt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  - realGe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  - realGt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
  - realIte :: sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realMin :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realMax :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realNeg :: sym -> SymReal sym -> IO (SymReal sym)
  - realAdd :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realMul :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realSub :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realSq :: sym -> SymReal sym -> IO (SymReal sym)
  - realDiv :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realMod :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - isInteger :: sym -> SymReal sym -> IO (Pred sym)
  - realIsNonNeg :: sym -> SymReal sym -> IO (Pred sym)
  - realSqrt :: sym -> SymReal sym -> IO (SymReal sym)
  - realPi :: sym -> IO (SymReal sym)
  - realLog :: sym -> SymReal sym -> IO (SymReal sym)
  - realExp :: sym -> SymReal sym -> IO (SymReal sym)
  - realSin :: sym -> SymReal sym -> IO (SymReal sym)
  - realCos :: sym -> SymReal sym -> IO (SymReal sym)
  - realTan :: sym -> SymReal sym -> IO (SymReal sym)
  - realSinh :: sym -> SymReal sym -> IO (SymReal sym)
  - realCosh :: sym -> SymReal sym -> IO (SymReal sym)
  - realTanh :: sym -> SymReal sym -> IO (SymReal sym)
  - realAbs :: sym -> SymReal sym -> IO (SymReal sym)
  - realHypot :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realAtan2 :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - realSpecialFunction :: sym -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr sym) BaseRealType) args -> IO (SymReal sym)
  - realSpecialFunction0 :: sym -> SpecialFunction EmptyCtx -> IO (SymReal sym)
  - realSpecialFunction1 :: sym -> SpecialFunction (EmptyCtx ::> R) -> SymReal sym -> IO (SymReal sym)
  - realSpecialFunction2 :: sym -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymReal sym -> SymReal sym -> IO (SymReal sym)
  - floatPZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
  - floatNZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
  - floatNaN :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
  - floatPInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
  - floatNInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
  - floatLitRational :: sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)
  - floatLit :: sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
  - floatNeg :: sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatAbs :: sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatSqrt :: sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatAdd :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatSub :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatMul :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatDiv :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatRem :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatMin :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatMax :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatFMA :: sym -> RoundingMode -> SymFloat sym fpp -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatEq :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatNe :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatFpEq :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatFpApart :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatFpUnordered :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatLe :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatLt :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatGe :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatGt :: sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
  - floatIsNaN :: sym -> SymFloat sym fpp -> IO (Pred sym)
  - floatIsInf :: sym -> SymFloat sym fpp -> IO (Pred sym)
  - floatIsZero :: sym -> SymFloat sym fpp -> IO (Pred sym)
  - floatIsPos :: sym -> SymFloat sym fpp -> IO (Pred sym)
  - floatIsNeg :: sym -> SymFloat sym fpp -> IO (Pred sym)
  - floatIsSubnorm :: sym -> SymFloat sym fpp -> IO (Pred sym)
  - floatIsNorm :: sym -> SymFloat sym fpp -> IO (Pred sym)
  - floatIte :: sym -> Pred sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatCast :: sym -> FloatPrecisionRepr fpp -> RoundingMode -> SymFloat sym fpp' -> IO (SymFloat sym fpp)
  - floatRound :: sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
  - floatFromBinary :: (2 <= eb, 2 <= sb) => sym -> FloatPrecisionRepr (FloatingPointPrecision eb sb) -> SymBV sym (eb + sb) -> IO (SymFloat sym (FloatingPointPrecision eb sb))
  - floatToBinary :: (2 <= eb, 2 <= sb) => sym -> SymFloat sym (FloatingPointPrecision eb sb) -> IO (SymBV sym (eb + sb))
  - bvToFloat :: 1 <= w => sym -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV sym w -> IO (SymFloat sym fpp)
  - sbvToFloat :: 1 <= w => sym -> FloatPrecisionRepr fpp -> RoundingMode -> SymBV sym w -> IO (SymFloat sym fpp)
  - realToFloat :: sym -> FloatPrecisionRepr fpp -> RoundingMode -> SymReal sym -> IO (SymFloat sym fpp)
  - floatToBV :: 1 <= w => sym -> NatRepr w -> RoundingMode -> SymFloat sym fpp -> IO (SymBV sym w)
  - floatToSBV :: 1 <= w => sym -> NatRepr w -> RoundingMode -> SymFloat sym fpp -> IO (SymBV sym w)
  - floatToReal :: sym -> SymFloat sym fpp -> IO (SymReal sym)
  - floatSpecialFunction :: sym -> FloatPrecisionRepr fpp -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr sym) (BaseFloatType fpp)) args -> IO (SymFloat sym fpp)
  - mkComplex :: sym -> Complex (SymReal sym) -> IO (SymCplx sym)
  - getRealPart :: sym -> SymCplx sym -> IO (SymReal sym)
  - getImagPart :: sym -> SymCplx sym -> IO (SymReal sym)
  - cplxGetParts :: sym -> SymCplx sym -> IO (Complex (SymReal sym))
  - mkComplexLit :: sym -> Complex Rational -> IO (SymCplx sym)
  - cplxFromReal :: sym -> SymReal sym -> IO (SymCplx sym)
  - cplxIte :: sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxNeg :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxAdd :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxSub :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxMul :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxMag :: sym -> SymCplx sym -> IO (SymReal sym)
  - cplxSqrt :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxSin :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxCos :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxTan :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxHypot :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxRound :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxFloor :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxCeil :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxConj :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxExp :: sym -> SymCplx sym -> IO (SymCplx sym)
  - cplxEq :: sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
  - cplxNe :: sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
- class (IsExprBuilder sym, IsSymFn (SymFn sym), OrdF (SymExpr sym), OrdF (BoundVar sym)) => IsSymExprBuilder sym where
  - freshConstant :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
  - freshLatch :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
  - freshBoundedBV :: 1 <= w => sym -> SolverSymbol -> NatRepr w -> Maybe Natural -> Maybe Natural -> IO (SymBV sym w)
  - freshBoundedSBV :: 1 <= w => sym -> SolverSymbol -> NatRepr w -> Maybe Integer -> Maybe Integer -> IO (SymBV sym w)
  - freshBoundedInt :: sym -> SolverSymbol -> Maybe Integer -> Maybe Integer -> IO (SymInteger sym)
  - freshBoundedReal :: sym -> SolverSymbol -> Maybe Rational -> Maybe Rational -> IO (SymReal sym)
  - exprUninterpConstants :: sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
  - freshBoundVar :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
  - varExpr :: sym -> BoundVar sym tp -> SymExpr sym tp
  - forallPred :: sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
  - existsPred :: sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
  - definedFn :: sym -> SolverSymbol -> Assignment (BoundVar sym) args -> SymExpr sym ret -> UnfoldPolicy -> IO (SymFn sym args ret)
  - inlineDefineFun :: CurryAssignmentClass args => sym -> SolverSymbol -> Assignment BaseTypeRepr args -> UnfoldPolicy -> CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret)) -> IO (SymFn sym args ret)
  - freshTotalUninterpFn :: forall args ret. sym -> SolverSymbol -> Assignment BaseTypeRepr args -> BaseTypeRepr ret -> IO (SymFn sym args ret)
  - applySymFn :: sym -> SymFn sym args ret -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
  - substituteBoundVars :: sym -> MapF (BoundVar sym) (SymExpr sym) -> SymExpr sym tp -> IO (SymExpr sym tp)
  - substituteSymFns :: sym -> MapF (SymFnWrapper sym) (SymFnWrapper sym) -> SymExpr sym tp -> IO (SymExpr sym tp)
- data SolverEvent
  - = SolverStartSATQuery SolverStartSATQuery
  - | SolverEndSATQuery SolverEndSATQuery
- data SolverStartSATQuery = SolverStartSATQueryRec {
  - satQuerySolverName :: !String
  - satQueryReason :: !String
  }
- data SolverEndSATQuery = SolverEndSATQueryRec {
  - satQueryResult :: !(SatResult () ())
  - satQueryError :: !(Maybe String)
  }
- bvJoinVector :: forall sym n w. (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> Vector n (SymBV sym w) -> IO (SymBV sym (n * w))
- 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))
- bvSwap :: forall sym n. (1 <= n, IsExprBuilder sym) => sym -> NatRepr n -> SymBV sym (n * 8) -> IO (SymBV sym (n * 8))
- bvBitreverse :: forall sym w. (1 <= w, IsExprBuilder sym) => sym -> SymBV sym w -> IO (SymBV sym w)
- data RoundingMode
  - = RNE
  - | RNA
  - | RTP
  - | RTN
  - | RTZ
- data Statistics = Statistics {
  - statAllocs :: !Integer
  - statNonLinearOps :: !Integer
  }
- zeroStatistics :: Statistics
- type Pred sym = SymExpr sym BaseBoolType
- type SymInteger sym = SymExpr sym BaseIntegerType
- type SymReal sym = SymExpr sym BaseRealType
- type SymFloat sym fpp = SymExpr sym (BaseFloatType fpp)
- type SymString sym si = SymExpr sym (BaseStringType si)
- type SymCplx sym = SymExpr sym BaseComplexType
- type SymStruct sym flds = SymExpr sym (BaseStructType flds)
- type SymBV sym n = SymExpr sym (BaseBVType n)
- type SymArray sym idx b = SymExpr sym (BaseArrayType idx b)
- data SymNat sym
- asNat :: IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
- natLit :: IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
- natAdd :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
- natSub :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
- natMul :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
- natDiv :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
- natMod :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
- natIte :: IsExprBuilder sym => sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
- natEq :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
- natLe :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
- natLt :: IsExprBuilder sym => sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
- natToInteger :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymInteger sym)
- natToIntegerPure :: SymNat sym -> SymInteger sym
- bvToNat :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymNat sym)
- natToReal :: IsExprBuilder sym => sym -> SymNat sym -> IO (SymReal sym)
- integerToNat :: IsExprBuilder sym => sym -> SymInteger sym -> IO (SymNat sym)
- realToNat :: IsExprBuilder sym => sym -> SymReal sym -> IO (SymNat sym)
- freshBoundedNat :: IsSymExprBuilder sym => sym -> SolverSymbol -> Maybe Natural -> Maybe Natural -> IO (SymNat sym)
- freshNat :: IsSymExprBuilder sym => sym -> SolverSymbol -> IO (SymNat sym)
- printSymNat :: IsExpr (SymExpr sym) => SymNat sym -> Doc ann
- data IndexLit idx where
  - IntIndexLit :: !Integer -> IndexLit BaseIntegerType
  - BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w)
- indexLit :: IsExprBuilder sym => sym -> IndexLit idx -> IO (SymExpr sym idx)
- newtype ArrayResultWrapper f idx tp = ArrayResultWrapper {
  - unwrapArrayResult :: f (BaseArrayType idx tp)
  }
- asConcrete :: IsExpr e => e tp -> Maybe (ConcreteVal tp)
- concreteToSym :: IsExprBuilder sym => sym -> ConcreteVal tp -> IO (SymExpr sym tp)
- baseIsConcrete :: forall e bt. IsExpr e => e bt -> Bool
- baseDefaultValue :: forall sym bt. IsExprBuilder sym => sym -> BaseTypeRepr bt -> IO (SymExpr sym bt)
- realExprAsInteger :: (IsExpr e, MonadFail m) => e BaseRealType -> m Integer
- rationalAsInteger :: MonadFail m => Rational -> m Integer
- cplxExprAsRational :: (MonadFail m, IsExpr e) => e BaseComplexType -> m Rational
- cplxExprAsInteger :: (MonadFail m, IsExpr e) => e BaseComplexType -> m Integer
- data SymEncoder sym v tp = SymEncoder {
  - symEncoderType :: !(BaseTypeRepr tp)
  - symFromExpr :: !(sym -> SymExpr sym tp -> IO v)
  - symToExpr :: !(sym -> v -> IO (SymExpr sym tp))
  }
- backendPred :: IsExprBuilder sym => sym -> Bool -> Pred sym
- andAllOf :: IsExprBuilder sym => sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
- orOneOf :: IsExprBuilder sym => sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
- itePredM :: (IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m) => sym -> Pred sym -> m (Pred sym) -> m (Pred sym) -> m (Pred sym)
- iteM :: IsExprBuilder sym => (sym -> Pred sym -> v -> v -> IO v) -> sym -> Pred sym -> IO v -> IO v -> IO v
- iteList :: IsExprBuilder sym => (sym -> Pred sym -> v -> v -> IO v) -> sym -> [(IO (Pred sym), IO v)] -> IO v -> IO v
- predToReal :: IsExprBuilder sym => sym -> Pred sym -> IO (SymReal sym)
- cplxDiv :: IsExprBuilder sym => sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
- cplxLog :: IsExprBuilder sym => sym -> SymCplx sym -> IO (SymCplx sym)
- cplxLogBase :: IsExprBuilder sym => Rational -> sym -> SymCplx sym -> IO (SymCplx sym)
- mkRational :: IsExprBuilder sym => sym -> Rational -> IO (SymCplx sym)
- mkReal :: (IsExprBuilder sym, Real a) => sym -> a -> IO (SymCplx sym)
- isNonZero :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)
- isReal :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)
- muxRange :: (IsExpr e, Monad m) => (Natural -> m (e BaseBoolType)) -> (e BaseBoolType -> a -> a -> m a) -> (Natural -> m a) -> Natural -> Natural -> m a
- data InvalidRange where
  - InvalidRange :: BaseTypeRepr bt -> Maybe (ConcreteValue bt) -> Maybe (ConcreteValue bt) -> InvalidRange
- module Data.Parameterized.NatRepr
- module What4.BaseTypes
- class HasAbsValue f
- data SolverSymbol
- emptySymbol :: SolverSymbol
- userSymbol :: String -> Either SolverSymbolError SolverSymbol
- safeSymbol :: String -> SolverSymbol
- data ValueRange tp
  - = SingleRange !tp
  - | UnboundedRange
  - | MinRange !tp
  - | MaxRange !tp
  - | IntervalRange !tp !tp
- data StringLiteral (si :: StringInfo) :: Type where
  - UnicodeLiteral :: !Text -> StringLiteral Unicode
  - Char8Literal :: !ByteString -> StringLiteral Char8
  - Char16Literal :: !Word16String -> StringLiteral Char16
- stringLiteralInfo :: StringLiteral si -> StringInfoRepr si

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

Minimal complete definition

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

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.

unsafeSetAbstractValue :: AbstractValue tp -> e tp -> e tp Source #

Set the abstract value of an expression. This is primarily useful for symbolic expressions where the domain is known to be narrower than what is contained in the expression. Setting the abstract value to use the narrower domain can, in some cases, allow the expression to be further simplified.

This is prefixed with `unsafe-` because it has the potential to introduce unsoundness if the new abstract value does not accurately represent the domain of the expression. As such, the burden is on users of this function to ensure that the new abstract value is used soundly.

Note that composing expressions together can sometimes widen the abstract domains involved, so if you use this function to change an abstract value, be careful than subsequent operations do not widen away the value. As a potential safeguard, one can use `annotateTerm` on the new expression to inhibit transformations that could change the abstract value.

#### 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 :: Natural). 1 <= w => Expr t (BaseBVType w) -> Maybe (Integer, Integer) Source #

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

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

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

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

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

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

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

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

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

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

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

class IsSymFn (fn :: Ctx BaseType -> BaseType -> Type) 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.

fnTestEquality :: fn args1 ret1 -> fn args2 ret2 -> Maybe ((args1 ::> ret1) :~: (args2 ::> ret2)) Source #

Test whether two functions are equal.

The implementation may be incomplete, that is, if it returns `Just` then the functions are equal, while if it returns `Nothing` then the functions may or may not be equal. The result of `freshTotalUninterpFn` or `definedFn` tests equal with itself.

fnCompare :: fn args1 ret1 -> fn args2 ret2 -> OrderingF (args1 ::> ret1) (args2 ::> ret2) Source #

Compare two functions for ordering.

The underlying equality test is provided by `fnTestEquality`.

#### Instances

Instances details

IsSymFn (ExprSymFn t) Source # |

Instance details

Defined in What4.Expr.App

Methods

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

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

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

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

data SomeSymFn sym Source #

Constructors

forall args ret. SomeSymFn (SymFn sym args ret) |

data SymFnWrapper sym ctx where Source #

Wrapper for `SymFn` that concatenates the arguments and the return types.

This is useful for implementing `TestEquality` and `OrdF` instances for `SymFn`, and for using `SymFn` as a key or a value in a `MapF`.

Constructors

SymFnWrapper :: forall sym args ret. SymFn sym args ret -> SymFnWrapper sym (args ::> ret) |

#### Instances

Instances details

IsSymFn (SymFn sym) => TestEquality (SymFnWrapper sym :: Ctx BaseType -> Type) Source # |
Instance details Defined in What4.Interface Methods testEquality :: forall (a :: k) (b :: k). SymFnWrapper sym a -> SymFnWrapper sym b -> Maybe (a :~: b) Source #
IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym :: Ctx BaseType -> Type) Source # |

Instance details

Defined in What4.Interface

Methods

compareF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool Source #

ltF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool Source #

geqF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool Source #

gtF :: forall (x :: k) (y :: k). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool 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.

#### Instances

Instances details

Show UnfoldPolicy Source # |
Instance details Defined in What4.Interface Methods showsPrec :: Int -> UnfoldPolicy -> ShowS Source # show :: UnfoldPolicy -> String Source # showList :: [UnfoldPolicy] -> ShowS Source #
Eq UnfoldPolicy Source # |
Instance details Defined in What4.Interface Methods (==) :: UnfoldPolicy -> UnfoldPolicy -> Bool Source # (/=) :: UnfoldPolicy -> UnfoldPolicy -> Bool Source #
Ord UnfoldPolicy Source # |

Instance details

Defined in What4.Interface

Methods

compare :: UnfoldPolicy -> UnfoldPolicy -> Ordering Source #

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

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

(>) :: UnfoldPolicy -> UnfoldPolicy -> Bool Source #

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

max :: UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy Source #

min :: UnfoldPolicy -> UnfoldPolicy -> UnfoldPolicy Source #

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), HashableF (BoundVar 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, getUnannotatedTerm, 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, arrayCopy, arraySet, arrayRangeEq, 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, realSpecialFunction, 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, floatSpecialFunction, 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.

getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp) Source #

Project the original, unannotated term from an annotated term. This returns `Nothing` for terms that do not have annotations.

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.

arrayCopy Source #

Arguments

:: 1 <= w |
=> sym |

-> SymArray sym (SingleCtx (BaseBVType w)) a

    dest_arr

-> SymBV sym w

    dest_idx

-> SymArray sym (SingleCtx (BaseBVType w)) a

    src_arr

-> SymBV sym w

    src_idx

-> SymBV sym w

    len

-> IO (SymArray sym (SingleCtx (BaseBVType w)) a) |

Copy elements from the source array to the destination array.

``arrayCopy` sym dest_arr dest_idx src_arr src_idx len` copies the elements from `src_arr` at indices `[src_idx .. (src_idx + len - 1)]` into `dest_arr` at indices `[dest_idx .. (dest_idx + len - 1)]`.

The result is undefined if either `dest_idx + len` or `src_idx + len` wraps around.

arraySet Source #

Arguments

:: 1 <= w |
=> sym |

-> SymArray sym (SingleCtx (BaseBVType w)) a

    arr

-> SymBV sym w

    idx

-> SymExpr sym a

    val

-> SymBV sym w

    len

-> IO (SymArray sym (SingleCtx (BaseBVType w)) a) |

Set elements of the given array.

``arraySet` sym arr idx val len` sets the elements of `arr` at indices `[idx .. (idx + len - 1)]` to `val`.

The result is undefined if `idx + len` wraps around.

arrayRangeEq Source #

Arguments

:: 1 <= w |
=> sym |

-> SymArray sym (SingleCtx (BaseBVType w)) a

    lhs_arr

-> SymBV sym w

    lhs_idx

-> SymArray sym (SingleCtx (BaseBVType w)) a

    rhs_arr

-> SymBV sym w

    rhs_idx

-> SymBV sym w

    len

-> IO (Pred sym) |

Check whether the lhs array and rhs array are equal at a range of indices.

``arrayRangeEq` sym lhs_arr lhs_idx rhs_arr rhs_idx len` checks whether the elements of `lhs_arr` at indices `[lhs_idx .. (lhs_idx + len - 1)]` and the elements of `rhs_arr` at indices `[rhs_idx .. (rhs_idx + len - 1)]` are equal.

The result is undefined if either `lhs_idx + len` or `rhs_idx + len` wraps around.

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

Arguments

:: sym |
-> SymString sym si | string to test
-> SymString sym si | substring to look for
-> IO (Pred sym) |

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

stringIsPrefixOf Source #

Arguments

:: sym |
-> SymString sym si | prefix string
-> SymString sym si | string to test
-> IO (Pred sym) |

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

stringIsSuffixOf Source #

Arguments

:: sym |
-> SymString sym si | suffix string
-> SymString sym si | string to test
-> IO (Pred sym) |

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

stringIndexOf Source #

Arguments

:: sym |
-> SymString sym si | string to search in
-> SymString sym si | substring to search for
-> SymInteger sym | starting index for search
-> IO (SymInteger sym) |

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

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

Compute the length of a string

stringSubstring Source #

Arguments

:: sym |
-> SymString sym si | string to select a substring from
-> SymInteger sym | offset of the beginning of the substring
-> SymInteger sym | length of the substring
-> IO (SymString sym si) |

`stringSubstring s off len` evaluates to the longest substring of `s` of length at most `len` starting at position `off`. It evaluates to the empty string if `len` is negative or `off` is not in the interval `[0,l-1]` where `l` is the length of `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.

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

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.

realSpecialFunction :: sym -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr sym) BaseRealType) args -> IO (SymReal sym) Source #

Apply a special function to real arguments

realSpecialFunction0 :: sym -> SpecialFunction EmptyCtx -> IO (SymReal sym) Source #

Access a 0-arity special function constant

realSpecialFunction1 :: sym -> SpecialFunction (EmptyCtx ::> R) -> SymReal sym -> IO (SymReal sym) Source #

Apply a 1-argument special function

realSpecialFunction2 :: sym -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> SymReal sym -> SymReal sym -> IO (SymReal sym) Source #

Apply a 2-argument special function

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.

floatSpecialFunction :: sym -> FloatPrecisionRepr fpp -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr sym) (BaseFloatType fpp)) args -> IO (SymFloat sym fpp) Source #

Apply a special function to floating-point arguments

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 #

getUnannotatedTerm :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> Maybe (SymExpr (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 :: Natural). 1 <= w => ExprBuilder t st fs -> NatRepr w -> BV w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvConcat :: forall (u :: Natural) (v :: Natural). (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 :: Natural) (n :: Natural) (w :: Natural). (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 :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvAdd :: forall (w :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 1 <= w => ExprBuilder t st fs -> Natural -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source #

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

bvIte :: forall (w :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) Source #

bvShl :: forall (w :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural) (r :: Natural). (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 :: Natural) (r :: Natural). (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 :: Natural) (w :: Natural). (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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymBV (ExprBuilder t st fs) w) Source #

bvSet :: forall (w :: Natural). 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 :: Natural). 1 <= w => ExprBuilder t st fs -> NatRepr w -> Pred (ExprBuilder t st fs) -> IO (SymBV (ExprBuilder t st fs) w) Source #

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

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

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

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

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

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

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

addUnsignedOF :: forall (w :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 #

arrayCopy :: forall (w :: Natural) (a :: BaseType). 1 <= w => ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a) Source #

arraySet :: forall (w :: Natural) (a :: BaseType). 1 <= w => ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymExpr (ExprBuilder t st fs) a -> SymBV (ExprBuilder t st fs) w -> IO (SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a) Source #

arrayRangeEq :: forall (w :: Natural) (a :: BaseType). 1 <= w => ExprBuilder t st fs -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymArray (ExprBuilder t st fs) (SingleCtx (BaseBVType w)) a -> SymBV (ExprBuilder t st fs) w -> SymBV (ExprBuilder t st fs) w -> IO (Pred (ExprBuilder t st fs)) 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 :: Natural). 1 <= w => ExprBuilder t st fs -> SymBV (ExprBuilder t st fs) w -> IO (SymInteger (ExprBuilder t st fs)) Source #

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

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

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

sbvToReal :: forall (w :: Natural). 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 :: Natural). 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 :: Natural). 1 <= w => ExprBuilder t st fs -> SymReal (ExprBuilder t st fs) -> NatRepr w -> IO (SymBV (ExprBuilder t st fs) w) Source #

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

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

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

intSetWidth :: forall (m :: Natural) (n :: Natural). (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 :: Natural) (n :: Natural). (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 :: Natural) (n :: Natural). (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 :: Natural) (n :: Natural). (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 #

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 #

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

realSpecialFunction :: forall (args :: Ctx Type). ExprBuilder t st fs -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st fs)) BaseRealType) args -> IO (SymReal (ExprBuilder t st fs)) Source #

realSpecialFunction0 :: ExprBuilder t st fs -> SpecialFunction EmptyCtx -> IO (SymReal (ExprBuilder t st fs)) Source #

realSpecialFunction1 :: ExprBuilder t st fs -> SpecialFunction (EmptyCtx ::> R) -> SymReal (ExprBuilder t st fs) -> IO (SymReal (ExprBuilder t st fs)) Source #

realSpecialFunction2 :: ExprBuilder t st fs -> SpecialFunction ((EmptyCtx ::> R) ::> R) -> 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 :: Natural) (sb :: Natural). (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 :: Natural) (sb :: Natural). (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 :: Natural) (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 :: Natural) (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 :: Natural) (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 :: Natural) (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 #

floatSpecialFunction :: forall (fpp :: FloatPrecision) (args :: Ctx Type). ExprBuilder t st fs -> FloatPrecisionRepr fpp -> SpecialFunction args -> Assignment (SpecialFnArg (SymExpr (ExprBuilder t st fs)) (BaseFloatType fpp)) args -> IO (SymFloat (ExprBuilder t st fs) fpp) 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), OrdF (BoundVar sym)) => IsSymExprBuilder sym where Source #

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

Minimal complete definition

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

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.

exprUninterpConstants :: sym -> SymExpr sym tp -> Set (Some (BoundVar sym)) Source #

Return the set of uninterpreted constants in the given expression.

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.

substituteBoundVars :: sym -> MapF (BoundVar sym) (SymExpr sym) -> SymExpr sym tp -> IO (SymExpr sym tp) Source #

Apply a variable substitution (variable to symbolic expression mapping) to a symbolic expression.

substituteSymFns :: sym -> MapF (SymFnWrapper sym) (SymFnWrapper sym) -> SymExpr sym tp -> IO (SymExpr sym tp) Source #

Apply a function substitution (function to function mapping) to a symbolic expression.

#### 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 :: Natural). 1 <= w => ExprBuilder t st fs -> SolverSymbol -> NatRepr w -> Maybe Natural -> Maybe Natural -> IO (SymBV (ExprBuilder t st fs) w) Source #

freshBoundedSBV :: forall (w :: Natural). 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 #

exprUninterpConstants :: forall (tp :: BaseType). ExprBuilder t st fs -> SymExpr (ExprBuilder t st fs) tp -> Set (Some (BoundVar (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 #

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

substituteSymFns :: forall (tp :: BaseType). ExprBuilder t st fs -> MapF (SymFnWrapper (ExprBuilder t st fs)) (SymFnWrapper (ExprBuilder t st fs)) -> SymExpr (ExprBuilder t st fs) tp -> IO (SymExpr (ExprBuilder t st fs) tp) 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.

Constructors

SolverStartSATQuery SolverStartSATQuery |
SolverEndSATQuery SolverEndSATQuery |

#### Instances

Instances details

Generic SolverEvent Source # |
Instance details Defined in What4.Interface Associated Types type Rep SolverEvent :: Type -> Type Source # Methods from :: SolverEvent -> Rep SolverEvent x Source # to :: Rep SolverEvent x -> SolverEvent Source #
Show SolverEvent Source # |
Instance details Defined in What4.Interface Methods showsPrec :: Int -> SolverEvent -> ShowS Source # show :: SolverEvent -> String Source # showList :: [SolverEvent] -> ShowS Source #
type Rep SolverEvent Source # |

Instance details

Defined in What4.Interface

type Rep SolverEvent = D1 ('MetaData "SolverEvent" "What4.Interface" "what4-1.5.1-96RHnAoFm39CNNNDj0F3kd" 'False) (C1 ('MetaCons "SolverStartSATQuery" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SolverStartSATQuery)) :+: C1 ('MetaCons "SolverEndSATQuery" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SolverEndSATQuery)))

data SolverStartSATQuery Source #

Constructors

SolverStartSATQueryRec |

Fields

- satQuerySolverName :: !String
- satQueryReason :: !String

#### Instances

Instances details

Generic SolverStartSATQuery Source # |
Instance details Defined in What4.Interface Associated Types type Rep SolverStartSATQuery :: Type -> Type Source # Methods from :: SolverStartSATQuery -> Rep SolverStartSATQuery x Source # to :: Rep SolverStartSATQuery x -> SolverStartSATQuery Source #
Show SolverStartSATQuery Source # |
Instance details Defined in What4.Interface Methods showsPrec :: Int -> SolverStartSATQuery -> ShowS Source # show :: SolverStartSATQuery -> String Source # showList :: [SolverStartSATQuery] -> ShowS Source #
type Rep SolverStartSATQuery Source # |

Instance details

Defined in What4.Interface

type Rep SolverStartSATQuery = D1 ('MetaData "SolverStartSATQuery" "What4.Interface" "what4-1.5.1-96RHnAoFm39CNNNDj0F3kd" 'False) (C1 ('MetaCons "SolverStartSATQueryRec" 'PrefixI 'True) (S1 ('MetaSel ('Just "satQuerySolverName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String) :*: S1 ('MetaSel ('Just "satQueryReason") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String)))

data SolverEndSATQuery Source #

Constructors

SolverEndSATQueryRec |

Fields

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

#### Instances

Instances details

Generic SolverEndSATQuery Source # |
Instance details Defined in What4.Interface Associated Types type Rep SolverEndSATQuery :: Type -> Type Source # Methods from :: SolverEndSATQuery -> Rep SolverEndSATQuery x Source # to :: Rep SolverEndSATQuery x -> SolverEndSATQuery Source #
Show SolverEndSATQuery Source # |
Instance details Defined in What4.Interface Methods showsPrec :: Int -> SolverEndSATQuery -> ShowS Source # show :: SolverEndSATQuery -> String Source # showList :: [SolverEndSATQuery] -> ShowS Source #
type Rep SolverEndSATQuery Source # |

Instance details

Defined in What4.Interface

type Rep SolverEndSATQuery = D1 ('MetaData "SolverEndSATQuery" "What4.Interface" "what4-1.5.1-96RHnAoFm39CNNNDj0F3kd" 'False) (C1 ('MetaCons "SolverEndSATQueryRec" '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

Methods

succ :: RoundingMode -> RoundingMode Source #

pred :: RoundingMode -> RoundingMode Source #

toEnum :: Int -> RoundingMode Source #

fromEnum :: RoundingMode -> Int Source #

enumFrom :: RoundingMode -> [RoundingMode] Source #

enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode] Source #

enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode] Source #

enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode] Source #

Generic RoundingMode Source # |
Instance details Defined in What4.Utils.FloatHelpers Associated Types type Rep RoundingMode :: Type -> Type Source # Methods from :: RoundingMode -> Rep RoundingMode x Source # to :: Rep RoundingMode x -> RoundingMode Source #
Show RoundingMode Source # |
Instance details Defined in What4.Utils.FloatHelpers Methods showsPrec :: Int -> RoundingMode -> ShowS Source # show :: RoundingMode -> String Source # showList :: [RoundingMode] -> ShowS Source #
Eq RoundingMode Source # |
Instance details Defined in What4.Utils.FloatHelpers Methods (==) :: RoundingMode -> RoundingMode -> Bool Source # (/=) :: RoundingMode -> RoundingMode -> Bool Source #
Ord RoundingMode Source # |

Instance details

Defined in What4.Utils.FloatHelpers

Methods

compare :: RoundingMode -> RoundingMode -> Ordering Source #

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

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

(>) :: RoundingMode -> RoundingMode -> Bool Source #

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

max :: RoundingMode -> RoundingMode -> RoundingMode Source #

min :: RoundingMode -> RoundingMode -> RoundingMode Source #

Hashable RoundingMode Source # |
Instance details Defined in What4.Utils.FloatHelpers Methods hashWithSalt :: Int -> RoundingMode -> Int Source # hash :: RoundingMode -> Int Source #
type Rep RoundingMode Source # |

Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.5.1-96RHnAoFm39CNNNDj0F3kd" '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

- statAllocs :: !Integer

  The number of times an expression node has been allocated.

- statNonLinearOps :: !Integer

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

#### Instances

Instances details

Show Statistics Source # |
Instance details Defined in What4.Interface Methods showsPrec :: Int -> Statistics -> ShowS Source # show :: Statistics -> String Source # showList :: [Statistics] -> ShowS Source #

zeroStatistics :: Statistics Source #

# 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 Source # (/=) :: SymNat sym -> SymNat sym -> Bool Source #
OrdF (SymExpr sym) => Ord (SymNat sym) Source # |

Instance details

Defined in What4.Interface

Methods

compare :: SymNat sym -> SymNat sym -> Ordering Source #

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

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

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

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

max :: SymNat sym -> SymNat sym -> SymNat sym Source #

min :: SymNat sym -> SymNat sym -> SymNat sym Source #

(HashableF (SymExpr sym), TestEquality (SymExpr sym)) => Hashable (SymNat sym) Source # |
Instance details Defined in What4.Interface Methods hashWithSalt :: Int -> SymNat sym -> Int Source # hash :: SymNat sym -> Int Source #

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.

natToIntegerPure :: SymNat sym -> SymInteger sym Source #

Convert a natural number to an integer. `natToInteger` is just this operation lifted into IO.

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) Source #
HashableF IndexLit Source # |
Instance details Defined in What4.IndexLit Methods hashWithSaltF :: forall (tp :: k). Int -> IndexLit tp -> Int Source # hashF :: forall (tp :: k). IndexLit tp -> Int Source #
OrdF IndexLit Source # |

Instance details

Defined in What4.IndexLit

Methods

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

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

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

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

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

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 Source # showF :: forall (tp :: k). IndexLit tp -> String Source # showsPrecF :: forall (tp :: k). Int -> IndexLit tp -> String -> String Source #
Show (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods showsPrec :: Int -> IndexLit tp -> ShowS Source # show :: IndexLit tp -> String Source # showList :: [IndexLit tp] -> ShowS Source #
Eq (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods (==) :: IndexLit tp -> IndexLit tp -> Bool Source # (/=) :: IndexLit tp -> IndexLit tp -> Bool Source #
Hashable (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods hashWithSalt :: Int -> IndexLit tp -> Int Source # hash :: IndexLit tp -> Int Source #

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

- unwrapArrayResult :: f (BaseArrayType idx tp)

#### 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) Source #
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 Source # hashF :: forall (tp :: k). ArrayResultWrapper e idx tp -> Int Source #

# 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

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

# Utility combinators

## Boolean operations

backendPred :: IsExprBuilder sym => sym -> Bool -> Pred sym 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.

Constructors

InvalidRange :: BaseTypeRepr bt -> Maybe (ConcreteValue bt) -> Maybe (ConcreteValue bt) -> InvalidRange |

#### Instances

Instances details

Exception InvalidRange Source # |
Instance details Defined in What4.Interface Methods toException :: InvalidRange -> SomeException Source # fromException :: SomeException -> Maybe InvalidRange Source # displayException :: InvalidRange -> String Source #
Show InvalidRange Source # |
Instance details Defined in What4.Interface Methods showsPrec :: Int -> InvalidRange -> ShowS Source # show :: InvalidRange -> String Source # showList :: [InvalidRange] -> ShowS Source #

# Reexports

module Data.Parameterized.NatRepr

module What4.BaseTypes

class HasAbsValue f Source #

A utility class for values that contain abstract values

Minimal complete definition

getAbsValue

#### Instances

Instances details

HasAbsValue (Dummy :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp Source #
HasAbsValue (Expr t) Source # |
Instance details Defined in What4.Expr.App Methods getAbsValue :: forall (tp :: BaseType). Expr t 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.

#### Instances

Instances details

Show SolverSymbol Source # |
Instance details Defined in What4.Symbol Methods showsPrec :: Int -> SolverSymbol -> ShowS Source # show :: SolverSymbol -> String Source # showList :: [SolverSymbol] -> ShowS Source #
Eq SolverSymbol Source # |
Instance details Defined in What4.Symbol Methods (==) :: SolverSymbol -> SolverSymbol -> Bool Source # (/=) :: SolverSymbol -> SolverSymbol -> Bool Source #
Ord SolverSymbol Source # |

Instance details

Defined in What4.Symbol

Methods

compare :: SolverSymbol -> SolverSymbol -> Ordering Source #

(<) :: SolverSymbol -> SolverSymbol -> Bool Source #

(<=) :: SolverSymbol -> SolverSymbol -> Bool Source #

(>) :: SolverSymbol -> SolverSymbol -> Bool Source #

(>=) :: SolverSymbol -> SolverSymbol -> Bool Source #

max :: SolverSymbol -> SolverSymbol -> SolverSymbol Source #

min :: SolverSymbol -> SolverSymbol -> SolverSymbol Source #

Hashable SolverSymbol Source # |
Instance details Defined in What4.Symbol Methods hashWithSalt :: Int -> SolverSymbol -> Int Source # hash :: SolverSymbol -> Int Source #

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
UnboundedRange | The number is unconstrained.
MinRange !tp | The number is greater than or equal to the given lower bound.
MaxRange !tp | The number is less than or equal to the given upper bound.
IntervalRange !tp !tp | The number is between the given lower and upper bounds.

data StringLiteral (si :: StringInfo) :: Type where Source #

Constructors

UnicodeLiteral :: !Text -> StringLiteral Unicode |
Char8Literal :: !ByteString -> StringLiteral Char8 |
Char16Literal :: !Word16String -> StringLiteral Char16 |

#### 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) Source #
HashableF StringLiteral Source # |
Instance details Defined in What4.Utils.StringLiteral Methods hashWithSaltF :: forall (tp :: k). Int -> StringLiteral tp -> Int Source # hashF :: forall (tp :: k). StringLiteral tp -> Int Source #
OrdF StringLiteral Source # |

Instance details

Defined in What4.Utils.StringLiteral

Methods

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

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

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

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

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

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 Source # showF :: forall (tp :: k). StringLiteral tp -> String Source # showsPrecF :: forall (tp :: k). Int -> StringLiteral tp -> String -> String Source #
IsString (StringLiteral Unicode) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods fromString :: String -> StringLiteral Unicode Source #
Semigroup (StringLiteral si) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods (<>) :: StringLiteral si -> StringLiteral si -> StringLiteral si Source # sconcat :: NonEmpty (StringLiteral si) -> StringLiteral si Source # stimes :: Integral b => b -> StringLiteral si -> StringLiteral si Source #
Show (StringLiteral si) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods showsPrec :: Int -> StringLiteral si -> ShowS Source # show :: StringLiteral si -> String Source # showList :: [StringLiteral si] -> ShowS Source #
Eq (StringLiteral si) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods (==) :: StringLiteral si -> StringLiteral si -> Bool Source # (/=) :: StringLiteral si -> StringLiteral si -> Bool Source #
Ord (StringLiteral si) Source # |

Instance details

Defined in What4.Utils.StringLiteral

Methods

compare :: StringLiteral si -> StringLiteral si -> Ordering Source #

(<) :: StringLiteral si -> StringLiteral si -> Bool Source #

(<=) :: StringLiteral si -> StringLiteral si -> Bool Source #

(>) :: StringLiteral si -> StringLiteral si -> Bool Source #

(>=) :: StringLiteral si -> StringLiteral si -> Bool Source #

max :: StringLiteral si -> StringLiteral si -> StringLiteral si Source #

min :: StringLiteral si -> StringLiteral si -> StringLiteral si Source #

Hashable (StringLiteral si) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods hashWithSalt :: Int -> StringLiteral si -> Int Source # hash :: StringLiteral si -> Int Source #

stringLiteralInfo :: StringLiteral si -> StringInfoRepr si Source #