From fa036ae486de82be9410d88c56ba9f49f2541dbd Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 11 Jan 2023 10:29:20 +0100
Subject: [PATCH] track clause name for debugging

---
 src/math/polysat/clause.cpp   |  1 +
 src/math/polysat/clause.h     |  7 +++++++
 src/math/polysat/conflict.cpp | 11 +++++++----
 3 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/math/polysat/clause.cpp b/src/math/polysat/clause.cpp
index 0c3df0704..286d5821a 100644
--- a/src/math/polysat/clause.cpp
+++ b/src/math/polysat/clause.cpp
@@ -37,6 +37,7 @@ namespace polysat {
                 out << " \\/ ";
             out << lit;
         }
+        out << " (" << (name() ? name() : "<null>") << ")";
         return out;
     }
 
diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h
index 6103ef7d6..7b0783715 100644
--- a/src/math/polysat/clause.h
+++ b/src/math/polysat/clause.h
@@ -36,6 +36,7 @@ namespace polysat {
         unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
         bool m_redundant = redundant_default;
         sat::literal_vector m_literals;
+        char const* m_name = "";
 
 
         /* TODO: embed literals to save an indirection?
@@ -64,6 +65,9 @@ namespace polysat {
         sat::literal operator[](unsigned idx) const { return m_literals[idx]; }
         sat::literal& operator[](unsigned idx) { return m_literals[idx]; }
 
+        sat::literal_vector& literals() { return m_literals; }
+        sat::literal_vector const& literals() const { return m_literals; }
+
         using const_iterator = typename sat::literal_vector::const_iterator;
         const_iterator begin() const { return m_literals.begin(); }
         const_iterator end() const { return m_literals.end(); }
@@ -72,6 +76,9 @@ namespace polysat {
 
         void set_redundant(bool r) { m_redundant = r; }
         bool is_redundant() const { return m_redundant; }
+
+        void set_name(char const* name) { m_name = name; }
+        char const* name() const { return m_name; }
     };
 
     inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }
diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index dc2c548d0..85084acf8 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -287,7 +287,7 @@ namespace polysat {
 
     void conflict::insert_vars(signed_constraint c) {
         for (pvar v : c->vars())
-            if (s.is_assigned(v)) 
+            if (s.is_assigned(v))
                 m_vars.insert(v);
     }
 
@@ -308,10 +308,13 @@ namespace polysat {
             if (s.m_bvars.is_true(lit))
                 verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
 
-        LOG_H3("Lemma " << (name ? name : "<unknown>") << ": " << show_deref(lemma));
+        if (!name)
+            name = "<unknown>";
+        LOG_H3("Lemma " << name << ": " << show_deref(lemma));
         SASSERT(lemma);
         s.m_simplify_clause.apply(*lemma);
         lemma->set_redundant(true);
+        lemma->set_name(name);
         for (sat::literal lit : *lemma) {
             LOG(lit_pp(s, lit));
             // NOTE: it can happen that the literal's bvalue is l_true at this point.
@@ -385,7 +388,7 @@ namespace polysat {
         if (!has_decision) {
             for (pvar v : c->vars()) {
                 if (s.is_assigned(v) && s.get_level(v) <= lvl) {
-                    m_vars.insert(v);                   
+                    m_vars.insert(v);
 // TODO - figure out what to do with constraints from conflict lemma that disappear here.
 //                    if (s.m_bvars.is_false(lit))
 //                        m_resolver->infer_lemmas_for_value(v, ~c, *this);
@@ -418,7 +421,7 @@ namespace polysat {
             insert(s.eq(i.hi(), i.hi_val()));
         }
         logger().log(inf_resolve_value(s, v));
-        
+
         revert_pvar(v);
     }