From 665af3d8b9da232ced38b03fbc00bd79880e5295 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Nov 2015 08:43:27 -0800 Subject: [PATCH] remove deprecated user-theory plugins and other unused functionality from API Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 3 +- src/api/api_context.cpp | 65 -- src/api/api_context.h | 9 - src/api/api_user_theory.cpp | 333 --------- src/api/z3_api.h | 391 +---------- src/smt/user_plugin/user_decl_plugin.cpp | 97 --- src/smt/user_plugin/user_decl_plugin.h | 62 -- .../user_plugin/user_simplifier_plugin.cpp | 81 --- src/smt/user_plugin/user_simplifier_plugin.h | 66 -- src/smt/user_plugin/user_smt_theory.cpp | 661 ------------------ src/smt/user_plugin/user_smt_theory.h | 324 --------- 11 files changed, 2 insertions(+), 2090 deletions(-) delete mode 100644 src/api/api_user_theory.cpp delete mode 100644 src/smt/user_plugin/user_decl_plugin.cpp delete mode 100644 src/smt/user_plugin/user_decl_plugin.h delete mode 100644 src/smt/user_plugin/user_simplifier_plugin.cpp delete mode 100644 src/smt/user_plugin/user_simplifier_plugin.h delete mode 100644 src/smt/user_plugin/user_smt_theory.cpp delete mode 100644 src/smt/user_plugin/user_smt_theory.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index dfe801bdd..1cb1e374f 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -51,7 +51,6 @@ def init_project_def(): add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa']) - add_lib('user_plugin', ['smt'], 'smt/user_plugin') add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv') add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') @@ -78,7 +77,7 @@ def init_project_def(): add_lib('smtparser', ['portfolio'], 'parsers/smt') add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h'] - add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp', 'opt'], + add_lib('api', ['portfolio', 'smtparser', 'realclosure', 'interp', 'opt'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3') add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 79a2fd965..d5901e97f 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -37,23 +37,6 @@ namespace api { exit(1); } - Z3_search_failure mk_Z3_search_failure(smt::failure f) { - switch(f) { - case smt::OK: return Z3_NO_FAILURE; - case smt::UNKNOWN: return Z3_UNKNOWN; - case smt::TIMEOUT: return Z3_TIMEOUT; - case smt::MEMOUT: return Z3_MEMOUT_WATERMARK; - case smt::CANCELED: return Z3_CANCELED; - case smt::NUM_CONFLICTS: return Z3_NUM_CONFLICTS; - case smt::THEORY: return Z3_THEORY; - case smt::QUANTIFIERS: return Z3_QUANTIFIERS; - default: - UNREACHABLE(); - break; - } - return static_cast(f); - } - context::add_plugins::add_plugins(ast_manager & m) { reg_decl_plugins(m); } @@ -94,7 +77,6 @@ namespace api { m_ast_trail(m()), m_replay_stack() { - m_solver = 0; m_error_code = Z3_OK; m_print_mode = Z3_PRINT_SMTLIB_FULL; m_searching = false; @@ -133,7 +115,6 @@ namespace api { m_ast_trail.reset(); } reset_parser(); - dealloc(m_solver); } void context::interrupt() { @@ -302,52 +283,6 @@ namespace api { } } - // ------------------------ - // - // Solver interface for backward compatibility - // - // ------------------------ - - smt::kernel & context::get_smt_kernel() { - if (!m_solver) { - m_fparams.updt_params(m_params); - m_solver = alloc(smt::kernel, m(), m_fparams); - } - return *m_solver; - } - - void context::assert_cnstr(expr * a) { - get_smt_kernel().assert_expr(a); - } - - lbool context::check(model_ref & m) { - flet searching(m_searching, true); - lbool r; - r = get_smt_kernel().check(); - if (r != l_false) - get_smt_kernel().get_model(m); - return r; - } - - void context::push() { - get_smt_kernel().push(); - m_ast_lim.push_back(m_ast_trail.size()); - m_replay_stack.push_back(0); - } - - void context::pop(unsigned num_scopes) { - for (unsigned i = 0; i < num_scopes; ++i) { - unsigned sz = m_ast_lim.back(); - m_ast_lim.pop_back(); - dealloc(m_replay_stack.back()); - m_replay_stack.pop_back(); - while (m_ast_trail.size() > sz) { - m_ast_trail.pop_back(); - } - } - SASSERT(num_scopes <= get_smt_kernel().get_scope_level()); - get_smt_kernel().pop(num_scopes); - } // ------------------------ // diff --git a/src/api/api_context.h b/src/api/api_context.h index d8331e2f8..2e7d89e7b 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -44,7 +44,6 @@ namespace realclosure { }; namespace api { - Z3_search_failure mk_Z3_search_failure(smt::failure f); class context : public tactic_manager { @@ -62,7 +61,6 @@ namespace api { // Support for old solver API smt_params m_fparams; - smt::kernel * m_solver; // General purpose solver for backward compatibility // ------------------------------- ast_ref_vector m_last_result; //!< used when m_user_ref_count == true @@ -210,13 +208,6 @@ namespace api { // // ------------------------ smt_params & fparams() { return m_fparams; } - bool has_solver() const { return m_solver != 0; } - smt::kernel & get_smt_kernel(); - void assert_cnstr(expr * a); - lbool check(model_ref & m); - void push(); - void pop(unsigned num_scopes); - unsigned get_num_scopes() const { return m_ast_lim.size(); } // ------------------------ // diff --git a/src/api/api_user_theory.cpp b/src/api/api_user_theory.cpp deleted file mode 100644 index fde34bbb2..000000000 --- a/src/api/api_user_theory.cpp +++ /dev/null @@ -1,333 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - api_user_theory.cpp - -Abstract: - API for external theories - -Author: - - Leonardo de Moura (leonardo) 2012-02-29. - -Revision History: - ---*/ -#include -#include"z3.h" -#include"api_log_macros.h" -#include"api_context.h" -#include"api_util.h" -#include"user_smt_theory.h" - -smt::user_theory * mk_t(Z3_theory t) { - return reinterpret_cast(t); -} - -extern "C" { - - /////////////////////////////// - // Theory plugin - // No support for logging - - Z3_theory Z3_mk_theory(Z3_context c, Z3_string th_name, void * ext_data) { - Z3_TRY; - RESET_ERROR_CODE(); - if (mk_c(c)->get_smt_kernel().get_scope_level() > 0) { - SET_ERROR_CODE(Z3_INVALID_USAGE); - return 0; - } - return reinterpret_cast(mk_user_theory(mk_c(c)->get_smt_kernel(), c, ext_data, th_name)); - Z3_CATCH_RETURN(0); - } - - void * Z3_theory_get_ext_data(Z3_theory t) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - void * r = mk_t(t)->get_ext_data(); - return r; - Z3_CATCH_RETURN(0); - } - - Z3_sort Z3_theory_mk_sort(Z3_context c, Z3_theory t, Z3_symbol s) { - Z3_TRY; - RESET_ERROR_CODE(); - sort * r = mk_t(t)->mk_sort(to_symbol(s)); - mk_c(c)->save_ast_trail(r); - return of_sort(r); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_theory_mk_value(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s) { - Z3_TRY; - RESET_ERROR_CODE(); - func_decl * d = mk_t(t)->mk_value_decl(to_symbol(n), to_sort(s)); - app * r = mk_c(c)->m().mk_const(d); - mk_c(c)->save_ast_trail(r); - return of_ast(r); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_theory_mk_constant(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s) { - Z3_TRY; - RESET_ERROR_CODE(); - Z3_func_decl d = Z3_theory_mk_func_decl(c, t, n, 0, 0, s); - app * r = mk_c(c)->m().mk_const(to_func_decl(d)); - mk_c(c)->save_ast_trail(r); - return of_ast(r); - Z3_CATCH_RETURN(0); - } - - Z3_func_decl Z3_theory_mk_func_decl(Z3_context c, Z3_theory t, Z3_symbol n, - unsigned domain_size, Z3_sort const domain[], - Z3_sort range) { - Z3_TRY; - RESET_ERROR_CODE(); - func_decl * r = mk_t(t)->mk_func_decl(to_symbol(n), domain_size, to_sorts(domain), to_sort(range)); - mk_c(c)->save_ast_trail(r); - return of_func_decl(r); - Z3_CATCH_RETURN(0); - } - - Z3_context Z3_theory_get_context(Z3_theory t) { - Z3_context c = reinterpret_cast(mk_t(t)->get_ext_context()); - RESET_ERROR_CODE(); - return c; - } - - void Z3_set_delete_callback(Z3_theory t, Z3_theory_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_delete_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_reduce_app_callback(Z3_theory t, Z3_reduce_app_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_reduce_app_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_reduce_eq_callback(Z3_theory t, Z3_reduce_eq_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_reduce_eq_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_reduce_distinct_callback(Z3_theory t, Z3_reduce_distinct_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_reduce_distinct_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_new_app_callback(Z3_theory t, Z3_theory_ast_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_new_app_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_new_elem_callback(Z3_theory t, Z3_theory_ast_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_new_elem_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_init_search_callback(Z3_theory t, Z3_theory_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_init_search_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_push_callback(Z3_theory t, Z3_theory_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_push_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_pop_callback(Z3_theory t, Z3_theory_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_pop_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_restart_callback(Z3_theory t, Z3_theory_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_restart_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_reset_callback(Z3_theory t, Z3_theory_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_reset_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_final_check_callback(Z3_theory t, Z3_theory_final_check_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_final_check_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_new_eq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_new_eq_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_new_diseq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_new_diseq_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_new_assignment_callback(Z3_theory t, Z3_theory_ast_bool_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_new_assignment_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_set_new_relevant_callback(Z3_theory t, Z3_theory_ast_callback_fptr f) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->set_new_relevant_fptr(reinterpret_cast(f)); - Z3_CATCH; - } - - void Z3_theory_assert_axiom(Z3_theory t, Z3_ast ax) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->assert_axiom(to_ast(ax)); - Z3_CATCH; - } - - void Z3_theory_assume_eq(Z3_theory t, Z3_ast lhs, Z3_ast rhs) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->assume_eq(to_ast(lhs), to_ast(rhs)); - Z3_CATCH; - } - - void Z3_theory_enable_axiom_simplification(Z3_theory t, Z3_bool flag) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - mk_t(t)->enable_axiom_simplification(flag == Z3_TRUE); - Z3_CATCH; - } - - Z3_ast Z3_theory_get_eqc_root(Z3_theory t, Z3_ast n) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return of_ast(mk_t(t)->get_root(to_ast(n))); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_theory_get_eqc_next(Z3_theory t, Z3_ast n) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return of_ast(mk_t(t)->get_next(to_ast(n))); - Z3_CATCH_RETURN(0); - } - - unsigned Z3_theory_get_num_parents(Z3_theory t, Z3_ast n) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return mk_t(t)->get_num_parents(to_ast(n)); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_theory_get_parent(Z3_theory t, Z3_ast n, unsigned i) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return of_ast(mk_t(t)->get_parent(to_ast(n), i)); - Z3_CATCH_RETURN(0); - } - - unsigned Z3_theory_get_num_elems(Z3_theory t) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return mk_t(t)->get_num_asts(); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_theory_get_elem(Z3_theory t, unsigned i) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return of_ast(mk_t(t)->get_ast(i)); - Z3_CATCH_RETURN(0); - } - - unsigned Z3_theory_get_num_apps(Z3_theory t) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return mk_t(t)->get_num_parents(); - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_theory_get_app(Z3_theory t, unsigned i) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return of_ast(mk_t(t)->get_parent(i)); - Z3_CATCH_RETURN(0); - } - - Z3_bool Z3_theory_is_value(Z3_theory t, Z3_ast n) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return is_app(to_ast(n)) && mk_t(t)->get_family_id() == to_app(to_ast(n))->get_family_id(); - Z3_CATCH_RETURN(Z3_FALSE); - } - - Z3_bool Z3_theory_is_decl(Z3_theory t, Z3_func_decl d) { - Z3_context c = Z3_theory_get_context(t); - Z3_TRY; - RESET_ERROR_CODE(); - return mk_t(t)->get_family_id() == to_func_decl(d)->get_family_id(); - Z3_CATCH_RETURN(Z3_FALSE); - } - -}; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index cc72aaa4c..65afa87d1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -24,7 +24,6 @@ Copyright (c) 2015 Microsoft Corporation #ifdef CorML3 DEFINE_TYPE(Z3_symbol); DEFINE_TYPE(Z3_literals); -DEFINE_TYPE(Z3_theory); DEFINE_TYPE(Z3_config); DEFINE_TYPE(Z3_context); DEFINE_TYPE(Z3_sort); @@ -55,7 +54,6 @@ DEFINE_TYPE(Z3_func_entry); DEFINE_TYPE(Z3_fixedpoint); DEFINE_TYPE(Z3_optimize); DEFINE_TYPE(Z3_rcf_num); -DEFINE_VOID(Z3_theory_data); #endif #ifndef __int64 @@ -1250,7 +1248,7 @@ typedef enum { Z3_PK_INVALID } Z3_param_kind; -#ifdef CorML3 +#if 0 /** \mlonly {!search_failure} \endmlonly \conly \brief The different kinds of search failure types. @@ -1345,8 +1343,6 @@ typedef enum def_Type('LITERALS', 'Z3_literals', 'Literals') def_Type('CONSTRUCTOR', 'Z3_constructor', 'Constructor') def_Type('CONSTRUCTOR_LIST', 'Z3_constructor_list', 'ConstructorList') - def_Type('THEORY', 'Z3_theory', 'ctypes.c_void_p') - def_Type('THEORY_DATA', 'Z3_theory_data', 'ctypes.c_void_p') def_Type('SOLVER', 'Z3_solver', 'SolverObj') def_Type('GOAL', 'Z3_goal', 'GoalObj') def_Type('TACTIC', 'Z3_tactic', 'TacticObj') @@ -5389,391 +5385,6 @@ END_MLAPI_EXCLUDE /*@}*/ -#ifdef CorML3 - /** - @name External Theory Plugins - */ - /*@{*/ - -#ifdef Conly - - // - // callbacks and void* don't work with CAMLIDL. - // - typedef Z3_bool Z3_reduce_eq_callback_fptr(Z3_theory t, Z3_ast a, Z3_ast b, Z3_ast * r); - - typedef Z3_bool Z3_reduce_app_callback_fptr(Z3_theory, Z3_func_decl, unsigned, Z3_ast const [], Z3_ast *); - - typedef Z3_bool Z3_reduce_distinct_callback_fptr(Z3_theory, unsigned, Z3_ast const [], Z3_ast *); - - typedef void Z3_theory_callback_fptr(Z3_theory t); - - typedef Z3_bool Z3_theory_final_check_callback_fptr(Z3_theory); - - typedef void Z3_theory_ast_callback_fptr(Z3_theory, Z3_ast); - - typedef void Z3_theory_ast_bool_callback_fptr(Z3_theory, Z3_ast, Z3_bool); - - typedef void Z3_theory_ast_ast_callback_fptr(Z3_theory, Z3_ast, Z3_ast); - -#endif - -#ifdef Conly - /** - \brief Create a new user defined theory. The new theory will be identified by the name \c th_name. - A theory must be created before asserting any assertion to the given context. - \conly Return \c NULL in case of failure. - - \conly \c data is a pointer to an external data-structure that may be used to store - \conly theory specific additional data. - */ - Z3_theory Z3_API Z3_mk_theory(Z3_context c, Z3_string th_name, Z3_theory_data data); - - /** - \brief Return a pointer to the external data-structure supplied to the function #Z3_mk_theory. - - \see Z3_mk_theory - */ - Z3_theory_data Z3_API Z3_theory_get_ext_data(Z3_theory t); -#endif - - /** - \brief Create an interpreted theory sort. - */ - Z3_sort Z3_API Z3_theory_mk_sort(Z3_context c, Z3_theory t, Z3_symbol s); - - /** - \brief Create an interpreted theory constant value. Values are assumed to be different from each other. - */ - Z3_ast Z3_API Z3_theory_mk_value(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s); - - /** - \brief Create an interpreted constant for the given theory. - */ - Z3_ast Z3_API Z3_theory_mk_constant(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s); - - /** - \brief Create an interpreted function declaration for the given theory. - */ - Z3_func_decl Z3_API Z3_theory_mk_func_decl(Z3_context c, Z3_theory t, Z3_symbol n, - unsigned domain_size, Z3_sort const domain[], - Z3_sort range); - - /** - \brief Return the context where the given theory is installed. - */ - Z3_context Z3_API Z3_theory_get_context(Z3_theory t); - - -#ifdef Conly - /** - \brief Set a callback that is invoked when theory \c t is deleted. - This callback should be used to delete external data-structures associated with the given theory. - - \conly The callback has the form f(t), where - \conly - \c t is the given theory - - \see Z3_mk_theory - \conly \see Z3_theory_get_ext_data - */ - void Z3_API Z3_set_delete_callback(Z3_theory t, Z3_theory_callback_fptr f); - - /** - \brief Set a callback for simplifying operators of the given theory. - The callback \c f is invoked by Z3's simplifier. - - \conly It is of the form f(t, d, n, args, r), where: - \conly - \c t is the given theory - \conly - \c d is the declaration of the theory operator - \conly - \c n is the number of arguments in the array \c args - \conly - \c args are arguments for the theory operator - \conly - \c r should contain the result: an expression equivalent to d(args[0], ..., args[n-1]). - - \conly If f(t, d, n, args, r) returns false, then \c r is ignored, and Z3 assumes that no simplification was performed. - */ - void Z3_API Z3_set_reduce_app_callback(Z3_theory t, Z3_reduce_app_callback_fptr f); - - /** - \brief Set a callback for simplifying the atom s_1 = s_2, when the - sort of \c s_1 and \c s_2 is an interpreted sort of the given theory. - The callback \c f is invoked by Z3's simplifier. - - \conly It has the form f(t, s_1, s_2, r), where: - \conly - \c t is the given theory - \conly - \c s_1 is the left-hand-side - \conly - \c s_2 is the right-hand-side - \conly - \c r should contain the result: an expression equivalent to s_1 = s_2. - - \conly If f(t, s_1, s_2, r) returns false, then \c r is ignored, and Z3 assumes that no simplification was performed. - */ - void Z3_API Z3_set_reduce_eq_callback(Z3_theory t, Z3_reduce_eq_callback_fptr f); - - /** - \brief Set a callback for simplifying the atom distinct(s_1, ..., s_n), when the - sort of \c s_1, ..., \c s_n is an interpreted sort of the given theory. - The callback \c f is invoked by Z3's simplifier. - - \conly It has the form f(t, n, args, r), where: - \conly - \c t is the given theory - \conly - \c n is the number of arguments in the array \c args - \conly - \c args are arguments for distinct. - \conly - \c r should contain the result: an expression equivalent to distinct(s_1, ..., s_n). - - \conly If f(t, n, args, r) returns false, then \c r is ignored, and Z3 assumes that no simplification was performed. - */ - void Z3_API Z3_set_reduce_distinct_callback(Z3_theory t, Z3_reduce_distinct_callback_fptr f); - - /** - \brief Set a callback that is invoked when a theory application - is finally added into the logical context. Note that, not every - application contained in an asserted expression is actually - added into the logical context because it may be simplified - during a preprocessing step. - - \conly The callback has the form f(t, n), where - \conly - \c t is the given theory - - \conly - \c n is a theory application, that is, an expression of the form g(...) where \c g is a theory operator. - - \remark An expression \c n added to the logical context at search level \c n, - will remain in the logical context until this level is backtracked. - */ - void Z3_API Z3_set_new_app_callback(Z3_theory t, Z3_theory_ast_callback_fptr f); - - /** - \brief Set a callback that is invoked when an expression of - sort \c s, where \c s is an interpreted sort of the theory \c - t, is finally added into the logical context. Note that, not - every expression contained in an asserted expression is - actually added into the logical context because it may be - simplified during a preprocessing step. - - \conly The callback has the form f(t, n), where - \conly - \c t is the given theory - - \conly - \c n is an expression of sort \c s, where \c s is an interpreted sort of \c t. - - \remark An expression \c n added to the logical context at search level \c n, - will remain in the logical context until this level is backtracked. - */ - void Z3_API Z3_set_new_elem_callback(Z3_theory t, Z3_theory_ast_callback_fptr f); - - /** - \brief Set a callback that is invoked when Z3 starts searching for a - satisfying assignment. - - \conly The callback has the form f(t), where - \conly - \c t is the given theory - */ - void Z3_API Z3_set_init_search_callback(Z3_theory t, Z3_theory_callback_fptr f); - - /** - \brief Set a callback that is invoked when Z3 creates a - case-split (aka backtracking point). - - When a case-split is created we say the search level is increased. - - \conly The callback has the form f(t), where - \conly - \c t is the given theory - */ - void Z3_API Z3_set_push_callback(Z3_theory t, Z3_theory_callback_fptr f); - - /** - \brief Set a callback that is invoked when Z3 backtracks a - case-split. - - When a case-split is backtracked we say the search level is decreased. - - \conly The callback has the form f(t), where - \conly - \c t is the given theory - */ - void Z3_API Z3_set_pop_callback(Z3_theory t, Z3_theory_callback_fptr f); - - /** - \brief Set a callback that is invoked when Z3 restarts the - search for a satisfying assignment. - - \conly The callback has the form f(t), where - \conly - \c t is the given theory - */ - void Z3_API Z3_set_restart_callback(Z3_theory t, Z3_theory_callback_fptr f); - - /** - \brief Set a callback that is invoked when the logical context - is reset by the user. This callback is useful for reseting any - data-structure maintained by the user theory solver. - - \conly The callback has the form f(t), where - \conly - \c t is the given theory - */ - void Z3_API Z3_set_reset_callback(Z3_theory t, Z3_theory_callback_fptr f); - - /** - \brief Set a callback that is invoked before Z3 starts building a model. - A theory may use this callback to perform expensive operations. - - \conly The callback has the form f(t), where - \conly - \c t is the given theory - - If the theory returns \mlonly \c false, \endmlonly \conly \c Z3_false, - Z3 will assume that theory is giving up, - and it will assume that it was not possible to decide if the asserted constraints - are satisfiable or not. - */ - void Z3_API Z3_set_final_check_callback(Z3_theory t, Z3_theory_final_check_callback_fptr f); - - /** - \brief Set a callback that is invoked when an equality s_1 = s_2 - is found by the logical context. - - \conly The callback has the form f(t, s_1, s_2), where: - \conly - \c t is the given theory - \conly - \c s_1 is the left-hand-side - \conly - \c s_2 is the right-hand-side - */ - void Z3_API Z3_set_new_eq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f); - - /** - \brief Set a callback that is invoked when a disequality s_1 != s_2 - is found by the logical context. - - \conly The callback has the form f(t, s_1, s_2), where: - \conly - \c t is the given theory - \conly - \c s_1 is the left-hand-side - \conly - \c s_2 is the right-hand-side - */ - void Z3_API Z3_set_new_diseq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f); - - /** - \brief Set a callback that is invoked when a theory predicate is assigned to true/false by Z3. - - \conly The callback has the form f(t, p, v), where: - \conly - \c t is the given theory - \conly - \c p is the assigned predicate. - \conly - \c v is the value (true/false) assigned to \c p. - */ - void Z3_API Z3_set_new_assignment_callback(Z3_theory t, Z3_theory_ast_bool_callback_fptr f); - - /** - \brief Set a callback that is invoked when an expression is - marked as relevant during the search. This callback is only - invoked when relevancy propagation is enabled. - - \conly The callback has the form f(t, n), where: - \conly - \c t is the given theory - \conly - \c n is the relevant expression - */ - void Z3_API Z3_set_new_relevant_callback(Z3_theory t, Z3_theory_ast_callback_fptr f); - -#endif - - /** - \brief Assert a theory axiom/lemmas during the search. - - An axiom added at search level \c n will remain in the logical context until - level \c n is backtracked. - - The callbacks for push (#Z3_set_push_callback) and pop - (#Z3_set_pop_callback) can be used to track when the search - level is increased (i.e., new case-split) and decreased (i.e., - case-split is backtracked). - - Z3 tracks the theory axioms asserted. So, multiple assertions of the same axiom are - ignored. - */ - void Z3_API Z3_theory_assert_axiom(Z3_theory t, Z3_ast ax); - - /** - \brief Inform to the logical context that \c lhs and \c rhs have the same interpretation - in the model being built by theory \c t. If lhs = rhs is inconsistent with other theories, - then the logical context will backtrack. - - For more information, see the paper "Model-Based Theory Combination" in the Z3 website. - */ - void Z3_API Z3_theory_assume_eq(Z3_theory t, Z3_ast lhs, Z3_ast rhs); - - /** - \brief Enable/disable the simplification of theory axioms asserted using #Z3_theory_assert_axiom. - By default, the simplification of theory specific operators is disabled. - That is, the reduce theory callbacks are not invoked for theory axioms. - The default behavior is useful when asserting axioms stating properties of theory operators. - */ - void Z3_API Z3_theory_enable_axiom_simplification(Z3_theory t, Z3_bool flag); - - /** - \brief Return the root of the equivalence class containing \c n. - */ - Z3_ast Z3_API Z3_theory_get_eqc_root(Z3_theory t, Z3_ast n); - - /** - \brief Return the next element in the equivalence class containing \c n. - - The elements in an equivalence class are organized in a circular list. - You can traverse the list by calling this function multiple times - using the result from the previous call. This is illustrated in the - code snippet below. - \code - Z3_ast curr = n; - do - curr = Z3_theory_get_eqc_next(theory, curr); - while (curr != n); - \endcode - */ - Z3_ast Z3_API Z3_theory_get_eqc_next(Z3_theory t, Z3_ast n); - - /** - \brief Return the number of parents of \c n that are operators of the given theory. - */ - unsigned Z3_API Z3_theory_get_num_parents(Z3_theory t, Z3_ast n); - - /** - \brief Return the i-th parent of \c n. - See #Z3_theory_get_num_parents. - */ - Z3_ast Z3_API Z3_theory_get_parent(Z3_theory t, Z3_ast n, unsigned i); - - /** - \brief Return \c Z3_TRUE if \c n is an interpreted theory value. - */ - Z3_bool Z3_API Z3_theory_is_value(Z3_theory t, Z3_ast n); - - /** - \brief Return \c Z3_TRUE if \c d is an interpreted theory declaration. - */ - Z3_bool Z3_API Z3_theory_is_decl(Z3_theory t, Z3_func_decl d); - - /** - \brief Return the number of expressions of the given theory in - the logical context. These are the expressions notified using the - callback #Z3_set_new_elem_callback. - */ - unsigned Z3_API Z3_theory_get_num_elems(Z3_theory t); - - /** - \brief Return the i-th elem of the given theory in the logical context. - - \see Z3_theory_get_num_elems - */ - Z3_ast Z3_API Z3_theory_get_elem(Z3_theory t, unsigned i); - - /** - \brief Return the number of theory applications in the logical - context. These are the expressions notified using the callback - #Z3_set_new_app_callback. - */ - unsigned Z3_API Z3_theory_get_num_apps(Z3_theory t); - - /** - \brief Return the i-th application of the given theory in the logical context. - - \see Z3_theory_get_num_apps - */ - Z3_ast Z3_API Z3_theory_get_app(Z3_theory t, unsigned i); - - /*@}*/ - -#endif - #ifdef CorML4 /** @name Fixedpoint facilities diff --git a/src/smt/user_plugin/user_decl_plugin.cpp b/src/smt/user_plugin/user_decl_plugin.cpp deleted file mode 100644 index 97264ce0b..000000000 --- a/src/smt/user_plugin/user_decl_plugin.cpp +++ /dev/null @@ -1,97 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - user_decl_plugin.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-05-22. - -Revision History: - ---*/ -#include"user_decl_plugin.h" -#include"warning.h" - -user_decl_plugin::user_decl_plugin() { -} - -void user_decl_plugin::finalize() { - m_manager->dec_array_ref(m_kind2func.size(), m_kind2func.c_ptr()); - m_manager->dec_array_ref(m_kind2sort.size(), m_kind2sort.c_ptr()); -} - -decl_plugin * user_decl_plugin::mk_fresh() { - user_decl_plugin * p = alloc(user_decl_plugin); - // TODO copy sorts and other goodness - return p; -} - -sort * user_decl_plugin::mk_sort(symbol const & name) { - unsigned kind = m_kind2sort.size(); - sort * s = m_manager->mk_sort(name, sort_info(m_family_id, kind)); - m_kind2sort.push_back(s); - m_manager->inc_ref(s); - if (!name.is_numerical()) { - m_sort_names.push_back(builtin_name(name.bare_str(), static_cast(kind))); - } - return s; -} - -func_decl * user_decl_plugin::mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) { - unsigned kind = m_kind2func.size(); - func_decl * f = m_manager->mk_func_decl(name, arity, domain, range, func_decl_info(m_family_id, kind)); - m_kind2func.push_back(f); - m_manager->inc_ref(f); - if (!name.is_numerical()) { - m_op_names.push_back(builtin_name(name.bare_str(), static_cast(kind))); - } - return f; -} - -func_decl * user_decl_plugin::mk_value_decl(symbol const & name, sort * s) { - func_decl * f = mk_func_decl(name, 0, 0, s); - m_values.insert(f); - return f; -} - -sort * user_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { - if (num_parameters > 0) { - throw default_exception("invalid user theory sort"); - return 0; - } - return m_kind2sort.get(k, 0); -} - -func_decl * user_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - func_decl * f = m_kind2func.get(k, 0); - if (num_parameters > 0 || f == 0) { - throw default_exception("invalid user theory function operator"); - return 0; - } - return f; -} - -bool user_decl_plugin::is_value(app * v) const { - return m_values.contains(v->get_decl()); -} - -bool user_decl_plugin::is_value(func_decl * f) const { - return m_values.contains(f); -} - -void user_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - op_names.append(m_op_names); -} - -void user_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { - sort_names.append(m_sort_names); -} - diff --git a/src/smt/user_plugin/user_decl_plugin.h b/src/smt/user_plugin/user_decl_plugin.h deleted file mode 100644 index e2c5d7b9f..000000000 --- a/src/smt/user_plugin/user_decl_plugin.h +++ /dev/null @@ -1,62 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - user_decl_plugin.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-05-22. - -Revision History: - ---*/ -#ifndef USER_DECL_PLUGIN_H_ -#define USER_DECL_PLUGIN_H_ - -#include"ast.h" -#include"obj_hashtable.h" - -class user_decl_plugin : public decl_plugin { - ptr_vector m_kind2sort; - ptr_vector m_kind2func; - obj_hashtable m_values; - svector m_op_names; - svector m_sort_names; -public: - user_decl_plugin(); - - virtual ~user_decl_plugin() {} - virtual void finalize(); - - virtual decl_plugin * mk_fresh(); - - sort * mk_sort(symbol const & name); - - func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range); - - func_decl * mk_value_decl(symbol const & name, sort * s); - - virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - virtual bool is_value(app*) const; - - virtual bool is_unique_value(app * a) const { return is_value(a); } - - bool is_value(func_decl *) const; - - virtual void get_op_names(svector & op_names, symbol const & logic); - - virtual void get_sort_names(svector & sort_names, symbol const & logic); -}; - -#endif /* USER_DECL_PLUGIN_H_ */ - diff --git a/src/smt/user_plugin/user_simplifier_plugin.cpp b/src/smt/user_plugin/user_simplifier_plugin.cpp deleted file mode 100644 index 866de805e..000000000 --- a/src/smt/user_plugin/user_simplifier_plugin.cpp +++ /dev/null @@ -1,81 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - user_simplifier_plugin.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-05-22. - -Revision History: - ---*/ -#include"user_simplifier_plugin.h" -#include"ast_pp.h" -#include"warning.h" - -user_simplifier_plugin::user_simplifier_plugin(symbol const & fname, ast_manager & m): - simplifier_plugin(fname, m), - m_owner(0), - m_enabled(true), - m_reduce_app_fptr(0), - m_reduce_eq_fptr(0), - m_reduce_distinct_fptr(0) { -} - -simplifier_plugin * user_simplifier_plugin::mk_fresh() { - ast_manager & m = get_manager(); - user_simplifier_plugin * new_sp = alloc(user_simplifier_plugin, m.get_family_name(get_family_id()), m); - new_sp->m_reduce_app_fptr = m_reduce_app_fptr; - new_sp->m_reduce_eq_fptr = m_reduce_eq_fptr; - new_sp->m_reduce_distinct_fptr = m_reduce_distinct_fptr; - return new_sp; -} - -bool user_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - if (m_reduce_app_fptr == 0 || !m_enabled) - return false; - expr * _result = 0; - bool flag = m_reduce_app_fptr(m_owner, f, num_args, args, &_result); - if (flag) { - if (_result == 0) - throw default_exception("invalid reduce_app callback: result is null"); - result = _result; - } - return flag; -} - -bool user_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { - if (m_reduce_eq_fptr == 0 || !m_enabled) - return false; - expr * _result = 0; - bool flag = m_reduce_eq_fptr(m_owner, lhs, rhs, &_result); - if (flag) { - if (_result == 0) - throw default_exception("invalid reduce_eq callback: result is null"); - result = _result; - } - return flag; -} - -bool user_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) { - if (m_reduce_distinct_fptr == 0 || !m_enabled) - return false; - expr * _result = 0; - bool flag = m_reduce_distinct_fptr(m_owner, num_args, args, &_result); - if (flag) { - if (_result == 0) - throw default_exception("invalid reduce_distinct callback: result is null"); - result = _result; - } - return flag; -} - -void user_simplifier_plugin::flush_caches() { -} diff --git a/src/smt/user_plugin/user_simplifier_plugin.h b/src/smt/user_plugin/user_simplifier_plugin.h deleted file mode 100644 index 87ff23032..000000000 --- a/src/smt/user_plugin/user_simplifier_plugin.h +++ /dev/null @@ -1,66 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - user_simplifier_plugin.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-05-22. - -Revision History: - ---*/ -#ifndef USER_SIMPLIFIER_PLUGIN_H_ -#define USER_SIMPLIFIER_PLUGIN_H_ - -#include"simplifier_plugin.h" - -typedef bool (*reduce_app_fptr)(void *, func_decl *, unsigned, expr * const *, expr **); -typedef bool (*reduce_eq_fptr)(void *, expr *, expr *, expr **); -typedef bool (*reduce_distinct_fptr)(void *, unsigned, expr * const *, expr **); - -class user_simplifier_plugin : public simplifier_plugin { - void * m_owner; - bool m_enabled; - reduce_app_fptr m_reduce_app_fptr; - reduce_eq_fptr m_reduce_eq_fptr; - reduce_distinct_fptr m_reduce_distinct_fptr; - -public: - user_simplifier_plugin(symbol const & fname, ast_manager & m); - - virtual simplifier_plugin * mk_fresh(); - - void set_reduce_app_fptr(reduce_app_fptr ptr) { - m_reduce_app_fptr = ptr; - } - - void set_reduce_eq_fptr(reduce_eq_fptr ptr) { - m_reduce_eq_fptr = ptr; - } - - void set_reduce_distinct_fptr(reduce_distinct_fptr ptr) { - m_reduce_distinct_fptr = ptr; - } - - void enable(bool flag) { m_enabled = flag; } - - void set_owner(void * ptr) { m_owner = ptr; } - - virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - - virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result); - - virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result); - - virtual void flush_caches(); -}; - -#endif /* USER_SIMPLIFIER_PLUGIN_H_ */ - diff --git a/src/smt/user_plugin/user_smt_theory.cpp b/src/smt/user_plugin/user_smt_theory.cpp deleted file mode 100644 index a2d1e4f37..000000000 --- a/src/smt/user_plugin/user_smt_theory.cpp +++ /dev/null @@ -1,661 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - user_smt_theory.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-05-22. - -Revision History: - ---*/ -#include"smt_context.h" -#include"user_smt_theory.h" -#include"ast_pp.h" -#include"smt_model_generator.h" -#include"stats.h" -#include"warning.h" - -namespace smt { - - // - // value factory for user sorts. - // - // NB. This value factory for user theories - // does not address theories where model - // values are structured objects such as - // arrays, records, or data-types. - // - - class user_smt_theory_factory : public simple_factory { - app* mk_value_core(unsigned const& val, sort* s) { - return m_manager.mk_model_value(val, s); - } - public: - user_smt_theory_factory(ast_manager& m, family_id fid): - simple_factory(m, fid) - {} - }; - - user_theory::user_theory(ast_manager & m, smt_params const& p, void * ext_context, void * ext_data, char const * name, family_id fid, user_decl_plugin * dp, user_simplifier_plugin * sp): - theory(fid), - m_params(p), - m_ext_context(ext_context), - m_ext_data(ext_data), - m_name(name), - m_simplify_axioms(false), - m_decl_plugin(dp), - m_simplifier_plugin(sp), - m_find(*this), - m_trail_stack(*this), - m_asserted_axioms(m), - m_persisted_axioms(m), - m_persisted_axioms_qhead(0), - m_delete_fptr(0), - m_new_app_fptr(0), - m_new_elem_fptr(0), - m_init_search_fptr(0), - m_push_fptr(0), - m_pop_fptr(0), - m_restart_fptr(0), - m_reset_fptr(0), - m_final_check_fptr(0), - m_new_eq_fptr(0), - m_new_diseq_fptr(0), - m_new_assignment_fptr(0), - m_new_relevant_fptr(0), - m_mk_fresh_fptr(0), - m_delete_invoking(false), - m_new_app_invoking(false), - m_new_elem_invoking(false), - m_init_search_invoking(false), - m_push_invoking(false), - m_pop_invoking(false), - m_restart_invoking(false), - m_reset_invoking(false), - m_final_check_invoking(false), - m_new_eq_invoking(false), - m_new_diseq_invoking(false), - m_new_assignment_invoking(false), - m_new_relevant_invoking(false) { - } - - user_theory::~user_theory() { - if (m_delete_fptr != 0) { - flet i(m_delete_invoking, true); - m_delete_fptr(this); - } - } - - theory * user_theory::mk_fresh(context * new_ctx) { - if (m_mk_fresh_fptr == 0) { - throw default_exception("The mk_fresh_ext_data callback was not set for user theory, you must use Z3_theory_set_mk_fresh_ext_data_callback"); - return 0; - } - user_simplifier_plugin * new_sp = static_cast(new_ctx->get_simplifier().get_plugin(get_family_id())); - SASSERT(new_sp != 0); - user_theory * new_th = alloc(user_theory, get_manager(), new_ctx->get_fparams(), m_ext_context, m_mk_fresh_fptr(this), get_name(), get_family_id(), - m_decl_plugin, new_sp); - new_sp->set_owner(new_th); - - new_th->m_delete_fptr = m_delete_fptr; - new_th->m_new_app_fptr = m_new_app_fptr; - new_th->m_new_elem_fptr = m_new_elem_fptr; - new_th->m_init_search_fptr = m_init_search_fptr; - new_th->m_push_fptr = m_push_fptr; - new_th->m_pop_fptr = m_pop_fptr; - new_th->m_restart_fptr = m_restart_fptr; - new_th->m_reset_fptr = m_reset_fptr; - new_th->m_final_check_fptr = m_final_check_fptr; - new_th->m_new_eq_fptr = m_new_eq_fptr; - new_th->m_new_diseq_fptr = m_new_diseq_fptr; - new_th->m_new_assignment_fptr = m_new_assignment_fptr; - new_th->m_new_relevant_fptr = m_new_relevant_fptr; - new_th->m_mk_fresh_fptr = m_mk_fresh_fptr; - return new_th; - } - - void user_theory::assert_axiom_core(app* a) { - if (m_asserted_axiom_set.contains(a)) { - return; - } - m_asserted_axiom_set.insert(a); - m_asserted_axioms.push_back(a); - if (m_params.m_user_theory_persist_axioms) { - m_persisted_axioms.push_back(a); - } - } - - /** - TODO: discuss semantics of assert_axiom. - Should we simplify axiom of not? - */ - void user_theory::assert_axiom(ast * axiom) { - ++m_stats.m_num_user_axioms; - TRACE("user_smt_theory", tout << mk_pp(axiom, get_manager()) << "\n";); - if (!is_expr(axiom)) { - throw default_exception("invalid expression"); - } - if (!get_manager().is_bool(to_expr(axiom))) { - throw default_exception("invalid theory axiom: axioms must have Boolean sort"); - } - if (!m_new_eq_invoking && - !m_new_diseq_invoking && - !m_new_assignment_invoking && - !m_new_relevant_invoking && - !m_final_check_invoking) { - throw default_exception("theory axioms can only be invoked during callbacks " - "for new (dis)equalities/assignments and final check"); - } - context & ctx = get_context(); - ast_manager & m = get_manager(); - - if (!is_app(axiom) || !to_app(axiom)->is_ground() || - ctx.get_fparams().m_user_theory_preprocess_axioms) { - asserted_formulas asf(m, ctx.get_fparams()); - asf.assert_expr(to_app(axiom)); - asf.reduce(); - unsigned sz = asf.get_num_formulas(); - unsigned qhead = asf.get_qhead(); - while (qhead < sz) { - expr * f = asf.get_formula(qhead); - assert_axiom_core(to_app(f)); - ++qhead; - } - } - else { - if (!m_simplify_axioms) { - m_simplifier_plugin->enable(false); - } - expr_ref s_axiom(m); - proof_ref pr(m); - simplifier & s = ctx.get_simplifier(); - s(to_app(axiom), s_axiom, pr); - if (!is_app(s_axiom)) { - throw default_exception("invalid theory axiom: axioms must be applications"); - } - axiom = s_axiom; - m_simplifier_plugin->enable(true); - assert_axiom_core(to_app(axiom)); - } - } - - void user_theory::assume_eq(ast * _lhs, ast * _rhs) { - if (!is_expr(_lhs) || !is_expr(_rhs)) { - throw default_exception("assume_eq must take expressions as arguments"); - } - expr* lhs = to_expr(_lhs); - expr* rhs = to_expr(_rhs); - ast_manager& m = get_manager(); - context& ctx = get_context(); - if (m.is_true(rhs)) { - std::swap(lhs, rhs); - } - if (m.is_true(lhs)) { - theory_var v2 = mk_var(rhs); - if (v2 == null_theory_var) { - throw default_exception("invalid assume eq: lhs or rhs is not a theory term"); - } - bool_var bv = ctx.get_bool_var(rhs); - ctx.set_true_first_flag(bv); - ctx.mark_as_relevant(get_enode(v2)); - return; - } - if (m.is_bool(lhs)) { - throw default_exception("assume_eq on Booleans must take 'true' as one of the arguments"); - } - theory_var v1 = mk_var(lhs); - theory_var v2 = mk_var(rhs); - if (v1 == null_theory_var || v2 == null_theory_var) { - throw default_exception("invalid assume eq: lhs or rhs is not a theory term"); - } - ctx.assume_eq(get_enode(v1), get_enode(v2)); - } - - void user_theory::reset_propagation_queues() { - m_new_eqs.reset(); - m_new_diseqs.reset(); - m_new_assignments.reset(); - m_new_relevant_apps.reset(); - } - - theory_var user_theory::get_var(ast * n) const { - if (!is_app(n)) - return null_theory_var; - context & ctx = get_context(); - if (ctx.e_internalized(to_app(n))) { - enode * e = ctx.get_enode(to_app(n)); - return e->get_th_var(get_id()); - } - return null_theory_var; - } - - theory_var user_theory::mk_var(ast * n) { - theory_var v = get_var(n); - if (v != null_theory_var || !is_app(n)) { - return v; - } - app* a = to_app(n); - if (a->get_family_id() == get_id() && - internalize_term(a)) { - return mk_var(get_context().get_enode(a)); - } - return v; - } - - ast * user_theory::get_root(ast * n) const { - theory_var v = get_var(n); - if (v != null_theory_var) { - theory_var r = m_find.find(v); - return get_ast(r); - } - return n; - } - - ast * user_theory::get_next(ast * n) const { - theory_var v = get_var(n); - if (v != null_theory_var) { - theory_var r = m_find.next(v); - return get_ast(r); - } - return n; - } - - void user_theory::shrink_use_list(unsigned sz) { - SASSERT(m_use_list.size() >= sz); - std::for_each(m_use_list.begin() + sz, m_use_list.end(), delete_proc >()); - m_use_list.shrink(sz); - } - - ptr_vector * user_theory::get_non_null_use_list(theory_var v) { - SASSERT(v != null_theory_var); - if (m_use_list[v] == 0) - m_use_list[v] = alloc(ptr_vector); - return m_use_list[v]; - } - - unsigned user_theory::get_num_parents(ast * n) const { - theory_var v = get_var(n); - if (v != null_theory_var && m_use_list[v] != 0) - return m_use_list[v]->size(); - return 0; - } - - - ast * user_theory::get_parent(ast * n, unsigned i) const { - theory_var v = get_var(n); - if (v != null_theory_var && m_use_list[v] != 0) - return m_use_list[v]->get(i, 0); - return 0; - } - - theory_var user_theory::mk_var(enode * n) { - if (is_attached_to_var(n)) - return n->get_th_var(get_id()); - theory_var r = theory::mk_var(n); - theory_var r2 = m_find.mk_var(); - m_use_list.push_back(0); - SASSERT(r == r2); - get_context().attach_th_var(n, this, r); - if (m_new_elem_fptr != 0) { - flet invoking(m_new_elem_invoking, true); - m_new_elem_fptr(this, n->get_owner()); - } - return r; - } - - bool user_theory::internalize_atom(app * atom, bool gate_ctx) { - return internalize_term(atom); - } - - bool user_theory::internalize_term(app * term) { - context & ctx = get_context(); - unsigned num_args = term->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - ctx.internalize(term->get_arg(i), false); - // the internalization of the arguments may trigger the internalization of term. - if (ctx.e_internalized(term)) - return true; - m_parents.push_back(term); - enode * e = ctx.mk_enode(term, false, get_manager().is_bool(term), true); - if (get_manager().is_bool(term)) { - bool_var bv = ctx.mk_bool_var(term); - ctx.set_var_theory(bv, get_id()); - ctx.set_enode_flag(bv, true); - } - // make sure every argument is attached to a theory variable... - for (unsigned i = 0; i < num_args; i++) { - enode * arg = e->get_arg(i); - theory_var v_arg = mk_var(arg); - ptr_vector * arg_use_list = get_non_null_use_list(v_arg); - arg_use_list->push_back(term); - m_trail_stack.push(push_back_trail(*arg_use_list)); - } - if (m_new_app_fptr != 0) { - flet invoking(m_new_app_invoking, true); - m_new_app_fptr(this, term); - } - return true; - } - - void user_theory::apply_sort_cnstr(enode * n, sort * s) { - mk_var(n); - } - - void user_theory::assign_eh(bool_var v, bool is_true) { - m_new_assignments.push_back(v); - } - - void user_theory::new_eq_eh(theory_var v1, theory_var v2) { - m_new_eqs.push_back(var_pair(v1, v2)); - } - - void user_theory::new_diseq_eh(theory_var v1, theory_var v2) { - m_new_diseqs.push_back(var_pair(v1, v2)); - } - - void user_theory::relevant_eh(app * n) { - m_new_relevant_apps.push_back(n); - } - - void user_theory::push_scope_eh() { - SASSERT(m_new_assignments.empty()); - SASSERT(m_new_eqs.empty()); - SASSERT(m_new_diseqs.empty()); - SASSERT(m_new_relevant_apps.empty()); - theory::push_scope_eh(); - m_trail_stack.push_scope(); - m_scopes.push_back(scope()); - scope & s = m_scopes.back(); - s.m_asserted_axioms_old_sz = m_asserted_axioms.size(); - s.m_parents_old_sz = m_parents.size(); - if (m_push_fptr != 0) { - flet invoke(m_push_invoking, true); - m_push_fptr(this); - } - } - - void user_theory::pop_scope_eh(unsigned num_scopes) { - reset_propagation_queues(); - if (m_pop_fptr != 0) { - for (unsigned i = 0; i < num_scopes; i++) { - flet invoke(m_pop_invoking, true); - m_pop_fptr(this); - } - } - unsigned new_lvl = m_scopes.size() - num_scopes; - scope & s = m_scopes[new_lvl]; - m_parents.shrink(s.m_parents_old_sz); - unsigned curr_sz = m_asserted_axioms.size(); - unsigned old_sz = s.m_asserted_axioms_old_sz; - for (unsigned i = old_sz; i < curr_sz; i++) { - m_asserted_axiom_set.erase(m_asserted_axioms.get(i)); - } - m_asserted_axioms.shrink(old_sz); - m_scopes.shrink(new_lvl); - m_trail_stack.pop_scope(num_scopes); - shrink_use_list(get_old_num_vars(num_scopes)); - theory::pop_scope_eh(num_scopes); - } - - void user_theory::restart_eh() { - if (m_restart_fptr != 0) { - flet invoke(m_restart_invoking, true); - m_restart_fptr(this); - } - } - - - void user_theory::init_search_eh() { - if (m_init_search_fptr != 0) { - flet invoke(m_init_search_invoking, true); - m_init_search_fptr(this); - } - } - - final_check_status user_theory::final_check_eh() { - if (m_final_check_fptr != 0) { - unsigned old_sz = m_asserted_axioms.size(); - flet invoke(m_final_check_invoking, true); - Z3_bool r = m_final_check_fptr(this); - if (old_sz != m_asserted_axioms.size()) { - assert_axioms_into_context(old_sz); - return r ? FC_CONTINUE : FC_GIVEUP; - } - return r ? FC_DONE : FC_GIVEUP; - } - return FC_DONE; - } - - bool user_theory::can_propagate() { - return - (m_persisted_axioms.size() > m_persisted_axioms_qhead) || - !m_new_eqs.empty() || - !m_new_diseqs.empty() || - !m_new_relevant_apps.empty() || - !m_new_assignments.empty(); - } - - literal user_theory::internalize_literal(expr * arg) { - context & ctx = get_context(); - ast_manager& m = get_manager(); - if (is_app(arg) && m.is_not(arg)) { - expr * arg_arg = to_app(arg)->get_arg(0); - if (!ctx.b_internalized(arg_arg)) - ctx.internalize(arg_arg, true); - return literal(ctx.get_bool_var(arg_arg), true); - } - else if (m.is_false(arg)) { - return false_literal; - } - else if (m.is_true(arg)) { - return true_literal; - } - else { - if (!ctx.b_internalized(arg)) - ctx.internalize(arg, true); - return literal(ctx.get_bool_var(arg)); - } - } - - void user_theory::assert_axioms_into_context(unsigned old_sz) { - for (unsigned i = old_sz; i < m_asserted_axioms.size(); i++) { - expr * axiom = m_asserted_axioms.get(i); - assert_axiom_into_context(axiom); - } - } - - void user_theory::mark_as_relevant(literal l) { - if (l == false_literal || l == true_literal) return; - get_context().mark_as_relevant(l); - } - - void user_theory::assert_axiom_into_context(expr * axiom) { - TRACE("user_smt_theory", tout << mk_pp(axiom, get_manager()) << "\n";); - ast_manager & m = get_manager(); - context & ctx = get_context(); - if (m.is_or(axiom)) { - literal_buffer lits; - unsigned num_args = to_app(axiom)->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - lits.push_back(internalize_literal(to_app(axiom)->get_arg(i))); - mark_as_relevant(lits.back()); - } - ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); - } - else { - literal l = internalize_literal(axiom); - mark_as_relevant(l); - ctx.mk_th_axiom(get_id(), 1, &l); - } - } - - void user_theory::propagate() { - - unsigned old_sz = m_asserted_axioms.size(); - if (m_persisted_axioms_qhead < m_persisted_axioms.size()) { - get_context().push_trail(value_trail(m_persisted_axioms_qhead)); - for (; m_persisted_axioms_qhead < m_persisted_axioms.size(); ++m_persisted_axioms_qhead) { - m_asserted_axioms.push_back(m_persisted_axioms[m_persisted_axioms_qhead].get()); - } - } - do { - for (unsigned i = 0; i < m_new_eqs.size(); i++) { - var_pair & p = m_new_eqs[i]; - if (m_new_eq_fptr != 0) { - ++m_stats.m_num_eq; - flet invoke(m_new_eq_invoking, true); - m_new_eq_fptr(this, get_app(p.first), get_app(p.second)); - } - m_find.merge(p.first, p.second); - } - m_new_eqs.reset(); - - if (m_new_diseq_fptr != 0) { - for (unsigned i = 0; i < m_new_diseqs.size(); i++) { - ++m_stats.m_num_diseq; - var_pair & p = m_new_diseqs[i]; - flet invoke(m_new_diseq_invoking, true); - m_new_diseq_fptr(this, get_app(p.first), get_app(p.second)); - } - } - m_new_diseqs.reset(); - - if (m_new_assignment_fptr != 0) { - context & ctx = get_context(); - for (unsigned i = 0; i < m_new_assignments.size(); i++) { - ++m_stats.m_num_assignment; - bool_var bv = m_new_assignments[i]; - lbool val = ctx.get_assignment(bv); - SASSERT(val != l_undef); - flet invoke(m_new_assignment_invoking, true); - m_new_assignment_fptr(this, to_app(ctx.bool_var2expr(bv)), val == l_true); - } - } - m_new_assignments.reset(); - - if (m_new_relevant_fptr != 0) { - for (unsigned i = 0; i < m_new_relevant_apps.size(); i++) { - flet invoke(m_new_relevant_invoking, true); - m_new_relevant_fptr(this, m_new_relevant_apps[i]); - } - } - m_new_relevant_apps.reset(); - - assert_axioms_into_context(old_sz); - old_sz = m_asserted_axioms.size(); - } - while (!m_new_eqs.empty() || !m_new_diseqs.empty() || !m_new_relevant_apps.empty() || !m_new_assignments.empty()); - } - - void user_theory::flush_eh() { - reset(false); - } - - void user_theory::reset_eh() { - reset(true); - } - - void user_theory::reset(bool full_reset) { - if (m_reset_fptr != 0) { - flet invoke(m_reset_invoking, true); - m_reset_fptr(this); - } - m_trail_stack.reset(); - reset_propagation_queues(); - m_asserted_axioms.reset(); - m_asserted_axiom_set.reset(); - shrink_use_list(0); - m_parents.reset(); - m_scopes.reset(); - m_persisted_axioms.reset(); - m_persisted_axioms_qhead = 0; - m_stats.reset(); - if (full_reset) - theory::reset_eh(); - } - - void user_theory::display_statistics(std::ostream & out) const { - print_stat(out, "num. user eqs: ", m_stats.m_num_eq); - print_stat(out, "num. user diseq: ", m_stats.m_num_diseq); - print_stat(out, "num. assignments: ", m_stats.m_num_assignment); - print_stat(out, "num. user axioms: ", m_stats.m_num_user_axioms); - } - - void user_theory::display_istatistics(std::ostream & out) const { - out << "NUM_USER_EQS " << m_stats.m_num_eq << "\n"; - out << "NUM_USER_DISEQ " << m_stats.m_num_diseq << "\n"; - out << "NUM_ASSIGNMENTS " << m_stats.m_num_assignment << "\n"; - out << "NUM_USER_AXIOMS " << m_stats.m_num_user_axioms << "\n"; - } - - class user_smt_model_value_proc : public model_value_proc { - func_decl_ref m_decl; - public: - user_smt_model_value_proc(ast_manager& m, func_decl* f) : m_decl(f, m) {} - - virtual app * mk_value(model_generator & mg, ptr_vector & values) { - ast_manager& m = mg.get_manager(); - return m.mk_app(m_decl, values.size(), values.c_ptr()); - } - }; - - bool user_theory::build_models() const { - return true; - } - - void user_theory::init_model(model_generator & m) { - m.register_factory(alloc(user_smt_theory_factory, get_manager(), get_id())); - } - - void user_theory::finalize_model(model_generator &) { - // No-op - } - - model_value_proc * user_theory::mk_value(enode * n, model_generator & mg) { - ast_manager& m = get_manager(); - func_decl* f = n->get_decl(); - if (m_decl_plugin->is_value(f)) { - return alloc(user_smt_model_value_proc, m, n->get_decl()); - } - else { - return mg.mk_model_value(n); - } - } - - bool user_theory::get_value(enode * n, expr_ref & r) { - return false; - } - - char const * user_theory::get_name() const { - return m_name.c_str(); - } - - void user_theory::display(std::ostream & out) const { - out << "Theory " << get_name() << ":\n"; - } - - user_theory * mk_user_theory(kernel & _s, void * ext_context, void * ext_data, char const * name) { - context & ctx = _s.get_context(); // HACK - symbol _name(name); - ast_manager & m = ctx.get_manager(); - family_id fid = m.mk_family_id(_name); - user_decl_plugin * dp = alloc(user_decl_plugin); - m.register_plugin(fid, dp); - simplifier & s = ctx.get_simplifier(); - user_simplifier_plugin * sp = alloc(user_simplifier_plugin, _name, m); - s.register_plugin(sp); - user_theory * th = alloc(user_theory, m, ctx.get_fparams(), ext_context, ext_data, name, fid, dp, sp); - ctx.register_plugin(th); - sp->set_owner(th); - return th; - } -}; - diff --git a/src/smt/user_plugin/user_smt_theory.h b/src/smt/user_plugin/user_smt_theory.h deleted file mode 100644 index 128780317..000000000 --- a/src/smt/user_plugin/user_smt_theory.h +++ /dev/null @@ -1,324 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - user_smt_theory.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2010-05-22. - -Revision History: - ---*/ -#ifndef USER_SMT_THEORY_H_ -#define USER_SMT_THEORY_H_ - -#include"user_decl_plugin.h" -#include"user_simplifier_plugin.h" -#include"smt_theory.h" -#include"union_find.h" -#include"smt_kernel.h" - -namespace smt { - - class user_theory; - typedef int Z3_bool; - - typedef void (*theory_callback_fptr)(user_theory * th); - typedef Z3_bool (*theory_final_check_callback_fptr)(user_theory * th); - typedef void (*theory_app_callback_fptr)(user_theory * th, app *); - typedef void (*theory_app_bool_callback_fptr)(user_theory * th, app *, Z3_bool); - typedef void (*theory_app_app_callback_fptr)(user_theory * th, app *, app *); - typedef void * (*theory_mk_fresh_ext_data_fptr)(user_theory * th); - - class user_theory : public theory { - - typedef trail_stack th_trail_stack; - typedef union_find th_union_find; - typedef std::pair var_pair; - - smt_params const& m_params; - void * m_ext_context; - void * m_ext_data; - std::string m_name; - bool m_simplify_axioms; - user_decl_plugin * m_decl_plugin; - user_simplifier_plugin * m_simplifier_plugin; - - th_union_find m_find; - th_trail_stack m_trail_stack; - - svector m_new_eqs; - svector m_new_diseqs; - svector m_new_assignments; - ptr_vector m_new_relevant_apps; - obj_hashtable m_asserted_axiom_set; - expr_ref_vector m_asserted_axioms; - ptr_vector m_parents; - ptr_vector > m_use_list; - - app_ref_vector m_persisted_axioms; - unsigned m_persisted_axioms_qhead; - - struct scope { - unsigned m_asserted_axioms_old_sz; - unsigned m_parents_old_sz; - }; - - svector m_scopes; - - theory_callback_fptr m_delete_fptr; - theory_app_callback_fptr m_new_app_fptr; - theory_app_callback_fptr m_new_elem_fptr; - theory_callback_fptr m_init_search_fptr; - theory_callback_fptr m_push_fptr; - theory_callback_fptr m_pop_fptr; - theory_callback_fptr m_restart_fptr; - theory_callback_fptr m_reset_fptr; - theory_final_check_callback_fptr m_final_check_fptr; - theory_app_app_callback_fptr m_new_eq_fptr; - theory_app_app_callback_fptr m_new_diseq_fptr; - theory_app_bool_callback_fptr m_new_assignment_fptr; - theory_app_callback_fptr m_new_relevant_fptr; - theory_mk_fresh_ext_data_fptr m_mk_fresh_fptr; - - - bool m_delete_invoking; - bool m_new_app_invoking; - bool m_new_elem_invoking; - bool m_init_search_invoking; - bool m_push_invoking; - bool m_pop_invoking; - bool m_restart_invoking; - bool m_reset_invoking; - bool m_final_check_invoking; - bool m_new_eq_invoking; - bool m_new_diseq_invoking; - bool m_new_assignment_invoking; - bool m_new_relevant_invoking; - - struct statistics { - unsigned m_num_eq; - unsigned m_num_diseq; - unsigned m_num_assignment; - unsigned m_num_user_axioms; - statistics() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - }; - - statistics m_stats; - - protected: - virtual theory_var mk_var(enode * n); - - literal internalize_literal(expr * arg); - - void assert_axioms_into_context(unsigned old_sz); - - void assert_axiom_into_context(expr * axiom); - - void reset_propagation_queues(); - - void shrink_use_list(unsigned sz); - - ptr_vector * get_non_null_use_list(theory_var v); - - void mark_as_relevant(literal l); - - void assert_axiom_core(app* axiom); - - public: - user_theory(ast_manager & m, smt_params const& p, void * ext_context, void * ext_data, char const * name, family_id fid, user_decl_plugin * dp, user_simplifier_plugin * sp); - virtual ~user_theory(); - - virtual theory * mk_fresh(context * new_ctx); - - void * get_ext_context() const { - return m_ext_context; - } - - void * get_ext_data() { - return m_ext_data; - } - - sort * mk_sort(symbol const & name) { - return m_decl_plugin->mk_sort(name); - } - - func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) { - return m_decl_plugin->mk_func_decl(name, arity, domain, range); - } - - func_decl * mk_value_decl(symbol const & name, sort * s) { - return m_decl_plugin->mk_value_decl(name, s); - } - - void assert_axiom(ast * axiom); - - void assume_eq(ast * lhs, ast * rhs); - - void enable_axiom_simplification(bool flag) { - m_simplify_axioms = flag; - } - - void set_delete_fptr(theory_callback_fptr ptr) { - m_delete_fptr = ptr; - } - - void set_reduce_app_fptr(reduce_app_fptr ptr) { - m_simplifier_plugin->set_reduce_app_fptr(ptr); - } - - void set_reduce_eq_fptr(reduce_eq_fptr ptr) { - m_simplifier_plugin->set_reduce_eq_fptr(ptr); - } - - void set_reduce_distinct_fptr(reduce_distinct_fptr ptr) { - m_simplifier_plugin->set_reduce_distinct_fptr(ptr); - } - - void set_new_app_fptr(theory_app_callback_fptr ptr) { - m_new_app_fptr = ptr; - } - - void set_new_elem_fptr(theory_app_callback_fptr ptr) { - m_new_elem_fptr = ptr; - } - - void set_init_search_fptr(theory_callback_fptr ptr) { - m_init_search_fptr = ptr; - } - - void set_push_fptr(theory_callback_fptr ptr) { - m_push_fptr = ptr; - } - - void set_pop_fptr(theory_callback_fptr ptr) { - m_pop_fptr = ptr; - } - - void set_restart_fptr(theory_callback_fptr ptr) { - m_restart_fptr = ptr; - } - - void set_reset_fptr(theory_callback_fptr ptr) { - m_reset_fptr = ptr; - } - - void set_final_check_fptr(theory_final_check_callback_fptr ptr) { - m_final_check_fptr = ptr; - } - - void set_new_eq_fptr(theory_app_app_callback_fptr ptr) { - m_new_eq_fptr = ptr; - } - - void set_new_diseq_fptr(theory_app_app_callback_fptr ptr) { - m_new_diseq_fptr = ptr; - } - - void set_new_assignment_fptr(theory_app_bool_callback_fptr ptr) { - m_new_assignment_fptr = ptr; - } - - void set_new_relevant_fptr(theory_app_callback_fptr ptr) { - m_new_relevant_fptr = ptr; - } - - th_trail_stack & get_trail_stack() { return m_trail_stack; } - - theory_var get_var(ast * n) const; - - theory_var mk_var(ast * n); - - ast * get_root(ast * n) const; - - ast * get_next(ast * n) const; - - unsigned get_num_parents(ast * n) const; - - ast * get_parent(ast * n, unsigned i) const; - - unsigned get_num_parents() const { return m_parents.size(); } - - ast * get_parent(unsigned i) const { return m_parents[i]; } - - unsigned get_num_apps() const { return get_num_vars(); } - - app * get_app(unsigned i) const { return get_enode(i)->get_owner(); } - - unsigned get_num_asts() const { return get_num_apps(); } - - ast * get_ast(unsigned i) const { return get_app(i); } - - static void merge_eh(theory_var, theory_var, theory_var, theory_var) {} - - static void after_merge_eh(theory_var, theory_var, theory_var, theory_var) {} - - virtual void unmerge_eh(theory_var, theory_var) {} - - virtual bool internalize_atom(app * atom, bool gate_ctx); - - virtual bool internalize_term(app * term); - - virtual void apply_sort_cnstr(enode * n, sort * s); - - virtual void assign_eh(bool_var v, bool is_true); - - virtual void new_eq_eh(theory_var v1, theory_var v2); - - virtual void new_diseq_eh(theory_var v1, theory_var v2); - - virtual void relevant_eh(app * n); - - virtual void push_scope_eh(); - - virtual void pop_scope_eh(unsigned num_scopes); - - virtual void restart_eh(); - - virtual void init_search_eh(); - - virtual final_check_status final_check_eh(); - - virtual bool can_propagate(); - - virtual void propagate(); - - virtual void flush_eh(); - - virtual void reset_eh(); - - void reset(bool full_reset); - - virtual void display_statistics(std::ostream & out) const; - - virtual void display_istatistics(std::ostream & out) const; - - virtual bool build_models() const; - - virtual void init_model(model_generator & m); - - virtual void finalize_model(model_generator & m); - - virtual model_value_proc * mk_value(enode * n, model_generator & mg); - - virtual bool get_value(enode * n, expr_ref & r); - - virtual char const * get_name() const; - - virtual void display(std::ostream & out) const; - }; - - user_theory * mk_user_theory(kernel & s, void * ext_context, void * ext_data, char const * name); -}; - - -#endif /* USER_SMT_THEORY_H_ */ -