Crate z3_sys 

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.

Build configuration

This crate needs to locate a Z3 library at build time. The method is controlled by Cargo features and environment variables.

Features

Feature	Behaviour
(default)	Link against a system-installed Z3 (brew install z3, etc.)
vendored	Build Z3 from source using cmake and statically link it
bundled	Deprecated. Alias for vendored; will be removed in a future release
gh-release	Build against a pre-compiled Z3 static library from GitHub Releases
vcpkg	Use a Z3 installed via vcpkg
bindgen	Regenerate functions.rs from local Z3 headers at build time

Environment variables

vendored feature

The vendored feature builds Z3 from source using cmake and statically links it. The Z3 source tree is shipped inside the z3-src crate and compiled locally — no network access is required at build time.

By default the Z3 version built is whatever version z3-src bundles. To use a specific version without managing source yourself, gh-release with Z3_SYS_Z3_VERSION is a simpler alternative.

Using your own Z3 checkout: Set Z3_SRC_SOURCE_DIR to the absolute path of a Z3 source tree:

Z3_SRC_SOURCE_DIR=/absolute/path/to/z3 cargo build

To use a project-relative path, add the following to your project’s .cargo/config.toml. The relative = true key tells Cargo to resolve the path relative to the config file’s location:

[env]
Z3_SRC_SOURCE_DIR = { value = "path/to/z3", relative = true }

Note: A z3 directory in your own project or workspace is not picked up automatically — you must set Z3_SRC_SOURCE_DIR explicitly, even if you have a Z3 git submodule in your repo.

Other variables

Variable	Feature	Description
Z3_SYS_Z3_HEADER	bindgen	Path to z3.h; defaults to z3-src/z3/src/api/z3.h
Z3_SYS_UPDATE_GENERATED	bindgen	Set to 1 to also write src/generated/functions.rs and src/generated/enums.rs
Z3_LIBRARY_PATH_OVERRIDE	default	Add an extra library search path for the linker
Z3_SYS_Z3_VERSION	gh-release	Z3 version to download (e.g. 4.13.0)
READ_ONLY_GITHUB_TOKEN	gh-release	GitHub PAT to avoid API rate limits in CI
CXXSTDLIB	any	Override which C++ standard library to link (e.g. c++, stdc++)

Example

use z3_sys::*;

unsafe {
    let cfg = Z3_mk_config().unwrap();
    let ctx = Z3_mk_context(cfg).unwrap();

    let a = Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_false(ctx).unwrap(), Z3_mk_true(ctx).unwrap()).unwrap()).unwrap();
    let b = Z3_mk_not(ctx, Z3_mk_iff(ctx, Z3_mk_false(ctx).unwrap(), Z3_mk_true(ctx).unwrap()).unwrap()).unwrap();
    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

AstKind

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

AstPrintMode

Z3 pretty printing modes (See Z3_set_ast_print_mode).

DeclKind

The different kinds of interpreted function kinds.

ErrorCode

Z3 error codes (See Z3_get_error_code).

GoalPrec

A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations.

ParamKind

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

ParameterKind

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

SortKind

The different kinds of Z3 types (See Z3_get_sort_kind).

SymbolKind

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

Constants

Z3_L_FALSE

Z3_L_TRUE

Z3_L_UNDEF

Functions

Z3_add_const_interp^⚠

Add a constant interpretation.

Z3_add_func_interp^⚠

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.

Z3_algebraic_eval^⚠

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_get_i^⚠

Return which root of the polynomial the algebraic number represents.

Z3_algebraic_get_poly^⚠

Return the coefficients of the defining polynomial.

Z3_algebraic_gt^⚠

Return true if a > b, and false otherwise.

Z3_algebraic_is_neg^⚠

Return true if a is negative, and false otherwise.

Z3_algebraic_is_pos^⚠

Return true if a is positive, and false otherwise.

Z3_algebraic_is_value^⚠

Return true if a can be used as value in the Z3 real algebraic number package.

Z3_algebraic_is_zero^⚠

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.

Z3_algebraic_power^⚠

Return the a^k

Z3_algebraic_root^⚠

Return the a^(1/k)

Z3_algebraic_roots^⚠

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

Z3_algebraic_sign^⚠

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^⚠

Convert a Z3_app into Z3_ast. This is just type casting.

Z3_append_log^⚠

Append user-defined string to interaction log.

Z3_apply_result_dec_ref^⚠

Decrement the reference counter of the given Z3_apply_result object.

Z3_apply_result_get_num_subgoals^⚠

Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.

Z3_apply_result_get_subgoal^⚠

Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.

Z3_apply_result_inc_ref^⚠

Increment the reference counter of the given Z3_apply_result object.

Z3_apply_result_to_string^⚠

Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.

Z3_ast_map_contains^⚠

Return true if the map m contains the AST key k.

Z3_ast_map_dec_ref^⚠

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.

Z3_ast_map_inc_ref^⚠

Increment the reference counter of the given AST map.

Z3_ast_map_insert^⚠

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.

Z3_ast_map_to_string^⚠

Convert the given map into a string.

Z3_ast_to_string^⚠

Convert the given AST node into a string.

Z3_ast_vector_dec_ref^⚠

Decrement the reference counter of the given AST vector.

Z3_ast_vector_get^⚠

Return the AST at position i in the AST vector v.

Z3_ast_vector_inc_ref^⚠

Increment the reference counter of the given AST vector.

Z3_ast_vector_push^⚠

Add the AST a in the end of the AST vector v. The size of v is increased by one.

Z3_ast_vector_resize^⚠

Resize the AST vector v.

Z3_ast_vector_set^⚠

Update position i of the AST vector v with the AST a.

Z3_ast_vector_size^⚠

Return the size of the given AST vector.

Z3_ast_vector_to_string^⚠

Convert AST vector into a string.

Z3_ast_vector_translate^⚠

Translate the AST vector v from context s into an AST vector in context t.

Z3_benchmark_to_smtlib_string^⚠

Convert the given benchmark into SMT-LIB formatted string.

Z3_close_log^⚠

Close interaction log.

Z3_constructor_num_fields^⚠

Retrieve the number of fields of a constructor

Z3_datatype_update_field^⚠

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.

Z3_del_constructor^⚠

Reclaim memory allocated to constructor.

Z3_del_constructor_list^⚠

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_concurrent_dec_ref^⚠

use concurrency control for dec-ref. Reference counting decrements are allowed in separate threads from the context. If this setting is not invoked, reference counting decrements are not going to be thread safe.

