## Expand description

## Z3

Z3 is a theorem prover from Microsoft Research.

This crate provides low-level bindings that provide no real affordances for usage from Rust and that mirror the C API.

For bindings that are easier to use from Rust, see the higher level bindings in the Z3 crate.

Example:

```
use z3_sys::*;
unsafe {
let cfg = Z3_mk_config();
let ctx = Z3_mk_context(cfg);
let a = Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_false(ctx), Z3_mk_true(ctx)));
let b = Z3_mk_not(ctx, Z3_mk_iff(ctx, Z3_mk_false(ctx), Z3_mk_true(ctx)));
assert_eq!(Z3_mk_true(ctx), Z3_simplify(ctx, a));
assert_eq!(Z3_mk_true(ctx), Z3_simplify(ctx, b));
Z3_del_config(cfg);
Z3_del_context(ctx);
}
```

## 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.
- Z3_add_rec_def
^{⚠}Define the body of a recursive function. - Z3_algebraic_add
^{⚠}Return the value`a + b`

. - Z3_algebraic_div
^{⚠}Return the value`a / b`

. - Z3_algebraic_eq
^{⚠}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])`

. - Z3_algebraic_ge
^{⚠}Return`true`

if`a >= b`

, and`false`

otherwise. - Z3_algebraic_gt
^{⚠}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. - Z3_algebraic_le
^{⚠}Return`true`

if`a <= b`

, and`false`

otherwise. - Z3_algebraic_lt
^{⚠}Return`true`

if`a < b`

, and`false`

otherwise. - Z3_algebraic_mul
^{⚠}Return the value`a * b`

. - Z3_algebraic_neq
^{⚠}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. - Z3_algebraic_sub
^{⚠}Return the value`a - b`

. - Z3_app_to_ast
^{⚠} - Z3_append_log
^{⚠}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.
- Z3_ast_map_erase
^{⚠}Erase a key from the map. - Z3_ast_map_find
^{⚠}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.
- Z3_ast_map_keys
^{⚠}Return the keys stored in the given map. - Z3_ast_map_reset
^{⚠}Remove all keys from the given map. - Z3_ast_map_size
^{⚠}Return the size of the given map. - Convert the given map into a string.
- Z3_ast_to_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.
- Z3_close_log
^{⚠}Close interaction log. - Update record field with a value.
- Z3_dec_ref
^{⚠}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`

. - Z3_del_config
^{⚠}Delete the given configuration object. - Reclaim memory allocated to constructor.
- Reclaim memory allocated for constructor list.
- Z3_del_context
^{⚠}Delete the given logical context. - Z3_disable_trace
^{⚠}Disable tracing messages tagged as`tag`

when Z3 is compiled in debug mode. It is a NOOP otherwise - Z3_enable_trace
^{⚠}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.
- Z3_fpa_get_ebits
^{⚠}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.
- Z3_fpa_get_sbits
^{⚠}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. - Convert the given func decl AST node into a string.
- 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. - Set 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.
- Z3_get_app_arg
^{⚠}Return the i-th argument of the given application. - Z3_get_app_decl
^{⚠}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. - Z3_get_arity
^{⚠}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. - Z3_get_ast_hash
^{⚠}Return a hash code for the given AST. - Z3_get_ast_id
^{⚠}Return a unique identifier for`t`

. - Z3_get_ast_kind
^{⚠}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.
- Z3_get_decl_kind
^{⚠}Return declaration kind corresponding to declaration. - Z3_get_decl_name
^{⚠}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.
- Z3_get_domain
^{⚠}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.
- Z3_get_error_msg
^{⚠}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. - Z3_get_numerator
^{⚠}Return the numerator (as a numeral AST) of a numeral AST of sort Real. - Z3_get_pattern
^{⚠}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.
- Z3_get_range
^{⚠}Return the range of the given declaration. - Return arity of relation.
- Return sort at i’th column of relation sort.
- Z3_get_sort
^{⚠}Return the sort of an AST node. - Z3_get_sort_id
^{⚠}Return a unique identifier for`s`

. - Z3_get_sort_kind
^{⚠}Return the sort kind (e.g., array, tuple, int, bool, etc). - Z3_get_sort_name
^{⚠}Return the sort name as a symbol. - Z3_get_string
^{⚠}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.
- Z3_get_version
^{⚠}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.
- Z3_goal_assert
^{⚠}Add a new formula`a`

