# Crate z3_sys[−][src]

## Enums

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Z3 pretty printing modes (See `Z3_set_ast_print_mode`

).

The different kinds of interpreted function kinds.

Z3 error codes (See `Z3_get_error_code`

).

Precision of a given goal. Some goals can be transformed using over/under approximations.

The different kinds of parameters that can be associated with parameter sets.
(see `Z3_mk_params`

).

The different kinds of parameters that can be associated with function symbols.

The different kinds of Z3 types.

The different kinds of symbol.
In Z3, a symbol can be represented using integers and
strings. See `Z3_get_symbol_kind`

.

## Constants

## Functions

Add a constant interpretation.

Create a fresh func_interp object, add it to a model for a specified function. It has reference count 0.

Define the body of a recursive function.

Return the value `a + b`

.

Return the value `a / b`

.

Return `true`

if `a == b`

, and `false`

otherwise.

Given a multivariate polynomial `p(x_0, ..., x_{n-1})`

, return the
sign of `p(a[0], ..., a[n-1])`

.

Return `true`

if `a >= b`

, and `false`

otherwise.

Return `true`

if `a > b`

, and `false`

otherwise.

Return `true`

if `a`

is negative, and `false`

otherwise.

Return `true`

if `a`

is positive, and `false`

otherwise.

Return `true`

if `a`

can be used as value in the Z3 real algebraic
number package.

Return `true`

if `a`

is zero, and `false`

otherwise.

Return `true`

if `a <= b`

, and `false`

otherwise.

Return `true`

if `a < b`

, and `false`

otherwise.

Return the value `a * b`

.

Return `true`

if `a != b`

, and `false`

otherwise.

Return the `a^k`

Return the `a^(1/k)`

Given a multivariate polynomial `p(x_0, ..., x_{n-1}, x_n)`

, returns the
roots of the univariate polynomial `p(a[0], ..., a[n-1], x_n)`

.

Return 1 if `a`

is positive, 0 if `a`

is zero, and -1 if `a`

is negative.

Return the value `a - b`

.

Convert a `Z3_app`

into `Z3_ast`

. This is just type casting.

Append user-defined string to interaction log.

Decrement the reference counter of the given `Z3_apply_result`

object.

Return the number of subgoals in the `Z3_apply_result`

object returned by `Z3_tactic_apply`

.

Return one of the subgoals in the `Z3_apply_result`

object returned by `Z3_tactic_apply`

.

Increment the reference counter of the given `Z3_apply_result`

object.

Convert the `Z3_apply_result`

object returned by `Z3_tactic_apply`

into a string.

Return true if the map `m`

contains the AST key `k`

.

Decrement the reference counter of the given AST map.

Erase a key from the map.

Return the value associated with the key `k`

.

Increment the reference counter of the given AST map.

Store/Replace a new key, value pair in the given map.

Return the keys stored in the given map.

Remove all keys from the given map.

Return the size of the given map.

Convert the given map into a string.

Convert the given AST node into a string.

Decrement the reference counter of the given AST vector.

Return the AST at position `i`

in the AST vector `v`

.

Increment the reference counter of the given AST vector.

Add the AST `a`

in the end of the AST vector `v`

. The size of `v`

is increased by one.

Resize the AST vector `v`

.

Update position `i`

of the AST vector `v`

with the AST `a`

.

Return the size of the given AST vector.

Convert AST vector into a string.

Translate the AST vector `v`

from context `s`

into an AST vector in context `t`

.

Convert the given benchmark into SMT-LIB formatted string.

Close interaction log.

Update record field with a value.

Decrement the reference counter of the given AST.
The context `c`

should have been created using `Z3_mk_context_rc`

.
This function is a NOOP if `c`

was created using `Z3_mk_context`

.

Delete the given configuration object.

Reclaim memory allocated to constructor.

Reclaim memory allocated for constructor list.

Delete the given logical context.

Disable tracing messages tagged as `tag`

when Z3 is compiled in debug mode.
It is a NOOP otherwise

Enable tracing messages tagged as `tag`

when Z3 is compiled in debug mode.
It is a NOOP otherwise

Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next evaluation builds on top of the previous call.

Destroy all allocated resources.

Set export callback for lemmas.

Add property about the predicate `pred`

.
Add a property of predicate `pred`

at `level`

.
It gets pushed forward when possible.

Add a Database fact.

Add an assumed invariant of predicate `pred`

.

Add a universal Horn clause as a named rule.
The `horn_rule`