Z3_enable_trace^⚠

Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise

Z3_eval_smtlib2_string^⚠

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.

Z3_finalize_memory^⚠

Destroy all allocated resources.

Z3_fixedpoint_add_callback^⚠

set export callback for lemmas

Z3_fixedpoint_add_constraint^⚠

Z3_fixedpoint_add_cover^⚠

Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forward when possible.

Z3_fixedpoint_add_fact^⚠

Add a Database fact.

Z3_fixedpoint_add_invariant^⚠

Add an invariant for the predicate pred. Add an assumed invariant of predicate pred.

Z3_fixedpoint_add_rule^⚠

Add a universal Horn clause as a named rule. The horn_rule should be of the form:

Z3_fixedpoint_assert^⚠

Assert a constraint to the fixedpoint context.

Z3_fixedpoint_dec_ref^⚠

Decrement the reference counter of the given fixedpoint context.

Z3_fixedpoint_from_file^⚠

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

Z3_fixedpoint_from_string^⚠

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

Z3_fixedpoint_get_answer^⚠

Retrieve a formula that encodes satisfying answers to the query.

Z3_fixedpoint_get_assertions^⚠

Retrieve set of background assertions from fixedpoint context.

Z3_fixedpoint_get_cover_delta^⚠

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.

Z3_fixedpoint_get_ground_sat_answer^⚠

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

Z3_fixedpoint_get_help^⚠

Return a string describing all fixedpoint available parameters.

Z3_fixedpoint_get_num_levels^⚠

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

Z3_fixedpoint_get_param_descrs^⚠

Return the parameter description set for the given fixedpoint object.

Z3_fixedpoint_get_reachable^⚠

Retrieve reachable states of a predicate. Note: this functionality is Spacer specific.

Z3_fixedpoint_get_reason_unknown^⚠

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

Z3_fixedpoint_get_rule_names_along_trace^⚠

Obtain the list of rules along the counterexample trace.

Z3_fixedpoint_get_rules^⚠

Retrieve set of rules from fixedpoint context.

Z3_fixedpoint_get_rules_along_trace^⚠

Obtain the list of rules along the counterexample trace.

Z3_fixedpoint_get_statistics^⚠

Retrieve statistics information from the last call to Z3_fixedpoint_query.

Z3_fixedpoint_inc_ref^⚠

Increment the reference counter of the given fixedpoint context

Z3_fixedpoint_init^⚠

Initialize the context with a user-defined state.

Z3_fixedpoint_query^⚠

Pose a query against the asserted rules.

Z3_fixedpoint_query_from_lvl^⚠

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

Z3_fixedpoint_query_relations^⚠

Pose multiple queries against the asserted rules.

Z3_fixedpoint_register_relation^⚠

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.

Z3_fixedpoint_set_params^⚠

Set parameters on fixedpoint context.

Z3_fixedpoint_set_predicate_representation^⚠

Configure the predicate representation.

Z3_fixedpoint_set_reduce_app_callback^⚠

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

Z3_fixedpoint_set_reduce_assign_callback^⚠

Register a callback to destructive updates.

Z3_fixedpoint_to_string^⚠

Print the current rules and background axioms as a string.

Z3_fixedpoint_update_rule^⚠

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.

Z3_fpa_get_numeral_exponent_bv^⚠

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

Z3_fpa_get_numeral_exponent_int64^⚠

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

Z3_fpa_get_numeral_exponent_string^⚠

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

Z3_fpa_get_numeral_sign^⚠

Retrieves the sign of a floating-point literal.

Z3_fpa_get_numeral_sign_bv^⚠

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

Z3_fpa_get_numeral_significand_bv^⚠

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

Z3_fpa_get_numeral_significand_string^⚠

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

Z3_fpa_get_numeral_significand_uint64^⚠

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.

Z3_fpa_is_numeral^⚠

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

Z3_fpa_is_numeral_inf^⚠

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

Z3_fpa_is_numeral_nan^⚠

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

Z3_fpa_is_numeral_negative^⚠

Checks whether a given floating-point numeral is negative.

Z3_fpa_is_numeral_normal^⚠

Checks whether a given floating-point numeral is normal.

Z3_fpa_is_numeral_positive^⚠

Checks whether a given floating-point numeral is positive.

Z3_fpa_is_numeral_subnormal^⚠

Checks whether a given floating-point numeral is subnormal.

Z3_fpa_is_numeral_zero^⚠

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

Z3_func_decl_to_ast^⚠

Convert a Z3_func_decl into Z3_ast. This is just type casting.

Z3_func_decl_to_string^⚠

Z3_func_entry_dec_ref^⚠

Decrement the reference counter of the given Z3_func_entry object.

Z3_func_entry_get_arg^⚠

Return an argument of a Z3_func_entry object.

Z3_func_entry_get_num_args^⚠

Return the number of arguments in a Z3_func_entry object.

Z3_func_entry_get_value^⚠

Return the value of this point.

Z3_func_entry_inc_ref^⚠

Increment the reference counter of the given Z3_func_entry object.

Z3_func_interp_add_entry^⚠

add a function entry to a function interpretation.

Z3_func_interp_dec_ref^⚠

Decrement the reference counter of the given Z3_func_interp object.

Z3_func_interp_get_arity^⚠

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

Z3_func_interp_get_else^⚠

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

Z3_func_interp_get_entry^⚠

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

Z3_func_interp_get_num_entries^⚠

Return the number of entries in the given function interpretation.

Z3_func_interp_inc_ref^⚠

Increment the reference counter of the given Z3_func_interp object.

Z3_func_interp_set_else^⚠

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

Z3_get_algebraic_number_lower^⚠

Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.

Z3_get_algebraic_number_upper^⚠

Return a upper bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.

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.

Z3_get_app_num_args^⚠

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.

Z3_get_array_arity^⚠

Return the arity (number of dimensions) of the given array sort.

Z3_get_array_sort_domain^⚠

Return the domain of the given array sort. In the case of a multi-dimensional array, this function returns the sort of the first dimension.

Z3_get_array_sort_domain_n^⚠

Return the i’th domain sort of an n-dimensional array.

Z3_get_array_sort_range^⚠

Return the range of the given array sort.

Z3_get_as_array_func_decl^⚠

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

Z3_get_ast_hash^⚠

Return a hash code for the given AST. The hash code is structural but two different AST objects can map to the same hash. The result of Z3_get_ast_id returns an identifier that is unique over the set of live AST objects.

