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

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

What4.Protocol.SMTWriter

Contents

- Type classes
- Terms
- SMTWriter
- SyGuS
- SMTWriter operations
- Reexports

Description

This defines common definitions used in writing SMTLIB (2.0 and later), and yices outputs from `Expr` values.

The writer is designed to support solvers with arithmetic, propositional logic, bitvector, tuples (aka. structs), and arrays.

It maps complex Expr values to either structs or arrays depending on what the solver supports (structs are preferred if both are supported).

It maps multi-dimensional arrays to either arrays with structs as indices if structs are supported or nested arrays if they are not.

The solver should detect when something is not supported and give an error rather than sending invalid output to a file.

Synopsis

- class Num v => SupportTermOps v where
  - boolExpr :: Bool -> v
  - notExpr :: v -> v
  - andAll :: [v] -> v
  - orAll :: [v] -> v
  - (.&&) :: v -> v -> v
  - (.||) :: v -> v -> v
  - (.==) :: v -> v -> v
  - (./=) :: v -> v -> v
  - impliesExpr :: v -> v -> v
  - letExpr :: [(Text, v)] -> v -> v
  - ite :: v -> v -> v -> v
  - sumExpr :: [v] -> v
  - termIntegerToReal :: v -> v
  - termRealToInteger :: v -> v
  - integerTerm :: Integer -> v
  - rationalTerm :: Rational -> v
  - (.<=) :: v -> v -> v
  - (.<) :: v -> v -> v
  - (.>) :: v -> v -> v
  - (.>=) :: v -> v -> v
  - intAbs :: v -> v
  - intDiv :: v -> v -> v
  - intMod :: v -> v -> v
  - intDivisible :: v -> Natural -> v
  - bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> v
  - bvNeg :: v -> v
  - bvAdd :: v -> v -> v
  - bvSub :: v -> v -> v
  - bvMul :: v -> v -> v
  - bvSLe :: v -> v -> v
  - bvULe :: v -> v -> v
  - bvSLt :: v -> v -> v
  - bvULt :: v -> v -> v
  - bvUDiv :: v -> v -> v
  - bvURem :: v -> v -> v
  - bvSDiv :: v -> v -> v
  - bvSRem :: v -> v -> v
  - bvAnd :: v -> v -> v
  - bvOr :: v -> v -> v
  - bvXor :: v -> v -> v
  - bvNot :: v -> v
  - bvShl :: v -> v -> v
  - bvLshr :: v -> v -> v
  - bvAshr :: v -> v -> v
  - bvConcat :: v -> v -> v
  - bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> v -> v
  - bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> v -> v
  - bvSumExpr :: forall (w :: Nat). NatRepr w -> [v] -> v
  - floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> v
  - floatNeg :: v -> v
  - floatAbs :: v -> v
  - floatSqrt :: RoundingMode -> v -> v
  - floatAdd :: RoundingMode -> v -> v -> v
  - floatSub :: RoundingMode -> v -> v -> v
  - floatMul :: RoundingMode -> v -> v -> v
  - floatDiv :: RoundingMode -> v -> v -> v
  - floatRem :: v -> v -> v
  - floatFMA :: RoundingMode -> v -> v -> v -> v
  - floatEq :: v -> v -> v
  - floatFpEq :: v -> v -> v
  - floatLe :: v -> v -> v
  - floatLt :: v -> v -> v
  - floatIsNaN :: v -> v
  - floatIsInf :: v -> v
  - floatIsZero :: v -> v
  - floatIsPos :: v -> v
  - floatIsNeg :: v -> v
  - floatIsSubnorm :: v -> v
  - floatIsNorm :: v -> v
  - floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> v -> v
  - floatRound :: RoundingMode -> v -> v
  - floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> v -> v
  - bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> v -> v
  - sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> v -> v
  - realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> v -> v
  - floatToBV :: Natural -> RoundingMode -> v -> v
  - floatToSBV :: Natural -> RoundingMode -> v -> v
  - floatToReal :: v -> v
  - realIsInteger :: v -> v
  - realDiv :: v -> v -> v
  - realSin :: v -> v
  - realCos :: v -> v
  - realTan :: v -> v
  - realATan2 :: v -> v -> v
  - realSinh :: v -> v
  - realCosh :: v -> v
  - realTanh :: v -> v
  - realExp :: v -> v
  - realLog :: v -> v
  - smtFnApp :: v -> [v] -> v
  - smtFnUpdate :: Maybe (v -> [v] -> v -> v)
  - lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> v -> v)
  - fromText :: Text -> v
- type ArrayConstantFn v = [Some TypeMap] -> Some TypeMap -> v -> v
- class SupportTermOps (Term h) => SMTWriter h where
  - forallExpr :: [(Text, Some TypeMap)] -> Term h -> Term h
  - existsExpr :: [(Text, Some TypeMap)] -> Term h -> Term h
  - arrayConstant :: Maybe (ArrayConstantFn (Term h))
  - arraySelect :: Term h -> [Term h] -> Term h
  - arrayUpdate :: Term h -> [Term h] -> Term h -> Term h
  - commentCommand :: f h -> Builder -> Command h
  - assertCommand :: f h -> Term h -> Command h
  - assertNamedCommand :: f h -> Term h -> Text -> Command h
  - pushCommand :: f h -> Command h
  - popCommand :: f h -> Command h
  - push2Command :: f h -> Command h
  - pop2Command :: f h -> Command h
  - popManyCommands :: f h -> Int -> [Command h]
  - resetCommand :: f h -> Command h
  - checkCommands :: f h -> [Command h]
  - checkWithAssumptionsCommands :: f h -> [Text] -> [Command h]
  - getUnsatAssumptionsCommand :: f h -> Command h
  - getUnsatCoreCommand :: f h -> Command h
  - getAbductCommand :: f h -> Text -> Term h -> Command h
  - getAbductNextCommand :: f h -> Command h
  - setOptCommand :: f h -> Text -> Text -> Command h
  - declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f h -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command h
  - defineCommand :: forall f (rtp :: BaseType). f h -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term h -> Command h
  - synthFunCommand :: forall f (tp :: BaseType). f h -> Text -> [(Text, Some TypeMap)] -> TypeMap tp -> Command h
  - declareVarCommand :: forall f (tp :: BaseType). f h -> Text -> TypeMap tp -> Command h
  - constraintCommand :: f h -> Term h -> Command h
  - declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t h -> Assignment TypeMap args -> IO ()
  - structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term h] -> Term h
  - structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term h -> Term h
  - stringTerm :: Text -> Term h
  - stringLength :: Term h -> Term h
  - stringIndexOf :: Term h -> Term h -> Term h -> Term h
  - stringContains :: Term h -> Term h -> Term h
  - stringIsPrefixOf :: Term h -> Term h -> Term h
  - stringIsSuffixOf :: Term h -> Term h -> Term h
  - stringSubstring :: Term h -> Term h -> Term h -> Term h
  - stringAppend :: [Term h] -> Term h
  - resetDeclaredStructs :: WriterConn t h -> IO ()
  - writeCommand :: WriterConn t h -> Command h -> IO ()
