From 4cdd3bf77dd5787684fd0b69bccf4633013b9567 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 31 Oct 2022 15:19:36 +0100
Subject: [PATCH] Add overload for conflict::add_lemma

---
 src/math/polysat/conflict.cpp | 16 +++++++++++-----
 src/math/polysat/conflict.h   |  1 +
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index cb431fe94..f8e47289e 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -329,14 +329,24 @@ namespace polysat {
                 m_vars.insert(v);
     }
 
+    void conflict::add_lemma(std::initializer_list<signed_constraint> cs) {
+        add_lemma(std::data(cs), cs.size());
+    }
+
     void conflict::add_lemma(signed_constraint const* cs, size_t cs_len) {
         clause_builder cb(s);
         for (size_t i = 0; i < cs_len; ++i)
             cb.push(cs[i]);
-        clause_ref lemma = cb.build();
+        add_lemma(cb.build());
+    }
+
+    void conflict::add_lemma(clause_ref lemma) {
         SASSERT(lemma);
         lemma->set_redundant(true);
         LOG("Side lemma: " << *lemma);
+        for (sat::literal lit : *lemma) {
+            LOG("   " << lit_pp(s, lit));
+        }
         m_lemmas.push_back(std::move(lemma));
         // If possible, we should set the new constraint to l_true;
         // and re-enable the assertions marked with "tag:true_by_side_lemma".
@@ -348,10 +358,6 @@ namespace polysat {
         // - l_false constraints are disallowed in the conflict (as before).
     }
 
-    void conflict::add_lemma(std::initializer_list<signed_constraint> cs) {
-        add_lemma(std::data(cs), cs.size());
-    }
-
 #if 0
     void conflict::bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len) {
         if (c.is_always_false()) {
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 344796184..d6a8df195 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -202,6 +202,7 @@ namespace polysat {
         /** Add a side lemma to the conflict; to be learned in addition to the main lemma after conflict resolution finishes. */
         void add_lemma(std::initializer_list<signed_constraint> cs);
         void add_lemma(signed_constraint const* cs, size_t cs_len);
+        void add_lemma(clause_ref lemma);
 
 #if 0
         /**