what4-1.1: Solver-agnostic symbolic values support for issuing queries
Safe HaskellNone
LanguageHaskell2010

What4.Protocol.SMTLib2.Syntax

Description

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.

Synopsis

Commands

newtype Command Source #

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

Constructors

Cmd Builder 

setLogic :: Logic -> Command Source #

Set the logic of the SMT solver

setOption :: Text -> Text -> Command Source #

Set an option in the SMT solver

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

setProduceModels :: Bool -> Command Source #

Set option to produce models

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

data SMTInfoFlag Source #

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

Instances

Instances details
Eq SMTInfoFlag Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Data SMTInfoFlag Source # 
Instance details

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 :: forall r r'. (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 Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Show SMTInfoFlag Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Generic SMTInfoFlag Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Associated Types

type Rep SMTInfoFlag :: Type -> Type #

type Rep SMTInfoFlag Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

type Rep SMTInfoFlag = D1 ('MetaData "SMTInfoFlag" "What4.Protocol.SMTLib2.Syntax" "what4-1.1-F6JmVDCUG2e4tsAmUzrLc2" '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 Source #

A get-info command

exit :: Command Source #

Request the SMT solver to exit

Declarations

declareSort :: Symbol -> Integer -> Command Source #

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

defineSort Source #

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

Declare a constant with the given name and return types.

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

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

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

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

Assertions and checking

checkSat :: Command Source #

Check the satisfiability of the current assertions

checkSatAssuming :: [Term] -> Command Source #

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

checkSatWithAssumptions :: [Text] -> Command Source #

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

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

getValue :: [Term] -> Command Source #

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

push :: Integer -> Command Source #

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

pop :: Integer -> Command Source #

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

resetAssertions :: Command Source #

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

assert :: Term -> Command Source #

Assert the predicate holds in the current context.

assertNamed :: Term -> Text -> Command Source #

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

Logic

newtype Logic Source #

Identifies the set of predefined sorts and operators available.

Constructors

Logic Builder 

qf_bv :: Logic Source #

Use the QF_BV logic

allSupported :: Logic Source #

Set the logic to all supported logics.

Sort

newtype Sort Source #

Sort for SMTLIB expressions

Constructors

Sort 

Fields

boolSort :: Sort Source #

Booleans

bvSort :: Natural -> Sort Source #

Bitvectors with the given number of bits.

intSort :: Sort Source #

Integers

realSort :: Sort Source #

Real numbers

varSort :: Symbol -> Sort Source #

Create a sort from a symbol name

Term

newtype Term Source #

Denotes an expression in the SMT solver

Constructors

T 

Fields

Instances

Instances details
Num Term Source # 
Instance details

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

Defined in What4.Protocol.SMTLib2.Syntax

Methods

fromString :: String -> Term #

Semigroup Term Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Methods

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

sconcat :: NonEmpty Term -> Term #

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

Monoid Term Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Methods

mempty :: Term #

mappend :: Term -> Term -> Term #

mconcat :: [Term] -> Term #

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 #

un_app :: Builder -> Term -> Term Source #

Construct an expression with the given operator and single argument.

bin_app :: Builder -> Term -> Term -> Term Source #

Construct an expression with the given operator and two arguments.

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

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

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

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

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

Core theory

true :: Term Source #

true Boolean term

false :: Term Source #

false Boolean term

not :: Term -> Term Source #

Complement a Boolean

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

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

and :: [Term] -> Term Source #

Conjunction of all terms

or :: [Term] -> Term Source #

Disjunction of all terms

xor :: [Term] -> Term Source #

Disjunction of all terms

eq :: [Term] -> Term Source #

Return true if all terms are equal.

distinct :: [Term] -> Term Source #

Asserts that each term in the list is unique.

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

Create an if-then-else expression.

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

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

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

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

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

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

Negate an integer or real number.

numeral :: Integer -> Term Source #

Create a numeral literal from the given integer.

decimal :: Integer -> Term Source #

Create a literal as a real from the given integer.

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

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

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

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

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

The terms are expected to have type Int.

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

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

mod :: Term -> Term -> Term Source #

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

The terms are expected to have type Int.

abs :: Term -> Term Source #

abs x1 returns the absolute value of x1.

The term is expected to have type Int.

le :: [Term] -> Term Source #

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

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

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

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

Maps a term with type Int to Real.

toInt :: Term -> Term Source #

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

isInt :: Term -> Term Source #

Returns true if this is an integer.

Bitvector theory and extensions

concat :: Term -> Term -> Term Source #

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

extract :: Natural -> Natural -> Term -> Term Source #

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

bvnot :: Term -> Term Source #

Bitwise negation of term.

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

Bitwise and of all arguments.

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

Bitwise include or of all arguments.

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

Bitvector exclusive or of all arguments.

bvneg :: Term -> Term Source #

Negate the bitvector

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

Bitvector addition

bvsub :: Term -> Term -> Term Source #

Bitvector subtraction

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

Bitvector multiplication

bvudiv :: Term -> Term -> Term Source #

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

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

When y = 0, this returns from_nat 0.

bvshl :: Term -> Term -> Term Source #

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

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

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

Extensions provided by QF_BV

bit0 :: Term Source #

A 1-bit bitvector representing 0.

bit1 :: Term Source #

A 1-bit bitvector representing 1.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

arrayConst :: Sort -> Sort -> Term -> Term Source #

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

select a i denotes the value of a at i.

store :: Term -> Term -> Term -> Term Source #

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