mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 00:48:45 +00:00
Code Activity

no need to keep an enode_pair, since the other is always the root

Browse source
This commit is contained in:
Jakob Rath 2023-08-08 17:13:05 +02:00
parent 99a078dd69
commit 3573305917
3 changed files with 8 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polysat/slicing.cpp
View file

@ -1363,7 +1363,7 @@ namespace polysat {
SASSERT(all_of(m_egraph.nodes(), [](enode* n) { return !n->is_marked1(); })); SASSERT(all_of(m_egraph.nodes(), [](enode* n) { return !n->is_marked1(); }));
} }
void slicing::collect_fixed(pvar v, fixed_bits_vector& out, euf::enode_pair_vector& out_just) { void slicing::collect_fixed(pvar v, fixed_bits_vector& out, euf::enode_vector& out_just) {
enode_vector& base = m_tmp2; enode_vector& base = m_tmp2;
SASSERT(base.empty()); SASSERT(base.empty());
get_base(var2slice(v), base); get_base(var2slice(v), base);
@ -1375,14 +1375,15 @@ namespace polysat {
unsigned const hi = lo + w - 1; unsigned const hi = lo + w - 1;
if (try_get_value(r, a)) { if (try_get_value(r, a)) {
out.push_back({hi, lo, a}); out.push_back({hi, lo, a});
out_just.push_back({n, r}); out_just.push_back(n);
} }
lo += w; lo += w;
} }
} }
void slicing::explain_fixed(euf::enode_pair const& just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) { void slicing::explain_fixed(euf::enode* const n, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {
auto [n, r] = just; enode* const r = n->get_root();
SASSERT(is_value(r));
NOT_IMPLEMENTED_YET(); // TODO: like explain_value NOT_IMPLEMENTED_YET(); // TODO: like explain_value
} }

4
src/math/polysat/slicing.h
View file

@ -339,8 +339,8 @@ namespace polysat {
void collect_simple_overlaps(pvar v, pvar_vector& out); void collect_simple_overlaps(pvar v, pvar_vector& out);
/** Collect fixed portions of the variable v */ /** Collect fixed portions of the variable v */
void collect_fixed(pvar v, fixed_bits_vector& out, euf::enode_pair_vector& out_just); void collect_fixed(pvar v, fixed_bits_vector& out, enode_vector& out_just);
void explain_fixed(euf::enode_pair const& just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var); void explain_fixed(euf::enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
std::ostream& display_tree(std::ostream& out) const; std::ostream& display_tree(std::ostream& out) const;

2
src/math/polysat/viable.cpp
View file

@ -976,7 +976,7 @@ namespace {
#if 0 #if 0
// TODO: wip // TODO: wip
fixed_bits_vector fbs; fixed_bits_vector fbs;
euf::enode_pair_vector fbs_just; euf::enode_vector fbs_just;
s.m_slicing.collect_fixed(v, fbs, fbs_just); s.m_slicing.collect_fixed(v, fbs, fbs_just);
for (unsigned idx = fbs.size(); idx-- > 0; ) { for (unsigned idx = fbs.size(); idx-- > 0; ) {