Z3Lib class

Constructors

Z3Lib(DynamicLibrary dynamicLibrary)

The symbols are looked up in dynamicLibrary.

Z3Lib.fromLookup(Pointer<T> lookup<T extends NativeType>(String symbolName))

The symbols are looked up with lookup.

Properties

hashCode → int

The hash code for this object.

no setter, inherited

runtimeType → Type

A representation of the runtime type of the object.

no setter, inherited

Methods

add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a) → void

\brief Add a constant interpretation.

add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value) → Z3_func_interp

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

add_rec_def(Z3_context c, Z3_func_decl f, int n, Pointer<Z3_ast> args, Z3_ast body) → void

\brief Define the body of a recursive function.

algebraic_add(Z3_context c, Z3_ast a, Z3_ast b) → Z3_ast

\brief Return the value a + b.

algebraic_div(Z3_context c, Z3_ast a, Z3_ast b) → Z3_ast

\brief Return the value a / b.

algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b) → bool

\brief Return \c true if a == b, and \c false otherwise.

algebraic_eval(Z3_context c, Z3_ast p, int n, Pointer<Z3_ast> a) → int

\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the sign of p(a0, ..., an-1).

algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b) → bool

\brief Return \c true if a >= b, and \c false otherwise.

algebraic_get_i(Z3_context c, Z3_ast a) → int

\brief Return which root of the polynomial the algebraic number represents.

algebraic_get_poly(Z3_context c, Z3_ast a) → Z3_ast_vector

\brief Return the coefficients of the defining polynomial.

algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b) → bool

\brief Return \c true if a > b, and \c false otherwise.

algebraic_is_neg(Z3_context c, Z3_ast a) → bool

\brief Return \c true if \c a is negative, and \c false otherwise.

algebraic_is_pos(Z3_context c, Z3_ast a) → bool

\brief Return \c true if \c a is positive, and \c false otherwise.

algebraic_is_value(Z3_context c, Z3_ast a) → bool

