From 7be82a36f2f17ab31c6b72b4c5cdbed8ddf53db8 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 28 Sep 2022 15:16:05 +0200
Subject: [PATCH] Recognize x != k among new literals in lemma

---
 src/math/polysat/constraint.h        |  5 ++-
 src/math/polysat/simplify_clause.cpp | 58 ++++++++++++++++++++++++++++
 src/math/polysat/simplify_clause.h   |  1 +
 src/test/polysat.cpp                 |  2 +-
 4 files changed, 64 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index fbc0c8a26..88f7ec34b 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -237,7 +237,8 @@ namespace polysat {
         }
 
         void negate() { m_positive = !m_positive; }
-        signed_constraint operator~() const { return {get(), !is_positive()}; }
+        signed_constraint negated() const { return {get(), !is_positive()}; }
+        signed_constraint operator~() const { return negated(); }
 
         bool is_positive() const { return m_positive; }
         bool is_negative() const { return !is_positive(); }
@@ -268,7 +269,9 @@ namespace polysat {
         constraint const& operator*() const { return *m_constraint; }
 
         bool is_eq() const;
+        bool is_diseq() const { return negated().is_eq(); }
         pdd const& eq() const;
+        pdd const& diseq() const { return negated().eq(); }
 
         signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }
 
diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
index 2401f1459..389d44c09 100644
--- a/src/math/polysat/simplify_clause.cpp
+++ b/src/math/polysat/simplify_clause.cpp
@@ -61,11 +61,69 @@ namespace polysat {
     {}
 
     bool simplify_clause::apply(clause& cl) {
+        if (try_recognize_bailout(cl))
+            return true;
         if (try_equal_body_subsumptions(cl))
             return true;
         return false;
     }
 
+    // If x != k appears among the new literals, all others are superfluous
+    bool simplify_clause::try_recognize_bailout(clause& cl) {
+        LOG_H2("Try to find bailout literal");
+        pvar v = null_var;
+        sat::literal eq = sat::null_literal;
+        rational k;
+        for (sat::literal lit : cl) {
+            LOG_V("Examine " << lit_pp(s, lit));
+            lbool status = s.m_bvars.value(lit);
+            // skip premise literals
+            if (status == l_false)
+                continue;
+            SASSERT(status != l_true);  // would be an invalid lemma
+            SASSERT_EQ(status, l_undef);  // new literal
+            auto c = s.lit2cnstr(lit);
+            // For now we only handle the case where exactly one variable is
+            // unassigned among the new constraints
+            for (pvar w : c->vars()) {
+                if (s.is_assigned(w))
+                    continue;
+                if (v == null_var)
+                    v = w;
+                else if (v != w)
+                    return false;
+            }
+            SASSERT(v != null_var);  // constraints without unassigned variables would be evaluated at this point
+            if (c.is_diseq() && c.diseq().is_unilinear()) {
+                pdd const& p = c.diseq();
+                if (p.hi().is_one()) {
+                    eq = lit;
+                    k = (-p.lo()).val();
+                }
+            }
+        }
+        if (eq == sat::null_literal)
+            return false;
+        LOG("Found bailout literal: " << lit_pp(s, eq));
+        // Keep all premise literals and the equation
+        unsigned j = 0;
+        for (unsigned i = 0; i < cl.size(); ++i) {
+            sat::literal const lit = cl[i];
+            lbool const status = s.m_bvars.value(lit);
+            if (status == l_false || lit == eq)
+                cl[j++] = cl[i];
+            else {
+                DEBUG_CODE({
+                    auto a = s.assignment();
+                    a.push_back({v, k});
+                    SASSERT(s.lit2cnstr(lit).is_currently_false(s, a));
+                });
+            }
+        }
+        cl.m_literals.shrink(j);
+        return true;
+    }
+
     /**
      * Abstract body of the polynomial (i.e., the variable terms without constant term)
      * by a single variable.
diff --git a/src/math/polysat/simplify_clause.h b/src/math/polysat/simplify_clause.h
index 3670b2194..b24b79de3 100644
--- a/src/math/polysat/simplify_clause.h
+++ b/src/math/polysat/simplify_clause.h
@@ -29,6 +29,7 @@ namespace polysat {
         solver& s;
         vector<subs_entry> m_entries;
 
+        bool try_recognize_bailout(clause& cl);
         bool try_equal_body_subsumptions(clause& cl);
 
         void prepare_subs_entry(subs_entry& entry, signed_constraint c);
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index a4a12e681..5f5ff4d77 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1408,7 +1408,7 @@ void tst_polysat() {
     // test_polysat::test_pop_conflict();  // ok now (had bad conflict/pop interaction)
 
     // test_polysat::test_l1();   // ok
-    // test_polysat::test_l2();   // TODO: loops
+    // test_polysat::test_l2();   // ok but enumerates values
     // test_polysat::test_l3();   // ok
     // test_polysat::test_l4();   // ok now (had assertion failure in conflict::insert)
     // test_polysat::test_l4b();  // ok