to the given goal. - 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.
- Z3_goal_dec_ref
^{⚠}Decrement the reference counter of the given goal. - Z3_goal_depth
^{⚠}Return the depth of the given goal. It tracks how many transformations were applied to it. - Z3_goal_formula
^{⚠}Return a formula from the given goal. - Z3_goal_inc_ref
^{⚠}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.
- Z3_goal_reset
^{⚠}Erase all formulas from the given goal. - Z3_goal_size
^{⚠}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`

. - Z3_inc_ref
^{⚠}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`

. - Z3_interrupt
^{⚠}Interrupt the execution of a Z3 procedure. - Return true if the given AST is a real algebraic number.
- Z3_is_app
^{⚠} - Z3_is_as_array
^{⚠}The`(_ as-array f)`

AST node is a construct for assigning interpretations for arrays in Z3. - Z3_is_eq_ast
^{⚠}Compare terms. - Compare terms.
- Z3_is_eq_sort
^{⚠}compare sorts. - Z3_is_lambda
^{⚠}Determine if ast is a lambda expression. - Determine if ast is an existential quantifier.
- Determine if quantifier is universal.
- Z3_is_re_sort
^{⚠}Check if`s`

is a regular expression sort. - Z3_is_seq_sort
^{⚠}Check if`s`

is a sequence sort. - Z3_is_string
^{⚠}Determine if`s`

is a string constant. - Check if
`s`

is a string sort. - Return true if the given expression
`t`

is well sorted. - Z3_mk_add
^{⚠}Create an AST node representing`args[0] + ... + args[num_args-1]`

. - Z3_mk_and
^{⚠}Create an AST node representing`args[0] and ... and args[num_args-1]`

. - Z3_mk_app
^{⚠}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.
- Z3_mk_array_ext
^{⚠}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)) - Z3_mk_array_sort
^{⚠}Create an array type. - Create an array type with N arguments
- Z3_mk_as_array
^{⚠}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. - Z3_mk_ast_map
^{⚠}Return an empty mapping from AST to AST - Z3_mk_ast_vector
^{⚠}Return an empty AST vector. - Z3_mk_atleast
^{⚠}Pseudo-Boolean relations. - Z3_mk_atmost
^{⚠}Pseudo-Boolean relations. - Z3_mk_bool_sort
^{⚠}Create the Boolean type. - Z3_mk_bound
^{⚠}Create a bound variable. - Z3_mk_bv2int
^{⚠}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. - Z3_mk_bv_numeral
^{⚠}create a bit-vector numeral from a vector of Booleans. - Z3_mk_bv_sort
^{⚠}Create a bit-vector type of the given size. - Z3_mk_bvadd
^{⚠}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. - Z3_mk_bvand
^{⚠}Bitwise and. - Z3_mk_bvashr
^{⚠}Arithmetic shift right. - Z3_mk_bvlshr
^{⚠}Logical shift right. - Z3_mk_bvmul
^{⚠}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. - Z3_mk_bvnand
^{⚠}Bitwise nand. - Z3_mk_bvneg
^{⚠}Standard two’s complement unary minus. - Check that bit-wise negation does not overflow when
`t1`

is interpreted as a signed bit-vector. - Z3_mk_bvnor
^{⚠}Bitwise nor. - Z3_mk_bvnot
^{⚠}Bitwise negation. - Z3_mk_bvor
^{⚠}Bitwise or. - Z3_mk_bvredand
^{⚠}Take conjunction of bits in vector, return vector of length 1. - Z3_mk_bvredor
^{⚠}Take disjunction of bits in vector, return vector of length 1. - Z3_mk_bvsdiv
^{⚠}Two’s complement signed division. - Create a predicate that checks that the bit-wise signed division of
`t1`

and`t2`

