Z3
Deprecated List
globalScope> Global Z3_assert_cnstr (__in Z3_context c, __in Z3_ast a)
Subsumed by Z3_solver_assert
globalScope> Global Z3_block_literals (__in Z3_context c, __in Z3_literals lbls)
This procedure is based on the old Solver API.
globalScope> Global Z3_check (__in Z3_context c)
Subsumed by Z3_solver_check
globalScope> Global Z3_check_and_get_model (__in Z3_context c, __out Z3_model *m)
Subsumed by Z3_solver_check
globalScope> Global Z3_check_assumptions (__in Z3_context c, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[], __out Z3_model *m, __out Z3_ast *proof, __inout unsigned *core_size, __inout_ecount(num_assumptions) Z3_ast core[])
Subsumed by Z3_solver_check_assumptions
globalScope> Global Z3_context_to_string (__in Z3_context c)
This method is obsolete. It just displays the internal representation of the global solver available for backward compatibility reasons.
globalScope> Global Z3_del_literals (__in Z3_context c, __in Z3_literals lbls)
This procedure is based on the old Solver API.
globalScope> Global Z3_del_model (__in Z3_context c, __in Z3_model m)
Subsumed by Z3_solver API
globalScope> Global Z3_disable_literal (__in Z3_context c, __in Z3_literals lbls, __in unsigned idx)
This procedure is based on the old Solver API.
globalScope> Global Z3_eval (__in Z3_context c, __in Z3_model m, __in Z3_ast t, __out Z3_ast *v)
Use Z3_model_eval
globalScope> Global Z3_eval_decl (__in Z3_context c, __in Z3_model m, __in Z3_func_decl d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[], __out Z3_ast *v)
Consider using Z3_model_eval and Z3_substitute_vars
globalScope> Global Z3_eval_func_decl (__in Z3_context c, __in Z3_model m, __in Z3_func_decl decl, __out Z3_ast *v)
Consider using Z3_model_eval or Z3_model_get_func_interp
globalScope> Global Z3_get_array_value (__in Z3_context c, __in Z3_model m, __in Z3_ast v, __in unsigned num_entries, __inout_ecount(num_entries) Z3_ast indices[], __inout_ecount(num_entries) Z3_ast values[], __out Z3_ast *else_value)
Use Z3_func_interp objects and Z3_get_as_array_func_decl
globalScope> Global Z3_get_context_assignment (__in Z3_context c)
This method is based on the old solver API.
globalScope> Global Z3_get_error_msg (__in Z3_error_code err)
Use Z3_get_error_msg_ex instead.
globalScope> Global Z3_get_guessed_literals (__in Z3_context c)
This procedure is based on the old Solver API.
globalScope> Global Z3_get_implied_equalities (__in Z3_context c, __in Z3_solver s, __in unsigned num_terms, __in_ecount(num_terms) Z3_ast const terms[], __out_ecount(num_terms) unsigned class_ids[])
To be moved outside of API.
globalScope> Global Z3_get_label_symbol (__in Z3_context c, __in Z3_literals lbls, __in unsigned idx)
This procedure is based on the old Solver API.
globalScope> Global Z3_get_literal (__in Z3_context c, __in Z3_literals lbls, __in unsigned idx)
This procedure is based on the old Solver API.
globalScope> Global Z3_get_model_constant (__in Z3_context c, __in Z3_model m, __in unsigned i)
use Z3_model_get_const_decl
globalScope> Global Z3_get_model_func_decl (__in Z3_context c, __in Z3_model m, __in unsigned i)
use Z3_model_get_func_decl
globalScope> Global Z3_get_model_func_else (__in Z3_context c, __in Z3_model m, __in unsigned i)
Use Z3_func_interp objects
globalScope> Global Z3_get_model_func_entry_arg (__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j, __in unsigned k)
Use Z3_func_interp objects
globalScope> Global Z3_get_model_func_entry_num_args (__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j)
Use Z3_func_interp objects
globalScope> Global Z3_get_model_func_entry_value (__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j)
Use Z3_func_interp objects
globalScope> Global Z3_get_model_func_num_entries (__in Z3_context c, __in Z3_model m, __in unsigned i)
Use Z3_func_interp objects
globalScope> Global Z3_get_model_num_constants (__in Z3_context c, __in Z3_model m)
use Z3_model_get_num_consts
globalScope> Global Z3_get_model_num_funcs (__in Z3_context c, __in Z3_model m)
use Z3_model_get_num_funcs
globalScope> Global Z3_get_num_literals (__in Z3_context c, __in Z3_literals lbls)
This procedure is based on the old Solver API.
globalScope> Global Z3_get_num_scopes (__in Z3_context c)
Subsumed by Z3_solver_get_num_scopes.
globalScope> Global Z3_get_relevant_labels (__in Z3_context c)
This procedure is based on the old Solver API.
globalScope> Global Z3_get_relevant_literals (__in Z3_context c)
This procedure is based on the old Solver API.
globalScope> Global Z3_get_search_failure (__in Z3_context c)
Subsumed by Z3_solver_get_reason_unknown
globalScope> Global Z3_is_array_value (__in Z3_context c, __in Z3_model m, __in Z3_ast v, __out unsigned *num_entries)
Use Z3_is_as_array
globalScope> Global Z3_mk_context (__in Z3_config c)
Use Z3_mk_context_rc
globalScope> Global Z3_mk_injective_function (__in Z3_context c, __in Z3_symbol s, unsigned domain_size, __in_ecount(domain_size) Z3_sort const domain[], __in 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.
globalScope> Global Z3_mk_label (__in Z3_context c, __in 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.
globalScope> Global Z3_persist_ast (__in Z3_context c, __in Z3_ast a, __in unsigned num_scopes)
Z3 users should move to Z3_mk_context_rc and use the reference counting APIs for managing AST nodes.
globalScope> Global Z3_pop (__in Z3_context c, __in unsigned num_scopes)
Subsumed by Z3_solver_pop
globalScope> Global Z3_push (__in Z3_context c)
Subsumed by Z3_solver_push
globalScope> Global Z3_set_logic (__in Z3_context c, __in Z3_string logic)
Subsumed by Z3_mk_solver_for_logic
globalScope> Global Z3_soft_check_cancel (__in Z3_context c)
Use Z3_interrupt instead.
globalScope> Global Z3_statistics_to_string (__in Z3_context c)
This method is based on the old solver API. Use Z3_stats_to_string when using the new solver API.