From 576e0b70b266fe8e21fd64d9104f6f5f20a194f0 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 1 Feb 2023 10:53:49 +0100
Subject: [PATCH] stub for conflict::find_deps

---
 src/math/polysat/conflict.cpp | 21 +++++++++++++++++++++
 src/math/polysat/conflict.h   |  2 ++
 src/math/polysat/solver.cpp   |  9 ++-------
 3 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index d9ebe3ebf..4ccab9f07 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -504,6 +504,27 @@ namespace polysat {
     }
 #endif
 
+    void conflict::find_deps(dependency_vector& out_deps) const {
+        sat::literal_vector todo;
+        sat::literal_set done;
+        indexed_uint_set deps;
+
+        LOG("conflict: " << *this);
+
+        // TODO: starting at literals/variables in the conflict, chase propagations backwards and accumulate dependencies.
+        verbose_stream() << "WARNING: unsat_core requested but dependency tracking in polysat is TODO\n";
+        for (signed_constraint c : *this) {
+            dependency d = s.m_bvars.dep(c.blit());
+            if (!d.is_null())
+                deps.insert(d.val());
+        }
+
+        for (unsigned d : deps)
+            out_deps.push_back(dependency(d));
+        if (!m_dep.is_null())
+            out_deps.push_back(m_dep);
+    }
+
     std::ostream& conflict::display(std::ostream& out) const {
         char const* sep = "";
         for (auto c : *this)
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index ccb1ee448..958b7993b 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -195,6 +195,8 @@ namespace polysat {
         /** Move the literals to be narrowed out of the conflict */
         sat::literal_vector take_narrow_queue();
 
+        void find_deps(dependency_vector& out_deps) const;
+
         std::ostream& display(std::ostream& out) const;
     };
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 042cb390e..774f15793 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1318,14 +1318,9 @@ namespace polysat {
     }
 
     void solver::unsat_core(dependency_vector& deps) {
-        verbose_stream() << "WARNING: unsat_core requested but dependency tracking in polysat is TODO\n";
+        VERIFY(is_conflict());
         deps.reset();
-        LOG("conflict" << m_conflict);
-        for (auto c : m_conflict) {
-            auto d = m_bvars.dep(c.blit());
-            if (d != null_dependency)
-                deps.push_back(d);
-        }
+        m_conflict.find_deps(deps);
     }
 
     std::ostream& solver::display(std::ostream& out) const {