Language.SMTLib2.Internals.Interface

Defines the user-accessible interface of the smtlib2 library

Documentation

checkSat :: Monad m => SMT' m Bool

Check if the model is satisfiable (e.g. if there is a value for each variable so that every assertion holds)

checkSatUsing :: Monad m => Tactic -> SMT' m Bool

Check if the model is satisfiable using a given tactic. (Works only with Z3)

checkSat' :: Monad m => Maybe Tactic -> CheckSatLimits -> SMT' m CheckSatResult

Like checkSat, but gives you more options like choosing a tactic (Z3 only) or providing memory/time-limits

isSat :: CheckSatResult -> Bool

apply :: Monad m => Tactic -> SMT' m [SMTExpr Bool]

Apply the given tactic to the current assertions. (Works only with Z3)

push :: Monad m => SMT' m ()

Push a new context on the stack

pop :: Monad m => SMT' m ()

Pop a new context from the stack

stack :: Monad m => SMT' m a -> SMT' m a

Perform a stacked operation, meaning that every assertion and declaration made in it will be undone after the operation.

comment :: Monad m => String -> SMT' m ()

Insert a comment into the SMTLib2 command stream. If you aren't looking at the command stream for debugging, this will do nothing.

varNamed :: (SMTType t, Typeable t, Unit (SMTAnnotation t), Monad m) => String -> SMT' m (SMTExpr t)

Create a new named variable

varNamedAnn :: (SMTType t, Typeable t, Monad m) => String -> SMTAnnotation t -> SMT' m (SMTExpr t)

Create a named and annotated variable.

varAnn :: (SMTType t, Typeable t, Monad m) => SMTAnnotation t -> SMT' m (SMTExpr t)

Create a annotated variable

var :: (SMTType t, Typeable t, Unit (SMTAnnotation t), Monad m) => SMT' m (SMTExpr t)

Create a fresh new variable

untypedNamedVar :: Monad m => String -> Sort -> SMT' m (SMTExpr Untyped)

Create a fresh untyped variable with a name

untypedVar :: Monad m => Sort -> SMT' m (SMTExpr Untyped)

Create a fresh untyped variable

argVarsAnn :: (Args a, Monad m) => ArgAnnotation a -> SMT' m a

Like argVarsAnnNamed, but defaults the name to "var"

argVarsAnnNamed :: (Args a, Monad m) => String -> ArgAnnotation a -> SMT' m a

Create annotated named SMT variables of the Args class. If more than one variable is needed, they get a numerical suffix.

argVarsAnnNamed' :: (Args a, Monad m) => Maybe String -> ArgAnnotation a -> SMT' m a

argVars :: (Args a, Unit (ArgAnnotation a), Monad m) => SMT' m a

Like argVarsAnn, but can only be used for unit type annotations.

constant :: (SMTValue t, Unit (SMTAnnotation t)) => t -> SMTExpr t

A constant expression.

constantAnn :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t

An annotated constant expression.

getValue :: (SMTValue t, Monad m) => SMTExpr t -> SMT' m t

getValues :: (LiftArgs arg, Monad m) => arg -> SMT' m (Unpacked arg)

getModel :: Monad m => SMT' m SMTModel

Extract all assigned values of the model

unmangleArray :: (Liftable i, LiftArgs i, Ix (Unpacked i), SMTValue v, Unit (ArgAnnotation i), Monad m) => (Unpacked i, Unpacked i) -> SMTExpr (SMTArray i v) -> SMT' m (Array (Unpacked i) v)

Extract all values of an array by giving the range of indices.

