From 2e4b1fb5e00514d9346eaa3ce8400cce32a053e8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 31 Mar 2021 13:27:34 -0700
Subject: [PATCH] more stub

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/polysat.cpp | 29 ++++++++++++++++++-----------
 src/math/polysat/polysat.h   |  2 +-
 2 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp
index 71027551f..5dd7c9f38 100644
--- a/src/math/polysat/polysat.cpp
+++ b/src/math/polysat/polysat.cpp
@@ -102,10 +102,6 @@ namespace polysat {
     }
 
     void solver::add_eq(pdd const& p, unsigned dep) {
-        //
-        // TODO reduce p using assignment (at current level, 
-        // assuming constraint is removed also at current level).
-        // 
         constraint* c = constraint::eq(m_level, p, m_dep_manager.mk_leaf(dep));
         m_constraints.push_back(c);
         add_watch(*c);
@@ -370,8 +366,7 @@ namespace polysat {
             v = m_search[i];
             if (!is_marked(v))
                 continue;
-            pdd q = isolate(v);
-            pdd r = resolve(v, q, p);
+            pdd r = resolve(v, p);
             pdd rval = r.subst_val(sub);
             if (!rval.is_non_zero())
                 goto backtrack;
@@ -426,8 +421,9 @@ namespace polysat {
     pdd solver::isolate(unsigned v) {
         if (m_cjust[v].empty()) 
             return sz2pdd(m_size[v]).zero();
-        pdd p = m_cjust[v][0]->p();
-        for (unsigned i = m_cjust[v].size(); i-- > 1; ) {
+        auto const& cs = m_cjust[v];
+        pdd p = cs[0]->p();
+        for (unsigned i = cs.size(); i-- > 1; ) {
             // TBD reduce with respect to v
         }
         return p;
@@ -436,9 +432,20 @@ namespace polysat {
     /**
      * Return residue of superposing p and q with respect to v.
      */
-    pdd solver::resolve(unsigned v, pdd const& p, pdd const& q) {
-        // TBD remove as much trace of v as possible.
-        return p;
+    pdd solver::resolve(unsigned v, pdd const& p) {
+        auto degree = p.degree(v);
+        auto const& cs = m_cjust[v];
+        pdd r = p;
+        while (degree > 0) {
+            for (auto * c : cs) {
+                if (degree >= c->p().degree(v)) {
+                    // TODO binary resolve, update r using result
+                    // add parity condition to presere falsification
+                    degree = r.degree(v);
+                }
+            }
+        }
+        return r;
     }
     
     void solver::reset_marks() {
diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h
index 09844282f..8c04b31e3 100644
--- a/src/math/polysat/polysat.h
+++ b/src/math/polysat/polysat.h
@@ -167,7 +167,7 @@ namespace polysat {
         void set_mark(unsigned v) { m_marks[v] = m_clock; }
 
         pdd isolate(unsigned v);
-        pdd resolve(unsigned v, pdd const& p, pdd const& q);
+        pdd resolve(unsigned v, pdd const& p);
         void decide();
         void resolve_conflict_core();