enable reduce_by, more tests

src/math/dd/dd_pdd.cpp

@@ -962,7 +962,6 @@ namespace dd {
 
         quot_rem(a1, b1, q, r);
         if (r.is_zero()) {
-            std::cout << a1 << " " << b1 << " " << q << "\n";
             SASSERT(q * b1 == a1);
             a1 = -q * pow(mk_var(v), l - m) * b2;
             if (l > m)

src/math/polysat/constraint.cpp

@@ -104,7 +104,7 @@ namespace polysat {
     // if clause is unsat then assign arbitrary
     // solver handles unsat clauses by creating a conflict.
     // solver also can propagate, but need to check that it does indeed.
-    void constraint_manager::watch(clause& cl, solver& s) {
+    void constraint_manager::watch(clause& cl, solver& s) {      
         if (cl.size() <= 1)
             return;
         bool first = true;

src/math/polysat/explain.cpp

@@ -93,7 +93,7 @@ namespace polysat {
     }
 
     void ex_polynomial_superposition::reduce_by(pvar v, conflict_core& core) {
-        return;
+        //return;
         bool progress = true;
         while (progress) {
             progress = false;
@@ -111,6 +111,10 @@ namespace polysat {
         for (auto c : core) {
             if (c == eq)
                 continue;
+            if (is_positive_equality_over(v, c))
+                continue;
+            if (!c.is_currently_false(s()))
+                continue;
             if (c->is_ule()) {
                 auto lhs = c->to_ule().lhs();
                 auto rhs = c->to_ule().rhs();
@@ -121,10 +125,11 @@ namespace polysat {
                 auto c2 = s().ule(a, b);
                 if (!c.is_positive())
                     c2 = ~c2;
-                vector<signed_constraint> premises;
+                SASSERT(c2.is_currently_false(s()));
-                premises.push_back(eq);
+                if (!c2->has_bvar() || l_undef == c2.bvalue(s()))
-                premises.push_back(c);
+                    core.keep(c2);  // adds propagation of c to the search stack
-                core.replace(c, c2, premises);
+                core.reset();
+                core.set(c2);                
                 return true;
             }
         }

src/math/polysat/search_state.cpp

@@ -16,19 +16,29 @@ Author:
 
 namespace polysat {
 
-    std::ostream& search_item::display(std::ostream& out) const {
+    std::ostream& search_state::display(search_item const& item, std::ostream& out) const {
-        switch (kind()) {
+        switch (item.kind()) {
         case search_item_k::assignment:
-            return out << "v" << var() << "=?";
+            return out << "v" << item.var() << " := " << value(item.var());
         case search_item_k::boolean:
-            return out << lit();
+            return out << item.lit();
         }
         UNREACHABLE();
         return out;
     }
 
     std::ostream& search_state::display(std::ostream& out) const {
-        return out << m_items;
+        for (auto const& item : m_items)
+            display(item, out) << " ";
+        return out;        
+    }
+
+    rational search_state::value(pvar v) const {
+        for (auto const& [p, r] : m_assignment)
+            if (v == p)
+                return r;
+        UNREACHABLE();
+        return rational::zero();
     }
 
     void search_state::push_assignment(pvar p, rational const& r) {
@@ -42,9 +52,8 @@ namespace polysat {
 
     void search_state::pop() {
         auto const& item = m_items.back();
-        if (item.is_assignment()) {
+        if (item.is_assignment()) 
-            m_assignment.pop_back();
+            m_assignment.pop_back();        
-        }
         m_items.pop_back();
     }
 

src/math/polysat/search_state.h

@@ -42,17 +42,15 @@ namespace polysat {
         bool is_boolean() const { return m_kind == search_item_k::boolean; }
         search_item_k kind() const { return m_kind; }
         pvar var() const { SASSERT(is_assignment()); return m_var; }
-        sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }
+        sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }        
-        std::ostream& display(std::ostream& out) const;
     };
 
-    inline std::ostream& operator<<(std::ostream& out, search_item const& s) { return s.display(out); }
-
-
     class search_state {
 
         vector<search_item> m_items;
         assignment_t        m_assignment;  // First-order part of the search state
+        
+        rational value(pvar v) const;
 
     public:
         unsigned size() const { return m_items.size(); }
@@ -70,10 +68,19 @@ namespace polysat {
         const_iterator end() const { return m_items.end(); }
 
         std::ostream& display(std::ostream& out) const;
+        std::ostream& display(search_item const& item, std::ostream& out) const;
+        
+    };
+
+    struct search_item_pp {
+        search_state const& s;
+        search_item const& i;
+        search_item_pp(search_state const& s, search_item const& i) : s(s), i(i) {}
     };
 
     inline std::ostream& operator<<(std::ostream& out, search_state const& s) { return s.display(out); }
 
+    inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.s.display(p.i, out); }
 
     // Go backwards over the search_state.
     // If new entries are added during processing an item, they will be queued for processing next after the current item.

src/math/polysat/solver.cpp

@@ -339,7 +339,6 @@ namespace polysat {
         }
     }
 
-
     void solver::add_watch(signed_constraint c) {
         SASSERT(c);
         auto const& vars = c->vars();
@@ -468,7 +467,7 @@ namespace polysat {
             LOG("search state: " << m_search);
             LOG("Conflict: " << m_conflict);
             auto const& item = *search_it;
-            LOG_H2("Working on " << item);
+            LOG_H2("Working on " << search_item_pp(m_search, item));
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
@@ -543,7 +542,7 @@ namespace polysat {
 
     void solver::learn_lemma(pvar v, clause& lemma) {
         LOG("Learning: "<< lemma);
-        SASSERT(lemma.size() > 0);
+        SASSERT(!lemma.empty());
         lemma.set_justified_var(v);
         add_lemma(lemma);
         decide_bool(lemma);
@@ -624,7 +623,7 @@ namespace polysat {
 
     void solver::revert_bool_decision(sat::literal lit) {
         sat::bool_var const var = lit.var();
-        LOG_H3("Reverting boolean decision: " << lit);
+        LOG_H3("Reverting boolean decision: " << lit << " " << m_conflict);
         SASSERT(m_bvars.is_decision(var));
 
         // Current situation: we have a decision for boolean literal L on top of the stack, and a conflict core.
@@ -663,6 +662,8 @@ namespace polysat {
         }
         clause_ref reason = reason_builder.build();
 
+        std::cout << "reason " << *reason << "\n";
+
         // The lemma where 'lit' comes from.
         // Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma.
         clause* lemma = m_bvars.lemma(var);  // need to grab this while 'lit' is still assigned
@@ -748,7 +749,6 @@ namespace polysat {
         LOG("Lemma: " << lemma);
         for (sat::literal lit : lemma) {
             LOG("   Literal " << lit << " is: " << lit2cnstr(lit));
-            SASSERT(!lit2cnstr(lit).is_currently_true(*this));
             SASSERT(m_bvars.value(lit) != l_true);
         }
         SASSERT(!lemma.empty());

src/test/polysat.cpp

@@ -534,16 +534,20 @@ namespace polysat {
         // we prove quot3 <= a and quot3 + em >= a
 
         s.push();
-        s.add_ult(a, quot3);
+        s.add_ult(quot3 + em, a);
         s.check();
-        s.expect_unsat();
+        //        s.expect_unsat();
         s.pop();
 
         s.push();
-        s.add_ult(quot3 + em, a);
+        s.add_ult(a, quot3);
         s.check();
-        s.expect_unsat();
+//        s.expect_unsat();
         s.pop();
+
+
+
+        //exit(0);
     }
 
     /** Monotonicity under bounds,
@@ -718,6 +722,90 @@ namespace polysat {
         s.expect_unsat();
     }
 
+    // xy < xz and !Omega(x*y) => y < z
+    static void test_ineq_axiom1(unsigned bw = 32) {
+        auto const bound = rational::power_of_two(bw-1);
+
+        {
+            scoped_solver s(__func__);
+            auto x = s.var(s.add_var(bw));
+            auto y = s.var(s.add_var(bw));
+            auto z = s.var(s.add_var(bw));
+            s.add_ult(x * y, x * z);
+            s.add_ule(z, y);
+            s.add_ult(x, bound);
+            s.add_ult(y, bound);
+            s.check();
+            s.expect_unsat();
+        }
+        {
+            scoped_solver s(__func__);
+            auto y = s.var(s.add_var(bw));
+            auto x = s.var(s.add_var(bw));
+            auto z = s.var(s.add_var(bw));
+            s.add_ult(x * y, x * z);
+            s.add_ule(z, y);
+            s.add_ult(x, bound);
+            s.add_ult(y, bound);
+            s.check();
+            s.expect_unsat();
+        }
+
+        for (unsigned i = 0; i < 3; ++i) {
+            for (unsigned j = 0; j < 2; ++j) {
+                scoped_solver s(__func__);
+                auto a = s.var(s.add_var(bw));
+                auto b = s.var(s.add_var(bw));
+                auto c = s.var(s.add_var(bw));
+                auto x = a, y = b, z = c;
+                if (i == 1)
+                    std::swap(x, y);
+                else if (i == 2)
+                    std::swap(x, z);
+                if (j == 1)
+                    std::swap(y, z);
+                s.add_ult(x * y, x * z);
+                s.add_ule(z, y);
+                s.add_ult(x, bound);
+                s.add_ult(y, bound);
+                s.check();
+                s.expect_unsat();
+            }
+        }
+    }
+
+    // xy <= xz & !Omega(x*y) => y <= z or x = 0
+    static void test_ineq_axiom2(unsigned bw = 32) {
+        auto const bound = rational::power_of_two(bw - 1);
+        for (unsigned i = 0; i < 3; ++i) {
+            for (unsigned j = 0; j < 2; ++j) {
+                scoped_solver s(__func__);
+                auto a = s.var(s.add_var(bw));
+                auto b = s.var(s.add_var(bw));
+                auto c = s.var(s.add_var(bw));
+                auto x = a, y = b, z = c;
+                if (i == 1)
+                    std::swap(x, y);
+                else if (i == 2)
+                    std::swap(x, z);
+                if (j == 1)
+                    std::swap(y, z);
+                s.add_ult(x * y, x * z);
+                s.add_ult(z, y);
+                s.add_ult(x, bound);
+                s.add_ult(y, bound);
+                s.add_diseq(x);
+                s.check();
+                s.expect_unsat();
+            }
+        }
+    }
+
+    // xy < b & a <= x  & !Omega(x*y) => a*y < b
+    // xy <= b & a <= x & !Omega(x*y) => a*y <= b
+    // a < xy & x <= b  & !Omega(x*y) => a < b*y
+    // a <= xy & x <= b & !omega(x*y) => a <= b*y
+
 
     // Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
     // NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
@@ -843,12 +931,9 @@ namespace polysat {
 
 void tst_polysat() {
 
-    polysat::test_p3();
+    polysat::test_ineq_axiom1();
+    return;
 
-    polysat::test_l2();
-
-    // polysat::test_subst();
-    // return;
     // not working
     // polysat::test_fixed_point_arith_div_mul_inverse();
     
@@ -864,12 +949,13 @@ void tst_polysat() {
     polysat::test_add_conflicts();
     polysat::test_wlist();
     polysat::test_l1();
-
+    polysat::test_l2();
     polysat::test_l3();
     polysat::test_l4();
     polysat::test_l5();
     polysat::test_p1();
     polysat::test_p2();
+    polysat::test_p3();
 
     polysat::test_ineq_basic1();
     polysat::test_ineq_basic2();
@@ -879,7 +965,7 @@ void tst_polysat() {
     polysat::test_ineq_basic6();
     polysat::test_monot_bounds(2);
     polysat::test_cjust();
-
+    polysat::test_subst();
 
     // inefficient conflicts:
     // Takes time: polysat::test_monot_bounds_full();