A Z3 configuration object.

A Z3 logical context.

A Z3 symbol.

Used to name types, constants and functions.

A Z3 AST node.

This is the data-structure used in Z3 to represent terms, formulas and types.

A kind of AST representing types.

A kind of AST representing function symbols.

A kind of AST representing constant and function declarations.

A kind of AST representing pattern and multi-patterns to guide quantifier instantiation.

A type contructor for a (recursive) datatype.

A model for the constraints asserted into the logical context.

An interpretation of a function in a model.

Representation of the value of a Z3_func_interp at a particular point.

A Z3 parameter set.

Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.

A Z3 solver engine.

A(n) (incremental) solver, possibly specialized by a particular tactic or logic.

Different kinds of Z3 types.

Different kinds of Z3 AST nodes.

A tactic

A result of applying a tactic

A goal (aka problem)

Result of a satisfiability check.

This corresponds to the z3_lbool type in the C API.

Create a configuration.

See withConfig.

Delete a configuration.

See withConfig.

Set a configuration parameter.

Run a computation using a temporally created configuration.

Note that the configuration object can be thrown away once it has been used to create the Z3 Context.

Create a context using the given configuration.

Z3_del_context is called by Haskell's garbage collector before freeing the Context object.

Create a Z3 (empty) parameter set.

Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.

Add a Boolean parameter k with value v to the parameter set p.

Add a unsigned parameter k with value v to the parameter set p.

Add a double parameter k with value v to the parameter set p.

Add a symbol parameter k with value v to the parameter set p.

Convert a parameter set into a string.

This function is mainly used for printing the contents of a parameter set.

Create a Z3 symbol using an integer.

mkIntSymbol c i requires 0 <= i < 2^30

Create a Z3 symbol using a String.

Create a free (uninterpreted) type using the given name (symbol).

Two free types are considered the same iff the have the same name.

Create the boolean type.

This type is used to create propositional variables and predicates.

Create the integer type.

This is the type of arbitrary precision integers. A machine integer can be represented using bit-vectors, see mkBvSort.

Create the real type.

This type is not a floating point number. Z3 does not have support for floating point numbers yet.

Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

mkBvSort c sz requires sz >= 0

Create a finite-domain type.

Create an array type

We usually represent the array type as: [domain -> range]. Arrays are usually used to model the heap/memory in software verification.

Create a tuple type

A tuple with n fields has a constructor and n projections. This function will also declare the constructor and projection functions.

Create a contructor

Create datatype, such as lists, trees, records, enumerations or unions of records.

The datatype may be recursive. Returns the datatype sort.

Create mutually recursive datatypes, such as a tree and forest.

Returns the datatype sorts

Create an set type with a given domain type

Declare a constant or function.

Create a constant or function application.

Declare and create a constant.

This is a shorthand for: do xd <- mkFunDecl c x [] s; mkApp c xd []

Declare a fresh constant or function.

Declare and create a fresh constant.

Declare and create a variable (aka constant).

An alias for mkConst.

Declarate and create a variable of sort bool.

See mkVar.

Declarate and create a variable of sort real.

See mkVar.

Declarate and create a variable of sort int.

See mkVar.

Declarate and create a variable of sort bit-vector.

See mkVar.

Declare and create a fresh variable (aka constant).

An alias for mkFreshConst.

Declarate and create a fresh variable of sort bool.

See mkFreshVar.

Declarate and create a fresh variable of sort real.

See mkFreshVar.

Declarate and create a fresh variable of sort int.

See mkFreshVar.

Declarate and create a fresh variable of sort bit-vector.

See mkFreshVar.

Create an AST node representing true.

Create an AST node representing false.

Create an AST node representing l = r.

Create an AST node representing not(a).

Create an AST node representing an if-then-else: ite(t1, t2, t3).

Create an AST node representing t1 iff t2.

Create an AST node representing t1 implies t2.

Create an AST node representing t1 xor t2.

Create an AST node representing args[0] and ... and args[num_args-1].

Create an AST node representing args[0] or ... or args[num_args-1].

The distinct construct is used for declaring the arguments pairwise distinct.

