mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

separate egraph functionality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-22 16:17:53 -08:00
parent 8eea2488e2
commit 9a7e50c1e8
2 changed files with 56 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

135
src/sat/smt/polysat_egraph.cpp
View file

@ -35,114 +35,85 @@ namespace polysat {
j.pop_back();
}
};
// walk the egraph starting with pvar for overlaps.
void solver::get_bitvector_suffixes(pvar pv, justified_slices& out) {
void solver::get_subslices(pvar pv, subslice_infos& slices) {
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, {}});
slices.push_back({ n, 0, {} });
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())
for (unsigned i = 0; i < slices.size(); ++i) {
auto [n, offset, just] = slices[i];
if (n->get_root()->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();
n->get_root()->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 });
slices.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)) {
for (auto p : euf::enode_parents(n->get_root())) {
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 });
slices.push_back({ p, offset + lo, just });
}
}
}
for (auto const& [n,offset,d] : todo)
for (auto const& [n,offset,d] : slices)
n->get_root()->unmark1();
}
// walk the egraph starting with pvar for overlaps.
void solver::get_bitvector_suffixes(pvar pv, justified_slices& out) {
subslice_infos slices;
get_subslices(pv, slices);
for (auto& [n, offset, just] : slices) {
if (offset != 0)
continue;
auto w = n->get_th_var(get_id());
if (w == euf::null_theory_var)
continue;
auto const& p = m_var2pdd[w];
if (p.is_var())
out.push_back({ p.var(), dependency(just, s().scope_lvl())}); // approximate to current scope
}
}
// walk the e-graph to retrieve fixed overlaps
void solver::get_fixed_bits(pvar pv, justified_fixed_bits& out) {
subslice_infos slices;
get_subslices(pv, slices);
for (auto& [n, offset, just] : slices) {
if (offset != 0)
continue;
n = n->get_root();
if (!n->interpreted())
continue;
auto w = n->get_th_var(get_id());
if (w == euf::null_theory_var)
continue;
auto const& p = m_var2pdd[w];
if (!p.is_var())
continue;
unsigned lo = offset, hi = bv.get_bv_size(n->get_expr());
rational value;
VERIFY(bv.is_numeral(n->get_expr(), value));
out.push_back({ fixed_bits(lo, hi, value), dependency(just, s().scope_lvl()) }); // approximate level
}
}
}

3
src/sat/smt/polysat_solver.h
View file

@ -34,6 +34,7 @@ namespace polysat {
typedef sat::literal literal;
typedef sat::bool_var bool_var;
typedef sat::literal_vector literal_vector;
using subslice_infos = vector<std::tuple<euf::enode*, unsigned, eq_justification>>;
using pdd = dd::pdd;
struct stats {
@ -74,6 +75,8 @@ namespace polysat {
sat::check_result intblast();
void get_subslices(pvar v, subslice_infos& slices);
// internalize
bool visit(expr* e) override;
bool visited(expr* e) override;