does not overflow. - Z3_mk_bvsge
^{⚠}Two’s complement signed greater than or equal to. - Z3_mk_bvsgt
^{⚠}Two’s complement signed greater than. - Z3_mk_bvshl
^{⚠}Shift left. - Z3_mk_bvsle
^{⚠}Two’s complement signed less than or equal to. - Z3_mk_bvslt
^{⚠}Two’s complement signed less than. - Z3_mk_bvsmod
^{⚠}Two’s complement signed remainder (sign follows divisor). - Z3_mk_bvsrem
^{⚠}Two’s complement signed remainder (sign follows dividend). - Z3_mk_bvsub
^{⚠}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. - Z3_mk_bvudiv
^{⚠}Unsigned division. - Z3_mk_bvuge
^{⚠}Unsigned greater than or equal to. - Z3_mk_bvugt
^{⚠}Unsigned greater than. - Z3_mk_bvule
^{⚠}Unsigned less than or equal to. - Z3_mk_bvult
^{⚠}Unsigned less than. - Z3_mk_bvurem
^{⚠}Unsigned remainder. - Z3_mk_bvxnor
^{⚠}Bitwise xnor. - Z3_mk_bvxor
^{⚠}Bitwise exclusive-or. - Z3_mk_concat
^{⚠}Concatenate the given bit-vectors. - Z3_mk_config
^{⚠}Create a configuration object for the Z3 context object. - Z3_mk_const
^{⚠}Declare and create a constant. - Create the constant array.
- Create a constructor.
- Create list of constructors.
- Z3_mk_context
^{⚠}Create a context using the given configuration. - Z3_mk_context_rc
^{⚠}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. - Z3_mk_datatype
^{⚠}Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort. - Z3_mk_datatypes
^{⚠}Create mutually recursive datatypes. - Z3_mk_distinct
^{⚠}Create an AST node representing`distinct(args[0], ..., args[num_args-1])`

. - Z3_mk_div
^{⚠}Create an AST node representing`arg1 div arg2`

. - Z3_mk_empty_set
^{⚠}Create the empty set. - Create a enumeration sort.
- Z3_mk_eq
^{⚠}Create an AST node representing`l = r`