- class SMTWriter h => SMTReadWriter h where
  - smtEvalFuns :: WriterConn t h -> InputStream Text -> SMTEvalFunctions h
  - smtSatResult :: f h -> WriterConn t h -> IO (SatResult () ())
  - smtUnsatCoreResult :: f h -> WriterConn t h -> IO [Text]
  - smtAbductResult :: f h -> WriterConn t h -> Text -> Term h -> IO String
  - smtAbductNextResult :: f h -> WriterConn t h -> IO String
  - smtUnsatAssumptionsResult :: f h -> WriterConn t h -> IO [(Bool, Text)]
- type SMTEvalBVArrayFn h (w :: Natural) (v :: Natural) = (1 <= w, 1 <= v) => NatRepr w -> NatRepr v -> Term h -> IO (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
- newtype SMTEvalBVArrayWrapper h = SMTEvalBVArrayWrapper {
  - unEvalBVArrayWrapper :: forall (w :: Natural) (v :: Natural). SMTEvalBVArrayFn h w v
  }
- type family Term h
- app :: Builder -> [Builder] -> Builder
- app_list :: Builder -> [Builder] -> Builder
- builder_list :: [Builder] -> Builder
- data WriterConn t h
- connState :: WriterConn t h -> h
- newWriterConn :: OutputStream Text -> InputStream Text -> AcknowledgementAction t cs -> String -> ResponseStrictness -> ProblemFeatures -> SymbolVarBimap t -> cs -> IO (WriterConn t cs)
- resetEntryStack :: WriterConn t h -> IO ()
- popEntryStackToTop :: WriterConn t h -> IO Int
- entryStackHeight :: WriterConn t h -> IO Int
- pushEntryStack :: WriterConn t h -> IO ()
- popEntryStack :: WriterConn t h -> IO ()
- cacheLookupFnNameBimap :: WriterConn t h -> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)
- type family Command h
- addCommand :: SMTWriter h => WriterConn t h -> Command h -> IO ()
- addCommandNoAck :: SMTWriter h => WriterConn t h -> Command h -> IO ()
- addCommands :: SMTWriter h => WriterConn t h -> [Command h] -> IO ()
- mkFreeVar :: forall h t (args :: Ctx BaseType) (rtp :: BaseType). SMTWriter h => WriterConn t h -> Assignment TypeMap args -> TypeMap rtp -> IO Text
- bindVarAsFree :: forall h t (tp :: BaseType). SMTWriter h => WriterConn t h -> ExprBoundVar t tp -> IO ()
- data TypeMap (tp :: BaseType) where
  - BoolTypeMap :: TypeMap 'BaseBoolType
  - IntegerTypeMap :: TypeMap 'BaseIntegerType
  - RealTypeMap :: TypeMap 'BaseRealType
  - BVTypeMap :: forall (w :: Natural). 1 <= w => !(NatRepr w) -> TypeMap ('BaseBVType w)
  - FloatTypeMap :: forall (fpp :: FloatPrecision). !(FloatPrecisionRepr fpp) -> TypeMap ('BaseFloatType fpp)
  - UnicodeTypeMap :: TypeMap ('BaseStringType Unicode)
  - ComplexToStructTypeMap :: TypeMap 'BaseComplexType
  - ComplexToArrayTypeMap :: TypeMap 'BaseComplexType
  - PrimArrayTypeMap :: forall (idxl :: Ctx BaseType) (idx :: BaseType) (tp1 :: BaseType). !(Assignment TypeMap (idxl ::> idx)) -> !(TypeMap tp1) -> TypeMap ('BaseArrayType (idxl ::> idx) tp1)
  - FnArrayTypeMap :: forall (idxl :: Ctx BaseType) (idx :: BaseType) (tp1 :: BaseType). !(Assignment TypeMap (idxl ::> idx)) -> TypeMap tp1 -> TypeMap ('BaseArrayType (idxl ::> idx) tp1)
  - StructTypeMap :: forall (idx :: Ctx BaseType). !(Assignment TypeMap idx) -> TypeMap ('BaseStructType idx)
- typeMap :: forall t h (tp :: BaseType). WriterConn t h -> BaseTypeRepr tp -> Either BaseTypeError (TypeMap tp)
- freshBoundVarName :: forall h t (rtp :: BaseType). SMTWriter h => WriterConn t h -> DefineStyle -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term h -> IO Text
- assumeFormula :: SMTWriter h => WriterConn t h -> Term h -> IO ()
- assumeFormulaWithName :: SMTWriter h => WriterConn t h -> Term h -> Text -> IO ()
- assumeFormulaWithFreshName :: SMTWriter h => WriterConn t h -> Term h -> IO Text
- data DefineStyle
  - = FunctionDefinition
  - | EqualityDefinition
- newtype AcknowledgementAction t h = AckAction {
  - runAckAction :: WriterConn t h -> Command h -> IO ()
  }
- data ResponseStrictness
  - = Lenient
  - | Strict
- parserStrictness :: Maybe (ConfigOption BaseBoolType) -> ConfigOption BaseBoolType -> Config -> IO ResponseStrictness
- nullAcknowledgementAction :: AcknowledgementAction t h
- addSynthFun :: forall h t (args :: Ctx BaseType) (ret :: BaseType). SMTWriter h => WriterConn t h -> ExprSymFn t args ret -> IO ()
- addDeclareVar :: forall h t (tp :: BaseType). SMTWriter h => WriterConn t h -> ExprBoundVar t tp -> IO ()
- addConstraint :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
- assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
- mkSMTTerm :: forall h t (tp :: BaseType). SMTWriter h => WriterConn t h -> Expr t tp -> IO (Term h)
- mkFormula :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO (Term h)
- mkAtomicFormula :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO Text
- data SMTEvalFunctions h = SMTEvalFunctions {
  - smtEvalBool :: Term h -> IO Bool
  - smtEvalBV :: forall (w :: Nat). NatRepr w -> Term h -> IO (BV w)
  - smtEvalReal :: Term h -> IO Rational
  - smtEvalFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term h -> IO (BV (FloatPrecisionBits fpp))
  - smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper h)
  - smtEvalString :: Term h -> IO Text
  }
- smtExprGroundEvalFn :: forall t h. SMTWriter h => WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
- data CollectorResults h a = CollectorResults {
  - crResult :: !a
  - crBindings :: ![(Text, Term h)]
  - crFreeConstants :: ![(Text, Some TypeMap)]
  - crSideConds :: ![Term h]
  }
- mkBaseExpr :: forall h t (tp :: BaseType). SMTWriter h => Expr t tp -> SMTCollector t h (Term h)
- runInSandbox :: SupportTermOps (Term h) => WriterConn t h -> SMTCollector t h a -> IO (CollectorResults h a)
- data RoundingMode
  - = RNE
  - | RNA
  - | RTP
  - | RTN
  - | RTZ

# Type classes

class Num v => SupportTermOps v where Source #

A class of values containing rational and operations.

Minimal complete definition

boolExpr, notExpr, andAll, orAll, (.==), letExpr, ite, termIntegerToReal, termRealToInteger, integerTerm, rationalTerm, (.<=), intAbs, intDiv, intMod, intDivisible, bvTerm, bvNeg, bvAdd, bvSub, bvMul, bvSLe, bvULe, bvSLt, bvULt, bvUDiv, bvURem, bvSDiv, bvSRem, bvAnd, bvOr, bvXor, bvNot, bvShl, bvLshr, bvAshr, bvConcat, bvExtract, floatTerm, floatNeg, floatAbs, floatSqrt, floatAdd, floatSub, floatMul, floatDiv, floatRem, floatFMA, floatEq, floatFpEq, floatLe, floatLt, floatIsNaN, floatIsInf, floatIsZero, floatIsPos, floatIsNeg, floatIsSubnorm, floatIsNorm, floatCast, floatRound, floatFromBinary, bvToFloat, sbvToFloat, realToFloat, floatToBV, floatToSBV, floatToReal, realIsInteger, realDiv, realSin, realCos, realTan, realATan2, realSinh, realCosh, realTanh, realExp, realLog, smtFnApp, fromText

Methods

boolExpr :: Bool -> v Source #

notExpr :: v -> v Source #

andAll :: [v] -> v Source #

orAll :: [v] -> v Source #

(.&&) :: v -> v -> v infixr 3 Source #

(.||) :: v -> v -> v infixr 2 Source #

(.==) :: v -> v -> v infix 4 Source #

Compare two elements for equality.

(./=) :: v -> v -> v infix 4 Source #

Compare two elements for in-equality.

impliesExpr :: v -> v -> v Source #

letExpr :: [(Text, v)] -> v -> v Source #

Create a let expression. This is a "sequential" let, which is syntactic sugar for a nested series of single let bindings. As a consequence, bound variables are in scope for the right-hand-sides of subsequent bindings.

ite :: v -> v -> v -> v Source #

Create an if-then-else expression.

sumExpr :: [v] -> v Source #

Add a list of values together.

termIntegerToReal :: v -> v Source #

Convert an integer expression to a real.

termRealToInteger :: v -> v Source #

Convert a real expression to an integer.

integerTerm :: Integer -> v Source #

Convert an integer to a term.

rationalTerm :: Rational -> v Source #

Convert a rational to a term.

(.<=) :: v -> v -> v infix 4 Source #

Less-then-or-equal

(.<) :: v -> v -> v infix 4 Source #

Less-then

(.>) :: v -> v -> v infix 4 Source #

Greater then

(.>=) :: v -> v -> v infix 4 Source #

Greater then or equal

intAbs :: v -> v Source #

Integer theory terms

intDiv :: v -> v -> v Source #

intMod :: v -> v -> v Source #

intDivisible :: v -> Natural -> v Source #

bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> v Source #

Create expression from bitvector.

bvNeg :: v -> v Source #

bvAdd :: v -> v -> v Source #

bvSub :: v -> v -> v Source #

bvMul :: v -> v -> v Source #

bvSLe :: v -> v -> v Source #

bvULe :: v -> v -> v Source #

bvSLt :: v -> v -> v Source #

bvULt :: v -> v -> v Source #

bvUDiv :: v -> v -> v Source #

bvURem :: v -> v -> v Source #

bvSDiv :: v -> v -> v Source #

bvSRem :: v -> v -> v Source #

bvAnd :: v -> v -> v Source #

bvOr :: v -> v -> v Source #

bvXor :: v -> v -> v Source #

bvNot :: v -> v Source #

bvShl :: v -> v -> v Source #

bvLshr :: v -> v -> v Source #

bvAshr :: v -> v -> v Source #

bvConcat :: v -> v -> v Source #

Concatenate two bitvectors together.

bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> v -> v Source #

`bvExtract w i n v` extracts bits [i..i+n) from `v` as a new bitvector. `v` must contain at least `w` elements, and `i+n` must be less than or equal to `w`. The result has `n` elements. The least significant bit of `v` should have index `0`.

bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> v -> v Source #

`bvTestBit w i x` returns predicate that holds if bit `i` in `x` is set to true. `w` should be the number of bits in `x`.

bvSumExpr :: forall (w :: Nat). NatRepr w -> [v] -> v Source #

floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> v Source #

floatNeg :: v -> v Source #

floatAbs :: v -> v Source #

floatSqrt :: RoundingMode -> v -> v Source #

floatAdd :: RoundingMode -> v -> v -> v Source #

floatSub :: RoundingMode -> v -> v -> v Source #

floatMul :: RoundingMode -> v -> v -> v Source #

floatDiv :: RoundingMode -> v -> v -> v Source #

floatRem :: v -> v -> v Source #

floatFMA :: RoundingMode -> v -> v -> v -> v Source #

floatEq :: v -> v -> v Source #

floatFpEq :: v -> v -> v Source #

floatLe :: v -> v -> v Source #

floatLt :: v -> v -> v Source #

floatIsNaN :: v -> v Source #

floatIsInf :: v -> v Source #

floatIsZero :: v -> v Source #

floatIsPos :: v -> v Source #

floatIsNeg :: v -> v Source #

floatIsSubnorm :: v -> v Source #

floatIsNorm :: v -> v Source #

floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> v -> v Source #

floatRound :: RoundingMode -> v -> v Source #

floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> v -> v Source #

bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> v -> v Source #

sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> v -> v Source #

realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> v -> v Source #

floatToBV :: Natural -> RoundingMode -> v -> v Source #

floatToSBV :: Natural -> RoundingMode -> v -> v Source #

floatToReal :: v -> v Source #

realIsInteger :: v -> v Source #

Predicate that holds if a real number is an integer.

realDiv :: v -> v -> v Source #

realSin :: v -> v Source #

realCos :: v -> v Source #

realTan :: v -> v Source #

realATan2 :: v -> v -> v Source #

realSinh :: v -> v Source #

realCosh :: v -> v Source #

realTanh :: v -> v Source #

realExp :: v -> v Source #

realLog :: v -> v Source #

smtFnApp :: v -> [v] -> v Source #

Apply the arguments to the given function.

smtFnUpdate :: Maybe (v -> [v] -> v -> v) Source #

Update a function value to return a new value at the given point.

This may be Nothing if solver has no builtin function for update.

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> v -> v) Source #

Function for creating a lambda term if output supports it.

Yices support lambda expressions, but SMTLIB2 does not. The function takes arguments and the expression.

fromText :: Text -> v Source #

#### Instances

Instances details

SupportTermOps Term Source # |

Instance details

Defined in What4.Protocol.SMTLib2

Methods

boolExpr :: Bool -> Term Source #

notExpr :: Term -> Term Source #

andAll :: [Term] -> Term Source #

orAll :: [Term] -> Term Source #

(.&&) :: Term -> Term -> Term Source #

(.||) :: Term -> Term -> Term Source #

(.==) :: Term -> Term -> Term Source #

(./=) :: Term -> Term -> Term Source #

impliesExpr :: Term -> Term -> Term Source #

letExpr :: [(Text, Term)] -> Term -> Term Source #

ite :: Term -> Term -> Term -> Term Source #

sumExpr :: [Term] -> Term Source #

termIntegerToReal :: Term -> Term Source #

termRealToInteger :: Term -> Term Source #

integerTerm :: Integer -> Term Source #

rationalTerm :: Rational -> Term Source #

(.<=) :: Term -> Term -> Term Source #

(.<) :: Term -> Term -> Term Source #

(.>) :: Term -> Term -> Term Source #

(.>=) :: Term -> Term -> Term Source #

intAbs :: Term -> Term Source #

intDiv :: Term -> Term -> Term Source #

intMod :: Term -> Term -> Term Source #

intDivisible :: Term -> Natural -> Term Source #

bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> Term Source #

bvNeg :: Term -> Term Source #

bvAdd :: Term -> Term -> Term Source #

bvSub :: Term -> Term -> Term Source #

bvMul :: Term -> Term -> Term Source #

bvSLe :: Term -> Term -> Term Source #

bvULe :: Term -> Term -> Term Source #

bvSLt :: Term -> Term -> Term Source #

bvULt :: Term -> Term -> Term Source #

bvUDiv :: Term -> Term -> Term Source #

bvURem :: Term -> Term -> Term Source #

bvSDiv :: Term -> Term -> Term Source #

bvSRem :: Term -> Term -> Term Source #

bvAnd :: Term -> Term -> Term Source #

bvOr :: Term -> Term -> Term Source #

bvXor :: Term -> Term -> Term Source #

bvNot :: Term -> Term Source #

bvShl :: Term -> Term -> Term Source #

bvLshr :: Term -> Term -> Term Source #

bvAshr :: Term -> Term -> Term Source #

bvConcat :: Term -> Term -> Term Source #

bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> Term -> Term Source #

bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> Term -> Term Source #

bvSumExpr :: forall (w :: Nat). NatRepr w -> [Term] -> Term Source #

floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> Term Source #

floatNeg :: Term -> Term Source #

floatAbs :: Term -> Term Source #

floatSqrt :: RoundingMode -> Term -> Term Source #

floatAdd :: RoundingMode -> Term -> Term -> Term Source #

floatSub :: RoundingMode -> Term -> Term -> Term Source #

floatMul :: RoundingMode -> Term -> Term -> Term Source #

floatDiv :: RoundingMode -> Term -> Term -> Term Source #

floatRem :: Term -> Term -> Term Source #

floatFMA :: RoundingMode -> Term -> Term -> Term -> Term Source #

floatEq :: Term -> Term -> Term Source #

floatFpEq :: Term -> Term -> Term Source #

floatLe :: Term -> Term -> Term Source #

floatLt :: Term -> Term -> Term Source #

floatIsNaN :: Term -> Term Source #

floatIsInf :: Term -> Term Source #

floatIsZero :: Term -> Term Source #

floatIsPos :: Term -> Term Source #

floatIsNeg :: Term -> Term Source #

floatIsSubnorm :: Term -> Term Source #

floatIsNorm :: Term -> Term Source #

floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatRound :: RoundingMode -> Term -> Term Source #

floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term -> Term Source #

bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatToBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToSBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToReal :: Term -> Term Source #

realIsInteger :: Term -> Term Source #

realDiv :: Term -> Term -> Term Source #

realSin :: Term -> Term Source #

realCos :: Term -> Term Source #

realTan :: Term -> Term Source #

realATan2 :: Term -> Term -> Term Source #

realSinh :: Term -> Term Source #

realCosh :: Term -> Term Source #

realTanh :: Term -> Term Source #

realExp :: Term -> Term Source #

realLog :: Term -> Term Source #

smtFnApp :: Term -> [Term] -> Term Source #

smtFnUpdate :: Maybe (Term -> [Term] -> Term -> Term) Source #

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> Term -> Term) Source #

fromText :: Text -> Term Source #

type ArrayConstantFn v Source #

Arguments

= [Some TypeMap] | Type for indices
-> Some TypeMap | Type for value.
-> v | Constant to assign all values.
-> v |

class SupportTermOps (Term h) => SMTWriter h where Source #

Typeclass need to generate SMTLIB commands.

Minimal complete definition

forallExpr, existsExpr, arraySelect, arrayUpdate, commentCommand, assertCommand, assertNamedCommand, pushCommand, popCommand, push2Command, pop2Command, resetCommand, checkCommands, checkWithAssumptionsCommands, getUnsatAssumptionsCommand, getUnsatCoreCommand, getAbductCommand, getAbductNextCommand, setOptCommand, declareCommand, defineCommand, synthFunCommand, declareVarCommand, constraintCommand, declareStructDatatype, structCtor, structProj, stringTerm, stringLength, stringIndexOf, stringContains, stringIsPrefixOf, stringIsSuffixOf, stringSubstring, stringAppend, resetDeclaredStructs, writeCommand

Methods

forallExpr :: [(Text, Some TypeMap)] -> Term h -> Term h Source #

Create a forall expression

existsExpr :: [(Text, Some TypeMap)] -> Term h -> Term h Source #

Create an exists expression

arrayConstant :: Maybe (ArrayConstantFn (Term h)) Source #

Create a constant array

This may return Nothing if the solver does not support constant arrays.

arraySelect :: Term h -> [Term h] -> Term h Source #

Select an element from an array

arrayUpdate :: Term h -> [Term h] -> Term h -> Term h Source #

'arrayUpdate a i v' returns an array that contains value `v` at index `i`, and the same value as in `a` at every other index.

commentCommand :: f h -> Builder -> Command h Source #

Create a command that just defines a comment.

assertCommand :: f h -> Term h -> Command h Source #

Create a command that asserts a formula.

assertNamedCommand :: f h -> Term h -> Text -> Command h Source #

Create a command that asserts a formula and attaches the given name to it (primarily for the purposes of later reporting unsatisfiable cores).

pushCommand :: f h -> Command h Source #

Generates command `(push 1)` that opens the corresponding assertion frame

popCommand :: f h -> Command h Source #

Generates command `(pop 1)` that closes the corresponding assertion frame

push2Command :: f h -> Command h Source #

Generates command `(push 2)` that opens the corresponding assertion frame

pop2Command :: f h -> Command h Source #

Generates command `(pop 2)` that closes the corresponding assertion frame, used for abduction

popManyCommands :: f h -> Int -> [Command h] Source #

Pop several scopes.

resetCommand :: f h -> Command h Source #

Reset the solver state, forgetting all pushed frames and assertions

checkCommands :: f h -> [Command h] Source #

Check if the current set of assumption is satisfiable. May require multiple commands. The intial commands require an ack. The last one does not.

checkWithAssumptionsCommands :: f h -> [Text] -> [Command h] Source #

Check if a collection of assumptions is satisfiable in the current context. The assumptions must be given as the names of literals already in scope.

getUnsatAssumptionsCommand :: f h -> Command h Source #

Ask the solver to return an unsatisfiable core from among the assumptions passed into the previous "check with assumptions" command.

getUnsatCoreCommand :: f h -> Command h Source #

Ask the solver to return an unsatisfiable core from among the named assumptions previously asserted using the `assertNamedCommand` after an unsatisfiable `checkCommand`.

getAbductCommand :: f h -> Text -> Term h -> Command h Source #

Ask the solver to return an abduct

getAbductNextCommand :: f h -> Command h Source #

Ask the solver for the next abduct, used after a get-abduct command

setOptCommand :: f h -> Text -> Text -> Command h Source #

Set an option/parameter.

declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f h -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command h Source #

Declare a new symbol with the given name, arguments types, and result type.

defineCommand Source #

Arguments

:: forall f (rtp :: BaseType). f h |
-> Text | Name of variable
-> [(Text, Some TypeMap)] |
-> TypeMap rtp |
-> Term h |
-> Command h |

Define a new symbol with the given name, arguments, result type, and associated expression.

The argument contains the variable name and the type of the variable.

synthFunCommand :: forall f (tp :: BaseType). f h -> Text -> [(Text, Some TypeMap)] -> TypeMap tp -> Command h Source #

Declare a new SyGuS function to synthesize with the given name, arguments, and result type.

declareVarCommand :: forall f (tp :: BaseType). f h -> Text -> TypeMap tp -> Command h Source #

Declare a new SyGuS universal variables with the given name and type.

constraintCommand :: f h -> Term h -> Command h Source #

Add a SyGuS formula to the set of synthesis constraints.

declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t h -> Assignment TypeMap args -> IO () Source #

Declare a struct datatype if is has not been already given the number of arguments in the struct.

structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term h] -> Term h Source #

Build a struct term with the given types and fields

structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term h -> Term h Source #

Project a field from a struct with the given types

stringTerm :: Text -> Term h Source #

Produce a term representing a string literal

stringLength :: Term h -> Term h Source #

Compute the length of a term

stringIndexOf :: Term h -> Term h -> Term h -> Term h Source #

`stringIndexOf s t i` computes the first index following or at i where `t` appears within `s` as a substring, or -1 if no such index exists

stringContains :: Term h -> Term h -> Term h Source #

Test if the first string contains the second string

stringIsPrefixOf :: Term h -> Term h -> Term h Source #

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

stringIsSuffixOf :: Term h -> Term h -> Term h Source #

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

stringSubstring :: Term h -> Term h -> Term h -> Term h Source #

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

stringAppend :: [Term h] -> Term h Source #

Append the given strings

resetDeclaredStructs :: WriterConn t h -> IO () Source #

Forget all previously-declared struct types.

writeCommand :: WriterConn t h -> Command h -> IO () Source #

Write a command to the connection.

#### Instances

Instances details

SMTWriter Connection Source # |

Instance details

Defined in What4.Solver.Yices

Methods

forallExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection Source #

existsExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection Source #

arrayConstant :: Maybe (ArrayConstantFn (Term Connection)) Source #

arraySelect :: Term Connection -> [Term Connection] -> Term Connection Source #

arrayUpdate :: Term Connection -> [Term Connection] -> Term Connection -> Term Connection Source #

commentCommand :: f Connection -> Builder -> Command Connection Source #

assertCommand :: f Connection -> Term Connection -> Command Connection Source #

assertNamedCommand :: f Connection -> Term Connection -> Text -> Command Connection Source #

pushCommand :: f Connection -> Command Connection Source #

popCommand :: f Connection -> Command Connection Source #

push2Command :: f Connection -> Command Connection Source #

pop2Command :: f Connection -> Command Connection Source #

popManyCommands :: f Connection -> Int -> [Command Connection] Source #

resetCommand :: f Connection -> Command Connection Source #

checkCommands :: f Connection -> [Command Connection] Source #

checkWithAssumptionsCommands :: f Connection -> [Text] -> [Command Connection] Source #

getUnsatAssumptionsCommand :: f Connection -> Command Connection Source #

getUnsatCoreCommand :: f Connection -> Command Connection Source #

getAbductCommand :: f Connection -> Text -> Term Connection -> Command Connection Source #

getAbductNextCommand :: f Connection -> Command Connection Source #

setOptCommand :: f Connection -> Text -> Text -> Command Connection Source #

declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f Connection -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command Connection Source #

defineCommand :: forall f (rtp :: BaseType). f Connection -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term Connection -> Command Connection Source #

synthFunCommand :: forall f (tp :: BaseType). f Connection -> Text -> [(Text, Some TypeMap)] -> TypeMap tp -> Command Connection Source #

declareVarCommand :: forall f (tp :: BaseType). f Connection -> Text -> TypeMap tp -> Command Connection Source #

constraintCommand :: f Connection -> Term Connection -> Command Connection Source #

declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t Connection -> Assignment TypeMap args -> IO () Source #

structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term Connection] -> Term Connection Source #

structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term Connection -> Term Connection Source #

stringTerm :: Text -> Term Connection Source #

stringLength :: Term Connection -> Term Connection Source #

stringIndexOf :: Term Connection -> Term Connection -> Term Connection -> Term Connection Source #

stringContains :: Term Connection -> Term Connection -> Term Connection Source #

stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection Source #

stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection Source #

stringSubstring :: Term Connection -> Term Connection -> Term Connection -> Term Connection Source #

stringAppend :: [Term Connection] -> Term Connection Source #

resetDeclaredStructs :: WriterConn t Connection -> IO () Source #

writeCommand :: WriterConn t Connection -> Command Connection -> IO () Source #

SMTLib2Tweaks a => SMTWriter (Writer a) Source # |

Instance details

Defined in What4.Protocol.SMTLib2

Methods

forallExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a) Source #

existsExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a) Source #

arrayConstant :: Maybe (ArrayConstantFn (Term (Writer a))) Source #

arraySelect :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a) Source #

arrayUpdate :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a) -> Term (Writer a) Source #

commentCommand :: f (Writer a) -> Builder -> Command (Writer a) Source #

assertCommand :: f (Writer a) -> Term (Writer a) -> Command (Writer a) Source #

assertNamedCommand :: f (Writer a) -> Term (Writer a) -> Text -> Command (Writer a) Source #

pushCommand :: f (Writer a) -> Command (Writer a) Source #

popCommand :: f (Writer a) -> Command (Writer a) Source #

push2Command :: f (Writer a) -> Command (Writer a) Source #

pop2Command :: f (Writer a) -> Command (Writer a) Source #

popManyCommands :: f (Writer a) -> Int -> [Command (Writer a)] Source #

resetCommand :: f (Writer a) -> Command (Writer a) Source #

checkCommands :: f (Writer a) -> [Command (Writer a)] Source #

checkWithAssumptionsCommands :: f (Writer a) -> [Text] -> [Command (Writer a)] Source #

getUnsatAssumptionsCommand :: f (Writer a) -> Command (Writer a) Source #

getUnsatCoreCommand :: f (Writer a) -> Command (Writer a) Source #

