What4.Protocol.SMTLib2.Syntax

This module defines types and operations for generating SMTLIB2 files.

It does not depend on the rest of What4 so that it can be used directly by clients interested in generating SMTLIB without depending on the What4 formula interface. All the type constructors are exposed so that clients can generate new values that are not exposed through this interface.

Commands

newtype Command

This represents a command to be sent to the SMT solver.

Constructors

Cmd Builder

setLogic :: Logic -> Command

Set the logic of the SMT solver

setOption :: Text -> Text -> Command

Set an option in the SMT solver

The name should not need to be prefixed with a colon."

setProduceModels :: Bool -> Command

Set option to produce models

This is a widely used option so, we we have a custom command to make it.

data SMTInfoFlag

This is a subtype of the type of the same name in Data.SBV.Control.

Constructors

Name

Version

ErrorBehavior

InfoKeyword Text

Instances

Eq SMTInfoFlag

Defined in What4.Protocol.SMTLib2.Syntax

Methods

(==) :: SMTInfoFlag -> SMTInfoFlag -> Bool

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

Data SMTInfoFlag

Defined in What4.Protocol.SMTLib2.Syntax

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SMTInfoFlag

toConstr :: SMTInfoFlag -> Constr

dataTypeOf :: SMTInfoFlag -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTInfoFlag)