. - Z3_mk_exists
^{⚠}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. - Z3_mk_extract
^{⚠}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`

. - Z3_mk_false
^{⚠}Create an AST node representing`false`

. - Create a named finite domain sort.
- Z3_mk_fixedpoint
^{⚠}Create a new fixedpoint context. - Z3_mk_forall
^{⚠}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.
- Z3_mk_fpa_abs
^{⚠}Floating-point absolute value - Z3_mk_fpa_add
^{⚠}Floating-point addition - Z3_mk_fpa_div
^{⚠}Floating-point division - Z3_mk_fpa_eq
^{⚠}Floating-point equality. - Z3_mk_fpa_fma
^{⚠}Floating-point fused multiply-add. - Z3_mk_fpa_fp
^{⚠}Create an expression of FloatingPoint sort from three bit-vector expressions. - Z3_mk_fpa_geq
^{⚠}Floating-point greater than or equal. - Z3_mk_fpa_gt
^{⚠}Floating-point greater than. - Z3_mk_fpa_inf
^{⚠}Create a floating-point infinity of sort`s`

. - Predicate indicating whether
`t`

is a floating-point number representing +oo or -oo. - Z3_mk_fpa_is_nan
^{⚠}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. - Z3_mk_fpa_leq
^{⚠}Floating-point less than or equal. - Z3_mk_fpa_lt
^{⚠}Floating-point less than. - Z3_mk_fpa_max
^{⚠}Maximum of floating-point numbers. - Z3_mk_fpa_min
^{⚠}Minimum of floating-point numbers. - Z3_mk_fpa_mul
^{⚠}Floating-point multiplication - Z3_mk_fpa_nan
^{⚠}Create a floating-point NaN of sort`s`

. - Z3_mk_fpa_neg
^{⚠}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.
- Z3_mk_fpa_rem
^{⚠}Floating-point remainder - Z3_mk_fpa_rna
^{⚠}Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. - Z3_mk_fpa_rne
^{⚠}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.
- Z3_mk_fpa_rtn
^{⚠}Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. - Z3_mk_fpa_rtp
^{⚠}Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. - Z3_mk_fpa_rtz
^{⚠}Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. - Z3_mk_fpa_sort
^{⚠}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.
- Z3_mk_fpa_sqrt
^{⚠}Floating-point square root - Z3_mk_fpa_sub
^{⚠}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.
- Z3_mk_fpa_to_sbv
^{⚠}Conversion of a floating-point term into a signed bit-vector. - Z3_mk_fpa_to_ubv
^{⚠}Conversion of a floating-point term into an unsigned bit-vector. - Z3_mk_fpa_zero
^{⚠}Create a floating-point zero of sort`s`

. - Declare and create a fresh constant.
- Declare a fresh constant or function.
- Z3_mk_full_set
^{⚠}Create the full set. - Z3_mk_func_decl
^{⚠}Declare a constant or function. - Z3_mk_ge
^{⚠}Create greater than or equal to. - Z3_mk_goal
^{⚠}Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. - Z3_mk_gt
^{⚠}Create greater than. - Z3_mk_iff
^{⚠}Create an AST node representing`t1 iff t2`

. - Z3_mk_implies
^{⚠}Create an AST node representing`t1 implies t2`

. - Z3_mk_int
^{⚠}Create a numeral of an int, bit-vector, or finite-domain sort. - Z3_mk_int2bv
^{⚠}Create an`n`

bit bit-vector from the integer argument`t1`

. - Z3_mk_int2real
^{⚠}Coerce an integer to a real. - Z3_mk_int64
^{⚠}Create a numeral of a int, bit-vector, or finite-domain sort. - Z3_mk_int_sort
^{⚠}Create the integer type. - Z3_mk_int_symbol
^{⚠}Create a Z3 symbol using an integer. - Z3_mk_int_to_str
^{⚠}Integer to string conversion. - Z3_mk_is_int
^{⚠}Check if a real number is an integer. - Z3_mk_ite
^{⚠}Create an AST node representing an if-then-else:`ite(t1, t2, t3)`

. - Z3_mk_lambda
^{⚠}Create a lambda expression. - Create a lambda expression using a list of constants that form the set of bound variables
- Z3_mk_le
^{⚠}Create less than or equal to. - Z3_mk_list_sort
^{⚠}Create a list sort - Z3_mk_lt
^{⚠}Create less than. - Z3_mk_map
^{⚠}Map f on the argument arrays. - Z3_mk_mod
^{⚠}Create an AST node representing`arg1 mod arg2`

. - Z3_mk_model
^{⚠}Create a fresh model object. It has reference count 0. - Z3_mk_mul
^{⚠}Create an AST node representing`args[0] * ... * args[num_args-1]`

. - Z3_mk_not
^{⚠}Create an AST node representing`not(a)`

. - Z3_mk_numeral
^{⚠}Create a numeral of a given sort. - Z3_mk_optimize
^{⚠}Create a new optimize context. - Z3_mk_or
^{⚠}Create an AST node representing`args[0] or ... or args[num_args-1]`

. - Z3_mk_params
^{⚠}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. - Z3_mk_pattern
^{⚠}Create a pattern for quantifier instantiation. - Z3_mk_pbeq
^{⚠}Pseudo-Boolean relations. - Z3_mk_pbge
^{⚠}Pseudo-Boolean relations. - Z3_mk_pble
^{⚠}Pseudo-Boolean relations. - Z3_mk_power
^{⚠}Create an AST node representing`arg1 ^ arg2`

. - Z3_mk_probe
^{⚠}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. - Z3_mk_quantifier
^{⚠}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`

. - Z3_mk_re_concat
^{⚠}Create the concatenation of the regular languages. - Z3_mk_re_empty
^{⚠}Create an empty regular expression of sort`re`

. - Z3_mk_re_full
^{⚠}Create an universal regular expression of sort`re`

. - Create the intersection of the regular languages.
- Z3_mk_re_loop
^{⚠}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. - Z3_mk_re_option
^{⚠}Create the regular language`[re]`

. - Z3_mk_re_plus
^{⚠}Create the regular language`re+`

. - Z3_mk_re_range
^{⚠}Create the range regular expression over two sequences of length 1. - Z3_mk_re_sort
^{⚠}Create a regular expression sort out of a sequence sort. - Z3_mk_re_star
^{⚠}Create the regular language`re*`

. - Z3_mk_re_union
^{⚠}Create the union of the regular languages. - Z3_mk_real
^{⚠}Create a real from a fraction. - Z3_mk_real2int
^{⚠}Coerce a real to an integer. - Z3_mk_real_sort
^{⚠}Create the real type. - Declare a recursive function
- Z3_mk_rem
^{⚠}Create an AST node representing`arg1 rem arg2`

. - Z3_mk_repeat
^{⚠}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. - Z3_mk_select
^{⚠}Array read. The argument`a`

is the array and`i`

is the index of the array that gets read. - Z3_mk_select_n
^{⚠}n-ary Array read. The argument`a`

is the array and`idxs`