getAbductCommand :: f (Writer a) -> Text -> Term (Writer a) -> Command (Writer a) Source #

getAbductNextCommand :: f (Writer a) -> Command (Writer a) Source #

setOptCommand :: f (Writer a) -> Text -> Text -> Command (Writer a) Source #

declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f (Writer a) -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command (Writer a) Source #

defineCommand :: forall f (rtp :: BaseType). f (Writer a) -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term (Writer a) -> Command (Writer a) Source #

synthFunCommand :: forall f (tp :: BaseType). f (Writer a) -> Text -> [(Text, Some TypeMap)] -> TypeMap tp -> Command (Writer a) Source #

declareVarCommand :: forall f (tp :: BaseType). f (Writer a) -> Text -> TypeMap tp -> Command (Writer a) Source #

constraintCommand :: f (Writer a) -> Term (Writer a) -> Command (Writer a) Source #

declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t (Writer a) -> Assignment TypeMap args -> IO () Source #

structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term (Writer a)] -> Term (Writer a) Source #

structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term (Writer a) -> Term (Writer a) Source #

stringTerm :: Text -> Term (Writer a) Source #

stringLength :: Term (Writer a) -> Term (Writer a) Source #

stringIndexOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringContains :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringIsPrefixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringIsSuffixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringSubstring :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringAppend :: [Term (Writer a)] -> Term (Writer a) Source #

