Z3
Deprecated List
Global Z3_assert_cnstr (Z3_context c, Z3_ast a)
Subsumed by Z3_solver_assert
Global Z3_block_literals (Z3_context c, Z3_literals lbls)
This procedure is based on the old Solver API.
Global Z3_check (Z3_context c)
Subsumed by Z3_solver_check
Global Z3_check_and_get_model (Z3_context c, Z3_model *m)
Subsumed by Z3_solver_check
Global Z3_check_assumptions (Z3_context c, unsigned num_assumptions, Z3_ast const assumptions[], Z3_model *m, Z3_ast *proof, unsigned *core_size, Z3_ast core[])
Subsumed by Z3_solver_check_assumptions
Global Z3_context_to_string (Z3_context c)
This method is obsolete. It just displays the internal representation of the global solver available for backward compatibility reasons.
Global Z3_del_literals (Z3_context c, Z3_literals lbls)
This procedure is based on the old Solver API.
Global Z3_del_model (Z3_context c, Z3_model m)
Subsumed by Z3_solver API
Global Z3_disable_literal (Z3_context c, Z3_literals lbls, unsigned idx)
This procedure is based on the old Solver API.
Global Z3_eval (Z3_context c, Z3_model m, Z3_ast t, Z3_ast *v)
Use Z3_model_eval
Global Z3_eval_decl (Z3_context c, Z3_model m, Z3_func_decl d, unsigned num_args, Z3_ast const args[], Z3_ast *v)
Consider using Z3_model_eval and Z3_substitute_vars
Global Z3_eval_func_decl (Z3_context c, Z3_model m, Z3_func_decl decl, Z3_ast *v)
Consider using Z3_model_eval or Z3_model_get_func_interp
Global Z3_get_array_value (Z3_context c, Z3_model m, Z3_ast v, unsigned num_entries, Z3_ast indices[], Z3_ast values[], Z3_ast *else_value)
Use Z3_func_interp objects and Z3_get_as_array_func_decl
Global Z3_get_context_assignment (Z3_context c)
This method is based on the old solver API.
Global Z3_get_error_msg (Z3_error_code err)
Use Z3_get_error_msg_ex instead.
Global Z3_get_guessed_literals (Z3_context c)
This procedure is based on the old Solver API.
Global Z3_get_implied_equalities (Z3_context c, Z3_solver s, unsigned num_terms, Z3_ast const terms[], unsigned class_ids[])
To be moved outside of API.
Global Z3_get_label_symbol (Z3_context c, Z3_literals lbls, unsigned idx)
This procedure is based on the old Solver API.
Global Z3_get_literal (Z3_context c, Z3_literals lbls, unsigned idx)
This procedure is based on the old Solver API.
Global Z3_get_model_constant (Z3_context c, Z3_model m, unsigned i)
use Z3_model_get_const_decl
Global Z3_get_model_func_decl (Z3_context c, Z3_model m, unsigned i)
use Z3_model_get_func_decl
Global Z3_get_model_func_else (Z3_context c, Z3_model m, unsigned i)
Use Z3_func_interp objects
Global Z3_get_model_func_entry_arg (Z3_context c, Z3_model m, unsigned i, unsigned j, unsigned k)
Use Z3_func_interp objects
Global Z3_get_model_func_entry_num_args (Z3_context c, Z3_model m, unsigned i, unsigned j)
Use Z3_func_interp objects
Global Z3_get_model_func_entry_value (Z3_context c, Z3_model m, unsigned i, unsigned j)
Use Z3_func_interp objects
Global Z3_get_model_func_num_entries (Z3_context c, Z3_model m, unsigned i)
Use Z3_func_interp objects
Global Z3_get_model_num_constants (Z3_context c, Z3_model m)
use Z3_model_get_num_consts
Global Z3_get_model_num_funcs (Z3_context c, Z3_model m)
use Z3_model_get_num_funcs
Global Z3_get_num_literals (Z3_context c, Z3_literals lbls)
This procedure is based on the old Solver API.
Global Z3_get_num_scopes (Z3_context c)
Subsumed by Z3_solver_get_num_scopes.
Global Z3_get_relevant_labels (Z3_context c)
This procedure is based on the old Solver API.
Global Z3_get_relevant_literals (Z3_context c)
This procedure is based on the old Solver API.
Global Z3_get_search_failure (Z3_context c)
Subsumed by Z3_solver_get_reason_unknown
Global Z3_is_array_value (Z3_context c, Z3_model m, Z3_ast v, unsigned *num_entries)
Use Z3_is_as_array
Global Z3_mk_context (Z3_config c)
Use Z3_mk_context_rc
Global Z3_mk_injective_function (Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
This method just asserts a (universally quantified) formula that asserts that the new function is injective. It is compatible with the old interface for solving: Z3_assert_cnstr, Z3_check_assumptions, etc.
Global Z3_mk_label (Z3_context c, Z3_symbol s, Z3_bool is_pos, Z3_ast f)
Labels are only supported by the old Solver API. This feature is not essential (it can be simulated using auxiliary Boolean variables). It is only available for backward compatibility.
Global Z3_persist_ast (Z3_context c, Z3_ast a, unsigned num_scopes)
Z3 users should move to Z3_mk_context_rc and use the reference counting APIs for managing AST nodes.
Global Z3_pop (Z3_context c, unsigned num_scopes)
Subsumed by Z3_solver_pop
Global Z3_push (Z3_context c)
Subsumed by Z3_solver_push
Global Z3_set_logic (Z3_context c, Z3_string logic)
Subsumed by Z3_mk_solver_for_logic
Global Z3_soft_check_cancel (Z3_context c)
Use Z3_interrupt instead.
Global Z3_statistics_to_string (Z3_context c)
This method is based on the old solver API. Use Z3_stats_to_string when using the new solver API.