What4.Protocol.SMTWriter

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.

Type classes

class Num v => SupportTermOps v where

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, realATan2, realSinh, realCosh, realExp, realLog, smtFnApp, fromText

Methods

boolExpr :: Bool -> v

notExpr :: v -> v

andAll :: [v] -> v

orAll :: [v] -> v

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

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

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

Compare two elements for equality.

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

Compare two elements for in-equality.

impliesExpr :: v -> v -> v

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

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

Create an if-then-else expression.

sumExpr :: [v] -> v

Add a list of values together.

termIntegerToReal :: v -> v

Convert an integer expression to a real.

termRealToInteger :: v -> v

Convert a real expression to an integer.

integerTerm :: Integer -> v

Convert an integer to a term.

rationalTerm :: Rational -> v

Convert a rational to a term.

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

Less-then-or-equal

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

Less-then

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

Greater then

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

Greater then or equal

intAbs :: v -> v

Integer theory terms

intDiv :: v -> v -> v

intMod :: v -> v -> v

intDivisible :: v -> Natural -> v

bvTerm :: NatRepr w -> BV w -> v

Create expression from bitvector.

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

Concatenate two bitvectors together.

bvExtract :: NatRepr w -> Natural -> Natural -> v -> v

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 :: NatRepr w -> Natural -> v -> v

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 :: NatRepr w -> [v] -> v

floatTerm :: 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 :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v

floatRound :: RoundingMode -> v -> v

floatFromBinary :: FloatPrecisionRepr fpp -> v -> v

bvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v

sbvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v

realToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v

floatToBV :: Natural -> RoundingMode -> v -> v

floatToSBV :: Natural -> RoundingMode -> v -> v

floatToReal :: v -> v

realIsInteger :: v -> v

Predicate that holds if a real number is an integer.

realDiv :: v -> v -> v

realSin :: v -> v

realCos :: v -> v

realATan2 :: v -> v -> v

realSinh :: v -> v

realCosh :: v -> v

realExp :: v -> v

realLog :: v -> v

smtFnApp :: v -> [v] -> v

Apply the arguments to the given function.

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

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)

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

Instances

SupportTermOps Term

Defined in What4.Protocol.SMTLib2

Methods

boolExpr :: Bool -> Term

notExpr :: Term -> Term

andAll :: [Term] -> Term

orAll :: [Term] -> Term

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

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

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

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

impliesExpr :: Term -> Term -> Term

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

ite :: Term -> Term -> Term -> Term

sumExpr :: [Term] -> Term

termIntegerToReal :: Term -> Term

termRealToInteger :: Term -> Term

integerTerm :: Integer -> Term

rationalTerm :: Rational -> Term

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

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

(.>) :: Term -> Term -> Term

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

intAbs :: Term -> Term

intDiv :: Term -> Term -> Term

intMod :: Term -> Term -> Term

intDivisible :: Term -> Natural -> Term

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

bvNeg :: Term -> Term

bvAdd :: Term -> Term -> Term

bvSub :: Term -> Term -> Term

bvMul :: Term -> Term -> Term

bvSLe :: Term -> Term -> Term

bvULe :: Term -> Term -> Term

bvSLt :: Term -> Term -> Term

bvULt :: Term -> Term -> Term

bvUDiv :: Term -> Term -> Term

bvURem :: Term -> Term -> Term

bvSDiv :: Term -> Term -> Term

bvSRem :: Term -> Term -> Term

bvAnd :: Term -> Term -> Term

bvOr :: Term -> Term -> Term

bvXor :: Term -> Term -> Term

bvNot :: Term -> Term

bvShl :: Term -> Term -> Term

bvLshr :: Term -> Term -> Term

bvAshr :: Term -> Term -> Term

bvConcat :: Term -> Term -> Term

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

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

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

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

floatNeg :: Term -> Term

floatAbs :: Term -> Term

floatSqrt :: RoundingMode -> Term -> Term

floatAdd :: RoundingMode -> Term -> Term -> Term

floatSub :: RoundingMode -> Term -> Term -> Term

floatMul :: RoundingMode -> Term -> Term -> Term

floatDiv :: RoundingMode -> Term -> Term -> Term

floatRem :: Term -> Term -> Term

floatFMA :: RoundingMode -> Term -> Term -> Term -> Term

floatEq :: Term -> Term -> Term

floatFpEq :: Term -> Term -> Term

floatLe :: Term -> Term -> Term

floatLt :: Term -> Term -> Term

floatIsNaN :: Term -> Term

floatIsInf :: Term -> Term

floatIsZero :: Term -> Term

floatIsPos :: Term -> Term

floatIsNeg :: Term -> Term

floatIsSubnorm :: Term -> Term

floatIsNorm :: Term -> Term

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

floatRound :: RoundingMode -> Term -> Term

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

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

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

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

floatToBV :: Natural -> RoundingMode -> Term -> Term

floatToSBV :: Natural -> RoundingMode -> Term -> Term

floatToReal :: Term -> Term

realIsInteger :: Term -> Term

realDiv :: Term -> Term -> Term

realSin :: Term -> Term

realCos :: Term -> Term