gmapT :: (forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r

gmapQ :: (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag

Ord SMTInfoFlag

Defined in What4.Protocol.SMTLib2.Syntax

Methods

compare :: SMTInfoFlag -> SMTInfoFlag -> Ordering

(<) :: SMTInfoFlag -> SMTInfoFlag -> Bool

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

(>) :: SMTInfoFlag -> SMTInfoFlag -> Bool

(>=) :: SMTInfoFlag -> SMTInfoFlag -> Bool

max :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag

min :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag

Show SMTInfoFlag

Defined in What4.Protocol.SMTLib2.Syntax

Methods

showsPrec :: Int -> SMTInfoFlag -> ShowS

show :: SMTInfoFlag -> String

showList :: [SMTInfoFlag] -> ShowS

Generic SMTInfoFlag

Defined in What4.Protocol.SMTLib2.Syntax

Associated Types

type Rep SMTInfoFlag :: Type -> Type

Methods

from :: SMTInfoFlag -> Rep SMTInfoFlag x

to :: Rep SMTInfoFlag x -> SMTInfoFlag

type Rep SMTInfoFlag

Defined in What4.Protocol.SMTLib2.Syntax

type Rep SMTInfoFlag = D1 (MetaData "SMTInfoFlag" "What4.Protocol.SMTLib2.Syntax" "what4-1.0-IcCGmY3T3YeXUBLCM24Pe" False) ((C1 (MetaCons "Name" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Version" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "ErrorBehavior" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "InfoKeyword" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Text))))

getInfo :: SMTInfoFlag -> Command

A get-info command

getVersion :: Command

getName :: Command

getErrorBehavior :: Command

exit :: Command

Request the SMT solver to exit

Declarations

declareSort :: Symbol -> Integer -> Command

Declare an uninterpreted sort with the given number of sort parameters.

defineSort

Arguments

:: Symbol

Name of new sort

-> [Symbol]

Parameters for polymorphic sorts

-> Sort

Definition

-> Command

Define a sort in terms of other sorts

declareConst :: Text -> Sort -> Command

Declare a constant with the given name and return types.

declareFun :: Text -> [Sort] -> Sort -> Command

Declare a function with the given name, argument types, and return type.

defineFun :: Text -> [(Text, Sort)] -> Sort -> Term -> Command

Declare a function with the given name, argument types, and return type.

type Symbol = Text

Assertions and checking

checkSat :: Command

Check the satisfiability of the current assertions

checkSatAssuming :: [Term] -> Command

Check the satisfiability of the current assertions and the additional ones in the list.

checkSatWithAssumptions :: [Text] -> Command

Check satisfiability of the given atomic assumptions in the current context.

NOTE! The names of variables passed to this function MUST be generated using a `declare-fun` statement, and NOT a `define-fun` statement. Thus, if you want to bind an arbitrary term, you must declare a new term and assert that it is equal to it's definition. Yes, this is quite irritating.

getModel :: Command

Get the model associated with the last call to check-sat.

getValue :: [Term] -> Command

Get the values associated with the terms from the last call to check-sat.

push :: Integer -> Command

Push the given number of scope frames to the SMT solver.

pop :: Integer -> Command

Pop the given number of scope frames to the SMT solver.

resetAssertions :: Command

Empties the assertion stack and remove all global assertions and declarations.

assert :: Term -> Command

Assert the predicate holds in the current context.

assertNamed :: Term -> Text -> Command

Assert the predicate holds in the current context, and assign it a name so it can appear in unsatisfiable core results.

getUnsatAssumptions :: Command

getUnsatCore :: Command

Logic

newtype Logic

Identifies the set of predefined sorts and operators available.

Constructors

Logic Builder

qf_bv :: Logic

Use the QF_BV logic

allSupported :: Logic

Set the logic to all supported logics.

Sort

newtype Sort

Sort for SMTLIB expressions

Constructors

Sort

Fields

• unSort :: Builder

boolSort :: Sort

Booleans

bvSort :: Natural -> Sort

Bitvectors with the given number of bits.

intSort :: Sort

Integers

realSort :: Sort

Real numbers

varSort :: Symbol -> Sort

Create a sort from a symbol name

Term

newtype Term

Denotes an expression in the SMT solver

Constructors

T

Fields

• renderTerm :: Builder

Instances

Num Term

Defined in What4.Protocol.SMTLib2

Methods

(+) :: Term -> Term -> Term

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

(*) :: Term -> Term -> Term

negate :: Term -> Term

abs :: Term -> Term

signum :: Term -> Term

fromInteger :: Integer -> Term

IsString Term

Defined in What4.Protocol.SMTLib2.Syntax

Methods

fromString :: String -> Term

Semigroup Term

Defined in What4.Protocol.SMTLib2.Syntax

Methods

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

sconcat :: NonEmpty Term -> Term

stimes :: Integral b => b -> Term -> Term

Monoid Term

Defined in What4.Protocol.SMTLib2.Syntax

Methods

mempty :: Term

mappend :: Term -> Term -> Term

mconcat :: [Term] -> Term

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

bvTestBit :: NatRepr w -> Natural -> Term -> Term

bvSumExpr :: NatRepr w -> [Term] -> Term

floatPZero :: FloatPrecisionRepr fpp -> Term

floatNZero :: FloatPrecisionRepr fpp -> Term

floatNaN :: FloatPrecisionRepr fpp -> Term

floatPInf :: FloatPrecisionRepr fpp -> Term

floatNInf :: FloatPrecisionRepr fpp -> 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

floatMin :: Term -> Term -> Term

floatMax :: 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 :: FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term

floatRound :: RoundingMode -> Term -> Term

floatFromBinary :: FloatPrecisionRepr fpp -> Term -> Term

bvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term

sbvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term

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

un_app :: Builder -> Term -> Term

Construct an expression with the given operator and single argument.

bin_app :: Builder -> Term -> Term -> Term

Construct an expression with the given operator and two arguments.

term_app :: Builder -> [Term] -> Term

Construct an expression with the given operator and list of arguments.

pairwise_app :: Builder -> [Term] -> Term

Construct a chainable term with the givne relation

pairwise_app p [x1, x2, ..., xn] is equivalent to forall_{i,j} p x_i x_j@.

namedTerm :: Term -> Text -> Term

Append a "name" to a term so that it will be printed when (get-assignment) is called.

builder_list :: [Builder] -> Builder

Core theory

true :: Term

true Boolean term

false :: Term

false Boolean term

not :: Term -> Term

Complement a Boolean

implies :: [Term] -> Term -> Term

implies c r is equivalent to c1 => c2 => .. cn => r.

and :: [Term] -> Term

Conjunction of all terms

or :: [Term] -> Term

Disjunction of all terms

xor :: [Term] -> Term

Disjunction of all terms

eq :: [Term] -> Term

Return true if all terms are equal.

distinct :: [Term] -> Term

Asserts that each term in the list is unique.

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

Create an if-then-else expression.

forall :: [(Text, Sort)] -> Term -> Term

forall vars t denotes a predicate that holds if t for every valuation of the variables in vars.

exists :: [(Text, Sort)] -> Term -> Term

exists vars t denotes a predicate that holds if t for some valuation of the variables in vars.

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

Create a let binding. NOTE: SMTLib2 defines this to be a "parallel" let, which means that the bound variables are NOT in scope in the right-hand sides of other bindings, even syntactically-later ones.

Ints, Reals, Reals_Ints theories

negate :: Term -> Term

Negate an integer or real number.

numeral :: Integer -> Term

Create a numeral literal from the given integer.

decimal :: Integer -> Term

Create a literal as a real from the given integer.

sub :: Term -> [Term] -> Term

sub x1 [x2, ..., xn] with n >= 1 returns x1 minus x2 + ... + xn.

The terms are expected to have type Int or Real.

add :: [Term] -> Term

add [x1, x2, ..., xn] with n >= 2 returns x1 minus x2 + ... + xn.

The terms are expected to have type Int or Real.

mul :: [Term] -> Term

add [x1, x2, ..., xn] with n >= 2 returns x1 minus x2 + ... + xn.

The terms are expected to have type Int or Real.

div :: Term -> [Term] -> Term

div x1 [x2, ..., xn] with n >= 1 returns x1 div x2 * ... * xn.

The terms are expected to have type Int.

(./) :: Term -> [Term] -> Term

x1 ./ [x2, ..., xn] with n >= 1 returns x1 / x2 * ... * xn.

mod :: Term -> Term -> Term

mod x1 x2 returns x1 - x2 * (x1 div [x2])@.

The terms are expected to have type Int.

abs :: Term -> Term

abs x1 returns the absolute value of x1.

The term is expected to have type Int.

le :: [Term] -> Term

Less than or equal over a chained list of terms.

le [x1, x2, ..., xn] is equivalent to x1 <= x2 x2 <= x3 ... / x(n-1) <= xn.

This is defined in the Reals, Ints, and Reals_Ints theories, and the number of elements must be at least 2.

With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.

lt :: [Term] -> Term

Less than over a chained list of terms.

lt [x1, x2, ..., xn] is equivalent to x1 < x2 x2 < x3 ... / x(n-1) < xn.

With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.

ge :: [Term] -> Term

Greater than or equal over a chained list of terms.

ge [x1, x2, ..., xn] is equivalent to x1 >= x2 x2 >= x3 ... / x(n-1) >= xn.

With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.

gt :: [Term] -> Term

Greater than over a chained list of terms.

gt [x1, x2, ..., xn] is equivalent to x1 > x2 x2 > x3 ... / x(n-1) > xn.

With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.

toReal :: Term -> Term

Maps a term with type Int to Real.

toInt :: Term -> Term

Returns the largest integer not larger than the given real term.

isInt :: Term -> Term

Returns true if this is an integer.

Bitvector theory and extensions

concat :: Term -> Term -> Term

concat x y returns the bitvector with the bits of x followed by the bits of y.

extract :: Natural -> Natural -> Term -> Term

extract i j x returns the bitvector containing the bits [j..i].

bvnot :: Term -> Term

Bitwise negation of term.

bvand :: Term -> [Term] -> Term

Bitwise and of all arguments.

bvor :: Term -> [Term] -> Term

Bitwise include or of all arguments.

bvxor :: Term -> [Term] -> Term

Bitvector exclusive or of all arguments.

bvneg :: Term -> Term

Negate the bitvector

bvadd :: Term -> [Term] -> Term

Bitvector addition

bvsub :: Term -> Term -> Term

Bitvector subtraction

bvmul :: Term -> [Term] -> Term

Bitvector multiplication

bvudiv :: Term -> Term -> Term

bvudiv x y returns floor (to_nat x / to_nat y) when y != 0.

When y = 0, this returns not (from_nat 0).

bvurem :: Term -> Term -> Term

bvurem x y returns x - y * bvudiv x y when y != 0.

When y = 0, this returns from_nat 0.

bvshl :: Term -> Term -> Term

bvshl x y shifts the bits in x to the left by to_nat u bits.

The new bits are zeros (false)

bvlshr :: Term -> Term -> Term

bvlshr x y shifts the bits in x to the right by to_nat u bits.

The new bits are zeros (false)

bvult :: Term -> Term -> Term

bvult x y returns a Boolean term that is true if to_nat x < to_nat y.

Extensions provided by QF_BV

bit0 :: Term

A 1-bit bitvector representing 0.

bit1 :: Term

A 1-bit bitvector representing 1.

bvbinary :: 1 <= w => NatRepr w -> BV w -> Term

bvbinary w x constructs a bitvector term with width w equal to x mod 2^w.

The width w must be positive.

The literal uses a binary notation.

bvdecimal :: 1 <= w => NatRepr w -> BV w -> Term

bvdecimal x w constructs a bitvector term with width w equal to x mod 2^w.

The width w must be positive.

The literal uses a decimal notation.

bvhexadecimal :: 1 <= w => NatRepr w -> BV w -> Term

bvhexadecimal x w constructs a bitvector term with width w equal to x mod 2^w.

The width w must be a positive multiple of 4.

The literal uses hex notation.

bvashr :: Term -> Term -> Term

bvashr x y shifts the bits in x to the right by to_nat u bits.

The new bits are the same as the most-significant bit of x.

Note. This is in QF_BV, but not the bitvector theory.

bvslt :: Term -> Term -> Term

bvslt x y returns a Boolean term that is true if to_int x < to_int y.

Note. This is in QF_BV, but not the bitvector theory.

bvsle :: Term -> Term -> Term

bvsle x y returns a Boolean term that is true if to_int x <= to_int y.

Note. This is in QF_BV, but not the bitvector theory.

bvule :: Term -> Term -> Term

bvule x y returns a Boolean term that is true if to_nat x <= to_nat y.

Note. This is in QF_BV, but not the bitvector theory.

bvsgt :: Term -> Term -> Term

bvsgt x y returns a Boolean term that is true if to_int x < to_int y.

Note. This is in QF_BV, but not the bitvector theory.

bvsge :: Term -> Term -> Term

bvsge x y returns a Boolean term that is true if to_int x <= to_int y.

Note. This is in QF_BV, but not the bitvector theory.

bvugt :: Term -> Term -> Term

bvugt x y returns a Boolean term that is true if to_nat x < to_nat y.

Note. This is in QF_BV, but not the bitvector theory.

bvuge :: Term -> Term -> Term

bvuge x y returns a Boolean term that is true if to_nat x <= to_nat y.

Note. This is in QF_BV, but not the bitvector theory.

bvsdiv :: Term -> Term -> Term

bvsdiv x y returns round_to_zero (to_int x / to_int y) when y != 0.

When y = 0, this returns not (from_nat 0).

Note. This is in QF_BV, but not the bitvector theory.

bvsrem :: Term -> Term -> Term

bvsrem x y returns x - y * bvsdiv x y when y != 0.

When y = 0, this returns from_nat 0.

Note. This is in QF_BV, but not the bitvector theory.

bvsignExtend :: Integer -> Term -> Term

bvsignExtend w x adds an additional w bits to the most significant bits of x by sign extending x.

Note. This is in QF_BV, but not the bitvector theory.

bvzeroExtend :: Integer -> Term -> Term

bvzeroExtend w x adds an additional w zero bits to the most significant bits of x.

Note. This is in QF_BV, but not the bitvector theory.

Array theory

arraySort :: Sort -> Sort -> Sort

arraySort a b denotes the set of functions from a to be b.

arrayConst :: Sort -> Sort -> Term -> Term

arrayConst t1 t2 c generates an array with index type t1 and value type t2 that always returns c.

This uses the non-standard SMTLIB2 syntax ((as const (Array t1 t2)) c) which is supported by CVC4 and Z3 (and perhaps others).

select :: Term -> Term -> Term

select a i denotes the value of a at i.

store :: Term -> Term -> Term -> Term

store a i v denotes the array whose valuation is v at index i and select a j at every other index j.