That is, and [ args!!i /= args!!j | i <- [0..length(args)-1], j <- [i+1..length(args)-1] ]

Create an AST node representing the given boolean.

Create an AST node representing args[0] + ... + args[num_args-1].

Create an AST node representing args[0] * ... * args[num_args-1].

Create an AST node representing args[0] - ... - args[num_args - 1].

Create an AST node representing -arg.

Create an AST node representing arg1 div arg2.

Create an AST node representing arg1 mod arg2.

Create an AST node representing arg1 rem arg2.

Create less than.

Create less than or equal to.

Create greater than.

Create greater than or equal to.

Coerce an integer to a real.

Coerce a real to an integer.

Check if a real number is an integer.

Bitwise negation.

Take conjunction of bits in vector, return vector of length 1.

Take disjunction of bits in vector, return vector of length 1.

Bitwise and.

Bitwise or.

Bitwise exclusive-or.

Bitwise nand.

Bitwise nor.

Bitwise xnor.

Standard two's complement unary minus.

Standard two's complement addition.

Standard two's complement subtraction.

Standard two's complement multiplication.

Unsigned division.

Two's complement signed division.

Unsigned remainder.

Two's complement signed remainder (sign follows dividend).

Two's complement signed remainder (sign follows divisor).

Unsigned less than.

Two's complement signed less than.

Unsigned less than or equal to.

Two's complement signed less than or equal to.

Unsigned greater than or equal to.

Two's complement signed greater than or equal to.

Unsigned greater than.

Two's complement signed greater than.

Concatenate the given bit-vectors.

Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1.

Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

Repeat the given bit-vector up length i.

Shift left.

Logical shift right.

Arithmetic shift right.

Rotate bits of t1 to the left i times.

Rotate bits of t1 to the right i times.

Rotate bits of t1 to the left t2 times.

Rotate bits of t1 to the right t2 times.

Create an n bit bit-vector from the integer argument t1.

Create an integer from the bit-vector argument t1.

If is_signed is false, then the bit-vector t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in t1. If is_signed is true, t1 is treated as a signed bit-vector.

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

Array read. The argument a is the array and i is the index of the array that gets read.

Array update.

The result of this function is an array that is equal to the input array (with respect to select) on all indices except for i, where it maps to v.

The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details.

Create the constant array.

The resulting term is an array, such that a select on an arbitrary index produces the value v.

Map a function f on the the argument arrays.

The n nodes args must be of array sorts [domain -> range_i]. The function declaration f must have type range_1 .. range_n -> range. The sort of the result is [domain -> range].

Access the array default value.

Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Create the empty set.

Create the full set.

Add an element to a set.

Remove an element from a set.

Take the union of a list of sets.

Take the intersection of a list of sets.

Take the set difference between two sets.

Take the complement of a set.

Check for set membership.

Check if the first set is a subset of the second set.

Create a numeral of a given sort.

Create a real from a fraction.

Create a numeral of an int, bit-vector, or finite-domain sort.

This function can be use to create numerals that fit in a machine integer. It is slightly faster than mkNumeral since it is not necessary to parse a string.

Create a numeral of an int, bit-vector, or finite-domain sort.

This function can be use to create numerals that fit in a machine unsigned integer. It is slightly faster than mkNumeral since it is not necessary to parse a string.

Create a numeral of an int, bit-vector, or finite-domain sort.

This function can be use to create numerals that fit in a machine 64-bit integer. It is slightly faster than mkNumeral since it is not necessary to parse a string.

Create a numeral of an int, bit-vector, or finite-domain sort.

This function can be use to create numerals that fit in a machine unsigned 64-bit integer. It is slightly faster than mkNumeral since it is not necessary to parse a string.

Create a numeral of an int, bit-vector, or finite-domain sort.

Create a numeral of sort real from a Rational.

Create a numeral of sort real from a Fixed.

Create a numeral of sort real from a Real.

Create a numeral of sort int from an Integer.

Create a numeral of sort int from an Integral.

Create a numeral of sort Bit-vector from an Integer.

Create a numeral of sort Bit-vector from an Integral.

Create a pattern for quantifier instantiation.