should be of the form:

Assert a constraint to the fixedpoint context.

Decrement the reference counter of the given fixedpoint context.

Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.

Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string.

Retrieve a formula that encodes satisfying answers to the query.

Retrieve set of background assertions from fixedpoint context.

Retrieve the current cover of `pred`

up to `level`

unfoldings.
Return just the delta that is known at `level`

. To
obtain the full set of properties of `pred`

one should query
at `level`

+1 , `level`

+2 etc, and include `level`

=-1.

Retrieve a bottom-up (from query) sequence of ground facts

Return a string describing all fixedpoint available parameters.

Query the PDR engine for the maximal levels properties are known about predicate.

Return the parameter description set for the given fixedpoint object.

Retrieve reachable states of a predicate.

Retrieve a string that describes the last status returned by `Z3_fixedpoint_query`

.

Obtain the list of rules along the counterexample trace.

Retrieve set of rules from fixedpoint context.

Obtain the list of rules along the counterexample trace.

Retrieve statistics information from the last call to `Z3_fixedpoint_query`

.

Increment the reference counter of the given fixedpoint context

Initialize the context with a user-defined state.

Pose a query against the asserted rules.

Pose a query against the asserted rules at the given level.

Pose multiple queries against the asserted rules.

Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact.

Set parameters on fixedpoint context.

Configure the predicate representation.

Register a callback for building terms based on the relational operators.

Register a callback to destructive updates.

Print the current rules and background axioms as a string.

Update a named rule. A rule with the same name must have been previously created.

Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.

Retrieves the exponent of a floating-point literal as a bit-vector expression.

Return the exponent value of a floating-point numeral as a signed 64-bit integer

Return the exponent value of a floating-point numeral as a string.

Retrieves the sign of a floating-point literal.

Retrieves the sign of a floating-point literal as a bit-vector expression.

Retrieves the significand of a floating-point literal as a bit-vector expression.

Return the significand value of a floating-point numeral as a string.

Return the significand value of a floating-point numeral as a uint64.

Retrieves the number of bits reserved for the significand in a FloatingPoint sort.

Checks whether a given floating-point numeral is a +oo or -oo.

Checks whether a given floating-point numeral is a NaN.

Checks whether a given floating-point numeral is negative.

Checks whether a given floating-point numeral is normal.

Checks whether a given floating-point numeral is positive.

Checks whether a given floating-point numeral is subnormal.

Checks whether a given floating-point numeral is +zero or -zero.

Convert a `Z3_func_decl`

into `Z3_ast`

. This is just type casting.

Decrement the reference counter of the given `Z3_func_entry`

object.

Return an argument of a `Z3_func_entry`

object.

Return the number of arguments in a `Z3_func_entry`

object.

Return the value of this point.

Increment the reference counter of the given `Z3_func_entry`

object.

add a function entry to a function interpretation.

Decrement the reference counter of the given `Z3_func_interp`

object.

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

Return the ‘else’ value of the given function interpretation.

Return a “point” of the given function interpretation. It represents
the value of `f`

in a particular point.

Return the number of entries in the given function interpretation.

Increment the reference counter of the given `Z3_func_interp`

object.

Return the ‘else’ value of the given function interpretation.

Return a lower bound for the given real algebraic number.

Return an upper bound for the given real algebraic number.

Return the i-th argument of the given application.

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.

Alias for `Z3_get_domain_size`

.

Return the domain of the given array sort.

Return the range of the given array sort.

Return the function declaration `f`

associated with a `(_ as_array f)`

node.

Return a hash code for the given AST.

Return a unique identifier for `t`

.

Return the kind of the given AST.

Return `Z3_L_TRUE`

if `a`

is true, `Z3_L_FALSE`

if it is false,
and `Z3_L_UNDEF`

otherwise.

Return the size of the given bit-vector sort.

Return idx’th constructor.

Return idx_a’th accessor for the idx_c’th constructor.

Return number of constructors for datatype.

Return idx’th recognizer.

Return the expression value associated with an expression parameter.

Return the double value associated with an double parameter.

Return the expression value associated with an expression parameter.

Return the integer value associated with an integer parameter.

Return declaration kind corresponding to declaration.

Return the constant declaration name as a symbol.

Return the number of parameters associated with a declaration.

Return the parameter type associated with a declaration.

Return the rational value, as a string, associated with a rational parameter.

Return the sort value associated with a sort parameter.

Return the double value associated with an double parameter.

Return the denominator (as a numeral AST) of a numeral AST of sort Real.

