diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index 633e16239..42e7a330c 100644 --- a/src/math/polysat/slicing.cpp +++ b/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 const& args) { SASSERT(args.size() >= 2); ptr_vector 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 args; - for (enode* n : slices) - args.push_back(n->get_expr()); + for (unsigned i = 0; i < num_slices; ++i) + 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 - enode_vector x_base; - enode_vector y_base; - get_base(x, x_base); - get_base(y, y_base); + // invariant: parents merged => base slices merged + enode_vector const x_base = get_base(x); + enode_vector const y_base = get_base(y); 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()) diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h index 0ebfb29eb..fcb5d9e02 100644 --- a/src/math/polysat/slicing.h +++ b/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 const& args); enode* mk_concat_node(enode_vector const& slices); + enode* mk_concat_node(std::initializer_list 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)); }