@name Algebraic Numbers / /**@{/ /** \brief Return \c true if \c a can be used as value in the Z3 real algebraic number package.

algebraic_is_zero(Z3_context c, Z3_ast a) → bool

\brief Return \c true if \c a is zero, and \c false otherwise.

algebraic_le(Z3_context c, Z3_ast a, Z3_ast b) → bool

\brief Return \c true if a <= b, and \c false otherwise.

algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b) → bool

\brief Return \c true if a < b, and \c false otherwise.

algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b) → Z3_ast

\brief Return the value a * b.

algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b) → bool

\brief Return \c true if a != b, and \c false otherwise.

algebraic_power(Z3_context c, Z3_ast a, int k) → Z3_ast

\brief Return the a^k

algebraic_root(Z3_context c, Z3_ast a, int k) → Z3_ast

\brief Return the a^(1/k)

algebraic_roots(Z3_context c, Z3_ast p, int n, Pointer<Z3_ast> a) → Z3_ast_vector

\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polynomial p(a0, ..., an-1, x_n).

algebraic_sign(Z3_context c, Z3_ast a) → int

\brief Return 1 if \c a is positive, 0 if \c a is zero, and -1 if \c a is negative.

algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b) → Z3_ast

\brief Return the value a - b.

app_to_ast(Z3_context c, Z3_app a) → Z3_ast

\brief Convert a \c Z3_app into \c Z3_ast. This is just type casting.

append_log(Z3_string string) → void

\brief Append user-defined string to interaction log.

apply_result_dec_ref(Z3_context c, Z3_apply_result r) → void

\brief Decrement the reference counter of the given \c Z3_apply_result object.

apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r) → int

\brief Return the number of subgoals in the \c Z3_apply_result object returned by #Z3_tactic_apply.

apply_result_get_subgoal(Z3_context c, Z3_apply_result r, int i) → Z3_goal

\brief Return one of the subgoals in the \c Z3_apply_result object returned by #Z3_tactic_apply.

apply_result_inc_ref(Z3_context c, Z3_apply_result r) → void

\brief Increment the reference counter of the given \c Z3_apply_result object.

apply_result_to_string(Z3_context c, Z3_apply_result r) → Z3_string

\brief Convert the \c Z3_apply_result object returned by #Z3_tactic_apply into a string.

assertions_enabled() → bool

ast_map_contains(Z3_context c, Z3_ast_map m, Z3_ast k) → bool

\brief Return true if the map \c m contains the AST key \c k.

ast_map_dec_ref(Z3_context c, Z3_ast_map m) → void

\brief Decrement the reference counter of the given AST map.

ast_map_erase(Z3_context c, Z3_ast_map m, Z3_ast k) → void

\brief Erase a key from the map.

ast_map_find(Z3_context c, Z3_ast_map m, Z3_ast k) → Z3_ast

\brief Return the value associated with the key \c k.

ast_map_inc_ref(Z3_context c, Z3_ast_map m) → void

\brief Increment the reference counter of the given AST map.

ast_map_insert(Z3_context c, Z3_ast_map m, Z3_ast k, Z3_ast v) → void

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

ast_map_keys(Z3_context c, Z3_ast_map m) → Z3_ast_vector

\brief Return the keys stored in the given map.

ast_map_reset(Z3_context c, Z3_ast_map m) → void

\brief Remove all keys from the given map.

ast_map_size(Z3_context c, Z3_ast_map m) → int

\brief Return the size of the given map.

ast_map_to_string(Z3_context c, Z3_ast_map m) → Z3_string

\brief Convert the given map into a string.

ast_to_string(Z3_context c, Z3_ast a) → Z3_string

\brief Convert the given AST node into a string.

ast_vector_dec_ref(Z3_context c, Z3_ast_vector v) → void

\brief Decrement the reference counter of the given AST vector.

ast_vector_get(Z3_context c, Z3_ast_vector v, int i) → Z3_ast

\brief Return the AST at position \c i in the AST vector \c v.

ast_vector_inc_ref(Z3_context c, Z3_ast_vector v) → void

\brief Increment the reference counter of the given AST vector.

ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a) → void

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

ast_vector_resize(Z3_context c, Z3_ast_vector v, int n) → void

\brief Resize the AST vector \c v.

ast_vector_set(Z3_context c, Z3_ast_vector v, int i, Z3_ast a) → void

\brief Update position \c i of the AST vector \c v with the AST \c a.

ast_vector_size(Z3_context c, Z3_ast_vector v) → int

\brief Return the size of the given AST vector.

ast_vector_to_string(Z3_context c, Z3_ast_vector v) → Z3_string

\brief Convert AST vector into a string.

ast_vector_translate(Z3_context s, Z3_ast_vector v, Z3_context t) → Z3_ast_vector

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

benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, int num_assumptions, Pointer<Z3_ast> assumptions, Z3_ast formula) → Z3_string

\brief Convert the given benchmark into SMT-LIB formatted string.

clearerr(Pointer<FILE> _Stream) → void

clearerr_s(Pointer<FILE> _Stream) → int

close_log() → void

\brief Close interaction log.

datatype_update_field(Z3_context c, Z3_func_decl field_access, Z3_ast t, Z3_ast value) → Z3_ast

\brief Update record field with a value.

dec_ref(Z3_context c, Z3_ast a) → void

\brief Decrement the reference counter of the given AST. The context \c c should have been created using #Z3_mk_context_rc. This function is a NOOP if \c c was created using #Z3_mk_context.

del_config(Z3_config c) → void

\brief Delete the given configuration object.

del_constructor(Z3_context c, Z3_constructor constr) → void

\brief Reclaim memory allocated to constructor.

del_constructor_list(Z3_context c, Z3_constructor_list clist) → void

\brief Reclaim memory allocated for constructor list.

del_context(Z3_context c) → void

\brief Delete the given logical context.

disable_trace(Z3_string tag) → void

\brief Disable tracing messages tagged as \c tag when Z3 is compiled in debug mode. It is a NOOP otherwise

enable_assertions(bool f) → void

enable_concurrent_dec_ref(Z3_context c) → void

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

enable_trace(Z3_string tag) → void

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

eval_smtlib2_string(Z3_context c, Z3_string str) → Z3_string

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

fclose(Pointer<FILE> _Stream) → int

fcloseall() → int

fdopen(int _FileHandle, Pointer<Char> _Format) → Pointer<FILE>

feof(Pointer<FILE> _Stream) → int

ferror(Pointer<FILE> _Stream) → int

fflush(Pointer<FILE> _Stream) → int

fgetc(Pointer<FILE> _Stream) → int

fgetchar() → int

fgetpos(Pointer<FILE> _Stream, Pointer<fpos_t> _Position) → int

fgets(Pointer<Char> _Buffer, int _MaxCount, Pointer<FILE> _Stream) → Pointer<Char>

fgetwc(Pointer<FILE> _Stream) → int

fgetws(Pointer<WChar> _Buffer, int _BufferCount, Pointer<FILE> _Stream) → Pointer<WChar>

fileno(Pointer<FILE> _Stream) → int

finalize_memory() → void

\brief Destroy all allocated resources.

fixedpoint_add_callback(Z3_context ctx, Z3_fixedpoint f, Pointer<Void> state, Z3_fixedpoint_new_lemma_eh new_lemma_eh, Z3_fixedpoint_predecessor_eh predecessor_eh, Z3_fixedpoint_unfold_eh unfold_eh) → void

\brief set export callback for lemmas

fixedpoint_add_constraint(Z3_context c, Z3_fixedpoint d, Z3_ast e, int lvl) → void

fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property) → void

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

fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, Z3_func_decl r, int num_args, Pointer<UnsignedInt> args) → void

\brief Add a Database fact.

fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) → void

\brief Add an invariant for the predicate \c pred. Add an assumed invariant of predicate \c pred.

fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name) → void

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

fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom) → void

\brief Assert a constraint to the fixedpoint context.

fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d) → void

\brief Decrement the reference counter of the given fixedpoint context.

fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s) → Z3_ast_vector

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

fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s) → Z3_ast_vector

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

fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d) → Z3_ast

\brief Retrieve a formula that encodes satisfying answers to the query.

fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f) → Z3_ast_vector

\brief Retrieve set of background assertions from fixedpoint context.

fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred) → Z3_ast

Retrieve the current cover of \c pred up to \c level unfoldings. Return just the delta that is known at \c level. To obtain the full set of properties of \c pred one should query at \c level+1 , \c level+2 etc, and include \c level=-1.

fixedpoint_get_ground_sat_answer(Z3_context c, Z3_fixedpoint d) → Z3_ast

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

fixedpoint_get_help(Z3_context c, Z3_fixedpoint f) → Z3_string

\brief Return a string describing all fixedpoint available parameters.

fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) → int

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

fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f) → Z3_param_descrs

\brief Return the parameter description set for the given fixedpoint object.

fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) → Z3_ast

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

fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d) → Z3_string

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

fixedpoint_get_rule_names_along_trace(Z3_context c, Z3_fixedpoint d) → Z3_symbol

\brief Obtain the list of rules along the counterexample trace.

fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f) → Z3_ast_vector

\brief Retrieve set of rules from fixedpoint context.

fixedpoint_get_rules_along_trace(Z3_context c, Z3_fixedpoint d) → Z3_ast_vector

\brief Obtain the list of rules along the counterexample trace.

fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d) → Z3_stats

\brief Retrieve statistics information from the last call to #Z3_fixedpoint_query.

fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d) → void

\brief Increment the reference counter of the given fixedpoint context

fixedpoint_init(Z3_context c, Z3_fixedpoint d, Pointer<Void> state) → void

\brief Initialize the context with a user-defined state.

fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query) → int

\brief Pose a query against the asserted rules.

fixedpoint_query_from_lvl(Z3_context c, Z3_fixedpoint d, Z3_ast query, int lvl) → int

@name Spacer facilities / /**@{/ /** \brief Pose a query against the asserted rules at the given level.

fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, int num_relations, Pointer<Z3_func_decl> relations) → int

\brief Pose multiple queries against the asserted rules.

fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f) → void

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

fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p) → void

\brief Set parameters on fixedpoint context.

fixedpoint_set_predicate_representation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f, int num_relations, Pointer<Z3_symbol> relation_kinds) → void

\brief Configure the predicate representation.

fixedpoint_set_reduce_app_callback(Z3_context c, Z3_fixedpoint d, Pointer<Z3_fixedpoint_reduce_app_callback_fptr> cb) → void

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

fixedpoint_set_reduce_assign_callback(Z3_context c, Z3_fixedpoint d, Pointer<Z3_fixedpoint_reduce_assign_callback_fptr> cb) → void

\brief Register a callback to destructive updates.

fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, int num_queries, Pointer<Z3_ast> queries) → Z3_string

\brief Print the current rules and background axioms as a string. \param c - context. \param f - fixedpoint context. \param num_queries - number of additional queries to print. \param queries - additional queries.

fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name) → void

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

flushall() → int

fopen(Pointer<Char> _FileName, Pointer<Char> _Mode) → Pointer<FILE>

fopen_s(Pointer<Pointer<FILE>> _Stream, Pointer<Char> _FileName, Pointer<Char> _Mode) → int

fpa_get_ebits(Z3_context c, Z3_sort s) → int

@name Z3-specific floating-point extensions / /**@{/ /** \brief Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.

fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, bool biased) → Z3_ast

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

fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, Pointer<Int64> n, bool biased) → bool

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

fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, bool biased) → Z3_string

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

fpa_get_numeral_sign(Z3_context c, Z3_ast t, Pointer<Int> sgn) → bool

\brief Retrieves the sign of a floating-point literal.

fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t) → Z3_ast

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

fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t) → Z3_ast

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

fpa_get_numeral_significand_string(Z3_context c, Z3_ast t) → Z3_string

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

fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, Pointer<Uint64> n) → bool

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

fpa_get_sbits(Z3_context c, Z3_sort s) → int

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

fpa_is_numeral_inf(Z3_context c, Z3_ast t) → bool

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

fpa_is_numeral_nan(Z3_context c, Z3_ast t) → bool

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

fpa_is_numeral_negative(Z3_context c, Z3_ast t) → bool

\brief Checks whether a given floating-point numeral is negative.

fpa_is_numeral_normal(Z3_context c, Z3_ast t) → bool

\brief Checks whether a given floating-point numeral is normal.

fpa_is_numeral_positive(Z3_context c, Z3_ast t) → bool

\brief Checks whether a given floating-point numeral is positive.

fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) → bool

\brief Checks whether a given floating-point numeral is subnormal.

fpa_is_numeral_zero(Z3_context c, Z3_ast t) → bool

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

fputc(int _Character, Pointer<FILE> _Stream) → int

fputchar(int _Ch) → int

fputs(Pointer<Char> _Buffer, Pointer<FILE> _Stream) → int

fputwc(int _Character, Pointer<FILE> _Stream) → int

fputws(Pointer<WChar> _Buffer, Pointer<FILE> _Stream) → int

fread(Pointer<Void> _Buffer, int _ElementSize, int _ElementCount, Pointer<FILE> _Stream) → int

fread_s(Pointer<Void> _Buffer, int _BufferSize, int _ElementSize, int _ElementCount, Pointer<FILE> _Stream) → int

freopen(Pointer<Char> _FileName, Pointer<Char> _Mode, Pointer<FILE> _Stream) → Pointer<FILE>

freopen_s(Pointer<Pointer<FILE>> _Stream, Pointer<Char> _FileName, Pointer<Char> _Mode, Pointer<FILE> _OldStream) → int

fseek(Pointer<FILE> _Stream, int _Offset, int _Origin) → int

fsetpos(Pointer<FILE> _Stream, Pointer<fpos_t> _Position) → int

ftell(Pointer<FILE> _Stream) → int

func_decl_to_ast(Z3_context c, Z3_func_decl f) → Z3_ast

\brief Convert a \c Z3_func_decl into \c Z3_ast. This is just type casting.

func_decl_to_string(Z3_context c, Z3_func_decl d) → Z3_string

def_API('Z3_func_decl_to_string', STRING, (_in(CONTEXT), _in(FUNC_DECL)))

func_entry_dec_ref(Z3_context c, Z3_func_entry e) → void

\brief Decrement the reference counter of the given \c Z3_func_entry object.

func_entry_get_arg(Z3_context c, Z3_func_entry e, int i) → Z3_ast

\brief Return an argument of a \c Z3_func_entry object.

func_entry_get_num_args(Z3_context c, Z3_func_entry e) → int

\brief Return the number of arguments in a \c Z3_func_entry object.

func_entry_get_value(Z3_context c, Z3_func_entry e) → Z3_ast

\brief Return the value of this point.

func_entry_inc_ref(Z3_context c, Z3_func_entry e) → void

\brief Increment the reference counter of the given \c Z3_func_entry object.

func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) → void

\brief add a function entry to a function interpretation.

func_interp_dec_ref(Z3_context c, Z3_func_interp f) → void

\brief Decrement the reference counter of the given Z3_func_interp object.

func_interp_get_arity(Z3_context c, Z3_func_interp f) → int

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

func_interp_get_else(Z3_context c, Z3_func_interp f) → Z3_ast

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

func_interp_get_entry(Z3_context c, Z3_func_interp f, int i) → Z3_func_entry

\brief Return a "point" of the given function interpretation. It represents the value of \c f in a particular point.

func_interp_get_num_entries(Z3_context c, Z3_func_interp f) → int

\brief Return the number of entries in the given function interpretation.

func_interp_inc_ref(Z3_context c, Z3_func_interp f) → void

\brief Increment the reference counter of the given Z3_func_interp object.

func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value) → void

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

fwrite(Pointer<Void> _Buffer, int _ElementSize, int _ElementCount, Pointer<FILE> _Stream) → int

get_algebraic_number_lower(Z3_context c, Z3_ast a, int precision) → Z3_ast

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

get_algebraic_number_upper(Z3_context c, Z3_ast a, int precision) → Z3_ast

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

get_app_arg(Z3_context c, Z3_app a, int i) → Z3_ast

\brief Return the i-th argument of the given application.

get_app_decl(Z3_context c, Z3_app a) → Z3_func_decl

\brief Return the declaration of a constant or function application.

get_app_num_args(Z3_context c, Z3_app a) → int

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

get_arity(Z3_context c, Z3_func_decl d) → int

\brief Alias for \c Z3_get_domain_size.

get_array_sort_domain(Z3_context c, Z3_sort t) → Z3_sort

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

get_array_sort_domain_n(Z3_context c, Z3_sort t, int idx) → Z3_sort

\brief Return the i'th domain sort of an n-dimensional array.

get_array_sort_range(Z3_context c, Z3_sort t) → Z3_sort

\brief Return the range of the given array sort.

get_as_array_func_decl(Z3_context c, Z3_ast a) → Z3_func_decl

\brief Return the function declaration \c f associated with a \ccode{(_ as_array f)} node.

get_ast_hash(Z3_context c, Z3_ast a) → int

\brief 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 \c Z3_get_ast_id returns an identifier that is unique over the set of live AST objects.

get_ast_id(Z3_context c, Z3_ast t) → int

\brief Return a unique identifier for \c 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.

get_ast_kind(Z3_context c, Z3_ast a) → int

\brief Return the kind of the given AST.

get_bool_value(Z3_context c, Z3_ast a) → int

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

get_bv_sort_size(Z3_context c, Z3_sort t) → int

\brief Return the size of the given bit-vector sort.

get_datatype_sort_constructor(Z3_context c, Z3_sort t, int idx) → Z3_func_decl

\brief Return idx'th constructor.

get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, int idx_c, int idx_a) → Z3_func_decl

\brief Return idx_a'th accessor for the idx_c'th constructor.

get_datatype_sort_num_constructors(Z3_context c, Z3_sort t) → int

\brief Return number of constructors for datatype.

get_datatype_sort_recognizer(Z3_context c, Z3_sort t, int idx) → Z3_func_decl

\brief Return idx'th recognizer.

get_decl_ast_parameter(Z3_context c, Z3_func_decl d, int idx) → Z3_ast

\brief Return the expression value associated with an expression parameter.

get_decl_double_parameter(Z3_context c, Z3_func_decl d, int idx) → double

\brief Return the double value associated with an double parameter.

get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, int idx) → Z3_func_decl

\brief Return the expression value associated with an expression parameter.

get_decl_int_parameter(Z3_context c, Z3_func_decl d, int idx) → int

\brief Return the integer value associated with an integer parameter.

get_decl_kind(Z3_context c, Z3_func_decl d) → int

\brief Return declaration kind corresponding to declaration.

get_decl_name(Z3_context c, Z3_func_decl d) → Z3_symbol

\brief Return the constant declaration name as a symbol.

get_decl_num_parameters(Z3_context c, Z3_func_decl d) → int

\brief Return the number of parameters associated with a declaration.

get_decl_parameter_kind(Z3_context c, Z3_func_decl d, int idx) → int

\brief Return the parameter type associated with a declaration.

get_decl_rational_parameter(Z3_context c, Z3_func_decl d, int idx) → Z3_string

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

get_decl_sort_parameter(Z3_context c, Z3_func_decl d, int idx) → Z3_sort

\brief Return the sort value associated with a sort parameter.

get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, int idx) → Z3_symbol

\brief Return the double value associated with an double parameter.

get_denominator(Z3_context c, Z3_ast a) → Z3_ast

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

get_domain(Z3_context c, Z3_func_decl d, int i) → Z3_sort

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

get_domain_size(Z3_context c, Z3_func_decl d) → int

\brief Return the number of parameters of the given declaration.

get_error_code(Z3_context c) → int

\brief Return the error code for the last API call.

get_error_msg(Z3_context c, int err) → Z3_string

\brief Return a string describing the given error code.

get_estimated_alloc_size() → int

\brief Return the estimated allocated memory in bytes.

get_finite_domain_sort_size(Z3_context c, Z3_sort s, Pointer<Uint64> r) → bool

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

get_full_version() → Z3_string

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

get_func_decl_id(Z3_context c, Z3_func_decl f) → int

\brief Return a unique identifier for \c f.

get_global_param_descrs(Z3_context c) → Z3_param_descrs

\brief Retrieve description of global parameters.

get_implied_equalities(Z3_context c, Z3_solver s, int num_terms, Pointer<Z3_ast> terms, Pointer<UnsignedInt> class_ids) → int

\brief Retrieve congruence class representatives for terms.

get_index_value(Z3_context c, Z3_ast a) → int

\brief Return index of de-Bruijn bound variable.

get_lstring(Z3_context c, Z3_ast s, Pointer<UnsignedInt> length) → Z3_char_ptr

\brief Retrieve the string constant stored in \c 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.

get_num_probes(Z3_context c) → int

\brief Return the number of builtin probes available in Z3.

get_num_simplifiers(Z3_context c) → int

\brief Return the number of builtin simplifiers available in Z3.

get_num_tactics(Z3_context c) → int

\brief Return the number of builtin tactics available in Z3.

get_numeral_binary_string(Z3_context c, Z3_ast a) → Z3_string

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

get_numeral_decimal_string(Z3_context c, Z3_ast a, int precision) → Z3_string

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

get_numeral_double(Z3_context c, Z3_ast a) → double

\brief Return numeral as a double.

get_numeral_int(Z3_context c, Z3_ast v, Pointer<Int> i) → bool

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

get_numeral_int64(Z3_context c, Z3_ast v, Pointer<Int64> i) → bool

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

get_numeral_rational_int64(Z3_context c, Z3_ast v, Pointer<Int64> num, Pointer<Int64> den) → bool

\brief Similar to #Z3_get_numeral_string, but only succeeds if the value can fit as a rational number as machine \c int64_t int. Return \c true if the call succeeded.

get_numeral_small(Z3_context c, Z3_ast a, Pointer<Int64> num, Pointer<Int64> den) → bool

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

get_numeral_string(Z3_context c, Z3_ast a) → Z3_string

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

get_numeral_uint(Z3_context c, Z3_ast v, Pointer<UnsignedInt> u) → bool

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

get_numeral_uint64(Z3_context c, Z3_ast v, Pointer<Uint64> u) → bool

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

get_numerator(Z3_context c, Z3_ast a) → Z3_ast

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

get_pattern(Z3_context c, Z3_pattern p, int idx) → Z3_ast

\brief Return i'th ast in pattern.

get_pattern_num_terms(Z3_context c, Z3_pattern p) → int

\brief Return number of terms in pattern.

get_probe_name(Z3_context c, int i) → Z3_string

\brief Return the name of the \c i probe.

get_quantifier_body(Z3_context c, Z3_ast a) → Z3_ast

\brief Return body of quantifier.

get_quantifier_bound_name(Z3_context c, Z3_ast a, int i) → Z3_symbol

\brief Return symbol of the i'th bound variable.

get_quantifier_bound_sort(Z3_context c, Z3_ast a, int i) → Z3_sort

\brief Return sort of the i'th bound variable.

get_quantifier_no_pattern_ast(Z3_context c, Z3_ast a, int i) → Z3_ast

\brief Return i'th no_pattern.

get_quantifier_num_bound(Z3_context c, Z3_ast a) → int

\brief Return number of bound variables of quantifier.

get_quantifier_num_no_patterns(Z3_context c, Z3_ast a) → int

\brief Return number of no_patterns used in quantifier.

get_quantifier_num_patterns(Z3_context c, Z3_ast a) → int

\brief Return number of patterns used in quantifier.

get_quantifier_pattern_ast(Z3_context c, Z3_ast a, int i) → Z3_pattern

\brief Return i'th pattern.

get_quantifier_weight(Z3_context c, Z3_ast a) → int

\brief Obtain weight of quantifier.

get_range(Z3_context c, Z3_func_decl d) → Z3_sort

\brief Return the range of the given declaration.

get_re_sort_basis(Z3_context c, Z3_sort s) → Z3_sort

\brief Retrieve basis sort for regex sort.

get_relation_arity(Z3_context c, Z3_sort s) → int

\brief Return arity of relation.

get_relation_column(Z3_context c, Z3_sort s, int col) → Z3_sort

\brief Return sort at i'th column of relation sort.

get_seq_sort_basis(Z3_context c, Z3_sort s) → Z3_sort

\brief Retrieve basis sort for sequence sort.

get_simplifier_name(Z3_context c, int i) → Z3_string

\brief Return the name of the idx simplifier.

get_sort(Z3_context c, Z3_ast a) → Z3_sort

\brief Return the sort of an AST node.

get_sort_id(Z3_context c, Z3_sort s) → int

\brief Return a unique identifier for \c s.

get_sort_kind(Z3_context c, Z3_sort t) → int

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

get_sort_name(Z3_context c, Z3_sort d) → Z3_symbol

\brief Return the sort name as a symbol.

get_string(Z3_context c, Z3_ast s) → Z3_string

\brief Retrieve the string constant stored in \c s. Characters outside the basic printable ASCII range are escaped.

get_string_contents(Z3_context c, Z3_ast s, int length, Pointer<UnsignedInt> contents) → void

\brief Retrieve the unescaped string constant stored in \c s.

get_string_length(Z3_context c, Z3_ast s) → int

\brief Retrieve the length of the unescaped string constant stored in \c s.

get_symbol_int(Z3_context c, Z3_symbol s) → int

\brief Return the symbol int value.

get_symbol_kind(Z3_context c, Z3_symbol s) → int

@name Accessors / /**@{/ /** \brief Return \c Z3_INT_SYMBOL if the symbol was constructed using #Z3_mk_int_symbol, and \c Z3_STRING_SYMBOL if the symbol was constructed using #Z3_mk_string_symbol.

get_symbol_string(Z3_context c, Z3_symbol s) → Z3_string

\brief Return the symbol name.

get_tactic_name(Z3_context c, int i) → Z3_string

\brief Return the name of the idx tactic.

get_tuple_sort_field_decl(Z3_context c, Z3_sort t, int i) → Z3_func_decl

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

get_tuple_sort_mk_decl(Z3_context c, Z3_sort t) → Z3_func_decl

\brief Return the constructor declaration of the given tuple sort.

get_tuple_sort_num_fields(Z3_context c, Z3_sort t) → int

\brief Return the number of fields of the given tuple sort.

get_version(Pointer<UnsignedInt> major, Pointer<UnsignedInt> minor, Pointer<UnsignedInt> build_number, Pointer<UnsignedInt> revision_number) → void

\brief Return Z3 version number information.

getc(Pointer<FILE> _Stream) → int

getchar() → int

gets_s(Pointer<Char> _Buffer, int _Size) → Pointer<Char>

getw(Pointer<FILE> _Stream) → int

getwc(Pointer<FILE> _Stream) → int

getwchar() → int

global_param_get(Z3_string param_id, Z3_string_ptr param_value) → bool

\brief Get a global (or module) parameter.

global_param_reset_all() → void

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

global_param_set(Z3_string param_id, Z3_string param_value) → void

@{*/ /** \brief Set a global (or module) parameter. This setting is shared by all Z3 contexts.

goal_assert(Z3_context c, Z3_goal g, Z3_ast a) → void

\brief Add a new formula \c 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 \c false, adding new formulas is a no-op. If the formula \c a is \c true, then nothing is added. If the formula \c a is \c false, then the entire goal is replaced by the formula \c false.

goal_convert_model(Z3_context c, Z3_goal g, Z3_model m) → Z3_model

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

goal_dec_ref(Z3_context c, Z3_goal g) → void

\brief Decrement the reference counter of the given goal.

goal_depth(Z3_context c, Z3_goal g) → int

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

goal_formula(Z3_context c, Z3_goal g, int idx) → Z3_ast

\brief Return a formula from the given goal.

goal_inc_ref(Z3_context c, Z3_goal g) → void

\brief Increment the reference counter of the given goal.

goal_inconsistent(Z3_context c, Z3_goal g) → bool

\brief Return \c true if the given goal contains the formula \c false.

goal_is_decided_sat(Z3_context c, Z3_goal g) → bool

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

goal_is_decided_unsat(Z3_context c, Z3_goal g) → bool

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

goal_num_exprs(Z3_context c, Z3_goal g) → int

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

goal_precision(Z3_context c, Z3_goal g) → int

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

goal_reset(Z3_context c, Z3_goal g) → void

\brief Erase all formulas from the given goal.

goal_size(Z3_context c, Z3_goal g) → int

\brief Return the number of formulas in the given goal.

goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names) → Z3_string

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

goal_to_string(Z3_context c, Z3_goal g) → Z3_string

\brief Convert a goal into a string.

goal_translate(Z3_context source, Z3_goal g, Z3_context target) → Z3_goal

\brief Copy a goal \c g from the context \c source to the context \c target.

inc_ref(Z3_context c, Z3_ast a) → void

\brief Increment the reference counter of the given AST. The context \c c should have been created using #Z3_mk_context_rc. This function is a NOOP if \c c was created using #Z3_mk_context.

interrupt(Z3_context c) → void

\brief Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.

is_algebraic_number(Z3_context c, Z3_ast a) → bool

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

is_app(Z3_context c, Z3_ast a) → bool

def_API('Z3_is_app', BOOL, (_in(CONTEXT), _in(AST)))

is_as_array(Z3_context c, Z3_ast a) → bool

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

is_char_sort(Z3_context c, Z3_sort s) → bool

\brief Check if \c s is a character sort.

is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2) → bool

\brief Compare terms.

is_eq_func_decl(Z3_context c, Z3_func_decl f1, Z3_func_decl f2) → bool

\brief Compare terms.

is_eq_sort(Z3_context c, Z3_sort s1, Z3_sort s2) → bool

\brief compare sorts.

is_lambda(Z3_context c, Z3_ast a) → bool

\brief Determine if ast is a lambda expression.

is_numeral_ast(Z3_context c, Z3_ast a) → bool

def_API('Z3_is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST)))

is_quantifier_exists(Z3_context c, Z3_ast a) → bool

\brief Determine if ast is an existential quantifier.

is_quantifier_forall(Z3_context c, Z3_ast a) → bool

\brief Determine if an ast is a universal quantifier.

is_re_sort(Z3_context c, Z3_sort s) → bool

\brief Check if \c s is a regular expression sort.

is_seq_sort(Z3_context c, Z3_sort s) → bool

\brief Check if \c s is a sequence sort.

is_string(Z3_context c, Z3_ast s) → bool

\brief Determine if \c s is a string constant.

is_string_sort(Z3_context c, Z3_sort s) → bool

\brief Check if \c s is a string sort.

is_well_sorted(Z3_context c, Z3_ast t) → bool

\brief Return \c true if the given expression \c t is well sorted.

mk_add(Z3_context c, int num_args, Pointer<Z3_ast> args) → Z3_ast

@name Integers and Reals / /**@{/ /** \brief Create an AST node representing \ccode{args0 + ... + argsnum_args-1}.

mk_and(Z3_context c, int num_args, Pointer<Z3_ast> args) → Z3_ast

\brief Create an AST node representing \ccode{args0 and ... and argsnum_args-1}.

mk_app(Z3_context c, Z3_func_decl d, int num_args, Pointer<Z3_ast> args) → Z3_ast

\brief Create a constant or function application.

mk_array_default(Z3_context c, Z3_ast array) → Z3_ast

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

mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2) → Z3_ast

\brief 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))

mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range) → Z3_sort

\brief Create an array type.

mk_array_sort_n(Z3_context c, int n, Pointer<Z3_sort> domain, Z3_sort range) → Z3_sort

\brief Create an array type with N arguments

mk_as_array(Z3_context c, Z3_func_decl f) → Z3_ast

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

mk_ast_map(Z3_context c) → Z3_ast_map

@name AST maps / /**@{/ /** \brief Return an empty mapping from AST to AST

mk_ast_vector(Z3_context c) → Z3_ast_vector

@name AST vectors / /**@{/ /** \brief Return an empty AST vector.

mk_atleast(Z3_context c, int num_args, Pointer<Z3_ast> args, int k) → Z3_ast

\brief Pseudo-Boolean relations.

mk_atmost(Z3_context c, int num_args, Pointer<Z3_ast> args, int k) → Z3_ast

\brief Pseudo-Boolean relations.

mk_bit2bool(Z3_context c, int i, Z3_ast t1) → Z3_ast

\brief Extracts the bit at position \ccode{i} of a bit-vector and yields a boolean.

mk_bool_sort(Z3_context c) → Z3_sort

\brief Create the Boolean type.

mk_bound(Z3_context c, int index, Z3_sort ty) → Z3_ast

\brief Create a variable.

mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed) → Z3_ast

\brief Create an integer from the bit-vector argument \c t1. If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. So the result is non-negative and in the range \ccode{0..2^N-1}, where N are the number of bits in \c t1. If \c is_signed is true, \c t1 is treated as a signed bit-vector.

mk_bv_numeral(Z3_context c, int sz, Pointer<Bool> bits) → Z3_ast

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

mk_bv_sort(Z3_context c, int sz) → Z3_sort

\brief Create a bit-vector type of the given size.

mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Standard two's complement addition.

mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed) → Z3_ast

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

mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

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

mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Bitwise and.

mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Arithmetic shift right.

mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Logical shift right.

mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Standard two's complement multiplication.

mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed) → Z3_ast

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

mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

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

mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Bitwise nand.

mk_bvneg(Z3_context c, Z3_ast t1) → Z3_ast

\brief Standard two's complement unary minus.

mk_bvneg_no_overflow(Z3_context c, Z3_ast t1) → Z3_ast

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

mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Bitwise nor.

mk_bvnot(Z3_context c, Z3_ast t1) → Z3_ast

@name Bit-vectors / /**@{/ /** \brief Bitwise negation.

mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Bitwise or.

mk_bvredand(Z3_context c, Z3_ast t1) → Z3_ast

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

mk_bvredor(Z3_context c, Z3_ast t1) → Z3_ast

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

mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Two's complement signed division.

mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

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

mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Two's complement signed greater than or equal to.

mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Two's complement signed greater than.

mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Shift left.

mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Two's complement signed less than or equal to.

mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Two's complement signed less than.

mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

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

mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

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

mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Standard two's complement subtraction.

mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

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

mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed) → Z3_ast

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

mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Unsigned division.

mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Unsigned greater than or equal to.

mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Unsigned greater than.

mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Unsigned less than or equal to.

mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Unsigned less than.

mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Unsigned remainder.

mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Bitwise xnor.

mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Bitwise exclusive-or.

mk_char(Z3_context c, int ch) → Z3_ast

\brief Create a character literal def_API('Z3_mk_char', AST, (_in(CONTEXT), _in(UINT)))

mk_char_from_bv(Z3_context c, Z3_ast bv) → Z3_ast

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

mk_char_is_digit(Z3_context c, Z3_ast ch) → Z3_ast

\brief Create a check if the character is a digit.

mk_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2) → Z3_ast

\brief Create less than or equal to between two characters.

mk_char_sort(Z3_context c) → Z3_sort

\brief Create a sort for unicode characters.

mk_char_to_bv(Z3_context c, Z3_ast ch) → Z3_ast

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

mk_char_to_int(Z3_context c, Z3_ast ch) → Z3_ast

\brief Create an integer (code point) from character.

mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Concatenate the given bit-vectors.

mk_config() → Z3_config

\brief Create a configuration object for the Z3 context object.

mk_const(Z3_context c, Z3_symbol s, Z3_sort ty) → Z3_ast

\brief Declare and create a constant.

mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v) → Z3_ast

\brief Create the constant array.

mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, int num_fields, Pointer<Z3_symbol> field_names, Pointer<Z3_sort> sorts, Pointer<UnsignedInt> sort_refs) → Z3_constructor

\brief Create a constructor.

mk_constructor_list(Z3_context c, int num_constructors, Pointer<Z3_constructor> constructors) → Z3_constructor_list

\brief Create list of constructors.

mk_context(Z3_config c) → Z3_context

\brief Create a context using the given configuration.

mk_context_rc(Z3_config c) → Z3_context

\brief 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 \c 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 \c Z3_ast returned by Z3, and #Z3_dec_ref whenever the \c Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.

mk_datatype(Z3_context c, Z3_symbol name, int num_constructors, Pointer<Z3_constructor> constructors) → Z3_sort

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

mk_datatype_sort(Z3_context c, Z3_symbol name) → Z3_sort

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

mk_datatypes(Z3_context c, int num_sorts, Pointer<Z3_symbol> sort_names, Pointer<Z3_sort> sorts, Pointer<Z3_constructor_list> constructor_lists) → void

\brief Create mutually recursive datatypes.

mk_distinct(Z3_context c, int num_args, Pointer<Z3_ast> args) → Z3_ast

\brief Create an AST node representing \ccode{distinct(args0, ..., argsnum_args-1)}.

mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2) → Z3_ast

\brief Create an AST node representing \ccode{arg1 div arg2}.

mk_divides(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Create division predicate.

mk_empty_set(Z3_context c, Z3_sort domain) → Z3_ast

\brief Create the empty set.

mk_enumeration_sort(Z3_context c, Z3_symbol name, int n, Pointer<Z3_symbol> enum_names, Pointer<Z3_func_decl> enum_consts, Pointer<Z3_func_decl> enum_testers) → Z3_sort

\brief Create a enumeration sort.

mk_eq(Z3_context c, Z3_ast l, Z3_ast r) → Z3_ast

\brief Create an AST node representing \ccode{l = r}.

mk_exists(Z3_context c, int weight, int num_patterns, Pointer<Z3_pattern> patterns, int num_decls, Pointer<Z3_sort> sorts, Pointer<Z3_symbol> decl_names, Z3_ast body) → Z3_ast

\brief Create an exists formula. Similar to #Z3_mk_forall.

mk_exists_const(Z3_context c, int weight, int num_bound, Pointer<Z3_app> bound, int num_patterns, Pointer<Z3_pattern> patterns, Z3_ast body) → Z3_ast

\brief Similar to #Z3_mk_forall_const.

mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Rotate bits of \c t1 to the left \c t2 times.

mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Rotate bits of \c t1 to the right \c t2 times.

mk_extract(Z3_context c, int high, int low, Z3_ast t1) → Z3_ast

\brief Extract the bits \c high down to \c low from a bit-vector of size \c m to yield a new bit-vector of size \c n, where \ccode{n = high - low + 1}.

mk_false(Z3_context c) → Z3_ast

\brief Create an AST node representing \c false.

mk_finite_domain_sort(Z3_context c, Z3_symbol name, int size) → Z3_sort

\brief Create a named finite domain sort.

mk_fixedpoint(Z3_context c) → Z3_fixedpoint

@name Fixedpoint facilities / /**@{/ /** \brief Create a new fixedpoint context.

mk_forall(Z3_context c, int weight, int num_patterns, Pointer<Z3_pattern> patterns, int num_decls, Pointer<Z3_sort> sorts, Pointer<Z3_symbol> decl_names, Z3_ast body) → Z3_ast

\brief Create a forall formula. It takes an expression \c body that contains bound variables of the same sorts as the sorts listed in the array \c sorts. The bound variables are de-Bruijn indices created using #Z3_mk_bound. The array \c decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the \c decl_names and \c sorts array refers to the variable with index 0, the second to last element of \c decl_names and \c sorts refers to the variable with index 1, etc.

mk_forall_const(Z3_context c, int weight, int num_bound, Pointer<Z3_app> bound, int num_patterns, Pointer<Z3_pattern> patterns, Z3_ast body) → Z3_ast

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

mk_fpa_abs(Z3_context c, Z3_ast t) → Z3_ast

\brief Floating-point absolute value

mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point addition

mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point division

mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point equality.

mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3) → Z3_ast

\brief Floating-point fused multiply-add.

mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig) → Z3_ast

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

mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point greater than or equal.

mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point greater than.

mk_fpa_inf(Z3_context c, Z3_sort s, bool negative) → Z3_ast

\brief Create a floating-point infinity of sort \c s.

mk_fpa_is_infinite(Z3_context c, Z3_ast t) → Z3_ast

\brief Predicate indicating whether \c t is a floating-point number representing +oo or -oo.

mk_fpa_is_nan(Z3_context c, Z3_ast t) → Z3_ast

\brief Predicate indicating whether \c t is a NaN.

mk_fpa_is_negative(Z3_context c, Z3_ast t) → Z3_ast

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

mk_fpa_is_normal(Z3_context c, Z3_ast t) → Z3_ast

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

mk_fpa_is_positive(Z3_context c, Z3_ast t) → Z3_ast

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

mk_fpa_is_subnormal(Z3_context c, Z3_ast t) → Z3_ast

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

mk_fpa_is_zero(Z3_context c, Z3_ast t) → Z3_ast

\brief Predicate indicating whether \c t is a floating-point number with zero value, i.e., +zero or -zero.

mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point less than or equal.

mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point less than.

mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Maximum of floating-point numbers.

mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Minimum of floating-point numbers.

mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point multiplication

mk_fpa_nan(Z3_context c, Z3_sort s) → Z3_ast

\brief Create a floating-point NaN of sort \c s.

mk_fpa_neg(Z3_context c, Z3_ast t) → Z3_ast

\brief Floating-point negation

mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty) → Z3_ast

\brief Create a numeral of FloatingPoint sort from a double.

mk_fpa_numeral_float(Z3_context c, double v, Z3_sort ty) → Z3_ast

\brief Create a numeral of FloatingPoint sort from a float.

mk_fpa_numeral_int(Z3_context c, int v, Z3_sort ty) → Z3_ast

\brief Create a numeral of FloatingPoint sort from a signed integer.

mk_fpa_numeral_int64_uint64(Z3_context c, bool sgn, int exp, int sig, Z3_sort ty) → Z3_ast

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

mk_fpa_numeral_int_uint(Z3_context c, bool sgn, int exp, int sig, Z3_sort ty) → Z3_ast

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

mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point remainder

mk_fpa_rna(Z3_context c) → Z3_ast

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

mk_fpa_rne(Z3_context c) → Z3_ast

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

mk_fpa_round_nearest_ties_to_away(Z3_context c) → Z3_ast

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

mk_fpa_round_nearest_ties_to_even(Z3_context c) → Z3_ast

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

mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t) → Z3_ast

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

mk_fpa_round_toward_negative(Z3_context c) → Z3_ast

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

mk_fpa_round_toward_positive(Z3_context c) → Z3_ast

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

mk_fpa_round_toward_zero(Z3_context c) → Z3_ast

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

mk_fpa_rounding_mode_sort(Z3_context c) → Z3_sort

@name Floating-Point Arithmetic / /**@{/ /** \brief Create the RoundingMode sort.

mk_fpa_rtn(Z3_context c) → Z3_ast

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

mk_fpa_rtp(Z3_context c) → Z3_ast

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

mk_fpa_rtz(Z3_context c) → Z3_ast

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

mk_fpa_sort(Z3_context c, int ebits, int sbits) → Z3_sort

\brief Create a FloatingPoint sort.

mk_fpa_sort_128(Z3_context c) → Z3_sort

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

mk_fpa_sort_16(Z3_context c) → Z3_sort

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

mk_fpa_sort_32(Z3_context c) → Z3_sort

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

mk_fpa_sort_64(Z3_context c) → Z3_sort

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

mk_fpa_sort_double(Z3_context c) → Z3_sort

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

mk_fpa_sort_half(Z3_context c) → Z3_sort

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

mk_fpa_sort_quadruple(Z3_context c) → Z3_sort

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

mk_fpa_sort_single(Z3_context c) → Z3_sort

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

mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t) → Z3_ast

\brief Floating-point square root

mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Floating-point subtraction

mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s) → Z3_ast

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

mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) → Z3_ast

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

mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) → Z3_ast

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

mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) → Z3_ast

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

mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) → Z3_ast

\brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) → Z3_ast

\brief Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.

mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) → Z3_ast

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

mk_fpa_to_real(Z3_context c, Z3_ast t) → Z3_ast

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

mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, int sz) → Z3_ast

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

mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, int sz) → Z3_ast

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

mk_fpa_zero(Z3_context c, Z3_sort s, bool negative) → Z3_ast

\brief Create a floating-point zero of sort \c s.

mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty) → Z3_ast

\brief Declare and create a fresh constant.

mk_fresh_func_decl(Z3_context c, Z3_string prefix, int domain_size, Pointer<Z3_sort> domain, Z3_sort range) → Z3_func_decl

\brief Declare a fresh constant or function.

mk_full_set(Z3_context c, Z3_sort domain) → Z3_ast

\brief Create the full set.

mk_func_decl(Z3_context c, Z3_symbol s, int domain_size, Pointer<Z3_sort> domain, Z3_sort range) → Z3_func_decl

\brief Declare a constant or function.

mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Create greater than or equal to.

mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs) → Z3_goal

@name Goals / /**@{/ /** \brief Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Create greater than.

mk_iff(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Create an AST node representing \ccode{t1 iff t2}.

mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Create an AST node representing \ccode{t1 implies t2}.

mk_int(Z3_context c, int v, Z3_sort ty) → Z3_ast

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

mk_int2bv(Z3_context c, int n, Z3_ast t1) → Z3_ast

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

mk_int2real(Z3_context c, Z3_ast t1) → Z3_ast

\brief Coerce an integer to a real.

mk_int64(Z3_context c, int v, Z3_sort ty) → Z3_ast

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

mk_int_sort(Z3_context c) → Z3_sort

\brief Create the integer type.

mk_int_symbol(Z3_context c, int i) → Z3_symbol

\brief Create a Z3 symbol using an integer.

mk_int_to_str(Z3_context c, Z3_ast s) → Z3_ast

\brief Integer to string conversion.

mk_is_int(Z3_context c, Z3_ast t1) → Z3_ast

\brief Check if a real number is an integer.

mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) → Z3_ast

\brief Create an AST node representing an if-then-else: \ccode{ite(t1, t2, t3)}.

mk_lambda(Z3_context c, int num_decls, Pointer<Z3_sort> sorts, Pointer<Z3_symbol> decl_names, Z3_ast body) → Z3_ast

\brief Create a lambda expression. It takes an expression \c body that contains bound variables of the same sorts as the sorts listed in the array \c sorts. The bound variables are de-Bruijn indices created using #Z3_mk_bound. The array \c decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the \c decl_names and \c sorts array refers to the variable with index 0, the second to last element of \c decl_names and \c sorts refers to the variable with index 1, etc. The sort of the resulting expression is \c (Array sorts range) where \c range is the sort of \c body. For example, if the lambda binds two variables of sort \c Int and \c Bool, and the \c body has sort \c Real, the sort of the expression is \c (Array Int Bool Real).

mk_lambda_const(Z3_context c, int num_bound, Pointer<Z3_app> bound, Z3_ast body) → Z3_ast

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

mk_le(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Create less than or equal to.

mk_linear_order(Z3_context c, Z3_sort a, int id) → Z3_func_decl

@name Special relations / /**@{/ /** \brief create a linear ordering relation over signature \c a. The relation is identified by the index \c id.

mk_list_sort(Z3_context c, Z3_symbol name, Z3_sort elem_sort, Pointer<Z3_func_decl> nil_decl, Pointer<Z3_func_decl> is_nil_decl, Pointer<Z3_func_decl> cons_decl, Pointer<Z3_func_decl> is_cons_decl, Pointer<Z3_func_decl> head_decl, Pointer<Z3_func_decl> tail_decl) → Z3_sort

\brief Create a list sort

mk_lstring(Z3_context c, int len, Z3_string s) → Z3_ast

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

mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Create less than.

mk_map(Z3_context c, Z3_func_decl f, int n, Pointer<Z3_ast> args) → Z3_ast

\brief Map f on the argument arrays.

mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2) → Z3_ast

\brief Create an AST node representing \ccode{arg1 mod arg2}.

mk_model(Z3_context c) → Z3_model

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

mk_mul(Z3_context c, int num_args, Pointer<Z3_ast> args) → Z3_ast

\brief Create an AST node representing \ccode{args0 * ... * argsnum_args-1}.

mk_not(Z3_context c, Z3_ast a) → Z3_ast

\brief Create an AST node representing \ccode{not(a)}.

mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty) → Z3_ast

@name Numerals / /**@{/ /** \brief Create a numeral of a given sort.

mk_optimize(Z3_context c) → Z3_optimize

@name Optimization facilities / /**@{/ /** \brief Create a new optimize context.

mk_or(Z3_context c, int num_args, Pointer<Z3_ast> args) → Z3_ast

\brief Create an AST node representing \ccode{args0 or ... or argsnum_args-1}.

mk_params(Z3_context c) → Z3_params

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

mk_parser_context(Z3_context c) → Z3_parser_context

\brief Create a parser context.

mk_partial_order(Z3_context c, Z3_sort a, int id) → Z3_func_decl

\brief create a partial ordering relation over signature \c a and index \c id.

mk_pattern(Z3_context c, int num_patterns, Pointer<Z3_ast> terms) → Z3_pattern

@name Quantifiers / /**@{/ /** \brief Create a pattern for quantifier instantiation.

mk_pbeq(Z3_context c, int num_args, Pointer<Z3_ast> args, Pointer<Int> coeffs, int k) → Z3_ast

\brief Pseudo-Boolean relations.

mk_pbge(Z3_context c, int num_args, Pointer<Z3_ast> args, Pointer<Int> coeffs, int k) → Z3_ast

\brief Pseudo-Boolean relations.

mk_pble(Z3_context c, int num_args, Pointer<Z3_ast> args, Pointer<Int> coeffs, int k) → Z3_ast

\brief Pseudo-Boolean relations.

mk_piecewise_linear_order(Z3_context c, Z3_sort a, int id) → Z3_func_decl

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

mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2) → Z3_ast

\brief Create an AST node representing \ccode{arg1 ^ arg2}.

mk_probe(Z3_context c, Z3_string name) → Z3_probe

\brief 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 \ccode{(help-tactic)} in the SMT 2.0 front-end.

mk_quantifier(Z3_context c, bool is_forall, int weight, int num_patterns, Pointer<Z3_pattern> patterns, int num_decls, Pointer<Z3_sort> sorts, Pointer<Z3_symbol> decl_names, Z3_ast body) → Z3_ast

\brief Create a quantifier - universal or existential, with pattern hints. See the documentation for #Z3_mk_forall for an explanation of the parameters.

mk_quantifier_const(Z3_context c, bool is_forall, int weight, int num_bound, Pointer<Z3_app> bound, int num_patterns, Pointer<Z3_pattern> patterns, Z3_ast body) → Z3_ast

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

mk_quantifier_const_ex(Z3_context c, bool is_forall, int weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, int num_bound, Pointer<Z3_app> bound, int num_patterns, Pointer<Z3_pattern> patterns, int num_no_patterns, Pointer<Z3_ast> no_patterns, Z3_ast body) → Z3_ast

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

mk_quantifier_ex(Z3_context c, bool is_forall, int weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, int num_patterns, Pointer<Z3_pattern> patterns, int num_no_patterns, Pointer<Z3_ast> no_patterns, int num_decls, Pointer<Z3_sort> sorts, Pointer<Z3_symbol> decl_names, Z3_ast body) → Z3_ast

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

mk_re_allchar(Z3_context c, Z3_sort regex_sort) → Z3_ast

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

mk_re_complement(Z3_context c, Z3_ast re) → Z3_ast

\brief Create the complement of the regular language \c re.

mk_re_concat(Z3_context c, int n, Pointer<Z3_ast> args) → Z3_ast

\brief Create the concatenation of the regular languages.

mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2) → Z3_ast

\brief Create the difference of regular expressions.

mk_re_empty(Z3_context c, Z3_sort re) → Z3_ast

\brief Create an empty regular expression of sort \c re.

mk_re_full(Z3_context c, Z3_sort re) → Z3_ast

\brief Create an universal regular expression of sort \c re.

mk_re_intersect(Z3_context c, int n, Pointer<Z3_ast> args) → Z3_ast

\brief Create the intersection of the regular languages.

mk_re_loop(Z3_context c, Z3_ast r, int lo, int hi) → Z3_ast

\brief Create a regular expression loop. The supplied regular expression \c r is repeated between \c lo and \c hi times. The \c lo should be below \c hi with one exception: when supplying the value \c hi as 0, the meaning is to repeat the argument \c r at least \c lo number of times, and with an unbounded upper bound.

mk_re_option(Z3_context c, Z3_ast re) → Z3_ast

\brief Create the regular language \c re.

mk_re_plus(Z3_context c, Z3_ast re) → Z3_ast

\brief Create the regular language \c re+.

mk_re_power(Z3_context c, Z3_ast re, int n) → Z3_ast

\brief Create a power regular expression.

mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi) → Z3_ast

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

mk_re_sort(Z3_context c, Z3_sort seq) → Z3_sort

\brief Create a regular expression sort out of a sequence sort.

mk_re_star(Z3_context c, Z3_ast re) → Z3_ast

\brief Create the regular language \c re*.

mk_re_union(Z3_context c, int n, Pointer<Z3_ast> args) → Z3_ast

\brief Create the union of the regular languages.

mk_real(Z3_context c, int num, int den) → Z3_ast

\brief Create a real from a fraction.

mk_real2int(Z3_context c, Z3_ast t1) → Z3_ast

\brief Coerce a real to an integer.

mk_real_int64(Z3_context c, int num, int den) → Z3_ast

\brief Create a real from a fraction of int64.

mk_real_sort(Z3_context c) → Z3_sort

\brief Create the real type.

mk_rec_func_decl(Z3_context c, Z3_symbol s, int domain_size, Pointer<Z3_sort> domain, Z3_sort range) → Z3_func_decl

\brief Declare a recursive function

mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2) → Z3_ast

\brief Create an AST node representing \ccode{arg1 rem arg2}.

mk_repeat(Z3_context c, int i, Z3_ast t1) → Z3_ast

\brief Repeat the given bit-vector up length \ccode{i}.

mk_rotate_left(Z3_context c, int i, Z3_ast t1) → Z3_ast

\brief Rotate bits of \c t1 to the left \c i times.

mk_rotate_right(Z3_context c, int i, Z3_ast t1) → Z3_ast

\brief Rotate bits of \c t1 to the right \c i times.

mk_sbv_to_str(Z3_context c, Z3_ast s) → Z3_ast

\brief Signed bit-vector to string conversion.

mk_select(Z3_context c, Z3_ast a, Z3_ast i) → Z3_ast

@name Arrays / /**@{/ /** \brief Array read. The argument \c a is the array and \c i is the index of the array that gets read.

mk_select_n(Z3_context c, Z3_ast a, int n, Pointer<Z3_ast> idxs) → Z3_ast

\brief n-ary Array read. The argument \c a is the array and \c idxs are the indices of the array that gets read.

mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index) → Z3_ast

\brief Retrieve from \c s the unit sequence positioned at position \c index. The sequence is empty if the index is out of bounds.

mk_seq_concat(Z3_context c, int n, Pointer<Z3_ast> args) → Z3_ast

\brief Concatenate sequences.

mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee) → Z3_ast

\brief Check if \c container contains \c containee.

mk_seq_empty(Z3_context c, Z3_sort seq) → Z3_ast

\brief Create an empty sequence of the sequence sort \c seq.

mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length) → Z3_ast

\brief Extract subsequence starting at \c offset of \c length.

mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re) → Z3_ast

\brief Check if \c seq is in the language generated by the regular expression \c re.

mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset) → Z3_ast

\brief Return index of the first occurrence of \c substr in \c s starting from offset \c offset. If \c s does not contain \c substr, then the value is -1, if \c offset is the length of \c s, then the value is -1 as well. The value is -1 if \c offset is negative or larger than the length of \c s.

mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr) → Z3_ast

\brief Return index of the last occurrence of \c substr in \c s. If \c s does not contain \c substr, then the value is -1, def_API('Z3_mk_seq_last_index', AST, (_in(CONTEXT), _in(AST), _in(AST)))

mk_seq_length(Z3_context c, Z3_ast s) → Z3_ast

\brief Return the length of the sequence \c s.

mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index) → Z3_ast

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

mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s) → Z3_ast

\brief Check if \c prefix is a prefix of \c s.

mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst) → Z3_ast

\brief Replace the first occurrence of \c src with \c dst in \c s.

mk_seq_sort(Z3_context c, Z3_sort s) → Z3_sort

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

mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s) → Z3_ast

\brief Check if \c suffix is a suffix of \c s.

mk_seq_to_re(Z3_context c, Z3_ast seq) → Z3_ast

\brief Create a regular expression that accepts the sequence \c seq.

mk_seq_unit(Z3_context c, Z3_ast a) → Z3_ast

\brief Create a unit sequence of \c a.

mk_set_add(Z3_context c, Z3_ast set1, Z3_ast elem) → Z3_ast

\brief Add an element to a set.

mk_set_complement(Z3_context c, Z3_ast arg) → Z3_ast

\brief Take the complement of a set.

mk_set_del(Z3_context c, Z3_ast set1, Z3_ast elem) → Z3_ast

\brief Remove an element to a set.

mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2) → Z3_ast

\brief Take the set difference between two sets.

mk_set_has_size(Z3_context c, Z3_ast set1, Z3_ast k) → Z3_ast

\brief Create predicate that holds if Boolean array \c set has \c k elements set to true.

mk_set_intersect(Z3_context c, int num_args, Pointer<Z3_ast> args) → Z3_ast

\brief Take the intersection of a list of sets.

mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set1) → Z3_ast

\brief Check for set membership.

mk_set_sort(Z3_context c, Z3_sort ty) → Z3_sort

@name Sets / /**@{/ /** \brief Create Set type.

mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2) → Z3_ast

\brief Check for subsetness of sets.

mk_set_union(Z3_context c, int num_args, Pointer<Z3_ast> args) → Z3_ast

\brief Take the union of a list of sets.

mk_sign_ext(Z3_context c, int i, Z3_ast t1) → Z3_ast

\brief Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size \ccode{m+i}, where \c m is the size of the given bit-vector.

mk_simple_solver(Z3_context c) → Z3_solver

\brief Create a new incremental solver.

mk_simplifier(Z3_context c, Z3_string name) → Z3_simplifier

\brief 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 \ccode{(help-simplifier)} in the SMT 2.0 front-end.

mk_solver(Z3_context c) → Z3_solver

@name Solvers*/ /@{*/ / \brief 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.

mk_solver_for_logic(Z3_context c, Z3_symbol logic) → Z3_solver

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

mk_solver_from_tactic(Z3_context c, Z3_tactic t) → Z3_solver

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

mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v) → Z3_ast

