na

src/math/polysat/conflict.cpp

@@ -308,9 +308,8 @@ namespace polysat {
             for (auto const& c : s.m_viable.get_constraints(v))
                 insert(c);        
 
-        for (auto* engine : ex_engines)
-            if (engine->try_explain(v, *this))
-                return true;
+        if (try_explain(v))
+            return true;
 
         // No value resolution method was successful => fall back to saturation and variable elimination
         while (s.inc()) {
@@ -345,6 +344,13 @@ namespace polysat {
         return false;
     }
 
+    bool conflict::try_explain(pvar v) {
+        for (auto* engine : ex_engines)
+            if (engine->try_explain(v, *this))
+                return true;
+        return false;
+    }
+
     void conflict::set_mark(signed_constraint c) {
         if (c->is_marked())
             return;

src/math/polysat/conflict.h

@@ -110,6 +110,7 @@ namespace polysat {
 
         bool try_eliminate(pvar v);
         bool try_saturate(pvar v);
+        bool try_explain(pvar v);
 
         using const_iterator = conflict_iterator;
         const_iterator begin() const;

src/math/polysat/constraint.cpp

@@ -202,6 +202,21 @@ namespace polysat {
         return ~ule(b, a); 
     }
 
+    bool signed_constraint::is_eq() const {
+        if (is_positive())
+            return m_constraint->is_eq();
+        else
+            return m_constraint->is_diseq();
+    }
+
+    pdd const& signed_constraint::eq() const {
+        SASSERT(is_eq());
+        if (is_positive())
+            return m_constraint->to_ule().lhs();
+        else
+            return m_constraint->to_ule().rhs();        
+    }
+
     /**
     * encode that the i'th bit of p is 1.
     * It holds if p << (K - i - 1) >= 2^{K-1}, where K is the bit-width.

src/math/polysat/constraint.h

@@ -159,6 +159,7 @@ namespace polysat {
         bool operator!=(constraint const& other) const { return !operator==(other); }
 
         virtual bool is_eq() const { return false; }
+        virtual bool is_diseq() const { return false; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }
         bool is_mul_ovfl() const { return m_kind == ckind_t::mul_ovfl_t; }
         ckind_t kind() const { return m_kind; }
@@ -253,6 +254,9 @@ namespace polysat {
         constraint& operator*() { return *m_constraint; }
         constraint const& operator*() const { return *m_constraint; }
 
+        bool is_eq() const;
+        pdd const& eq() const;
+
 
         signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }
 

src/math/polysat/explain.cpp

@@ -24,8 +24,8 @@ namespace polysat {
         LOG_H3("Resolving upon v" << v);
         LOG("c1: " << c1);
         LOG("c2: " << c2);
-        pdd a = c1->to_ule().p();
-        pdd b = c2->to_ule().p();
+        pdd a = c1.eq();
+        pdd b = c2.eq();
         pdd r = a;
         if (!a.resolve(v, b, r) && !b.resolve(v, a, r))
             return {};
@@ -40,30 +40,19 @@ namespace polysat {
         return c;
     }
 
-    bool ex_polynomial_superposition::is_positive_equality_over(pvar v, signed_constraint const& c) {
-        return c.is_positive() && c->is_eq() && c->contains_var(v);
-    }
 
     // c2 ... constraint that is currently false
     // Try to replace it with a new false constraint (derived from superposition with a true constraint)
     lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
         vector<signed_constraint> premises;
 
-        // TBD: replacement can be obtained from stack not just core.
-        // see test_l5. Exposes unsoundness bug: a new consequence is derived 
-        // after some variable decision was already processed. Then the 
-        // behavior of evaluating literals "is_currently_true" and bvalue
-        // uses the full search stack
-#if 1
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
-            auto c1 = s.lit2cnstr(si.lit());
-        
-#else
-        for (auto c1 : core) {
-#endif
-            if (!is_positive_equality_over(v, c1))
+            auto c1 = s.lit2cnstr(si.lit());       
+            if (!c1->contains_var(v))
+                continue;
+            if (!c1.is_eq())
                 continue;
             if (!c1.is_currently_true(s))
                 continue;
@@ -107,7 +96,9 @@ namespace polysat {
     // TODO: can try multiple replacements at once; then the c2 loop needs to be done only once... (requires some reorganization for storing the premises)
     lbool ex_polynomial_superposition::try_explain1(pvar v, conflict& core) {
         for (auto c2 : core) {
-            if (!is_positive_equality_over(v, c2))
+            if (!c2->contains_var(v))
+                continue;
+            if (!c2.is_eq())
                 continue;
             if (!c2.is_currently_false(s))
                 continue;
@@ -124,52 +115,68 @@ namespace polysat {
     }
 
     void ex_polynomial_superposition::reduce_by(pvar v, conflict& core) {
-        //return;
         bool progress = true;
         while (progress) {
             progress = false;
             for (auto c : core) {
-                if (is_positive_equality_over(v, c) && c.is_currently_true(s) && reduce_by(v, c, core)) {
-                    progress = true;
-                    break;
-                }
+                if (!c->contains_var(v))
+                    continue;
+                if (!c.is_eq())
+                    continue;
+#if 0
+                if (!c.is_currently_true(s))
+                    continue;
+#endif
+
+                if (!reduce_by(v, c, core))
+                    continue;
+                progress = true;
+                break;                
             }
         }
     }
 
     bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict& core) {
-        pdd p = eq->to_ule().p();
+        pdd p = eq.eq();
+        LOG("using v" << v << " " << eq);
         for (auto c : core) {
             if (c == eq)
                 continue;
-            if (is_positive_equality_over(v, c))
+            if (!c->contains_var(v))
                 continue;
+            if (c.is_eq())
+                continue;
+            LOG("try-reduce: " << c << " " << c.is_currently_false(s));
+#if 0
             if (!c.is_currently_false(s))
                 continue;
-            if (c->is_ule()) {
-                auto lhs = c->to_ule().lhs();
-                auto rhs = c->to_ule().rhs();
-                auto a = lhs.reduce(v, p);
-                auto b = rhs.reduce(v, p);
-                if (a == lhs && b == rhs)
-                    continue;
-                auto c2 = s.ule(a, b);
-                if (!c.is_positive())
-                    c2 = ~c2;
-                SASSERT(c2.is_currently_false(s));                
-                if (!c2->has_bvar() || l_undef == c2.bvalue(s))
-                    core.keep(c2);  // adds propagation of c to the search stack
-                core.reset();
-                LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2);
-                if (c2.bvalue(s) == l_false) {
-                    core.insert(eq);
-                    core.insert(c);
-                    core.insert(~c2);
-                    return false;
-                }
-                core.set(c2);                
-                return true;
+#endif
+            if (!c->is_ule())
+                continue;
+            auto lhs = c->to_ule().lhs();
+            auto rhs = c->to_ule().rhs();
+            auto a = lhs.reduce(v, p);
+            auto b = rhs.reduce(v, p);
+            if (a == lhs && b == rhs)
+                continue;
+            auto c2 = s.ule(a, b);
+            if (!c.is_positive())
+                c2 = ~c2;
+            if (!c2.is_currently_false(s))
+                continue;
+            SASSERT(c2.is_currently_false(s));
+            if (!c2->has_bvar() || l_undef == c2.bvalue(s))
+                core.keep(c2);  // adds propagation of c to the search stack
+            core.reset();
+            LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2);
+            if (c2.bvalue(s) == l_false) {
+                core.insert(eq);
+                core.insert(c);
+                core.insert(~c2);
+                return false;
             }
+            core.set(c2);
+            return true;
         }
         return false;
     }

src/math/polysat/explain.h

@@ -33,7 +33,6 @@ namespace polysat {
 
     class ex_polynomial_superposition : public explainer {
     private:
-        bool is_positive_equality_over(pvar v, signed_constraint const& c);
         signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2);
         lbool find_replacement(signed_constraint c2, pvar v, conflict& core);
         void reduce_by(pvar v, conflict& core);

src/math/polysat/mul_ovfl_constraint.cpp

@@ -134,6 +134,8 @@ namespace polysat {
         //std::cout << "Already true " << conseq.is_currently_true(s) << "\n";
 
         SASSERT(premise.is_currently_true(s));
+        SASSERT(bound * p.val() > max);
+        SASSERT((bound - 1) * p.val() <= max);
         clause_builder cb(s);
         cb.push_new(~sc);
         cb.push_new(~premise);

src/math/polysat/solver.cpp

@@ -462,9 +462,15 @@ namespace polysat {
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
             VERIFY(m_viable.resolve(v, m_conflict));
             // TBD: saturate resulting conflict to get better lemmas.
-            LOG("try-saturate");
-            m_conflict.try_saturate(v);
-            LOG("end-try-saturate");
+            LOG("try-eliminate v" << v);
+            if (m_conflict.try_explain(v))
+                ;
+            else if (m_conflict.try_eliminate(v))
+                ;
+            else
+                m_conflict.try_saturate(v);
+            
+            LOG("end-try-eliminate v");
         }
 
         search_iterator search_it(m_search);

src/math/polysat/ule_constraint.h

@@ -41,7 +41,8 @@ namespace polysat {
         unsigned hash() const override;
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return m_rhs.is_zero(); }
-        pdd const& p() const { SASSERT(is_eq()); return m_lhs; }
+        bool is_diseq() const override { return m_lhs.is_one(); }
+        // pdd const& p() const { SASSERT(is_eq()); return m_lhs; }
     };
 
 }

src/math/polysat/viable.cpp

@@ -170,6 +170,7 @@ namespace polysat {
     *   and division with coeff are valid. Is there a more relaxed scheme?
     */
     bool viable::refine_viable(pvar v, rational const& val) {
+        //return true;
         auto* e = m_non_units[v];
         if (!e)
             return true;
@@ -408,7 +409,7 @@ namespace polysat {
         }             
         while (e != first);
 
-        core.set_bailout();
+        // core.set_bailout();
         for (auto c : core) {
             if (c.bvalue(s) == l_false) {
                 core.reset();