remove incorrect and inefficient default model conversion

src/solver/solver.cpp

@@ -202,12 +202,6 @@ bool solver::is_literal(ast_manager& m, expr* e) {
 
 void solver::assert_expr(expr* f) {
     expr_ref fml(f, get_manager());
-    if (m_enforce_model_conversion) {
-        model_converter_ref mc = get_model_converter();
-        if (mc) {
-            (*mc)(fml);        
-        }
-    }
     assert_expr_core(fml);    
 }
 
@@ -215,13 +209,6 @@ void solver::assert_expr(expr* f, expr* t) {
     ast_manager& m = get_manager();
     expr_ref fml(f, m);    
     expr_ref a(t, m);
-    if (m_enforce_model_conversion) {
-        model_converter_ref mc = get_model_converter();
-        if (mc) {
-            (*mc)(fml);        
-            // (*mc)(a);        
-        }
-    }
     assert_expr_core2(fml, a);    
 }
 
@@ -241,14 +228,12 @@ void solver::collect_param_descrs(param_descrs & r) {
 void solver::reset_params(params_ref const & p) {
     m_params = p;
     solver_params sp(m_params);
-    m_enforce_model_conversion = sp.enforce_model_conversion();
     m_cancel_backup_file = sp.cancel_backup_file();
 }
 
 void solver::updt_params(params_ref const & p) {
     m_params.copy(p);
     solver_params sp(m_params);
-    m_enforce_model_conversion = sp.enforce_model_conversion();
     m_cancel_backup_file = sp.cancel_backup_file();
 }
 

src/solver/solver.h

@@ -49,10 +49,9 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p);
 */
 class solver : public check_sat_result {
     params_ref  m_params;
-    bool        m_enforce_model_conversion;
     symbol      m_cancel_backup_file;
 public:
-    solver(): m_enforce_model_conversion(false) {}
+     solver() {}
     ~solver() override {}
 
     /**

src/solver/solver_params.pyg

@@ -2,8 +2,7 @@
 def_module_params('solver', 
                   description='solver parameters',
                   export=True,
-                  params=(('enforce_model_conversion', BOOL, False, "apply model transformation on new assertions"),
-                          ('smtlib2_log', SYMBOL, '', "file to save solver interaction"),
+                  params=(('smtlib2_log', SYMBOL, '', "file to save solver interaction"),
                           ('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"),
                           ('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"),
                           ))

src/tactic/generic_model_converter.cpp

@@ -139,68 +139,6 @@ void generic_model_converter::set_env(ast_pp_util* visitor) {
     }
 }
 
-struct min_app_idx_proc {
-    unsigned m_min;
-    obj_map<func_decl, unsigned>& m_idxs;
-    min_app_idx_proc(obj_map<func_decl, unsigned>& idxs) : m_min(UINT_MAX), m_idxs(idxs) {}
-    void operator()(app * n) {
-        unsigned idx;
-        if (m_idxs.find(n->get_decl(), idx)) {
-            m_min = std::min(m_min, idx);
-        }
-    }
-    void operator()(var * n) {}
-    void operator()(quantifier * n) {}
-};
-
-void generic_model_converter::operator()(expr_ref& fml) {
-    min_app_idx_proc min_proc(m_first_idx);
-    for_each_expr(min_proc, fml);
-    unsigned min_idx = min_proc.m_min;
-    if (min_idx == UINT_MAX) return;
-    expr_ref_vector fmls(m);
-    fmls.push_back(fml);
-    for (unsigned i = m_entries.size(); i-- > min_idx;) {
-        entry const& e = m_entries[i];
-        if (e.m_instruction != instruction::ADD) {
-            continue;
-        }
-        unsigned arity = e.m_f->get_arity();
-        if (arity == 0) {
-            fmls.push_back(simplify_def(e));
-        }
-        else {
-            expr_ref_vector args(m);
-            sort_ref_vector sorts(m);
-            svector<symbol> names;
-            for (unsigned i = 0; i < arity; ++i) {
-                sorts.push_back(e.m_f->get_domain(i));
-                names.push_back(symbol(i));
-                args.push_back(m.mk_var(i, sorts.back()));
-            }
-            // TBD: check if order is correct with respect to quantifier binding ordering
-            expr_ref lhs(m.mk_app(e.m_f, arity, args.data()), m);
-            expr_ref body(m.mk_eq(lhs, e.m_def), m);
-            fmls.push_back(m.mk_forall(arity, sorts.data(), names.data(), body));
-        }
-        if (m_first_idx[e.m_f] == i) {
-            m_first_idx.remove(e.m_f);
-        }
-    }
-    unsigned j = min_idx;
-    for (unsigned i = min_idx; i < m_entries.size(); ++i) {
-        entry& e = m_entries[i];
-        if (e.m_instruction == instruction::HIDE) {
-            if (i != j) {
-                m_entries[j] = e;
-            }
-            ++j;
-        }
-    }
-    m_entries.shrink(j);
-    fml = mk_and(fmls);
-}
-
 void generic_model_converter::get_units(obj_map<expr, bool>& units) {
     th_rewriter rw(m);
     expr_safe_replace rep(m);

src/tactic/generic_model_converter.h

@@ -54,6 +54,8 @@ public:
     
     void operator()(model_ref & md) override;
 
+    void operator()(expr_ref& fml) override { UNREACHABLE(); }
+
     void cancel() override {}
 
     void display(std::ostream & out) override;
@@ -64,8 +66,6 @@ public:
 
     void set_env(ast_pp_util* visitor) override;
 
-    void operator()(expr_ref& fml) override; 
-
     void get_units(obj_map<expr, bool>& units) override;
 };
 

src/tactic/horn_subsume_model_converter.cpp

@@ -169,10 +169,6 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod
 }
 
 
-void horn_subsume_model_converter::operator()(expr_ref& fml) {
-    NOT_IMPLEMENTED_YET();
-}
-
 void horn_subsume_model_converter::operator()(model_ref& mr) {
 
     func_decl_ref pred(m);

src/tactic/horn_subsume_model_converter.h

@@ -72,8 +72,6 @@ public:
     
     void operator()(model_ref& _m) override;
 
-    void operator()(expr_ref& fml) override;
-
     model_converter * translate(ast_translation & translator) override;
 
     ast_manager& get_manager() { return m; }

src/tactic/model_converter.h

@@ -76,6 +76,8 @@ public:
     virtual void operator()(model_ref & m) = 0;
 
     virtual void operator()(labels_vec & r) {}
+
+    virtual void operator()(expr_ref& fml) { UNREACHABLE(); }
     
     virtual model_converter * translate(ast_translation & translator) = 0;
     
@@ -86,7 +88,6 @@ public:
        The operator has as side effect of adding definitions as assertions to the
        formula and removing these definitions from the model converter.
      */
-    virtual void operator()(expr_ref& formula) { UNREACHABLE(); }
 
     virtual void get_units(obj_map<expr, bool>& fmls) { UNREACHABLE(); }
 };