Z3_get_ast_id^⚠

Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.

Z3_get_ast_kind^⚠

Return the kind of the given AST.

Z3_get_bool_value^⚠

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

Z3_get_bv_sort_size^⚠

Return the size of the given bit-vector sort.

Z3_get_datatype_sort_constructor^⚠

Return idx’th constructor.

Z3_get_datatype_sort_constructor_accessor^⚠

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

Z3_get_datatype_sort_num_constructors^⚠

Return number of constructors for datatype.

Z3_get_datatype_sort_recognizer^⚠

Return idx’th recognizer.

Z3_get_decl_ast_parameter^⚠

Return the expression value associated with an expression parameter.

Z3_get_decl_double_parameter^⚠

Return the double value associated with an double parameter.

Z3_get_decl_func_decl_parameter^⚠

Return the expression value associated with an expression parameter.

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

Z3_get_decl_num_parameters^⚠

Return the number of parameters associated with a declaration.

Z3_get_decl_parameter_kind^⚠

Return the parameter type associated with a declaration.

Z3_get_decl_rational_parameter^⚠

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

Z3_get_decl_sort_parameter^⚠

Return the sort value associated with a sort parameter.

Z3_get_decl_symbol_parameter^⚠

Return the double value associated with an double parameter.

Z3_get_denominator^⚠

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

Z3_get_depth^⚠

Z3_get_domain^⚠

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

Z3_get_domain_size^⚠

Return the number of parameters of the given declaration.

Z3_get_error_code^⚠

Return the error code for the last API call.

Z3_get_error_msg^⚠

Return a string describing the given error code.

Z3_get_estimated_alloc_size^⚠

Return the estimated allocated memory in bytes.

Z3_get_finite_domain_sort_size^⚠

Store the size of the sort in r. Return false if the call failed. That is, Z3_get_sort_kind(s) == Z3_FINITE_DOMAIN_SORT

Z3_get_full_version^⚠

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

Z3_get_func_decl_id^⚠

Return a unique identifier for f.

Z3_get_global_param_descrs^⚠

Retrieve description of global parameters.

Z3_get_implied_equalities^⚠

Retrieve congruence class representatives for terms.

Z3_get_index_value^⚠

Return index of de-Bruijn bound variable.

Z3_get_lstring^⚠

Retrieve the string constant stored in s. The string can contain escape sequences. Characters in the range 1 to 255 are literal. Characters in the range 0, and 256 above are escaped.

Z3_get_num_probes^⚠

Return the number of builtin probes available in Z3.

Z3_get_num_simplifiers^⚠

Return the number of builtin simplifiers available in Z3.

Z3_get_num_tactics^⚠

Return the number of builtin tactics available in Z3.

Z3_get_numeral_binary_string^⚠

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

Z3_get_numeral_decimal_string^⚠

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

Z3_get_numeral_double^⚠

Return numeral as a double.

Z3_get_numeral_int^⚠

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int. Return true if the call succeeded.

Z3_get_numeral_int64^⚠

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.

Z3_get_numeral_rational_int64^⚠

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.

Z3_get_numeral_small^⚠

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

Z3_get_numeral_string^⚠

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

Z3_get_numeral_uint^⚠

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.

Z3_get_numeral_uint64^⚠

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.

Z3_get_pattern_num_terms^⚠

Return number of terms in pattern.

Z3_get_probe_name^⚠

Return the name of the i probe.

Z3_get_quantifier_body^⚠

Return body of quantifier.

Z3_get_quantifier_bound_name^⚠

Return symbol of the i’th bound variable.

Z3_get_quantifier_bound_sort^⚠

Return sort of the i’th bound variable.

Z3_get_quantifier_id^⚠

Obtain id of quantifier.

Z3_get_quantifier_no_pattern_ast^⚠

Return i’th no_pattern.

Z3_get_quantifier_num_bound^⚠

Return number of bound variables of quantifier.

Z3_get_quantifier_num_no_patterns^⚠

Return number of no_patterns used in quantifier.

Z3_get_quantifier_num_patterns^⚠

Return number of patterns used in quantifier.

Z3_get_quantifier_pattern_ast^⚠

Return i’th pattern.

Z3_get_quantifier_skolem_id^⚠

Obtain skolem id of quantifier.

Z3_get_quantifier_weight^⚠

Obtain weight of quantifier.

Z3_get_range^⚠

Return the range of the given declaration.

Z3_get_re_sort_basis^⚠

Retrieve basis sort for regex sort.

Z3_get_relation_arity^⚠

Return arity of relation.

Z3_get_relation_column^⚠

Return sort at i’th column of relation sort.

Z3_get_seq_sort_basis^⚠

Retrieve basis sort for sequence sort.

Z3_get_simplifier_name^⚠

Return the name of the idx simplifier.

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. Characters outside the basic printable ASCII range are escaped.

Z3_get_string_contents^⚠

Retrieve the unescaped string constant stored in s.

Z3_get_string_length^⚠

Retrieve the length of the unescaped string constant stored in s.

Z3_get_symbol_int^⚠

Return the symbol int value.

Z3_get_symbol_kind^⚠

Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if the symbol was constructed using Z3_mk_string_symbol.

Z3_get_symbol_string^⚠

Return the symbol name.

Z3_get_tactic_name^⚠

Return the name of the idx tactic.

Z3_get_tuple_sort_field_decl^⚠

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

Z3_get_tuple_sort_mk_decl^⚠

Return the constructor declaration of the given tuple sort.

Z3_get_tuple_sort_num_fields^⚠

Return the number of fields of the given tuple sort.

Z3_get_version^⚠

Return Z3 version number information.

Z3_global_param_get^⚠

Get a global (or module) parameter.

Z3_global_param_reset_all^⚠

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

Z3_global_param_set^⚠

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

Z3_goal_convert_model^⚠

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.

Z3_goal_inconsistent^⚠

Return true if the given goal contains the formula false.

Z3_goal_is_decided_sat^⚠

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

Z3_goal_is_decided_unsat^⚠

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

Z3_goal_num_exprs^⚠

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

Z3_goal_precision^⚠

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.

Z3_goal_to_dimacs_string^⚠

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 if the caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.

Z3_goal_to_string^⚠

Convert a goal into a string.

Z3_goal_translate^⚠

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. This procedure can be used to interrupt: solvers, simplifiers and tactics.

