From fe164c843dda6ee55b14ec53dbf0e3a2be43e83a Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 1 Feb 2023 14:52:06 +0100
Subject: [PATCH] Fix/simplify constraint_manager::watch

---
 src/math/polysat/constraint_manager.cpp | 40 -------------------------
 src/math/polysat/solver.cpp             | 24 +++++----------
 2 files changed, 7 insertions(+), 57 deletions(-)

diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index 4ba310bcf..f6ea3aadb 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -143,46 +143,6 @@ namespace polysat {
         if (cl.empty())
             return;
 
-        {
-            // First, try to bool-propagate.
-            // Otherwise, we might get a clause-conflict and a missed propagation after resolving the conflict.
-            // With this, we will get a constraint-conflict instead.
-            // TODO: maybe it makes sense to choose bool vs. eval depending on which has the lower level?
-            sat::literal undef_lit = sat::null_literal;
-            for (sat::literal lit : cl) {
-                if (s.m_bvars.is_false(lit))
-                    continue;
-                if (s.m_bvars.is_true(lit)) {
-                    undef_lit = sat::null_literal;
-                    break;
-                }
-                SASSERT(!s.m_bvars.is_assigned(lit));
-                if (undef_lit == sat::null_literal)
-                    undef_lit = lit;
-                else {
-                    undef_lit = sat::null_literal;
-                    break;
-                }
-            }
-            if (undef_lit != sat::null_literal)
-                s.assign_propagate(undef_lit, cl);
-
-            // this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?)
-            // (this loop also masks the mistake of calling clause_builder::insert instead of clause_builder::insert_eval)
-            for (sat::literal lit : cl) {
-                if (s.m_bvars.is_false(lit))
-                    continue;
-                signed_constraint sc = s.lit2cnstr(lit);
-                if (sc.is_currently_false(s)) {
-                    if (s.m_bvars.is_true(lit)) {
-                        s.set_conflict(sc);
-                        return;
-                    }
-                    s.assign_eval(~lit);
-                }
-            }
-        }
-
         if (cl.size() == 1) {
             if (s.m_bvars.is_false(cl[0]))
                 s.set_conflict(cl);
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index db2aeacd9..c660de34c 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1193,30 +1193,20 @@ namespace polysat {
         }
     }
 
-    // Add clause to storage
+    // Add clause to solver
     void solver::add_clause(clause& clause) {
         LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
         for (sat::literal lit : clause) {
-            LOG("   " << lit_pp(*this, lit));
-            // TODO: move into constraint_manager::watch
+            // Try to evaluate literals without boolean value.
+            // (Normally this should have been done already by using clause_builder::insert_eval/insert_try_eval when constructing the clause.)
             if (!m_bvars.is_assigned(lit)) {
-                switch (lit2cnstr(lit).eval(*this)) {
-                case l_true:
+                lbool const status = lit2cnstr(lit).eval(*this);
+                if (status == l_true)
                     assign_eval(lit);
-                    break;
-                case l_false:
+                else if (status == l_false)
                     assign_eval(~lit);
-                    break;
-                default:
-                    break;
-                }
-            }
-            // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
-            if (m_bvars.value(lit) == l_true) {
-                // in this case the clause is useless
-                LOG("   Clause is already true, skipping...");
-                return;
             }
+            LOG("    " << lit_pp(*this, lit));
         }
         SASSERT(!clause.empty());
         m_constraints.store(&clause);