Return the sort of the i-th parameter of the given function declaration.

Return the number of parameters of the given declaration.

Return the error code for the last API call.

Return a string describing the given error code.

Return the estimated allocated memory in bytes.

Store the size of the sort in `r`

. Return `false`

if the call failed.
That is, `Z3_get_sort_kind(s) == SortKind::FiniteDomain`

Return a string that fully describes the version of Z3 in use.

Return a unique identifier for `f`

.

Retrieve congruence class representatives for terms.

Return index of de-Bruijn bound variable.

Return the number of builtin probes available in Z3.

Return the number of builtin tactics available in Z3.

Return numeral as a string in decimal notation.
The result has at most `precision`

decimal places.

Return numeral as a double.

Similar to `Z3_get_numeral_string`

, but only succeeds if
the value can fit in a machine int. Return `true`

if the call succeeded.

Similar to `Z3_get_numeral_string`

,
but only succeeds if the value can fit in a machine `int64_t`

int.
Return `true`

if the call succeeded.

Similar to `Z3_get_numeral_string`

,
but only succeeds if the value can fit as a rational number as
machine `int64_t`

int. Return `true`

if the call succeeded.

Return numeral value, as a pair of 64 bit numbers if the representation fits.

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

Similar to `Z3_get_numeral_string`

,
but only succeeds if the value can fit in a machine unsigned int.
Return `true`

if the call succeeded.

Similar to `Z3_get_numeral_string`

,
but only succeeds if the value can fit in a machine `uint64_t`

int.
Return `true`

if the call succeeded.

Return the numerator (as a numeral AST) of a numeral AST of sort Real.

Return i’th ast in pattern.

Return number of terms in pattern.

Return the name of the `i`

probe.

Return body of quantifier.

Return symbol of the i’th bound variable.

Return sort of the i’th bound variable.

Return i’th no_pattern.

Return number of bound variables of quantifier.

Return number of no_patterns used in quantifier.

Return number of patterns used in quantifier.

Return i’th pattern.

Obtain weight of quantifier.

Return the range of the given declaration.

Return arity of relation.

Return sort at i’th column of relation sort.

Return the sort of an AST node.

Return a unique identifier for `s`

.

Return the sort kind (e.g., array, tuple, int, bool, etc).

Return the sort name as a symbol.

Retrieve the string constant stored in `s`

.

Return the symbol int value.

Return `SymbolKind::Int`

if the symbol was constructed
using `Z3_mk_int_symbol`

,
and `SymbolKind::String`

if the symbol
was constructed using `Z3_mk_string_symbol`

.

Return the symbol name.

Return the name of the idx tactic.

Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.

Return the constructor declaration of the given tuple sort.

Return the number of fields of the given tuple sort.

Return Z3 version number information.

Get a global (or module) parameter.

Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers).

Set a global (or module) parameter. This setting is shared by all Z3 contexts.

Add a new formula `a`

to the given goal.
The formula is split according to the following procedure that is applied
until a fixed-point:
Conjunctions are split into separate formulas.
Negations are distributed over disjunctions, resulting in separate formulas.
If the goal is `false`

, adding new formulas is a no-op.
If the formula `a`

is `true`

, then nothing is added.
If the formula `a`

is `false`

, then the entire goal is replaced by the formula `false`

.

Convert a model of the formulas of a goal to a model of an original goal. The model may be null, in which case the returned model is valid if the goal was established satisfiable.

Decrement the reference counter of the given goal.

Return the depth of the given goal. It tracks how many transformations were applied to it.

Return a formula from the given goal.

Increment the reference counter of the given goal.

Return true if the given goal contains the formula `false`

.

Return true if the goal is empty, and it is precise or the product of a under approximation.

Return true if the goal contains false, and it is precise or the product of an over approximation.

Return the number of formulas, subformulas and terms in the given goal.

Return the “precision” of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

Erase all formulas from the given goal.

Return the number of formulas in the given goal.

Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically converted to Booleans either, so the if caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.

Convert a goal into a string.

Copy a goal `g`

from the context `source`

to the context `target`

.

Increment the reference counter of the given AST.
The context `c`

should have been created using `Z3_mk_context_rc`

.
This function is a NOOP if `c`

was created using `Z3_mk_context`

.

Interrupt the execution of a Z3 procedure.

Return true if the given AST is a real algebraic number.

The `(_ as-array f)`

AST node is a construct for assigning interpretations
for arrays in Z3.