Z3_is_algebraic_number^⚠

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. It is the array such that forall indices i we have that (select (_ as-array f) i) is equal to (f i). This procedure returns true if the a is an as-array AST node.

Z3_is_char_sort^⚠

Check if s is a character sort.

Z3_is_eq_ast^⚠

Compare terms.

Z3_is_eq_func_decl^⚠

Compare terms.

Z3_is_eq_sort^⚠

compare sorts.

Z3_is_ground^⚠

Z3_is_lambda^⚠

Determine if ast is a lambda expression.

Z3_is_numeral_ast^⚠

Z3_is_quantifier_exists^⚠

Determine if ast is an existential quantifier.

Z3_is_quantifier_forall^⚠

Determine if an ast is a universal quantifier.

Z3_is_re_sort^⚠

Check if s is a regular expression sort.

Z3_is_recursive_datatype_sort^⚠

Check if s is a recursive datatype sort.

Z3_is_seq_sort^⚠

Check if s is a sequence sort.

Z3_is_string^⚠

Determine if s is a string constant.

Z3_is_string_sort^⚠

Check if s is a string sort.

Z3_is_well_sorted^⚠

Return true if the given expression t is well sorted.

Z3_mk_abs^⚠

Take the absolute value of an integer

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.

Z3_mk_array_default^⚠

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.

Z3_mk_array_sort_n^⚠

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_bit2bool^⚠

Extracts the bit at position i of a bit-vector and yields a boolean.

Z3_mk_bool_sort^⚠

Create the Boolean type.

Z3_mk_bound^⚠

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

Z3_mk_bvadd_no_overflow^⚠

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

Z3_mk_bvadd_no_underflow^⚠

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.

Z3_mk_bvmul_no_overflow^⚠

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

Z3_mk_bvmul_no_underflow^⚠

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.

Z3_mk_bvneg_no_overflow^⚠

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.

Z3_mk_bvsdiv_no_overflow^⚠

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.

Z3_mk_bvsub_no_overflow^⚠

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

Z3_mk_bvsub_no_underflow^⚠

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_char^⚠

Create a character literal

Z3_mk_char_from_bv^⚠

Create a character from a bit-vector (code point).

Z3_mk_char_is_digit^⚠

Create a check if the character is a digit.

Z3_mk_char_le^⚠

Create less than or equal to between two characters.

Z3_mk_char_sort^⚠

Create a sort for unicode characters.

Z3_mk_char_to_bv^⚠

Create a bit-vector (code point) from character.

Z3_mk_char_to_int^⚠

Create an integer (code point) from character.

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.

Z3_mk_const_array^⚠

Create the constant array.

Z3_mk_constructor^⚠

Create a constructor.

Z3_mk_constructor_list^⚠

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_datatype_sort^⚠

create a forward reference to a recursive datatype being declared. The forward reference can be used in a nested occurrence: the range of an array or as element sort of a sequence. The forward reference should only be used when used in an accessor for a recursive datatype that gets declared.

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_divides^⚠

Create division predicate.

Z3_mk_empty_set^⚠

Create the empty set.

Z3_mk_enumeration_sort^⚠

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.

Z3_mk_exists_const^⚠

Similar to Z3_mk_forall_const.

Z3_mk_ext_rotate_left^⚠

Rotate bits of t1 to the left t2 times.

Z3_mk_ext_rotate_right^⚠

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.

Z3_mk_finite_domain_sort^⚠

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.

Z3_mk_forall_const^⚠

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.

Z3_mk_fpa_is_infinite^⚠

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.

Z3_mk_fpa_is_negative^⚠

Predicate indicating whether t is a negative floating-point number.

Z3_mk_fpa_is_normal^⚠

Predicate indicating whether t is a normal floating-point number.

Z3_mk_fpa_is_positive^⚠

Predicate indicating whether t is a positive floating-point number.

Z3_mk_fpa_is_subnormal^⚠

Predicate indicating whether t is a subnormal floating-point number.

Z3_mk_fpa_is_zero^⚠

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

Z3_mk_fpa_numeral_double^⚠

Create a numeral of FloatingPoint sort from a double.

Z3_mk_fpa_numeral_float^⚠

Create a numeral of FloatingPoint sort from a float.

Z3_mk_fpa_numeral_int^⚠

Create a numeral of FloatingPoint sort from a signed integer.

Z3_mk_fpa_numeral_int64_uint64^⚠

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

Z3_mk_fpa_numeral_int_uint^⚠

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.

Z3_mk_fpa_round_nearest_ties_to_away^⚠

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

Z3_mk_fpa_round_nearest_ties_to_even^⚠

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

Z3_mk_fpa_round_to_integral^⚠

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

Z3_mk_fpa_round_toward_negative^⚠

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

Z3_mk_fpa_round_toward_positive^⚠

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

Z3_mk_fpa_round_toward_zero^⚠

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

Z3_mk_fpa_rounding_mode_sort^⚠

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.

Z3_mk_fpa_sort_16^⚠

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

Z3_mk_fpa_sort_32^⚠

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

Z3_mk_fpa_sort_64^⚠

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

Z3_mk_fpa_sort_128^⚠

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

Z3_mk_fpa_sort_double^⚠

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

Z3_mk_fpa_sort_half^⚠

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

Z3_mk_fpa_sort_quadruple^⚠

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

Z3_mk_fpa_sort_single^⚠

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

Z3_mk_fpa_sqrt^⚠

Floating-point square root

Z3_mk_fpa_sub^⚠

Floating-point subtraction

Z3_mk_fpa_to_fp_bv^⚠

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

Z3_mk_fpa_to_fp_float^⚠

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

Z3_mk_fpa_to_fp_int_real^⚠

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

Z3_mk_fpa_to_fp_real^⚠

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

Z3_mk_fpa_to_fp_signed^⚠

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

Z3_mk_fpa_to_fp_unsigned^⚠

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

Z3_mk_fpa_to_ieee_bv^⚠

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

Z3_mk_fpa_to_real^⚠

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.

Z3_mk_fresh_const^⚠

Declare and create a fresh constant.

Z3_mk_fresh_func_decl^⚠

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. 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. The sort of the resulting expression is (Array sorts range) where range is the sort of body. For example, if the lambda binds two variables of sort Int and Bool, and the body has sort Real, the sort of the expression is (Array Int Bool Real).

Z3_mk_lambda_const^⚠

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_linear_order^⚠

create a linear ordering relation over signature a. The relation is identified by the index id.

Z3_mk_list_sort^⚠

Create a list sort