are the indices of the array that gets read. - Z3_mk_seq_at
^{⚠}Retrieve from`s`

the unit sequence positioned at position`index`

. - Z3_mk_seq_concat
^{⚠}Concatenate sequences. - Check if
`container`

contains`containee`

. - Z3_mk_seq_empty
^{⚠}Create an empty sequence of the sequence sort`seq`

. - Extract subsequence starting at
`offset`

of`length`

. - Z3_mk_seq_in_re
^{⚠}Check if`seq`

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

. - Z3_mk_seq_index
^{⚠}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`

. - Z3_mk_seq_length
^{⚠}Return the length of the sequence`s`

. - Z3_mk_seq_prefix
^{⚠}Check if`prefix`

is a prefix of`s`

. - Replace the first occurrence of
`src`

with`dst`

in`s`

. - Z3_mk_seq_sort
^{⚠}Create a sequence sort out of the sort for the elements. - Z3_mk_seq_suffix
^{⚠}Check if`suffix`

is a suffix of`s`

. - Z3_mk_seq_to_re
^{⚠}Create a regular expression that accepts the sequence`seq`

. - Z3_mk_seq_unit
^{⚠}Create a unit sequence of`a`

. - Z3_mk_set_add
^{⚠}Add an element to a set. - Take the complement of a set.
- Z3_mk_set_del
^{⚠}Remove an element to a set. - Take the set difference between two sets.
- Take the intersection of a list of sets.
- Z3_mk_set_member
^{⚠}Check for set membership. - Z3_mk_set_sort
^{⚠}Create Set type. - Z3_mk_set_subset
^{⚠}Check for subsetness of sets. - Z3_mk_set_union
^{⚠}Take the union of a list of sets. - Z3_mk_sign_ext
^{⚠}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.
- Z3_mk_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. - Z3_mk_store
^{⚠}Array update. - Z3_mk_store_n
^{⚠}n-ary Array update. - Z3_mk_str_to_int
^{⚠}Convert string to integer. - Z3_mk_string
^{⚠}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.
- Z3_mk_sub
^{⚠}Create an AST node representing`args[0] - ... - args[num_args - 1]`

. - Z3_mk_tactic
^{⚠}Return a tactic associated with the given name. - Z3_mk_true
^{⚠}Create an AST node representing`true`

. - Z3_mk_tuple_sort
^{⚠}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.
- Z3_mk_xor
^{⚠}Create an AST node representing`t1 xor t2`

. - Z3_mk_zero_ext
^{⚠}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. - Z3_model_dec_ref
^{⚠}Decrement the reference counter of the given model. - Z3_model_eval
^{⚠}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`

. - Z3_model_inc_ref
^{⚠}Increment the reference counter of the given model. - Convert the given model into a string.
- Translate model from context
`c`

to context`dst`

. - Z3_open_log
^{⚠}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.
- Z3_optimize_pop
^{⚠}Backtrack one level. - Z3_optimize_push
^{⚠}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. - Convert the given pattern AST node into a string.
- Return the nonzero subresultants of
`p`

and`q`

with respect to the “variable”`x`

. - Z3_probe_and
^{⚠}Return a probe that evaluates to “true” when`p1`

and`p2`

evaluates to true. - Z3_probe_apply
^{⚠}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. - Z3_probe_const
^{⚠}Return a probe that always evaluates to val. - Z3_probe_dec_ref
^{⚠}Decrement the reference counter of the given probe. - Z3_probe_eq
^{⚠}Return a probe that evaluates to “true” when the value returned by`p1`

is equal to the value returned by`p2`

. - Z3_probe_ge
^{⚠}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.
- Z3_probe_gt
^{⚠}Return a probe that evaluates to “true” when the value returned by`p1`

is greater than the value returned by`p2`

. - Z3_probe_inc_ref
^{⚠}Increment the reference counter of the given probe. - Z3_probe_le
^{⚠}Return a probe that evaluates to “true” when the value returned by`p1`

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

. - Z3_probe_lt
^{⚠}Return a probe that evaluates to “true” when the value returned by`p1`

is less than the value returned by`p2`

. - Z3_probe_not
^{⚠}Return a probe that evaluates to “true” when`p`

does not evaluate to true. - Z3_probe_or
^{⚠}Return a probe that evaluates to “true” when`p1`

or`p2`

