separate egraph functionality

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

src/sat/smt/CMakeLists.txt

@@ -35,6 +35,7 @@ z3_add_component(sat_smt
     pb_internalize.cpp
     pb_pb.cpp
     pb_solver.cpp
+    polysat_egraph.cpp
     polysat_internalize.cpp
     polysat_model.cpp
     polysat_solver.cpp

src/sat/smt/polysat/core.cpp

@@ -389,11 +389,11 @@ namespace polysat {
         }                   
     }
 
-    void core::get_bitvector_suffixes(pvar v, pvar_vector& out) {
+    void core::get_bitvector_suffixes(pvar v, justified_slices& out) {
         s.get_bitvector_suffixes(v, out);
     }
 
-    void core::get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits) {
+    void core::get_fixed_bits(pvar v, justified_fixed_bits& fixed_bits) {
         s.get_fixed_bits(v, fixed_bits);
     }
 

src/sat/smt/polysat/core.h

@@ -83,8 +83,8 @@ namespace polysat {
         void propagate_unsat_core();
         void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
 
-        void get_bitvector_suffixes(pvar v, pvar_vector& out);
-        void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits);
+        void get_bitvector_suffixes(pvar v, justified_slices& out);
+        void get_fixed_bits(pvar v, justified_fixed_bits& fixed_bits);
         bool inconsistent() const;
 
         void add_watch(unsigned idx, unsigned var);

src/sat/smt/polysat/types.h

@@ -28,25 +28,31 @@ namespace polysat {
     };
 
     using pvar_vector = unsigned_vector;
+    using theory_var_pair = std::pair<theory_var, theory_var>;
+    using theory_var_pairs = svector<theory_var_pair>;
     inline const pvar null_var = UINT_MAX;
 
     class signed_constraint;
 
+
     class dependency {
         struct axiom_t {};
-        std::variant<axiom_t, sat::literal, std::pair<theory_var, theory_var>> m_data;
+        std::variant<axiom_t, sat::literal, theory_var_pair, theory_var_pairs> m_data;
         unsigned m_level;
         dependency(): m_data(axiom_t()), m_level(0) {}
     public:
         dependency(sat::literal lit, unsigned level) : m_data(lit), m_level(level) {}
         dependency(theory_var v1, theory_var v2, unsigned level) : m_data(std::make_pair(v1, v2)), m_level(level) {} 
+        dependency(theory_var_pairs& j, unsigned level) : m_data(j), m_level(level) {}
         static dependency axiom() { return dependency(); } 
         bool is_null() const { return is_literal() && *std::get_if<sat::literal>(&m_data) == sat::null_literal; }
         bool is_axiom() const { return std::holds_alternative<axiom_t>(m_data); }
-        bool is_eq() const { return std::holds_alternative<std::pair<theory_var, theory_var>>(m_data); }
+        bool is_eqs() const { return std::holds_alternative<theory_var_pairs>(m_data); }
+        bool is_eq() const { return std::holds_alternative<theory_var_pair>(m_data); }
         bool is_literal() const { return std::holds_alternative<sat::literal>(m_data); }
         sat::literal literal() const { SASSERT(is_literal()); return *std::get_if<sat::literal>(&m_data); }
-        std::pair<theory_var, theory_var> eq() const { SASSERT(!is_literal()); return *std::get_if<std::pair<theory_var, theory_var>>(&m_data); }
+        theory_var_pair eq() const { SASSERT(!is_literal()); return *std::get_if<theory_var_pair>(&m_data); }
+        theory_var_pairs const& eqs() const { SASSERT(!is_literal()); return *std::get_if<theory_var_pairs>(&m_data); }
         unsigned level() const { return m_level; }
         void set_level(unsigned level) { m_level = level; }
         dependency operator~() const { SASSERT(is_literal()); return dependency(~literal(), level()); }
@@ -61,8 +67,14 @@ namespace polysat {
             return out << "axiom@" << d.level();
         else if (d.is_literal())
             return out << d.literal() << "@" << d.level();
-        else
+        else if (d.is_eq())
             return out << "v" << d.eq().first << " == v" << d.eq().second << "@" << d.level();
+        else {
+            char const* sep = "";
+            for (auto [v1, v2] : d.eqs())
+                out << sep << "v" << d.eq().first << " == v" << d.eq().second, sep = ", ";
+            return out << " @" << d.level();
+        }
     }
 
 
@@ -78,7 +90,7 @@ namespace polysat {
         fixed_bits(unsigned hi, unsigned lo, rational value) : hi(hi), lo(lo), value(value) {}
     };
 
-    struct justified_fixed_bits : public fixed_bits, public dependency {};
+    using justified_fixed_bits = vector<std::pair<fixed_bits, dependency>>;
 
     using dependency_vector = vector<dependency>;
     using constraint_or_dependency = std::variant<signed_constraint, dependency>;
@@ -88,7 +100,8 @@ namespace polysat {
     using core_vector = std::initializer_list<constraint_or_dependency>;
     using constraint_id_vector = svector<constraint_id>;
     using constraint_id_list = std::initializer_list<constraint_id>;
-
+    using justified_slices = vector<std::pair<pvar, dependency>>;
+    using eq_justification = svector<std::pair<theory_var, theory_var>>;
 
     //
     // The interface that PolySAT uses to the SAT/SMT solver.
@@ -104,8 +117,8 @@ namespace polysat {
         virtual void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) = 0;
         virtual trail_stack& trail() = 0;
         virtual bool inconsistent() const = 0;
-        virtual void get_bitvector_suffixes(pvar v, pvar_vector& out) = 0;
-        virtual void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits) = 0;
+        virtual void get_bitvector_suffixes(pvar v, justified_slices& out) = 0;
+        virtual void get_fixed_bits(pvar v, justified_fixed_bits& fixed_bits) = 0;
     };
 
 }

