From f3328c743e0db90d2f84067393310aa3dd858479 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Sep 2021 16:43:55 -0700
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/conflict.cpp |  9 +++++++--
 src/math/polysat/solver.cpp   | 21 ++-------------------
 src/test/polysat.cpp          | 16 +++++++++-------
 3 files changed, 18 insertions(+), 28 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 440be370c..56bc7dfb9 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -230,6 +230,8 @@ namespace polysat {
                 continue;
             auto diseq = ~s.eq(s.var(v), s.get_value(v));
             cm().ensure_bvar(diseq.get());
+            //if (diseq.bvalue(s) == l_undef) 
+            //    s.assign_bool(s.get_level(v), ~diseq.blit(), nullptr, nullptr);            
             lemma.push(diseq);
         }        
 
@@ -271,8 +273,11 @@ namespace polysat {
         //      - cjust_v contains true constraints
         //      - core contains both false and true constraints (originally only false ones, but additional true ones may come from saturation)
 
-        if (is_bailout())
+        if (is_bailout()) {
+            if (!s.m_justification[v].is_decision())
+                m_vars.remove(v);
             return false;
+        }
 
         if (conflict_var() == v) {
             forbidden_intervals fi;
@@ -359,7 +364,7 @@ namespace polysat {
 
     void conflict::inc_pref(pvar v) {
         if (v >= m_pvar2count.size())
-            m_pvar2count.resize(v + 1);
+            m_pvar2count.resize(v + 1);        
         m_pvar2count[v]++;
     }
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 8a1ef2729..af62d2d67 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -621,24 +621,9 @@ namespace polysat {
         //      (L')^{L' \/ ¬L \/ ...}
         //      again L is in core, unless we core-reduced it away
 
-        clause_builder reason_builder = m_conflict.build_lemma();
-        
+        clause_builder reason_builder = m_conflict.build_lemma();        
+        SASSERT(std::find(reason_builder.begin(), reason_builder.end(), ~lit));
 
-        bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit);
-        if (!contains_lit) {
-            // At this point, we do not have ~lit in the reason.
-            // For now, we simply add it (thus weakening the reason)
-            //
-            // Alternative (to be considered later):
-            // - 'reason' itself (without ~L) would already be an explanation for ~L
-            // - however if it doesn't contain ~L, it breaks the boolean resolution invariant
-            // - would need to check what we can gain by relaxing that invariant
-            // - drawback: might have to bail out at boolean resolution
-            // Also: maybe we can skip ~L in some cases? but in that case it shouldn't be marked.
-            //
-            std::cout << "ADD extra " << ~lit << "\n";
-            reason_builder.push(~lit);
-        }
         clause_ref reason = reason_builder.build();
 
         if (reason->empty()) {
@@ -868,8 +853,6 @@ namespace polysat {
             signed_constraint sc(c, is_positive);
             for (auto const& wlist : m_pwatch) {
                 auto n = std::count(wlist.begin(), wlist.end(), sc);
-                if (n > 1)
-                    std::cout << sc << "\n" << * this << "\n";
                 VERIFY(n <= 1);  // no duplicates in the watchlist
                 num_watches += n;
             }
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index daf4ea24b..ffbe3060a 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1047,15 +1047,13 @@ namespace polysat {
 
 void tst_polysat() {
 
-    polysat::test_ineq_basic4();
-    return;
+    polysat::test_cjust();
 
-    polysat::test_p3();
+    
 
-    polysat::test_var_minimize();
-    //return;
 
-    polysat::test_subst();
+
+    
 
 
 
@@ -1086,8 +1084,12 @@ void tst_polysat() {
     polysat::test_ineq_basic4();
     polysat::test_ineq_basic5();
     polysat::test_ineq_basic6();
-    polysat::test_monot_bounds(2);
+
     polysat::test_cjust();
+    polysat::test_subst();
+    polysat::test_monot_bounds(2);
+
+    polysat::test_var_minimize();
 
     return;