resetDeclaredStructs :: WriterConn t (Writer a) -> IO () Source #

writeCommand :: WriterConn t (Writer a) -> Command (Writer a) -> IO () Source #

class SMTWriter h => SMTReadWriter h where Source #

Used when we need two way communication with the solver.

Methods

smtEvalFuns :: WriterConn t h -> InputStream Text -> SMTEvalFunctions h Source #

Get functions for parsing values out of the solver.

smtSatResult :: f h -> WriterConn t h -> IO (SatResult () ()) Source #

Parse a set result from the solver's response.

smtUnsatCoreResult :: f h -> WriterConn t h -> IO [Text] Source #

Parse a list of names of assumptions that form an unsatisfiable core. These correspond to previously-named assertions.

smtAbductResult :: f h -> WriterConn t h -> Text -> Term h -> IO String Source #

Parse an abduct returned by the get-abduct command

smtAbductNextResult :: f h -> WriterConn t h -> IO String Source #

Parse an abduct returned by the get-abduct-next command

smtUnsatAssumptionsResult :: f h -> WriterConn t h -> IO [(Bool, Text)] Source #

Parse a list of names of assumptions that form an unsatisfiable core. The boolean indicates the polarity of the atom: true for an ordinary atom, false for a negated atom.

#### Instances