Compare terms.

Compare terms.

compare sorts.

Determine if ast is a lambda expression.

Determine if ast is an existential quantifier.

Determine if quantifier is universal.

Check if `s`

is a regular expression sort.

Check if `s`

is a sequence sort.

Determine if `s`

is a string constant.

Check if `s`

is a string sort.

Return true if the given expression `t`

is well sorted.

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

.

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

.

Create a constant or function application.

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 array extensionality index given two arrays with the same sort. The meaning is given by the axiom: (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))

Create an array type.

Create an array type with N arguments

Create array with the same interpretation as a function. The array satisfies the property (f x) = (select (_ as-array f) x) for every argument x.

Return an empty mapping from AST to AST

Return an empty AST vector.

Pseudo-Boolean relations.

Pseudo-Boolean relations.

Create the Boolean type.

Create a bound variable.

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.

create a bit-vector numeral from a vector of Booleans.

Create a bit-vector type of the given size.

Standard two’s complement addition.

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.

Bitwise and.

Arithmetic shift right.

Logical shift right.

Standard two’s complement multiplication.

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.

Bitwise nand.

Standard two’s complement unary minus.

Check that bit-wise negation does not overflow when
`t1`

is interpreted as a signed bit-vector.

Bitwise nor.

Bitwise negation.

Bitwise or.

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

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

Two’s complement signed division.

Create a predicate that checks that the bit-wise signed division
of `t1`

and `t2`

does not overflow.

Two’s complement signed greater than or equal to.

Two’s complement signed greater than.

Shift left.

Two’s complement signed less than or equal to.

Two’s complement signed less than.

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

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

Standard two’s complement subtraction.

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.

Unsigned division.

Unsigned greater than or equal to.

Unsigned greater than.

Unsigned less than or equal to.

Unsigned less than.

Unsigned remainder.

Bitwise xnor.

Bitwise exclusive-or.

Concatenate the given bit-vectors.

Create a configuration object for the Z3 context object.

Declare and create a constant.

Create the constant array.

Create a constructor.

Create list of constructors.

Create a context using the given configuration.

Create a context using the given configuration.
This function is similar to `Z3_mk_context`

. However,
in the context returned by this function, the user
is responsible for managing `Z3_ast`

reference counters.
Managing reference counters is a burden and error-prone,
but allows the user to use the memory more efficiently.
The user must invoke `Z3_inc_ref`

for any `Z3_ast`

returned
by Z3, and `Z3_dec_ref`

whenever the `Z3_ast`

is not needed
anymore. This idiom is similar to the one used in
BDD (binary decision diagrams) packages such as CUDD.

Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.

Create mutually recursive datatypes.

Create an AST node representing `distinct(args[0], ..., args[num_args-1])`

.

Create an AST node representing `arg1 div arg2`

.

Create the empty set.

Create a enumeration sort.

Create an AST node representing `l = r`

.

Create an exists formula. Similar to `Z3_mk_forall`

.

Similar to `Z3_mk_forall_const`

.

Rotate bits of `t1`

to the left `t2`

times.

Rotate bits of `t1`

to the right `t2`

times.

Extract the bits `high`

down to `low`

from a bit-vector of
size `m`

to yield a new bit-vector of size `n`

, where `n = high - low + 1`

.

Create an AST node representing `false`

.

Create a named finite domain sort.

Create a new fixedpoint context.

Create a forall formula. It takes an expression `body`

that contains bound variables
of the same sorts as the sorts listed in the array `sorts`

. The bound variables are de-Bruijn indices created
using `Z3_mk_bound`

. The array `decl_names`

contains the names that the quantified formula uses for the
bound variables. Z3 applies the convention that the last element in the `decl_names`

and `sorts`

array
refers to the variable with index 0, the second to last element of `decl_names`

and `sorts`

refers
to the variable with index 1, etc.

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

Floating-point absolute value

Floating-point addition

Floating-point division

Floating-point equality.

Floating-point fused multiply-add.

Create an expression of FloatingPoint sort from three bit-vector expressions.

Floating-point greater than or equal.

Floating-point greater than.

Create a floating-point infinity of sort `s`

.

Predicate indicating whether `t`

is a floating-point number representing +oo or -oo.

Predicate indicating whether `t`

is a NaN.

Predicate indicating whether `t`

is a negative floating-point number.

Predicate indicating whether `t`

is a normal floating-point number.

Predicate indicating whether `t`

is a positive floating-point number.

Predicate indicating whether `t`

