add option to bypass model converter during constraint addition. Simplify model definitions that come from blocked clauses

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

src/sat/sat_solver/inc_sat_solver.cpp

@@ -266,6 +266,7 @@ public:
     }
     virtual void set_produce_models(bool f) {}
     virtual void collect_param_descrs(param_descrs & r) {
+        solver::collect_param_descrs(r);
         goal2sat::collect_param_descrs(r);
         sat::solver::collect_param_descrs(r);
     }

src/solver/solver.cpp

@@ -178,24 +178,37 @@ bool solver::is_literal(ast_manager& m, expr* e) {
 
 void solver::assert_expr(expr* f) {
     expr_ref fml(f, get_manager());
-    model_converter_ref mc = get_model_converter();
-    mc = concat(mc0(), mc.get());
-    if (mc) {
-        (*mc)(fml);        
+    if (m_enforce_model_conversion) {
+        model_converter_ref mc = get_model_converter();
+        mc = concat(mc0(), mc.get());
+        if (mc) {
+            (*mc)(fml);        
+        }
     }
     assert_expr_core(fml);    
 }
 
 void solver::assert_expr(expr* f, expr* t) {
     ast_manager& m = get_manager();
-    expr_ref fml(f, m);
+    expr_ref fml(f, m);    
     expr_ref a(t, m);
-    model_converter_ref mc = get_model_converter();
-    mc = concat(mc0(), mc.get());
-    if (mc) {
-        (*mc)(fml);        
-        // (*mc)(a);        
+    if (m_enforce_model_conversion) {
+        model_converter_ref mc = get_model_converter();
+        mc = concat(mc0(), mc.get());
+        if (mc) {
+            (*mc)(fml);        
+            // (*mc)(a);        
+        }
     }
     assert_expr_core(fml, a);    
 }
 
+void solver::collect_param_descrs(param_descrs & r) {
+    r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: true) enforce model conversion when asserting formulas");
+}
+
+void solver::updt_params(params_ref const & p) { 
+    m_params.copy(p); 
+    m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", true);
+}
+

src/solver/solver.h

@@ -45,7 +45,9 @@ public:
 */
 class solver : public check_sat_result {
     params_ref m_params;
+    bool       m_enforce_model_conversion;
 public:
+    solver(): m_enforce_model_conversion(true) {}
     virtual ~solver() {}
 
     /**
@@ -56,7 +58,7 @@ public:
     /**
        \brief Update the solver internal settings. 
     */
-    virtual void updt_params(params_ref const & p) { m_params.copy(p); }
+    virtual void updt_params(params_ref const & p);
 
     /**
        \brief Retrieve set of parameters set on solver.
@@ -67,7 +69,7 @@ public:
        \brief Store in \c r a description of the configuration
        parameters available in this solver.
     */
-    virtual void collect_param_descrs(param_descrs & r) {}
+    virtual void collect_param_descrs(param_descrs & r);
     
     /**
        \brief Enable/Disable model generation for this solver object.

src/tactic/generic_model_converter.cpp

@@ -20,6 +20,8 @@ Notes:
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_util.h"
+#include "ast/occurs.h"
+#include "ast/rewriter/expr_safe_replace.h"
 #include "tactic/generic_model_converter.h"
 #include "model/model_v2_pp.h"
 #include "model/model_evaluator.h"
@@ -110,7 +112,7 @@ void generic_model_converter::operator()(expr_ref& fml) {
         entry const& e = m_add_entries[i];
         unsigned arity = e.m_f->get_arity();
         if (arity == 0) {
-            fmls.push_back(m.mk_eq(m.mk_const(e.m_f), e.m_def));
+            fmls.push_back(simplify_def(e));
         }
         else {
             expr_ref_vector args(m);
@@ -133,3 +135,34 @@ void generic_model_converter::operator()(expr_ref& fml) {
     }
     fml = mk_and(fmls);
 }
+
+/*
+ \brief simplify definition expansion from model converter in the case they come from blocked clauses.
+ In this case the definitions are of the form:
+ 
+    x <=> x or not (C)
+
+  or dually,
+
+    x <=> not (not x or not C)
+
+  in either case the definitions simplify to
+
+    x or C
+
+ */
+expr_ref generic_model_converter::simplify_def(entry const& e) {
+    expr_ref result(m);
+    expr_ref c(m.mk_const(e.m_f), m);
+    if (m.is_bool(c) && occurs(c, e.m_def)) {
+        expr_safe_replace rep(m);
+        expr_ref result1 = e.m_def;
+        expr_ref result2 = e.m_def;
+        rep.apply_substitution(c, m.mk_true(),  result1);
+        rep.apply_substitution(c, m.mk_false(), result2);
+        return expr_ref(m.mk_and(m.mk_or(c, result2), m.mk_or(m.mk_not(c), result1)), m);
+    }
+    else {
+        return expr_ref(m.mk_eq(c, e.m_def), m);
+    }
+}

src/tactic/generic_model_converter.h

@@ -35,6 +35,9 @@ class generic_model_converter : public model_converter {
     vector<entry> m_add_entries;
     vector<entry> m_hide_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) {}