fix #4904

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<reslimit> 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);

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<macro_decl>::iterator begin() const { return m_decls->begin(); }
     vector<macro_decl>::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<generic_model_converter> m_mcs;
     ast_manager *                m_manager;
     bool                         m_own_manager;
     bool                         m_manager_initialized;
@@ -449,7 +451,7 @@ public:
 
     dictionary<macro_decls> 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;
 

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;

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;