From ae728374c84a6bf65f4849d3341ad83140105005 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 15 Jan 2018 17:20:19 -0800
Subject: [PATCH] disable buggy clausification in ba_solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp                 |  2 ++
 src/sat/sat_solver/inc_sat_solver.cpp | 26 +++++++++++++++++++++-----
 src/solver/solver.cpp                 |  2 ++
 3 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 7865f618e..4099693c5 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2649,6 +2649,7 @@ namespace sat {
     }
 
     bool ba_solver::clausify(literal lit, unsigned n, literal const* lits, unsigned k) {
+        return false;
         bool is_def = lit != null_literal;
         if ((!is_def || !s().was_eliminated(lit)) && 
             !std::any_of(lits, lits + n, [&](literal l) { return s().was_eliminated(l); })) {
@@ -2667,6 +2668,7 @@ namespace sat {
     }
 
     bool ba_solver::clausify(card& c) {
+        return false;
         if (get_config().m_card_solver)
             return false;
 
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 9f248c25f..ef85ad921 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -60,7 +60,8 @@ class inc_sat_solver : public solver {
     goal_ref_buffer     m_subgoals;
     proof_converter_ref m_pc;
     model_converter_ref m_mc;
-    model_converter_ref m_mc0;
+    mutable model_converter_ref m_mc0;
+    mutable obj_hashtable<func_decl>  m_inserted_const2bits;
     ref<sat2goal::mc>   m_sat_mc;
     mutable model_converter_ref m_cached_mc;
     svector<double>     m_weights;
@@ -227,6 +228,7 @@ public:
             n = m_num_scopes;     // take over for another solver.
         }
         if (m_bb_rewriter) m_bb_rewriter->pop(n);
+        m_inserted_const2bits.reset();
         m_map.pop(n);
         SASSERT(n <= m_num_scopes);
         m_solver.user_pop(n);
@@ -443,7 +445,8 @@ public:
         if (m_cached_mc)
             return m_cached_mc;
         if (is_internalized() && m_internalized_converted) {            
-            m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
+            insert_const2bits();
+            m_cached_mc = m_mc0.get();
             m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
             m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
             return m_cached_mc;
@@ -500,6 +503,21 @@ public:
 
 private:
 
+    void insert_const2bits() const {
+        if (!m_bb_rewriter) return;
+        obj_map<func_decl, expr*> to_insert;
+        obj_map<func_decl, expr*> const& const2bits = m_bb_rewriter->const2bits();
+        for (auto const& kv : const2bits) {
+            if (!m_inserted_const2bits.contains(kv.m_key)) {
+                m_inserted_const2bits.insert(kv.m_key);
+                to_insert.insert(kv.m_key, kv.m_value);
+            }
+        }
+        if (!to_insert.empty()) {
+            m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, to_insert));
+        }
+    }
+
 
     lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
         m_mc.reset();
@@ -790,9 +808,7 @@ private:
         if (m_sat_mc) {
             (*m_sat_mc)(m_model);
         }
-        if (m_bb_rewriter.get() && !m_bb_rewriter->const2bits().empty()) {
-            m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
-        }
+        insert_const2bits();
         if (m_mc0) {            
             (*m_mc0)(m_model);
         }
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 43ca9870a..9fbaa8032 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -193,6 +193,8 @@ void solver::assert_expr(expr* f, expr* t) {
     expr_ref fml(f, m);    
     expr_ref a(t, m);
     if (m_enforce_model_conversion) {
+        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) {