\brief Array update.

mk_store_n(Z3_context c, Z3_ast a, int n, Pointer<Z3_ast> idxs, Z3_ast v) → Z3_ast

\brief n-ary Array update.

mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s) → Z3_ast

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

mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s) → Z3_ast

\brief Check if \c s1 is lexicographically strictly less than \c s2.

mk_str_to_int(Z3_context c, Z3_ast s) → Z3_ast

\brief Convert string to integer.

mk_string(Z3_context c, Z3_string s) → Z3_ast

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

mk_string_from_code(Z3_context c, Z3_ast a) → Z3_ast

\brief Code to string conversion.

mk_string_sort(Z3_context c) → Z3_sort

\brief Create a sort for unicode strings.

mk_string_symbol(Z3_context c, Z3_string s) → Z3_symbol

\brief Create a Z3 symbol using a C string.

mk_string_to_code(Z3_context c, Z3_ast a) → Z3_ast

\brief String to code conversion.

mk_sub(Z3_context c, int num_args, Pointer<Z3_ast> args) → Z3_ast

\brief Create an AST node representing \ccode{args0 - ... - argsnum_args - 1}.

mk_tactic(Z3_context c, Z3_string name) → Z3_tactic

@name Tactics, Simplifiers and Probes / /**@{/ /** \brief 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 \ccode{(help-tactic)} in the SMT 2.0 front-end.

mk_transitive_closure(Z3_context c, Z3_func_decl f) → Z3_func_decl

\brief create transitive closure of binary relation.

mk_tree_order(Z3_context c, Z3_sort a, int id) → Z3_func_decl

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

mk_true(Z3_context c) → Z3_ast

@name Propositional Logic and Equality / /**@{/ /** \brief Create an AST node representing \c true.

mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, int num_fields, Pointer<Z3_symbol> field_names, Pointer<Z3_sort> field_sorts, Pointer<Z3_func_decl> mk_tuple_decl, Pointer<Z3_func_decl> proj_decl) → Z3_sort

\brief Create a tuple type.

mk_type_variable(Z3_context c, Z3_symbol s) → Z3_sort

\brief Create a type variable.

mk_u32string(Z3_context c, int len, Pointer<UnsignedInt> chars) → Z3_ast

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

mk_ubv_to_str(Z3_context c, Z3_ast s) → Z3_ast

\brief Unsigned bit-vector to string conversion.

mk_unary_minus(Z3_context c, Z3_ast arg) → Z3_ast

\brief Create an AST node representing \ccode{- arg}.

mk_uninterpreted_sort(Z3_context c, Z3_symbol s) → Z3_sort

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

mk_unsigned_int(Z3_context c, int v, Z3_sort ty) → Z3_ast

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

mk_unsigned_int64(Z3_context c, int v, Z3_sort ty) → Z3_ast

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

mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2) → Z3_ast

\brief Create an AST node representing \ccode{t1 xor t2}.

mk_zero_ext(Z3_context c, int i, Z3_ast t1) → Z3_ast

\brief Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size \ccode{m+i}, where \c m is the size of the given bit-vector.

model_dec_ref(Z3_context c, Z3_model m) → void

\brief Decrement the reference counter of the given model.

model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Pointer<Z3_ast> v) → bool

\brief Evaluate the AST node \c t in the given model. Return \c true if succeeded, and store the result in \c v.

model_extrapolate(Z3_context c, Z3_model m, Z3_ast fml) → Z3_ast

\brief Extrapolates a model of a formula

model_get_const_decl(Z3_context c, Z3_model m, int i) → Z3_func_decl

\brief Return the i-th constant in the given model.

model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) → Z3_ast

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

model_get_func_decl(Z3_context c, Z3_model m, int i) → Z3_func_decl

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

model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f) → Z3_func_interp

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

model_get_num_consts(Z3_context c, Z3_model m) → int

\brief Return the number of constants assigned by the given model.

model_get_num_funcs(Z3_context c, Z3_model m) → int

\brief Return the number of function interpretations in the given model.

model_get_num_sorts(Z3_context c, Z3_model m) → int

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

model_get_sort(Z3_context c, Z3_model m, int i) → Z3_sort

\brief Return a uninterpreted sort that \c m assigns an interpretation.

model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s) → Z3_ast_vector

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

model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a) → bool

\brief Test if there exists an interpretation (i.e., assignment) for \c a in the model \c m.

model_inc_ref(Z3_context c, Z3_model m) → void

\brief Increment the reference counter of the given model.

model_to_string(Z3_context c, Z3_model m) → Z3_string

\brief Convert the given model into a string.

model_translate(Z3_context c, Z3_model m, Z3_context dst) → Z3_model

\brief translate model from context \c c to context \c dst.

noSuchMethod(Invocation invocation) → dynamic

Invoked when a nonexistent method or property is accessed.

inherited

open_log(Z3_string filename) → bool

@name Interaction logging / /**@{/ /** \brief Log interaction to a file.

optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a) → void

\brief Assert hard constraint to the optimization context.

optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t) → void

\brief Assert tracked hard constraint to the optimization context.

optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) → int

\brief Assert soft constraint to the optimization context. \param c - context \param o - optimization context \param a - formula \param weight - a penalty for violating soft constraint. Negative weights convert into rewards. \param id - optional identifier to group soft constraints

optimize_check(Z3_context c, Z3_optimize o, int num_assumptions, Pointer<Z3_ast> assumptions) → int

\brief Check consistency and produce optimal values. \param c - context \param o - optimization context \param num_assumptions - number of additional assumptions \param assumptions - the additional assumptions

optimize_dec_ref(Z3_context c, Z3_optimize d) → void

\brief Decrement the reference counter of the given optimize context.

optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s) → void

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

optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s) → void

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

optimize_get_assertions(Z3_context c, Z3_optimize o) → Z3_ast_vector

\brief Return the set of asserted formulas on the optimization context.

optimize_get_help(Z3_context c, Z3_optimize t) → Z3_string

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

optimize_get_lower(Z3_context c, Z3_optimize o, int idx) → Z3_ast

\brief Retrieve lower bound value or approximation for the i'th optimization objective.

optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, int idx) → Z3_ast_vector

\brief 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 \c a, \c b, \c c and encode the result of #Z3_optimize_get_lower \ccode{a * infinity + b + c * epsilon}.

optimize_get_model(Z3_context c, Z3_optimize o) → Z3_model

\brief Retrieve the model for the last #Z3_optimize_check

optimize_get_objectives(Z3_context c, Z3_optimize o) → Z3_ast_vector

\brief 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 \ccode{(+ (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.

optimize_get_param_descrs(Z3_context c, Z3_optimize o) → Z3_param_descrs

\brief Return the parameter description set for the given optimize object.

optimize_get_reason_unknown(Z3_context c, Z3_optimize d) → Z3_string

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

optimize_get_statistics(Z3_context c, Z3_optimize d) → Z3_stats

\brief Retrieve statistics information from the last call to #Z3_optimize_check

optimize_get_unsat_core(Z3_context c, Z3_optimize o) → Z3_ast_vector

\brief Retrieve the unsat core for the last #Z3_optimize_check The unsat core is a subset of the assumptions \c a.

optimize_get_upper(Z3_context c, Z3_optimize o, int idx) → Z3_ast

\brief Retrieve upper bound value or approximation for the i'th optimization objective.

optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, int idx) → Z3_ast_vector

\brief Retrieve upper bound value or approximation for the i'th optimization objective.

optimize_inc_ref(Z3_context c, Z3_optimize d) → void

\brief Increment the reference counter of the given optimize context

optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t) → int

\brief Add a maximization constraint. \param c - context \param o - optimization context \param t - arithmetical term

optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t) → int

\brief Add a minimization constraint. \param c - context \param o - optimization context \param t - arithmetical term

optimize_pop(Z3_context c, Z3_optimize d) → void

\brief Backtrack one level.

optimize_push(Z3_context c, Z3_optimize d) → void

\brief Create a backtracking point.

optimize_register_model_eh(Z3_context c, Z3_optimize o, Z3_model m, Pointer<Void> ctx, Pointer<Z3_model_eh> model_eh) → void

\brief register a model event handler for new models.

optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p) → void

\brief Set parameters on optimization context.

optimize_to_string(Z3_context c, Z3_optimize o) → Z3_string

\brief Print the current context as a string. \param c - context. \param o - optimization context.

param_descrs_dec_ref(Z3_context c, Z3_param_descrs p) → void

\brief Decrement the reference counter of the given parameter description set.

param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s) → Z3_string

\brief Retrieve documentation string corresponding to parameter name \c s.

param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n) → int

\brief Return the kind associated with the given parameter name \c n.

param_descrs_get_name(Z3_context c, Z3_param_descrs p, int i) → Z3_symbol

\brief Return the name of the parameter at given index \c i.

param_descrs_inc_ref(Z3_context c, Z3_param_descrs p) → void

\brief Increment the reference counter of the given parameter description set.

param_descrs_size(Z3_context c, Z3_param_descrs p) → int

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

param_descrs_to_string(Z3_context c, Z3_param_descrs p) → Z3_string

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

params_dec_ref(Z3_context c, Z3_params p) → void

\brief Decrement the reference counter of the given parameter set.

params_inc_ref(Z3_context c, Z3_params p) → void

\brief Increment the reference counter of the given parameter set.

params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v) → void

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

params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v) → void

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

params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v) → void

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

params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, int v) → void

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

params_to_string(Z3_context c, Z3_params p) → Z3_string

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

params_validate(Z3_context c, Z3_params p, Z3_param_descrs d) → void

\brief Validate the parameter set \c p against the parameter description set \c d.

parse_smtlib2_file(Z3_context c, Z3_string file_name, int num_sorts, Pointer<Z3_symbol> sort_names, Pointer<Z3_sort> sorts, int num_decls, Pointer<Z3_symbol> decl_names, Pointer<Z3_func_decl> decls) → Z3_ast_vector

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

parse_smtlib2_string(Z3_context c, Z3_string str, int num_sorts, Pointer<Z3_symbol> sort_names, Pointer<Z3_sort> sorts, int num_decls, Pointer<Z3_symbol> decl_names, Pointer<Z3_func_decl> decls) → Z3_ast_vector

@name Parser interface / /**@{/ /** \brief Parse the given string using the SMT-LIB2 parser.

parser_context_add_decl(Z3_context c, Z3_parser_context pc, Z3_func_decl f) → void

\brief Add a function declaration.

parser_context_add_sort(Z3_context c, Z3_parser_context pc, Z3_sort s) → void

\brief Add a sort declaration.

parser_context_dec_ref(Z3_context c, Z3_parser_context pc) → void

\brief Decrement the reference counter of the given \c Z3_parser_context object.

parser_context_from_string(Z3_context c, Z3_parser_context pc, Z3_string s) → Z3_ast_vector

\brief Parse a string of SMTLIB2 commands. Return assertions.

parser_context_inc_ref(Z3_context c, Z3_parser_context pc) → void

\brief Increment the reference counter of the given \c Z3_parser_context object.

pattern_to_ast(Z3_context c, Z3_pattern p) → Z3_ast

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

pattern_to_string(Z3_context c, Z3_pattern p) → Z3_string

def_API('Z3_pattern_to_string', STRING, (_in(CONTEXT), _in(PATTERN)))

perror(Pointer<Char> _ErrorMessage) → void

polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) → Z3_ast_vector

\brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x.

probe_and(Z3_context x, Z3_probe p1, Z3_probe p2) → Z3_probe

\brief Return a probe that evaluates to "true" when \c p1 and \c p2 evaluates to true.

probe_apply(Z3_context c, Z3_probe p, Z3_goal g) → double

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

probe_const(Z3_context x, double val) → Z3_probe

\brief Return a probe that always evaluates to val.

probe_dec_ref(Z3_context c, Z3_probe p) → void

\brief Decrement the reference counter of the given probe.

probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2) → Z3_probe

\brief Return a probe that evaluates to "true" when the value returned by \c p1 is equal to the value returned by \c p2.

probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2) → Z3_probe

\brief Return a probe that evaluates to "true" when the value returned by \c p1 is greater than or equal to the value returned by \c p2.

probe_get_descr(Z3_context c, Z3_string name) → Z3_string

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

probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2) → Z3_probe

\brief Return a probe that evaluates to "true" when the value returned by \c p1 is greater than the value returned by \c p2.

probe_inc_ref(Z3_context c, Z3_probe p) → void

\brief Increment the reference counter of the given probe.

probe_le(Z3_context x, Z3_probe p1, Z3_probe p2) → Z3_probe

\brief Return a probe that evaluates to "true" when the value returned by \c p1 is less than or equal to the value returned by \c p2.

probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2) → Z3_probe

\brief Return a probe that evaluates to "true" when the value returned by \c p1 is less than the value returned by \c p2.

probe_not(Z3_context x, Z3_probe p) → Z3_probe

\brief Return a probe that evaluates to "true" when \c p does not evaluate to true.

probe_or(Z3_context x, Z3_probe p1, Z3_probe p2) → Z3_probe

\brief Return a probe that evaluates to "true" when \c p1 or \c p2 evaluates to true.

putc(int _Character, Pointer<FILE> _Stream) → int

putchar(int _Character) → int

puts(Pointer<Char> _Buffer) → int

putw(int _Ch, Pointer<FILE> _Stream) → int

putwc(int _Character, Pointer<FILE> _Stream) → int

putwchar(int _Character) → int

qe_lite(Z3_context c, Z3_ast_vector vars, Z3_ast body) → Z3_ast

\brief Best-effort quantifier elimination

qe_model_project(Z3_context c, Z3_model m, int num_bounds, Pointer<Z3_app> bound, Z3_ast body) → Z3_ast

\brief Project variables given a model

qe_model_project_skolem(Z3_context c, Z3_model m, int num_bounds, Pointer<Z3_app> bound, Z3_ast body, Z3_ast_map map) → Z3_ast

\brief Project variables given a model

query_constructor(Z3_context c, Z3_constructor constr, int num_fields, Pointer<Z3_func_decl> constructor, Pointer<Z3_func_decl> tester, Pointer<Z3_func_decl> accessors) → void

\brief Query constructor for declared functions.

rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → Z3_rcf_num

\brief Return the value \ccode{a + b}.

rcf_del(Z3_context c, Z3_rcf_num a) → void

@name Real Closed Fields / /**@{/ /** \brief Delete a RCF numeral created using the RCF API.

rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → Z3_rcf_num

\brief Return the value \ccode{a / b}.

rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → bool

\brief Return \c true if \ccode{a == b}.

rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → bool

\brief Return \c true if \ccode{a >= b}.

rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Pointer<Z3_rcf_num> n, Pointer<Z3_rcf_num> d) → void

\brief Extract the "numerator" and "denominator" of the given RCF numeral. We have that \ccode{a = n/d}, moreover \c n and \c d are not represented using rational functions.

rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → bool

\brief Return \c true if \ccode{a > b}.

rcf_inv(Z3_context c, Z3_rcf_num a) → Z3_rcf_num

\brief Return the value \ccode{1/a}.

rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → bool

\brief Return \c true if \ccode{a <= b}.

rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → bool

\brief Return \c true if \ccode{a < b}.

rcf_mk_e(Z3_context c) → Z3_rcf_num

\brief Return e (Euler's constant)

rcf_mk_infinitesimal(Z3_context c) → Z3_rcf_num

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

rcf_mk_pi(Z3_context c) → Z3_rcf_num

\brief Return Pi

rcf_mk_rational(Z3_context c, Z3_string val) → Z3_rcf_num

\brief Return a RCF rational using the given string.

rcf_mk_roots(Z3_context c, int n, Pointer<Z3_rcf_num> a, Pointer<Z3_rcf_num> roots) → int

\brief Store in roots the roots of the polynomial \ccode{an-1*x^{n-1} + ... + a0}. The output vector \c roots must have size \c n. It returns the number of roots of the polynomial.

rcf_mk_small_int(Z3_context c, int val) → Z3_rcf_num

\brief Return a RCF small integer.

rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → Z3_rcf_num

\brief Return the value \ccode{a * b}.

rcf_neg(Z3_context c, Z3_rcf_num a) → Z3_rcf_num

\brief Return the value \ccode{-a}.

rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → bool

\brief Return \c true if \ccode{a != b}.

rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, int prec) → Z3_string

\brief Convert the RCF numeral into a string in decimal notation.

rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html) → Z3_string

\brief Convert the RCF numeral into a string.

rcf_power(Z3_context c, Z3_rcf_num a, int k) → Z3_rcf_num

\brief Return the value \ccode{a^k}.

rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) → Z3_rcf_num

\brief Return the value \ccode{a - b}.

remove(Pointer<Char> _FileName) → int

rename(Pointer<Char> _OldFileName, Pointer<Char> _NewFileName) → int

reset_memory() → void

\brief Reset all allocated resources.

rewind(Pointer<FILE> _Stream) → void

rmtmp() → int

set_ast_print_mode(Z3_context c, int mode) → void

@name String conversion / /**@{/ /** \brief Select mode for the format used for pretty-printing AST nodes.

set_error(Z3_context c, int e) → void

\brief Set an error.

set_error_handler(Z3_context c, Pointer<Z3_error_handler> h) → void

\brief Register a Z3 error handler.

set_param_value(Z3_config c, Z3_string param_id, Z3_string param_value) → void

\brief Set a configuration parameter.

setbuf(Pointer<FILE> _Stream, Pointer<Char> _Buffer) → void

setvbuf(Pointer<FILE> _Stream, Pointer<Char> _Buffer, int _Mode, int _Size) → int

simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2) → Z3_simplifier

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

simplifier_dec_ref(Z3_context c, Z3_simplifier g) → void

\brief Decrement the reference counter of the given simplifier.

simplifier_get_descr(Z3_context c, Z3_string name) → Z3_string

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

simplifier_get_help(Z3_context c, Z3_simplifier t) → Z3_string

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

simplifier_get_param_descrs(Z3_context c, Z3_simplifier t) → Z3_param_descrs

\brief Return the parameter description set for the given simplifier object.

simplifier_inc_ref(Z3_context c, Z3_simplifier t) → void

\brief Increment the reference counter of the given simplifier.

simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p) → Z3_simplifier

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

simplify(Z3_context c, Z3_ast a) → Z3_ast

\brief Interface to simplifier.

simplify_ex(Z3_context c, Z3_ast a, Z3_params p) → Z3_ast

\brief Interface to simplifier.

simplify_get_help(Z3_context c) → Z3_string

\brief Return a string describing all available parameters.

simplify_get_param_descrs(Z3_context c) → Z3_param_descrs

\brief Return the parameter description set for the simplify procedure.

solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier) → Z3_solver

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

solver_assert(Z3_context c, Z3_solver s, Z3_ast a) → void

\brief Assert a constraint into the solver.

solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p) → void

\brief Assert a constraint \c a into the solver, and track it (in the unsat) core using the Boolean constant \c p.

solver_check(Z3_context c, Z3_solver s) → int

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

solver_check_assumptions(Z3_context c, Z3_solver s, int num_assumptions, Pointer<Z3_ast> assumptions) → int

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

solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a) → Z3_ast

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

solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a) → Z3_ast

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

solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, int backtrack_level) → Z3_ast_vector

\brief extract a next cube for a solver. The last cube is the constant \c true or \c 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.

solver_dec_ref(Z3_context c, Z3_solver s) → void

\brief Decrement the reference counter of the given solver.

solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name) → void

\brief load solver assertions from a file.

solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name) → void

\brief load solver assertions from a string.

solver_get_assertions(Z3_context c, Z3_solver s) → Z3_ast_vector

\brief Return the set of asserted formulas on the solver.

solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences) → int

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

solver_get_help(Z3_context c, Z3_solver s) → Z3_string

\brief Return a string describing all solver available parameters.

solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, int sz, Pointer<UnsignedInt> levels) → void

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

solver_get_model(Z3_context c, Z3_solver s) → Z3_model

\brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions

solver_get_non_units(Z3_context c, Z3_solver s) → Z3_ast_vector

\brief Return the set of non units in the solver state.

solver_get_num_scopes(Z3_context c, Z3_solver s) → int

\brief Return the number of backtracking points.

solver_get_param_descrs(Z3_context c, Z3_solver s) → Z3_param_descrs

\brief Return the parameter description set for the given solver object.

solver_get_proof(Z3_context c, Z3_solver s) → Z3_ast

\brief Retrieve the proof for the last #Z3_solver_check or #Z3_solver_check_assumptions

solver_get_reason_unknown(Z3_context c, Z3_solver s) → Z3_string

\brief Return a brief justification for an "unknown" result (i.e., \c Z3_L_UNDEF) for the commands #Z3_solver_check and #Z3_solver_check_assumptions

solver_get_statistics(Z3_context c, Z3_solver s) → Z3_stats

\brief Return statistics for the given solver.

solver_get_trail(Z3_context c, Z3_solver s) → Z3_ast_vector

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

solver_get_units(Z3_context c, Z3_solver s) → Z3_ast_vector

\brief Return the set of units modulo model conversion.

solver_get_unsat_core(Z3_context c, Z3_solver s) → Z3_ast_vector

\brief Retrieve the unsat core for the last #Z3_solver_check_assumptions The unsat core is a subset of the assumptions \c a.

solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst) → void

\brief Ad-hoc method for importing model conversion from solver.

solver_inc_ref(Z3_context c, Z3_solver s) → void

\brief Increment the reference counter of the given solver.

solver_interrupt(Z3_context c, Z3_solver s) → void

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

solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, int idx, int phase) → bool

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.

solver_pop(Z3_context c, Z3_solver s, int n) → void

\brief Backtrack \c n backtracking points.

solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, int num_fixed, Pointer<Z3_ast> fixed, int num_eqs, Pointer<Z3_ast> eq_lhs, Pointer<Z3_ast> eq_rhs, Z3_ast conseq) → bool

\brief propagate a consequence based on fixed values. This is a callback a client may invoke during the fixed_eh callback. The callback adds a propagation consequence based on the fixed values of the \c ids. The solver might discard the propagation in case it is true in the current state. The function returns false in this case; otw. the function returns true. At least one propagation in the final callback has to return true in order to prevent the solver from finishing.

solver_propagate_created(Z3_context c, Z3_solver s, Pointer<Z3_created_eh> created_eh) → void

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

solver_propagate_decide(Z3_context c, Z3_solver s, Pointer<Z3_decide_eh> decide_eh) → void

\brief 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

solver_propagate_declare(Z3_context c, Z3_symbol name, int n, Pointer<Z3_sort> domain, Z3_sort range) → Z3_func_decl

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

solver_propagate_diseq(Z3_context c, Z3_solver s, Pointer<Z3_eq_eh> eq_eh) → void

\brief register a callback on expression dis-equalities.

solver_propagate_eq(Z3_context c, Z3_solver s, Pointer<Z3_eq_eh> eq_eh) → void

\brief register a callback on expression equalities.

solver_propagate_final(Z3_context c, Z3_solver s, Pointer<Z3_final_eh> final_eh) → void

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

solver_propagate_fixed(Z3_context c, Z3_solver s, Pointer<Z3_fixed_eh> fixed_eh) → void

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

solver_propagate_init(Z3_context c, Z3_solver s, Pointer<Void> user_context, Pointer<Z3_push_eh> push_eh, Pointer<Z3_pop_eh> pop_eh, Pointer<Z3_fresh_eh> fresh_eh) → void

\brief register a user-propagator with the solver.

solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e) → void

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

solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e) → void

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

solver_push(Z3_context c, Z3_solver s) → void

\brief Create a backtracking point.

solver_register_on_clause(Z3_context c, Z3_solver s, Pointer<Void> user_context, Pointer<Z3_on_clause_eh> on_clause_eh) → void

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

solver_reset(Z3_context c, Z3_solver s) → void

\brief Remove all assertions from the solver.

solver_set_params(Z3_context c, Z3_solver s, Z3_params p) → void

\brief Set the given solver using the given parameters.

solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names) → Z3_string

\brief Convert a solver into a DIMACS formatted string. \sa Z3_goal_to_diamcs_string for requirements.

solver_to_string(Z3_context c, Z3_solver s) → Z3_string

\brief Convert a solver into a string.

solver_translate(Z3_context source, Z3_solver s, Z3_context target) → Z3_solver

\brief Copy a solver \c s from the context \c source to the context \c target.

sort_to_ast(Z3_context c, Z3_sort s) → Z3_ast

\brief Convert a \c Z3_sort into \c Z3_ast. This is just type casting.

sort_to_string(Z3_context c, Z3_sort s) → Z3_string

def_API('Z3_sort_to_string', STRING, (_in(CONTEXT), _in(SORT)))

stats_dec_ref(Z3_context c, Z3_stats s) → void

\brief Decrement the reference counter of the given statistics object.

stats_get_double_value(Z3_context c, Z3_stats s, int idx) → double

\brief Return the double value of the given statistical data.

stats_get_key(Z3_context c, Z3_stats s, int idx) → Z3_string

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

stats_get_uint_value(Z3_context c, Z3_stats s, int idx) → int

\brief Return the unsigned value of the given statistical data.

stats_inc_ref(Z3_context c, Z3_stats s) → void

\brief Increment the reference counter of the given statistics object.

stats_is_double(Z3_context c, Z3_stats s, int idx) → bool

\brief Return \c true if the given statistical data is a double.

stats_is_uint(Z3_context c, Z3_stats s, int idx) → bool

\brief Return \c true if the given statistical data is a unsigned integer.

stats_size(Z3_context c, Z3_stats s) → int

\brief Return the number of statistical data in \c s.

stats_to_string(Z3_context c, Z3_stats s) → Z3_string

\brief Convert a statistics into a string.

substitute(Z3_context c, Z3_ast a, int num_exprs, Pointer<Z3_ast> from, Pointer<Z3_ast> to) → Z3_ast

\brief Substitute every occurrence of \ccode{fromi} in \c a with \ccode{toi}, for \c i smaller than \c num_exprs. The result is the new AST. The arrays \c from and \c to must have size \c num_exprs. For every \c i smaller than \c num_exprs, we must have that sort of \ccode{fromi} must be equal to sort of \ccode{toi}.

substitute_funs(Z3_context c, Z3_ast a, int num_funs, Pointer<Z3_func_decl> from, Pointer<Z3_ast> to) → Z3_ast

\brief Substitute functions in \c from with new expressions in \c to.

substitute_vars(Z3_context c, Z3_ast a, int num_exprs, Pointer<Z3_ast> to) → Z3_ast

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

tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2) → Z3_tactic

\brief Return a tactic that applies \c t1 to a given goal and \c t2 to every subgoal produced by \c t1.

tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g) → Z3_apply_result

\brief Apply tactic \c t to the goal \c g.

tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p) → Z3_apply_result

\brief Apply tactic \c t to the goal \c g using the parameter set \c p.

tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2) → Z3_tactic

\brief Return a tactic that applies \c t1 to a given goal if the probe \c p evaluates to true, and \c t2 if \c p evaluates to false.

tactic_dec_ref(Z3_context c, Z3_tactic g) → void

\brief Decrement the reference counter of the given tactic.

tactic_fail(Z3_context c) → Z3_tactic

\brief Return a tactic that always fails.

tactic_fail_if(Z3_context c, Z3_probe p) → Z3_tactic

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

tactic_fail_if_not_decided(Z3_context c) → Z3_tactic

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

tactic_get_descr(Z3_context c, Z3_string name) → Z3_string

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

tactic_get_help(Z3_context c, Z3_tactic t) → Z3_string

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

tactic_get_param_descrs(Z3_context c, Z3_tactic t) → Z3_param_descrs

\brief Return the parameter description set for the given tactic object.

tactic_inc_ref(Z3_context c, Z3_tactic t) → void

\brief Increment the reference counter of the given tactic.

tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2) → Z3_tactic

\brief Return a tactic that first applies \c t1 to a given goal, if it fails then returns the result of \c t2 applied to the given goal.

tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2) → Z3_tactic

\brief Return a tactic that applies \c t1 to a given goal and then \c t2 to every subgoal produced by \c t1. The subgoals are processed in parallel.

tactic_par_or(Z3_context c, int num, Pointer<Z3_tactic> ts) → Z3_tactic

\brief Return a tactic that applies the given tactics in parallel.

tactic_repeat(Z3_context c, Z3_tactic t, int max) → Z3_tactic

\brief Return a tactic that keeps applying \c t until the goal is not modified anymore or the maximum number of iterations \c max is reached.

tactic_skip(Z3_context c) → Z3_tactic

\brief Return a tactic that just return the given goal.

tactic_try_for(Z3_context c, Z3_tactic t, int ms) → Z3_tactic

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

tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p) → Z3_tactic

\brief Return a tactic that applies \c t using the given set of parameters.

tactic_when(Z3_context c, Z3_probe p, Z3_tactic t) → Z3_tactic

\brief Return a tactic that applies \c t to a given goal is the probe \c p evaluates to true. If \c p evaluates to false, then the new tactic behaves like the skip tactic.

tempnam(Pointer<Char> _Directory, Pointer<Char> _FilePrefix) → Pointer<Char>

tmpfile() → Pointer<FILE>

tmpfile_s(Pointer<Pointer<FILE>> _Stream) → int

tmpnam(Pointer<Char> _Buffer) → Pointer<Char>

tmpnam_s(Pointer<Char> _Buffer, int _Size) → int

to_app(Z3_context c, Z3_ast a) → Z3_app

\brief Convert an \c ast into an \c APP_AST. This is just type casting.

to_func_decl(Z3_context c, Z3_ast a) → Z3_func_decl

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

toggle_warning_messages(bool enabled) → void

\brief Enable/disable printing warning messages to the console.

toString() → String

A string representation of this object.

inherited

translate(Z3_context source, Z3_ast a, Z3_context target) → Z3_ast

\brief Translate/Copy the AST \c a from context \c source to context \c target. AST \c a must have been created using context \c source. \pre source != target

ungetc(int _Character, Pointer<FILE> _Stream) → int

ungetwc(int _Character, Pointer<FILE> _Stream) → int

unlink(Pointer<Char> _FileName) → int

update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value) → void

\brief Set a value of a context parameter.

update_term(Z3_context c, Z3_ast a, int num_args, Pointer<Z3_ast> args) → Z3_ast

@name Modifiers / /**@{/ /** \brief Update the arguments of term \c a using the arguments \c args. The number of arguments \c num_args should coincide with the number of arguments to \c a. If \c a is a quantifier, then num_args has to be 1.

Operators

operator ==(Object other) → bool

The equality operator.

inherited