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