- Global Z3_assert_cnstr (__in Z3_context c, __in Z3_ast a)
- Subsumed by Z3_solver_assert
- Global Z3_block_literals (__in Z3_context c, __in Z3_literals lbls)
- This procedure is based on the old Solver API.
- Global Z3_check (__in Z3_context c)
- Subsumed by Z3_solver_check
- Global Z3_check_and_get_model (__in Z3_context c, __out Z3_model *m)
- Subsumed by Z3_solver_check
- 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
- 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.
- Global Z3_del_literals (__in Z3_context c, __in Z3_literals lbls)
- This procedure is based on the old Solver API.
- Global Z3_del_model (__in Z3_context c, __in Z3_model m)
- Subsumed by Z3_solver API
- Global Z3_disable_literal (__in Z3_context c, __in Z3_literals lbls, __in unsigned idx)
- This procedure is based on the old Solver API.
- Global Z3_eval (__in Z3_context c, __in Z3_model m, __in Z3_ast t, __out Z3_ast *v)
- Use Z3_model_eval
- 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
- 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
- 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
- Global Z3_get_context_assignment (__in Z3_context c)
- This method is based on the old solver API.
- Global Z3_get_error_msg (__in Z3_error_code err)
- Use Z3_get_error_msg_ex instead.
- Global Z3_get_guessed_literals (__in Z3_context c)
- This procedure is based on the old Solver API.
- 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.
- 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.
- Global Z3_get_literal (__in Z3_context c, __in Z3_literals lbls, __in unsigned idx)
- This procedure is based on the old Solver API.
- Global Z3_get_model_constant (__in Z3_context c, __in Z3_model m, __in unsigned i)
- use Z3_model_get_const_decl
- Global Z3_get_model_func_decl (__in Z3_context c, __in Z3_model m, __in unsigned i)
- use Z3_model_get_func_decl
- Global Z3_get_model_func_else (__in Z3_context c, __in Z3_model m, __in unsigned i)
- Use Z3_func_interp objects
- 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
- 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
- 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
- Global Z3_get_model_func_num_entries (__in Z3_context c, __in Z3_model m, __in unsigned i)
- Use Z3_func_interp objects
- Global Z3_get_model_num_constants (__in Z3_context c, __in Z3_model m)
- use Z3_model_get_num_consts
- Global Z3_get_model_num_funcs (__in Z3_context c, __in Z3_model m)
- use Z3_model_get_num_funcs
- Global Z3_get_num_literals (__in Z3_context c, __in Z3_literals lbls)
- This procedure is based on the old Solver API.
- Global Z3_get_num_scopes (__in Z3_context c)
- Subsumed by Z3_solver_get_num_scopes.
- Global Z3_get_relevant_labels (__in Z3_context c)
- This procedure is based on the old Solver API.
- Global Z3_get_relevant_literals (__in Z3_context c)
- This procedure is based on the old Solver API.
- Global Z3_get_search_failure (__in Z3_context c)
- Subsumed by Z3_solver_get_reason_unknown
- 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
- Global Z3_mk_context (__in Z3_config c)
- Use Z3_mk_context_rc
- 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.
- 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.
- 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.
- Global Z3_pop (__in Z3_context c, __in unsigned num_scopes)
- Subsumed by Z3_solver_pop
- Global Z3_push (__in Z3_context c)
- Subsumed by Z3_solver_push
- Global Z3_set_logic (__in Z3_context c, __in Z3_string logic)
- Subsumed by Z3_mk_solver_for_logic
- Global Z3_soft_check_cancel (__in Z3_context c)
- Use Z3_interrupt instead.
- 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.