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.

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

• 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
  Precision of a given goal. Some goals can be transformed using over/under 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.
• 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_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_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_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 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.
• 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_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^⚠
  Convert the given func decl AST node into a 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^⚠
  Set the ‘else’ value of the given function interpretation.
• Z3_get_algebraic_number_lower^⚠
  Return a lower bound for the given real algebraic number.
• Z3_get_algebraic_number_upper^⚠
  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.
• 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_sort_domain^⚠
  Return the domain of the given array sort.
• 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.
• Z3_get_ast_id^⚠
  Return a unique identifier for t.
• 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_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) == SortKind::FiniteDomain
• 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_implied_equalities^⚠
  Retrieve congruence class representatives for terms.
• Z3_get_index_value^⚠
  Return index of de-Bruijn bound variable.
• Z3_get_num_probes^⚠
  Return the number of builtin probes available in Z3.
• Z3_get_num_tactics^⚠
  Return the number of builtin tactics available in Z3.
• 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 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_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_weight^⚠
  Obtain weight of quantifier.
• Z3_get_range^⚠
  Return the range of the given declaration.
• Z3_get_relation_arity^⚠
  Return arity of relation.
• Z3_get_relation_column^⚠
  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.
• Z3_get_symbol_int^⚠
  Return the symbol int value.
• Z3_get_symbol_kind^⚠
  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.
• 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.
• 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 the if 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.
• 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.
• Z3_is_eq_ast^⚠
  Compare terms.
• Z3_is_eq_func_decl^⚠
  Compare terms.
• Z3_is_eq_sort^⚠
  compare sorts.
• 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 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.
• 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_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_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.
• 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_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_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.
• 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.
• 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_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.
• 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_complement^⚠
  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.
• 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 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.
• 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_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.
• 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_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.
• Z3_mk_seq_replace^⚠
  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.
• 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_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_to_int^⚠
  Convert string to integer.
• Z3_mk_string^⚠
  Create a string constant out of the string that is passed in
• Z3_mk_string_sort^⚠
  Create a sort for 8 bit strings.
• Z3_mk_string_symbol^⚠
  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.
• 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.
• 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.
• 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 an 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_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.
• 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_set_params^⚠
  Set parameters on optimization context.
• Z3_optimize_to_string^⚠
  Print the current context as a string.
• 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 number of parameters in the given parameter description set.
• 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_pattern_to_ast^⚠
  Convert a Z3_pattern into Z3_ast. This is just type casting.
• Z3_pattern_to_string^⚠
  Convert the given pattern AST node into a 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_query_constructor^⚠
  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.
• Z3_rcf_get_numerator_denominator^⚠
  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)
• 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_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_sub^⚠
  Return the value a - b.
• 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_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_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_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_model^⚠
  Retrieve the model for the last Z3_solver_check
• 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
• Z3_solver_get_reason_unknown^⚠
  Return a brief justification for an “unknown” result (i.e., Z3_L_UNDEF) for the commands Z3_solver_check
• Z3_solver_get_statistics^⚠
  Return statistics for the given solver.
• 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_pop^⚠
  Backtrack n backtracking points.
• Z3_solver_push^⚠
  Create a backtracking point.
• Z3_solver_reset^⚠
  Remove all assertions from the solver.
• Z3_solver_set_params^⚠
  Set the given solver using the given parameters.
• 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^⚠
  Convert the given sort AST node into a 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.
• Z3_substitute_vars^⚠
  Substitute the free variables in a with the expressions in to.
• 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 Z3_app. This is just type casting.
• Z3_to_func_decl^⚠
  Convert an AST into a Z3_func_decl. 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.
• Z3_update_param_value^⚠
  Set a value of a context parameter.
• Z3_update_term^⚠
  Update the arguments of term a using the arguments args.

Type Definitions

• 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_map
  Mapping from Z3_ast to Z3_ast objects.
• Z3_ast_vector
  Vector of Z3_ast objects.
• 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_error_handler
  Z3 custom error handler (See Z3_set_error_handler).
• 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_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_lbool
  Lifted Boolean type: false, undefined, true.
• Z3_literals
• Z3_model
  Model for the constraints inserted into the logical context.
• 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_params
  Parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.
• Z3_pattern
  Kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation.
• 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_rcf_num
• Z3_solver
  (Incremental) solver, possibly specialized by a particular tactic or logic.
• Z3_sort
  Kind of AST used to represent types.
• 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_tactic
  Basic building block for creating custom solvers for specific problem domains.