helpers

src/math/polysat/slicing.cpp

@@ -158,6 +158,16 @@ namespace polysat {
         return m_bv->get_bv_size(s->get_expr());
     }
 
+    slicing::enode* slicing::sibling(enode* s) const {
+        enode* p = parent(s);
+        SASSERT(p);
+        SASSERT(sub_lo(p) == s || sub_hi(p) == s);
+        if (s != sub_hi(p))
+            return sub_hi(p);
+        else
+            return sub_lo(p);
+    }
+
     func_decl* slicing::mk_concat_decl(ptr_vector<expr> const& args) {
         SASSERT(args.size() >= 2);
         ptr_vector<sort> domain;
@@ -303,7 +313,7 @@ namespace polysat {
         i.reset();
         i.var = var;
         enode* n = m_egraph.mk(e, 0, num_args, args);  // NOTE: the egraph keeps a strong reference to 'e'
-        LOG("alloc_enode: " << e_pp(n));
+        // LOG("alloc_enode: " << e_pp(n));
         return n;
     }
 
@@ -323,11 +333,15 @@ namespace polysat {
     }
 
     slicing::enode* slicing::mk_concat_node(enode_vector const& slices) {
+        return mk_concat_node(slices.size(), slices.data());
+    }
+
+    slicing::enode* slicing::mk_concat_node(unsigned num_slices, enode* const* slices) {
         ptr_vector<expr> args;
-        for (enode* n : slices)
+        for (unsigned i = 0; i < num_slices; ++i)
-            args.push_back(n->get_expr());
+            args.push_back(slices[i]->get_expr());
         app_ref a(m_ast.mk_app(mk_concat_decl(args), args), m_ast);
-        return find_or_alloc_enode(a, slices.size(), slices.data(), null_var);
+        return find_or_alloc_enode(a, num_slices, slices, null_var);
     }
 
     void slicing::add_concat_node(enode* s, enode* concat) {
@@ -868,7 +882,7 @@ namespace polysat {
     }
 
     void slicing::egraph_on_merge(enode* root, enode* other) {
-        // LOG("on_merge:\nroot " << e_pp(root) << "other " << e_pp(other));
+        LOG("on_merge: root " << slice_pp(*this, root) << "other " << slice_pp(*this, other));
         if (root->interpreted())
             return;
         SASSERT(!other->interpreted());  // by convention, interpreted nodes are always chosen as root
@@ -972,7 +986,6 @@ namespace polysat {
     }
 
     bool slicing::merge_base(enode* s1, enode* s2, dep_t dep) {
-        LOG("merge_base: " << slice_pp(*this, s1) << " and " << slice_pp(*this, s2));
         SASSERT(!has_sub(s1));
         SASSERT(!has_sub(s2));
         return egraph_merge(s1, s2, dep);
@@ -989,11 +1002,9 @@ namespace polysat {
                 continue;
             if (x->get_root() == y->get_root()) {
                 DEBUG_CODE({
-                    // parents merged => base slices merged
+                    // invariant: parents merged => base slices merged
-                    enode_vector x_base;
+                    enode_vector const x_base = get_base(x);
-                    enode_vector y_base;
+                    enode_vector const y_base = get_base(y);
-                    get_base(x, x_base);
-                    get_base(y, y_base);
                     SASSERT_EQ(x_base.size(), y_base.size());
                     for (unsigned i = x_base.size(); i-- > 0; ) {
                         SASSERT_EQ(x_base[i]->get_root(), y_base[i]->get_root());
@@ -1100,6 +1111,12 @@ namespace polysat {
         SASSERT(todo.empty());
     }
 
+    slicing::enode_vector slicing::get_base(enode* src) const {
+        enode_vector out;
+        get_base(src, out);
+        return out;
+    }
+
     pvar slicing::mk_extract(enode* src, unsigned hi, unsigned lo, pvar replay_var) {
         LOG("mk_extract: src=" << slice_pp(*this, src) << " hi=" << hi << " lo=" << lo);
         enode_vector& slices = m_tmp3;
@@ -1522,6 +1539,8 @@ namespace polysat {
         out << "{id:" << s->get_id();
         out << ",w:" << width(s);
         out << ",root:" << s->get_root_id();
+        if (slice2var(s) != null_var)
+            out << ",var:v" << slice2var(s);
         if (is_value(s))
             out << ",value:" << get_value(s);
         if (s->interpreted())

src/math/polysat/slicing.h

@@ -41,8 +41,9 @@ namespace polysat {
 
     public:
         using enode = euf::enode;
-        using enode_pair = euf::enode_pair;
         using enode_vector = euf::enode_vector;
+        using enode_pair = euf::enode_pair;
+        using enode_pair_vector = euf::enode_pair_vector;
 
     private:
         class dep_t {
@@ -130,6 +131,8 @@ namespace polysat {
 
         func_decl* mk_concat_decl(ptr_vector<expr> const& args);
         enode* mk_concat_node(enode_vector const& slices);
+        enode* mk_concat_node(std::initializer_list<enode*> slices) { return mk_concat_node(slices.size(), slices.begin()); }
+        enode* mk_concat_node(unsigned num_slices, enode* const* slices);
         // Add s = concat(s1, ..., sn)
         void add_concat_node(enode* s, enode* concat);
 
@@ -154,6 +157,8 @@ namespace polysat {
         enode* get_value_node(enode* s) const { return info(s->get_root()).value_node; }
         void set_value_node(enode* s, enode* value_node);
 
+        unsigned get_cut(enode* s) const { return info(s).cut; }
+
         bool has_sub(enode* s) const { return info(s).has_sub(); }
 
         /// Upper subslice (direct child, not necessarily the representative)
@@ -162,6 +167,9 @@ namespace polysat {
         /// Lower subslice (direct child, not necessarily the representative)
         enode* sub_lo(enode* s) const { return info(s).sub_lo; }
 
+        /// sub_lo(parent(s)) or sub_hi(parent(s)), whichever is different from s.
+        enode* sibling(enode* s) const;
+
         // Retrieve (or create) a slice representing the given value.
         enode* mk_value_slice(rational const& val, unsigned bit_width);
 
@@ -177,6 +185,7 @@ namespace polysat {
 
         /// Retrieve base slices s_1,...,s_n such that src == s_1 ++ ... ++ s_n (actual descendant subslices)
         void get_base(enode* src, enode_vector& out_base) const;
+        enode_vector get_base(enode* src) const;
 
         /// Retrieve (or create) base slices s_1,...,s_n such that src[hi:lo] == s_1 ++ ... ++ s_n.
         /// If output_full_src is true, return the new base for src, i.e., src == s_1 ++ ... ++ s_n.
@@ -333,7 +342,6 @@ namespace polysat {
         bool is_extract(pvar x, pvar src, unsigned& out_hi, unsigned& out_lo);
 
         // Track value assignments to variables (and propagate to subslices)
-        // (could generalize to fixed bits, then we need a way to merge interpreted enodes)
         void add_value(pvar v, rational const& value);
         void add_value(pvar v, unsigned value) { add_value(v, rational(value)); }
         void add_value(pvar v, int value) { add_value(v, rational(value)); }