diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index a91a681d9..ab711dde7 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -578,6 +578,16 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return st; } + expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args) { + expr_ref result(m()); + proof_ref pr(m()); + if (BR_FAILED == reduce_app(f, num_args, args, result, pr)) { + result = m().mk_app(f, num_args, args); + } + return result; + } + + bool reduce_quantifier(quantifier * old_q, expr * new_body, expr * const * new_patterns, @@ -695,6 +705,9 @@ struct th_rewriter::imp : public rewriter_tpl { rewriter_tpl(m, m.proofs_enabled(), m_cfg), m_cfg(m, p) { } + expr_ref mk_app(func_decl* f, unsigned sz, expr* const* args) { + return m_cfg.mk_app(f, sz, args); + } }; th_rewriter::th_rewriter(ast_manager & m, params_ref const & p): @@ -776,3 +789,7 @@ void th_rewriter::reset_used_dependencies() { m_imp->cfg().m_used_dependencies = 0; } } + +expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args) { + return m_imp->mk_app(f, num_args, args); +} diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index 222625077..bd5ce9c66 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -45,6 +45,8 @@ public: void operator()(expr * t, expr_ref & result, proof_ref & result_pr); void operator()(expr * n, unsigned num_bindings, expr * const * bindings, expr_ref & result); + expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args); + void cleanup(); void reset(); diff --git a/src/model/model_params.pyg b/src/model/model_params.pyg index dfa3748bc..14e83952c 100644 --- a/src/model/model_params.pyg +++ b/src/model/model_params.pyg @@ -4,6 +4,5 @@ def_module_params('model', ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'), ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'), ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'), - ('new_eval', BOOL, True, 'use new evaluator (temporary parameter for testing)'), )) diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 609f5d47b..22e9770e0 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -66,7 +66,7 @@ void display_usage() { #ifdef Z3GITHASH std::cout << " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH); #endif - std::cout << "]. (C) Copyright 2006-2014 Microsoft Corp.\n"; + std::cout << "]. (C) Copyright 2006-2016 Microsoft Corp.\n"; std::cout << "Usage: z3 [options] [-file:]file\n"; std::cout << "\nInput format:\n"; std::cout << " -smt use parser for SMT input format.\n"; diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index cb6b8c68d..cfc037a68 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -25,19 +25,17 @@ 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, params_ref const & p): +proto_model::proto_model(ast_manager & m, params_ref const & p): model_core(m), - m_simplifier(s), m_afid(m.mk_family_id(symbol("array"))), - m_eval(*this) { + m_eval(*this), + m_rewrite(m) { register_factory(alloc(basic_factory, m)); m_user_sort_factory = alloc(user_sort_factory, m); register_factory(m_user_sort_factory); m_model_partial = model_params(p).partial(); - m_use_new_eval = model_params(p).new_eval(); } @@ -85,61 +83,6 @@ 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.m(), 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; -} bool proto_model::is_select_of_model_value(expr* e) const { return @@ -159,192 +102,16 @@ bool proto_model::is_select_of_model_value(expr* e) const { So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers. */ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { - if (m_use_new_eval) { - m_eval.set_model_completion(model_completion); - try { - m_eval(e, result); - return true; - } - catch (model_evaluator_exception & ex) { - (void)ex; - TRACE("model_evaluator", tout << ex.msg() << "\n";); - return false; - } + m_eval.set_model_completion(model_completion); + try { + m_eval(e, result); + return true; } - - bool is_ok = true; - SASSERT(is_well_sorted(m_manager, e)); - TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n"; - tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";); - - obj_map eval_cache; - expr_ref_vector trail(m_manager); - sbuffer, 128> todo; - ptr_buffer args; - expr * null = static_cast(0); - todo.push_back(std::make_pair(e, null)); - - - expr * a; - expr * expanded_a; - while (!todo.empty()) { - std::pair & p = todo.back(); - a = p.first; - expanded_a = p.second; - if (expanded_a != 0) { - expr * r = 0; - eval_cache.find(expanded_a, r); - SASSERT(r != 0); - todo.pop_back(); - eval_cache.insert(a, r); - TRACE("model_eval", - tout << "orig:\n" << mk_pp(a, m_manager) << "\n"; - tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n"; - tout << "new:\n" << mk_pp(r, m_manager) << "\n";); - } - else { - switch(a->get_kind()) { - case AST_APP: { - app * t = to_app(a); - bool visited = true; - args.reset(); - unsigned num_args = t->get_num_args(); - for (unsigned i = 0; i < num_args; ++i) { - expr * arg = 0; - if (!eval_cache.find(t->get_arg(i), arg)) { - visited = false; - todo.push_back(std::make_pair(t->get_arg(i), null)); - } - else { - args.push_back(arg); - } - } - if (!visited) { - continue; - } - SASSERT(args.size() == t->get_num_args()); - expr_ref new_t(m_manager); - func_decl * f = t->get_decl(); - - if (!has_interpretation(f)) { - // the model does not assign an interpretation to f. - SASSERT(new_t.get() == 0); - if (f->get_family_id() == null_family_id) { - if (model_completion) { - // create an interpretation for f. - new_t = mk_some_interp_for(f); - } - else { - TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";); - is_ok = false; - } - } - if (new_t.get() == 0) { - // t is interpreted or model completion is disabled. - m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t); - TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";); - trail.push_back(new_t); - if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) { - // if the result is not of the form (f ...), then assume we must simplify it. - expr * new_new_t = 0; - if (!eval_cache.find(new_t.get(), new_new_t)) { - todo.back().second = new_t; - todo.push_back(std::make_pair(new_t, null)); - continue; - } - else { - new_t = new_new_t; - } - } - } - } - else { - // the model has an interpretaion for f. - if (num_args == 0) { - // t is a constant - new_t = get_const_interp(f); - } - else { - // t is a function application - SASSERT(new_t.get() == 0); - // try to use function graph first - func_interp * fi = get_func_interp(f); - SASSERT(fi->get_arity() == num_args); - expr_ref r1(m_manager); - // fi may be partial... - 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()); - fi->set_else(r); - SASSERT(!fi->is_partial()); - new_t = r; - } - else { - // f is an uninterpreted function, there is no need to use m_simplifier.mk_app - new_t = m_manager.mk_app(f, num_args, args.c_ptr()); - trail.push_back(new_t); - TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";); - is_ok = false; - } - } - else { - SASSERT(r1); - trail.push_back(r1); - TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";); - expr * r2 = 0; - if (!eval_cache.find(r1.get(), r2)) { - todo.back().second = r1; - todo.push_back(std::make_pair(r1, null)); - continue; - } - else { - new_t = r2; - } - } - } - } - TRACE("model_eval", - tout << "orig:\n" << mk_pp(t, m_manager) << "\n"; - tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";); - todo.pop_back(); - SASSERT(new_t.get() != 0); - eval_cache.insert(t, new_t); - break; - } - case AST_VAR: - SASSERT(a != 0); - eval_cache.insert(a, a); - todo.pop_back(); - break; - case AST_QUANTIFIER: - TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";); - is_ok = false; // evaluator does not handle quantifiers. - SASSERT(a != 0); - eval_cache.insert(a, a); - todo.pop_back(); - break; - default: - UNREACHABLE(); - break; - } - } + catch (model_evaluator_exception & ex) { + (void)ex; + TRACE("model_evaluator", tout << ex.msg() << "\n";); + return false; } - - if (!eval_cache.find(e, a)) { - TRACE("model_eval", tout << "FAILED e: " << mk_bounded_pp(e, m_manager) << "\n";); - UNREACHABLE(); - } - - result = a; - TRACE("model_eval", - ast_ll_pp(tout << "original: ", m_manager, e); - ast_ll_pp(tout << "evaluated: ", m_manager, a); - ast_ll_pp(tout << "reduced: ", m_manager, result.get()); - tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n"; - ); - SASSERT(is_well_sorted(m_manager, result.get())); - return is_ok; } /** @@ -400,7 +167,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au if (m_aux_decls.contains(f)) found_aux_fs.insert(f); expr_ref new_t(m_manager); - m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t); + new_t = m_rewrite.mk_app(f, num_args, args.c_ptr()); if (t != new_t.get()) trail.push_back(new_t); todo.pop_back(); diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index 2c27ac39a..78dc457f5 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -32,23 +32,22 @@ Revision History: #include"model_evaluator.h" #include"value_factory.h" #include"plugin_manager.h" -#include"simplifier.h" #include"arith_decl_plugin.h" #include"func_decl_dependencies.h" #include"model.h" #include"params.h" +#include"th_rewriter.h" class proto_model : public model_core { plugin_manager m_factories; user_sort_factory * m_user_sort_factory; - simplifier & m_simplifier; family_id m_afid; //!< array family id: hack for displaying models in V1.x style func_decl_set m_aux_decls; ptr_vector m_tmp; model_evaluator m_eval; + th_rewriter m_rewrite; bool m_model_partial; - bool m_use_new_eval; expr * mk_some_interp_for(func_decl * d); @@ -62,7 +61,7 @@ class proto_model : public model_core { bool is_select_of_model_value(expr* e) const; public: - proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref()); + proto_model(ast_manager & m, params_ref const & p = params_ref()); virtual ~proto_model() {} void register_factory(value_factory * f) { m_factories.register_plugin(f); } diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 42fb8f1b5..21a310a42 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -49,7 +49,7 @@ namespace smt { void model_generator::init_model() { SASSERT(!m_model); // PARAM-TODO smt_params ---> params_ref - m_model = alloc(proto_model, m_manager, m_context->get_simplifier()); // , m_context->get_fparams()); + m_model = alloc(proto_model, m_manager); // , m_context->get_fparams()); ptr_vector::const_iterator it = m_context->begin_theories(); ptr_vector::const_iterator end = m_context->end_theories(); for (; it != end; ++it) {