Merge branch 'poly' of https://github.com/z3prover/z3 into poly

src/sat/smt/intblast_solver.cpp

@@ -235,12 +235,6 @@ namespace intblast {
             }
 
 #if 0
-            namespace fs = std::filesystem;
-            static unsigned num_check = 0;
-            fs::path filename = std::string("validation/int-") + std::to_string(++num_check) + ".smt2";
-            fs::create_directories(filename.parent_path());
-            IF_VERBOSE(1, verbose_stream() << "validation check written to file " << filename << "\n");
-            std::ofstream file(filename);
             std::string name_esc;
             if (name) {
                 name_esc = name;
@@ -251,6 +245,16 @@ namespace intblast {
             else
                 name_esc = "<none>";
 
+            namespace fs = std::filesystem;
+            static unsigned num_check = 0;
+            num_check += 1;
+
+            {
+                fs::path filename = std::string("validation/int-") + std::to_string(num_check) + ".smt2";
+                fs::create_directories(filename.parent_path());
+                IF_VERBOSE(1, verbose_stream() << "validation check written to file " << filename << "\n");
+                std::ofstream file(filename);
+
                 file << "(set-logic ALL)\n";
                 file << "(set-info :source |\n";
                 file << "    Name: " << name_esc << "\n";
@@ -262,8 +266,26 @@ namespace intblast {
                 m_solver->pop(1);
 
                 file.close();
+            }
 
-            // if (num_check == 68)
+            {
+                fs::path filename = std::string("validation/bv-") + std::to_string(num_check) + ".smt2";
+                std::ofstream file(filename);
+
+                file << "(set-logic ALL)\n";
+                file << "(set-info :source |\n";
+                file << "    Name: " << name_esc << "\n";
+                file << original_es << "\n|)\n";
+
+                m_solver->push();
+                m_solver->assert_expr(original_es);
+                m_solver->display(file) << "(check-sat)\n";
+                m_solver->pop(1);
+
+                file.close();
+            }
+
+            // if (num_check == 62)
             //     std::abort();
 
             r = l_false;
@@ -286,6 +308,7 @@ namespace intblast {
 
         IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
         if (r == l_true) {
+            verbose_stream() << "validation failed: " << name << "\n";
             IF_VERBOSE(0,
                 model_ref mdl;
                 m_solver->get_model(mdl);
@@ -501,7 +524,7 @@ namespace intblast {
 
     bool solver::is_bounded(expr* x, rational const& N) {
         return any_of(m_vars, [&](expr* v) {
-            return is_translated(v) && translated(v) == x && bv.get_bv_size(v) <= N;
+            return is_translated(v) && translated(v) == x && bv_size(v) <= N;
         });
     }
 
@@ -570,7 +593,7 @@ namespace intblast {
     * Perform simplifications that are claimed sound when the bit-vector interpretations of
     * mod/div always guard the mod and dividend to be non-zero.
     * Potentially shady area is for arithmetic expressions created by int2bv. 
-    * They will be guarded by a modulus which dose not disappear.
+    * They will be guarded by a modulus which does not disappear.
     */
     expr* solver::amod(expr* bv_expr, expr* x, rational const& N) {
         rational v;

src/sat/smt/polysat/constraints.h

@@ -56,7 +56,7 @@ namespace polysat {
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
 
 
-    class signed_constraint {
+    class signed_constraint final {
         bool m_sign = false;
         ckind_t m_op = ule_t;
         constraint* m_constraint = nullptr;
@@ -92,6 +92,8 @@ namespace polysat {
         op_constraint const& to_op() const { SASSERT(is_op()); return *reinterpret_cast<op_constraint*>(m_constraint); }
         bool is_eq(pvar& v, rational& val);
         std::ostream& display(std::ostream& out) const;
+        bool operator==(signed_constraint const& other) { return m_sign == other.m_sign && m_op == other.m_op && m_constraint == other.m_constraint; }
+        bool operator!=(signed_constraint const& other) { return !operator==(other); }
     };
 
     inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) { return c.display(out); }

src/sat/smt/polysat/monomials.cpp

@@ -324,27 +324,27 @@ namespace polysat {
         c.get_bitvector_suffixes(x, x_suffixes);        
         rational x_val, y_val;
         for (auto const& xslice : x_suffixes) {
-            if (c.size(xslice.v) == mon.num_bits())
+            if (c.size(xslice.child) == mon.num_bits())
                 continue;
-            auto const& xmax_value = c.var(xslice.v).manager().max_value();
+            auto const& xmax_value = c.var(xslice.child).manager().max_value();
             if (mon.val <= xmax_value)
                 continue;
-            if (!c.try_eval(c.var(xslice.v), x_val) || x_val != mon.arg_vals[0])
+            if (!c.try_eval(c.var(xslice.child), x_val) || x_val != mon.arg_vals[0])
                 continue;
             if (!y_computed)
                 c.get_bitvector_suffixes(y, y_suffixes);
             y_computed = true;
             for (auto const& yslice : y_suffixes) {
-                if (c.size(yslice.v) != c.size(xslice.v))
+                if (c.size(yslice.child) != c.size(xslice.child))
                     continue;
-                if (!c.try_eval(c.var(yslice.v), y_val) || y_val != mon.arg_vals[1])
+                if (!c.try_eval(c.var(yslice.child), y_val) || y_val != mon.arg_vals[1])
                     continue;
                 bool added = c.add_axiom("0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k",
                     { dependency({x, xslice}), dependency({y, yslice}),
                      ~C.ule(mon.args[0], xmax_value),
                      ~C.ule(mon.args[1], xmax_value),
                      ~C.ugt(mon.var, xmax_value), 
-                      C.umul_ovfl(c.var(xslice.v), c.var(yslice.v)) }, 
+                      C.umul_ovfl(c.var(xslice.child), c.var(yslice.child)) }, 
                     true);
                 if (added)
                     return true;

src/sat/smt/polysat/saturation.cpp

@@ -144,7 +144,7 @@ namespace polysat {
      * [y] z' <  y /\ yx <  zx  ==>  Ω*(x,y) \/ (z' + 1)x < zx   (TODO?)
      */
     void saturation::try_ugt_y(pvar v, inequality const& i) {
-        auto y = c.var(v);
+        pdd const y = c.var(v);
         pdd x = y;
         pdd z = y;
         if (!i.is_Xy_l_XZ(v, x, z))
@@ -216,10 +216,12 @@ namespace polysat {
     /**
      * Expand the following axioms:
      * Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}
+     * [ as approximation of Ovfl(x, y) & x <= y => y >= ceil(sqrt(2^N)) ]
      * Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 1
      * Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 1 => 0x * 0y >= 2^N
      *
      * ~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}
+     * [ as approximation of ~Ovfl(x, y) & x <= y => x < ceil(sqrt(2^N)) ]
      * ~Ovfl(x,y) & msb(x) >= k => msb(y) <= N - k + 1
      * ~Ovfl(x,y) & msb(x) >= k & msb(y) >= N - k + 1 => 0x * 0y < 2^N
      */
@@ -231,7 +233,7 @@ namespace polysat {
             return;
         if (!c.try_eval(y, vy))
             return;
-        auto N = x.manager().power_of_2();
+        unsigned N = x.manager().power_of_2();
         auto d = c.get_dependency(sc.id());
 
         auto bx = vx.get_num_bits();
@@ -258,7 +260,7 @@ namespace polysat {
             }            
             else if (bx + by > N + 1) 
                 add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k + 1", 
-                    {d, ~C.msb_ge(x, bx), C.msb_le(y, N - bx + 1)}, true);            
+                    { d, ~C.msb_ge(x, bx), C.msb_le(y, N - bx + 1) }, true);            
             else {
                 auto x1 = c.mk_zero_extend(1, x);
                 auto y1 = c.mk_zero_extend(1, y);                
@@ -271,9 +273,9 @@ namespace polysat {
             if (bx <= 1) {
                 add_clause("Ovfl(x, y) => x > 1", { d, C.ugt(x, 1) }, true);
             }
-            else if (bx < (N + 1) / 2) {
+            else if (by < N / 2) {
-                add_clause("Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}", 
+                add_clause("Ovfl(x, y) & x <= y => y >= 2^{N div 2}", 
-                    { d, ~C.ule(x, y), C.uge(x, rational::power_of_two((N + 1) / 2)) }, true);
+                    { d, ~C.ule(x, y), C.uge(y, rational::power_of_two(N / 2)) }, true);
             }
             else if (bx + by < N + 1) {
                 SASSERT(bx <= by);

src/sat/smt/polysat/types.h

@@ -36,34 +36,37 @@ namespace polysat {
     class signed_constraint;
 
     struct fixed_slice {
+        pvar child;
         unsigned offset = 0;
         unsigned length = 0;
         rational value;
         fixed_slice() = default;
-        fixed_slice(rational value, unsigned offset, unsigned length) : offset(offset), length(length), value(std::move(value)) {}
+        fixed_slice(pvar child, rational value, unsigned offset, unsigned length) : 
+            child(child), offset(offset), length(length), value(std::move(value)) {}
         unsigned end() const { return offset + length; }
     };
 
     struct fixed_claim : public fixed_slice {
-        pvar v;
+        pvar parent;
         fixed_claim() = default;
-        fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(std::move(value), offset, length), v(v) {}
+        fixed_claim(pvar v, rational value, unsigned offset, unsigned length) : fixed_slice(child, std::move(value), offset, length), parent(v) {}
-        fixed_claim(pvar v, fixed_slice const& s) : fixed_slice(s), v(v) {}
+        fixed_claim(pvar v, fixed_slice const& s) : fixed_slice(s), parent(v) {}
     };
 
     struct offset_slice {
-        pvar v;
+        pvar child;
         unsigned offset;
         offset_slice() = default;
-        offset_slice(pvar v, unsigned offset) : v(v), offset(offset) {}
+        offset_slice(pvar v, unsigned offset) : child(v), offset(offset) {}
     };
 
     struct offset_claim : public offset_slice {
-        pvar w;
+        pvar parent;
         offset_claim() = default;
-        offset_claim(pvar w, offset_slice const& s) : offset_slice(s), w(w) {}
+        offset_claim(pvar w, offset_slice const& s) : offset_slice(s), parent(w) {}
     };
 
+
     class dependency {
         struct axiom_t {};
         std::variant<axiom_t, sat::bool_var, theory_var_pair, offset_claim, fixed_claim> m_data;
@@ -99,11 +102,11 @@ namespace polysat {
             return out << "tv" << d.eq().first << " == tv" << d.eq().second;
         else if (d.is_offset_claim()) {
             auto offs = d.offset();
-            return out << "v" << offs.v << " == v" << offs.w << " offset " << offs.offset;
+            return out << "v" << offs.child << " == v" << offs.parent << " offset " << offs.offset;
         }
         else if (d.is_fixed_claim()) {
             auto fixed = d.fixed();
-            return out << fixed.value << " == v" << fixed.v << " [" << fixed.length << "]@" << fixed.offset;
+            return out << fixed.value << " == v" << fixed.parent << " [" << fixed.length << "]@" << fixed.offset;
         }
         else {
             UNREACHABLE();
@@ -115,8 +118,8 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, offset_slice const& js) {
         if (js.offset == 0)
-            return out << "v" << js.v;
+            return out << "v" << js.child;
-        return out << "v" << js.v << " at offset " << js.offset;
+        return out << "v" << js.child << " at offset " << js.offset;
     }
 
     using fixed_bits_vector = vector<fixed_slice>;
@@ -125,8 +128,8 @@ namespace polysat {
         unsigned level = 0;  // level when sub-slice was fixed to value
         dependency dep = null_dependency;
         fixed_slice_extra() = default;
-        fixed_slice_extra(rational value, unsigned offset, unsigned length, unsigned level, dependency dep):
+        fixed_slice_extra(rational value, unsigned offset, unsigned length, unsigned level, dependency dep) :
-            fixed_slice(std::move(value), offset, length), level(level), dep(std::move(dep)) {}
+            fixed_slice(child, std::move(value), offset, length), level(level), dep(std::move(dep)) {}
     };
     using fixed_slice_extra_vector = vector<fixed_slice_extra>;
 
@@ -137,6 +140,7 @@ namespace polysat {
     };
     using offset_slice_extra_vector = vector<offset_slice_extra>;
 
+
     using dependency_vector = vector<dependency>;
     using constraint_or_dependency = std::variant<signed_constraint, dependency>;
     using constraint_id_or_constraint = std::variant<constraint_id, signed_constraint>;

src/sat/smt/polysat/ule_constraint.cpp

@@ -227,6 +227,32 @@ namespace polysat {
             lhs *= x;
             SASSERT(lhs.leading_coefficient().is_power_of_two());
         }
+
+        // shared parity of LHS/RHS __without__ the constant terms
+        unsigned const lhs_parity = (lhs - lhs.offset()).min_parity();
+        unsigned const rhs_parity = (rhs - rhs.offset()).min_parity();
+        unsigned const parity = std::min(lhs_parity, rhs_parity);
+        SASSERT(parity < N);  // since at least one side is a non-constant
+
+        if (parity > lhs.offset().parity(N) || parity > rhs.offset().parity(N)) {
+            verbose_stream() << "lhs = " << lhs << "   rhs = " << rhs << "   parity = " << parity << "\n";
+            // 2^k p + a <= 2^k q + b   with 0 <= a < 2^k and 0 <= b < 2^k
+            //      --> 2^k p <= 2^k q  if a <= b
+            //      --> 2^k p <  2^k q  if a >  b
+            rational a = mod2k(lhs.offset(), parity);
+            rational b = mod2k(rhs.offset(), parity);
+            SASSERT(!a.is_zero() || !b.is_zero());
+            lhs = lhs - a;
+            rhs = rhs - b;
+            if (a > b) {
+                swap(lhs, rhs);
+                is_positive = !is_positive;
+            }
+            // one more round to detect trivial constraints
+            return simplify_impl(is_positive, lhs, rhs);
+            verbose_stream() << "lhs' = " << lhs << "   rhs' = " << rhs << "\n";
+        }
+
     } // simplify_impl
 }
 
@@ -256,6 +282,7 @@ namespace polysat {
         pdd const old_lhs = lhs;
         pdd const old_rhs = rhs;
 #endif
+        // verbose_stream() << "simplify: sign " << !is_positive << " lhs " << lhs << " rhs " << rhs << "\n";
         simplify_impl(is_positive, lhs, rhs);
 #ifndef NDEBUG
         if (old_is_positive != is_positive || old_lhs != lhs || old_rhs != rhs) {
@@ -274,6 +301,14 @@ namespace polysat {
                 SASSERT(rhs.is_zero());
             }
         }
+        CTRACE("bv_verbose", !is_simplified(lhs, rhs), {
+            tout << "Result of simplify_impl is not fully simplified:\n    " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
+            bool pos2 = is_positive;
+            pdd lhs2 = lhs;
+            pdd rhs2 = rhs;
+            simplify_impl(pos2, lhs2, rhs2);
+            tout << "It should be:\n    " << ule_pp(to_lbool(pos2), lhs2, rhs2) << "\n";
+        });
         SASSERT(is_simplified(lhs, rhs));  // rewriting should be idempotent
 #endif
     }
@@ -352,6 +387,7 @@ namespace polysat {
     }
 
     void ule_constraint::activate(core& c, bool sign, dependency const& d) {
+        /*
         auto p = c.subst(lhs());
         auto q = c.subst(rhs());
         auto& C = c.cs();
@@ -359,6 +395,7 @@ namespace polysat {
             c.add_axiom("lhs > rhs  ==>  -1 > rhs", { d, C.ult(rhs(), -1) }, false);
             c.add_axiom("lhs > rhs  ==>  lhs > 0", { d, C.ult(0, lhs()) }, false);
         }
+        */
     }
 
 

src/sat/smt/polysat/viable.cpp

@@ -154,7 +154,7 @@ namespace polysat {
     void viable::init_overlaps(pvar v) {
         m_overlaps.reset();
         c.get_bitvector_suffixes(v, m_overlaps);
-        std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.v) < c.size(y.v); });
+        std::sort(m_overlaps.begin(), m_overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.child) < c.size(y.child); });
     }
 
 
@@ -566,7 +566,7 @@ namespace polysat {
         auto last = m_explain.back();
         auto after = last;
 
-        verbose_stream() << m_explain_kind << "\n";
+        verbose_stream() << "viable::explain: " << m_explain_kind << " v" << m_var << "\n";
 
         if (c.inconsistent())
             verbose_stream() << "inconsistent explain\n";
@@ -594,8 +594,12 @@ namespace polysat {
                 result.push_back(d);
             }
             result.append(e->deps);
-            if (!index.is_null())
+            if (!index.is_null()) {
+                VERIFY_EQ(e->src.size(), 1);
+                VERIFY_EQ(c.get_constraint(index), e->src[0]);
                 result.push_back(c.get_dependency(index));
+                // result.append(c.explain_weak_eval(c.get_constraint(index)));
+            }
         };
 
         if (last.e->interval.is_full()) {
@@ -637,6 +641,13 @@ namespace polysat {
                 result.clear();
                 result.push_back(exp);
             }
+            else {
+                // could not propagate to subslice
+                // conflict depends on evaluation
+                auto index = last.e->constraint_index;
+                if (!index.is_null())
+                    result.append(c.explain_weak_eval(c.get_constraint(index)));
+            }
         }
         unmark();
         if (c.inconsistent())
@@ -672,7 +683,7 @@ namespace polysat {
         //     e.g., prefers constant 'c' if we have pvars for both 'c' and 'concat(c,...)'
         std::sort(subslices.begin(), subslices.end(), [&](auto const& a, auto const& b) -> bool {
             return a.level > b.level
-                || (a.level == b.level && c.size(a.v) < c.size(b.v));
+                || (a.level == b.level && c.size(a.child) < c.size(b.child));
         });
 
         for (auto const& slice : subslices)
@@ -682,7 +693,7 @@ namespace polysat {
     }
 
     dependency viable::propagate_from_containing_slice(entry* e, rational const& value, dependency_vector const& e_deps, fixed_slice_extra_vector const& fixed, offset_slice_extra const& slice) {
-        pvar w = slice.v;
+        pvar w = slice.child;
         unsigned offset = slice.offset;
         unsigned w_level = slice.level;  // level where value of w was fixed
         if (w == m_var)
@@ -816,7 +827,7 @@ namespace polysat {
             unsigned remaining_z_off = z_sz - remaining_z_sz;
             // find next fixed slice (prefer lower level)
             fixed_slice_extra best;
-            unsigned best_off = UINT_MAX;
+            unsigned best_off = z_sz;
             for (auto const& f : fixed) {
                 if (f.level >= w_level)
                     continue;
@@ -881,8 +892,9 @@ namespace polysat {
         });
 
         if (ivl.is_full()) {
-            // TODO: set conflict
+            pdd zero = c.var2pdd(m_var).zero();
-            NOT_IMPLEMENTED_YET();
+            auto sc = cs.ult(zero, zero);  // false
+            return c.propagate(sc, deps, "propagate from containing slice (conflict)");
         }
         else {
             // proper interval
@@ -1086,6 +1098,7 @@ namespace polysat {
 
     /*
      * Register constraint at index 'idx' as unitary in v.
+     * Returns 'multiple' when either intervals are unchanged or there really are multiple values left.
      */
     find_t viable::add_unitary(pvar v, constraint_id idx, rational& var_value) {
 
@@ -1459,7 +1472,7 @@ namespace polysat {
             e = e->next();
             ++count;
             if (count > 10) {
-                out << " ...";
+                out << " ... (total: " << count << " entries)";
                 break;
             }
         } 
@@ -1472,9 +1485,7 @@ namespace polysat {
             for (auto const& layer : m_units[v].get_layers()) {
                 if (!layer.entries)
                     continue;
-                out << "v" << v << ": ";
+                out << "v" << v << "[" << layer.bit_width << "]: ";
-                if (layer.bit_width != c.size(v))
-                    out << "width[" << layer.bit_width << "] ";
                 display_all(out, layer.entries, " ");
                 out << "\n";
             }
@@ -1483,11 +1494,11 @@ namespace polysat {
     }
 
     std::ostream& viable::display_state(std::ostream& out) const {
-        out << "v" << m_var << ": ";
+        out << "v" << m_var << ":";
         for (auto const& slice : m_overlaps) {
-            out << "v" << slice.v << ":" << c.size(slice.v) << "@" << slice.offset << " ";
+            out << "  v" << slice.child << ":" << c.size(slice.child) << "@" << slice.offset;
-            if (c.is_assigned(slice.v))
+            if (c.is_assigned(slice.child))
-                out << "value(" << c.get_assignment().value(slice.v) << ") ";
+                out << " value=" << c.get_assignment().value(slice.child);
         }
         out << "\n";
         return out;
@@ -1496,7 +1507,7 @@ namespace polysat {
     std::ostream& viable::display_explain(std::ostream& out) const {
         display_state(out);
         for (auto const& e : m_explain)
-            display_one(out << "v" << m_var << "[" << e.e->bit_width << "] : = " << e.value << " ", e.e) << "\n";
+            display_one(out << "v" << m_var << "[" << e.e->bit_width << "] := " << e.value << " ", e.e) << "\n";
         return out;
     }
 

src/sat/smt/polysat_egraph.cpp

@@ -115,7 +115,7 @@ namespace polysat {
             unsigned length = bv.get_bv_size(r->get_expr());
             rational value;
             VERIFY(bv.is_numeral(r->get_expr(), value));
-            out.push_back({ fixed_slice(value, offset, length) });
+            out.push_back({ fixed_slice(null_var, value, offset, length) });
             return false;
         };
    
@@ -186,6 +186,10 @@ namespace polysat {
         m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq);
     }
 
+    //
+    // explain that pv contains a fixed sub-slice at offset/length
+    // in addition, if slice.child is not null_var, then explain that
+    //
     void solver::explain_fixed(pvar pv, fixed_slice const& slice, std::function<void(euf::enode*, euf::enode*)> const& consume_eq) {
         euf::theory_var v = m_pddvar2var[pv];
         expr_ref val(bv.mk_numeral(slice.value, slice.length), m);
@@ -197,6 +201,11 @@ namespace polysat {
 
         SASSERT(b);
         m_bv_plugin->explain_slice(var2enode(v), slice.offset, b, consume_eq);
+
+        if (slice.child != null_var) {
+            auto c = var2enode(m_pddvar2var[slice.child]);
+            m_bv_plugin->explain_slice(b, 0, c, consume_eq);
+        }
     }
 
 }

src/sat/smt/polysat_internalize.cpp

@@ -1,4 +1,4 @@
-/*++
+/*++
 Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
@@ -741,7 +741,7 @@ namespace polysat {
         auto gelo = mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(lo), sz_x), x));
         auto name = "extract";
         add_axiom(name, { eq0, gelo });
-        if (hi + 1 == sz_e)
+        if (hi + 1 == sz_x)
             add_axiom(name, { ~eq0, ~gelo });
     }
 

src/sat/smt/polysat_solver.cpp

@@ -148,11 +148,11 @@ namespace polysat {
         }
         else if (d.is_fixed_claim()) {
             auto const& o = d.fixed();
-            explain_fixed(o.v, o, consume);
+            explain_fixed(o.parent, o, consume);
         }
         else if (d.is_offset_claim()) {
             auto const& offs = d.offset();
-            explain_slice(offs.v, offs.w, offs.offset, consume);
+            explain_slice(offs.child, offs.parent, offs.offset, consume);
         }
         else {
             auto const [v1, v2] = d.eq();