Z3_mk_lstring^⚠

Create a string constant out of the string that is passed in It takes the length of the string as well to take into account 0 characters. The string is treated as if it is unescaped so a sequence of characters \u{0} is treated as 5 characters and not the character 0.

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_parser_context^⚠

Create a parser context.

Z3_mk_partial_order^⚠

create a partial ordering relation over signature a and index id.

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_piecewise_linear_order^⚠

create a piecewise linear ordering relation over signature a and index id.

Z3_mk_polymorphic_datatype^⚠

Create a parametric datatype with explicit type parameters.

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.

Z3_mk_quantifier_const^⚠

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

Z3_mk_quantifier_const_ex^⚠

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

Z3_mk_quantifier_ex^⚠

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

Z3_mk_re_allchar^⚠

Create a regular expression that accepts all singleton sequences of the regular expression sort

Z3_mk_re_complement^⚠

Create the complement of the regular language re.

Z3_mk_re_concat^⚠

Create the concatenation of the regular languages.

Z3_mk_re_diff^⚠

Create the difference of regular expressions.

Z3_mk_re_empty^⚠

Create an empty regular expression of sort re.

Z3_mk_re_full^⚠

Create an universal regular expression of sort re.

Z3_mk_re_intersect^⚠

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 exception: 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_power^⚠

Create a power regular expression.

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_int64^⚠

Create a real from a fraction of int64.

Z3_mk_real_sort^⚠

Create the real type.

Z3_mk_rec_func_decl^⚠

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.

Z3_mk_rotate_left^⚠

Rotate bits of t1 to the left i times.

Z3_mk_rotate_right^⚠

Rotate bits of t1 to the right i times.

Z3_mk_sbv_to_str^⚠

Signed bit-vector to string conversion.

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. The sequence is empty if the index is out of bounds.

Z3_mk_seq_concat^⚠

Concatenate sequences.

Z3_mk_seq_contains^⚠

Check if container contains containee.

Z3_mk_seq_empty^⚠

Create an empty sequence of the sequence sort seq.

Z3_mk_seq_extract^⚠

Extract subsequence starting at offset of length.

Z3_mk_seq_foldl^⚠

Create a fold of the function f over the sequence s with accumulator a.

Z3_mk_seq_foldli^⚠

Create a fold with index tracking of the function f over the sequence s with accumulator a starting at index i.

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 the 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 value is -1 if offset is negative or larger than the length of s.

Z3_mk_seq_last_index^⚠

Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -1,

Z3_mk_seq_length^⚠

Return the length of the sequence s.

Z3_mk_seq_map^⚠

Create a map of the function f over the sequence s.

Z3_mk_seq_mapi^⚠

Create a map of the function f over the sequence s starting at index i.

Z3_mk_seq_nth^⚠

Retrieve from s the element positioned at position index. The function is under-specified if the index is out of bounds.

Z3_mk_seq_prefix^⚠

Check if prefix is a prefix of s.

Z3_mk_seq_replace^⚠

Replace the first occurrence of src with dst in s.

Z3_mk_seq_replace_all^⚠

Replace all occurrences of src with dst in s.

Z3_mk_seq_replace_re^⚠

Replace the first occurrence of regular expression re with dst in s.

Z3_mk_seq_replace_re_all^⚠

Replace all occurrences of regular expression re 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.

Z3_mk_set_complement^⚠

Take the complement of a set.

Z3_mk_set_del^⚠

Remove an element to a set.

Z3_mk_set_difference^⚠

Take the set difference between two sets.

Z3_mk_set_intersect^⚠

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.

Z3_mk_simple_solver^⚠

Create a new incremental solver.

Z3_mk_simplifier^⚠

Return a simplifier associated with the given name. The complete list of simplifiers may be obtained using the procedures Z3_get_num_simplifiers and Z3_get_simplifier_name. It may also be obtained using the command (help-simplifier) in the SMT 2.0 front-end.

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.

Z3_mk_solver_for_logic^⚠

Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unknown or unsupported.

Z3_mk_solver_from_tactic^⚠

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_le^⚠

Check if s1 is equal or lexicographically strictly less than s2.

Z3_mk_str_lt^⚠

Check if s1 is lexicographically strictly less than s2.

Z3_mk_str_to_int^⚠

Convert string to integer.

Z3_mk_string^⚠

Create a string constant out of the string that is passed in The string may contain escape encoding for non-printable characters or characters outside of the basic printable ASCII range. For example, the escape encoding \u{0} represents the character 0 and the encoding \u{100} represents the character 256.

Z3_mk_string_from_code^⚠

Code to string conversion.

Z3_mk_string_sort^⚠

Create a sort for unicode strings.

Z3_mk_string_symbol^⚠

Create a Z3 symbol using a C string.

Z3_mk_string_to_code^⚠

String to code conversion.

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. The complete list of tactics may be obtained using the procedures Z3_get_num_tactics and Z3_get_tactic_name. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end.

Z3_mk_transitive_closure^⚠

create transitive closure of binary relation.

Z3_mk_tree_order^⚠

create a tree ordering relation over signature a identified using index id.

Z3_mk_true^⚠

Create an AST node representing true.

Z3_mk_tuple_sort^⚠

Create a tuple type.

Z3_mk_type_variable^⚠

Create a type variable.

Z3_mk_u32string^⚠

Create a string constant out of the string that is passed in It takes the length of the string as well to take into account 0 characters. The string is unescaped.

Z3_mk_ubv_to_str^⚠

Unsigned bit-vector to string conversion.

Z3_mk_unary_minus^⚠

Create an AST node representing - arg.

Z3_mk_uninterpreted_sort^⚠

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

Z3_mk_unsigned_int^⚠

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

Z3_mk_unsigned_int64^⚠

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.

Z3_model_extrapolate^⚠

Extrapolates a model of a formula

Z3_model_get_const_decl^⚠

Return the i-th constant in the given model.

Z3_model_get_const_interp^⚠

Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL, if the model does not assign an interpretation for a. That should be interpreted as: the value of a does not matter.

Z3_model_get_func_decl^⚠

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

Z3_model_get_func_interp^⚠

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

Z3_model_get_num_consts^⚠

Return the number of constants assigned by the given model.

Z3_model_get_num_funcs^⚠

Return the number of function interpretations in the given model.

Z3_model_get_num_sorts^⚠

Return the number of uninterpreted sorts that m assigns an interpretation to.

Z3_model_get_sort^⚠

Return a uninterpreted sort that m assigns an interpretation.