is a subnormal floating-point number.

Predicate indicating whether `t`

is a floating-point number with zero value, i.e., +zero or -zero.

Floating-point less than or equal.

Floating-point less than.

Maximum of floating-point numbers.

Minimum of floating-point numbers.

Floating-point multiplication

Create a floating-point NaN of sort `s`

.

Floating-point negation

Create a numeral of FloatingPoint sort from a double.

Create a numeral of FloatingPoint sort from a float.

Create a numeral of FloatingPoint sort from a signed integer.

Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.

Create a numeral of FloatingPoint sort from a sign bit and two integers.

Floating-point remainder

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

Create the RoundingMode sort.

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

Create a FloatingPoint sort.

Create the half-precision (16-bit) FloatingPoint sort.

Create the single-precision (32-bit) FloatingPoint sort.

Create the double-precision (64-bit) FloatingPoint sort.

Create the quadruple-precision (128-bit) FloatingPoint sort.

Create the double-precision (64-bit) FloatingPoint sort.

Create the half-precision (16-bit) FloatingPoint sort.

Create the quadruple-precision (128-bit) FloatingPoint sort.

Create the single-precision (32-bit) FloatingPoint sort.

Floating-point square root

Floating-point subtraction

Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.

Conversion of a term of real sort into a term of FloatingPoint sort.

Conversion of a 2’s complement signed bit-vector term into a term of FloatingPoint sort.

Conversion of a 2’s complement unsigned bit-vector term into a term of FloatingPoint sort.

Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

Conversion of a floating-point term into a real-numbered term.

Conversion of a floating-point term into a signed bit-vector.

Conversion of a floating-point term into an unsigned bit-vector.

Create a floating-point zero of sort `s`

.

Declare and create a fresh constant.

Declare a fresh constant or function.

Create the full set.

Declare a constant or function.

Create greater than or equal to.

Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

Create greater than.

Create an AST node representing `t1 iff t2`

.

Create an AST node representing `t1 implies t2`

.

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

Create an `n`

bit bit-vector from the integer argument `t1`

.

Coerce an integer to a real.

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

Create the integer type.

Create a Z3 symbol using an integer.

Integer to string conversion.

Check if a real number is an integer.

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

.

Create a lambda expression.

Create a lambda expression using a list of constants that form the set of bound variables

Create less than or equal to.

Create a list sort

Create less than.

Map f on the argument arrays.

Create an AST node representing `arg1 mod arg2`

.

Create a fresh model object. It has reference count 0.

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

.

Create an AST node representing `not(a)`

.

Create a numeral of a given sort.

Create a new optimize context.

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

.

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.

Create a pattern for quantifier instantiation.

Pseudo-Boolean relations.

Pseudo-Boolean relations.

Pseudo-Boolean relations.

Create an AST node representing `arg1 ^ arg2`

.

Return a probe associated with the given name.
The complete list of probes may be obtained using the procedures `Z3_get_num_probes`

and `Z3_get_probe_name`

.
It may also be obtained using the command `(help-tactic)`

in the SMT 2.0 front-end.

Create a quantifier - universal or existential, with pattern hints.
See the documentation for `Z3_mk_forall`

for an explanation of the parameters.

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

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

Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes

Create the complement of the regular language `re`

.

Create the concatenation of the regular languages.

Create an empty regular expression of sort `re`

.

Create an universal regular expression of sort `re`

.

Create the intersection of the regular languages.

Create a regular expression loop. The supplied regular expression `r`

is repeated
between `lo`

and `hi`

times. The `lo`

should be below `hi`

with one execution: when
supplying the value `hi`

as 0, the meaning is to repeat the argument `r`

at least
`lo`

number of times, and with an unbounded upper bound.

Create the regular language `[re]`

.

Create the regular language `re+`

.

Create the range regular expression over two sequences of length 1.

Create a regular expression sort out of a sequence sort.

Create the regular language `re*`

.

Create the union of the regular languages.

Create a real from a fraction.

Coerce a real to an integer.

Create the real type.

Declare a recursive function

Create an AST node representing `arg1 rem arg2`

.

Repeat the given bit-vector up length `i`

.

Rotate bits of `t1`

to the left `i`

times.

Rotate bits of `t1`

to the right `i`

times.

Array read.
The argument `a`

is the array and `i`

is the index of the array that gets read.

n-ary Array read.
The argument `a`

is the array and `idxs`

are the indices of the array that gets read.

Retrieve from `s`

