From 759504880a14c698e496893527c852c7aee9879e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Oct 2012 20:15:33 -0700 Subject: [PATCH] isolated proto_model obsolete code Signed-off-by: Leonardo de Moura --- scripts/mk_project.py | 9 +-- src/model/func_interp.cpp | 67 ------------------- src/model/func_interp.h | 9 +-- src/{model => old_params}/model_params.cpp | 0 src/{model => old_params}/model_params.h | 0 .../proto_model}/array_factory.cpp | 0 .../proto_model}/array_factory.h | 0 .../proto_model}/datatype_factory.cpp | 0 .../proto_model}/datatype_factory.h | 0 .../proto_model}/numeral_factory.cpp | 0 .../proto_model}/numeral_factory.h | 0 .../proto_model}/proto_model.cpp | 59 +++++++++++++++- src/{model => smt/proto_model}/proto_model.h | 0 .../proto_model}/struct_factory.cpp | 0 .../proto_model}/struct_factory.h | 2 - .../proto_model}/value_factory.cpp | 0 .../proto_model}/value_factory.h | 0 17 files changed, 68 insertions(+), 78 deletions(-) rename src/{model => old_params}/model_params.cpp (100%) rename src/{model => old_params}/model_params.h (100%) rename src/{model => smt/proto_model}/array_factory.cpp (100%) rename src/{model => smt/proto_model}/array_factory.h (100%) rename src/{model => smt/proto_model}/datatype_factory.cpp (100%) rename src/{model => smt/proto_model}/datatype_factory.h (100%) rename src/{model => smt/proto_model}/numeral_factory.cpp (100%) rename src/{model => smt/proto_model}/numeral_factory.h (100%) rename src/{model => smt/proto_model}/proto_model.cpp (90%) rename src/{model => smt/proto_model}/proto_model.h (100%) rename src/{model => smt/proto_model}/struct_factory.cpp (100%) rename src/{model => smt/proto_model}/struct_factory.h (95%) rename src/{model => smt/proto_model}/value_factory.cpp (100%) rename src/{model => smt/proto_model}/value_factory.h (100%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index f0d5414d8..a57f84f1a 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -22,12 +22,12 @@ def init_project_def(): add_lib('simplifier', ['rewriter'], 'ast/simplifier') # Model module should not depend on simplifier module. # We must replace all occurrences of simplifier with rewriter. - add_lib('model', ['rewriter', 'simplifier']) + add_lib('model', ['rewriter']) add_lib('tactic', ['ast', 'model']) # Old (non-modular) parameter framework. It has been subsumed by util\params.h. # However, it is still used by many old components. - add_lib('old_params', ['model', 'simplifier']) - add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier']) + add_lib('old_params', ['simplifier']) + add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params']) add_lib('substitution', ['ast'], 'ast/substitution') add_lib('normal_forms', ['rewriter', 'old_params'], 'ast/normal_forms') add_lib('parser_util', ['ast'], 'parsers/util') @@ -38,7 +38,8 @@ def init_project_def(): add_lib('euclid', ['util'], 'math/euclid') add_lib('proof_checker', ['rewriter', 'old_params'], 'ast/proof_checker') add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params'], 'ast/rewriter/bit_blaster') - add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', + add_lib('proto_model', ['model', 'simplifier', 'old_params'], 'smt/proto_model') + add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util']) add_lib('user_plugin', ['smt'], 'smt/user_plugin') add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core') diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index e612734eb..678d95c86 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -16,8 +16,6 @@ Revision History: --*/ #include"func_interp.h" -#include"simplifier.h" -#include"basic_simplifier_plugin.h" #include"var_subst.h" #include"obj_hashtable.h" #include"ast_pp.h" @@ -182,71 +180,6 @@ bool func_interp::eval_else(expr * const * args, expr_ref & result) const { return true; } -/** - \brief Store in r the result of applying args to this function. - Return true in case of success. - The function may fail if m_else == 0. -*/ -bool func_interp::eval(simplifier & s, expr * const * args, expr_ref & result) { - bool actuals_are_values = true; - - if (!m_entries.empty()) { - for (unsigned i = 0; actuals_are_values && i < m_arity; i++) { - actuals_are_values = m_manager.is_value(args[i]); - } - } - - func_entry * entry = get_entry(args); - if (entry != 0) { - result = entry->get_result(); - TRACE("func_interp", tout << "found entry for: "; - for(unsigned i = 0; i < m_arity; i++) - tout << mk_pp(args[i], m_manager) << " "; - tout << "\nresult: " << mk_pp(result, m_manager) << "\n";); - return true; - } - - TRACE("func_interp", tout << "failed to find entry for: "; - for(unsigned i = 0; i < m_arity; i++) - tout << mk_pp(args[i], m_manager) << " "; - tout << "\nis partial: " << is_partial() << "\n";); - - if (!eval_else(args, result)) { - TRACE("func_interp", tout << "function is partial, failed to evaluate\n";); - return false; - } - - if (actuals_are_values && m_args_are_values) { - // cheap case... we are done - return true; - } - - - // build symbolic result... the actuals may be equal to the args of one of the entries. - basic_simplifier_plugin * bs = static_cast(s.get_plugin(m_manager.get_basic_family_id())); - ptr_vector::iterator it = m_entries.begin(); - ptr_vector::iterator end = m_entries.end(); - for (; it != end; ++it) { - func_entry * curr = *it; - SASSERT(!curr->eq_args(m_arity, args)); - if (!actuals_are_values || !curr->args_are_values()) { - expr_ref_buffer eqs(m_manager); - unsigned i = m_arity; - while (i > 0) { - --i; - expr_ref new_eq(m_manager); - bs->mk_eq(curr->get_arg(i), args[i], new_eq); - eqs.push_back(new_eq); - } - SASSERT(eqs.size() == m_arity); - expr_ref new_cond(m_manager); - bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond); - bs->mk_ite(new_cond, curr->get_result(), result, result); - } - } - return true; -} - /** \brief Return the result with the maximal number of occurrencies in m_entries. */ diff --git a/src/model/func_interp.h b/src/model/func_interp.h index 73244efc1..b10fe0dad 100644 --- a/src/model/func_interp.h +++ b/src/model/func_interp.h @@ -34,7 +34,6 @@ Revision History: #include"ast_translation.h" class func_interp; -class simplifier; class func_entry { bool m_args_are_values; //!< true if is_value(m_args[i]) is true for all i in [0, arity) @@ -50,10 +49,10 @@ class func_entry { friend class func_interp; void set_result(ast_manager & m, expr * r); - bool args_are_values() const { return m_args_are_values; } public: static func_entry * mk(ast_manager & m, unsigned arity, expr * const * args, expr * result); + bool args_are_values() const { return m_args_are_values; } void deallocate(ast_manager & m, unsigned arity); expr * get_result() const { return m_result; } expr * get_arg(unsigned idx) const { return m_args[idx]; } @@ -81,6 +80,8 @@ public: func_interp(ast_manager & m, unsigned arity); ~func_interp(); + ast_manager & m () const { return m_manager; } + func_interp * copy() const; unsigned get_arity() const { return m_arity; } @@ -88,8 +89,9 @@ public: bool is_partial() const { return m_else == 0; } // A function interpretation is said to be simple if m_else is ground. bool is_simple() const { return is_partial() || is_ground(m_else); } - bool is_constant() const; + // Return true if all arguments of the function graph are values. + bool args_are_values() const { return m_args_are_values; } expr * get_else() const { return m_else; } void set_else(expr * e); @@ -98,7 +100,6 @@ public: void insert_new_entry(expr * const * args, expr * r); func_entry * get_entry(expr * const * args) const; bool eval_else(expr * const * args, expr_ref & result) const; - bool eval(simplifier & s, expr * const * args, expr_ref & result); unsigned num_entries() const { return m_entries.size(); } func_entry const * const * get_entries() const { return m_entries.c_ptr(); } func_entry const * get_entry(unsigned idx) const { return m_entries[idx]; } diff --git a/src/model/model_params.cpp b/src/old_params/model_params.cpp similarity index 100% rename from src/model/model_params.cpp rename to src/old_params/model_params.cpp diff --git a/src/model/model_params.h b/src/old_params/model_params.h similarity index 100% rename from src/model/model_params.h rename to src/old_params/model_params.h diff --git a/src/model/array_factory.cpp b/src/smt/proto_model/array_factory.cpp similarity index 100% rename from src/model/array_factory.cpp rename to src/smt/proto_model/array_factory.cpp diff --git a/src/model/array_factory.h b/src/smt/proto_model/array_factory.h similarity index 100% rename from src/model/array_factory.h rename to src/smt/proto_model/array_factory.h diff --git a/src/model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp similarity index 100% rename from src/model/datatype_factory.cpp rename to src/smt/proto_model/datatype_factory.cpp diff --git a/src/model/datatype_factory.h b/src/smt/proto_model/datatype_factory.h similarity index 100% rename from src/model/datatype_factory.h rename to src/smt/proto_model/datatype_factory.h diff --git a/src/model/numeral_factory.cpp b/src/smt/proto_model/numeral_factory.cpp similarity index 100% rename from src/model/numeral_factory.cpp rename to src/smt/proto_model/numeral_factory.cpp diff --git a/src/model/numeral_factory.h b/src/smt/proto_model/numeral_factory.h similarity index 100% rename from src/model/numeral_factory.h rename to src/smt/proto_model/numeral_factory.h diff --git a/src/model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp similarity index 90% rename from src/model/proto_model.cpp rename to src/smt/proto_model/proto_model.cpp index 4b5d201b9..f944990ee 100644 --- a/src/model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -24,6 +24,7 @@ Revision History: #include"well_sorted.h" #include"used_symbols.h" #include"model_v2_pp.h" +#include"basic_simplifier_plugin.h" proto_model::proto_model(ast_manager & m, simplifier & s, model_params const & p): model_core(m), @@ -115,6 +116,62 @@ expr * proto_model::mk_some_interp_for(func_decl * d) { return r; } +// Auxiliary function for computing fi(args[0], ..., args[fi.get_arity() - 1]). +// The result is stored in result. +// Return true if succeeded, and false otherwise. +// It uses the simplifier s during the computation. +bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) { + bool actuals_are_values = true; + + if (fi.num_entries() != 0) { + for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) { + actuals_are_values = fi.m().is_value(args[i]); + } + } + + func_entry * entry = fi.get_entry(args); + if (entry != 0) { + result = entry->get_result(); + return true; + } + + TRACE("func_interp", tout << "failed to find entry for: "; + for(unsigned i = 0; i < fi.get_arity(); i++) + tout << mk_pp(args[i], fi.m()) << " "; + tout << "\nis partial: " << fi.is_partial() << "\n";); + + if (!fi.eval_else(args, result)) { + return false; + } + + if (actuals_are_values && fi.args_are_values()) { + // cheap case... we are done + return true; + } + + // build symbolic result... the actuals may be equal to the args of one of the entries. + basic_simplifier_plugin * bs = static_cast(s.get_plugin(fi.m().get_basic_family_id())); + for (unsigned k = 0; k < fi.num_entries(); k++) { + func_entry const * curr = fi.get_entry(k); + SASSERT(!curr->eq_args(fi.get_arity(), args)); + if (!actuals_are_values || !curr->args_are_values()) { + expr_ref_buffer eqs(fi.m()); + unsigned i = fi.get_arity(); + while (i > 0) { + --i; + expr_ref new_eq(fi.m()); + bs->mk_eq(curr->get_arg(i), args[i], new_eq); + eqs.push_back(new_eq); + } + SASSERT(eqs.size() == fi.get_arity()); + expr_ref new_cond(fi.m()); + bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond); + bs->mk_ite(new_cond, curr->get_result(), result, result); + } + } + return true; +} + /** \brief Evaluate the expression e in the current model, and store the result in \c result. It returns \c true if succeeded, and false otherwise. If the evaluation fails, @@ -223,7 +280,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { SASSERT(fi->get_arity() == num_args); expr_ref r1(m_manager); // fi may be partial... - if (!fi->eval(m_simplifier, args.c_ptr(), r1)) { + if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) { SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial. if (model_completion) { expr * r = get_some_value(f->get_range()); diff --git a/src/model/proto_model.h b/src/smt/proto_model/proto_model.h similarity index 100% rename from src/model/proto_model.h rename to src/smt/proto_model/proto_model.h diff --git a/src/model/struct_factory.cpp b/src/smt/proto_model/struct_factory.cpp similarity index 100% rename from src/model/struct_factory.cpp rename to src/smt/proto_model/struct_factory.cpp diff --git a/src/model/struct_factory.h b/src/smt/proto_model/struct_factory.h similarity index 95% rename from src/model/struct_factory.h rename to src/smt/proto_model/struct_factory.h index 62e73589a..c9ba4e886 100644 --- a/src/model/struct_factory.h +++ b/src/smt/proto_model/struct_factory.h @@ -48,8 +48,6 @@ public: virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2); virtual void register_value(expr * array_value); - - proto_model & get_model() { return m_model; } }; #endif /* _STRUCT_FACTORY_H_ */ diff --git a/src/model/value_factory.cpp b/src/smt/proto_model/value_factory.cpp similarity index 100% rename from src/model/value_factory.cpp rename to src/smt/proto_model/value_factory.cpp diff --git a/src/model/value_factory.h b/src/smt/proto_model/value_factory.h similarity index 100% rename from src/model/value_factory.h rename to src/smt/proto_model/value_factory.h