Z3_model_get_sort_universe^⚠

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

Z3_model_has_interp^⚠

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.

Z3_model_to_string^⚠

Convert the given model into a string.

Z3_model_translate^⚠

translate model from context c to context dst.

Z3_open_log^⚠

Log interaction to a file.

Z3_optimize_assert^⚠

Assert hard constraint to the optimization context.

Z3_optimize_assert_and_track^⚠

Assert tracked hard constraint to the optimization context.

Z3_optimize_assert_soft^⚠

Assert soft constraint to the optimization context.

Z3_optimize_check^⚠

Check consistency and produce optimal values.

Z3_optimize_dec_ref^⚠

Decrement the reference counter of the given optimize context.

Z3_optimize_from_file^⚠

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

Z3_optimize_from_string^⚠

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

Z3_optimize_get_assertions^⚠

Return the set of asserted formulas on the optimization context.

Z3_optimize_get_help^⚠

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

Z3_optimize_get_lower^⚠

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

Z3_optimize_get_lower_as_vector^⚠

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.

Z3_optimize_get_model^⚠

Retrieve the model for the last Z3_optimize_check

Z3_optimize_get_objectives^⚠

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.

Z3_optimize_get_param_descrs^⚠

Return the parameter description set for the given optimize object.

Z3_optimize_get_reason_unknown^⚠

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

Z3_optimize_get_statistics^⚠

Retrieve statistics information from the last call to Z3_optimize_check

Z3_optimize_get_unsat_core^⚠

Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions a.

Z3_optimize_get_upper^⚠

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

Z3_optimize_get_upper_as_vector^⚠

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

Z3_optimize_inc_ref^⚠

Increment the reference counter of the given optimize context

Z3_optimize_maximize^⚠

Add a maximization constraint.

Z3_optimize_minimize^⚠

Add a minimization constraint.

Z3_optimize_pop^⚠

Backtrack one level.

Z3_optimize_push^⚠

Create a backtracking point.

Z3_optimize_register_model_eh^⚠

register a model event handler for new models.

Z3_optimize_set_initial_value^⚠

provide an initialization hint to the solver. The initialization hint is used to calibrate an initial value of the expression that represents a variable. If the variable is Boolean, the initial phase is set according to value. If the variable is an integer or real, the initial Simplex tableau is recalibrated to attempt to follow the value assignment.

Z3_optimize_set_params^⚠

Set parameters on optimization context.

Z3_optimize_to_string^⚠

Print the current context as a string.

Z3_optimize_translate^⚠

Copy an optimization context from a source to a target context.

Z3_param_descrs_dec_ref^⚠

Decrement the reference counter of the given parameter description set.

Z3_param_descrs_get_documentation^⚠

Retrieve documentation string corresponding to parameter name s.

Z3_param_descrs_get_kind^⚠

Return the kind associated with the given parameter name n.

Z3_param_descrs_get_name^⚠

Return the name of the parameter at given index i.

Z3_param_descrs_inc_ref^⚠

Increment the reference counter of the given parameter description set.

Z3_param_descrs_size^⚠

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

Z3_param_descrs_to_string^⚠

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

Z3_params_dec_ref^⚠

Decrement the reference counter of the given parameter set.

Z3_params_inc_ref^⚠

Increment the reference counter of the given parameter set.

Z3_params_set_bool^⚠

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

Z3_params_set_double^⚠

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

Z3_params_set_symbol^⚠

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

Z3_params_set_uint^⚠

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

Z3_params_to_string^⚠

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

Z3_params_validate^⚠

Validate the parameter set p against the parameter description set d.

Z3_parse_smtlib2_file^⚠

Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.

Z3_parse_smtlib2_string^⚠

Parse the given string using the SMT-LIB2 parser.

Z3_parser_context_add_decl^⚠

Add a function declaration.

Z3_parser_context_add_sort^⚠

Add a sort declaration.

Z3_parser_context_dec_ref^⚠

Decrement the reference counter of the given Z3_parser_context object.

Z3_parser_context_from_string^⚠

Parse a string of SMTLIB2 commands. Return assertions.

Z3_parser_context_inc_ref^⚠

Increment the reference counter of the given Z3_parser_context object.

Z3_pattern_to_ast^⚠

Convert a Z3_pattern into Z3_ast. This is just type casting.

Z3_pattern_to_string^⚠

Z3_polynomial_subresultants^⚠

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.

Z3_probe_get_descr^⚠

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

Z3_qe_model_project^⚠

Project variables given a model

Z3_qe_model_project_skolem^⚠

Project variables given a model

Z3_qe_model_project_with_witness^⚠

Project with witness extraction.

Z3_query_constructor^⚠

Query constructor for declared functions.

Z3_rcf_add^⚠

Return the value a + b.

Z3_rcf_coefficient^⚠

Extract a coefficient from an algebraic number.

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_extension_index^⚠

Return the index of a field extension.

Z3_rcf_ge^⚠

Return true if a >= b.

Z3_rcf_get_numerator_denominator^⚠

Extract the “numerator” and “denominator” of the given RCF numeral. We have that a = n/d, moreover n and d are not represented using rational functions.

Z3_rcf_gt^⚠

Return true if a > b.

Z3_rcf_infinitesimal_name^⚠

Return the name of an infinitesimal.

Z3_rcf_interval^⚠

Extract an interval from an algebraic number.

Z3_rcf_inv^⚠

Return the value 1/a.

Z3_rcf_is_algebraic^⚠

Return true if a represents an algebraic number.

Z3_rcf_is_infinitesimal^⚠

Return true if a represents an infinitesimal.

Z3_rcf_is_rational^⚠

Return true if a represents a rational number.

Z3_rcf_is_transcendental^⚠

Return true if a represents a transcendental number.

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)

Z3_rcf_mk_infinitesimal^⚠

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

Z3_rcf_mk_pi^⚠

Return Pi

Z3_rcf_mk_rational^⚠

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.

Z3_rcf_mk_small_int^⚠

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.

Z3_rcf_num_coefficients^⚠

Return the number of coefficients in an algebraic number.

Z3_rcf_num_sign_condition_coefficients^⚠

Return the number of sign condition polynomial coefficients of an algebraic number.

Z3_rcf_num_sign_conditions^⚠

Return the number of sign conditions of an algebraic number.

Z3_rcf_num_to_decimal_string^⚠

Convert the RCF numeral into a string in decimal notation.

Z3_rcf_num_to_string^⚠

