From 5b3f500900dd8bfc74130796a7b2254b319bf2a0 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 23 Mar 2023 07:18:36 +0100
Subject: [PATCH] Try to keep conflict alive for longer

---
 src/math/polysat/conflict.cpp | 18 +++++++++++++++++-
 src/math/polysat/conflict.h   |  1 +
 src/math/polysat/solver.cpp   | 25 +++++++++++++++++--------
 3 files changed, 35 insertions(+), 9 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index ec303127e..ed67f3077 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -171,6 +171,7 @@ namespace polysat {
     }
 
     void conflict::reset() {
+        LOG("Reset conflict");
         m_literals.reset();
         m_vars.reset();
         m_var_occurrences.reset();
@@ -190,6 +191,22 @@ namespace polysat {
         return contains(lit) || contains(~lit);
     }
 
+    unsigned conflict::effective_level() const {
+        // If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier.
+        if (m_dep != null_dependency)
+            return m_level;
+        // In other cases, m_level just tracks the level at which the conflict appeared.
+        // Find the minimal level at which the conflict is still valid.
+        unsigned lvl = 0;
+        for (unsigned lit_idx : m_literals) {
+            sat::literal const lit = sat::to_literal(lit_idx);
+            lvl = std::max(lvl, s.m_bvars.level(lit));
+        }
+        for (pvar v : m_vars)
+            lvl = std::max(lvl, s.get_level(v));
+        return lvl;
+    }
+
     void conflict::init_at_base_level(dependency dep) {
         SASSERT(empty());
         SASSERT(s.at_base_level());
@@ -396,7 +413,6 @@ namespace polysat {
         SASSERT(contains(lit));
         SASSERT(!contains(~lit));
 
-        unsigned const lvl = s.m_bvars.level(lit);
         signed_constraint c = s.lit2cnstr(lit);
 
         unsigned const eval_idx = s.m_search.get_bool_index(lit);
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index babe17c90..39bdb99b4 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -122,6 +122,7 @@ namespace polysat {
         uint_set const& vars() const { return m_vars; }
 
         unsigned level() const { return m_level; }
+        unsigned effective_level() const;
 
         bool is_relevant_pvar(pvar v) const;
         bool is_relevant(sat::literal lit) const;
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 3cc6830f3..9bcd75c26 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1434,17 +1434,26 @@ namespace polysat {
     void solver::pop(unsigned num_scopes) {
         VERIFY(m_base_levels.size() >= num_scopes);
         SASSERT_EQ(m_base_index.size(), m_base_levels.size());
-        unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes];
         LOG_H3("Pop " << num_scopes << " user scopes");
-        pop_levels(m_level - base_level + 1);
-        if (m_level < m_conflict.level()) {
-            clause_ref_vector lemmas = m_conflict.take_lemmas();
+
+        unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes];
+        unsigned const target_level = base_level - 1;
+
+        clause_ref_vector lemmas;
+        if (is_conflict() && target_level < m_conflict.effective_level()) {
+            lemmas = m_conflict.take_lemmas();
             m_conflict.reset();
-            // TODO: currently we forget all new lemmas at this point.
-            for (clause* lemma : lemmas)
-                if (lemma->is_active())
-                    propagate_clause(*lemma);
         }
+
+        pop_levels(m_level - base_level + 1);
+        SASSERT_EQ(m_level, target_level);
+
+        // TODO: currently we forget all new lemmas at this point.
+        //       (but anything that uses popped assumptions cannot be used anymore.)
+        for (clause* lemma : lemmas)
+            if (lemma->is_active())
+                propagate_clause(*lemma);
+
         m_base_levels.shrink(m_base_levels.size() - num_scopes);
         m_base_index.shrink(m_base_index.size() - num_scopes);
     }