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

Change declaration of projector

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-14 06:37:09 -07:00
parent bbd917a0e6
commit e355123e37
2 changed files with 235 additions and 238 deletions
Download patch file Download diff file Expand all files Collapse all files

470
src/qe/qe_term_graph.cpp
View file

@ -540,270 +540,268 @@ namespace qe {
m_cg_table.reset(); m_cg_table.reset();
} }
namespace { class term_graph::projector {
class projector { term_graph &m_tg;
term_graph &m_tg; ast_manager &m;
ast_manager &m; u_map<expr*> m_term2app;
u_map<expr*> m_term2app; u_map<expr*> m_root2rep;
u_map<expr*> m_root2rep;
model_ref m_model; model_ref m_model;
expr_ref_vector m_pinned; // tracks expr in the maps expr_ref_vector m_pinned; // tracks expr in the maps
expr* mk_pure(term const& t) { expr* mk_pure(term const& 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) {
if (!t2) return t1 != nullptr;
return m.is_unique_value(t1) && !m.is_unique_value(t2);
}
void purify() {
// - propagate representatives up over parents.
// use work-list + marking to propagate.
// - produce equalities over represented classes.
// - produce other literals over represented classes
// (walk disequalities in m_lits and represent
// lhs/rhs over decls or excluding decls)
ptr_vector<term> worklist;
for (term * t : m_tg.m_terms) {
worklist.push_back(t);
t->set_mark(true);
} }
while (!worklist.empty()) {
term* t = worklist.back();
worklist.pop_back();
t->set_mark(false);
if (m_term2app.contains(t->get_id()))
continue;
if (!t->is_theory() && is_projected(*t))
continue;
bool is_better_rep(expr *t1, expr *t2) { expr* pure = mk_pure(*t);
if (!t2) return t1 != nullptr; if (!pure) continue;
return m.is_unique_value(t1) && !m.is_unique_value(t2);
}
void purify() { m_term2app.insert(t->get_id(), pure);
// - propagate representatives up over parents. expr* rep = nullptr;
// use work-list + marking to propagate. // ensure that the root has a representative
// - produce equalities over represented classes. m_root2rep.find(t->get_root().get_id(), rep);
// - produce other literals over represented classes
// (walk disequalities in m_lits and represent
// lhs/rhs over decls or excluding decls)
ptr_vector<term> worklist; // update rep with pure if it is better
for (term * t : m_tg.m_terms) { if (pure != rep && is_better_rep(pure, rep)) {
worklist.push_back(t); m_root2rep.insert(t->get_root().get_id(), pure);
t->set_mark(true); for (term * p : term::parents(t->get_root())) {
} m_term2app.remove(p->get_id());
if (!p->is_marked()) {
while (!worklist.empty()) { p->set_mark(true);
term* t = worklist.back(); worklist.push_back(p);
worklist.pop_back();
t->set_mark(false);
if (m_term2app.contains(t->get_id()))
continue;
if (!t->is_theory() && is_projected(*t))
continue;
expr* pure = mk_pure(*t);
if (!pure) continue;
m_term2app.insert(t->get_id(), pure);
expr* rep = nullptr;
// ensure that the root has a representative
m_root2rep.find(t->get_root().get_id(), rep);
// update rep with pure if it is better
if (pure != rep && is_better_rep(pure, rep)) {
m_root2rep.insert(t->get_root().get_id(), pure);
for (term * p : term::parents(t->get_root())) {
m_term2app.remove(p->get_id());
if (!p->is_marked()) {
p->set_mark(true);
worklist.push_back(p);
}
} }
} }
} }
// Here we could also walk equivalence classes that
// contain interpreted values by sort and extract
// disequalities bewteen non-unique value
// representatives. these disequalities are implied
// and can be mined using other means, such as theory
// aware core minimization
m_tg.reset_marks();
} }
void solve_core() { // Here we could also walk equivalence classes that
ptr_vector<term> worklist; // contain interpreted values by sort and extract
for (term * t : m_tg.m_terms) { // disequalities bewteen non-unique value
// skip pure terms // representatives. these disequalities are implied
if (m_term2app.contains(t->get_id())) continue; // and can be mined using other means, such as theory
worklist.push_back(t); // aware core minimization
t->set_mark(true); m_tg.reset_marks();
} }
while (!worklist.empty()) { void solve_core() {
term* t = worklist.back(); ptr_vector<term> worklist;
worklist.pop_back(); for (term * t : m_tg.m_terms) {
t->set_mark(false); // skip pure terms
if (m_term2app.contains(t->get_id())) if (m_term2app.contains(t->get_id())) continue;
continue; worklist.push_back(t);
t->set_mark(true);
}
expr* pure = mk_pure(*t); while (!worklist.empty()) {
if (!pure) continue; term* t = worklist.back();
worklist.pop_back();
t->set_mark(false);
if (m_term2app.contains(t->get_id()))
continue;
m_term2app.insert(t->get_id(), pure); expr* pure = mk_pure(*t);
expr* rep = nullptr; if (!pure) continue;
// ensure that the root has a representative
m_root2rep.find(t->get_root().get_id(), rep);
if (!rep) { m_term2app.insert(t->get_id(), pure);
m_root2rep.insert(t->get_root().get_id(), pure); expr* rep = nullptr;
for (term * p : term::parents(t->get_root())) { // ensure that the root has a representative
SASSERT(!m_term2app.contains(p->get_id())); m_root2rep.find(t->get_root().get_id(), rep);
if (!p->is_marked()) {
p->set_mark(true); if (!rep) {
worklist.push_back(p); m_root2rep.insert(t->get_root().get_id(), pure);
} for (term * p : term::parents(t->get_root())) {
SASSERT(!m_term2app.contains(p->get_id()));
if (!p->is_marked()) {
p->set_mark(true);
worklist.push_back(p);
} }
} }
} }
m_tg.reset_marks();
} }
m_tg.reset_marks();
}
bool find_app(term &t, expr *&res) { bool find_app(term &t, expr *&res) {
return m_root2rep.find(t.get_root().get_id(), res); return m_root2rep.find(t.get_root().get_id(), res);
}
bool find_app(expr *lit, expr *&res) {
return m_root2rep.find(m_tg.get_term(lit)->get_root().get_id(), res);
}
void mk_lits(expr_ref_vector &res) {
expr *e = nullptr;
for (auto *lit : m_tg.m_lits) {
if (!m.is_eq(lit) && find_app(lit, e))
res.push_back(e);
} }
}
bool find_app(expr *lit, expr *&res) { void mk_pure_equalities(const term &t, expr_ref_vector &res) {
return m_root2rep.find(m_tg.get_term(lit)->get_root().get_id(), res); SASSERT(t.is_root());
expr *rep = nullptr;
if (!m_root2rep.find(t.get_id(), rep)) return;
obj_hashtable<expr> members;
members.insert(rep);
term const * r = &t;
do {
expr* member = nullptr;
if (m_term2app.find(r->get_id(), member) && !members.contains(member)) {
res.push_back (m.mk_eq (rep, member));
members.insert(member);
}
r = &r->get_next();
} }
while (r != &t);
}
void mk_lits(expr_ref_vector &res) { bool is_projected(const term &t) {return m_tg.m_is_var(t);}
expr *e = nullptr;
for (auto *lit : m_tg.m_lits) { void mk_unpure_equalities(const term &t, expr_ref_vector &res) {
if (!m.is_eq(lit) && find_app(lit, e)) expr *rep = nullptr;
res.push_back(e); if (!m_root2rep.find(t.get_id(), rep)) return;
obj_hashtable<expr> members;
members.insert(rep);
term const * r = &t;
do {
expr* member = mk_pure(*r);
SASSERT(member);
if (!members.contains(member) &&
(!is_projected(*r) || !is_solved_eq(rep, member))) {
res.push_back(m.mk_eq(rep, member));
members.insert(member);
}
r = &r->get_next();
}
while (r != &t);
}
void mk_equalities(bool pure, expr_ref_vector &res) {
for (term *t : m_tg.m_terms) {
if (!t->is_root()) continue;
if (!m_root2rep.contains(t->get_id())) continue;
if (pure)
mk_pure_equalities(*t, res);
else
mk_unpure_equalities(*t, res);
}
}
void mk_pure_equalities(expr_ref_vector &res) {
return mk_equalities(true, res);
}
void mk_unpure_equalities(expr_ref_vector &res) {
return mk_equalities(false, res);
}
// TBD: generalize for also the case of a (:var n)
bool is_solved_eq(expr *lhs, expr* rhs) {
return is_uninterp_const(rhs) && !occurs(rhs, lhs);
}
/// Add equalities and disequalities for all pure representatives
/// based on their equivalence in the model
void model_complete(expr_ref_vector &res) {
if (!m_model) return;
obj_map<expr,expr*> val2rep;
model_evaluator mev(*m_model);
for (auto &kv : m_root2rep) {
expr *rep = kv.m_value;
expr_ref val(m);
expr *u = nullptr;
if (!mev.eval(rep, val)) continue;
if (val2rep.find(val, u)) {
res.push_back(m.mk_eq(u, rep));
}
else {
val2rep.insert(val, rep);
} }
} }
// TBD: this ignores types, need one use of 'distinct' per sort.
void mk_pure_equalities(const term &t, expr_ref_vector &res) { // TBD: probably ignore distinct on values
SASSERT(t.is_root()); // TBD: ignore distinct on Booleans
expr *rep = nullptr; ptr_buffer<expr> reps;
if (!m_root2rep.find(t.get_id(), rep)) return; for (auto &kv : val2rep) {
obj_hashtable<expr> members; reps.push_back(kv.m_value);
members.insert(rep); std::cout << mk_pp(kv.m_value, m) << "\n";
term const * r = &t;
do {
expr* member = nullptr;
if (m_term2app.find(r->get_id(), member) && !members.contains(member)) {
res.push_back (m.mk_eq (rep, member));
members.insert(member);
}
r = &r->get_next();
}
while (r != &t);
} }
// res.push_back(m.mk_distinct(reps.size(), reps.c_ptr()));
}
bool is_projected(const term &t) {return m_tg.m_is_var(t);} public:
projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {}
void mk_unpure_equalities(const term &t, expr_ref_vector &res) { void set_model(model &mdl) { m_model = &mdl; }
expr *rep = nullptr;
if (!m_root2rep.find(t.get_id(), rep)) return;
obj_hashtable<expr> members;
members.insert(rep);
term const * r = &t;
do {
expr* member = mk_pure(*r);
SASSERT(member);
if (!members.contains(member) &&
(!is_projected(*r) || !is_solved_eq(rep, member))) {
res.push_back(m.mk_eq(rep, member));
members.insert(member);
}
r = &r->get_next();
}
while (r != &t);
}
void mk_equalities(bool pure, expr_ref_vector &res) { void reset() {
for (term *t : m_tg.m_terms) { m_tg.reset_marks();
if (!t->is_root()) continue; m_term2app.reset();
if (!m_root2rep.contains(t->get_id())) continue; m_root2rep.reset();
if (pure) m_pinned.reset();
mk_pure_equalities(*t, res); m_model.reset();
else }
mk_unpure_equalities(*t, res); expr_ref_vector project() {
} expr_ref_vector res(m);
} purify();
mk_lits(res);
void mk_pure_equalities(expr_ref_vector &res) { mk_pure_equalities(res);
return mk_equalities(true, res); model_complete(res);
} reset();
return res;
void mk_unpure_equalities(expr_ref_vector &res) { }
return mk_equalities(false, res); expr_ref_vector solve() {
} expr_ref_vector res(m);
purify();
// TBD: generalize for also the case of a (:var n) solve_core();
bool is_solved_eq(expr *lhs, expr* rhs) { mk_lits(res);
return is_uninterp_const(rhs) && !occurs(rhs, lhs); mk_unpure_equalities(res);
} reset();
return res;
/// Add equalities and disequalities for all pure representatives }
/// based on their equivalence in the model };
void model_complete(expr_ref_vector &res) {
if (!m_model) return;
obj_map<expr,expr*> val2rep;
model_evaluator mev(*m_model);
for (auto &kv : m_root2rep) {
expr *rep = kv.m_value;
expr_ref val(m);
expr *u = nullptr;
if (!mev.eval(rep, val)) continue;
if (val2rep.find(val, u)) {
res.push_back(m.mk_eq(u, rep));
}
else {
val2rep.insert(val, rep);
}
}
// TBD: this ignores types, need one use of 'distinct' per sort.
// TBD: probably ignore distinct on values
// TBD: ignore distinct on Booleans
ptr_buffer<expr> reps;
for (auto &kv : val2rep) {
reps.push_back(kv.m_value);
std::cout << mk_pp(kv.m_value, m) << "\n";
}
// res.push_back(m.mk_distinct(reps.size(), reps.c_ptr()));
}
public:
projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {}
void set_model(model &mdl) { m_model = &mdl; }
void reset() {
m_tg.reset_marks();
m_term2app.reset();
m_root2rep.reset();
m_pinned.reset();
m_model.reset();
}
expr_ref_vector project() {
expr_ref_vector res(m);
purify();
mk_lits(res);
mk_pure_equalities(res);
model_complete(res);
reset();
return res;
}
expr_ref_vector solve() {
expr_ref_vector res(m);
purify();
solve_core();
mk_lits(res);
mk_unpure_equalities(res);
reset();
return res;
}
};
}
void term_graph::set_vars(func_decl_ref_vector const& decls, bool exclude) { void term_graph::set_vars(func_decl_ref_vector const& decls, bool exclude) {
m_is_var.set_decls(decls, exclude); m_is_var.set_decls(decls, exclude);
@ -812,13 +810,13 @@ namespace qe {
expr_ref_vector term_graph::project() { expr_ref_vector term_graph::project() {
// reset solved vars so that they are not considered pure by projector // reset solved vars so that they are not considered pure by projector
m_is_var.reset_solved(); m_is_var.reset_solved();
projector p(*this); term_graph::projector p(*this);
return p.project(); return p.project();
} }
expr_ref_vector term_graph::project(model &mdl) { expr_ref_vector term_graph::project(model &mdl) {
m_is_var.reset_solved(); m_is_var.reset_solved();
projector p(*this); term_graph::projector p(*this);
p.set_model(mdl); p.set_model(mdl);
return p.project(); return p.project();
} }
@ -826,7 +824,7 @@ namespace qe {
expr_ref_vector term_graph::solve() { expr_ref_vector term_graph::solve() {
// reset solved vars so that they are not considered pure by projector // reset solved vars so that they are not considered pure by projector
m_is_var.reset_solved(); m_is_var.reset_solved();
projector p(*this); term_graph::projector p(*this);
return p.solve(); return p.solve();
} }

3
src/qe/qe_term_graph.h
View file

@ -28,10 +28,9 @@ Notes:
namespace qe { namespace qe {
class term; class term;
namespace {class projector;}
class term_graph { class term_graph {
friend class projector; class projector;
class is_variable_proc : public ::is_variable_proc { class is_variable_proc : public ::is_variable_proc {
bool m_exclude; bool m_exclude;