mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

get_app --> get_expr + fix term_lt()

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-11 11:36:46 -07:00
parent dda65fdd2e
commit 9c7d9818d3
2 changed files with 151 additions and 146 deletions
Download patch file Download diff file Expand all files Collapse all files

257
src/qe/qe_term_graph.cpp
View file

@ -28,46 +28,46 @@ namespace qe {
class term { class term {
// -- an app represented by this term // -- an app represented by this term
expr* m_app; // NSB: to make usable with exprs expr* m_expr; // NSB: to make usable with exprs
// -- root of the equivalence class // -- root of the equivalence class
term* m_root; term* m_root;
// -- next element in the equivalence class (cyclic linked list) // -- next element in the equivalence class (cyclic linked list)
term* m_next; term* m_next;
// -- eq class size // -- eq class size
unsigned m_class_size; unsigned m_class_size;
// -- general purpose mark // -- general purpose mark
unsigned m_mark:1; unsigned m_mark:1;
// -- general purpose second mark // -- general purpose second mark
unsigned m_mark2:1; unsigned m_mark2:1;
// -- is an interpreted constant // -- is an interpreted constant
unsigned m_interpreted:1; unsigned m_interpreted:1;
// -- terms that contain this term as a child // -- terms that contain this term as a child
ptr_vector<term> m_parents; ptr_vector<term> m_parents;
// arguments of term. // arguments of term.
ptr_vector<term> m_children; ptr_vector<term> m_children;
public: public:
term(expr* a, u_map<term*>& app2term) : term(expr* v, u_map<term*>& app2term) :
m_app(a), m_expr(v),
m_root(this), m_root(this),
m_next(this), m_next(this),
m_class_size(1), m_class_size(1),
m_mark(false), m_mark(false),
m_mark2(false), m_mark2(false),
m_interpreted(false) { m_interpreted(false) {
if (!is_app(a)) return; if (!is_app()) return;
for (expr* e : *to_app(a)) { for (expr* e : *to_app(m_expr)) {
term* t = app2term[e->get_id()]; term* t = app2term[e->get_id()];
t->get_root().m_parents.push_back(this); t->get_root().m_parents.push_back(this);
m_children.push_back(t); m_children.push_back(t);
} }
} }
~term() {} ~term() {}
class parents { class parents {
term const& t; term const& t;
public: public:
@ -76,7 +76,7 @@ namespace qe {
ptr_vector<term>::const_iterator begin() const { return t.m_parents.begin(); } ptr_vector<term>::const_iterator begin() const { return t.m_parents.begin(); }
ptr_vector<term>::const_iterator end() const { return t.m_parents.end(); } ptr_vector<term>::const_iterator end() const { return t.m_parents.end(); }
}; };
class children { class children {
term const& t; term const& t;
public: public:
@ -85,20 +85,20 @@ namespace qe {
ptr_vector<term>::const_iterator begin() const { return t.m_children.begin(); } ptr_vector<term>::const_iterator begin() const { return t.m_children.begin(); }
ptr_vector<term>::const_iterator end() const { return t.m_children.end(); } ptr_vector<term>::const_iterator end() const { return t.m_children.end(); }
}; };
// Congruence table hash function is based on // Congruence table hash function is based on
// roots of children and function declaration. // roots of children and function declaration.
unsigned get_hash() const { unsigned get_hash() const {
unsigned a, b, c; unsigned a, b, c;
a = b = c = get_decl_id(); a = b = c = get_decl_id();
for (term * ch : children(this)) { for (term * ch : children(this)) {
a = ch->get_root().get_id(); a = ch->get_root().get_id();
mix(a, b, c); mix(a, b, c);
} }
return c; return c;
} }
static bool cg_eq(term const * t1, term const * t2) { static bool cg_eq(term const * t1, term const * t2) {
if (t1->get_decl_id() != t2->get_decl_id()) return false; if (t1->get_decl_id() != t2->get_decl_id()) return false;
if (t1->m_children.size() != t2->m_children.size()) return false; if (t1->m_children.size() != t2->m_children.size()) return false;
@ -107,41 +107,43 @@ namespace qe {
} }
return true; return true;
} }
unsigned get_id() const { return m_app->get_id();} unsigned get_id() const { return m_expr->get_id();}
unsigned get_decl_id() const { return is_app(m_app) ? to_app(m_app)->get_decl()->get_id() : m_app->get_id(); } unsigned get_decl_id() const { return is_app() ? get_app()->get_decl()->get_id() : m_expr->get_id(); }
bool is_marked() const {return m_mark;} bool is_marked() const {return m_mark;}
void set_mark(bool v){m_mark = v;} void set_mark(bool v){m_mark = v;}
bool is_marked2() const {return m_mark2;} // NSB: where is this used? bool is_marked2() const {return m_mark2;} // NSB: where is this used?
void set_mark2(bool v){m_mark2 = v;} // NSB: where is this used? void set_mark2(bool v){m_mark2 = v;} // NSB: where is this used?
bool is_interpreted() const {return m_interpreted;} bool is_interpreted() const {return m_interpreted;}
bool is_theory() const { return !is_app(m_app) || to_app(m_app)->get_family_id() != null_family_id; } bool is_theory() const { return !is_app() || get_app()->get_family_id() != null_family_id; }
void mark_as_interpreted() {m_interpreted=true;} void mark_as_interpreted() {m_interpreted=true;}
expr* get_app() const {return m_app;} expr* get_expr() const {return m_expr;}
unsigned get_num_args() const { return is_app(m_app) ? to_app(m_app)->get_num_args() : 0; } bool is_app() const {return ::is_app(m_expr);}
app *get_app() const {return is_app() ? to_app(m_expr) : nullptr;}
unsigned get_num_args() const { return is_app() ? get_app()->get_num_args() : 0; }
term &get_root() const {return *m_root;} term &get_root() const {return *m_root;}
bool is_root() const {return m_root == this;} bool is_root() const {return m_root == this;}
void set_root(term &r) {m_root = &r;} void set_root(term &r) {m_root = &r;}
term &get_next() const {return *m_next;} term &get_next() const {return *m_next;}
void add_parent(term* p) { m_parents.push_back(p); } void add_parent(term* p) { m_parents.push_back(p); }
unsigned get_class_size() const {return m_class_size;} unsigned get_class_size() const {return m_class_size;}
void merge_eq_class(term &b) { void merge_eq_class(term &b) {
std::swap(this->m_next, b.m_next); std::swap(this->m_next, b.m_next);
m_class_size += b.get_class_size(); m_class_size += b.get_class_size();
// -- reset (useful for debugging) // -- reset (useful for debugging)
b.m_class_size = 0; b.m_class_size = 0;
} }
// -- make this term the root of its equivalence class // -- make this term the root of its equivalence class
void mk_root() { void mk_root() {
if (is_root()) return; if (is_root()) return;
term *curr = this; term *curr = this;
do { do {
if (curr->is_root()) { if (curr->is_root()) {
@ -156,26 +158,26 @@ namespace qe {
while (curr != this); while (curr != this);
} }
}; };
class arith_term_graph_plugin : public term_graph_plugin { class arith_term_graph_plugin : public term_graph_plugin {
term_graph &m_g; term_graph &m_g;
ast_manager &m; ast_manager &m;
arith_util m_arith; arith_util m_arith;
public: public:
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;
e2 = _e2; e2 = _e2;
if (m_arith.is_zero(e1)) { if (m_arith.is_zero(e1)) {
std::swap(e1, e2); std::swap(e1, e2);
} }
@ -194,7 +196,7 @@ namespace qe {
res = m.mk_eq(e1, e2); res = m.mk_eq(e1, e2);
return true; return true;
} }
app* mk_le_zero(expr *arg) { app* mk_le_zero(expr *arg) {
expr *e1, *e2, *e3; expr *e1, *e2, *e3;
// XXX currently disabled // XXX currently disabled
@ -226,7 +228,7 @@ namespace qe {
} }
return m_arith.mk_ge(arg, mk_zero()); return m_arith.mk_ge(arg, mk_zero());
} }
bool mk_le_core (expr *arg1, expr * arg2, expr_ref &result) { bool mk_le_core (expr *arg1, expr * arg2, expr_ref &result) {
// t <= -1 ==> t < 0 ==> ! (t >= 0) // t <= -1 ==> t < 0 ==> ! (t >= 0)
rational n; rational n;
@ -245,13 +247,13 @@ namespace qe {
} }
return false; return false;
} }
expr * mk_zero () {return m_arith.mk_numeral (rational (0), true);} expr * mk_zero () {return m_arith.mk_numeral (rational (0), true);}
bool is_one (expr const * n) const { bool is_one (expr const * n) const {
rational val; rational val;
return m_arith.is_numeral (n, val) && val.is_one (); return m_arith.is_numeral (n, val) && val.is_one ();
} }
bool mk_ge_core (expr * arg1, expr * arg2, expr_ref &result) { bool mk_ge_core (expr * arg1, expr * arg2, expr_ref &result) {
// t >= 1 ==> t > 0 ==> ! (t <= 0) // t >= 1 ==> t > 0 ==> ! (t <= 0)
rational n; rational n;
@ -270,17 +272,17 @@ namespace qe {
} }
return false; return false;
} }
expr_ref process_lit (expr *_lit) override { expr_ref process_lit (expr *_lit) override {
expr *lit = _lit; expr *lit = _lit;
expr *e1, *e2; expr *e1, *e2;
// strip negation // strip negation
bool is_neg = m.is_not(lit); bool is_neg = m.is_not(lit);
if (is_neg) { if (is_neg) {
lit = to_app(to_app(lit)->get_arg(0)); lit = to_app(to_app(lit)->get_arg(0));
} }
expr_ref res(m); expr_ref res(m);
res = lit; res = lit;
if (m.is_eq (lit, e1, e2)) { if (m.is_eq (lit, e1, e2)) {
@ -292,12 +294,12 @@ namespace qe {
else if (m_arith.is_ge(lit, e1, e2)) { else if (m_arith.is_ge(lit, e1, e2)) {
mk_ge_core(e1, e2, res); mk_ge_core(e1, e2, res);
} }
// restore negation // restore negation
if (is_neg) { if (is_neg) {
res = mk_not(m, res); res = mk_not(m, res);
} }
return res; return res;
} }
}; };
@ -309,16 +311,16 @@ namespace qe {
term_graph::term_graph(ast_manager &man) : m(man), m_lits(m), m_pinned(m) { term_graph::term_graph(ast_manager &man) : m(man), m_lits(m), m_pinned(m) {
m_plugins.register_plugin (alloc(arith_term_graph_plugin, *this)); m_plugins.register_plugin (alloc(arith_term_graph_plugin, *this));
} }
term_graph::~term_graph() { term_graph::~term_graph() {
reset(); reset();
} }
static family_id get_family_id(ast_manager &m, expr *lit) { static family_id get_family_id(ast_manager &m, expr *lit) {
if (m.is_not(lit, lit)) if (m.is_not(lit, lit))
return get_family_id(m, lit); return get_family_id(m, lit);
expr *a = nullptr, *b = nullptr; expr *a = nullptr, *b = nullptr;
// deal with equality using sort of range // deal with equality using sort of range
if (m.is_eq (lit, a, b)) { if (m.is_eq (lit, a, b)) {
return get_sort (a)->get_family_id(); return get_sort (a)->get_family_id();
@ -331,10 +333,10 @@ namespace qe {
return null_family_id; return null_family_id;
} }
} }
void term_graph::add_lit(expr *l) { void term_graph::add_lit(expr *l) {
expr_ref lit(m); expr_ref lit(m);
family_id fid = get_family_id (m, l); family_id fid = get_family_id (m, l);
term_graph_plugin *pin = m_plugins.get_plugin(fid); term_graph_plugin *pin = m_plugins.get_plugin(fid);
if (pin) { if (pin) {
@ -345,16 +347,16 @@ namespace qe {
m_lits.push_back(lit); m_lits.push_back(lit);
internalize_lit(lit); internalize_lit(lit);
} }
bool term_graph::is_internalized(expr *a) { bool term_graph::is_internalized(expr *a) {
return m_app2term.contains(a->get_id()); return m_app2term.contains(a->get_id());
} }
term* term_graph::get_term(expr *a) { term* term_graph::get_term(expr *a) {
term *res; term *res;
return m_app2term.find (a->get_id(), res) ? res : nullptr; return m_app2term.find (a->get_id(), res) ? res : nullptr;
} }
term *term_graph::mk_term(expr *a) { term *term_graph::mk_term(expr *a) {
term * t = alloc(term, a, m_app2term); term * t = alloc(term, a, m_app2term);
if (t->get_num_args() == 0 && m.is_unique_value(a)){ if (t->get_num_args() == 0 && m.is_unique_value(a)){
@ -365,8 +367,8 @@ namespace qe {
m_app2term.insert(a->get_id(), t); m_app2term.insert(a->get_id(), t);
return t; return t;
} }
term* term_graph::internalize_term(expr *t) { term* term_graph::internalize_term(expr *t) {
term* res = get_term(t); term* res = get_term(t);
if (res) return res; if (res) return res;
ptr_buffer<expr> todo; ptr_buffer<expr> todo;
@ -381,7 +383,7 @@ namespace qe {
unsigned sz = todo.size(); unsigned sz = todo.size();
if (is_app(t)) { if (is_app(t)) {
for (expr * arg : *::to_app(t)) { for (expr * arg : *::to_app(t)) {
if (!get_term(arg)) if (!get_term(arg))
todo.push_back(arg); todo.push_back(arg);
} }
} }
@ -392,7 +394,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)->get_root(), internalize_term(a2)->get_root()); merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root());
@ -402,7 +404,7 @@ namespace qe {
void term_graph::internalize_lit(expr* lit) { void term_graph::internalize_lit(expr* lit) {
expr *e1 = nullptr, *e2 = nullptr; expr *e1 = nullptr, *e2 = nullptr;
if (m.is_eq (lit, e1, e2)) { if (m.is_eq (lit, e1, e2)) {
internalize_eq (e1, e2); internalize_eq (e1, e2);
} }
else { else {
@ -422,19 +424,19 @@ namespace qe {
void term_graph::merge(term &t1, term &t2) { void term_graph::merge(term &t1, term &t2) {
// -- merge might invalidate term2map cache // -- merge might invalidate term2map cache
m_term2app.reset(); m_term2app.reset();
m_pinned.reset(); m_pinned.reset();
SASSERT(t1.is_root()); SASSERT(t1.is_root());
SASSERT(t2.is_root()); SASSERT(t2.is_root());
if (&t1 == &t2) return; if (&t1 == &t2) return;
term *a = &t1; term *a = &t1;
term *b = &t2; term *b = &t2;
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()) {
@ -442,15 +444,15 @@ namespace qe {
m_cg_table.erase(p); m_cg_table.erase(p);
} }
} }
// make 'a' be the root of the equivalence class of 'b' // make 'a' be the root of the equivalence class of 'b'
b->set_root(*a); b->set_root(*a);
for (term *it = &b->get_next(); it != b; it = &it->get_next()) { for (term *it = &b->get_next(); it != b; it = &it->get_next()) {
it->set_root(*a); it->set_root(*a);
} }
// merge equivalence classes // merge equivalence classes
a->merge_eq_class(*b); a->merge_eq_class(*b);
// Insert parents of b's old equilvalence class into the cg table // Insert parents of b's old equilvalence class into the cg table
for (term* p : term::parents(a)) { for (term* p : term::parents(a)) {
if (p->is_marked()) { if (p->is_marked()) {
@ -462,16 +464,16 @@ namespace qe {
m_merge.push_back(std::make_pair(p, p_old)); m_merge.push_back(std::make_pair(p, p_old));
} }
} }
} }
} }
expr* term_graph::mk_app_core (expr *e) { expr* term_graph::mk_app_core (expr *e) {
if (is_app(e)) { if (is_app(e)) {
expr_ref_vector kids(m); expr_ref_vector kids(m);
app* a = ::to_app(e); app* a = ::to_app(e);
for (expr * arg : *a) { for (expr * arg : *a) {
kids.push_back (mk_app(arg)); kids.push_back (mk_app(arg));
} }
app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.c_ptr()); app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.c_ptr());
m_pinned.push_back(res); m_pinned.push_back(res);
return res; return res;
@ -483,44 +485,44 @@ namespace qe {
expr_ref term_graph::mk_app(term const &r) { expr_ref term_graph::mk_app(term const &r) {
SASSERT(r.is_root()); SASSERT(r.is_root());
if (r.get_num_args() == 0) { if (r.get_num_args() == 0) {
return expr_ref(r.get_app(), m); return expr_ref(r.get_expr(), m);
} }
expr* res = nullptr; expr* res = nullptr;
if (m_term2app.find(r.get_id(), res)) { if (m_term2app.find(r.get_id(), res)) {
return expr_ref(res, m); return expr_ref(res, m);
} }
res = mk_app_core (r.get_app()); res = mk_app_core (r.get_app());
m_term2app.insert(r.get_id(), res); m_term2app.insert(r.get_id(), res);
return expr_ref(res, m); return expr_ref(res, m);
} }
expr_ref term_graph::mk_app(expr *a) { expr_ref term_graph::mk_app(expr *a) {
term *t = get_term(a); term *t = get_term(a);
if (!t) if (!t)
return expr_ref(a, m); return expr_ref(a, m);
else else
return mk_app(t->get_root()); return mk_app(t->get_root());
} }
void term_graph::mk_equalities(term const &t, expr_ref_vector &out) { void term_graph::mk_equalities(term const &t, expr_ref_vector &out) {
SASSERT(t.is_root()); SASSERT(t.is_root());
expr_ref rep(mk_app(t), m); expr_ref rep(mk_app(t), m);
for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { for (term *it = &t.get_next(); it != &t; it = &it->get_next()) {
expr* mem = mk_app_core(it->get_app()); expr* mem = mk_app_core(it->get_app());
out.push_back (m.mk_eq (rep, mem)); out.push_back (m.mk_eq (rep, mem));
} }
} }
void term_graph::mk_all_equalities(term const &t, expr_ref_vector &out) { void term_graph::mk_all_equalities(term const &t, expr_ref_vector &out) {
mk_equalities(t, out); mk_equalities(t, out);
for (term *it = &t.get_next(); it != &t; it = &it->get_next ()) { for (term *it = &t.get_next(); it != &t; it = &it->get_next ()) {
expr* a1 = mk_app_core (it->get_app()); expr* a1 = mk_app_core (it->get_app());
for (term *it2 = &it->get_next(); it2 != &t; it2 = &it2->get_next()) { for (term *it2 = &it->get_next(); it2 != &t; it2 = &it2->get_next()) {
@ -529,30 +531,32 @@ namespace qe {
} }
} }
} }
void term_graph::reset_marks() { void term_graph::reset_marks() {
for (term * t : m_terms) { for (term * t : m_terms) {
t->set_mark(false); t->set_mark(false);
} }
} }
/// Order of preference for roots of equivalence classes /// Order of preference for roots of equivalence classes
/// XXX This should be factored out to let clients control the preference /// XXX This should be factored out to let clients control the preference
bool term_graph::term_le(term const &t1, term const &t2) { bool term_graph::term_lt(term const &t1, term const &t2) {
// prefer constants over applications // prefer constants over applications
// prefer uninterpreted constants over values // prefer uninterpreted constants over values
// prefer smaller expressions over larger ones // prefer smaller expressions over larger ones
if (t1.get_num_args() == 0 && t2.get_num_args() > 0) { if (t1.get_num_args() == 0 || t2.get_num_args() == 0) {
return true; if (t1.get_num_args() == t2.get_num_args()) {
// t1.get_num_args() == t2.get_num_args() == 0
if (m.is_value(t1.get_expr()) == m.is_value(t2.get_expr()))
return t1.get_id() < t2.get_id();
return m.is_value(t2.get_expr());
}
return t1.get_num_args() < t2.get_num_args();
} }
if (t1.get_num_args() == t2.get_num_args()) {
// NSB: how does this possibly define an order? unsigned sz1 = get_num_exprs(t1.get_expr());
return m.is_value(t2.get_app()); unsigned sz2 = get_num_exprs(t1.get_expr());
}
unsigned sz1 = get_num_exprs(t1.get_app());
unsigned sz2 = get_num_exprs(t1.get_app());
return sz1 < sz2; return sz1 < sz2;
} }
@ -560,9 +564,9 @@ namespace qe {
term *r = &t; term *r = &t;
for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { for (term *it = &t.get_next(); it != &t; it = &it->get_next()) {
it->set_mark(true); it->set_mark(true);
if (term_le(*it, *r)) { r = it; } if (term_lt(*it, *r)) { r = it; }
} }
// -- if found something better, make it the new root // -- if found something better, make it the new root
if (r != &t) { if (r != &t) {
r->mk_root(); r->mk_root();
@ -572,47 +576,47 @@ namespace qe {
/// Choose better roots for equivalence classes /// Choose better roots for equivalence classes
void term_graph::pick_roots() { void term_graph::pick_roots() {
for (term* t : m_terms) { for (term* t : m_terms) {
if (!t->is_marked() && t->is_root()) if (!t->is_marked() && t->is_root())
pick_root(*t); pick_root(*t);
} }
reset_marks(); reset_marks();
} }
void term_graph::display(std::ostream &out) { void term_graph::display(std::ostream &out) {
for (term * t : m_terms) { for (term * t : m_terms) {
out << mk_pp(t->get_app(), m) << " is root " << t->is_root() out << mk_pp(t->get_expr(), m) << " is root " << t->is_root()
<< " cls sz " << t->get_class_size() << " cls sz " << t->get_class_size()
<< " term " << t << " term " << t
<< "\n"; << "\n";
} }
} }
void term_graph::to_lits (expr_ref_vector &lits, bool all_equalities) { void term_graph::to_lits (expr_ref_vector &lits, bool all_equalities) {
pick_roots(); pick_roots();
for (expr * a : m_lits) { for (expr * a : m_lits) {
if (is_internalized(a)) { if (is_internalized(a)) {
lits.push_back (::to_app(mk_app(a))); lits.push_back (::to_app(mk_app(a)));
} }
} }
for (term * t : m_terms) { for (term * t : m_terms) {
if (!t->is_root()) if (!t->is_root())
continue; continue;
else if (all_equalities) else if (all_equalities)
mk_all_equalities (*t, lits); mk_all_equalities (*t, lits);
else else
mk_equalities(*t, lits); mk_equalities(*t, lits);
} }
} }
expr_ref term_graph::to_app() { expr_ref term_graph::to_app() {
expr_ref_vector lits(m); expr_ref_vector lits(m);
to_lits(lits); to_lits(lits);
return mk_and(lits); return mk_and(lits);
} }
void term_graph::reset() { void term_graph::reset() {
m_term2app.reset(); m_term2app.reset();
m_pinned.reset(); m_pinned.reset();
@ -622,9 +626,10 @@ namespace qe {
m_lits.reset(); m_lits.reset();
m_cg_table.reset(); m_cg_table.reset();
} }
expr* term_graph::mk_pure(term& t) { expr* term_graph::mk_pure(term& t) {
expr* e = t.get_app(); expr* e = t.get_expr();
// AG: the if-statement looks wrong
if (m_term2app.find(t.get_id(), e)) e; if (m_term2app.find(t.get_id(), e)) e;
if (!is_app(e)) return nullptr; if (!is_app(e)) return nullptr;
app* a = ::to_app(e); app* a = ::to_app(e);
@ -638,35 +643,35 @@ namespace qe {
m_term2app.insert(t.get_id(), result); m_term2app.insert(t.get_id(), result);
return result; return result;
} }
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) {
u_map<bool> _decls; u_map<bool> _decls;
for (func_decl* f : decls) _decls.insert(f->get_id(), true); for (func_decl* f : decls) _decls.insert(f->get_id(), true);
// . 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 lhs/rhs over decls or excluding decls) // (walk disequalities in m_lits and represent lhs/rhs over decls or excluding decls)
expr_ref_vector result(m); expr_ref_vector result(m);
m_term2app.reset(); m_term2app.reset();
m_pinned.reset(); m_pinned.reset();
obj_hashtable<expr> eqs; obj_hashtable<expr> eqs;
expr_ref eq(m); expr_ref eq(m);
ptr_vector<term> worklist; ptr_vector<term> worklist;
for (term * t : m_terms) { for (term * t : 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() && exclude == _decls.contains(t->get_decl_id())) if (!t->is_theory() && exclude == _decls.contains(t->get_decl_id()))
continue; continue;
term& root = t->get_root(); term& root = t->get_root();
@ -675,7 +680,7 @@ namespace qe {
if (!pure) continue; if (!pure) continue;
// ensure that the root has a representative // ensure that the root has a representative
// either by looking up cached version, // either by looking up cached version,
// computing it for the first time, or // computing it for the first time, or
// inheriting pure. // inheriting pure.
expr* rep = nullptr; expr* rep = nullptr;
@ -691,7 +696,7 @@ namespace qe {
} }
bool update_rep = false; bool update_rep = false;
// Add equations between pure and rep, // Add equations between pure and rep,
// optionally swap the roles of rep and pure if // optionally swap the roles of rep and pure if
// pure makes a better representative. // pure makes a better representative.
if (rep != pure) { if (rep != pure) {
@ -706,7 +711,7 @@ namespace qe {
} }
} }
// update the worklist if this is the first // update the worklist if this is the first
// representative or pure was swapped into rep. // representative or pure was swapped into rep.
if (!has_rep || update_rep) { if (!has_rep || update_rep) {
for (term * p : term::parents(root)) { for (term * p : term::parents(root)) {
@ -723,10 +728,10 @@ namespace qe {
if (!m.is_eq(e) && m_term2app.find(get_term(e)->get_root().get_id(), e)) { if (!m.is_eq(e) && m_term2app.find(get_term(e)->get_root().get_id(), e)) {
result.push_back(e); result.push_back(e);
} }
} }
// Here we could also walk equivalence classes that contain interpreted values by sort and // Here we could also walk equivalence classes that contain interpreted values by sort and
// extract disequalities bewteen non-unique value representatives. // extract disequalities bewteen non-unique value representatives.
// these disequalities are implied and can be mined using other means, such as // these disequalities are implied and can be mined using other means, such as
// theory aware core minimization // theory aware core minimization
m_term2app.reset(); m_term2app.reset();
m_pinned.reset(); m_pinned.reset();

40
src/qe/qe_term_graph.h
View file

@ -33,11 +33,11 @@ namespace qe {
virtual ~term_graph_plugin() {} virtual ~term_graph_plugin() {}
family_id get_family_id() const {return m_id;} family_id get_family_id() const {return m_id;}
/// Process (and potentially augment) a literal /// Process (and potentially augment) a literal
virtual expr_ref process_lit (expr *lit) = 0; virtual expr_ref process_lit (expr *lit) = 0;
}; };
class term_graph { class term_graph {
struct term_hash { unsigned operator()(term const* t) const; }; struct term_hash { unsigned operator()(term const* t) const; };
@ -45,62 +45,62 @@ namespace qe {
ast_manager & m; ast_manager & m;
ptr_vector<term> m_terms; ptr_vector<term> m_terms;
expr_ref_vector m_lits; // NSB: expr_ref_vector? expr_ref_vector m_lits; // NSB: expr_ref_vector?
u_map<term* > m_app2term; u_map<term* > m_app2term;
ast_ref_vector m_pinned; ast_ref_vector m_pinned;
u_map<expr*> m_term2app; u_map<expr*> m_term2app;
plugin_manager<term_graph_plugin> m_plugins; plugin_manager<term_graph_plugin> m_plugins;
ptr_hashtable<term, term_hash, term_eq> m_cg_table; ptr_hashtable<term, term_hash, term_eq> m_cg_table;
vector<std::pair<term*,term*>> m_merge; vector<std::pair<term*,term*>> m_merge;
void merge(term &t1, term &t2); void merge(term &t1, term &t2);
void merge_flush(); void merge_flush();
term *mk_term(expr *t); term *mk_term(expr *t);
term *get_term(expr *t); term *get_term(expr *t);
term *internalize_term(expr *t); term *internalize_term(expr *t);
void internalize_eq(expr *a1, expr *a2); void internalize_eq(expr *a1, expr *a2);
void internalize_lit(expr *lit); void internalize_lit(expr *lit);
bool is_internalized(expr *a); bool is_internalized(expr *a);
bool term_le(term const &t1, term const &t2); bool term_lt(term const &t1, term const &t2);
void pick_root (term &t); void pick_root (term &t);
void pick_roots(); void pick_roots();
void reset_marks(); void reset_marks();
expr* mk_app_core(expr* a); expr* mk_app_core(expr* a);
expr_ref mk_app(term const &t); expr_ref mk_app(term const &t);
expr* mk_pure(term& t); expr* mk_pure(term& t);
expr_ref mk_app(expr *a); expr_ref mk_app(expr *a);
void mk_equalities(term const &t, expr_ref_vector &out); void mk_equalities(term const &t, expr_ref_vector &out);
void mk_all_equalities(term const &t, expr_ref_vector &out); void mk_all_equalities(term const &t, expr_ref_vector &out);
void display(std::ostream &out); void display(std::ostream &out);
public: public:
term_graph(ast_manager &m); term_graph(ast_manager &m);
~term_graph(); ~term_graph();
ast_manager& get_ast_manager() const { return m;} ast_manager& get_ast_manager() const { return m;}
void add_lit(expr *lit); void add_lit(expr *lit);
void add_lits(expr_ref_vector const &lits) { for (expr* e : lits) add_lit(e); } void add_lits(expr_ref_vector const &lits) { for (expr* e : lits) add_lit(e); }
void add_eq(expr* a, expr* b) { internalize_eq(a, b); } void add_eq(expr* a, expr* b) { internalize_eq(a, b); }
void reset(); void reset();
// deprecate? // deprecate?
void to_lits(expr_ref_vector &lits, bool all_equalities = false); void to_lits(expr_ref_vector &lits, bool all_equalities = false);
expr_ref to_app(); expr_ref to_app();
/** /**
* Return literals obtained by projecting added literals * Return literals obtained by projecting added literals
* onto the vocabulary of decls (if exclude is false) or outside the * onto the vocabulary of decls (if exclude is false) or outside the
* vocabulary of decls (if exclude is true). * vocabulary of decls (if exclude is true).
*/ */
expr_ref_vector project(func_decl_ref_vector const& decls, bool exclude); expr_ref_vector project(func_decl_ref_vector const& decls, bool exclude);
}; };
} }