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

What4.Protocol.SMTWriter

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

Type classes

class Num v => SupportTermOps v where Source #

A class of values containing rational and operations.

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

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

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

floatFromBinary :: FloatPrecisionRepr fpp -> v -> v Source #

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

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

realToFloat :: 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 #

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

realSinh :: v -> v Source #

realCosh :: 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 #

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

realSinh :: Term -> Term Source #

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

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 #

Push 1 new scope

popCommand :: f h -> Command h Source #

Pop 1 existing scope

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.

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

Set an option/parameter.

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

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

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

Build a struct term with the given types and fields

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

Project a field from a struct with the given types

stringTerm :: ByteString -> 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 #

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 #

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 #

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 :: ByteString -> 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 #

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 #

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 #

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 :: ByteString -> 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 -> InputStream Text -> IO (SatResult () ()) Source #

Parse a set result from the solver's response.

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

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

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

Terms

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

A term in the output language.

Instances

Instances details
type Term Connection Source # 
Instance details

Defined in What4.Solver.Yices

type Term (Writer a) Source # 
Instance details

Defined in What4.Protocol.SMTLib2

type Term (Writer a) = Term

SMTWriter

data WriterConn t (h :: Type) 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.

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

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

Instances

Instances details
type Command Connection Source # 
Instance details

Defined in What4.Solver.Yices

type Command (Writer a) Source # 
Instance details

Defined in What4.Protocol.SMTLib2

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.

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

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

Create a new variable with the given name.

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

Instances

Instances details
TestEquality TypeMap Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Methods

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

ShowF TypeMap Source # 
Instance details

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

Defined in What4.Protocol.SMTWriter

Methods

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

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

Show (TypeMap a) Source # 
Instance details

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

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

data DefineStyle Source #

Instances

Instances details
Eq DefineStyle Source # 
Instance details

Defined in What4.Protocol.SMTWriter

Show DefineStyle Source # 
Instance details

Defined in What4.Protocol.SMTWriter

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

nullAcknowledgementAction :: AcknowledgementAction t h Source #

An acknowledgement action that does nothing

SMTWriter operations

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

Write assume formula predicates for asserting predicate holds.

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

data SMTEvalFunctions h Source #

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

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

Eq RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Ord RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Show RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Generic RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

Associated Types

type Rep RoundingMode :: Type -> Type #

Hashable RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode Source # 
Instance details

Defined in What4.Utils.FloatHelpers

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