From a6771eb56724fb2b6662250320a68393481813b8 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 16 Mar 2023 16:50:09 +0100
Subject: [PATCH] bool watch: order by search index instead of decision level

---
 src/math/polysat/boolean.cpp |  5 +++--
 src/math/polysat/boolean.h   |  5 ++++-
 src/math/polysat/solver.cpp  | 12 ++++++------
 src/math/polysat/solver.h    |  1 +
 4 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index e61cfc4d1..1b002d604 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -12,6 +12,7 @@ Author:
 --*/
 #include "math/polysat/boolean.h"
 #include "math/polysat/clause.h"
+#include "math/polysat/solver.h"
 #include "math/polysat/log.h"
 
 namespace polysat {
@@ -131,14 +132,14 @@ namespace polysat {
     }
 
     /**
-     * A literal may be watched if there is no unwatched literal at higher level,
+     * A literal may be watched if there is no unwatched literal that has been assigned later,
      * where true and unassigned literals are considered at infinite level.
      * We prefer true literals to unassigned literals.
      */
     uint64_t bool_var_manager::get_watch_level(sat::literal lit) const {
         switch (value(lit)) {
             case l_false:
-                return level(lit);
+                return s.m_search.get_bool_index(lit);
             case l_true:
                 return std::numeric_limits<uint64_t>::max();
             case l_undef:
diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index 9acb40eac..7b3213571 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -15,6 +15,8 @@ Author:
 
 namespace polysat {
 
+    class solver;
+
     class bool_var_manager {
 
         enum class kind_t {
@@ -28,6 +30,7 @@ namespace polysat {
             evaluation,
         };
 
+        solver&                     s;
         svector<sat::bool_var>      m_unused;   // previously deleted variables that can be reused by new_var();
         svector<lbool>              m_value;    // current value (indexed by literal)
         unsigned_vector             m_level;    // level of assignment (indexed by variable)
@@ -41,7 +44,7 @@ namespace polysat {
         bool invariant(sat::literal lit) const { return invariant(lit.var()); }
 
     public:
-        bool_var_manager() {}
+        bool_var_manager(solver& s): s(s) {}
 
         // allocated size (not the number of active variables)
         unsigned size() const { return m_level.size(); }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index a3cb46fdc..12d4b4606 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -42,7 +42,7 @@ namespace polysat {
         m_simplify_clause(*this),
         m_simplify(*this),
         m_restart(*this),
-        m_bvars(),
+        m_bvars(*this),
         m_free_pvars(m_activity),
         m_constraints(*this),
         m_search(*this) {
@@ -499,7 +499,7 @@ namespace polysat {
         // - false literal, propagated at higher level than lit
         //   (may happen if a clause has been generated that propagated lit at a lower than current level)
         unsigned i = cl.size();
-        uint64_t i_lvl = m_bvars.level(lit);
+        uint64_t i_lvl = m_bvars.get_watch_level(~lit);
         for (unsigned j = 2; j < cl.size(); ++j) {
             uint64_t j_lvl = m_bvars.get_watch_level(cl[j]);
             if (i_lvl < j_lvl) {
@@ -1794,10 +1794,10 @@ namespace polysat {
         }
         // Check watch literal invariant for long clauses:
         // - true literals may always be watched
-        // - if at least one true literal is watched, the clause is fine
-        // - otherwise, a literal may only be watched if there is no unwatched literal at higher level.
+        // - if at least one true literal is watched, the clause is fine ... (or at least, we cannot detect violations because we do not update watches after a true literal is watched)
+        // - otherwise, a literal may only be watched if there is no unwatched literal at higher search-queue-index.
         auto const get_watch_level = [&](sat::literal lit) -> unsigned {
-            return m_bvars.is_false(lit) ? m_bvars.level(lit) : UINT_MAX;
+            return m_bvars.is_false(lit) ? m_search.get_bool_index(lit) : UINT_MAX;
         };
         for (clause const& cl : m_constraints.clauses()) {
             if (cl.size() <= 2)
@@ -1813,7 +1813,7 @@ namespace polysat {
             for (unsigned i = 2; i < cl.size(); ++i)
                 lvl_tail = std::max(lvl_tail, get_watch_level(cl[i]));
             if (lvl_cl0 < lvl_tail || lvl_cl1 < lvl_tail) {
-                verbose_stream() << "Broken constraint on levels of watched literals of clause: " << cl << "\n";
+                verbose_stream() << "Broken constraint on index of watched literals of clause: " << cl << "\n";
                 for (sat::literal lit : cl) {
                     verbose_stream() << "    " << lit_pp(*this, lit);
                     if (count(m_bvars.watch(lit), &cl) != 0)
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 3ace14a98..c61978910 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -106,6 +106,7 @@ namespace polysat {
 
         // TODO: Why so many friends? Can't we just make the relevant functions public?
         friend class assignment;
+        friend class bool_var_manager;
         friend class constraint;
         friend class ule_constraint;
         friend class umul_ovfl_constraint;