debugging mc

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

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<func_decls>::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);
 }

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

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

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

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

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;

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

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"))
     {
     }
 

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());
     }
 }

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

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());
                     }

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

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) {

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

src/tactic/arith/lia2pb_tactic.cpp

@@ -222,7 +222,7 @@ class lia2pb_tactic : public tactic {
             
             ref<generic_model_converter> gmc;
             if (m_produce_models) {
-                gmc = alloc(generic_model_converter, m);
+                gmc = alloc(generic_model_converter, m, "lia2pb");
             }
             
             expr_ref zero(m);

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)) {

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

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

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<app, expr*> & 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<app, std::pair<expr*,expr*> >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end();
             for (; it != end; ++it) {

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

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

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

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<generic_model_converter> filter = alloc(generic_model_converter, m);
+            ref<generic_model_converter> 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);

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());
                 }
             }

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

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

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;

src/tactic/core/reduce_args_tactic.cpp

@@ -393,7 +393,7 @@ struct reduce_args_tactic::imp {
         ptr_buffer<expr> new_args;
         var_ref_vector   new_vars(m_manager);
         ptr_buffer<expr> 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;

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;

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;
 

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<expr> 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));
     }

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<entry> m_entries;
     obj_map<func_decl, unsigned> 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() { }
     

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

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);
+            model_converter_ref mc = bounded_model_converter();
-            filter_model(mdl);
+            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]);

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);
+            model_converter_ref mc = enum_model_converter();
-            filter_model(mdl);            
+            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<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
-    virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
+    virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { 
-    virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { return m_solver->cube(vars, backtrack_level); }
+        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();

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 {

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

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