Convert the RCF numeral into a string.

Z3_rcf_power^⚠

Return the value a^k.

Z3_rcf_sign_condition_coefficient^⚠

Extract the j-th polynomial coefficient of the i-th sign condition.

Z3_rcf_sign_condition_sign^⚠

Extract the sign of a sign condition from an algebraic number.

Z3_rcf_sub^⚠

Return the value a - b.

Z3_rcf_transcendental_name^⚠

Return the name of a transcendental.

Z3_reset_memory^⚠

Reset all allocated resources.

Z3_set_ast_print_mode^⚠

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

Z3_set_error^⚠

Set an error.

Z3_set_error_handler^⚠

Register a Z3 error handler.

Z3_set_param_value^⚠

Set a configuration parameter.

Z3_simplifier_and_then^⚠

Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1.

Z3_simplifier_dec_ref^⚠

Decrement the reference counter of the given simplifier.

Z3_simplifier_get_descr^⚠

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

Z3_simplifier_get_help^⚠

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

Z3_simplifier_get_param_descrs^⚠

Return the parameter description set for the given simplifier object.

Z3_simplifier_inc_ref^⚠

Increment the reference counter of the given simplifier.

Z3_simplifier_using_params^⚠

Return a simplifier that applies t using the given set of parameters.

Z3_simplify^⚠

Interface to simplifier.

Z3_simplify_ex^⚠

Interface to simplifier.

Z3_simplify_get_help^⚠

Return a string describing all available parameters.

Z3_simplify_get_param_descrs^⚠

Return the parameter description set for the simplify procedure.

Z3_solver_add_simplifier^⚠

Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing.

Z3_solver_assert^⚠

Assert a constraint into the solver.

Z3_solver_assert_and_track^⚠

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.

Z3_solver_check_assumptions^⚠

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

Z3_solver_congruence_explain^⚠

retrieve explanation for congruence.

Z3_solver_congruence_next^⚠

retrieve the next expression in the congruence class. The set of congruent siblings form a cyclic list. Repeated calls on the siblings will result in returning to the original expression.

Z3_solver_congruence_root^⚠

retrieve the congruence closure root of an expression. The root is retrieved relative to the state where the solver was in when it completed. If it completed during a set of case splits, the congruence roots are relative to these case splits. That is, the congruences are not consequences but they are true under the current state.

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.

Z3_solver_dec_ref^⚠

Decrement the reference counter of the given solver.

Z3_solver_from_file^⚠

load solver assertions from a file.

Z3_solver_from_string^⚠

load solver assertions from a string.

Z3_solver_get_assertions^⚠

Return the set of asserted formulas on the solver.

Z3_solver_get_consequences^⚠

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

Z3_solver_get_help^⚠

Return a string describing all solver available parameters.

Z3_solver_get_levels^⚠

retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat call and no other calls (to extract models) have been invoked.

Z3_solver_get_model^⚠

Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions

Z3_solver_get_non_units^⚠

Return the set of non units in the solver state.

Z3_solver_get_num_scopes^⚠

Return the number of backtracking points.

Z3_solver_get_param_descrs^⚠

Return the parameter description set for the given solver object.

Z3_solver_get_proof^⚠

Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions

Z3_solver_get_reason_unknown^⚠

Return a brief justification for an “unknown” result (i.e., Z3_L_UNDEF) for the commands Z3_solver_check and Z3_solver_check_assumptions

Z3_solver_get_statistics^⚠

Return statistics for the given solver.

Z3_solver_get_trail^⚠

Return the trail modulo model conversion, in order of decision level The decision level can be retrieved using Z3_solver_get_level based on the trail.

Z3_solver_get_units^⚠

Return the set of units modulo model conversion.

Z3_solver_get_unsat_core^⚠

Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the assumptions a.

Z3_solver_import_model_converter^⚠

Ad-hoc method for importing model conversion from solver.

Z3_solver_inc_ref^⚠

Increment the reference counter of the given solver.

Z3_solver_interrupt^⚠

Solver local interrupt. Normally you should use Z3_interrupt to cancel solvers because only one solver is enabled concurrently per context. However, per GitHub issue #1006, there are use cases where it is more convenient to cancel a specific solver. Solvers that are not selected for interrupts are left alone.

Z3_solver_next_split^⚠

Sets the next (registered) expression to split on. The function returns false and ignores the given expression in case the expression is already assigned internally (due to relevancy propagation, this assignments might not have been reported yet by the fixed callback). In case the function is called in the decide callback, it overrides the currently selected variable and phase.

Z3_solver_pop^⚠

Backtrack n backtracking points.

Z3_solver_propagate_consequence^⚠

propagate a consequence based on fixed values and equalities. A client may invoke it during the propagate_fixed, propagate_eq, propagate_diseq, and propagate_final callbacks. The callback adds a propagation consequence based on the fixed values passed ids and equalities eqs based on parameters lhs, rhs.

Z3_solver_propagate_created^⚠

register a callback when a new expression with a registered function is used by the solver The registered function appears at the top level and is created using \ref Z3_solver_propagate_declare.

Z3_solver_propagate_decide^⚠

register a callback when the solver decides to split on a registered expression. The callback may change the arguments by providing other values by calling \ref Z3_solver_next_split

Z3_solver_propagate_declare^⚠

Create uninterpreted function declaration for the user propagator. When expressions using the function are created by the solver invoke a callback to \ref Z3_solver_propagate_created with arguments

Z3_solver_propagate_diseq^⚠

register a callback on expression dis-equalities.

Z3_solver_propagate_eq^⚠

register a callback on expression equalities.

Z3_solver_propagate_final^⚠

register a callback on final check. This provides freedom to the propagator to delay actions or implement a branch-and bound solver. The final check is invoked when all decision variables have been assigned by the solver.

Z3_solver_propagate_fixed^⚠

register a callback for when an expression is bound to a fixed value. The supported expression types are

Z3_solver_propagate_init^⚠

register a user-propagator with the solver.

Z3_solver_propagate_on_binding^⚠

register a callback when the solver instantiates a quantifier. If the callback returns false, the actual instantiation of the quantifier is blocked. This allows the user propagator selectively prioritize instantiations without relying on default or configured weights.

Z3_solver_propagate_register^⚠

register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Vector can be registered for propagation.

Z3_solver_propagate_register_cb^⚠

register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Vector can be registered for propagation. Unlike \ref Z3_solver_propagate_register, this function takes a solver callback context as argument. It can be invoked during a callback to register new expressions.

