generalize subsumption to non-univariate

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/dd/dd_pdd.cpp

@@ -1736,6 +1736,14 @@ namespace dd {
         return p.val();
     }
 
+    rational const& pdd::offset() const {
+        pdd p = *this;
+        while (!p.is_val())
+            p = p.lo();
+        return p.val();        
+    }
+ 
+
     pdd pdd::shl(unsigned n) const {
         return (*this) * rational::power_of_two(n);
     }

src/math/dd/dd_pdd.h

@@ -407,6 +407,7 @@ namespace dd {
         unsigned var() const { return m.var(root); }
         rational const& val() const { SASSERT(is_val()); return m.val(root); }
         rational const& leading_coefficient() const;
+        rational const& offset() const;
         bool is_val() const { return m.is_val(root); }
         bool is_one() const { return m.is_one(root); }
         bool is_zero() const { return m.is_zero(root); }

src/math/polysat/simplify_clause.cpp

@@ -21,18 +21,63 @@ namespace polysat {
         s(s)
     {}
 
-    bool simplify_clause::apply(clause& cl)
+    bool simplify_clause::apply(clause& cl) {
-    {
         bool changed = false;
-        if (try_unilinear_subsumption(cl)) changed = true;
+        if (try_unilinear_subsumption(cl)) 
+            changed = true;
         return changed;
     }
 
-    struct subs_entry : fi_record {
+    pdd simplify_clause::abstract(pdd const& p, pdd& v) {
-        unsigned lit_idx;
+        if (p.is_val())
-        pvar var;
+            return p;
-        bool subsumed;
+        if (p.is_unilinear()) {
-    };
+            v = p.manager().mk_var(p.var());
+            return p;
+        }
+        unsigned max_var = p.var();
+        auto& m = p.manager();
+        pdd r(m);
+        v = p - p.offset();
+        r = p - v;
+        if (p.leading_coefficient() < 0) {
+            v = -v;
+            r -= m.mk_var(max_var);
+        }
+        else 
+            r += m.mk_var(max_var);
+        return r;
+    }
+
+    void simplify_clause::prepare_subs_entry(subs_entry& entry, signed_constraint c) {
+        entry.valid = false;
+        if (!c->is_ule())
+            return;
+        forbidden_intervals fi(s);
+
+        auto const& ule = c->to_ule();
+        auto& m = ule.lhs().manager();
+        signed_constraint sc = c;
+        pdd v_lhs(m), v_rhs(m);
+        pdd lhs = abstract(ule.lhs(), v_lhs);
+        pdd rhs = abstract(ule.rhs(), v_rhs);
+        if (lhs.is_val() && rhs.is_val())
+            return;
+        if (!lhs.is_val() && !rhs.is_val() && v_lhs != v_rhs)
+            return;
+        if (lhs != ule.lhs() || rhs != ule.rhs()) {
+            sc = s.ule(lhs, rhs);
+            if (c.is_negative())
+                sc.negate();
+        }
+        pvar v = rhs.is_val() ? lhs.var() : rhs.var();
+        VERIFY(fi.get_interval(sc, v, entry));
+        if (entry.coeff != 1)
+            return;
+        entry.var = lhs.is_val() ? v_rhs : v_lhs;
+        entry.subsumed = false;
+        entry.valid = true;
+    }
 
     /**
      * Test simple subsumption between univariate and linear literals, i.e.,
@@ -41,87 +86,44 @@ namespace polysat {
      * A literal C subsumes literal D if the forbidden interval of C is a subset of the forbidden interval of D.
      * C subsumes D  <==  fi(C) subset fi(D)
      */
-    bool simplify_clause::try_unilinear_subsumption(clause& cl)
+    bool simplify_clause::try_unilinear_subsumption(clause& cl) {
-    {
         LOG_H2("Unilinear subsumption for: " << cl);
-        subs_entry entry;
+
-        vector<subs_entry> entries;  // TODO: we don't need to store the full fi_record
+        m_entries.reserve(cl.size());
-        forbidden_intervals fi(s);
-        // Find univariate and linear constraints and their forbidden intervals
         for (unsigned i = 0; i < cl.size(); ++i) {
+            subs_entry& entry = m_entries[i];
             sat::literal lit = cl[i];
-            signed_constraint c = s.lit2cnstr(lit);
-            if (!c->is_ule())
-                continue;
-            auto const& ule = c->to_ule();
-            pdd const& lhs = ule.lhs();
-            pdd const& rhs = ule.rhs();
-            if (!lhs.is_val() && !lhs.is_unilinear())
-                continue;
-            if (!rhs.is_val() && !rhs.is_unilinear())
-                continue;
-            if (!lhs.is_val() && !rhs.is_val() && lhs.var() != rhs.var())
-                continue;
             LOG("Literal " << lit_pp(s, lit));
-            SASSERT(!lhs.is_val() || !rhs.is_val());  // purely numeric constraints should have been filtered out by the clause_builder
+            signed_constraint c = s.lit2cnstr(lit);
-            pvar v = rhs.is_val() ? lhs.var() : rhs.var();
+            prepare_subs_entry(entry, c);
-            VERIFY(fi.get_interval(c, v, entry));
-            if (entry.coeff != 1)
-                continue;
-            entry.lit_idx = i;
-            entry.var = v;
-            entry.subsumed = false;
-            entries.push_back(entry);
         }
+        
         // Check subsumption between intervals for the same variable
         bool any_subsumed = false;
-        for (unsigned i = 0; i < entries.size(); ++i) {
+        for (unsigned i = 0; i < cl.size(); ++i) {
-            subs_entry& e = entries[i];
+            subs_entry& e = m_entries[i];
-            if (e.subsumed)
+            if (e.subsumed || !e.valid)
                 continue;
-            for (unsigned j = i + 1; j < entries.size(); ++j) {
+            for (unsigned j = 0; j < cl.size(); ++j) {
-                subs_entry& f = entries[j];
+                subs_entry& f = m_entries[j];
-                SASSERT(e.lit_idx != f.lit_idx);
+                if (f.subsumed || !f.valid || i == j || !e.var || !f.var || *e.var != *f.var)
-                if (e.var != f.var)
                     continue;
                 if (e.interval.currently_contains(f.interval)) {
                     // f subset of e  ==>  f.src subsumes e.src
-                    LOG("Literal " << cl[e.lit_idx] << " subsumed by " << cl[f.lit_idx]);
+                    LOG("Literal " << s.lit2cnstr(cl[i]) << " subsumed by " << s.lit2cnstr(cl[j]) << "\n");
                     e.subsumed = true;
                     any_subsumed = true;
                     break;
                 }
-                if (f.interval.currently_contains(e.interval)) {
-                    // e subset of f  ==>  e.src subsumes f.src
-                    LOG("Literal " << cl[f.lit_idx] << " subsumed by " << cl[e.lit_idx]);
-                    f.subsumed = true;
-                    any_subsumed = true;
-                    continue;
-                }
             }
         }
         // Remove subsumed literals
         if (!any_subsumed)
             return false;
-        auto e_it = entries.begin();
+        unsigned j = 0;
-        while (e_it != entries.end() && !e_it->subsumed)
+        for (unsigned i = 0; i < cl.size(); ++i) 
-            ++e_it;
+            if (!m_entries[i].subsumed)
-        SASSERT(e_it != entries.end() && e_it->subsumed);
+                cl[j++] = cl[i];
-        unsigned next_subsumed_i = e_it->lit_idx;
-        unsigned i = next_subsumed_i;
-        unsigned j = next_subsumed_i;
-        while (i < cl.size()) {
-            if (i == next_subsumed_i) {
-                while (e_it != entries.end() && !e_it->subsumed)
-                    ++e_it;
-                if (e_it != entries.end())
-                    next_subsumed_i = e_it->lit_idx;
-                // NOTE: no need to update next_subsumed_i in the else-branch since we already passed that location
-                i++;
-            }
-            else
-                cl[j++] = cl[i++];
-        }
         cl.m_literals.shrink(j);
         return true;
     }

src/math/polysat/simplify_clause.h

@@ -12,16 +12,29 @@ Author:
 --*/
 #pragma once
 #include "math/polysat/constraint.h"
+#include "math/polysat/forbidden_intervals.h"
 
 namespace polysat {
 
     class solver;
 
     class simplify_clause {
+
+        struct subs_entry : fi_record {
+            optional<pdd>  var;
+            bool subsumed = false;
+            bool valid = false;
+        };
+
         solver& s;
+        vector<subs_entry> m_entries;
 
         bool try_unilinear_subsumption(clause& cl);
 
+        void prepare_subs_entry(subs_entry& entry, signed_constraint c);
+
+        pdd abstract(pdd const& p, pdd& v);
+        
     public:
         simplify_clause(solver& s);