From f04e805fa4da46c5a305fb6a6fab773c34140a61 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Mar 2018 18:02:37 -0800 Subject: [PATCH] add hiding to auxiliary declarations created in mc Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 4 +++- src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 3 +++ src/cmd_context/cmd_context.cpp | 3 ++- src/sat/sat_asymm_branch.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 8 ++++---- src/tactic/generic_model_converter.cpp | 7 +++++-- src/tactic/generic_model_converter.h | 2 +- src/tactic/model_converter.cpp | 2 +- 8 files changed, 20 insertions(+), 11 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index ba591083f..8d35ae8bb 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1718,11 +1718,13 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); +#if 0 static unsigned count = 0; - if (n->m_id == 404) { + if (n->m_id == 1293522) { ++count; //if (count == 2) SASSERT(false); } +#endif TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 3573d44f3..bcef44440 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -15,6 +15,9 @@ Author: Notes: + TBD: also keep track of which fresh constants are introduced + to instruct model converter to delete them. + --*/ #include "ast/rewriter/bit_blaster/bit_blaster_rewriter.h" #include "ast/bv_decl_plugin.h" diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f82f8868d..ddcaa0b03 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -870,11 +870,12 @@ void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domai dictionary::entry * e = m_func_decls.insert_if_not_there2(s, func_decls()); func_decls & fs = e->get_data().m_value; fs.insert(m(), fn); + VERIFY(fn->get_range() == m().get_sort(t)); m_mc0->add(fn, t); } void cmd_context::model_del(func_decl* f) { - if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m(), "model_del"); + 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()); m_mc0->hide(f); } diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 5822d7cef..35d594b34 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -245,7 +245,7 @@ namespace sat { m_pos.push_back(l); m_neg.push_back(~l); } -#if 0 +#if 1 compare_left cmp(big); std::sort(m_pos.begin(), m_pos.end(), cmp); std::sort(m_neg.begin(), m_neg.end(), cmp); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 87742d27a..1b0e0ebae 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -142,7 +142,6 @@ struct goal2sat::imp { sat::bool_var v = m_solver.mk_var(ext); m_map.insert(t, v); l = sat::literal(v, sign); - // if (to_app(t)->get_decl()->get_name() == "XX") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(t, m) << ": " << "v" << v << "\n";); TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";); if (ext && !is_uninterp_const(t)) { m_interpreted_atoms.push_back(t); @@ -1051,8 +1050,9 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { expr_ref sat2goal::mc::lit2expr(sat::literal l) { if (!m_var2expr.get(l.var())) { app* aux = m.mk_fresh_const(0, m.mk_bool_sort()); - // if (aux->get_decl()->get_name() == "k!81740") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(aux, m) << ": " << "v" << l.var() << "\n";); m_var2expr.set(l.var(), aux); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); + m_gmc->hide(aux->get_decl()); } VERIFY(m_var2expr.get(l.var())); expr_ref result(m_var2expr.get(l.var()), m); @@ -1094,9 +1094,9 @@ struct sat2goal::imp { app* aux = mc ? mc->var2expr(l.var()) : nullptr; if (!aux) { aux = m.mk_fresh_const(0, m.mk_bool_sort()); - // if (aux->get_decl()->get_name() == "k!81740") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(aux, m) << ": " << "v" << l.var() << "\n";); - if (mc) + if (mc) { mc->insert(l.var(), aux, true); + } } sat::literal lit(l.var(), false); m_lit2expr.set(lit.index(), aux); diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index c51adf8da..ddc396597 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -28,9 +28,12 @@ Notes: #include "model/model_evaluator.h" +generic_model_converter::~generic_model_converter() { +} + void generic_model_converter::add(func_decl * d, expr* e) { VERIFY(e); - struct entry et(d, e, m, ADD); + 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()); m_entries.push_back(et); @@ -169,7 +172,7 @@ void generic_model_converter::operator()(expr_ref& fml) { } unsigned j = min_idx; for (unsigned i = min_idx; i < m_entries.size(); ++i) { - entry const& e = m_entries[i]; + entry& e = m_entries[i]; if (e.m_instruction == instruction::HIDE) { if (i != j) { m_entries[j] = e; diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index ebac1f6d9..d303fb2e3 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -48,7 +48,7 @@ class generic_model_converter : public model_converter { public: generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {} - virtual ~generic_model_converter() { } + virtual ~generic_model_converter(); void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 296c2007b..127b6f5a0 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -24,7 +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); + 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));