From fc6e127cca5766b291bf0eb00b2784bbc9d66eb3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Nov 2021 20:19:58 +0100
Subject: [PATCH] don't add viable premises on decisions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/conflict.cpp | 10 +++++++---
 src/math/polysat/solver.cpp   |  1 -
 src/math/polysat/viable.cpp   |  1 -
 src/test/polysat.cpp          | 11 ++++++-----
 4 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 465b5b077..b4208dc33 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -298,12 +298,16 @@ namespace polysat {
             return false;
         }
 
+        auto const& j = s.m_justification[v];
+
         s.inc_activity(v); 
         
         m_vars.remove(v);
 
-        for (auto const& c : s.m_viable.get_constraints(v))
-            insert(c);
+        if (!j.is_decision()) {
+            for (auto const& c : s.m_viable.get_constraints(v))
+                insert(c);
+        }
 
         for (auto* engine : ex_engines)
             if (engine->try_explain(v, *this))
@@ -318,7 +322,7 @@ namespace polysat {
                 break;
         }
         set_bailout();
-        if (s.is_assigned(v) && s.m_justification[v].is_decision())
+        if (s.is_assigned(v) && j.is_decision())
             m_vars.insert(v);
         return false;
     }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b31a9e76a..d01182b5f 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -50,7 +50,6 @@ namespace polysat {
         m_branch_bool = m_params.get_bool("branch_bool", false);
         m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
         m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
-        std::cout << m_max_conflicts << "\n";
     }
 
     bool solver::should_search() {
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 14c2cb6d6..9331f572d 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -278,7 +278,6 @@ namespace polysat {
     }
 
     bool viable::resolve(pvar v, conflict& core) {
-        std::cout << "resolve " << v << "\n";
         if (has_viable(v))
             return false;
         auto* e = m_viable[v];
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 02a29d46a..51e2567d3 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -18,8 +18,7 @@ namespace polysat {
 
     public:
         scoped_solver(std::string name): solver(lim), m_name(name) {
-            std::cout << "\n\n\n" << std::string(78, '#') << "\n";
-            std::cout << "\nSTART: " << m_name << "\n";
+            LOG("\n\n\n" << std::string(78, '#') << "\n\nSTART: " << m_name << "\n");
             params_ref p;
             p.set_uint("max_conflicts", 10);
             updt_params(p);
@@ -27,11 +26,10 @@ namespace polysat {
 
         void check() {
             m_last_result = check_sat();
-            std::cout << m_name << ": " << m_last_result << "\n";
+            LOG(m_name << ": " << m_last_result << "\n");
             statistics st;
             collect_statistics(st);
-            std::cout << st << "\n";
-            std::cout << *this << "\n";
+            LOG(st << "\n" << *this << "\n");
         }
 
         void expect_unsat() {
@@ -1068,6 +1066,9 @@ namespace polysat {
 void tst_polysat() {
 
 
+    polysat::test_l5();
+    return;
+
     polysat::test_ineq_basic6();
             
     // polysat::test_monot_bounds(8);