arithmetic

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

src/sat/smt/polysat/forbidden_intervals.cpp

@@ -22,7 +22,8 @@ Author:
 namespace polysat {
 
     std::ostream& operator<<(std::ostream& out, fi_record const& fi) {
-        out << "fi_record(bw = " << fi.bit_width << ", coeff = " << fi.coeff << ", " << fi.interval << ", " << fi.src << fi.side_cond << fi.deps << ")";
+        out << "fi_record(bw = " << fi.bit_width << ", coeff = " << fi.coeff << ", " << fi.interval << ", " 
+            << fi.src << (fi.src.empty()?"": " ") << fi.side_cond << (fi.side_cond.empty()?"":" ") << fi.deps << ")";
         return out;
     }
 

src/sat/smt/polysat/viable.cpp

@@ -643,9 +643,15 @@ namespace polysat {
             // Then value is chosen, min x . coeff * x >= t.
             // In other words:
             //
-            // coeff * (value - 1) <= t < coeff*value + 1
+            // x >= t div coeff
-            //
+            // => t <= coeff * x
-            auto vlo = c.value(mod((e.value - 1) * p2eb, p2b), bw);
+            
+            // (x - 1) * coeff < t <= x * coeff
+            
+            // a < x <= b <=>
+            // a + 1 <= x < b + 1
+
+            auto vlo = c.value(mod((e.value - 1) * p2eb + 1, p2b), bw);
             auto vhi = c.value(mod(e.value * p2eb + 1, p2b), bw);
 
 #if 0
@@ -655,6 +661,7 @@ namespace polysat {
             verbose_stream() << "before bw " << ebw << " " << bw << " " << *e.e << "\nafter  bw " << abw << " " << aw << " " << *after.e << "\n";
             if (!t.is_val())
                 IF_VERBOSE(0, verbose_stream() << "symbolic t : " << t << "\n");
+
 #endif
             auto sc = cs.ult(t - vlo, vhi - vlo);
             CTRACE("bv", sc.is_always_false(), c.display(tout));

src/sat/smt/polysat_internalize.cpp

@@ -531,12 +531,12 @@ namespace polysat {
 
         // Axioms for quotient/remainder
         // 
-        //      a = b*q + r
+        //      x = y*q + r
         //      multiplication does not overflow in b*q
-        //      addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
+        //      addition does not overflow in (y*q) + r; for now expressed as: r <= yq+r
-        //      b ≠ 0  ==>  r < b
+        //      y ≠ 0  ==>  r < y
-        //      b = 0  ==>  q = -1
+        //      y = 0  ==>  q = -1
-        // TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
+        // TODO: when x,y become evaluable, can we actually propagate q,r? doesn't seem like it.
         //       Maybe we need something like an op_constraint for better propagation.
 
         add_axiom("quot-rem", { eq_internalize(bv.mk_bv_add(bv.mk_bv_mul(y, quot), rem), x)}, false);
@@ -545,12 +545,11 @@ namespace polysat {
         //  { apply equivalence:  p <= q  <=>  q-p <= -p-1 }
         // b*q <= -r-1
         auto minus_one = bv.mk_numeral(rational::power_of_two(sz) - 1, sz);
-        auto one = bv.mk_numeral(1, sz);
         auto zero = bv.mk_numeral(0, sz);
         add_axiom("quot-rem", { mk_literal(bv.mk_ule(bv.mk_bv_mul(y, quot), bv.mk_bv_sub(minus_one, rem))) }, false);
         auto c_eq = eq_internalize(y, zero);
         add_axiom("quot-rem", { c_eq, ~mk_literal(bv.mk_ule(y, rem)) }, false);
-        add_axiom("quot-rem", { ~c_eq, eq_internalize(bv.mk_bv_add(quot, one), zero) }, false);
+        add_axiom("quot-rem", { ~c_eq, eq_internalize(quot, minus_one) }, false);
     }
 
     void solver::internalize_sign_extend(app* e) {

src/sat/smt/polysat_solver.cpp

@@ -459,18 +459,42 @@ namespace polysat {
     }
 
     expr_ref solver::pdd2expr(pdd const& p) {
-        if (p.is_val()) {
+
-            expr* n = bv.mk_numeral(p.val(), p.power_of_2());
+        auto mk_num = [&](rational const& c) {
-            return expr_ref(n, m);
+            return bv.mk_numeral(c, p.power_of_2());
+        };
+
+        auto mk_var = [&](pvar v) {
+            return var2expr(m_pddvar2var[v]);
+        };
+
+        if (p.is_val()) 
+            return expr_ref(mk_num(p.val()), m);
+        
+        expr_ref_vector args(m);
+        for (auto const& mon : p) {
+            auto c = mon.coeff;
+            if (mon.vars.empty())
+                args.push_back(mk_num(c));
+            else if (mon.coeff == 1 && mon.vars.size() == 1)
+                args.push_back(mk_var(mon.vars[0]));
+            else if (mon.vars.size() == 1)
+                args.push_back(bv.mk_bv_mul(mk_num(c), mk_var(mon.vars[0])));
+            else {
+                expr_ref_vector args2(m);
+                for (auto v : mon.vars)
+                    args2.push_back(mk_var(v));
+                if (c == 1)
+                    args.push_back(bv.mk_bv_mul(args2));
+                else
+                    args.push_back(bv.mk_bv_mul(mk_num(c), bv.mk_bv_mul(args2)));
+            }
         }          
-        auto v = var2enode(m_pddvar2var[p.var()]);
         expr_ref r(m);
-        r = v->get_expr();
+        if (args.size() == 1)
-        if (!p.hi().is_one())
+            r = args.get(0);
-            r = bv.mk_bv_mul(r, pdd2expr(p.hi()));
+        else
-        if (!p.lo().is_zero())
+            r = bv.mk_bv_add(args);
-            r = bv.mk_bv_add(r, pdd2expr(p.lo()));
-        ctx.get_rewriter()(r);
         return r;
     }