realATan2 :: Term -> Term -> Term

realSinh :: Term -> Term

realCosh :: Term -> Term

realExp :: Term -> Term

realLog :: Term -> Term

smtFnApp :: Term -> [Term] -> Term

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

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

fromText :: Text -> Term

type ArrayConstantFn v

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

Typeclass need to generate SMTLIB commands.

Minimal complete definition

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

Methods

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

Create a forall expression

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

Create an exists expression

arrayConstant :: Maybe (ArrayConstantFn (Term h))

Create a constant array

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

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

Select an element from an array

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

'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

Create a command that just defines a comment.

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

Create a command that asserts a formula.

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

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

Push 1 new scope

popCommand :: f h -> Command h

Pop 1 existing scope

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

Pop several scopes.

resetCommand :: f h -> Command h

Reset the solver state, forgetting all pushed frames and assertions

checkCommands :: f h -> [Command h]

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]

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

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

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

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

Set an option/parameter.

declareCommand :: f h -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command h

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

defineCommand

Arguments

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

declareStructDatatype :: WriterConn t h -> Assignment TypeMap args -> IO ()

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

structCtor :: Assignment TypeMap args -> [Term h] -> Term h

Build a struct term with the given types and fields

structProj :: Assignment TypeMap args -> Index args tp -> Term h -> Term h

Project a field from a struct with the given types

stringTerm :: ByteString -> Term h

Produce a term representing a string literal

stringLength :: Term h -> Term h

Compute the length of a term

stringIndexOf :: Term h -> Term h -> Term h -> Term h

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

Test if the first string contains the second string

stringIsPrefixOf :: Term h -> Term h -> Term h

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

stringIsSuffixOf :: Term h -> Term h -> Term h

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

stringSubstring :: Term h -> Term h -> Term h -> Term h

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

Append the given strings

resetDeclaredStructs :: WriterConn t h -> IO ()

Forget all previously-declared struct types.

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

Write a command to the connection.

Instances

SMTWriter Connection

Defined in What4.Solver.Yices

Methods

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

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

arrayConstant :: Maybe (ArrayConstantFn (Term Connection))

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

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

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

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

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

pushCommand :: f Connection -> Command Connection

popCommand :: f Connection -> Command Connection

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

resetCommand :: f Connection -> Command Connection

checkCommands :: f Connection -> [Command Connection]

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

getUnsatAssumptionsCommand :: f Connection -> Command Connection

getUnsatCoreCommand :: f Connection -> Command Connection

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

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

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

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

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

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

stringTerm :: ByteString -> Term Connection

stringLength :: Term Connection -> Term Connection

stringIndexOf :: Term Connection -> Term Connection -> Term Connection -> Term Connection

stringContains :: Term Connection -> Term Connection -> Term Connection

stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection

stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection

stringSubstring :: Term Connection -> Term Connection -> Term Connection -> Term Connection

stringAppend :: [Term Connection] -> Term Connection

resetDeclaredStructs :: WriterConn t Connection -> IO ()

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

SMTLib2Tweaks a => SMTWriter (Writer a)

Defined in What4.Protocol.SMTLib2

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

stringTerm :: ByteString -> Term (Writer a)

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

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

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

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

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

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

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

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

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

class SMTWriter h => SMTReadWriter h where

Used when we need two way communication with the solver.

Methods

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

Get functions for parsing values out of the solver.

smtSatResult :: f h -> InputStream Text -> IO (SatResult () ())

Parse a set result from the solver's response.

smtUnsatCoreResult :: f h -> InputStream Text -> IO [Text]

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

smtUnsatAssumptionsResult :: f h -> InputStream Text -> IO [(Bool, Text)]

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

SMTReadWriter Connection

Defined in What4.Solver.Yices

Methods

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

smtSatResult :: f Connection -> InputStream Text -> IO (SatResult () ())

smtUnsatCoreResult :: f Connection -> InputStream Text -> IO [Text]

smtUnsatAssumptionsResult :: f Connection -> InputStream Text -> IO [(Bool, Text)]

SMTLib2Tweaks a => SMTReadWriter (Writer a)

Defined in What4.Protocol.SMTLib2

Methods

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

smtSatResult :: f (Writer a) -> InputStream Text -> IO (SatResult () ())

smtUnsatCoreResult :: f (Writer a) -> InputStream Text -> IO [Text]

smtUnsatAssumptionsResult :: f (Writer a) -> InputStream Text -> IO [(Bool, Text)]

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

newtype SMTEvalBVArrayWrapper h

Constructors

SMTEvalBVArrayWrapper

Fields

• unEvalBVArrayWrapper :: forall w v. SMTEvalBVArrayFn h w v

Terms

type family Term (h :: Type) :: Type

A term in the output language.

Instances

type Term Connection

Defined in What4.Solver.Yices

type Term Connection

type Term (Writer a)

Defined in What4.Protocol.SMTLib2

type Term (Writer a) = Term

app :: Builder -> [Builder] -> Builder

app_list :: Builder -> [Builder] -> Builder

builder_list :: [Builder] -> Builder

SMTWriter

data WriterConn t (h :: Type)

