From 1bb68a4fc126528017c8e296292e834d59087455 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 1 Feb 2023 10:47:26 +0100
Subject: [PATCH] track dependency of base-level conflict

---
 src/math/polysat/conflict.cpp | 7 +++++--
 src/math/polysat/conflict.h   | 3 ++-
 src/math/polysat/solver.cpp   | 6 ++----
 src/math/polysat/solver.h     | 2 +-
 4 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 1c0b7ed45..d9ebe3ebf 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -158,6 +158,7 @@ namespace polysat {
             SASSERT(m_vars_occurring.empty());
             SASSERT(m_lemmas.empty());
             SASSERT(m_narrow_queue.empty());
+            SASSERT(m_dep.is_null());
         }
         return is_empty;
     }
@@ -170,6 +171,7 @@ namespace polysat {
         m_lemmas.reset();
         m_narrow_queue.reset();
         m_level = UINT_MAX;
+        m_dep = null_dependency;
         SASSERT(empty());
     }
 
@@ -181,10 +183,11 @@ namespace polysat {
         return contains(lit) || contains(~lit);
     }
 
-    void conflict::init_at_base_level() {
+    void conflict::init_at_base_level(dependency dep) {
         SASSERT(empty());
         SASSERT(s.at_base_level());
         m_level = s.m_level;
+        m_dep = dep;
         SASSERT(!empty());
         // TODO: logger().begin_conflict???
         // TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
@@ -434,7 +437,7 @@ namespace polysat {
 
         clause_builder lemma(s);
 
-        for (auto c : *this)
+        for (signed_constraint c : *this)
             lemma.insert(~c);
 
         for (unsigned v : m_vars) {
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index affdb4ba7..ccb1ee448 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -101,6 +101,7 @@ namespace polysat {
 
         // Level at which the conflict was discovered
         unsigned m_level = UINT_MAX;
+        dependency m_dep = null_dependency;
 
     public:
         conflict(solver& s);
@@ -126,7 +127,7 @@ namespace polysat {
         bool is_relevant(sat::literal lit) const;
 
         /** conflict due to obvious input inconsistency */
-        void init_at_base_level();
+        void init_at_base_level(dependency dep);
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** boolean conflict with the given clause */
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 43707e395..042cb390e 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -158,8 +158,7 @@ namespace polysat {
         case l_false:
             // Input literal contradicts current boolean state (e.g., opposite literals in the input)
             // => conflict only flags the inconsistency
-            set_conflict_at_base_level();
-            SASSERT(dep == null_dependency && "track dependencies is TODO");
+            set_conflict_at_base_level(dep);
             return;
         case l_true:
             // constraint c is already asserted => ignore
@@ -174,8 +173,7 @@ namespace polysat {
         case l_false:
             // asserted an always-false constraint => conflict at base level
             LOG("Always false: " << c);
-            set_conflict_at_base_level();
-            SASSERT(dep == null_dependency && "track dependencies is TODO");
+            set_conflict_at_base_level(dep);
             return;
         case l_true:
             // asserted an always-true constraint => ignore
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index cf31c2c6e..d6931e665 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -253,7 +253,7 @@ namespace polysat {
         void erase_pwatch(pvar v, constraint* c);
         void erase_pwatch(constraint* c);
 
-        void set_conflict_at_base_level() { m_conflict.init_at_base_level(); }
+        void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }
         void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }