From a863a0e8536586265c1f664e3e3fdc9ebbcf2e97 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 1 Apr 2021 15:12:54 -0700
Subject: [PATCH] reorg resolution loop

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

diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp
index f3ebe09aa..827917105 100644
--- a/src/math/polysat/polysat.cpp
+++ b/src/math/polysat/polysat.cpp
@@ -373,16 +373,16 @@ namespace polysat {
             }
             pdd r = resolve(v, p);
             pdd rval = r.subst_val(sub);
-            if (!rval.is_non_zero()) {
-                backtrack(i);
-                return;
-            }
-            if (r.is_val()) {
+            if (r.is_val() && rval.is_non_zero()) {
                 report_unsat();
                 return;
             }
             if (j.is_decision()) {
-                revert_decision(i);
+                revert_decision(p, i);
+                return;
+            }
+            if (!rval.is_non_zero()) {
+                backtrack(i);
                 return;
             }
             SASSERT(j.is_propagation());
@@ -422,20 +422,40 @@ namespace polysat {
         // are in the unsat core that is produced as a side-effect        
     }
 
-   void solver::revert_decision(unsigned i) {
+    void solver::revert_decision(pdd const& p, unsigned i) {
+        auto v = m_search[i];
+        SASSERT(m_justification[v].is_decision());
+        // 
+        // TBD: compute level and dependencies for p
+        // Dependencies should be accumulated during resolve_conflict
+        // the level is computed from the free variables in p (except v)
+        // it should correspond to the implication level.
+        // 
+        unsigned level = 0;
+        u_dependency* deps = nullptr; 
+        constraint* c = constraint::eq(level, p, deps);
+        m_cjust[v].push_back(c);        
+        m_redundant.push_back(c);
+        add_watch(*c);
+        SASSERT(invariant(m_redundant)); // TBD enforce level invariant
+        //
+        // TBD: remove current value from viable
+        // m_values[v]
+        // 
+        // 1. undo levels until i
+        // 2. find a new decision if there is one, 
+        //    propagate if decision is singular,
+        //    otherwise if there are no viable decisions, learn_and_backjump
+        //    and set a new conflict.
+        // 
+    }
 
-   }
-
-    void solver::learn_and_backjump(pdd const& lemma, unsigned new_level) {
+    void solver::backjump(unsigned new_level) {
         unsigned num_levels = m_level - new_level;
         SASSERT(num_levels > 0);
         pop_levels(num_levels);
-        m_trail.pop_scope(num_levels);
-        
-        // TBD: add new constraints & lemmas.
+        m_trail.pop_scope(num_levels);        
     }
-
-
     
     /**
      * resolve polynomials associated with unit propagating on v
diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h
index ef919237f..b6f38ed44 100644
--- a/src/math/polysat/polysat.h
+++ b/src/math/polysat/polysat.h
@@ -179,8 +179,8 @@ namespace polysat {
         void resolve_conflict();            
         void backtrack(unsigned i);
         void report_unsat();
-        void revert_decision(unsigned i);
-        void learn_and_backjump(pdd const& lemma, unsigned new_level);
+        void revert_decision(pdd const& p, unsigned i);
+        void backjump(unsigned new_level);
 
         bool can_decide() const { return !m_free_vars.empty(); }
         void decide(rational & val, unsigned& var);
@@ -201,8 +201,7 @@ namespace polysat {
         ~solver();
 
         /**
-         * Self-contained satisfiability checker.
-         * Main mode is to have external solver drive state machine.
+         * End-game satisfiability checker.
          */
         lbool check_sat();
         
@@ -216,7 +215,6 @@ namespace polysat {
          */
         pdd var(unsigned v) { return m_vars[v]; }
 
-
         /**
          * Add polynomial constraints
          * Each constraint is tracked by a dependency.
@@ -237,6 +235,10 @@ namespace polysat {
         bool can_propagate();
         void propagate();
 
+        /**
+         * External context managment.
+         * Adds so-called user-scope.
+         */
         void push();
         void pop(unsigned num_scopes);