From 0a0953ae7806a712fe0c8285d61dd65afeb6363c Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 23 Sep 2022 16:04:51 +0200
Subject: [PATCH] Reduce log output

---
 src/math/polysat/boolean.cpp        |  2 +-
 src/math/polysat/boolean.h          |  2 +-
 src/math/polysat/solver.cpp         | 12 +++++++-----
 src/math/polysat/ule_constraint.cpp |  6 +++---
 4 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index c18f4a36e..fac2b1f4d 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -67,7 +67,7 @@ namespace polysat {
     }
 
     void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
-        LOG("Eval literal " << lit << " @ " << lvl);
+        LOG_V("Eval literal " << lit << " @ " << lvl);
         assign(kind_t::value_propagation, lit, lvl, nullptr);
         SASSERT(is_value_propagation(lit));
     }
diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index a3a83d349..d7a7b274a 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -83,7 +83,7 @@ namespace polysat {
             case kind_t::assumption: return out << "assumption";
             default: UNREACHABLE(); return out;
             }
-         }
+        }
     };
 
     struct bool_justification_pp {
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 5e82f50c0..f7566250d 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -394,7 +394,7 @@ namespace polysat {
 
     void solver::add_pwatch(constraint* c, pvar v) {
         SASSERT(m_locked_wlist != v);  // the propagate loop will not discover the new size
-        LOG("Watching v" << v << " in constraint " << show_deref(c));
+        LOG_V("Watching v" << v << " in constraint " << show_deref(c));
         m_pwatch[v].push_back(c);
     }
 
@@ -855,8 +855,10 @@ namespace polysat {
     }
 
     void solver::backjump(unsigned new_level) {
-        LOG_H3("Backjumping to level " << new_level << " from level " << m_level);
-        pop_levels(m_level - new_level);
+        if (m_level != new_level) {
+            LOG_H3("Backjumping to level " << new_level << " from level " << m_level);
+            pop_levels(m_level - new_level);
+        }
     }
 
     // Add lemma to storage
@@ -916,14 +918,14 @@ namespace polysat {
     }
 
     void solver::push() {
-        LOG("Push user scope");
+        LOG_H3("Push user scope");
         push_level();
         m_base_levels.push_back(m_level);
     }
 
     void solver::pop(unsigned num_scopes) {
         unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes];
-        LOG("Pop " << num_scopes << " user scopes");
+        LOG_H3("Pop " << num_scopes << " user scopes");
         pop_levels(m_level - base_level + 1);
         if (m_level < m_conflict.level())
             m_conflict.reset();
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index eb292ff06..2e9207bf9 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -128,9 +128,9 @@ namespace polysat {
         signed_constraint sc(this, is_positive);
 
         LOG_H3("Narrowing " << sc);
-        LOG("Assignment: " << assignments_pp(s));
-        LOG("Substituted LHS: " << lhs() << " := " << p);
-        LOG("Substituted RHS: " << rhs() << " := " << q);
+        LOG_V("Assignment: " << assignments_pp(s));
+        LOG_V("Substituted LHS: " << lhs() << " := " << p);
+        LOG_V("Substituted RHS: " << rhs() << " := " << q);
 
         if (is_always_false(is_positive, p, q)) {
             s.set_conflict(sc);