the unit sequence positioned at position `index`

.

Concatenate sequences.

Check if `container`

contains `containee`

.

Create an empty sequence of the sequence sort `seq`

.

Extract subsequence starting at `offset`

of `length`

.

Check if `seq`

is in the language generated by the regular expression `re`

.

Return index of first occurrence of `substr`

in `s`

starting from offset `offset`

.
If `s`

does not contain `substr`

, then the value is -1, if `offset`

is the length of `s`

, then the value is -1 as well.
The function is under-specified if `offset`

is negative or larger than the length of `s`

.

Return the length of the sequence `s`

.

Check if `prefix`

is a prefix of `s`

.

Replace the first occurrence of `src`

with `dst`

in `s`

.

Create a sequence sort out of the sort for the elements.

Check if `suffix`

is a suffix of `s`

.

Create a regular expression that accepts the sequence `seq`

.

Create a unit sequence of `a`

.

Add an element to a set.

Take the complement of a set.

Remove an element to a set.

Take the set difference between two sets.

Take the intersection of a list of sets.

Check for set membership.

Create Set type.

Check for subsetness of sets.

Take the union of a list of sets.

Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of
size `m+i`

, where `m`

is the size of the given
bit-vector.

Create a new incremental solver.

Create a new solver. This solver is a “combined solver” (see combined_solver module) that internally uses a non-incremental (solver1) and an incremental solver (solver2). This combined solver changes its behaviour based on how it is used and how its parameters are set.

Create a new solver customized for the given logic.
It behaves like `Z3_mk_solver`

if the logic is unknown or unsupported.

Create a new solver that is implemented using the given tactic.
The solver supports the commands `Z3_solver_push`

and `Z3_solver_pop`

, but it
will always solve each `Z3_solver_check`

from scratch.

Array update.

n-ary Array update.

Convert string to integer.

Create a string constant out of the string that is passed in

Create a sort for 8 bit strings.

Create a Z3 symbol using a C string.

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

.

Return a tactic associated with the given name.

Create an AST node representing `true`

.

Create a tuple type.

Create an AST node representing `- arg`

.

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

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

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

Create an AST node representing `t1 xor t2`

.

Extend the given bit-vector with zeros to the (unsigned) equivalent
bit-vector of size `m+i`

, where `m`

is the size of the
given bit-vector.

Decrement the reference counter of the given model.

Evaluate the AST node `t`

in the given model.
Return `true`

if succeeded, and store the result in `v`

.

Extrapolates a model of a formula

Return the i-th constant in the given model.

Return the interpretation (i.e., assignment) of constant `a`

in the model `m`

.

Return the declaration of the i-th function in the given model.

Return the interpretation of the function `f`

in the model `m`

.

Return the number of constants assigned by the given model.

Return the number of function interpretations in the given model.

Return the number of uninterpreted sorts that `m`

assigns an
interpretation to.

Return an uninterpreted sort that `m`

assigns an interpretation.

Return the finite set of distinct values that represent the interpretation for sort `s`

.

Test if there exists an interpretation (i.e., assignment) for `a`

in the model `m`

.

Increment the reference counter of the given model.

Convert the given model into a string.

Translate model from context `c`

to context `dst`

.

Log interaction to a file.

Assert hard constraint to the optimization context.

Assert soft constraint to the optimization context.

Check consistency and produce optimal values.

Decrement the reference counter of the given optimize context.

Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

Return the set of asserted formulas on the optimization context.

Return a string containing a description of parameters accepted by optimize.

Retrieve lower bound value or approximation for the i’th optimization objective.

Retrieve lower bound value or approximation for the i’th optimization objective.
The returned vector is of length 3. It always contains numerals.
The three numerals are coefficients a, b, c and encode the result of `Z3_optimize_get_lower`

a * infinity + b + c * epsilon.

Retrieve the model for the last `Z3_optimize_check`

Return objectives on the optimization context. If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) …) If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective.

Return the parameter description set for the given optimize object.

Retrieve a string that describes the last status returned by `Z3_optimize_check`

.

Retrieve statistics information from the last call to `Z3_optimize_check`

Retrieve the unsat core for the last `Z3_optimize_check`

.

Retrieve upper bound value or approximation for the i’th optimization objective.

Retrieve upper bound value or approximation for the i’th optimization objective.

Increment the reference counter of the given optimize context

Add a maximization constraint.

Add a minimization constraint.

Backtrack one level.

Create a backtracking point.

Set parameters on optimization context.

