The SMT monad used for communating with the SMT solver

Haskell types which can be represented in SMT

Haskell values which can be represented as SMT constants

A type class for all types which support arithmetic operations in SMT

Lifts the Ord class into SMT

An abstract SMT expression

Options controling the behaviour of the SMT solver

An array which maps indices of type i to elements of type v.

Represents a constructor of a datatype a Can be obtained by using the template haskell extension module

Represents a field of the datatype a of the type f

Instances of this class may be used as arguments for constructed functions and quantifiers.

An extension of the Args class: Instances of this class can be represented as native haskell data types.

Set an option for the underlying SMT solver

Get information about the underlying SMT solver

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

Asserts that a boolean expression is true

Push a new context on the stack

Pop a new context from the stack

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

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

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

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

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

The result of a check-sat query

Describe limits on the ressources that an SMT-solver can use

Extract all assigned values of the model

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

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

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

Identifies a clause in an unsatisfiable core

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

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

Create a new interpolation group

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

Create a fresh new variable

Create a new named variable

Create a named and annotated variable.

Create a annotated variable

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

Like argVarsAnnNamed, but defaults the name to "var"

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

Create a fresh untyped variable

Create a fresh untyped variable with a name

A constant expression.

An annotated constant expression.

Reconstruct the type annotation for a given SMT expression.

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.

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

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

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

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

Recursively fold a function over all sub-expressions of this expression. It is implemented as a special case of foldExprM.

Recursively fold a monadic function over all sub-expressions of this expression

Recursively fold a function over all sub-expressions of the argument. It is implemented as a special case of foldArgsM.

Recursively fold a monadic function over all sub-expressions of the argument

Two expressions shall be equal

A generalized version of .==.

Declares all arguments to be distinct

If-then-else construct

Boolean conjunction

Boolean disjunction

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

Negates a boolean expression

Implication

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

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

An annotated version of forAll.

An annotated version of exists.

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

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

Calculate the sum of arithmetic expressions

Subtracts two expressions

Calculate the product of arithmetic expressions

Divide an arithmetic expression by another

Perform a modulo operation on an arithmetic expression

Calculate the remainder of the division of two integer expressions

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

Divide a rational expression by another one

Convert an integer expression to a real expression

Convert a real expression into an integer expression

Extracts an element of an array by its index

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

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

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

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.

Create an array where each element is the same.

Bitvector and

Bitvector or

Bitvector or

Bitvector not

Bitvector signed negation

Bitvector addition

Bitvector subtraction

Bitvector multiplication

Bitvector unsigned remainder

Bitvector signed remainder

Bitvector unsigned division

Bitvector signed division

Bitvector unsigned less-or-equal

Bitvector unsigned less-than

Bitvector unsigned greater-or-equal

Bitvector unsigned greater-than

Bitvector signed less-or-equal

Bitvector signed less-than

Bitvector signed greater-or-equal

Bitvector signed greater-than

Bitvector shift left

Bitvector logical right shift

Bitvector arithmetical right shift

Concats two bitvectors into one.

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

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

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

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

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

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

Extract a sub-vector out of a given bitvector.

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

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

funAnn with an annotation only for the return type.

Create a new uninterpreted function.

Apply a function to an argument

Define a new function with a body

Define a new constant.

Define a new constant with a name

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

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

Lift a function to arrays

Checks if the expression is formed a specific constructor.

Access a field of an expression

Takes the first element of a list

Drops the first element from a list

Checks if a list is empty.

Checks if a list is non-empty.