Z3 uses pattern matching to instantiate quantifiers. If a pattern is not provided for a quantifier, then Z3 will automatically compute a set of patterns for it. However, for optimal performance, the user should provide the patterns.

Patterns comprise a list of terms. If the list comprises of more than one term, it is a called a multi-pattern.

In general, one can pass in a list of (multi-)patterns in the quantifier constructor.

Create a bound variable.

Bound variables are indexed by de-Bruijn indices.

See http://z3prover.github.io/api/html/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e

Create a forall formula.

The bound variables are de-Bruijn indices created using mkBound.

Z3 applies the convention that the last element in xs refers to the variable with index 0, the second to last element of xs refers to the variable with index 1, etc.

Create an exists formula.

Similar to mkForall.

Create a universal quantifier using a list of constants that will form the set of bound variables.

Create a existential quantifier using a list of constants that will form the set of bound variables.

Return the symbol name.

Return the sort kind of the given sort.

Return the size of the given bit-vector sort.

Get list of constructors for datatype.

Get list of recognizers for datatype.

Get list of accessors for the datatype constructor.

Return the constant declaration name as a symbol.

Returns the number of parameters of the given declaration

Returns the sort of the i-th parameter of the given function declaration

Returns the range of the given declaration.

Convert an app into AST. This is just type casting.

Return the declaration of a constant or function application.

Return the number of argument of an application. If t is an constant, then the number of arguments is 0.

Return the i-th argument of the given application.

Return a list of all the arguments of the given application.

Return the sort of an AST node.

Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.

Return the kind of the given AST.

Return True if an ast is APP_AST, False otherwise.

Convert an ast into an APP_AST. This is just type casting.

Return numeral value, as a string of a numeric constant term.

Read a Bool value from an AST

Read an Integer value from an AST

Read a Rational value from an AST

Read the Integer value from an AST of sort bit-vector.

See mkBv2int.

Evaluate an AST node in the given model.

The evaluation may fail for the following reasons:

• t contains a quantifier.
• the model m is partial.
• t is type incorrect.

Evaluate an array as a function, if possible.

Return the interpretation of the function f in the model m. Return NULL, if the model does not assign an interpretation for f. That should be interpreted as: the f does not matter.

The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3. It is the array such that forall indices i we have that (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE if the a is an as-array AST node.

Return the function declaration f associated with a (_ as_array f) node.

Return the number of entries in the given function interpretation.

Return a _point_ of the given function intepretation. It represents the value of f in a particular point.

Return the 'else' value of the given function interpretation.

Return the arity (number of arguments) of the given function interpretation.

Return the value of this point.

Return the number of arguments in a Z3_func_entry object.

Return an argument of a Z3_func_entry object.

Convert the given model into a string.

Alias for modelToString.

Type of an evaluation function for AST.

Evaluation may fail (i.e. return Nothing) for a few reasons, see modelEval.

An alias for modelEval with model completion enabled.

Evaluate an AST node of sort bool in the given model.

See modelEval and getBool.

Evaluate an AST node of sort int in the given model.

See modelEval and getInt.

Evaluate an AST node of sort real in the given model.

See modelEval and getReal.

Evaluate an AST node of sort bit-vector in the given model.

The flag signed decides whether the bit-vector value is interpreted as a signed or unsigned integer.

See modelEval and getBv.

Run a evaluation function on a Traversable data structure of ASTs (e.g. [AST], Vector AST, Maybe AST, etc).

This a generic version of evalT which can be used in combination with other helpers. For instance, mapEval (evalInt c) can be used to obtain the Integer interpretation of a list of AST of sort int.

Evaluate a collection of AST nodes in the given model.

The interpretation of a function.

Evaluate a function declaration to a list of argument/value pairs.

Pretty-printing mode for converting ASTs to strings. The mode can be one of the following:

• Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.
• Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
• Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format.
• Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format.

Set the pretty-printing mode for converting ASTs to strings.

Convert an AST to a string.

Convert a pattern to a string.

Convert a sort to a string.

Convert a FuncDecl to a string.

Convert the given benchmark into SMT-LIB formatted string.

The output format can be configured via setASTPrintMode.