defFun :: (Args a, SMTType r, Unit (ArgAnnotation a), Monad m) => (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

Define a new function with a body

defConst :: (SMTType r, Monad m) => SMTExpr r -> SMT' m (SMTExpr r)

Define a new constant.

defConstNamed :: (SMTType r, Monad m) => String -> SMTExpr r -> SMT' m (SMTExpr r)

Define a new constant with a name

defConstNamed' :: (SMTType r, Monad m) => Maybe String -> SMTExpr r -> SMT' m (SMTExpr r)

defFunAnnNamed :: (Args a, SMTType r, Monad m) => String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

Define a new function with a body and custom type annotations for arguments and result.

defFunAnnNamed' :: (Args a, SMTType r, Monad m) => Maybe String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

defFunAnn :: (Args a, SMTType r, Monad m) => ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

Like defFunAnnNamed, but defaults the function name to "fun".

and' :: SMTFunction [SMTExpr Bool] Bool

Boolean conjunction

(.&&.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

or' :: SMTFunction [SMTExpr Bool] Bool

Boolean disjunction

(.||.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

arrayEquals :: (LiftArgs i, Liftable i, SMTValue v, Ix (Unpacked i), Unit (ArgAnnotation i), Unit (SMTAnnotation v)) => SMTExpr (SMTArray i v) -> Array (Unpacked i) v -> SMTExpr Bool

Create a boolean expression that encodes that the array is equal to the supplied constant array.

assert :: Monad m => SMTExpr Bool -> SMT' m ()

Asserts that a boolean expression is true

interpolationGroup :: Monad m => SMT' m InterpolationGroup

Create a new interpolation group

assertId :: Monad m => SMTExpr Bool -> SMT' m ClauseId

Assert a boolean expression and track it for an unsat core call later

assertInterp :: Monad m => SMTExpr Bool -> InterpolationGroup -> SMT' m ()

Assert a boolean expression to be true and assign it to an interpolation group

getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool)

interpolate :: Monad m => [SMTExpr Bool] -> SMT' m [SMTExpr Bool]

setOption :: Monad m => SMTOption -> SMT' m ()

Set an option for the underlying SMT solver

getInfo :: (Monad m, Typeable i) => SMTInfo i -> SMT' m i

Get information about the underlying SMT solver

funAnn :: (Liftable a, SMTType r, Monad m) => ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

Create a new uniterpreted function with annotations for the argument and the return type.

funAnnNamed :: (Liftable a, SMTType r, Monad m) => String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

Create a new uninterpreted named function with annotation for the argument and the return type.

funAnnNamed' :: (Liftable a, SMTType r, Monad m) => Maybe String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

funAnnRet :: (Liftable a, SMTType r, Unit (ArgAnnotation a), Monad m) => SMTAnnotation r -> SMT' m (SMTFunction a r)

funAnn with an annotation only for the return type.

fun :: (Liftable a, SMTType r, SMTAnnotation r ~ (), Unit (ArgAnnotation a), Monad m) => SMT' m (SMTFunction a r)

Create a new uninterpreted function.

app :: (Args arg, SMTType res) => SMTFunction arg res -> arg -> SMTExpr res

Apply a function to an argument

map' :: (Liftable arg, Args i, SMTType res) => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res)

Lift a function to arrays

(.==.) :: SMTType a => SMTExpr a -> SMTExpr a -> SMTExpr Bool infix 4

Two expressions shall be equal

argEq :: Args a => a -> a -> SMTExpr Bool

A generalized version of .==.

distinct :: SMTType a => [SMTExpr a] -> SMTExpr Bool

Declares all arguments to be distinct

plus :: SMTArith a => SMTFunction [SMTExpr a] a

Calculate the sum of arithmetic expressions

mult :: SMTArith a => SMTFunction [SMTExpr a] a

Calculate the product of arithmetic expressions

minus :: SMTArith a => SMTFunction (SMTExpr a, SMTExpr a) a

Subtracts two expressions

div' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

Divide an arithmetic expression by another

div'' :: SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer

mod' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

Perform a modulo operation on an arithmetic expression

mod'' :: SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer

rem' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

Calculate the remainder of the division of two integer expressions

rem'' :: SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer

divide :: SMTExpr Rational -> SMTExpr Rational -> SMTExpr Rational

Divide a rational expression by another one

divide' :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational

neg :: SMTArith a => SMTFunction (SMTExpr a) a

For an expression x, this returns the expression -x.

toReal :: SMTExpr Integer -> SMTExpr Rational

Convert an integer expression to a real expression

toInt :: SMTExpr Rational -> SMTExpr Integer

Convert a real expression into an integer expression

ite

Arguments

:: SMTType a

=> SMTExpr Bool

If this expression is true

-> SMTExpr a

Then return this expression

-> SMTExpr a

Else this one

-> SMTExpr a

If-then-else construct

xor :: SMTFunction [SMTExpr Bool] Bool

Exclusive or: Return true if exactly one argument is true.

(.=>.)

Arguments

:: SMTExpr Bool

If this expression is true

-> SMTExpr Bool

This one must be as well

-> SMTExpr Bool

Implication

not' :: SMTExpr Bool -> SMTExpr Bool

Negates a boolean expression

not'' :: SMTFunction (SMTExpr Bool) Bool

select :: (Liftable i, SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v

Extracts an element of an array by its index

store :: (Liftable i, SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v -> SMTExpr (SMTArray i v)

The expression store arr i v stores the value v in the array arr at position i and returns the resulting new array.

asArray :: (Args arg, Unit (ArgAnnotation arg), SMTType res) => SMTFunction arg res -> SMTExpr (SMTArray arg res)

Interpret a function f from i to v as an array with indices i and elements v. Such that: f `app` j .==. select (asArray f) j for all indices j.

constArray

Arguments

:: (Args i, SMTType v)

=> SMTExpr v

This element will be at every index of the array

-> ArgAnnotation i

Annotations of the index type

-> SMTExpr (SMTArray i v)

Create an array where each element is the same.

bvand :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector and

bvor :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector or

bvxor :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector or

bvnot :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector not

bvneg :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector signed negation

bvadd :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector addition

bvsub :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector subtraction

bvmul :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector multiplication

bvurem :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector unsigned remainder

bvsrem :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector signed remainder

bvudiv :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector unsigned division

bvsdiv :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector signed division

bvule :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector unsigned less-or-equal

bvult :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector unsigned less-than

bvuge :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector unsigned greater-or-equal

bvugt :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector unsigned greater-than

bvsle :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector signed less-or-equal

bvslt :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector signed less-than

bvsge :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector signed greater-or-equal

bvsgt :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector signed greater-than

bvshl :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector shift left

bvlshr :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector logical right shift

bvashr :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector arithmetical right shift

bvconcat :: Concatable t1 t2 => SMTExpr (BitVector t1) -> SMTExpr (BitVector t2) -> SMTExpr (BitVector (ConcatResult t1 t2))

Concats two bitvectors into one.

bvextract

Arguments

:: (TypeableNat start, TypeableNat len, Extractable tp len')

=> Proxy start

The start of the extracted region

-> Proxy len

-> SMTExpr (BitVector tp)

The bitvector to extract from

-> SMTExpr (BitVector len')

Extract a sub-vector out of a given bitvector.

bvextract' :: Integer -> Integer -> SMTExpr (BitVector BVUntyped) -> SMTExpr (BitVector BVUntyped)

bvsplitu16to8 :: SMTExpr BV16 -> (SMTExpr BV8, SMTExpr BV8)

Safely split a 16-bit bitvector into two 8-bit bitvectors.

bvsplitu32to16 :: SMTExpr BV32 -> (SMTExpr BV16, SMTExpr BV16)

Safely split a 32-bit bitvector into two 16-bit bitvectors.

bvsplitu32to8 :: SMTExpr BV32 -> (SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8)

Safely split a 32-bit bitvector into four 8-bit bitvectors.

bvsplitu64to32 :: SMTExpr BV64 -> (SMTExpr BV32, SMTExpr BV32)

Safely split a 64-bit bitvector into two 32-bit bitvectors.

bvsplitu64to16 :: SMTExpr BV64 -> (SMTExpr BV16, SMTExpr BV16, SMTExpr BV16, SMTExpr BV16)

Safely split a 64-bit bitvector into four 16-bit bitvectors.

bvsplitu64to8 :: SMTExpr BV64 -> (SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8)

Safely split a 64-bit bitvector into eight 8-bit bitvectors.

mkQuantified :: (Args a, SMTType b) => (Integer -> [ProxyArg] -> SMTExpr b -> SMTExpr b) -> ArgAnnotation a -> (a -> SMTExpr b) -> SMTExpr b

forAll :: (Args a, Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool

If the supplied function returns true for all possible values, the forall quantification returns true.

forAllAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool

An annotated version of forAll.

exists :: (Args a, Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool

If the supplied function returns true for at least one possible value, the exists quantification returns true.

existsAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool

An annotated version of exists.

let' :: (Args a, Unit (ArgAnnotation a), SMTType b) => a -> (a -> SMTExpr b) -> SMTExpr b

Binds an expression to a variable. Can be used to prevent blowups in the command stream if expressions are used multiple times. let' x f is functionally equivalent to f x.

letAnn :: (Args a, SMTType b) => ArgAnnotation a -> a -> (a -> SMTExpr b) -> SMTExpr b

Like let', but can be given an additional type annotation for the argument of the function.

lets :: (Args a, Unit (ArgAnnotation a), SMTType b) => [a] -> ([a] -> SMTExpr b) -> SMTExpr b

Like let', but can define multiple variables of the same type.

forAllList

Arguments

:: (Args a, Unit (ArgAnnotation a))

=> Integer

Number of variables to quantify

-> ([a] -> SMTExpr Bool)

Function which takes a list of the quantified variables

-> SMTExpr Bool

Like forAll, but can quantify over more than one variable (of the same type).

existsList

Arguments

:: (Args a, Unit (ArgAnnotation a))

=> Integer

Number of variables to quantify

-> ([a] -> SMTExpr Bool)

Function which takes a list of the quantified variables

-> SMTExpr Bool

Like exists, but can quantify over more than one variable (of the same type).

is :: (Args arg, SMTType dt) => SMTExpr dt -> Constructor arg dt -> SMTExpr Bool

Checks if the expression is formed a specific constructor.

(.#) :: (SMTType a, SMTType f) => SMTExpr a -> Field a f -> SMTExpr f

Access a field of an expression

head' :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr a

Takes the first element of a list

tail' :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr [a]

Drops the first element from a list

isNil :: SMTType a => SMTExpr [a] -> SMTExpr Bool

Checks if a list is empty.

isInsert :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr Bool

Checks if a list is non-empty.

setLogic :: Monad m => String -> SMT' m ()

Sets the logic used for the following program (Not needed for many solvers).

named :: (SMTType a, SMTAnnotation a ~ (), Monad m) => String -> SMTExpr a -> SMT' m (SMTExpr a, SMTExpr a)

Given an arbitrary expression, this creates a named version of it and a name to reference it later on.

named' :: (SMTType a, SMTAnnotation a ~ (), Monad m) => SMTExpr a -> SMT' m (SMTExpr a, SMTExpr a)

Like named, but defaults the name to "named".

getProof :: Monad m => SMT' m (SMTExpr Bool)

After an unsuccessful checkSat this method extracts a proof from the SMT solver that the instance is unsatisfiable.

simplify :: (SMTType t, Monad m) => SMTExpr t -> SMT' m (SMTExpr t)

Use the SMT solver to simplify a given expression. Currently only works with Z3.

getUnsatCore :: Monad m => SMT' m [ClauseId]

After an unsuccessful checkSat, return a list of clauses which make the instance unsatisfiable.

optimizeExpr' :: SMTExpr a -> SMTExpr a