From f3ac879fa42704bddc5fdf8ac34c0221b2899506 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Dec 2021 08:25:52 -0800
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/forbidden_intervals.cpp |  4 ++--
 src/math/polysat/solver.cpp              | 27 +++---------------------
 src/math/polysat/solver.h                |  1 -
 src/math/polysat/viable.cpp              |  2 +-
 4 files changed, 6 insertions(+), 28 deletions(-)

diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index c98e7e404..12dcf9a43 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -73,9 +73,9 @@ namespace polysat {
         if (p.is_val())
             return;
         else if (is_zero)
-            side_cond.push_back(s.m_constraints.eq(p));
+            side_cond.push_back(s.eq(p));
         else
-            side_cond.push_back(~s.m_constraints.eq(p));
+            side_cond.push_back(~s.eq(p));
     }
 
     std::tuple<bool, rational, pdd, pdd> forbidden_intervals::linear_decompose(pvar v, pdd const& p, vector<signed_constraint>& out_side_cond) {
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 394f441a0..bd6ca895b 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -393,7 +393,7 @@ namespace polysat {
     void solver::decide() {
         LOG_H2("Decide");
         SASSERT(can_decide());
-        if (m_bvars.can_decide() && m_branch_bool)
+        if (m_branch_bool && m_bvars.can_decide())
             bdecide(m_bvars.next_var());
         else
             pdecide(m_free_pvars.next_var());
@@ -446,19 +446,6 @@ namespace polysat {
 
     /**
      * Conflict resolution.
-     * - m_conflict are constraints that are infeasible in the current assignment.
-     * 1. walk m_search from top down until last variable in m_conflict.
-     * 2. resolve constraints in m_cjust to isolate lowest degree polynomials
-     *    using variable.
-     *    Use Olm-Seidl division by powers of 2 to preserve invertibility.
-     * 3. resolve conflict with result of resolution.
-     * 4. If the resulting lemma is still infeasible continue, otherwise bail out
-     *    and undo the last assignment by accumulating conflict trail (but without resolution).
-     * 5. When hitting the last decision, determine whether conflict polynomial is asserting,
-     *    If so, apply propagation.
-     * 6. Otherwise, add accumulated constraints to explanation for the next viable solution, prune
-     *    viable solutions by excluding the previous guess.
-     *
      */
     void solver::resolve_conflict() {        
         LOG_H2("Resolve conflict");
@@ -472,9 +459,7 @@ namespace polysat {
 
         if (m_conflict.conflict_var() != null_var) {
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
-            VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict));
-            // TBD: make sure last value decision is blocked by this conflict.
-            // A conflict in test_l5 reverts v1 = 2 more than once.
+            VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict));           
         }
 
         search_iterator search_it(m_search);
@@ -491,8 +476,7 @@ namespace polysat {
                     continue;
                 }
                 justification& j = m_justification[v];
-                LOG("Justification: " << j);
-                if (j.level() > base_level() && !resolve_value(v) && j.is_decision()) {
+                if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
                     revert_decision(v);
                     return;
                 }
@@ -520,11 +504,6 @@ namespace polysat {
         report_unsat();
     }
 
-    /** Conflict resolution case where propagation 'v := ...' is on top of the stack */
-    bool solver::resolve_value(pvar v) {
-        return m_conflict.resolve_value(v);
-    }
-
     /**
     * Variable activity accounting.
     * As a placeholder we increment activity 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 97213f388..1d4405911 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -184,7 +184,6 @@ namespace polysat {
         unsigned base_level() const;
 
         void resolve_conflict();
-        bool resolve_value(pvar v);
         void resolve_bool(sat::literal lit);
         void revert_decision(pvar v);
         void revert_bool_decision(sat::literal lit);
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index f9807a0c7..3beb72e87 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -187,7 +187,7 @@ namespace polysat {
                     // pass
                 }
                 else if (e->interval.lo_val() <= coeff_val) {
-                    rational lambda_u = floor((max_value - coeff_val - 1) / e->coeff);
+                    rational lambda_u = floor((max_value - coeff_val) / e->coeff);
                     hi = val + lambda_u + 1;
                     if (hi > max_value)
                         hi = 0;