From e4f29a7b8a1f8692b65d73b0a1dfe009df567b67 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Jan 2018 21:09:52 -0800 Subject: [PATCH] debugging mc Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 4 +- src/muz/base/dl_rule.cpp | 2 +- src/muz/fp/horn_tactic.cpp | 2 +- src/muz/transforms/dl_mk_bit_blast.cpp | 2 +- src/muz/transforms/dl_mk_coi_filter.cpp | 4 +- src/opt/opt_context.cpp | 4 +- src/opt/sortmax.cpp | 2 +- src/qe/qsat.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 4 +- src/solver/solver.cpp | 3 - src/solver/solver2tactic.cpp | 2 +- src/tactic/arith/card2bv_tactic.cpp | 2 +- src/tactic/arith/degree_shift_tactic.cpp | 2 +- src/tactic/arith/fix_dl_var_tactic.cpp | 2 +- src/tactic/arith/lia2pb_tactic.cpp | 2 +- src/tactic/arith/nla2bv_tactic.cpp | 2 +- src/tactic/arith/normalize_bounds_tactic.cpp | 2 +- src/tactic/arith/pb2bv_tactic.cpp | 2 +- src/tactic/arith/purify_arith_tactic.cpp | 4 +- src/tactic/arith/recover_01_tactic.cpp | 2 +- src/tactic/bv/bv_size_reduction_tactic.cpp | 6 +- src/tactic/bv/bvarray2uf_tactic.cpp | 2 +- src/tactic/bv/dt2bv_tactic.cpp | 3 +- src/tactic/core/elim_term_ite_tactic.cpp | 2 +- src/tactic/core/elim_uncnstr_tactic.cpp | 4 +- src/tactic/core/nnf_tactic.cpp | 2 +- src/tactic/core/occf_tactic.cpp | 2 +- src/tactic/core/reduce_args_tactic.cpp | 2 +- src/tactic/core/solve_eqs_tactic.cpp | 2 +- src/tactic/core/tseitin_cnf_tactic.cpp | 2 +- src/tactic/generic_model_converter.cpp | 35 +++++------ src/tactic/generic_model_converter.h | 3 +- src/tactic/model_converter.cpp | 1 + .../portfolio/bounded_int2bv_solver.cpp | 61 ++++++++++--------- src/tactic/portfolio/enum2bv_solver.cpp | 53 ++++++++++------ src/tactic/portfolio/pb2bv_solver.cpp | 31 +++++++--- src/tactic/ufbv/macro_finder_tactic.cpp | 2 +- src/tactic/ufbv/quasi_macros_tactic.cpp | 2 +- 38 files changed, 143 insertions(+), 123 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 93d83d2a4..0b2decec8 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -864,7 +864,7 @@ void cmd_context::insert(symbol const & s, object_ref * r) { } void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t) { - if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m()); + if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m(), "cmd_context"); if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get()); func_decl_ref fn(m().mk_func_decl(s, arity, domain, m().get_sort(t)), m()); dictionary::entry * e = m_func_decls.insert_if_not_there2(s, func_decls()); @@ -874,7 +874,7 @@ void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domai } void cmd_context::model_del(func_decl* f) { - if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m()); + if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m(), "model_del"); if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get()); m_mc0->hide(f); } diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index c188426f0..c74b9cfc4 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -326,7 +326,7 @@ namespace datalog { rules.set_output_predicate(qpred); if (m_ctx.get_model_converter()) { - generic_model_converter* mc = alloc(generic_model_converter, m); + generic_model_converter* mc = alloc(generic_model_converter, m, "dl_rule"); mc->hide(qpred); m_ctx.add_model_converter(mc); } diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 881ae9aec..5027e42cf 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -225,7 +225,7 @@ class horn_tactic : public tactic { } queries.reset(); queries.push_back(q); - generic_model_converter* mc1 = alloc(generic_model_converter, m); + generic_model_converter* mc1 = alloc(generic_model_converter, m, "horn"); mc1->hide(q); g->add(mc1); } diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 7f3ae43f3..4d4c22780 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -299,7 +299,7 @@ namespace datalog { } if (m_context.get_model_converter()) { - generic_model_converter* fmc = alloc(generic_model_converter, m); + generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast"); bit_blast_model_converter* bvmc = alloc(bit_blast_model_converter, m); func_decl_ref_vector const& old_funcs = m_rewriter.m_cfg.old_funcs(); func_decl_ref_vector const& new_funcs = m_rewriter.m_cfg.new_funcs(); diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index a75c08ec4..afaf5ba19 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -90,7 +90,7 @@ namespace datalog { // set to false each unreached predicate if (m_context.get_model_converter()) { - generic_model_converter* mc0 = alloc(generic_model_converter, m); + generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi"); for (auto const& kv : engine) { if (!kv.m_value.is_reachable()) { mc0->add(kv.m_key, m.mk_false()); @@ -127,7 +127,7 @@ namespace datalog { if (res && m_context.get_model_converter()) { func_decl_set::iterator end = pruned_preds.end(); func_decl_set::iterator it = pruned_preds.begin(); - generic_model_converter* mc0 = alloc(generic_model_converter, m); + generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi"); for (; it != end; ++it) { const rule_vector& rules = source.get_predicate_rules(*it); expr_ref_vector fmls(m); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 7cb2c6034..9e72d24dc 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -126,7 +126,7 @@ namespace opt { m_box_index(UINT_MAX), m_optsmt(m), m_scoped_state(m), - m_fm(m), + m_fm(m, "opt"), m_objective_refs(m), m_enable_sat(false), m_is_clausal(false), @@ -1062,7 +1062,7 @@ namespace opt { std::ostringstream out; out << mk_pp(term, m); app* q = m.mk_fresh_const(out.str().c_str(), m.get_sort(term)); - if (!fm) fm = alloc(generic_model_converter, m); + if (!fm) fm = alloc(generic_model_converter, m, "opt"); m_hard_constraints.push_back(m.mk_eq(q, term)); fm->hide(q); return q; diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index 18c3edc76..966fe12db 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -50,7 +50,7 @@ namespace opt { if (is_sat != l_true) { return is_sat; } - m_filter = alloc(generic_model_converter, m); + m_filter = alloc(generic_model_converter, m, "sortmax"); rational offset = m_lower; m_upper = offset; expr_ref_vector in(m); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 2e78574ec..a5ef4e94d 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -44,7 +44,7 @@ namespace qe { m(m), m_asms(m), m_trail(m), - m_fmc(alloc(generic_model_converter, m)) + m_fmc(alloc(generic_model_converter, m, "qsat")) { } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 0b9f9805a..2dfcb7bb8 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -900,7 +900,7 @@ void sat2goal::mc::flush_gmc() { sat::literal_vector updates; m_smc.expand(updates); m_smc.reset(); - if (!m_gmc) m_gmc = alloc(generic_model_converter, m); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); // now gmc owns the model converter sat::literal_vector clause; expr_ref_vector tail(m); @@ -1018,7 +1018,7 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { if (aux) { SASSERT(is_uninterp_const(atom)); SASSERT(m.is_bool(atom)); - if (!m_gmc) m_gmc = alloc(generic_model_converter, m); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); m_gmc->hide(atom->get_decl()); } } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 9fbaa8032..356eaf2ed 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -43,7 +43,6 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum get_assertions(fmls); ast_pp_util visitor(get_manager()); model_converter_ref mc = get_model_converter(); - mc = concat(mc0(), mc.get()); if (mc.get()) { mc->collect(visitor); } @@ -180,7 +179,6 @@ void solver::assert_expr(expr* f) { expr_ref fml(f, get_manager()); if (m_enforce_model_conversion) { model_converter_ref mc = get_model_converter(); - mc = concat(mc0(), mc.get()); if (mc) { (*mc)(fml); } @@ -196,7 +194,6 @@ void solver::assert_expr(expr* f, expr* t) { IF_VERBOSE(0, verbose_stream() << "enforce model conversion\n";); exit(0); model_converter_ref mc = get_model_converter(); - mc = concat(mc0(), mc.get()); if (mc) { (*mc)(fml); // (*mc)(a); diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 6863c935e..ecf676bc6 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -65,7 +65,7 @@ void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clause bool2dep.insert(b, d); assumptions.push_back(b); if (!fmc) { - fmc = alloc(generic_model_converter, m); + fmc = alloc(generic_model_converter, m, "solver2tactic"); } fmc->hide(to_app(b)->get_decl()); } diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 6349c40b2..36a73198d 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -86,7 +86,7 @@ public: func_decl_ref_vector const& fns = rw2.fresh_constants(); if (!fns.empty()) { - generic_model_converter* filter = alloc(generic_model_converter, m); + generic_model_converter* filter = alloc(generic_model_converter, m, "card2bv"); for (func_decl* f : fns) filter->hide(f); g->add(filter); } diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index 704d48eac..4e9a39a97 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -198,7 +198,7 @@ class degree_shift_tactic : public tactic { SASSERT(!m_var2degree.empty()); generic_model_converter * xmc = 0; if (m_produce_models) { - xmc = alloc(generic_model_converter, m); + xmc = alloc(generic_model_converter, m, "degree_shift"); mc = xmc; } for (auto const& kv : m_var2degree) { diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index fe1b64e90..45ff10953 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -266,7 +266,7 @@ class fix_dl_var_tactic : public tactic { m_rw.set_substitution(&subst); if (m_produce_models) { - generic_model_converter * mc = alloc(generic_model_converter, m); + generic_model_converter * mc = alloc(generic_model_converter, m, "fix_dl"); mc->add(var, zero); g->add(mc); } diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 274c6dd40..9d62e6dc4 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -222,7 +222,7 @@ class lia2pb_tactic : public tactic { ref gmc; if (m_produce_models) { - gmc = alloc(generic_model_converter, m); + gmc = alloc(generic_model_converter, m, "lia2pb"); } expr_ref zero(m); diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index f7c985129..9eca330cd 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -85,7 +85,7 @@ class nla2bv_tactic : public tactic { TRACE("nla2bv", g.display(tout); tout << "Muls: " << count_mul(g) << "\n"; ); - m_fmc = alloc(generic_model_converter, m_manager); + m_fmc = alloc(generic_model_converter, m_manager, "nla2bv"); m_bounds(g); collect_power2(g); if(!collect_vars(g)) { diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index 130b5cfe6..a4454679c 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -94,7 +94,7 @@ class normalize_bounds_tactic : public tactic { generic_model_converter * gmc = 0; if (produce_models) { - gmc = alloc(generic_model_converter, m); + gmc = alloc(generic_model_converter, m, "normalize_bounds"); in->add(gmc); } diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index de4fa8221..14593c9a8 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -947,7 +947,7 @@ private: if (m_produce_models) { model_converter_ref mc; - generic_model_converter * mc1 = alloc(generic_model_converter, m); + generic_model_converter * mc1 = alloc(generic_model_converter, m, "pb2bv"); for (auto const& kv : m_const2bit) mc1->hide(kv.m_value); // store temp int constants in the filter diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 692d6ab6d..a75e0dc52 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -765,7 +765,7 @@ struct purify_arith_proc { // add generic_model_converter to eliminate auxiliary variables from model if (produce_models) { - generic_model_converter * fmc = alloc(generic_model_converter, m()); + generic_model_converter * fmc = alloc(generic_model_converter, m(), "purify"); mc = fmc; obj_map & f2v = r.cfg().m_app2fresh; for (auto const& kv : f2v) { @@ -775,7 +775,7 @@ struct purify_arith_proc { } } if (produce_models && !m_sin_cos.empty()) { - generic_model_converter* emc = alloc(generic_model_converter, m()); + generic_model_converter* emc = alloc(generic_model_converter, m(), "purify_sin_cos"); mc = concat(mc.get(), emc); obj_map >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end(); for (; it != end; ++it) { diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 7645f34cd..4e1727139 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -325,7 +325,7 @@ class recover_01_tactic : public tactic { } if (m_produce_models) { - gmc = alloc(generic_model_converter, m); + gmc = alloc(generic_model_converter, m, "recover_01"); new_goal->add(gmc); } diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 8c4ea22ad..5577b3dfe 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -265,10 +265,10 @@ struct bv_size_reduction_tactic::imp { subst.insert(v, new_def); if (m_produce_models) { if (!m_mc) - m_mc = alloc(bv_size_reduction_mc, m); + m_mc = alloc(bv_size_reduction_mc, m, "bv_size_reduction"); m_mc->add(v, new_def); if (!m_fmc && new_const) - m_fmc = alloc(generic_model_converter, m); + m_fmc = alloc(generic_model_converter, m, "bv_size_reduction"); if (new_const) m_fmc->hide(new_const); } @@ -334,7 +334,7 @@ struct bv_size_reduction_tactic::imp { m_mc = alloc(bv_size_reduction_mc, m); m_mc->insert(v->get_decl(), new_def); if (!m_fmc && new_const) - m_fmc = alloc(generic_model_converter, m); + m_fmc = alloc(generic_model_converter, m, "bv_size_reduction"); if (new_const) m_fmc->hide(new_const); } diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 7718a9679..0636c74cf 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -65,7 +65,7 @@ class bvarray2uf_tactic : public tactic { model_converter_ref mc; if (m_produce_models) { - generic_model_converter * fmc = alloc(generic_model_converter, m_manager); + generic_model_converter * fmc = alloc(generic_model_converter, m_manager, "bvarray2uf"); mc = fmc; m_rw.set_mcs(fmc); } diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index bbfbe02fd..f8456e12b 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -25,7 +25,6 @@ Revision History: #include "ast/datatype_decl_plugin.h" #include "ast/bv_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" -#include "tactic/generic_model_converter.h" #include "ast/rewriter/var_subst.h" #include "ast/ast_util.h" #include "ast/rewriter/enum2bv_rewriter.h" @@ -128,7 +127,7 @@ public: for (sort* s : m_non_fd_sorts) m_fd_sorts.remove(s); if (!m_fd_sorts.empty()) { - ref filter = alloc(generic_model_converter, m); + ref filter = alloc(generic_model_converter, m, "dt2bv"); enum2bv_rewriter rw(m, m_params); rw.set_is_fd(&m_is_fd); expr_ref new_curr(m); diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index e4e337e00..49815b6d1 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -55,7 +55,7 @@ class elim_term_ite_tactic : public tactic { m_num_fresh++; if (m_produce_models) { if (!m_mc) - m_mc = alloc(generic_model_converter, m); + m_mc = alloc(generic_model_converter, m, "elim_term_ite"); m_mc->hide(_result->get_decl()); } } diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index cc5402e41..2f961f9bc 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -808,7 +808,7 @@ class elim_uncnstr_tactic : public tactic { m_mc = 0; return; } - m_mc = alloc(mc, m()); + m_mc = alloc(mc, m(), "elim_uncstr"); } void init_rw(bool produce_proofs) { @@ -867,7 +867,7 @@ class elim_uncnstr_tactic : public tactic { app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars; m_num_elim_apps = fresh_vars.size(); if (produce_models && !fresh_vars.empty()) { - generic_model_converter * fmc = alloc(generic_model_converter, m()); + generic_model_converter * fmc = alloc(generic_model_converter, m(), "elim_uncnstr"); for (app * f : fresh_vars) fmc->hide(f); g->add(concat(fmc, m_mc.get())); diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index c13f49b52..b6bab648c 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -93,7 +93,7 @@ public: result.push_back(g.get()); unsigned num_extra_names = dnames.get_num_names(); if (num_extra_names > 0) { - generic_model_converter * fmc = alloc(generic_model_converter, m); + generic_model_converter * fmc = alloc(generic_model_converter, m, "nnf"); g->add(fmc); for (unsigned i = 0; i < num_extra_names; i++) fmc->hide(dnames.get_name_decl(i)); diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index e875a0472..86e776081 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -153,7 +153,7 @@ class occf_tactic : public tactic { if (!is_target(cls)) continue; if (produce_models && !m_mc) { - m_mc = alloc(generic_model_converter, m); + m_mc = alloc(generic_model_converter, m, "occf"); g->add(m_mc); } expr * keep = 0; diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 1e7baa14f..ac4a009e9 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -393,7 +393,7 @@ struct reduce_args_tactic::imp { ptr_buffer new_args; var_ref_vector new_vars(m_manager); ptr_buffer new_eqs; - generic_model_converter * f_mc = alloc(generic_model_converter, m_manager); + generic_model_converter * f_mc = alloc(generic_model_converter, m_manager, "reduce_args"); for (auto const& kv : decl2arg2funcs) { func_decl * f = kv.m_key; arg2func * map = kv.m_value; diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 22b87d60e..5fbf9aaf5 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -606,7 +606,7 @@ class solve_eqs_tactic : public tactic { m_num_eliminated_vars += m_ordered_vars.size(); if (m_produce_models) { if (mc.get() == 0) - mc = alloc(gmc, m()); + mc = alloc(gmc, m(), "solve_eqs"); for (app * v : m_ordered_vars) { expr * def = 0; proof * pr; diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index 91f974eb9..eae724c7a 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -813,7 +813,7 @@ class tseitin_cnf_tactic : public tactic { m_frame_stack.reset(); m_clauses.reset(); if (m_produce_models) - m_mc = alloc(generic_model_converter, m); + m_mc = alloc(generic_model_converter, m, "tseitin"); else m_mc = 0; diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index aa1f1cdc4..4f48c78e1 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -29,6 +29,7 @@ Notes: void generic_model_converter::add(func_decl * d, expr* e) { + VERIFY(e); struct entry et(d, e, m, ADD); VERIFY(d->get_range() == m.get_sort(e)); m_first_idx.insert_if_not_there(et.m_f, m_entries.size()); @@ -39,9 +40,10 @@ void generic_model_converter::operator()(model_ref & md) { TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout);); model_evaluator ev(*(md.get())); ev.set_model_completion(true); - ev.set_expand_array_equalities(false); + ev.set_expand_array_equalities(false); expr_ref val(m); unsigned arity; + bool reset_ev = false; for (unsigned i = m_entries.size(); i-- > 0; ) { entry const& e = m_entries[i]; switch (e.m_instruction) { @@ -50,32 +52,16 @@ void generic_model_converter::operator()(model_ref & md) { break; case instruction::ADD: ev(e.m_def, val); -#if 0 - if (e.m_f->get_name() == symbol("XX")) { - IF_VERBOSE(0, verbose_stream() << e.m_f->get_name() << " " << e.m_def << " -> " << val << "\n";); - ptr_vector ts; - ts.push_back(e.m_def); - while (!ts.empty()) { - app* t = to_app(ts.back()); - ts.pop_back(); - if (t->get_num_args() > 0) { - ts.append(t->get_num_args(), t->get_args()); - } - expr_ref tmp(m); - ev(t, tmp); - IF_VERBOSE(0, verbose_stream() << mk_pp(t, m) << " -> " << tmp << "\n";); - } - } -#endif TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";); arity = e.m_f->get_arity(); + reset_ev = false; if (arity == 0) { expr* old_val = md->get_const_interp(e.m_f); if (old_val && old_val == val) { // skip } else { - if (old_val) ev.reset(); + reset_ev = old_val != nullptr; md->register_decl(e.m_f, val); } } @@ -85,12 +71,17 @@ void generic_model_converter::operator()(model_ref & md) { // skip } else { - if (old_val) ev.reset(); + reset_ev = old_val != nullptr; func_interp * new_fi = alloc(func_interp, m, arity); new_fi->set_else(val); md->register_decl(e.m_f, new_fi); } } + if (reset_ev) { + ev.reset(); + ev.set_model_completion(true); + ev.set_expand_array_equalities(false); + } break; } } @@ -98,7 +89,9 @@ void generic_model_converter::operator()(model_ref & md) { } void generic_model_converter::display(std::ostream & out) { + unsigned i = 0; for (entry const& e : m_entries) { + ++i; switch (e.m_instruction) { case instruction::HIDE: display_del(out, e.m_f); @@ -112,7 +105,7 @@ void generic_model_converter::display(std::ostream & out) { model_converter * generic_model_converter::translate(ast_translation & translator) { ast_manager& to = translator.to(); - generic_model_converter * res = alloc(generic_model_converter, to); + generic_model_converter * res = alloc(generic_model_converter, to, m_orig.c_str()); for (entry const& e : m_entries) { res->m_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction)); } diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index 8d40d55b7..a85cc9766 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -39,13 +39,14 @@ class generic_model_converter : public model_converter { } }; ast_manager& m; + std::string m_orig; vector m_entries; obj_map m_first_idx; expr_ref simplify_def(entry const& e); public: - generic_model_converter(ast_manager & m) : m(m) {} + generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {} virtual ~generic_model_converter() { } diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 161666d01..6c77d91b6 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -24,6 +24,7 @@ Notes: * Add or overwrite value in model. */ void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const { + VERIFY(e); smt2_pp_environment_dbg env(m); smt2_pp_environment* _env = m_env ? m_env : &env; VERIFY(f->get_range() == m.get_sort(e)); diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 3e1b5d2f4..ee6630fd3 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -81,9 +81,10 @@ public: for (func_decl* f : m_bv_fns) result->m_bv_fns.push_back(tr(f)); for (func_decl* f : m_int_fns) result->m_int_fns.push_back(tr(f)); for (bound_manager* b : m_bounds) result->m_bounds.push_back(b->translate(dst_m)); - if (mc0()) { + model_converter_ref mc = external_model_converter(); + if (mc) { ast_translation tr(m, dst_m); - result->set_model_converter(mc0()->translate(tr)); + result->set_model_converter(mc->translate(tr)); } return result; } @@ -151,11 +152,36 @@ public: virtual void get_model_core(model_ref & mdl) { m_solver->get_model(mdl); if (mdl) { - extend_model(mdl); - filter_model(mdl); + model_converter_ref mc = bounded_model_converter(); + if (mc) (*mc)(mdl); } } - virtual model_converter_ref get_model_converter() const { return m_solver->get_model_converter(); } + model_converter* external_model_converter() const { + return concat(mc0(), bounded_model_converter()); + } + model_converter* bounded_model_converter() const { + if (m_int2bv.empty() && m_bv_fns.empty()) return nullptr; + generic_model_converter* mc = alloc(generic_model_converter, m, "bounded_int2bv"); + for (func_decl* f : m_bv_fns) + mc->hide(f); + for (auto const& kv : m_int2bv) { + rational offset; + VERIFY (m_bv2offset.find(kv.m_value, offset)); + expr_ref value(m_bv.mk_bv2int(m.mk_const(kv.m_value)), m); + if (!offset.is_zero()) { + value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true)); + } + TRACE("int2bv", tout << mk_pp(kv.m_key, m) << " " << value << "\n";); + mc->add(kv.m_key, value); + } + return mc; + } + + virtual model_converter_ref get_model_converter() const { + model_converter_ref mc = concat(mc0(), bounded_model_converter()); + mc = concat(mc.get(), m_solver->get_model_converter().get()); + return mc; + } virtual proof * get_proof() { return m_solver->get_proof(); } virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } @@ -198,35 +224,10 @@ public: } } return r; - } private: - void filter_model(model_ref& mdl) const { - if (m_bv_fns.empty()) { - return; - } - generic_model_converter filter(m); - for (func_decl* f : m_bv_fns) filter.hide(f); - filter(mdl); - } - - void extend_model(model_ref& mdl) { - generic_model_converter ext(m); - for (auto const& kv : m_int2bv) { - rational offset; - VERIFY (m_bv2offset.find(kv.m_value, offset)); - expr_ref value(m_bv.mk_bv2int(m.mk_const(kv.m_value)), m); - if (!offset.is_zero()) { - value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true)); - } - TRACE("int2bv", tout << mk_pp(kv.m_key, m) << " " << value << "\n";); - ext.add(kv.m_key, value); - } - ext(mdl); - } - void accumulate_sub(expr_safe_replace& sub) const { for (unsigned i = 0; i < m_bounds.size(); ++i) { accumulate_sub(sub, *m_bounds[i]); diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 5db907c2c..9567f369f 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -50,9 +50,10 @@ public: virtual solver* translate(ast_manager& dst_m, params_ref const& p) { solver* result = alloc(enum2bv_solver, dst_m, p, m_solver->translate(dst_m, p)); - if (mc0()) { + model_converter_ref mc = external_model_converter(); + if (mc) { ast_translation tr(m, dst_m); - result->set_model_converter(mc0()->translate(tr)); + result->set_model_converter(mc->translate(tr)); } return result; } @@ -91,18 +92,43 @@ public: virtual void get_model_core(model_ref & mdl) { m_solver->get_model(mdl); if (mdl) { - extend_model(mdl); - filter_model(mdl); + model_converter_ref mc = enum_model_converter(); + if (mc) (*mc)(mdl); } } - virtual model_converter_ref get_model_converter() const { return m_solver->get_model_converter(); } + model_converter* enum_model_converter() const { + if (m_rewriter.enum2def().empty() && + m_rewriter.enum2bv().empty()) { + return nullptr; + } + generic_model_converter* mc = alloc(generic_model_converter, m, "enum2bv"); + for (auto const& kv : m_rewriter.enum2bv()) + mc->hide(kv.m_value); + for (auto const& kv : m_rewriter.enum2def()) + mc->add(kv.m_key, kv.m_value); + return mc; + } + + model_converter* external_model_converter() const { + return concat(mc0(), enum_model_converter()); + } + + virtual model_converter_ref get_model_converter() const { + model_converter_ref mc = external_model_converter(); + mc = concat(mc.get(), m_solver->get_model_converter().get()); + return mc; + } virtual proof * get_proof() { return m_solver->get_proof(); } virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } - virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } - virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { return m_solver->cube(vars, backtrack_level); } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { + return m_solver->find_mutexes(vars, mutexes); + } + virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { + return m_solver->cube(vars, backtrack_level); + } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { datatype_util dt(m); @@ -152,20 +178,7 @@ public: return r; } - void filter_model(model_ref& mdl) { - generic_model_converter filter(m); - for (auto const& kv : m_rewriter.enum2bv()) { - filter.hide(kv.m_value); - } - filter(mdl); - } - void extend_model(model_ref& mdl) { - generic_model_converter ext(m); - for (auto const& kv : m_rewriter.enum2def()) - ext.add(kv.m_key, kv.m_value); - ext(mdl); - } virtual unsigned get_num_assertions() const { return m_solver->get_num_assertions(); diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index cee566ec6..6660e1bb4 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -50,9 +50,10 @@ public: virtual solver* translate(ast_manager& dst_m, params_ref const& p) { flush_assertions(); solver* result = alloc(pb2bv_solver, dst_m, p, m_solver->translate(dst_m, p)); - if (mc0()) { + model_converter_ref mc = external_model_converter(); + if (mc.get()) { ast_translation tr(m, dst_m); - result->set_model_converter(mc0()->translate(tr)); + result->set_model_converter(mc->translate(tr)); } return result; } @@ -93,7 +94,14 @@ public: filter_model(mdl); } } - virtual model_converter_ref get_model_converter() const { return m_solver->get_model_converter(); } + model_converter* external_model_converter() const { + return concat(mc0(), filter_model_converter()); + } + virtual model_converter_ref get_model_converter() const { + model_converter_ref mc = concat(mc0(), filter_model_converter()); + mc = concat(mc.get(), m_solver->get_model_converter().get()); + return mc; + } virtual proof * get_proof() { return m_solver->get_proof(); } virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } @@ -105,16 +113,23 @@ public: flush_assertions(); return m_solver->get_consequences(asms, vars, consequences); } - void filter_model(model_ref& mdl) { + model_converter* filter_model_converter() const { if (m_rewriter.fresh_constants().empty()) { - return; + return nullptr; } - generic_model_converter filter(m); + generic_model_converter* filter = alloc(generic_model_converter, m, "pb2bv"); func_decl_ref_vector const& fns = m_rewriter.fresh_constants(); for (func_decl* f : fns) { - filter.hide(f); + filter->hide(f); + } + return filter; + } + + void filter_model(model_ref& mdl) { + model_converter_ref mc = filter_model_converter(); + if (mc.get()) { + (*mc)(mdl); } - filter(mdl); } virtual unsigned get_num_assertions() const { diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index efed67486..62c1d0340 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -65,7 +65,7 @@ class macro_finder_tactic : public tactic { produce_proofs ? new_proofs.get(i) : 0, unsat_core_enabled ? new_deps.get(i) : 0); - generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager()); + generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager(), "macro_finder"); unsigned num = mm.get_num_macros(); for (unsigned i = 0; i < num; i++) { expr_ref f_interp(mm.get_manager()); diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 05c5bdd73..93e893f89 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -77,7 +77,7 @@ class quasi_macros_tactic : public tactic { produce_proofs ? proofs.get(i) : 0, produce_unsat_cores ? deps.get(i) : 0); - generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager()); + generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager(), "quasi_macros"); unsigned num = mm.get_num_macros(); for (unsigned i = 0; i < num; i++) { expr_ref f_interp(mm.get_manager());