Z3_solver_push^⚠

Create a backtracking point.

Z3_solver_register_on_clause^⚠

register a callback to that retrieves assumed, inferred and deleted clauses during search.

Z3_solver_reset^⚠

Remove all assertions from the solver.

Z3_solver_set_initial_value^⚠

provide an initialization hint to the solver. The initialization hint is used to calibrate an initial value of the expression that represents a variable. If the variable is Boolean, the initial phase is set according to value. If the variable is an integer or real, the initial Simplex tableau is recalibrated to attempt to follow the value assignment.

Z3_solver_set_params^⚠

Set the given solver using the given parameters.

Z3_solver_solve_for^⚠

retrieve a ‘solution’ for variables as defined by equalities in maintained by solvers. At this point, only linear solution are supported. The solution to variables may be presented in triangular form, such that variables used in solutions themselves have solutions.

Z3_solver_to_dimacs_string^⚠

Convert a solver into a DIMACS formatted string.

Z3_solver_to_string^⚠

Convert a solver into a string.

Z3_solver_translate^⚠

Copy a solver s from the context source to the context target.

Z3_sort_to_ast^⚠

Convert a Z3_sort into Z3_ast. This is just type casting.

Z3_sort_to_string^⚠

Z3_stats_dec_ref^⚠

Decrement the reference counter of the given statistics object.

Z3_stats_get_double_value^⚠

Return the double value of the given statistical data.

Z3_stats_get_key^⚠

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

Z3_stats_get_uint_value^⚠

Return the unsigned value of the given statistical data.

Z3_stats_inc_ref^⚠

Increment the reference counter of the given statistics object.

Z3_stats_is_double^⚠

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.

Z3_stats_to_string^⚠

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. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].

Z3_substitute_funs^⚠

Substitute functions in from with new expressions in to.

Z3_substitute_vars^⚠

Substitute the variables in a with the expressions in to. For every i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term to[i]. Note that a variable is created using the function \ref Z3_mk_bound.

Z3_tactic_and_then^⚠

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.

Z3_tactic_apply_ex^⚠

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.

Z3_tactic_dec_ref^⚠

Decrement the reference counter of the given tactic.

Z3_tactic_fail^⚠

Return a tactic that always fails.

Z3_tactic_fail_if^⚠

Return a tactic that fails if the probe p evaluates to false.

Z3_tactic_fail_if_not_decided^⚠

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

Z3_tactic_get_descr^⚠

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

Z3_tactic_get_help^⚠

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

Z3_tactic_get_param_descrs^⚠

Return the parameter description set for the given tactic object.

Z3_tactic_inc_ref^⚠

Increment the reference counter of the given tactic.

Z3_tactic_or_else^⚠

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.

Z3_tactic_par_and_then^⚠

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.

Z3_tactic_try_for^⚠

Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms milliseconds, then it fails.

Z3_tactic_using_params^⚠

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 APP_AST. This is just type casting.

Z3_to_func_decl^⚠

Convert an AST into a FUNC_DECL_AST. This is just type casting.

Z3_toggle_warning_messages^⚠

Enable/disable printing warning messages to the console.

Z3_translate^⚠

Translate/Copy the AST a from context source to context target. AST a must have been created using context source.

Z3_update_param_value^⚠

Set a value of a context parameter.

Z3_update_term^⚠

Update the arguments of term a using the arguments args. The number of arguments num_args should coincide with the number of arguments to a. If a is a quantifier, then num_args has to be 1.

Type Aliases

Z3_app

Kind of AST used to represent function applications.

Z3_apply_result

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

Z3_ast

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

Z3_ast_kind

Z3_ast_map

Mapping from Z3_ast to Z3_ast objects.

Z3_ast_print_mode

Z3_ast_vector

Vector of Z3_ast objects.

Z3_char_ptr

Pointer to a C string (same underlying type as Z3_string but used as output).

Z3_config

Configuration object used to initialize logical contexts.

Z3_constructor

Type constructor for a (recursive) datatype.

Z3_constructor_list

List of constructors for a (recursive) datatype.

Z3_context

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

Z3_created_eh

Callback invoked when a new term is created during solver propagation.

Z3_decide_eh

Callback invoked when the solver makes a decision during propagation.

Z3_decl_kind

Z3_eq_eh

Callback invoked when two terms are equated during solver propagation.

Z3_error_code

Z3_error_handler

Z3 custom error handler (See crate::Z3_set_error_handler).

Z3_final_eh

Callback invoked when all remaining assignments are final during solver propagation.

Z3_fixed_eh

Callback invoked when a variable is fixed during solver propagation.

Z3_fixedpoint

Context for the recursive predicate solver.

Z3_fixedpoint_new_lemma_eh

Z3_fixedpoint_predecessor_eh

Z3_fixedpoint_reduce_app_callback_fptr

Z3_fixedpoint_reduce_assign_callback_fptr

The following utilities allows adding user-defined domains.

Z3_fixedpoint_unfold_eh

Z3_fresh_eh

Callback invoked to create a fresh user context for a new solver thread.

Z3_func_decl

Kind of AST used to represent function symbols.

Z3_func_entry

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

Z3_func_interp

Interpretation of a function in a model.

Z3_goal

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

Z3_goal_prec

Z3_lbool

Lifted Boolean type: false, undefined, true.

Z3_literals

Z3_model

Model for the constraints inserted into the logical context.

Z3_model_eh

Callback invoked when an optimization model is found.

Z3_on_binding_eh

Callback invoked on binding during solver propagation; returns whether to keep the binding.

Z3_on_clause_eh

Callback invoked when a clause is learned by the solver.

Z3_optimize

Context for solving optimization queries.

Z3_param_descrs

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

Z3_param_kind

Z3_parameter_kind

Z3_params

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

Z3_parser_context

Context for incrementally parsing SMTLIB2 strings.

Z3_pattern

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

Z3_pop_eh

Callback invoked when scopes are popped during solver propagation.

Z3_probe

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.

Z3_push_eh

Callback invoked when a new scope is pushed during solver propagation.

Z3_rcf_num

Z3_simplifier

Simplifier object.

Z3_solver

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

Z3_solver_callback

Callback object for user-defined solver propagation.

Z3_sort

Kind of AST used to represent types.

Z3_sort_kind

Z3_stats

Statistical data for a solver.

Z3_string

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

Z3_string_ptr

Z3_symbol

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

Z3_symbol_kind

Z3_tactic

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