From e1f71d4932846c0775e0931ae45aa37b09e1c16a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 18 Dec 2020 14:32:16 -0800 Subject: [PATCH] fix #4904 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 24 +++++++++++++++--------- src/cmd_context/cmd_context.h | 6 ++++-- src/tactic/generic_model_converter.cpp | 3 ++- src/tactic/generic_model_converter.h | 4 +++- 4 files changed, 24 insertions(+), 13 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 8bd4b616f..51738219f 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -311,6 +311,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma } void cmd_context::erase_macro(symbol const& s) { + std::cout << "erase " << s << "\n"; macro_decls decls; VERIFY(m_macros.find(s, decls)); decls.erase_last(m()); @@ -501,6 +502,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): install_basic_cmds(*this); install_ext_basic_cmds(*this); install_core_tactic_cmds(*this); + m_mcs.push_back(nullptr); SASSERT(m != 0 || !has_manager()); if (m_main_ctx) { set_verbose_stream(diagnostic_stream()); @@ -516,7 +518,7 @@ cmd_context::~cmd_context() { finalize_tactic_cmds(); finalize_probes(); reset(true); - m_mc0 = nullptr; + m_mcs.reset(); m_solver = nullptr; m_check_sat_result = nullptr; } @@ -889,21 +891,22 @@ 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(), "cmd_context"); - if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get()); + if (!mc0()) m_mcs.set(m_mcs.size()-1, alloc(generic_model_converter, m(), "cmd_context")); + if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(mc0()); func_decl_ref fn(m().mk_func_decl(s, arity, domain, m().get_sort(t)), m()); func_decls & fs = m_func_decls.insert_if_not_there(s, func_decls()); fs.insert(m(), fn); VERIFY(fn->get_range() == m().get_sort(t)); - m_mc0->add(fn, t); + mc0()->add(fn, t); if (!m_global_decls) m_func_decls_stack.push_back(sf_pair(s, fn)); } + void cmd_context::model_del(func_decl* f) { - 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); + if (!mc0()) m_mcs.set(m_mcs.size() - 1, alloc(generic_model_converter, m(), "cmd_context")); + if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(mc0()); + mc0()->hide(f); } @@ -1295,7 +1298,7 @@ void cmd_context::reset(bool finalize) { reset_func_decls(); restore_assertions(0); m_solver = nullptr; - m_mc0 = nullptr; + m_mcs.reset(); m_scopes.reset(); m_opt = nullptr; m_pp_env = nullptr; @@ -1369,6 +1372,8 @@ void cmd_context::push() { s.m_assertions_lim = m_assertions.size(); if (!m_global_decls) pm().push(); + ast_translation tr(m(), m()); + m_mcs.push_back(m_mcs.back() ? m_mcs.back()->copy(tr) : nullptr); unsigned timeout = m_params.m_timeout; m().limit().push(m_params.rlimit()); cancel_eh eh(m().limit()); @@ -1494,6 +1499,7 @@ void cmd_context::pop(unsigned n) { restore_aux_pdecls(s.m_aux_pdecls_lim); restore_assertions(s.m_assertions_lim); restore_psort_inst(s.m_psort_inst_stack_lim); + m_mcs.shrink(m_mcs.size() - n); m_scopes.shrink(new_lvl); if (!m_global_decls) pm().pop(n); @@ -1655,7 +1661,7 @@ void cmd_context::display_dimacs() { void cmd_context::display_model(model_ref& mdl) { if (mdl) { - if (m_mc0) (*m_mc0)(mdl); + if (mc0()) (*mc0())(mdl); model_params p; if (p.compact()) mdl->compress(); add_declared_functions(*mdl); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 3260f16d5..1b074792e 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -84,6 +84,7 @@ public: bool empty() const { return !m_decls || m_decls->empty(); } expr* find(unsigned arity, sort *const* domain) const; void erase_last(ast_manager& m); + macro_decl const& last() const { return m_decls->back(); } vector::iterator begin() const { return m_decls->begin(); } vector::iterator end() const { return m_decls->end(); } }; @@ -197,7 +198,8 @@ protected: static std::ostringstream g_error_stream; - generic_model_converter_ref m_mc0; + generic_model_converter* mc0() { return m_mcs.back(); } + sref_vector m_mcs; ast_manager * m_manager; bool m_own_manager; bool m_manager_initialized; @@ -449,7 +451,7 @@ public: dictionary const & get_macros() const { return m_macros; } - model_converter* get_model_converter() { return m_mc0.get(); } + model_converter* get_model_converter() { return mc0(); } bool is_model_available(model_ref& md) const; diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index bf04a3ee2..886b2d040 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -104,7 +104,7 @@ void generic_model_converter::display(std::ostream & out) { } } -model_converter * generic_model_converter::translate(ast_translation & translator) { +generic_model_converter * generic_model_converter::copy(ast_translation & translator) { ast_manager& to = translator.to(); generic_model_converter * res = alloc(generic_model_converter, to, m_orig.c_str()); for (entry const& e : m_entries) { @@ -123,6 +123,7 @@ model_converter * generic_model_converter::translate(ast_translation & translato return res; } + void generic_model_converter::set_env(ast_pp_util* visitor) { if (!visitor) { m_env = nullptr; diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index bd937870f..54268ac1b 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -58,7 +58,9 @@ public: void display(std::ostream & out) override; - model_converter * translate(ast_translation & translator) override; + model_converter * translate(ast_translation & translator) override { return copy(translator); } + + generic_model_converter* copy(ast_translation & translator); void set_env(ast_pp_util* visitor) override;