From 155b746e0332f3e9d8b2e5e834c35aa731a33920 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 7 Oct 2022 10:18:29 +0200
Subject: [PATCH] side lemmas

---
 src/math/polysat/conflict.cpp | 33 ++++++++++++++++++++++++++++++++-
 src/math/polysat/conflict.h   | 10 ++++++++--
 2 files changed, 40 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 242996459..adcc870a4 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -337,6 +337,12 @@ namespace polysat {
         return m_lemmas.get(idx, {}).get();
     }
 
+    void conflict::set_side_lemma(sat::literal lit, clause_ref lemma) {
+        SASSERT_EQ(side_lemma(lit), nullptr);
+        unsigned const idx = lit.to_uint();
+        m_lemmas.insert(idx, std::move(lemma));
+    }
+
     void conflict::resolve_bool(sat::literal lit, clause const& cl) {
         // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
         //       clause: x \/ u \/ v
@@ -456,11 +462,36 @@ namespace polysat {
         logger().log_lemma(lemma);
         logger().end_conflict();
 
-        // TODO: additional lemmas
+        learn_side_lemmas();
 
         return lemma.build();
     }
 
+    void conflict::learn_side_lemmas() {
+        auto needs_side_lemma = [this](sat::literal lit) -> bool {
+            return s.m_bvars.value(lit) == l_undef && side_lemma(lit);
+        };
+        sat::literal_vector todo;
+        for (auto c : *this)
+            if (needs_side_lemma(c.blit()))
+                todo.push_back(c.blit());
+        while (!todo.empty()) {
+            sat::literal lit = todo.back();
+            todo.pop_back();
+            if (s.m_bvars.value(lit) != l_undef)
+                continue;
+            clause* lemma = side_lemma(lit);
+            SASSERT(lemma);
+            // Need to add the full derivation tree
+            for (auto lit2 : *lemma)
+                if (needs_side_lemma(lit2))
+                    todo.push_back(lit2);
+            // Store and bool-propagate the lemma
+            s.m_constraints.store(lemma, s, false);
+        }
+        m_lemmas.reset();
+    }
+
     bool conflict::minimize_vars(signed_constraint c) {
         if (m_vars.empty())
             return false;
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index ea49ecd39..ceacfd78d 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -71,7 +71,7 @@ Lemma:       y < z or xz <= xy or O(x,y)
 #include "math/polysat/types.h"
 #include "math/polysat/constraint.h"
 #include "math/polysat/inference_logger.h"
-#include <optional>
+#include <initializer_list>
 
 namespace polysat {
 
@@ -119,6 +119,12 @@ namespace polysat {
         void set_impl(signed_constraint c);
         bool minimize_vars(signed_constraint c);
 
+        void set_side_lemma(signed_constraint c, clause_ref lemma) { SASSERT(c); set_side_lemma(c.blit(), std::move(lemma)); }
+        void set_side_lemma(sat::literal lit, clause_ref lemma);
+
+        /** Store relevant side lemmas */
+        void learn_side_lemmas();
+
     public:
         conflict(solver& s);
         ~conflict();
@@ -228,7 +234,7 @@ namespace polysat {
 
     public:
         using value_type = signed_constraint;
-        using difference_type = unsigned;
+        using difference_type = std::ptrdiff_t;
         using pointer = signed_constraint const*;
         using reference = signed_constraint const&;
         using iterator_category = std::input_iterator_tag;