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

Set the logic of the SMT solver

Set an option in the SMT solver

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

Set option to produce models

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

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

A get-info command

Request the SMT solver to exit

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

Define a sort in terms of other sorts

Declare a constant with the given name and return types.

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

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

Check the satisfiability of the current assertions

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

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.

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

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

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

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

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

Assert the predicate holds in the current context.

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

Identifies the set of predefined sorts and operators available.

Use the QF_BV logic

Set the logic to all supported logics.

Sort for SMTLIB expressions

Booleans

Bitvectors with the given number of bits.

Integers

Real numbers

Create a sort from a symbol name

Denotes an expression in the SMT solver

Construct an expression with the given operator and single argument.

Construct an expression with the given operator and two arguments.

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

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

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

true Boolean term

false Boolean term

Complement a Boolean

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

Conjunction of all terms

Disjunction of all terms

Disjunction of all terms

Return true if all terms are equal.

Asserts that each term in the list is unique.

Create an if-then-else expression.

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

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

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.

Negate an integer or real number.

Create a numeral literal from the given integer.

Create a literal as a real from the given integer.

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

The terms are expected to have type Int or Real.

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

The terms are expected to have type Int or Real.

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

The terms are expected to have type Int or Real.

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

The terms are expected to have type Int.

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

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

The terms are expected to have type Int.

abs x1 returns the absolute value of x1.

The term is expected to have type Int.

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.

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.

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.

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.

Maps a term with type Int to Real.

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

Returns true if this is an integer.

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

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

Bitwise negation of term.

Bitwise and of all arguments.

Bitwise include or of all arguments.

Bitvector exclusive or of all arguments.

Negate the bitvector

Bitvector addition

Bitvector subtraction

Bitvector multiplication

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

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

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

When y = 0, this returns from_nat 0.

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

The new bits are zeros (false)

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

The new bits are zeros (false)

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

A 1-bit bitvector representing 0.

A 1-bit bitvector representing 1.

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

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

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 a i denotes the value of a at i.

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