Instances details

SMTReadWriter Connection Source # |

Instance details

Defined in What4.Solver.Yices

Methods

smtEvalFuns :: WriterConn t Connection -> InputStream Text -> SMTEvalFunctions Connection Source #

smtSatResult :: f Connection -> WriterConn t Connection -> IO (SatResult () ()) Source #

smtUnsatCoreResult :: f Connection -> WriterConn t Connection -> IO [Text] Source #

smtAbductResult :: f Connection -> WriterConn t Connection -> Text -> Term Connection -> IO String Source #

smtAbductNextResult :: f Connection -> WriterConn t Connection -> IO String Source #

smtUnsatAssumptionsResult :: f Connection -> WriterConn t Connection -> IO [(Bool, Text)] Source #

SMTLib2Tweaks a => SMTReadWriter (Writer a) Source # |

Instance details

Defined in What4.Protocol.SMTLib2

Methods

smtEvalFuns :: WriterConn t (Writer a) -> InputStream Text -> SMTEvalFunctions (Writer a) Source #

smtSatResult :: f (Writer a) -> WriterConn t (Writer a) -> IO (SatResult () ()) Source #

smtUnsatCoreResult :: f (Writer a) -> WriterConn t (Writer a) -> IO [Text] Source #

smtAbductResult :: f (Writer a) -> WriterConn t (Writer a) -> Text -> Term (Writer a) -> IO String Source #