connState :: WriterConn t h -> h

The specific connection information.

newWriterConn

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.

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

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

popEntryStackToTop :: WriterConn t h -> IO Int

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

entryStackHeight :: WriterConn t h -> IO Int

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

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

popEntryStack :: WriterConn t h -> IO ()

type family Command (h :: Type) :: Type

Instances

type Command Connection

Defined in What4.Solver.Yices

type Command Connection

type Command (Writer a)

Defined in What4.Protocol.SMTLib2

type Command (Writer a) = Command

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

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

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

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

mkFreeVar :: SMTWriter h => WriterConn t h -> Assignment TypeMap args -> TypeMap rtp -> IO Text

Create a new variable with the given name.

bindVarAsFree :: SMTWriter h => WriterConn t h -> ExprBoundVar t tp -> IO ()

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

data TypeMap (tp :: BaseType) where

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 :: 1 <= w => !(NatRepr w) -> TypeMap (BaseBVType w)

FloatTypeMap :: !(FloatPrecisionRepr fpp) -> TypeMap (BaseFloatType fpp)

Char8TypeMap :: TypeMap (BaseStringType Char8)

ComplexToStructTypeMap :: TypeMap BaseComplexType

ComplexToArrayTypeMap :: TypeMap BaseComplexType

PrimArrayTypeMap :: !(Assignment TypeMap (idxl ::> idx)) -> !(TypeMap tp) -> TypeMap (BaseArrayType (idxl ::> idx) tp)

FnArrayTypeMap :: !(Assignment TypeMap (idxl ::> idx)) -> TypeMap tp -> TypeMap (BaseArrayType (idxl ::> idx) tp)

StructTypeMap :: !(Assignment TypeMap idx) -> TypeMap (BaseStructType idx)

Instances

TestEquality TypeMap

Defined in What4.Protocol.SMTWriter

Methods

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

ShowF TypeMap

Defined in What4.Protocol.SMTWriter

Methods

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

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

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

Eq (TypeMap tp)

Defined in What4.Protocol.SMTWriter

Methods

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

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

Show (TypeMap a)

Defined in What4.Protocol.SMTWriter

Methods

showsPrec :: Int -> TypeMap a -> ShowS

show :: TypeMap a -> String

showList :: [TypeMap a] -> ShowS

typeMap :: WriterConn t h -> BaseTypeRepr tp -> Either BaseTypeError (TypeMap tp)

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

Arguments

:: 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 ()

Assume that the given formula holds.

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

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

data DefineStyle

Constructors

FunctionDefinition

EqualityDefinition

Instances

Eq DefineStyle

Defined in What4.Protocol.SMTWriter

Methods

(==) :: DefineStyle -> DefineStyle -> Bool

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

Show DefineStyle

Defined in What4.Protocol.SMTWriter

Methods

showsPrec :: Int -> DefineStyle -> ShowS

show :: DefineStyle -> String

showList :: [DefineStyle] -> ShowS

newtype AcknowledgementAction t h

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

nullAcknowledgementAction :: AcknowledgementAction t h

An acknowledgement action that does nothing

SMTWriter operations

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

Write assume formula predicates for asserting predicate holds.

mkSMTTerm :: SMTWriter h => WriterConn t h -> Expr t tp -> IO (Term h)

Write a expression to SMT

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

Write a logical expression.

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

data SMTEvalFunctions h

Constructors

SMTEvalFunctions

Fields

• smtEvalBool :: Term h -> IO Bool

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

• smtEvalBV :: forall w. 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. 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 ByteString

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

smtExprGroundEvalFn

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

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 :: SMTWriter h => Expr t tp -> SMTCollector t h (Term h)

Convert an element to a base expression.

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

This runs the side collector and collects the results.

Reexports

data RoundingMode

Rounding modes for IEEE-754 floating point operations.

Constructors

RNE

Round to nearest even.

RNA

Round to nearest away.

RTP

Round toward plus Infinity.

RTN

Round toward minus Infinity.

RTZ

Round toward zero.

Instances

Enum RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

succ :: RoundingMode -> RoundingMode

pred :: RoundingMode -> RoundingMode

toEnum :: Int -> RoundingMode

fromEnum :: RoundingMode -> Int

enumFrom :: RoundingMode -> [RoundingMode]

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

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

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

Eq RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

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

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

Ord RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

compare :: RoundingMode -> RoundingMode -> Ordering

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

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

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

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

max :: RoundingMode -> RoundingMode -> RoundingMode

min :: RoundingMode -> RoundingMode -> RoundingMode

Show RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

showsPrec :: Int -> RoundingMode -> ShowS

show :: RoundingMode -> String

showList :: [RoundingMode] -> ShowS

Generic RoundingMode

Defined in What4.Utils.FloatHelpers

Associated Types

type Rep RoundingMode :: Type -> Type

Methods

from :: RoundingMode -> Rep RoundingMode x

to :: Rep RoundingMode x -> RoundingMode

Hashable RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

hashWithSalt :: Int -> RoundingMode -> Int

hash :: RoundingMode -> Int

type Rep RoundingMode

Defined in What4.Utils.FloatHelpers

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