Crate z3_sys [−] [src]
Enums
AstKind |
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types. |
AstPrintMode |
Z3 pretty printing modes (See |
DeclKind |
The different kinds of interpreted function kinds. |
ErrorCode |
Z3 error codes (See |
GoalPrec |
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations. |
ParamKind |
The different kinds of parameters that can be associated with parameter sets.
(see |
ParameterKind |
The different kinds of parameters that can be associated with function symbols. |
SortKind |
The different kinds of Z3 types (See |
SymbolKind |
The different kinds of symbol.
In Z3, a symbol can be represented using integers and
strings (See |
Constants
Z3_FALSE | |
Z3_L_FALSE | |
Z3_L_TRUE | |
Z3_L_UNDEF | |
Z3_TRUE |
Functions
Z3_add_const_interp⚠ |
Add a constant interpretation. |
Z3_add_func_interp⚠ |
Create a fresh func_interp object, add it to a model for a specified function. It has reference count 0. |
Z3_algebraic_add⚠ |
Return the value |
Z3_algebraic_div⚠ |
Return the value |
Z3_algebraic_eq⚠ |
Return |
Z3_algebraic_eval⚠ |
Given a multivariate polynomial |
Z3_algebraic_ge⚠ |
Return |
Z3_algebraic_gt⚠ |
Return |
Z3_algebraic_is_neg⚠ |
Return |
Z3_algebraic_is_pos⚠ |
Return |
Z3_algebraic_is_value⚠ |
Return |
Z3_algebraic_is_zero⚠ |
Return |
Z3_algebraic_le⚠ |
Return |
Z3_algebraic_lt⚠ |
Return |
Z3_algebraic_mul⚠ |
Return the value |
Z3_algebraic_neq⚠ |
Return |
Z3_algebraic_power⚠ |
Return the |
Z3_algebraic_root⚠ |
Return the |
Z3_algebraic_roots⚠ |
Given a multivariate polynomial |
Z3_algebraic_sign⚠ |
Return 1 if |
Z3_algebraic_sub⚠ |
Return the value |
Z3_app_to_ast⚠ |
Convert a |
Z3_append_log⚠ |
Append user-defined string to interaction log. |
Z3_apply_result_convert_model⚠ |
Convert a model for the subgoal |
Z3_apply_result_dec_ref⚠ |
Decrement the reference counter of the given |
Z3_apply_result_get_num_subgoals⚠ |
Return the number of subgoals in the |
Z3_apply_result_get_subgoal⚠ |
Return one of the subgoals in the |
Z3_apply_result_inc_ref⚠ |
Increment the reference counter of the given |
Z3_apply_result_to_string⚠ |
Convert the |
Z3_ast_map_contains⚠ |
Return true if the map |
Z3_ast_map_dec_ref⚠ |
Decrement the reference counter of the given AST map. |
Z3_ast_map_erase⚠ |
Erase a key from the map. |
Z3_ast_map_find⚠ |
Return the value associated with the key |
Z3_ast_map_inc_ref⚠ |
Increment the reference counter of the given AST map. |
Z3_ast_map_insert⚠ |
Store/Replace a new key, value pair in the given map. |
Z3_ast_map_keys⚠ |
Return the keys stored in the given map. |
Z3_ast_map_reset⚠ |
Remove all keys from the given map. |
Z3_ast_map_size⚠ |
Return the size of the given map. |
Z3_ast_map_to_string⚠ |
Convert the given map into a string. |
Z3_ast_to_string⚠ |
Convert the given AST node into a string. |
Z3_ast_vector_dec_ref⚠ |
Decrement the reference counter of the given AST vector. |
Z3_ast_vector_get⚠ |
Return the AST at position |
Z3_ast_vector_inc_ref⚠ |
Increment the reference counter of the given AST vector. |
Z3_ast_vector_push⚠ |
Add the AST |
Z3_ast_vector_resize⚠ |
Resize the AST vector |
Z3_ast_vector_set⚠ |
Update position |
Z3_ast_vector_size⚠ |
Return the size of the given AST vector. |
Z3_ast_vector_to_string⚠ |
Convert AST vector into a string. |
Z3_ast_vector_translate⚠ |
Translate the AST vector |
Z3_benchmark_to_smtlib_string⚠ |
Convert the given benchmark into SMT-LIB formatted string. |
Z3_check_interpolant⚠ |
Check the correctness of an interpolant. The Z3 context must have no constraints asserted when this call is made. That means that after interpolating, you must first fully pop the Z3 context before calling this. See Z3_interpolate for meaning of parameters. |
Z3_close_log⚠ |
Close interaction log. |
Z3_compute_interpolant⚠ | |
Z3_datatype_update_field⚠ |
Update record field with a value. |
Z3_dec_ref⚠ |
Decrement the reference counter of the given AST.
The context |
Z3_del_config⚠ |
Delete the given configuration object. |
Z3_del_constructor⚠ |
Reclaim memory allocated to constructor. |
Z3_del_constructor_list⚠ |
Reclaim memory allocated for constructor list. |
Z3_del_context⚠ |
Delete the given logical context. |
Z3_disable_trace⚠ |
Disable tracing messages tagged as |
Z3_enable_trace⚠ |
Enable tracing messages tagged as |
Z3_finalize_memory⚠ |
Destroy all allocated resources. |
Z3_fixedpoint_add_cover⚠ |
Add property about the predicate |
Z3_fixedpoint_add_fact⚠ |
Add a Database fact. |
Z3_fixedpoint_add_invariant⚠ |
Add an assumed invariant of predicate |
Z3_fixedpoint_add_rule⚠ |
Add a universal Horn clause as a named rule.
The |
Z3_fixedpoint_assert⚠ |
Assert a constraint to the fixedpoint context. |
Z3_fixedpoint_dec_ref⚠ |
Decrement the reference counter of the given fixedpoint context. |
Z3_fixedpoint_from_file⚠ |
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file. |
Z3_fixedpoint_from_string⚠ |
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string. |
Z3_fixedpoint_get_answer⚠ |
Retrieve a formula that encodes satisfying answers to the query. |
Z3_fixedpoint_get_assertions⚠ |
Retrieve set of background assertions from fixedpoint context. |
Z3_fixedpoint_get_cover_delta⚠ |
Retrieve the current cover of |
Z3_fixedpoint_get_ground_sat_answer⚠ |
Retrieve a bottom-up (from query) sequence of ground facts |
Z3_fixedpoint_get_help⚠ |
Return a string describing all fixedpoint available parameters. |
Z3_fixedpoint_get_num_levels⚠ |
Query the PDR engine for the maximal levels properties are known about predicate. |
Z3_fixedpoint_get_param_descrs⚠ |
Return the parameter description set for the given fixedpoint object. |
Z3_fixedpoint_get_reachable⚠ |
Retrieve reachable states of a predicate. |
Z3_fixedpoint_get_reason_unknown⚠ |
Retrieve a string that describes the last status returned by |
Z3_fixedpoint_get_rule_names_along_trace⚠ |
Obtain the list of rules along the counterexample trace. |
Z3_fixedpoint_get_rules⚠ |
Retrieve set of rules from fixedpoint context. |
Z3_fixedpoint_get_rules_along_trace⚠ |
Obtain the list of rules along the counterexample trace. |
Z3_fixedpoint_get_statistics⚠ |
Retrieve statistics information from the last call to |
Z3_fixedpoint_inc_ref⚠ |
Increment the reference counter of the given fixedpoint context |
Z3_fixedpoint_init⚠ |
Initialize the context with a user-defined state. |
Z3_fixedpoint_pop⚠ |
Backtrack one backtracking point. |
Z3_fixedpoint_push⚠ |
Create a backtracking point. |
Z3_fixedpoint_query⚠ |
Pose a query against the asserted rules. |
Z3_fixedpoint_query_from_lvl⚠ |
Pose a query against the asserted rules at the given level. |
Z3_fixedpoint_query_relations⚠ |
Pose multiple queries against the asserted rules. |
Z3_fixedpoint_register_relation⚠ |
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact. |
Z3_fixedpoint_set_params⚠ |
Set parameters on fixedpoint context. |
Z3_fixedpoint_set_predicate_representation⚠ |
Configure the predicate representation. |
Z3_fixedpoint_set_reduce_app_callback⚠ |
Register a callback for building terms based on the relational operators. |
Z3_fixedpoint_set_reduce_assign_callback⚠ |
Register a callback to destructive updates. |
Z3_fixedpoint_to_string⚠ |
Print the current rules and background axioms as a string. |
Z3_fixedpoint_update_rule⚠ |
Update a named rule. A rule with the same name must have been previously created. |
Z3_fpa_get_ebits⚠ |
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. |
Z3_fpa_get_numeral_exponent_bv⚠ |
Retrieves the exponent of a floating-point literal as a bit-vector expression. |
Z3_fpa_get_numeral_exponent_int64⚠ |
Return the exponent value of a floating-point numeral as a signed 64-bit integer |
Z3_fpa_get_numeral_exponent_string⚠ |
Return the exponent value of a floating-point numeral as a string. |
Z3_fpa_get_numeral_sign⚠ |
Retrieves the sign of a floating-point literal. |
Z3_fpa_get_numeral_sign_bv⚠ |
Retrieves the sign of a floating-point literal as a bit-vector expression. |
Z3_fpa_get_numeral_significand_bv⚠ |
Retrieves the significand of a floating-point literal as a bit-vector expression. |
Z3_fpa_get_numeral_significand_string⚠ |
Return the significand value of a floating-point numeral as a string. |
Z3_fpa_get_numeral_significand_uint64⚠ |
Return the significand value of a floating-point numeral as a uint64. |
Z3_fpa_get_sbits⚠ |
Retrieves the number of bits reserved for the significand in a FloatingPoint sort. |
Z3_fpa_is_numeral_inf⚠ |
Checks whether a given floating-point numeral is a +oo or -oo. |
Z3_fpa_is_numeral_nan⚠ |
Checks whether a given floating-point numeral is a NaN. |
Z3_fpa_is_numeral_negative⚠ |
Checks whether a given floating-point numeral is negative. |
Z3_fpa_is_numeral_normal⚠ |
Checks whether a given floating-point numeral is normal. |
Z3_fpa_is_numeral_positive⚠ |
Checks whether a given floating-point numeral is positive. |
Z3_fpa_is_numeral_subnormal⚠ |
Checks whether a given floating-point numeral is subnormal. |
Z3_fpa_is_numeral_zero⚠ |
Checks whether a given floating-point numeral is +zero or -zero. |
Z3_func_decl_to_ast⚠ |
Convert a |
Z3_func_decl_to_string⚠ | |
Z3_func_entry_dec_ref⚠ |
Decrement the reference counter of the given |
Z3_func_entry_get_arg⚠ |
Return an argument of a |
Z3_func_entry_get_num_args⚠ |
Return the number of arguments in a |
Z3_func_entry_get_value⚠ |
Return the value of this point. |
Z3_func_entry_inc_ref⚠ |
Increment the reference counter of the given |
Z3_func_interp_add_entry⚠ |
add a function entry to a function interpretation. |
Z3_func_interp_dec_ref⚠ |
Decrement the reference counter of the given |
Z3_func_interp_get_arity⚠ |
Return the arity (number of arguments) of the given function interpretation. |
Z3_func_interp_get_else⚠ |
Return the 'else' value of the given function interpretation. |
Z3_func_interp_get_entry⚠ |
Return a "point" of the given function intepretation. It represents the
value of |
Z3_func_interp_get_num_entries⚠ |
Return the number of entries in the given function interpretation. |
Z3_func_interp_inc_ref⚠ |
Increment the reference counter of the given |
Z3_func_interp_set_else⚠ |
Return the 'else' value of the given function interpretation. |
Z3_get_algebraic_number_lower⚠ |
Return a lower bound for the given real algebraic number. |
Z3_get_algebraic_number_upper⚠ |
Return a upper bound for the given real algebraic number. |
Z3_get_app_arg⚠ |
Return the i-th argument of the given application. |
Z3_get_app_decl⚠ |
Return the declaration of a constant or function application. |
Z3_get_app_num_args⚠ |
Return the number of argument of an application. If |
Z3_get_arity⚠ |
Alias for |
Z3_get_array_sort_domain⚠ |
Return the domain of the given array sort. |
Z3_get_array_sort_range⚠ |
Return the range of the given array sort. |
Z3_get_as_array_func_decl⚠ |
Return the function declaration |
Z3_get_ast_hash⚠ |
Return a hash code for the given AST. |
Z3_get_ast_id⚠ |
Return a unique identifier for |
Z3_get_ast_kind⚠ |
Return the kind of the given AST. |
Z3_get_bool_value⚠ |
Return |
Z3_get_bv_sort_size⚠ |
Return the size of the given bit-vector sort. |
Z3_get_datatype_sort_constructor⚠ |
Return idx'th constructor. |
Z3_get_datatype_sort_constructor_accessor⚠ |
Return idx_a'th accessor for the idx_c'th constructor. |
Z3_get_datatype_sort_num_constructors⚠ |
Return number of constructors for datatype. |
Z3_get_datatype_sort_recognizer⚠ |
Return idx'th recognizer. |
Z3_get_decl_ast_parameter⚠ |
Return the expression value associated with an expression parameter. |
Z3_get_decl_double_parameter⚠ |
Return the double value associated with an double parameter. |
Z3_get_decl_func_decl_parameter⚠ |
Return the expression value associated with an expression parameter. |
Z3_get_decl_int_parameter⚠ |
Return the integer value associated with an integer parameter. |
Z3_get_decl_kind⚠ |
Return declaration kind corresponding to declaration. |
Z3_get_decl_name⚠ |
Return the constant declaration name as a symbol. |
Z3_get_decl_num_parameters⚠ |
Return the number of parameters associated with a declaration. |
Z3_get_decl_parameter_kind⚠ |
Return the parameter type associated with a declaration. |
Z3_get_decl_rational_parameter⚠ |
Return the rational value, as a string, associated with a rational parameter. |
Z3_get_decl_sort_parameter⚠ |
Return the sort value associated with a sort parameter. |
Z3_get_decl_symbol_parameter⚠ |
Return the double value associated with an double parameter. |
Z3_get_denominator⚠ |
Return the denominator (as a numeral AST) of a numeral AST of sort Real. |
Z3_get_domain⚠ |
Return the sort of the i-th parameter of the given function declaration. |
Z3_get_domain_size⚠ |
Return the number of parameters of the given declaration. |
Z3_get_error_code⚠ |
Return the error code for the last API call. |
Z3_get_error_msg⚠ |
Return a string describing the given error code. |
Z3_get_error_msg_ex⚠ |
Return a string describing the given error code. |
Z3_get_estimated_alloc_size⚠ |
Return the estimated allocated memory in bytes. |
Z3_get_finite_domain_sort_size⚠ |
Store the size of the sort in |
Z3_get_full_version⚠ |
Return a string that fully describes the version of Z3 in use. |
Z3_get_func_decl_id⚠ |
Return a unique identifier for |
Z3_get_implied_equalities⚠ |
Retrieve congruence class representatives for terms. |
Z3_get_index_value⚠ |
Return index of de-Bruijn bound variable. |
Z3_get_interpolant⚠ |
Compute an interpolant from a refutation. This takes a proof of
"false" from a set of formulas C, and an interpolation
pattern. The pattern pat is a formula combining the formulas in C
using logical conjunction and the "interp" operator (see
|
Z3_get_num_probes⚠ |
Return the number of builtin probes available in Z3. |
Z3_get_num_tactics⚠ |
Return the number of builtin tactics available in Z3. |
Z3_get_numeral_decimal_string⚠ |
Return numeral as a string in decimal notation.
The result has at most |
Z3_get_numeral_int⚠ |
Similar to |
Z3_get_numeral_int64⚠ |
Similar to |
Z3_get_numeral_rational_int64⚠ |
Similar to |
Z3_get_numeral_small⚠ |
Return numeral value, as a pair of 64 bit numbers if the representation fits. |
Z3_get_numeral_string⚠ |
Return numeral value, as a string of a numeric constant term |
Z3_get_numeral_uint⚠ |
Similar to |
Z3_get_numeral_uint64⚠ |
Similar to |
Z3_get_numerator⚠ |
Return the numerator (as a numeral AST) of a numeral AST of sort Real. |
Z3_get_parser_error⚠ |
Retrieve that last error message information generated from parsing. |
Z3_get_pattern⚠ |
Return i'th ast in pattern. |
Z3_get_pattern_num_terms⚠ |
Return number of terms in pattern. |
Z3_get_probe_name⚠ |
Return the name of the i probe. |
Z3_get_quantifier_body⚠ |
Return body of quantifier. |
Z3_get_quantifier_bound_name⚠ |
Return symbol of the i'th bound variable. |
Z3_get_quantifier_bound_sort⚠ |
Return sort of the i'th bound variable. |
Z3_get_quantifier_no_pattern_ast⚠ |
Return i'th no_pattern. |
Z3_get_quantifier_num_bound⚠ |
Return number of bound variables of quantifier. |
Z3_get_quantifier_num_no_patterns⚠ |
Return number of no_patterns used in quantifier. |
Z3_get_quantifier_num_patterns⚠ |
Return number of patterns used in quantifier. |
Z3_get_quantifier_pattern_ast⚠ |
Return i'th pattern. |
Z3_get_quantifier_weight⚠ |
Obtain weight of quantifier. |
Z3_get_range⚠ |
Return the range of the given declaration. |
Z3_get_relation_arity⚠ |
Return arity of relation. |
Z3_get_relation_column⚠ |
Return sort at i'th column of relation sort. |
Z3_get_sort⚠ |
Return the sort of an AST node. |
Z3_get_sort_id⚠ |
Return a unique identifier for |
Z3_get_sort_kind⚠ |
Return the sort kind (e.g., array, tuple, int, bool, etc). |
Z3_get_sort_name⚠ |
Return the sort name as a symbol. |
Z3_get_string⚠ |
Retrieve the string constant stored in |
Z3_get_symbol_int⚠ |
Return the symbol int value. |
Z3_get_symbol_kind⚠ |
Return |
Z3_get_symbol_string⚠ |
Return the symbol name. |
Z3_get_tactic_name⚠ |
Return the name of the idx tactic. |
Z3_get_tuple_sort_field_decl⚠ |
Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort. |
Z3_get_tuple_sort_mk_decl⚠ |
Return the constructor declaration of the given tuple sort. |
Z3_get_tuple_sort_num_fields⚠ |
Return the number of fields of the given tuple sort. |
Z3_get_version⚠ |
Return Z3 version number information. |
Z3_global_param_get⚠ |
Get a global (or module) parameter. |
Z3_global_param_reset_all⚠ |
Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers). |
Z3_global_param_set⚠ |
Set a global (or module) parameter. This setting is shared by all Z3 contexts. |
Z3_goal_assert⚠ |
Add a new formula |
Z3_goal_dec_ref⚠ |
Decrement the reference counter of the given goal. |
Z3_goal_depth⚠ |
Return the depth of the given goal. It tracks how many transformations were applied to it. |
Z3_goal_formula⚠ |
Return a formula from the given goal. |
Z3_goal_inc_ref⚠ |
Increment the reference counter of the given goal. |
Z3_goal_inconsistent⚠ |
Return true if the given goal contains the formula |
Z3_goal_is_decided_sat⚠ |
Return true if the goal is empty, and it is precise or the product of a under approximation. |
Z3_goal_is_decided_unsat⚠ |
Return true if the goal contains false, and it is precise or the product of an over approximation. |
Z3_goal_num_exprs⚠ |
Return the number of formulas, subformulas and terms in the given goal. |
Z3_goal_precision⚠ |
Return the "precision" of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal. |
Z3_goal_reset⚠ |
Erase all formulas from the given goal. |
Z3_goal_size⚠ |
Return the number of formulas in the given goal. |
Z3_goal_to_string⚠ |
Convert a goal into a string. |
Z3_goal_translate⚠ |
Copy a goal |
Z3_inc_ref⚠ |
Increment the reference counter of the given AST.
The context |
Z3_interpolation_profile⚠ |
Return a string summarizing cumulative time used for interpolation. This string is purely for entertainment purposes and has no semantics. |
Z3_interrupt⚠ |
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics. |
Z3_is_algebraic_number⚠ |
Return true if the give AST is a real algebraic number. |
Z3_is_app⚠ | |
Z3_is_as_array⚠ |
The |
Z3_is_eq_ast⚠ |
Compare terms. |
Z3_is_eq_func_decl⚠ |
Compare terms. |
Z3_is_eq_sort⚠ |
compare sorts. |
Z3_is_numeral_ast⚠ | |
Z3_is_quantifier_forall⚠ |
Determine if quantifier is universal. |
Z3_is_re_sort⚠ |
Check if |
Z3_is_seq_sort⚠ |
Check if |
Z3_is_string⚠ |
Determine if |
Z3_is_string_sort⚠ |
Check if |
Z3_is_well_sorted⚠ |
Return true if the given expression |
Z3_mk_add⚠ |
Create an AST node representing |
Z3_mk_and⚠ |
Create an AST node representing |
Z3_mk_app⚠ |
Create a constant or function application. |
Z3_mk_array_default⚠ |
Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value. |
Z3_mk_array_ext⚠ |
Create array extensionality index given two arrays with the same sort. The meaning is given by the axiom: (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B)) |
Z3_mk_array_sort⚠ |
Create an array type. |
Z3_mk_array_sort_n⚠ |
Create an array type with N arguments |
Z3_mk_as_array⚠ |
Create array with the same interpretation as a function. The array satisfies the property (f x) = (select (_ as-array f) x) for every argument x. |
Z3_mk_ast_map⚠ |
Return an empty mapping from AST to AST |
Z3_mk_ast_vector⚠ |
Return an empty AST vector. |
Z3_mk_atleast⚠ |
Pseudo-Boolean relations. |
Z3_mk_atmost⚠ |
Pseudo-Boolean relations. |
Z3_mk_bool_sort⚠ |
Create the Boolean type. |
Z3_mk_bound⚠ |
Create a bound variable. |
Z3_mk_bv2int⚠ |
Create an integer from the bit-vector argument |
Z3_mk_bv_numeral⚠ |
create a bit-vector numeral from a vector of Booleans. |
Z3_mk_bv_sort⚠ |
Create a bit-vector type of the given size. |
Z3_mk_bvadd⚠ |
Standard two's complement addition. |
Z3_mk_bvadd_no_overflow⚠ |
Create a predicate that checks that the bit-wise addition
of |
Z3_mk_bvadd_no_underflow⚠ |
Create a predicate that checks that the bit-wise signed addition
of |
Z3_mk_bvand⚠ |
Bitwise and. |
Z3_mk_bvashr⚠ |
Arithmetic shift right. |
Z3_mk_bvlshr⚠ |
Logical shift right. |
Z3_mk_bvmul⚠ |
Standard two's complement multiplication. |
Z3_mk_bvmul_no_overflow⚠ |
Create a predicate that checks that the bit-wise multiplication
of |
Z3_mk_bvmul_no_underflow⚠ |
Create a predicate that checks that the bit-wise signed multiplication
of |
Z3_mk_bvnand⚠ |
Bitwise nand. |
Z3_mk_bvneg⚠ |
Standard two's complement unary minus. |
Z3_mk_bvneg_no_overflow⚠ |
Check that bit-wise negation does not overflow when
|
Z3_mk_bvnor⚠ |
Bitwise nor. |
Z3_mk_bvnot⚠ |
Bitwise negation. |
Z3_mk_bvor⚠ |
Bitwise or. |
Z3_mk_bvredand⚠ |
Take conjunction of bits in vector, return vector of length 1. |
Z3_mk_bvredor⚠ |
Take disjunction of bits in vector, return vector of length 1. |
Z3_mk_bvsdiv⚠ |
Two's complement signed division. |
Z3_mk_bvsdiv_no_overflow⚠ |
Create a predicate that checks that the bit-wise signed division
of |
Z3_mk_bvsge⚠ |
Two's complement signed greater than or equal to. |
Z3_mk_bvsgt⚠ |
Two's complement signed greater than. |
Z3_mk_bvshl⚠ |
Shift left. |
Z3_mk_bvsle⚠ |
Two's complement signed less than or equal to. |
Z3_mk_bvslt⚠ |
Two's complement signed less than. |
Z3_mk_bvsmod⚠ |
Two's complement signed remainder (sign follows divisor). |
Z3_mk_bvsrem⚠ |
Two's complement signed remainder (sign follows dividend). |
Z3_mk_bvsub⚠ |
Standard two's complement subtraction. |
Z3_mk_bvsub_no_overflow⚠ |
Create a predicate that checks that the bit-wise signed subtraction
of |
Z3_mk_bvsub_no_underflow⚠ |
Create a predicate that checks that the bit-wise subtraction
of |
Z3_mk_bvudiv⚠ |
Unsigned division. |
Z3_mk_bvuge⚠ |
Unsigned greater than or equal to. |
Z3_mk_bvugt⚠ |
Unsigned greater than. |
Z3_mk_bvule⚠ |
Unsigned less than or equal to. |
Z3_mk_bvult⚠ |
Unsigned less than. |
Z3_mk_bvurem⚠ |
Unsigned remainder. |
Z3_mk_bvxnor⚠ |
Bitwise xnor. |
Z3_mk_bvxor⚠ |
Bitwise exclusive-or. |
Z3_mk_concat⚠ |
Concatenate the given bit-vectors. |
Z3_mk_config⚠ |
Create a configuration object for the Z3 context object. |
Z3_mk_const⚠ |
Declare and create a constant. |
Z3_mk_const_array⚠ |
Create the constant array. |
Z3_mk_constructor⚠ |
Create a constructor. |
Z3_mk_constructor_list⚠ |
Create list of constructors. |
Z3_mk_context⚠ |
Create a context using the given configuration. |
Z3_mk_context_rc⚠ |
Create a context using the given configuration.
This function is similar to |
Z3_mk_datatype⚠ |
Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort. |
Z3_mk_datatypes⚠ |
Create mutually recursive datatypes. |
Z3_mk_distinct⚠ |
Create an AST node representing |
Z3_mk_div⚠ |
Create an AST node representing |
Z3_mk_empty_set⚠ |
Create the empty set. |
Z3_mk_enumeration_sort⚠ |
Create a enumeration sort. |
Z3_mk_eq⚠ |
Create an AST node representing |
Z3_mk_exists⚠ |
Create an exists formula. Similar to |
Z3_mk_exists_const⚠ |
Similar to |
Z3_mk_ext_rotate_left⚠ |
Rotate bits of |
Z3_mk_ext_rotate_right⚠ |
Rotate bits of |
Z3_mk_extract⚠ |
Extract the bits |
Z3_mk_false⚠ |
Create an AST node representing |
Z3_mk_finite_domain_sort⚠ |
Create a named finite domain sort. |
Z3_mk_fixedpoint⚠ |
Create a new fixedpoint context. |
Z3_mk_forall⚠ |
Create a forall formula. It takes an expression |
Z3_mk_forall_const⚠ |
Create a universal quantifier using a list of constants that will form the set of bound variables. |
Z3_mk_fpa_abs⚠ |
Floating-point absolute value |
Z3_mk_fpa_add⚠ |
Floating-point addition |
Z3_mk_fpa_div⚠ |
Floating-point division |
Z3_mk_fpa_eq⚠ |
Floating-point equality. |
Z3_mk_fpa_fma⚠ |
Floating-point fused multiply-add. |
Z3_mk_fpa_fp⚠ |
Create an expression of FloatingPoint sort from three bit-vector expressions. |
Z3_mk_fpa_geq⚠ |
Floating-point greater than or equal. |
Z3_mk_fpa_gt⚠ |
Floating-point greater than. |
Z3_mk_fpa_inf⚠ |
Create a floating-point infinity of sort s. |
Z3_mk_fpa_is_infinite⚠ |
Predicate indicating whether t is a floating-point number representing +oo or -oo. |
Z3_mk_fpa_is_nan⚠ |
Predicate indicating whether t is a NaN. |
Z3_mk_fpa_is_negative⚠ |
Predicate indicating whether t is a negative floating-point number. |
Z3_mk_fpa_is_normal⚠ |
Predicate indicating whether t is a normal floating-point number. |
Z3_mk_fpa_is_positive⚠ |
Predicate indicating whether t is a positive floating-point number. |
Z3_mk_fpa_is_subnormal⚠ |
Predicate indicating whether t is a subnormal floating-point number. |
Z3_mk_fpa_is_zero⚠ |
Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero. |
Z3_mk_fpa_leq⚠ |
Floating-point less than or equal. |
Z3_mk_fpa_lt⚠ |
Floating-point less than. |
Z3_mk_fpa_max⚠ |
Maximum of floating-point numbers. |
Z3_mk_fpa_min⚠ |
Minimum of floating-point numbers. |
Z3_mk_fpa_mul⚠ |
Floating-point multiplication |
Z3_mk_fpa_nan⚠ |
Create a floating-point NaN of sort s. |
Z3_mk_fpa_neg⚠ |
Floating-point negation |
Z3_mk_fpa_numeral_double⚠ |
Create a numeral of FloatingPoint sort from a double. |
Z3_mk_fpa_numeral_float⚠ |
Create a numeral of FloatingPoint sort from a float. |
Z3_mk_fpa_numeral_int⚠ |
Create a numeral of FloatingPoint sort from a signed integer. |
Z3_mk_fpa_numeral_int64_uint64⚠ |
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. |
Z3_mk_fpa_numeral_int_uint⚠ |
Create a numeral of FloatingPoint sort from a sign bit and two integers. |
Z3_mk_fpa_rem⚠ |
Floating-point remainder |
Z3_mk_fpa_rna⚠ |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. |
Z3_mk_fpa_rne⚠ |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. |
Z3_mk_fpa_round_nearest_ties_to_away⚠ |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. |
Z3_mk_fpa_round_nearest_ties_to_even⚠ |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. |
Z3_mk_fpa_round_to_integral⚠ |
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number. |
Z3_mk_fpa_round_toward_negative⚠ |
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. |
Z3_mk_fpa_round_toward_positive⚠ |
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. |
Z3_mk_fpa_round_toward_zero⚠ |
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. |
Z3_mk_fpa_rounding_mode_sort⚠ |
Create the RoundingMode sort. |
Z3_mk_fpa_rtn⚠ |
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. |
Z3_mk_fpa_rtp⚠ |
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. |
Z3_mk_fpa_rtz⚠ |
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. |
Z3_mk_fpa_sort⚠ |
Create a FloatingPoint sort. |
Z3_mk_fpa_sort_16⚠ |
Create the half-precision (16-bit) FloatingPoint sort. |
Z3_mk_fpa_sort_32⚠ |
Create the single-precision (32-bit) FloatingPoint sort. |
Z3_mk_fpa_sort_64⚠ |
Create the double-precision (64-bit) FloatingPoint sort. |
Z3_mk_fpa_sort_128⚠ |
Create the quadruple-precision (128-bit) FloatingPoint sort. |
Z3_mk_fpa_sort_double⚠ |
Create the double-precision (64-bit) FloatingPoint sort. |
Z3_mk_fpa_sort_half⚠ |
Create the half-precision (16-bit) FloatingPoint sort. |
Z3_mk_fpa_sort_quadruple⚠ |
Create the quadruple-precision (128-bit) FloatingPoint sort. |
Z3_mk_fpa_sort_single⚠ |
Create the single-precision (32-bit) FloatingPoint sort. |
Z3_mk_fpa_sqrt⚠ |
Floating-point square root |
Z3_mk_fpa_sub⚠ |
Floating-point subtraction |
Z3_mk_fpa_to_fp_bv⚠ |
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. |
Z3_mk_fpa_to_fp_float⚠ |
Conversion of a FloatingPoint term into another term of different FloatingPoint sort. |
Z3_mk_fpa_to_fp_int_real⚠ |
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. |
Z3_mk_fpa_to_fp_real⚠ |
Conversion of a term of real sort into a term of FloatingPoint sort. |
Z3_mk_fpa_to_fp_signed⚠ |
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. |
Z3_mk_fpa_to_fp_unsigned⚠ |
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort. |
Z3_mk_fpa_to_ieee_bv⚠ |
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. |
Z3_mk_fpa_to_real⚠ |
Conversion of a floating-point term into a real-numbered term. |
Z3_mk_fpa_to_sbv⚠ |
Conversion of a floating-point term into a signed bit-vector. |
Z3_mk_fpa_to_ubv⚠ |
Conversion of a floating-point term into an unsigned bit-vector. |
Z3_mk_fpa_zero⚠ |
Create a floating-point zero of sort s. |
Z3_mk_fresh_const⚠ |
Declare and create a fresh constant. |
Z3_mk_fresh_func_decl⚠ |
Declare a fresh constant or function. |
Z3_mk_full_set⚠ |
Create the full set. |
Z3_mk_func_decl⚠ |
Declare a constant or function. |
Z3_mk_ge⚠ |
Create greater than or equal to. |
Z3_mk_goal⚠ |
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. |
Z3_mk_gt⚠ |
Create greater than. |
Z3_mk_iff⚠ |
Create an AST node representing |
Z3_mk_implies⚠ |
Create an AST node representing |
Z3_mk_int⚠ |
Create a numeral of an int, bit-vector, or finite-domain sort. |
Z3_mk_int64⚠ |
Create a numeral of a int, bit-vector, or finite-domain sort. |
Z3_mk_int2bv⚠ |
Create an |
Z3_mk_int2real⚠ |
Coerce an integer to a real. |
Z3_mk_int_sort⚠ |
Create the integer type. |
Z3_mk_int_symbol⚠ |
Create a Z3 symbol using an integer. |
Z3_mk_int_to_str⚠ |
Integer to string conversion. |
Z3_mk_interpolant⚠ |
Create an AST node marking a formula position for interpolation. |
Z3_mk_interpolation_context⚠ |
This function generates a Z3 context suitable for generation of interpolants. Formulas can be generated as abstract syntax trees in this context using the Z3 C API. |
Z3_mk_is_int⚠ |
Check if a real number is an integer. |
Z3_mk_ite⚠ |
Create an AST node representing an if-then-else: |
Z3_mk_le⚠ |
Create less than or equal to. |
Z3_mk_list_sort⚠ |
Create a list sort |
Z3_mk_lt⚠ |
Create less than. |
Z3_mk_map⚠ |
Map f on the argument arrays. |
Z3_mk_mod⚠ |
Create an AST node representing |
Z3_mk_model⚠ |
Create a fresh model object. It has reference count 0. |
Z3_mk_mul⚠ |
Create an AST node representing |
Z3_mk_not⚠ |
Create an AST node representing |
Z3_mk_numeral⚠ |
Create a numeral of a given sort. |
Z3_mk_optimize⚠ |
Create a new optimize context. |
Z3_mk_or⚠ |
Create an AST node representing |
Z3_mk_params⚠ |
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc. |
Z3_mk_pattern⚠ |
Create a pattern for quantifier instantiation. |
Z3_mk_pbeq⚠ |
Pseudo-Boolean relations. |
Z3_mk_pbge⚠ |
Pseudo-Boolean relations. |
Z3_mk_pble⚠ |
Pseudo-Boolean relations. |
Z3_mk_power⚠ |
Create an AST node representing |
Z3_mk_probe⚠ |
Return a probe associated with the given name.
The complete list of probes may be obtained using the procedures |
Z3_mk_quantifier⚠ |
Create a quantifier - universal or existential, with pattern hints.
See the documentation for |
Z3_mk_quantifier_const⚠ |
Create a universal or existential quantifier using a list of constants that will form the set of bound variables. |
Z3_mk_quantifier_const_ex⚠ |
Create a universal or existential quantifier using a list of constants that will form the set of bound variables. |
Z3_mk_quantifier_ex⚠ |
Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes |
Z3_mk_re_complement⚠ |
Create the complement of the regular language |
Z3_mk_re_concat⚠ |
Create the concatenation of the regular languages. |
Z3_mk_re_empty⚠ |
Create an empty regular expression of sort |
Z3_mk_re_full⚠ |
Create an universal regular expression of sort |
Z3_mk_re_intersect⚠ |
Create the intersection of the regular languages. |
Z3_mk_re_loop⚠ |
Create a regular expression loop. The supplied regular expression |
Z3_mk_re_option⚠ |
Create the regular language ``[re]. |
Z3_mk_re_plus⚠ |
Create the regular language |
Z3_mk_re_range⚠ |
Create the range regular expression over two sequences of length 1. |
Z3_mk_re_sort⚠ |
Create a regular expression sort out of a sequence sort. |
Z3_mk_re_star⚠ |
Create the regular language |
Z3_mk_re_union⚠ |
Create the union of the regular languages. |
Z3_mk_real⚠ |
Create a real from a fraction. |
Z3_mk_real2int⚠ |
Coerce a real to an integer. |
Z3_mk_real_sort⚠ |
Create the real type. |
Z3_mk_rem⚠ |
Create an AST node representing |
Z3_mk_repeat⚠ |
Repeat the given bit-vector up length |
Z3_mk_rotate_left⚠ |
Rotate bits of |
Z3_mk_rotate_right⚠ |
Rotate bits of |
Z3_mk_select⚠ |
Array read.
The argument |
Z3_mk_select_n⚠ |
n-ary Array read.
The argument |
Z3_mk_seq_at⚠ |
Retrieve from |
Z3_mk_seq_concat⚠ |
Concatenate sequences. |
Z3_mk_seq_contains⚠ |
Check if |
Z3_mk_seq_empty⚠ |
Create an empty sequence of the sequence sort |
Z3_mk_seq_extract⚠ |
Extract subsequence starting at |
Z3_mk_seq_in_re⚠ |
Check if |
Z3_mk_seq_index⚠ |
Return index of first occurrence of |
Z3_mk_seq_length⚠ |
Return the length of the sequence |
Z3_mk_seq_prefix⚠ |
Check if |
Z3_mk_seq_replace⚠ |
Replace the first occurrence of |
Z3_mk_seq_sort⚠ |
Create a sequence sort out of the sort for the elements. |
Z3_mk_seq_suffix⚠ |
Check if |
Z3_mk_seq_to_re⚠ |
Create a regular expression that accepts the sequence |
Z3_mk_seq_unit⚠ |
Create a unit sequence of |
Z3_mk_set_add⚠ |
Add an element to a set. |
Z3_mk_set_complement⚠ |
Take the complement of a set. |
Z3_mk_set_del⚠ |
Remove an element to a set. |
Z3_mk_set_difference⚠ |
Take the set difference between two sets. |
Z3_mk_set_intersect⚠ |
Take the intersection of a list of sets. |
Z3_mk_set_member⚠ |
Check for set membership. |
Z3_mk_set_sort⚠ |
Create Set type. |
Z3_mk_set_subset⚠ |
Check for subsetness of sets. |
Z3_mk_set_union⚠ |
Take the union of a list of sets. |
Z3_mk_sign_ext⚠ |
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of
size |
Z3_mk_simple_solver⚠ |
Create a new incremental solver. |
Z3_mk_solver⚠ |
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally uses a non-incremental (solver1) and an incremental solver (solver2). This combined solver changes its behaviour based on how it is used and how its parameters are set. |
Z3_mk_solver_for_logic⚠ |
Create a new solver customized for the given logic.
It behaves like |
Z3_mk_solver_from_tactic⚠ |
Create a new solver that is implemented using the given tactic.
The solver supports the commands |
Z3_mk_store⚠ |
Array update. |
Z3_mk_store_n⚠ |
n-ary Array update. |
Z3_mk_str_to_int⚠ |
Convert string to integer. |
Z3_mk_string⚠ |
Create a string constant out of the string that is passed in |
Z3_mk_string_sort⚠ |
Create a sort for 8 bit strings. |
Z3_mk_string_symbol⚠ |
Create a Z3 symbol using a C string. |
Z3_mk_sub⚠ |
Create an AST node representing |
Z3_mk_tactic⚠ |
Return a tactic associated with the given name. |
Z3_mk_true⚠ |
Create an AST node representing |
Z3_mk_tuple_sort⚠ |
Create a tuple type. |
Z3_mk_unary_minus⚠ |
Create an AST node representing |
Z3_mk_uninterpreted_sort⚠ |
Create a free (uninterpreted) type using the given name (symbol). |
Z3_mk_unsigned_int⚠ |
Create a numeral of a int, bit-vector, or finite-domain sort. |
Z3_mk_unsigned_int64⚠ |
Create a numeral of a int, bit-vector, or finite-domain sort. |
Z3_mk_xor⚠ |
Create an AST node representing |
Z3_mk_zero_ext⚠ |
Extend the given bit-vector with zeros to the (unsigned) equivalent
bit-vector of size |
Z3_model_dec_ref⚠ |
Decrement the reference counter of the given model. |
Z3_model_eval⚠ |
Evaluate the AST node |
Z3_model_extrapolate⚠ |
Extrapolates a model of a formula |
Z3_model_get_const_decl⚠ |
Return the i-th constant in the given model. |
Z3_model_get_const_interp⚠ |
Return the interpretation (i.e., assignment) of constant |
Z3_model_get_func_decl⚠ |
Return the declaration of the i-th function in the given model. |
Z3_model_get_func_interp⚠ |
Return the interpretation of the function |
Z3_model_get_num_consts⚠ |
Return the number of constants assigned by the given model. |
Z3_model_get_num_funcs⚠ |
Return the number of function interpretations in the given model. |
Z3_model_get_num_sorts⚠ |
Return the number of uninterpreted sorts that |
Z3_model_get_sort⚠ |
Return a uninterpreted sort that |
Z3_model_get_sort_universe⚠ |
Return the finite set of distinct values that represent the interpretation for sort |
Z3_model_has_interp⚠ |
Test if there exists an interpretation (i.e., assignment) for |
Z3_model_inc_ref⚠ |
Increment the reference counter of the given model. |
Z3_model_to_string⚠ |
Convert the given model into a string. |
Z3_open_log⚠ |
Log interaction to a file. |
Z3_optimize_assert⚠ |
Assert hard constraint to the optimization context. |
Z3_optimize_assert_soft⚠ |
Assert soft constraint to the optimization context. |
Z3_optimize_check⚠ |
Check consistency and produce optimal values. |
Z3_optimize_dec_ref⚠ |
Decrement the reference counter of the given optimize context. |
Z3_optimize_from_file⚠ |
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context. |
Z3_optimize_from_string⚠ |
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context. |
Z3_optimize_get_assertions⚠ |
Return the set of asserted formulas on the optimization context. |
Z3_optimize_get_help⚠ |
Return a string containing a description of parameters accepted by optimize. |
Z3_optimize_get_lower⚠ |
Retrieve lower bound value or approximation for the i'th optimization objective. |
Z3_optimize_get_lower_as_vector⚠ |
Retrieve lower bound value or approximation for the i'th optimization objective.
The returned vector is of length 3. It always contains numerals.
The three numerals are coefficients a, b, c and encode the result of |
Z3_optimize_get_model⚠ |
Retrieve the model for the last |
Z3_optimize_get_objectives⚠ |
Return objectives on the optimization context. If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...) If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective. |
Z3_optimize_get_param_descrs⚠ |
Return the parameter description set for the given optimize object. |
Z3_optimize_get_reason_unknown⚠ |
Retrieve a string that describes the last status returned by |
Z3_optimize_get_statistics⚠ |
Retrieve statistics information from the last call to |
Z3_optimize_get_upper⚠ |
Retrieve upper bound value or approximation for the i'th optimization objective. |
Z3_optimize_get_upper_as_vector⚠ |
Retrieve upper bound value or approximation for the i'th optimization objective. |
Z3_optimize_inc_ref⚠ |
Increment the reference counter of the given optimize context |
Z3_optimize_maximize⚠ |
Add a maximization constraint. |
Z3_optimize_minimize⚠ |
Add a minimization constraint. |
Z3_optimize_pop⚠ |
Backtrack one level. |
Z3_optimize_push⚠ |
Create a backtracking point. |
Z3_optimize_set_params⚠ |
Set parameters on optimization context. |
Z3_optimize_to_string⚠ |
Print the current context as a string. |
Z3_param_descrs_dec_ref⚠ |
Decrement the reference counter of the given parameter description set. |
Z3_param_descrs_get_documentation⚠ |
Retrieve documentation string corresponding to parameter name |
Z3_param_descrs_get_kind⚠ |
Return the kind associated with the given parameter name |
Z3_param_descrs_get_name⚠ |
Return the number of parameters in the given parameter description set. |
Z3_param_descrs_inc_ref⚠ |
Increment the reference counter of the given parameter description set. |
Z3_param_descrs_size⚠ |
Return the number of parameters in the given parameter description set. |
Z3_param_descrs_to_string⚠ |
Convert a parameter description set into a string. This function is mainly used for printing the contents of a parameter description set. |
Z3_params_dec_ref⚠ |
Decrement the reference counter of the given parameter set. |
Z3_params_inc_ref⚠ |
Increment the reference counter of the given parameter set. |
Z3_params_set_bool⚠ |
Add a Boolean parameter |
Z3_params_set_double⚠ |
Add a double parameter |
Z3_params_set_symbol⚠ |
Add a symbol parameter |
Z3_params_set_uint⚠ |
Add a unsigned parameter |
Z3_params_to_string⚠ |
Convert a parameter set into a string. This function is mainly used for printing the contents of a parameter set. |
Z3_params_validate⚠ |
Validate the parameter set |
Z3_parse_smtlib2_file⚠ |
Similar to |
Z3_parse_smtlib2_string⚠ |
Parse the given string using the SMT-LIB2 parser. |
Z3_pattern_to_ast⚠ |
Convert a |
Z3_pattern_to_string⚠ | |
Z3_polynomial_subresultants⚠ |
Return the nonzero subresultants of |
Z3_probe_and⚠ |
Return a probe that evaluates to "true" when |
Z3_probe_apply⚠ |
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. |
Z3_probe_const⚠ |
Return a probe that always evaluates to val. |
Z3_probe_dec_ref⚠ |
Decrement the reference counter of the given probe. |
Z3_probe_eq⚠ |
Return a probe that evaluates to "true" when the value returned by |
Z3_probe_ge⚠ |
Return a probe that evaluates to "true" when the value returned by |
Z3_probe_get_descr⚠ |
Return a string containing a description of the probe with the given name. |
Z3_probe_gt⚠ |
Return a probe that evaluates to "true" when the value returned by |
Z3_probe_inc_ref⚠ |
Increment the reference counter of the given probe. |
Z3_probe_le⚠ |
Return a probe that evaluates to "true" when the value returned by |
Z3_probe_lt⚠ |
Return a probe that evaluates to "true" when the value returned by |
Z3_probe_not⚠ |
Return a probe that evaluates to "true" when |
Z3_probe_or⚠ |
Return a probe that evaluates to "true" when |
Z3_qe_lite⚠ |
Best-effort quantifier elimination |
Z3_qe_model_project⚠ |
Project variables given a model |
Z3_qe_model_project_skolem⚠ |
Project variables given a model |
Z3_query_constructor⚠ |
Query constructor for declared functions. |
Z3_rcf_add⚠ |
Return the value a + b. |
Z3_rcf_del⚠ |
Delete a RCF numeral created using the RCF API. |
Z3_rcf_div⚠ |
Return the value a / b. |
Z3_rcf_eq⚠ |
Return |
Z3_rcf_ge⚠ |
Return |
Z3_rcf_get_numerator_denominator⚠ |
Extract the "numerator" and "denominator" of the given RCF numeral. |
Z3_rcf_gt⚠ |
Return |
Z3_rcf_inv⚠ |
Return the value 1/a |
Z3_rcf_le⚠ |
Return |
Z3_rcf_lt⚠ |
Return |
Z3_rcf_mk_e⚠ |
Return e (Euler's constant) |
Z3_rcf_mk_infinitesimal⚠ |
Return a new infinitesimal that is smaller than all elements in the Z3 field. |
Z3_rcf_mk_pi⚠ |
Return Pi |
Z3_rcf_mk_rational⚠ |
Return a RCF rational using the given string. |
Z3_rcf_mk_roots⚠ |
Store in roots the roots of the polynomial |
Z3_rcf_mk_small_int⚠ |
Return a RCF small integer. |
Z3_rcf_mul⚠ |
Return the value a * b. |
Z3_rcf_neg⚠ |
Return the value -a |
Z3_rcf_neq⚠ |
Return |
Z3_rcf_num_to_decimal_string⚠ |
Convert the RCF numeral into a string in decimal notation. |
Z3_rcf_num_to_string⚠ |
Convert the RCF numeral into a string. |
Z3_rcf_power⚠ |
Return the value a^k |
Z3_rcf_sub⚠ |
Return the value a - b. |
Z3_read_interpolation_problem⚠ |
Read an interpolation problem from file. |
Z3_reset_memory⚠ |
Reset all allocated resources. |
Z3_set_ast_print_mode⚠ |
Select mode for the format used for pretty-printing AST nodes. |
Z3_set_error⚠ |
Set an error. |
Z3_set_error_handler⚠ |
Register a Z3 error handler. |
Z3_set_param_value⚠ |
Set a configuration parameter. |
Z3_simplify⚠ |
Interface to simplifier. |
Z3_simplify_ex⚠ |
Interface to simplifier. |
Z3_simplify_get_help⚠ |
Return a string describing all available parameters. |
Z3_simplify_get_param_descrs⚠ |
Return the parameter description set for the simplify procedure. |
Z3_solver_assert⚠ |
Assert a constraint into the solver. |
Z3_solver_assert_and_track⚠ |
Assert a constraint |
Z3_solver_check⚠ |
Check whether the assertions in a given solver are consistent or not. |
Z3_solver_check_assumptions⚠ |
Check whether the assertions in the given solver and optional assumptions are consistent or not. |
Z3_solver_dec_ref⚠ |
Decrement the reference counter of the given solver. |
Z3_solver_from_file⚠ |
load solver assertions from a file. |
Z3_solver_from_string⚠ |
load solver assertions from a string. |
Z3_solver_get_assertions⚠ |
Return the set of asserted formulas on the solver. |
Z3_solver_get_consequences⚠ |
retrieve consequences from solver that determine values of the supplied function symbols. |
Z3_solver_get_help⚠ |
Return a string describing all solver available parameters. |
Z3_solver_get_model⚠ |
Retrieve the model for the last |
Z3_solver_get_num_scopes⚠ |
Return the number of backtracking points. |
Z3_solver_get_param_descrs⚠ |
Return the parameter description set for the given solver object. |
Z3_solver_get_proof⚠ |
Retrieve the proof for the last |
Z3_solver_get_reason_unknown⚠ |
Return a brief justification for an "unknown" result (i.e., |
Z3_solver_get_statistics⚠ |
Return statistics for the given solver. |
Z3_solver_get_unsat_core⚠ |
Retrieve the unsat core for the last |
Z3_solver_inc_ref⚠ |
Increment the reference counter of the given solver. |
Z3_solver_pop⚠ |
Backtrack |
Z3_solver_push⚠ |
Create a backtracking point. |
Z3_solver_reset⚠ |
Remove all assertions from the solver. |
Z3_solver_set_params⚠ |
Set the given solver using the given parameters. |
Z3_solver_to_string⚠ |
Convert a solver into a string. |
Z3_solver_translate⚠ |
Copy a solver |
Z3_sort_to_ast⚠ |
Convert a |
Z3_sort_to_string⚠ | |
Z3_stats_dec_ref⚠ |
Decrement the reference counter of the given statistics object. |
Z3_stats_get_double_value⚠ |
Return the double value of the given statistical data. |
Z3_stats_get_key⚠ |
Return the key (a string) for a particular statistical data. |
Z3_stats_get_uint_value⚠ |
Return the unsigned value of the given statistical data. |
Z3_stats_inc_ref⚠ |
Increment the reference counter of the given statistics object. |
Z3_stats_is_double⚠ |
Return |
Z3_stats_is_uint⚠ |
Return |
Z3_stats_size⚠ |
Return the number of statistical data in |
Z3_stats_to_string⚠ |
Convert a statistics into a string. |
Z3_substitute⚠ |
Substitute every occurrence of |
Z3_substitute_vars⚠ |
Substitute the free variables in |
Z3_tactic_and_then⚠ |
Return a tactic that applies |
Z3_tactic_apply⚠ |
Apply tactic |
Z3_tactic_apply_ex⚠ |
Apply tactic |
Z3_tactic_cond⚠ |
Return a tactic that applies |
Z3_tactic_dec_ref⚠ |
Decrement the reference counter of the given tactic. |
Z3_tactic_fail⚠ |
Return a tactic that always fails. |
Z3_tactic_fail_if⚠ |
Return a tactic that fails if the probe |
Z3_tactic_fail_if_not_decided⚠ |
Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false). |
Z3_tactic_get_descr⚠ |
Return a string containing a description of the tactic with the given name. |
Z3_tactic_get_help⚠ |
Return a string containing a description of parameters accepted by the given tactic. |
Z3_tactic_get_param_descrs⚠ |
Return the parameter description set for the given tactic object. |
Z3_tactic_inc_ref⚠ |
Increment the reference counter of the given tactic. |
Z3_tactic_or_else⚠ |
Return a tactic that first applies |
Z3_tactic_par_and_then⚠ |
Return a tactic that applies |
Z3_tactic_par_or⚠ |
Return a tactic that applies the given tactics in parallel. |
Z3_tactic_repeat⚠ |
Return a tactic that keeps applying |
Z3_tactic_skip⚠ |
Return a tactic that just return the given goal. |
Z3_tactic_try_for⚠ |
Return a tactic that applies |
Z3_tactic_using_params⚠ |
Return a tactic that applies |
Z3_tactic_when⚠ |
Return a tactic that applies |
Z3_to_app⚠ |
Convert an |
Z3_to_func_decl⚠ |
Convert an AST into a |
Z3_toggle_warning_messages⚠ |
Enable/disable printing warning messages to the console. |
Z3_translate⚠ |
Translate/Copy the AST |
Z3_update_param_value⚠ |
Set a value of a context parameter. |
Z3_update_term⚠ |
Update the arguments of term |
Z3_write_interpolation_problem⚠ |
Write an interpolation problem to file suitable for reading with Z3_read_interpolation_problem. The output file is a sequence of SMT-LIB2 format commands, suitable for reading with command-line Z3 or other interpolating solvers. |
Type Definitions
Z3_app |
Kind of AST used to represent function applications. |
Z3_apply_result |
Collection of subgoals resulting from applying of a tactic to a goal. |
Z3_ast |
Abstract Syntax Tree node. That is, the data structure used in Z3 to represent terms, formulas, and types. |
Z3_ast_map | |
Z3_ast_vector |
Vector of |
Z3_bool |
Z3 Boolean type. It is just an alias for |
Z3_config |
Configuration object used to initialize logical contexts. |
Z3_constructor |
Type constructor for a (recursive) datatype. |
Z3_constructor_list |
List of constructors for a (recursive) datatype. |
Z3_context |
Manager of all other Z3 objects, global configuration options, etc. |
Z3_error_handler |
Z3 custom error handler (See |
Z3_fixedpoint |
Context for the recursive predicate solver. |
Z3_fixedpoint_reduce_app_callback_fptr | |
Z3_fixedpoint_reduce_assign_callback_fptr |
The following utilities allows adding user-defined domains. |
Z3_func_decl |
Kind of AST used to represent function symbols. |
Z3_func_entry |
Representation of the value of a
|
Z3_func_interp |
Interpretation of a function in a model. |
Z3_goal |
Set of formulas that can be solved and/or transformed using tactics and solvers. |
Z3_lbool |
Lifted Boolean type: |
Z3_literals | |
Z3_model |
Model for the constraints inserted into the logical context. |
Z3_optimize |
Context for solving optimization queries. |
Z3_param_descrs |
Provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters. |
Z3_params |
Parameter set used to configure many components such as: simplifiers, tactics, solvers, etc. |
Z3_pattern |
Kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation. |
Z3_probe |
Function/predicate used to inspect a goal and collect information that may be used to decide which solver and/or preprocessing step will be used. |
Z3_rcf_num | |
Z3_solver |
(Incremental) solver, possibly specialized by a particular tactic or logic. |
Z3_sort |
Kind of AST used to represent types. |
Z3_stats |
Statistical data for a solver. |
Z3_string |
Z3 string type. It is just an alias for |
Z3_string_ptr | |
Z3_symbol |
Lisp-like symbol used to name types, constants, and functions. A symbol can be created using string or integers. |
Z3_tactic |
Basic building block for creating custom solvers for specific problem domains. |