smtAbductNextResult :: f (Writer a) -> WriterConn t (Writer a) -> IO String Source #

smtUnsatAssumptionsResult :: f (Writer a) -> WriterConn t (Writer a) -> IO [(Bool, Text)] Source #

type SMTEvalBVArrayFn h (w :: Natural) (v :: Natural) = (1 <= w, 1 <= v) => NatRepr w -> NatRepr v -> Term h -> IO (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))) Source #

newtype SMTEvalBVArrayWrapper h Source #

Constructors

SMTEvalBVArrayWrapper |

Fields

- unEvalBVArrayWrapper :: forall (w :: Natural) (v :: Natural). SMTEvalBVArrayFn h w v

# Terms

type family Term h Source #

A term in the output language.

#### Instances

Instances details

type Term Connection Source # |
Instance details Defined in What4.Solver.Yices type Term Connection
type Term (Writer a) Source # |
Instance details Defined in What4.Protocol.SMTLib2 type Term (Writer a) = Term

app :: Builder -> [Builder] -> Builder Source #

app_list :: Builder -> [Builder] -> Builder Source #

builder_list :: [Builder] -> Builder Source #

# SMTWriter

data WriterConn t h Source #

connState :: WriterConn t h -> h Source #

The specific connection information.

newWriterConn Source #

Arguments

:: OutputStream Text | Stream to write queries onto
-> InputStream Text | Input stream to read responses from (may be the `nullInput` stream if no responses are expected)
-> AcknowledgementAction t cs | An action to consume solver acknowledgement responses
-> String | Name of solver for reporting purposes.
-> ResponseStrictness | Be strict in parsing responses?
-> ProblemFeatures | Indicates what features are supported by the solver.
-> SymbolVarBimap t | A bijective mapping between variables and their canonical name (if any).
-> cs | State information specific to the type of connection
-> IO (WriterConn t cs) |

resetEntryStack :: WriterConn t h -> IO () Source #

Clear the entry stack, and start with a fresh one.

popEntryStackToTop :: WriterConn t h -> IO Int Source #

Pop all but the topmost stack entry. Return the number of entries on the stack prior to popping.

entryStackHeight :: WriterConn t h -> IO Int Source #

Return the number of pushed stack frames. Note, this is one fewer than the number of entries in the stack beacuse the base entry is the top-level context that is not in the scope of any push.

pushEntryStack :: WriterConn t h -> IO () Source #

Push a new frame to the stack for maintaining the writer cache.

popEntryStack :: WriterConn t h -> IO () Source #

cacheLookupFnNameBimap :: WriterConn t h -> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text) Source #

Construct a function/name bimap. Each function is associated with its cached name if there is one, otherwise with its original name.

type family Command h Source #

#### Instances

Instances details

type Command Connection Source # |
Instance details Defined in What4.Solver.Yices type Command Connection
type Command (Writer a) Source # |
Instance details Defined in What4.Protocol.SMTLib2 type Command (Writer a) = Command

addCommand :: SMTWriter h => WriterConn t h -> Command h -> IO () Source #

Write a command to the connection along with position information if it differs from the last position.

addCommandNoAck :: SMTWriter h => WriterConn t h -> Command h -> IO () Source #

addCommands :: SMTWriter h => WriterConn t h -> [Command h] -> IO () Source #

Write a sequence of commands. All but the last should have acknowledgement.

mkFreeVar :: forall h t (args :: Ctx BaseType) (rtp :: BaseType). SMTWriter h => WriterConn t h -> Assignment TypeMap args -> TypeMap rtp -> IO Text Source #

Create a new variable with the given name.

bindVarAsFree :: forall h t (tp :: BaseType). SMTWriter h => WriterConn t h -> ExprBoundVar t tp -> IO () Source #

Consider the bound variable as free within the current assumption frame.

data TypeMap (tp :: BaseType) where Source #

`TypeMap` defines how a given `BaseType` maps to an SMTLIB type.

It is necessary as there may be several ways in which a base type can be encoded.

Constructors

