initial overflow test

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

src/math/polysat/constraint.cpp

@@ -202,6 +202,9 @@ namespace polysat {
         return ~ule(b, a); 
     }
 
+    signed_constraint constraint_manager::mul_ovfl(pdd const& a, pdd const& b) {
+        return { dedup(alloc(mul_ovfl_constraint, *this, a, b)), true };
+    }
 
 
     // To do signed comparison of bitvectors, flip the msb and do unsigned comparison:

src/math/polysat/constraint.h

@@ -94,6 +94,7 @@ namespace polysat {
         signed_constraint ult(pdd const& a, pdd const& b); 
         signed_constraint sle(pdd const& a, pdd const& b);
         signed_constraint slt(pdd const& a, pdd const& b);
+        signed_constraint mul_ovfl(pdd const& p, pdd const& q);
 
         constraint *const* begin() const { return m_constraints.data(); }
         constraint *const* end() const { return m_constraints.data() + m_constraints.size(); }

src/math/polysat/mul_ovfl_constraint.cpp

@@ -18,7 +18,6 @@ namespace polysat {
 
     mul_ovfl_constraint::mul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q):
         constraint(m, ckind_t::mul_ovfl_t), m_p(p), m_q(q) {
-
         simplify();
         m_vars.append(m_p.free_vars());
         for (auto v : m_q.free_vars())
@@ -33,6 +32,8 @@ namespace polysat {
             m_p = 0;
             return;
         }
+        if (m_p.index() > m_q.index())
+            std::swap(m_p, m_q);
     }
 
     std::ostream& mul_ovfl_constraint::display(std::ostream& out, lbool status) const {
@@ -104,8 +105,6 @@ namespace polysat {
     * TODO optimizations:
     * if p is constant, q variable, update viable for q
     * 
-    * Use bounds on variables in p instead of current assignment as premise.
-    * This is a more general lemma
     */
     bool mul_ovfl_constraint::narrow_bound(solver& s, bool is_positive, 
         pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
@@ -118,22 +117,31 @@ namespace polysat {
         // p * q >= max + 1 <=> q >= (max + 1)/p <=> q >= ceil((max+1)/p)
         auto bound = ceil((max + 1) / p.val());
 
+        //
         // the clause that explains bound <= q or bound > q 
         // 
         // Ovfl(p, q)  & p <= p.val() => q >= bound
         // ~Ovfl(p, q) & p >= p.val() => q < bound 
+        //
 
         signed_constraint sc(this, is_positive);       
         signed_constraint premise = is_positive ? s.ule(p0, p.val()) : s.ule(p.val(), p0);
         signed_constraint conseq = is_positive ? s.ule(bound, q0) : s.ult(q0, bound);
 
-        SASSERT(premise.is_currently_false(s));
+        //std::cout << premise << "\n";
+        //std::cout << sc << "\n";
+        //std::cout << conseq << "\n";
+        //std::cout << "Already true " << conseq.is_currently_true(s) << "\n";
+
+        SASSERT(premise.is_currently_true(s));
         clause_builder cb(s);
         cb.push_new(~sc);
         cb.push_new(~premise);
         cb.push_new(conseq);
         clause_ref just = cb.build();
-        s.assign_propagate(conseq.blit(), *just);
+        s.add_lemma(*just);
+        s.propagate();
+        SASSERT(s.m_bvars.is_true(conseq.blit()));
         return true;
     }
 

src/math/polysat/solver.h

@@ -289,6 +289,8 @@ namespace polysat {
         signed_constraint ult(rational const& p, pdd const& q) { return ult(q.manager().mk_val(p), q); }
         signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); }
         signed_constraint slt(pdd const& p, pdd const& q) { return m_constraints.slt(p, q); }
+        signed_constraint mul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); }
+        signed_constraint mul_ovfl(rational const& p, pdd const& q) { return mul_ovfl(q.manager().mk_val(p), q); }
 
 
         /** Create and activate polynomial constraints. */
@@ -298,6 +300,8 @@ namespace polysat {
         void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(ult(p, q), dep); }
         void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(sle(p, q), dep); }
         void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(slt(p, q), dep); }
+        void add_noovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); }
+        void add_ovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); }
 
         void add_ule(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); }
         void add_ule(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); }
@@ -307,6 +311,10 @@ namespace polysat {
         void add_ult(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); }
         void add_ult(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_ult(p, rational(q), dep); }
         void add_ult(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_ult(rational(p), q, dep); }
+        void add_noovfl(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); }
+        void add_noovfl(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); }
+        void add_noovfl(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_noovfl(p, rational(q), dep); }
+        void add_noovfl(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); }
 
         /**
          * Activate the constraint corresponding to the given boolean variable.

src/math/polysat/viable.cpp

@@ -197,8 +197,8 @@ namespace polysat {
                     rational lambda_l = floor(coeff_val / e->coeff);
                     lo = val - lambda_l;                   
                 }
-                SASSERT(hi <= s.var2pdd(v).max_value());
                 LOG("forbidden interval " << e->interval << " - " << val << " " << coeff_val << " [" << lo << ", " << hi << "[");
+                SASSERT(hi <= max_value);
                 entry* ne = alloc_entry();
                 ne->src = e->src;
                 ne->side_cond = e->side_cond;

src/test/polysat.cpp

@@ -940,6 +940,22 @@ namespace polysat {
         }
     }
 
+    static void test_quot_rem(unsigned bw = 32) {
+        scoped_solver s(__func__);
+        auto a = s.var(s.add_var(bw));
+        auto quot = s.var(s.add_var(bw));
+        auto rem = s.var(s.add_var(bw));
+        auto x = a * 123;
+        auto y = 123;
+        // quot = udiv(a*123, 123)
+        s.add_eq(quot * y + rem - x);
+        s.add_diseq(a - quot);
+        s.add_noovfl(quot, y);     
+        // s.add_ult(rem, x);
+        s.check();
+        s.expect_sat();
+    }
+
 
     // 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)
@@ -1065,6 +1081,9 @@ namespace polysat {
 
 void tst_polysat() {
 
+    polysat::test_quot_rem();
+    return;
+
     polysat::test_ineq_axiom1();
     polysat::test_ineq_axiom2();
     polysat::test_ineq_axiom3();