Print the current context as a string.

Decrement the reference counter of the given parameter description set.

Retrieve documentation string corresponding to parameter name `s`

.

Return the kind associated with the given parameter name `n`

.

Return the number of parameters in the given parameter description set.

Increment the reference counter of the given parameter description set.

Return the number of parameters in the given parameter description set.

Convert a parameter description set into a string. This function is mainly used for printing the contents of a parameter description set.

Decrement the reference counter of the given parameter set.

Increment the reference counter of the given parameter set.

Add a Boolean 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`

.

Add a unsigned 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.

Validate the parameter set `p`

against the parameter description set `d`

.

Similar to `Z3_parse_smtlib2_string`

,
but reads the benchmark from a file.

Parse the given string using the SMT-LIB2 parser.

Convert a `Z3_pattern`

into `Z3_ast`

. This is just type casting.

Return the nonzero subresultants of `p`

and `q`

with respect to the “variable” `x`

.

Return a probe that evaluates to “true” when `p1`

and `p2`

evaluates to true.

Execute the probe over the goal. The probe always produce a double value. “Boolean” probes return 0.0 for false, and a value different from 0.0 for true.

Return a probe that always evaluates to val.

Decrement the reference counter of the given probe.

Return a probe that evaluates to “true” when the value returned by `p1`

is equal to the value returned by `p2`

.

Return a probe that evaluates to “true” when the value returned by `p1`

is greater than or equal to the value returned by `p2`

.

Return a string containing a description of the probe with the given name.

Return a probe that evaluates to “true” when the value returned by `p1`

is greater than the value returned by `p2`

.

Increment the reference counter of the given probe.

Return a probe that evaluates to “true” when the value returned by `p1`

is less than or equal to the value returned by `p2`

.

Return a probe that evaluates to “true” when the value returned by `p1`

is less than the value returned by `p2`

.

Return a probe that evaluates to “true” when `p`

does not evaluate to true.

Return a probe that evaluates to “true” when `p1`

or `p2`

evaluates to true.

Best-effort quantifier elimination

Project variables given a model

Project variables given a model

Query constructor for declared functions.

Return the value `a + b`

.

Delete a RCF numeral created using the RCF API.

Return the value `a / b`

.

Return `true`

if `a == b`

.

Return `true`

if `a >= b`

.

Extract the “numerator” and “denominator” of the given RCF numeral.

Return `true`

if `a > b`

.

Return the value `1/a`

.

Return `true`

if `a <= b`

.

Return `true`

if `a < b`

.

Return e (Euler’s constant)

Return a new infinitesimal that is smaller than all elements in the Z3 field.

Return Pi

Return a RCF rational using the given string.

Store in roots the roots of the polynomial `a[n-1]*x^{n-1} + ... + a[0]`

.
The output vector `roots`

must have size `n`

.
It returns the number of roots of the polynomial.

Return a RCF small integer.

Return the value `a * b`

.

Return the value `-a`

.

Return `true`

if `a != b`

.

Convert the RCF numeral into a string in decimal notation.

Convert the RCF numeral into a string.

Return the value `a^k`

.

Return the value `a - b`

.

Reset all allocated resources.

Select mode for the format used for pretty-printing AST nodes.

Set an error.

Register a Z3 error handler.

Set a configuration parameter.

Interface to simplifier.

Interface to simplifier.

Return a string describing all available parameters.

Return the parameter description set for the simplify procedure.

Assert a constraint into the solver.

Assert a constraint `a`

into the solver, and track it (in the
unsat) core using the Boolean constant `p`

.

Check whether the assertions in a given solver are consistent or not.

Check whether the assertions in the given solver and optional assumptions are consistent or not.

Extract a next cube for a solver. The last cube is the constant `true`

or `false`

.
The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled
using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction.

Decrement the reference counter of the given solver.

load solver assertions from a file.

load solver assertions from a string.

Return the set of asserted formulas on the solver.

retrieve consequences from solver that determine values of the supplied function symbols.

Return a string describing all solver available parameters.

Retrieve the model for the last `Z3_solver_check`

or `Z3_solver_check_assumptions`

Return the set of non units in the solver state.

Return the number of backtracking points.

Return the parameter description set for the given solver object.

Retrieve the proof for the last `Z3_solver_check`

or `Z3_solver_check_assumptions`

Return a brief justification for an “unknown” result (i.e., `Z3_L_UNDEF`

) for
the commands `Z3_solver_check`

and `Z3_solver_check_assumptions`

Return statistics for the given solver.

Return the set of units modulo model conversion.

Retrieve the unsat core for the last `Z3_solver_check_assumptions`

The unsat core is a subset of the assumptions `a`

.

Ad-hoc method for importing model conversion from solver.

Increment the reference counter of the given solver.

Backtrack `n`

backtracking points.

Create a backtracking point.

Remove all assertions from the solver.

Set the given solver using the given parameters.

Convert a solver into a string.

Copy a solver `s`

from the context `source`

to the context `target`

.

Convert a `Z3_sort`

into `Z3_ast`

. This is just type casting.

Decrement the reference counter of the given statistics object.

Return the double value of the given statistical data.

Return the key (a string) for a particular statistical data.

Return the unsigned value of the given statistical data.

Increment the reference counter of the given statistics object.

Return `true`

if the given statistical data is a double.

Return `true`

if the given statistical data is a unsigned integer.

Return the number of statistical data in `s`

.

Convert a statistics into a string.

Substitute every occurrence of `from[i]`

in `a`

with `to[i]`

, for `i`

smaller than `num_exprs`

.

Substitute the free variables in `a`

with the expressions in `to`

.

Return a tactic that applies `t1`

to a given goal and `t2`

to every subgoal produced by `t1`

.

Apply tactic `t`

to the goal `g`

.

Apply tactic `t`

to the goal `g`

using the parameter set `p`

.

Return a tactic that applies `t1`

to a given goal if the probe `p`

evaluates to true,
and `t2`

if `p`

evaluates to false.

Decrement the reference counter of the given tactic.

Return a tactic that always fails.

Return a tactic that fails if the probe `p`

evaluates to false.

Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false).

Return a string containing a description of the tactic with the given name.

Return a string containing a description of parameters accepted by the given tactic.

Return the parameter description set for the given tactic object.

Increment the reference counter of the given tactic.

Return a tactic that first applies `t1`

to a given goal,
if it fails then returns the result of `t2`

applied to the given goal.

Return a tactic that applies `t1`

to a given goal and then `t2`

to every subgoal produced by `t1`

. The subgoals are processed in parallel.

Return a tactic that applies the given tactics in parallel.

Return a tactic that keeps applying `t`

until the goal is not modified anymore or the maximum
number of iterations `max`

is reached.

Return a tactic that just return the given goal.

Return a tactic that applies `t`

to a given goal for `ms`

milliseconds.
If `t`

does not terminate in `ms`

milliseconds, then it fails.

Return a tactic that applies `t`

using the given set of parameters.

Return a tactic that applies `t`

to a given goal is the probe `p`

evaluates to true.
If `p`

evaluates to false, then the new tactic behaves like the skip tactic.

Convert an `ast`

into an `Z3_App`

. This is just type casting.

Convert an AST into a `Z3_func_decl`

. This is just type casting.

Enable/disable printing warning messages to the console.

Translate/Copy the AST `a`

from context `source`

to context `target`

.

Set a value of a context parameter.

Update the arguments of term `a`

using the arguments `args`

.

## Type Definitions

Kind of AST used to represent function applications.

Collection of subgoals resulting from applying of a tactic to a goal.

Abstract Syntax Tree node. That is, the data structure used in Z3 to represent terms, formulas, and types.

Vector of `Z3_ast`

objects.

Configuration object used to initialize logical contexts.

Type constructor for a (recursive) datatype.

List of constructors for a (recursive) datatype.

Manager of all other Z3 objects, global configuration options, etc.

Z3 custom error handler (See `Z3_set_error_handler`

).

Context for the recursive predicate solver.

The following utilities allows adding user-defined domains.

Kind of AST used to represent function symbols.

Representation of the value of a
`Z3_func_interp`

at a particular point.

Interpretation of a function in a model.

Set of formulas that can be solved and/or transformed using tactics and solvers.

Lifted Boolean type: `false`

, `undefined`

, `true`

.

Model for the constraints inserted into the logical context.

Context for solving optimization queries.

Provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.

Parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.

Kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation.

Function/predicate used to inspect a goal and collect information that may be used to decide which solver and/or preprocessing step will be used.

(Incremental) solver, possibly specialized by a particular tactic or logic.

Kind of AST used to represent types.

Statistical data for a solver.

Z3 string type. It is just an alias for `const char *`

.

Lisp-like symbol used to name types, constants, and functions. A symbol can be created using string or integers.

Basic building block for creating custom solvers for specific problem domains.