BoolTypeMap :: TypeMap 'BaseBoolType |
IntegerTypeMap :: TypeMap 'BaseIntegerType |
RealTypeMap :: TypeMap 'BaseRealType |
BVTypeMap :: forall (w :: Natural). 1 <= w => !(NatRepr w) -> TypeMap ('BaseBVType w) |
FloatTypeMap :: forall (fpp :: FloatPrecision). !(FloatPrecisionRepr fpp) -> TypeMap ('BaseFloatType fpp) |
UnicodeTypeMap :: TypeMap ('BaseStringType Unicode) |
ComplexToStructTypeMap :: TypeMap 'BaseComplexType |
ComplexToArrayTypeMap :: TypeMap 'BaseComplexType |
PrimArrayTypeMap :: forall (idxl :: Ctx BaseType) (idx :: BaseType) (tp1 :: BaseType). !(Assignment TypeMap (idxl ::> idx)) -> !(TypeMap tp1) -> TypeMap ('BaseArrayType (idxl ::> idx) tp1) |
FnArrayTypeMap :: forall (idxl :: Ctx BaseType) (idx :: BaseType) (tp1 :: BaseType). !(Assignment TypeMap (idxl ::> idx)) -> TypeMap tp1 -> TypeMap ('BaseArrayType (idxl ::> idx) tp1) |
StructTypeMap :: forall (idx :: Ctx BaseType). !(Assignment TypeMap idx) -> TypeMap ('BaseStructType idx) |

#### Instances

Instances details

TestEquality TypeMap Source # |
Instance details Defined in What4.Protocol.SMTWriter Methods testEquality :: forall (a :: BaseType) (b :: BaseType). TypeMap a -> TypeMap b -> Maybe (a :~: b) Source #
ShowF TypeMap Source # |
Instance details Defined in What4.Protocol.SMTWriter Methods withShow :: forall p q (tp :: BaseType) a. p TypeMap -> q tp -> (Show (TypeMap tp) => a) -> a Source # showF :: forall (tp :: BaseType). TypeMap tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> TypeMap tp -> String -> String Source #
Show (TypeMap a) Source # |
Instance details Defined in What4.Protocol.SMTWriter Methods showsPrec :: Int -> TypeMap a -> ShowS Source # show :: TypeMap a -> String Source # showList :: [TypeMap a] -> ShowS Source #
Eq (TypeMap tp) Source # |
Instance details Defined in What4.Protocol.SMTWriter Methods (==) :: TypeMap tp -> TypeMap tp -> Bool Source # (/=) :: TypeMap tp -> TypeMap tp -> Bool Source #

typeMap :: forall t h (tp :: BaseType). WriterConn t h -> BaseTypeRepr tp -> Either BaseTypeError (TypeMap tp) Source #

Given a solver connection and a base type repr, `typeMap` attempts to find the best encoding for a variable of that type supported by teh solver.

freshBoundVarName Source #

Arguments

:: forall h t (rtp :: BaseType). SMTWriter h |
=> WriterConn t h |
-> DefineStyle |
-> [(Text, Some TypeMap)] | Names of variables in term and associated type.
-> TypeMap rtp | Type of expression.
-> Term h |
-> IO Text |

Create a variable name eqivalent to the given expression.

assumeFormula :: SMTWriter h => WriterConn t h -> Term h -> IO () Source #

Assume that the given formula holds.

assumeFormulaWithName :: SMTWriter h => WriterConn t h -> Term h -> Text -> IO () Source #

assumeFormulaWithFreshName :: SMTWriter h => WriterConn t h -> Term h -> IO Text Source #

data DefineStyle Source #

Constructors

FunctionDefinition |
EqualityDefinition |

#### Instances

Instances details

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

newtype AcknowledgementAction t h Source #

An action for consuming an acknowledgement message from the solver, if it is configured to produce ack messages.

Constructors

AckAction |

Fields

- runAckAction :: WriterConn t h -> Command h -> IO ()

data ResponseStrictness Source #

Strictness level for parsing solver responses.

Constructors

Lenient | allows other output preceeding recognized solver responses
Strict | parse _only_ recognized solver responses; fail on anything else

#### Instances

Instances details

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

parserStrictness :: Maybe (ConfigOption BaseBoolType) -> ConfigOption BaseBoolType -> Config -> IO ResponseStrictness Source #

Given an optional override configuration option, return the SMT response parsing strictness that should be applied based on the override or thedefault strictSMTParsing configuration.

nullAcknowledgementAction :: AcknowledgementAction t h Source #

An acknowledgement action that does nothing

# SyGuS

addSynthFun :: forall h t (args :: Ctx BaseType) (ret :: BaseType). SMTWriter h => WriterConn t h -> ExprSymFn t args ret -> IO () Source #

addDeclareVar :: forall h t (tp :: BaseType). SMTWriter h => WriterConn t h -> ExprBoundVar t tp -> IO () Source #

addConstraint :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO () Source #

# SMTWriter operations

assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO () Source #

Write assume formula predicates for asserting predicate holds.

mkSMTTerm :: forall h t (tp :: BaseType). SMTWriter h => WriterConn t h -> Expr t tp -> IO (Term h) Source #

Write a expression to SMT

mkFormula :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO (Term h) Source #

Write a logical expression.

mkAtomicFormula :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO Text Source #

data SMTEvalFunctions h Source #

Constructors

SMTEvalFunctions |

Fields

- smtEvalBool :: Term h -> IO Bool

  Given a SMT term for a Boolean value, this should return an indication of whether the term is assigned true or false.

- smtEvalBV :: forall (w :: Nat). NatRepr w -> Term h -> IO (BV w)

  Given a bitwidth, and a SMT term for a bitvector with that bitwidth, this should return an unsigned integer with the value of that bitvector.

- smtEvalReal :: Term h -> IO Rational

  Given a SMT term for real value, this should return a rational value for that term.

- smtEvalFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term h -> IO (BV (FloatPrecisionBits fpp))

  Given floating point format, and an SMT term for a floating-point value in that format, this returns an unsigned integer with the bits of the IEEE-754 representation.

- smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper h)

  If `Just`, a function to read arrays whose domain and codomain are both bitvectors. If `Nothing`, signifies that we should fall back to index-selection representation of arrays.

- smtEvalString :: Term h -> IO Text

  Given a SMT term representing as sequence of bytes, return the value as a bytestring.

smtExprGroundEvalFn Source #

Arguments

:: forall t h. SMTWriter h |
=> WriterConn t h | Connection to SMT solver.
-> SMTEvalFunctions h |
-> IO (GroundEvalFn t) |

The function creates a function for evaluating elts to concrete values given a connection to an SMT solver along with some functions for evaluating different types of terms to concrete values.

data CollectorResults h a Source #

This describes the result that was collected from the solver.

Constructors

CollectorResults |

Fields

- crResult :: !a

  Result from sandboxed computation.

- crBindings :: ![(Text, Term h)]

  List of bound variables.

- crFreeConstants :: ![(Text, Some TypeMap)]

  Constants added during generation.

- crSideConds :: ![Term h]

  List of Boolean predicates asserted by collector.

mkBaseExpr :: forall h t (tp :: BaseType). SMTWriter h => Expr t tp -> SMTCollector t h (Term h) Source #

Convert an element to a base expression.

runInSandbox :: SupportTermOps (Term h) => WriterConn t h -> SMTCollector t h a -> IO (CollectorResults h a) Source #

This runs the side collector and collects the results.

# Reexports

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 |

Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.6.3-9uBVkRxr1Ru1evGDxWAmM9" '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))))

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.6.3-9uBVkRxr1Ru1evGDxWAmM9" '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))))