src/sat/smt/polysat/viable.cpp

@@ -103,15 +103,15 @@ namespace polysat {
             return l_false;  // conflict already added
 #endif
 
-        pvar_vector overlaps;
+        justified_slices overlaps;
         c.get_bitvector_suffixes(v, overlaps);
-        std::sort(overlaps.begin(), overlaps.end(), [&](pvar x, pvar y) { return c.size(x) > c.size(y); });
+        std::sort(overlaps.begin(), overlaps.end(), [&](auto const& x, auto const& y) { return c.size(x.first) > c.size(y.first); });
 
         uint_set widths_set;
         // max size should always be present, regardless of whether we have intervals there (to make sure all fixed bits are considered)
         widths_set.insert(c.size(v));
 
-        for (pvar v : overlaps) 
+        for (auto const& [v, j] : overlaps) 
             for (layer const& l : m_units[v].get_layers()) 
                 widths_set.insert(l.bit_width);
                     
@@ -147,7 +147,7 @@ namespace polysat {
     lbool viable::find_on_layers(
         pvar const v,
         unsigned_vector const& widths,
-        pvar_vector const& overlaps,
+        justified_slices const& overlaps,
         fixed_bits_info const& fbi,
         rational const& to_cover_lo,
         rational const& to_cover_hi,
@@ -176,7 +176,7 @@ namespace polysat {
             // however, we probably should rotate to avoid getting stuck in refinement loop on a 'bad' constraint
             bool refined = false;
             for (unsigned i = overlaps.size(); i-- > 0; ) {
-                pvar x = overlaps[i];
+                pvar x = overlaps[i].first;
                 rational const& mod_value = c.var2pdd(x).two_to_N();
                 rational x_val = mod(val, mod_value);
                 if (!refine_viable(x, x_val)) {
@@ -201,7 +201,7 @@ namespace polysat {
         pvar const v,
         unsigned const w_idx,
         unsigned_vector const& widths,
-        pvar_vector const& overlaps,
+        justified_slices const& overlaps,
         fixed_bits_info const& fbi,
         rational const& to_cover_lo,
         rational const& to_cover_hi,
@@ -240,7 +240,7 @@ namespace polysat {
 
         // find relevant interval lists
         svector<entry_cursor> ecs;
-        for (pvar x : overlaps) {
+        for (auto const& [x, j] : overlaps) {
             if (c.size(x) < w)  // note that overlaps are sorted by variable size descending
                 break;
             if (entry* e = m_units[x].get_entries(w)) {
@@ -614,17 +614,17 @@ namespace polysat {
         out_fbi.reset(v_sz);
         auto& [fixed, just_src, just_side_cond, just_slice] = out_fbi;
 
-        svector<justified_fixed_bits> fbs;        
+        justified_fixed_bits fbs;        
         c.get_fixed_bits(v, fbs);
 
-        for (auto const& fb : fbs) {
+        for (auto const& [fb, d] : fbs) {
             LOG("slicing fixed bits: v" << v << "[" << fb.hi << ":" << fb.lo << "] = " << fb.value);
             for (unsigned i = fb.lo; i <= fb.hi; ++i) {
                 SASSERT(out_fbi.just_src[i].empty());  // since we don't get overlapping ranges from collect_fixed.
                 SASSERT(out_fbi.just_side_cond[i].empty());
                 SASSERT(out_fbi.just_slicing[i].empty());
                 out_fbi.fixed[i] = to_lbool(fb.value.get_bit(i - fb.lo));
-                out_fbi.just_slicing[i].push_back(fb);
+                out_fbi.just_slicing[i].push_back({ fb, d });
             }
         }
 

src/sat/smt/polysat/viable.h

@@ -107,7 +107,7 @@ namespace polysat {
             svector<lbool> fixed;
             vector<vector<signed_constraint>> just_src;
             vector<vector<signed_constraint>> just_side_cond;
-            vector<svector<justified_fixed_bits>> just_slicing;
+            vector<justified_fixed_bits> just_slicing;
 
             bool is_empty() const {
                 SASSERT_EQ(fixed.empty(), just_src.empty());
@@ -186,7 +186,7 @@ namespace polysat {
         lbool find_on_layers(
             pvar v,
             unsigned_vector const& widths,
-            pvar_vector const& overlaps,
+            justified_slices const& overlaps,
             fixed_bits_info const& fbi,
             rational const& to_cover_lo,
             rational const& to_cover_hi,
@@ -196,7 +196,7 @@ namespace polysat {
             pvar v,
             unsigned w_idx,
             unsigned_vector const& widths,
-            pvar_vector const& overlaps,
+            justified_slices const& overlaps,
             fixed_bits_info const& fbi,
             rational const& to_cover_lo,
             rational const& to_cover_hi,

src/sat/smt/polysat_egraph.cpp

@@ -0,0 +1,148 @@
+/*---
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    polysat_egraph.cpp
+
+Abstract:
+
+    PolySAT interface to bit-vector
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-01-26
+
+
+--*/
+
+#include "ast/euf/euf_bv_plugin.h"
+#include "sat/smt/polysat_solver.h"
+#include "sat/smt/euf_solver.h"
+
+namespace polysat {
+
+    struct solver::scoped_eq_justification {
+        eq_justification& j;
+        euf::enode* a, * b;
+        scoped_eq_justification(solver& s, eq_justification& j, euf::enode* a, euf::enode* b) :
+            j(j), a(a), b(b) {
+            if (a != b)
+                j.push_back({ s.get_th_var(a), s.get_th_var(b) });
+        }
+        ~scoped_eq_justification() {
+            if (a != b)
+                j.pop_back();
+        }
+    };
+
+    // walk the egraph starting with pvar for overlaps.
+    void solver::get_bitvector_suffixes(pvar pv, justified_slices& out) {
+        theory_var v = m_pddvar2var[pv];
+        svector<std::pair<euf::enode*, eq_justification>> todo;       
+        uint_set seen;
+        unsigned lo, hi;
+        expr* e = nullptr;
+        euf::enode* n = var2enode(v);
+        todo.push_back({ n, {}});
+
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            auto [n, just] = todo[i];
+            scoped_eq_justification sp(*this, just, n, n->get_root());
+            n = n->get_root();
+            if (n->is_marked1())
+                continue;
+            n->mark1();
+            for (auto sib : euf::enode_class(n)) {
+                theory_var w = sib->get_th_var(get_id());
+
+                // identify prefixes
+                if (bv.is_concat(sib->get_expr())) {
+                    scoped_eq_justification sp(*this, just, n, sib);
+                    todo.push_back({ sib->get_arg(sib->num_args() - 1), just });
+                }
+                if (w == euf::null_theory_var)
+                    continue;
+                if (seen.contains(w))
+                    continue;
+                seen.insert(w);
+                auto const& p = m_var2pdd[w];
+                if (p.is_var())
+                    out.push_back({ p.var(), dependency(just, s().scope_lvl())}); // approximate to current scope
+            }
+            for (auto p : euf::enode_parents(n)) {
+                if (p->is_marked1())
+                    continue;
+                // find prefixes: e[hi:0] a parent of n
+                if (bv.is_extract(p->get_expr(), lo, hi, e) && lo == 0) {
+                    auto child = expr2enode(e);
+                    SASSERT(n == child->get_root());
+                    scoped_eq_justification sp(*this, just, child, n);
+                    todo.push_back({ p, just });
+                }
+            }  
+        }
+        for (auto n : todo)
+            n.first->get_root()->unmark1();
+    }
+
+    // walk the e-graph to retrieve fixed overlaps
+    void solver::get_fixed_bits(pvar pv, justified_fixed_bits& out) {
+        theory_var v = m_pddvar2var[pv];
+        svector<std::tuple<euf::enode*, unsigned, eq_justification>> todo;
+        uint_set seen;
+        unsigned lo, hi;
+        expr* e = nullptr;
+        euf::enode* n = var2enode(v);
+        todo.push_back({ n, 0, {} });
+
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            auto [n, offset, just] = todo[i];
+            scoped_eq_justification sp(*this, just, n, n->get_root());
+            n = n->get_root();
+            if (n->is_marked1())
+                continue;
+            n->mark1();
+            for (auto sib : euf::enode_class(n)) {
+                if (bv.is_concat(sib->get_expr())) {
+                    unsigned delta = 0;
+                    scoped_eq_justification sp(*this, just, n, sib);
+                    for (unsigned j = sib->num_args(); j-- > 0; ) {
+                        auto arg = sib->get_arg(j);
+                        todo.push_back({ arg, offset + delta, just });
+                        delta += bv.get_bv_size(arg->get_expr());
+                    }
+                }if (!sib->interpreted())
+                    continue;
+                theory_var w = sib->get_th_var(get_id());
+                if (w == euf::null_theory_var)
+                    continue;
+                if (seen.contains(w))
+                    continue;
+                seen.insert(w);
+                
+                auto const& p = m_var2pdd[w];
+                if (p.is_var()) {
+                    unsigned lo = offset, hi = bv.get_bv_size(sib->get_expr());
+                    rational value;
+                    VERIFY(bv.is_numeral(sib->get_expr(), value));
+                    out.push_back({ fixed_bits(lo, hi, value), dependency(just, s().scope_lvl()) }); // approximate level
+                }
+                
+            }
+            for (auto p : euf::enode_parents(n)) {
+                if (p->is_marked1())
+                    continue;
+                if (bv.is_extract(p->get_expr(), lo, hi, e)) {
+                    auto child = expr2enode(e);
+                    SASSERT(n == child->get_root());
+                    scoped_eq_justification sp(*this, just, child, n);
+                    todo.push_back({ p, offset + lo, just });
+                }
+            }
+        }
+        for (auto const& [n,offset,d] : todo)
+            n->get_root()->unmark1();
+    }
+
+}

src/sat/smt/polysat_solver.cpp

@@ -269,6 +269,10 @@ namespace polysat {
                     auto [v1, v2] = d.eq();
                     lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2)));
                 }
+                else if (d.is_eqs()) {
+                    for (auto [v1, v2] : d.eqs())
+                        lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2)));
+                }
                 else {
                     SASSERT(d.is_axiom());
                 }
@@ -321,67 +325,4 @@ namespace polysat {
             r = bv.mk_bv_add(r, pdd2expr(p.lo()));
         return expr_ref(r, m);
     }
-
-    // walk the egraph starting with pvar for overlaps.
-    void solver::get_bitvector_suffixes(pvar pv, pvar_vector& out) {
-        theory_var v = m_pddvar2var[pv];
-        euf::enode_vector todo;
-        uint_set seen;
-        unsigned lo, hi;
-        expr* e = nullptr;
-        todo.push_back(var2enode(v));
-        for (unsigned i = 0; i < todo.size(); ++i) {
-            auto n = todo[i]->get_root();
-            if (n->is_marked1())
-                continue;
-            n->mark1();
-            for (auto sib : euf::enode_class(n)) {
-                theory_var w = sib->get_th_var(get_id());
-
-                // identify prefixes
-                if (bv.is_concat(sib->get_expr()))
-                    todo.push_back(sib->get_arg(sib->num_args() - 1));                
-                if (w == euf::null_theory_var)
-                    continue;
-                if (seen.contains(w))
-                    continue;
-                seen.insert(w);
-                auto const& p = m_var2pdd[w];
-                if (p.is_var())
-                    out.push_back(p.var());
-            }
-            for (auto p : euf::enode_parents(n)) {
-                if (p->is_marked1())
-                    continue;
-                // find prefixes: e[hi:0] a parent of n
-                if (bv.is_extract(p->get_expr(), lo, hi, e) && lo == 0) {
-                    SASSERT(n == expr2enode(e)->get_root());
-                    todo.push_back(p);
-                }
-            }  
-        }
-        for (auto n : todo)
-            n->get_root()->unmark1();
-    }
-
-    void solver::get_fixed_bits(pvar pv, svector<justified_fixed_bits>& fixed_bits) {
-        theory_var v = m_pddvar2var[pv];
-        auto n = var2enode(v);
-        auto r = n->get_root();
-        unsigned lo, hi;
-        expr* e = nullptr;
-        for (auto p : euf::enode_parents(r)) {
-            if (!p->interpreted())
-                continue;
-            for (auto sib : euf::enode_class(p)) {
-                if (bv.is_extract(sib->get_expr(), lo, hi, e) && r == expr2enode(e)->get_root()) {
-                    throw default_exception("get_fixed nyi");
-                    // TODO                    
-                    // dependency d = dependency(p->get_th_var(get_id()), n->get_th_var(get_id()), s().scope_lvl());
-                    // fixed_bits.push_back({ hi, lo, rational::zero(), null_dependency()});
-                }
-            }
-        }
-    }
-
 }

src/sat/smt/polysat_solver.h

@@ -166,8 +166,8 @@ namespace polysat {
         void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) override;
         trail_stack& trail() override;
         bool inconsistent() const override;
-        void get_bitvector_suffixes(pvar v, pvar_vector& out) override;
-        void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits) override;
+        void get_bitvector_suffixes(pvar v, justified_slices& out) override;
+        void get_fixed_bits(pvar v, justified_fixed_bits& fixed_bits) override;
 
         bool add_axiom(char const* name, core_vector const& clause, bool redundant) {
             return add_axiom(name, clause.begin(), clause.end(), redundant);
@@ -177,6 +177,8 @@ namespace polysat {
 
         expr_ref constraint2expr(signed_constraint const& sc);
         expr_ref pdd2expr(pdd const& p);
+
+        struct scoped_eq_justification;
 	       
     public:
         solver(euf::solver& ctx, theory_id id);