From e1edadabec801c0a2059fecc8204de2dc73cd7ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Sep 2021 17:06:59 -0700
Subject: [PATCH] na

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

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 440be370c..5eb50ef8c 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -279,22 +279,16 @@ namespace polysat {
             if (fi.perform(s, v, cjust_v, *this))
                 return true;
         }
-
-        std::cout << "vars " << m_vars << " contains: " << m_vars.contains(v) << "\n";
         
         m_vars.remove(v);
 
         for (auto c : cjust_v)
             insert(c);
 
-        std::cout << "try explain v" << v << "\n";
-
         for (auto* engine : ex_engines)
             if (engine->try_explain(v, *this))
                 return true;
 
-        std::cout << "try elim v" << v << "\n";
-
         // No value resolution method was successful => fall back to saturation and variable elimination
         while (s.inc()) {
             // TODO: as a last resort, substitute v by m_value[v]?
@@ -306,7 +300,6 @@ namespace polysat {
         set_bailout();
         if (s.is_assigned(v))
             m_vars.insert(v);
-        std::cout << "vars " << m_vars << "\n";
         return false;
     }
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 8a1ef2729..e0ff8c31e 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -192,7 +192,6 @@ namespace polysat {
 
     bool solver::propagate(sat::literal lit, clause& cl) {
         SASSERT(cl.size() >= 2);
-        std::cout << lit << ": " << cl << "\n";
         unsigned idx = cl[0] == ~lit ? 1 : 0;
         SASSERT(cl[1 - idx] == ~lit);
         if (m_bvars.is_true(cl[idx]))
@@ -636,7 +635,6 @@ namespace polysat {
             // - 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();
@@ -869,7 +867,7 @@ namespace polysat {
             for (auto const& wlist : m_pwatch) {
                 auto n = std::count(wlist.begin(), wlist.end(), sc);
                 if (n > 1)
-                    std::cout << sc << "\n" << * this << "\n";
+                    LOG("violated watch constraint " << sc << "\n" << *this);
                 VERIFY(n <= 1);  // no duplicates in the watchlist
                 num_watches += n;
             }