mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

wip: term_graph::project and term_graph::solve

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-11 17:38:14 -07:00
parent 144d8df5d5
commit e0aaf4452b
1 changed files with 60 additions and 60 deletions
Download patch file Download diff file Expand all files Collapse all files

120
src/qe/qe_term_graph.cpp
View file

@ -65,9 +65,9 @@ namespace qe {
m_children.push_back(t); m_children.push_back(t);
} }
} }
~term() {} ~term() {}
class parents { class parents {
term const& t; term const& t;
public: public:
@ -168,9 +168,9 @@ namespace qe {
arith_term_graph_plugin(term_graph &g) : arith_term_graph_plugin(term_graph &g) :
term_graph_plugin (g.get_ast_manager().mk_family_id("arith")), term_graph_plugin (g.get_ast_manager().mk_family_id("arith")),
m_g(g), m(g.get_ast_manager()), m_arith(m) {(void)m_g;} m_g(g), m(g.get_ast_manager()), m_arith(m) {(void)m_g;}
virtual ~arith_term_graph_plugin() {} virtual ~arith_term_graph_plugin() {}
bool mk_eq_core (expr *_e1, expr *_e2, expr_ref &res) { bool mk_eq_core (expr *_e1, expr *_e2, expr_ref &res) {
expr *e1, *e2; expr *e1, *e2;
e1 = _e1; e1 = _e1;
@ -385,7 +385,7 @@ namespace qe {
SASSERT(res); SASSERT(res);
return res; return res;
} }
void term_graph::internalize_eq(expr *a1, expr* a2) { void term_graph::internalize_eq(expr *a1, expr* a2) {
SASSERT(m_merge.empty()); SASSERT(m_merge.empty());
merge(*internalize_term(a1), *internalize_term(a2)); merge(*internalize_term(a1), *internalize_term(a2));
@ -415,17 +415,17 @@ namespace qe {
void term_graph::merge(term &t1, term &t2) { void term_graph::merge(term &t1, term &t2) {
// -- merge might invalidate term2app cache // -- merge might invalidate term2app cache
m_term2app.reset(); m_term2app.reset();
m_pinned.reset(); m_pinned.reset();
term *a = &t1.get_root(); term *a = &t1.get_root();
term *b = &t2.get_root(); term *b = &t2.get_root();
if (a == b) return; if (a == b) return;
if (a->get_class_size() > b->get_class_size()) { if (a->get_class_size() > b->get_class_size()) {
std::swap(a, b); std::swap(a, b);
} }
// Remove parents of it from the cg table. // Remove parents of it from the cg table.
for (term* p : term::parents(b)) { for (term* p : term::parents(b)) {
if (!p->is_marked()) { if (!p->is_marked()) {
@ -626,21 +626,21 @@ namespace qe {
expr_ref_vector m_pinned; // tracks expr in the maps expr_ref_vector m_pinned; // tracks expr in the maps
expr* mk_pure(term& t) { expr* mk_pure(term& t) {
expr* e = nullptr; expr* e = nullptr;
if (m_term2app.find(t.get_id(), e)) return e; if (m_term2app.find(t.get_id(), e)) return e;
e = t.get_expr(); e = t.get_expr();
if (!is_app(e)) return nullptr; if (!is_app(e)) return nullptr;
app* a = ::to_app(e); app* a = ::to_app(e);
expr_ref_buffer kids(m); expr_ref_buffer kids(m);
for (term* ch : term::children(t)) { for (term* ch : term::children(t)) {
if (!m_root2rep.find(ch->get_root().get_id(), e)) return nullptr; if (!m_root2rep.find(ch->get_root().get_id(), e)) return nullptr;
kids.push_back(e); kids.push_back(e);
} }
expr* pure = m.mk_app(a->get_decl(), kids.size(), kids.c_ptr()); expr* pure = m.mk_app(a->get_decl(), kids.size(), kids.c_ptr());
m_pinned.push_back(pure); m_pinned.push_back(pure);
m_term2app.insert(t.get_id(), pure); m_term2app.insert(t.get_id(), pure);
return pure; return pure;
} }
bool is_better_rep(expr *t1, expr *t2) { bool is_better_rep(expr *t1, expr *t2) {
if (!t2) return t1; if (!t2) return t1;
@ -648,34 +648,34 @@ namespace qe {
} }
void purify() { void purify() {
// - propagate representatives up over parents. // - propagate representatives up over parents.
// use work-list + marking to propagate. // use work-list + marking to propagate.
// - produce equalities over represented classes. // - produce equalities over represented classes.
// - produce other literals over represented classes // - produce other literals over represented classes
// (walk disequalities in m_lits and represent // (walk disequalities in m_lits and represent
// lhs/rhs over decls or excluding decls) // lhs/rhs over decls or excluding decls)
ptr_vector<term> worklist; ptr_vector<term> worklist;
for (term * t : m_tg.m_terms) { for (term * t : m_tg.m_terms) {
worklist.push_back(t); worklist.push_back(t);
t->set_mark(true); t->set_mark(true);
} }
while (!worklist.empty()) { while (!worklist.empty()) {
term* t = worklist.back(); term* t = worklist.back();
worklist.pop_back(); worklist.pop_back();
t->set_mark(false); t->set_mark(false);
if (m_term2app.contains(t->get_id())) if (m_term2app.contains(t->get_id()))
continue; continue;
if (!t->is_theory() && is_projected(*t)) if (!t->is_theory() && is_projected(*t))
continue; continue;
expr* pure = mk_pure(*t); expr* pure = mk_pure(*t);
if (!pure) continue; if (!pure) continue;
m_term2app.insert(t->get_id(), pure); m_term2app.insert(t->get_id(), pure);
expr* rep = nullptr; expr* rep = nullptr;
// ensure that the root has a representative // ensure that the root has a representative
m_root2rep.find(t->get_root().get_id(), rep); m_root2rep.find(t->get_root().get_id(), rep);
// update rep with pure if it is better // update rep with pure if it is better
@ -686,9 +686,9 @@ namespace qe {
if (!p->is_marked()) { if (!p->is_marked()) {
p->set_mark(true); p->set_mark(true);
worklist.push_back(p); worklist.push_back(p);
} }
} }
} }
} }
// Here we could also walk equivalence classes that // Here we could also walk equivalence classes that
@ -698,7 +698,7 @@ namespace qe {
// and can be mined using other means, such as theory // and can be mined using other means, such as theory
// aware core minimization // aware core minimization
m_tg.reset_marks(); m_tg.reset_marks();
} }
void solve() { void solve() {
ptr_vector<term> worklist; ptr_vector<term> worklist;
@ -707,7 +707,7 @@ namespace qe {
if (m_term2app.contains(t->get_id())) continue; if (m_term2app.contains(t->get_id())) continue;
worklist.push_back(t); worklist.push_back(t);
t->set_mark(true); t->set_mark(true);
} }
while (!worklist.empty()) { while (!worklist.empty()) {
term* t = worklist.back(); term* t = worklist.back();
@ -728,13 +728,13 @@ namespace qe {
m_root2rep.insert(t->get_root().get_id(), pure); m_root2rep.insert(t->get_root().get_id(), pure);
for (term * p : term::parents(t->get_root())) { for (term * p : term::parents(t->get_root())) {
SASSERT(!m_term2app.contains(p->get_id())); SASSERT(!m_term2app.contains(p->get_id()));
if (!p->is_marked()) { if (!p->is_marked()) {
p->set_mark(true); p->set_mark(true);
worklist.push_back(p); worklist.push_back(p);
}
}
} }
} }
}
}
m_tg.reset_marks(); m_tg.reset_marks();
} }
@ -744,7 +744,7 @@ namespace qe {
bool find_app(expr *lit, expr *&res) { bool find_app(expr *lit, expr *&res) {
return m_root2rep.find(m_tg.get_term(lit)->get_root().get_id(), res); return m_root2rep.find(m_tg.get_term(lit)->get_root().get_id(), res);
} }
void mk_lits(expr_ref_vector &res) { void mk_lits(expr_ref_vector &res) {
expr *e = nullptr; expr *e = nullptr;
@ -800,16 +800,16 @@ namespace qe {
} }
bool is_solved_eq(expr *_lhs, expr* _rhs) { bool is_solved_eq(expr *_lhs, expr* _rhs) {
if (!is_app(_lhs) || !is_app(_rhs)) return false; if (!is_app(_lhs) || !is_app(_rhs)) return false;
app *lhs, *rhs; app *lhs, *rhs;
lhs = ::to_app(_lhs); lhs = ::to_app(_lhs);
rhs = ::to_app(_rhs); rhs = ::to_app(_rhs);
if (rhs->get_num_args() > 0) return false; if (rhs->get_num_args() > 0) return false;
if (rhs->get_family_id() != null_family_id) return false; if (rhs->get_family_id() != null_family_id) return false;
return !occurs(rhs, lhs); return !occurs(rhs, lhs);
} }
public: public:
projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {} projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {}
@ -820,7 +820,7 @@ namespace qe {
m_root2rep.reset(); m_root2rep.reset();
m_decls.reset(); m_decls.reset();
m_pinned.reset(); m_pinned.reset();
} }
expr_ref_vector project(func_decl_ref_vector const &decls, bool exclude) { expr_ref_vector project(func_decl_ref_vector const &decls, bool exclude) {
expr_ref_vector res(m); expr_ref_vector res(m);
m_exclude = exclude; m_exclude = exclude;
@ -830,7 +830,7 @@ namespace qe {
mk_pure_equalities(res); mk_pure_equalities(res);
reset(); reset();
return res; return res;
} }
expr_ref_vector solve(func_decl_ref_vector const &decls, bool exclude) { expr_ref_vector solve(func_decl_ref_vector const &decls, bool exclude) {
expr_ref_vector res(m); expr_ref_vector res(m);
m_exclude = exclude; m_exclude = exclude;
@ -842,12 +842,12 @@ namespace qe {
return res; return res;
} }
}; };
} }
expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) { expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) {
projector p(*this); projector p(*this);
return p.project(decls, exclude); return p.project(decls, exclude);
} }
expr_ref_vector term_graph::solve(func_decl_ref_vector const &decls, bool exclude) { expr_ref_vector term_graph::solve(func_decl_ref_vector const &decls, bool exclude) {
projector p(*this); projector p(*this);