evaluates to true. - Z3_qe_lite
^{⚠}Best-effort quantifier elimination - Project variables given a model
- Project variables given a model
- Query constructor for declared functions.
- Z3_rcf_add
^{⚠}Return the value`a + b`

. - Z3_rcf_del
^{⚠}Delete a RCF numeral created using the RCF API. - Z3_rcf_div
^{⚠}Return the value`a / b`

. - Z3_rcf_eq
^{⚠}Return`true`

if`a == b`

. - Z3_rcf_ge
^{⚠}Return`true`

if`a >= b`

. - Extract the “numerator” and “denominator” of the given RCF numeral.
- Z3_rcf_gt
^{⚠}Return`true`

if`a > b`

. - Z3_rcf_inv
^{⚠}Return the value`1/a`

. - Z3_rcf_le
^{⚠}Return`true`

if`a <= b`

. - Z3_rcf_lt
^{⚠}Return`true`

if`a < b`

. - Z3_rcf_mk_e
^{⚠}Return e (Euler’s constant) - Return a new infinitesimal that is smaller than all elements in the Z3 field.
- Z3_rcf_mk_pi
^{⚠}Return Pi - Return a RCF rational using the given string.
- Z3_rcf_mk_roots
^{⚠}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.
- Z3_rcf_mul
^{⚠}Return the value`a * b`

. - Z3_rcf_neg
^{⚠}Return the value`-a`

. - Z3_rcf_neq
^{⚠}Return`true`

if`a != b`

. - Convert the RCF numeral into a string in decimal notation.
- Convert the RCF numeral into a string.
- Z3_rcf_power
^{⚠}Return the value`a^k`

. - Z3_rcf_sub
^{⚠}Return the value`a - b`

. - Z3_reset_memory
^{⚠}Reset all allocated resources. - Select mode for the format used for pretty-printing AST nodes.
- Z3_set_error
^{⚠}Set an error. - Register a Z3 error handler.
- Set a configuration parameter.
- Z3_simplify
^{⚠}Interface to simplifier. - Z3_simplify_ex
^{⚠}Interface to simplifier. - Return a string describing all available parameters.
- Return the parameter description set for the simplify procedure.
- Z3_solver_assert
^{⚠}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`

. - Z3_solver_check
^{⚠}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.
- Z3_solver_cube
^{⚠}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`

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

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

) for the commands`Z3_solver_check`

- 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.
- Z3_solver_pop
^{⚠}Backtrack`n`

backtracking points. - Z3_solver_push
^{⚠}Create a backtracking point. - Z3_solver_reset
^{⚠}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`

. - Z3_sort_to_ast
^{⚠} - Convert the given sort AST node into a string.
- Z3_stats_dec_ref
^{⚠}Decrement the reference counter of the given statistics object. - Return the double value of the given statistical data.
- Z3_stats_get_key
^{⚠}Return the key (a string) for a particular statistical data. - Return the unsigned value of the given statistical data.
- Z3_stats_inc_ref
^{⚠}Increment the reference counter of the given statistics object. - Return
`true`

if the given statistical data is a double. - Z3_stats_is_uint
^{⚠}Return`true`

if the given statistical data is a unsigned integer. - Z3_stats_size
^{⚠}Return the number of statistical data in`s`

. - Convert a statistics into a string.
- Z3_substitute
^{⚠}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`

. - Z3_tactic_apply
^{⚠}Apply tactic`t`

to the goal`g`

. - Apply tactic
`t`

to the goal`g`

using the parameter set`p`

. - Z3_tactic_cond
^{⚠}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.
- Z3_tactic_fail
^{⚠}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. - Z3_tactic_par_or
^{⚠}Return a tactic that applies the given tactics in parallel. - Z3_tactic_repeat
^{⚠}Return a tactic that keeps applying`t`

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

is reached. - Z3_tactic_skip
^{⚠}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. - Z3_tactic_when
^{⚠}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. - Z3_to_app
^{⚠}Convert an`ast`

into an`Z3_app`

. This is just type casting. - Z3_to_func_decl
^{⚠}Convert an AST into a`Z3_func_decl`

. This is just type casting. - Enable/disable printing warning messages to the console.
- Z3_translate
^{⚠}Translate/Copy the AST`a`

from context`source`

to context`target`

. - Set a value of a context parameter.
- Z3_update_term
^{⚠}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.