From 9c7d9818d304ab0212d946d7d7c59c3dbfb63ad9 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 11 Jun 2018 11:36:46 -0700 Subject: [PATCH] get_app --> get_expr + fix term_lt() --- src/qe/qe_term_graph.cpp | 257 ++++++++++++++++++++------------------- src/qe/qe_term_graph.h | 40 +++--- 2 files changed, 151 insertions(+), 146 deletions(-) diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index e723542a2..b951244f3 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -28,46 +28,46 @@ namespace qe { class 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 term* m_root; // -- next element in the equivalence class (cyclic linked list) term* m_next; // -- eq class size unsigned m_class_size; - + // -- general purpose mark unsigned m_mark:1; // -- general purpose second mark unsigned m_mark2:1; // -- is an interpreted constant unsigned m_interpreted:1; - + // -- terms that contain this term as a child ptr_vector m_parents; - + // arguments of term. ptr_vector m_children; - + public: - term(expr* a, u_map& app2term) : - m_app(a), - m_root(this), + term(expr* v, u_map& app2term) : + m_expr(v), + m_root(this), m_next(this), - m_class_size(1), - m_mark(false), + m_class_size(1), + m_mark(false), m_mark2(false), m_interpreted(false) { - if (!is_app(a)) return; - for (expr* e : *to_app(a)) { + if (!is_app()) return; + for (expr* e : *to_app(m_expr)) { term* t = app2term[e->get_id()]; t->get_root().m_parents.push_back(this); m_children.push_back(t); } } - + ~term() {} - + class parents { term const& t; public: @@ -76,7 +76,7 @@ namespace qe { ptr_vector::const_iterator begin() const { return t.m_parents.begin(); } ptr_vector::const_iterator end() const { return t.m_parents.end(); } }; - + class children { term const& t; public: @@ -85,20 +85,20 @@ namespace qe { ptr_vector::const_iterator begin() const { return t.m_children.begin(); } ptr_vector::const_iterator end() const { return t.m_children.end(); } }; - + // Congruence table hash function is based on // roots of children and function declaration. - + unsigned get_hash() const { unsigned a, b, c; - a = b = c = get_decl_id(); + a = b = c = get_decl_id(); for (term * ch : children(this)) { a = ch->get_root().get_id(); mix(a, b, c); } return c; } - + static bool cg_eq(term const * t1, term const * t2) { if (t1->get_decl_id() != t2->get_decl_id()) return false; if (t1->m_children.size() != t2->m_children.size()) return false; @@ -107,41 +107,43 @@ namespace qe { } return true; } - - unsigned get_id() const { return m_app->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_id() const { return m_expr->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;} void set_mark(bool v){m_mark = v;} 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? - + 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;} - expr* get_app() const {return m_app;} - unsigned get_num_args() const { return is_app(m_app) ? to_app(m_app)->get_num_args() : 0; } - + expr* get_expr() const {return m_expr;} + 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;} bool is_root() const {return m_root == this;} void set_root(term &r) {m_root = &r;} term &get_next() const {return *m_next;} void add_parent(term* p) { m_parents.push_back(p); } - + unsigned get_class_size() const {return m_class_size;} - + void merge_eq_class(term &b) { std::swap(this->m_next, b.m_next); m_class_size += b.get_class_size(); // -- reset (useful for debugging) b.m_class_size = 0; } - + // -- make this term the root of its equivalence class void mk_root() { if (is_root()) return; - + term *curr = this; do { if (curr->is_root()) { @@ -156,26 +158,26 @@ namespace qe { while (curr != this); } }; - + class arith_term_graph_plugin : public term_graph_plugin { term_graph &m_g; ast_manager &m; arith_util m_arith; - + public: arith_term_graph_plugin(term_graph &g) : 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;} - + virtual ~arith_term_graph_plugin() {} - + bool mk_eq_core (expr *_e1, expr *_e2, expr_ref &res) { expr *e1, *e2; e1 = _e1; e2 = _e2; - + if (m_arith.is_zero(e1)) { std::swap(e1, e2); } @@ -194,7 +196,7 @@ namespace qe { res = m.mk_eq(e1, e2); return true; } - + app* mk_le_zero(expr *arg) { expr *e1, *e2, *e3; // XXX currently disabled @@ -226,7 +228,7 @@ namespace qe { } return m_arith.mk_ge(arg, mk_zero()); } - + bool mk_le_core (expr *arg1, expr * arg2, expr_ref &result) { // t <= -1 ==> t < 0 ==> ! (t >= 0) rational n; @@ -245,13 +247,13 @@ namespace qe { } return false; } - + expr * mk_zero () {return m_arith.mk_numeral (rational (0), true);} bool is_one (expr const * n) const { rational val; return m_arith.is_numeral (n, val) && val.is_one (); } - + bool mk_ge_core (expr * arg1, expr * arg2, expr_ref &result) { // t >= 1 ==> t > 0 ==> ! (t <= 0) rational n; @@ -270,17 +272,17 @@ namespace qe { } return false; } - + expr_ref process_lit (expr *_lit) override { expr *lit = _lit; expr *e1, *e2; - + // strip negation bool is_neg = m.is_not(lit); if (is_neg) { lit = to_app(to_app(lit)->get_arg(0)); } - + expr_ref res(m); res = lit; if (m.is_eq (lit, e1, e2)) { @@ -292,12 +294,12 @@ namespace qe { else if (m_arith.is_ge(lit, e1, e2)) { mk_ge_core(e1, e2, res); } - + // restore negation if (is_neg) { res = mk_not(m, res); } - + return res; } }; @@ -309,16 +311,16 @@ namespace qe { 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)); } - + term_graph::~term_graph() { reset(); } 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); - expr *a = nullptr, *b = nullptr; + expr *a = nullptr, *b = nullptr; // deal with equality using sort of range if (m.is_eq (lit, a, b)) { return get_sort (a)->get_family_id(); @@ -331,10 +333,10 @@ namespace qe { return null_family_id; } } - + void term_graph::add_lit(expr *l) { expr_ref lit(m); - + family_id fid = get_family_id (m, l); term_graph_plugin *pin = m_plugins.get_plugin(fid); if (pin) { @@ -345,16 +347,16 @@ namespace qe { m_lits.push_back(lit); internalize_lit(lit); } - + bool term_graph::is_internalized(expr *a) { return m_app2term.contains(a->get_id()); } - + term* term_graph::get_term(expr *a) { term *res; return m_app2term.find (a->get_id(), res) ? res : nullptr; } - + term *term_graph::mk_term(expr *a) { term * t = alloc(term, a, m_app2term); if (t->get_num_args() == 0 && m.is_unique_value(a)){ @@ -365,8 +367,8 @@ namespace qe { m_app2term.insert(a->get_id(), t); return t; } - - term* term_graph::internalize_term(expr *t) { + + term* term_graph::internalize_term(expr *t) { term* res = get_term(t); if (res) return res; ptr_buffer todo; @@ -381,7 +383,7 @@ namespace qe { unsigned sz = todo.size(); if (is_app(t)) { for (expr * arg : *::to_app(t)) { - if (!get_term(arg)) + if (!get_term(arg)) todo.push_back(arg); } } @@ -392,7 +394,7 @@ namespace qe { SASSERT(res); return res; } - + void term_graph::internalize_eq(expr *a1, expr* a2) { SASSERT(m_merge.empty()); merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root()); @@ -402,7 +404,7 @@ namespace qe { void term_graph::internalize_lit(expr* lit) { expr *e1 = nullptr, *e2 = nullptr; - if (m.is_eq (lit, e1, e2)) { + if (m.is_eq (lit, e1, e2)) { internalize_eq (e1, e2); } else { @@ -422,19 +424,19 @@ namespace qe { void term_graph::merge(term &t1, term &t2) { // -- merge might invalidate term2map cache m_term2app.reset(); - m_pinned.reset(); - + m_pinned.reset(); + SASSERT(t1.is_root()); SASSERT(t2.is_root()); - + if (&t1 == &t2) return; - + term *a = &t1; term *b = &t2; if (a->get_class_size() > b->get_class_size()) { std::swap(a, b); } - + // Remove parents of it from the cg table. for (term* p : term::parents(b)) { if (!p->is_marked()) { @@ -442,15 +444,15 @@ namespace qe { 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); for (term *it = &b->get_next(); it != b; it = &it->get_next()) { it->set_root(*a); } - + // merge equivalence classes a->merge_eq_class(*b); - + // Insert parents of b's old equilvalence class into the cg table for (term* p : term::parents(a)) { if (p->is_marked()) { @@ -462,16 +464,16 @@ namespace qe { m_merge.push_back(std::make_pair(p, p_old)); } } - } + } } - + expr* term_graph::mk_app_core (expr *e) { if (is_app(e)) { - expr_ref_vector kids(m); + expr_ref_vector kids(m); app* a = ::to_app(e); for (expr * arg : *a) { kids.push_back (mk_app(arg)); - } + } app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.c_ptr()); m_pinned.push_back(res); return res; @@ -483,44 +485,44 @@ namespace qe { expr_ref term_graph::mk_app(term const &r) { SASSERT(r.is_root()); - + if (r.get_num_args() == 0) { - return expr_ref(r.get_app(), m); + return expr_ref(r.get_expr(), m); } - + expr* res = nullptr; if (m_term2app.find(r.get_id(), res)) { return expr_ref(res, m); } - + res = mk_app_core (r.get_app()); m_term2app.insert(r.get_id(), res); return expr_ref(res, m); - + } expr_ref term_graph::mk_app(expr *a) { term *t = get_term(a); - if (!t) + if (!t) return expr_ref(a, m); - else + else return mk_app(t->get_root()); - + } void term_graph::mk_equalities(term const &t, expr_ref_vector &out) { SASSERT(t.is_root()); expr_ref rep(mk_app(t), m); - + for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { expr* mem = mk_app_core(it->get_app()); out.push_back (m.mk_eq (rep, mem)); } } - + void term_graph::mk_all_equalities(term const &t, expr_ref_vector &out) { mk_equalities(t, out); - + for (term *it = &t.get_next(); it != &t; it = &it->get_next ()) { expr* a1 = mk_app_core (it->get_app()); for (term *it2 = &it->get_next(); it2 != &t; it2 = &it2->get_next()) { @@ -529,30 +531,32 @@ namespace qe { } } } - + void term_graph::reset_marks() { for (term * t : m_terms) { t->set_mark(false); } } - + /// Order of preference for roots of equivalence classes /// 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 uninterpreted constants over values // prefer smaller expressions over larger ones - if (t1.get_num_args() == 0 && t2.get_num_args() > 0) { - return true; + if (t1.get_num_args() == 0 || t2.get_num_args() == 0) { + 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? - return m.is_value(t2.get_app()); - } - - unsigned sz1 = get_num_exprs(t1.get_app()); - unsigned sz2 = get_num_exprs(t1.get_app()); + + unsigned sz1 = get_num_exprs(t1.get_expr()); + unsigned sz2 = get_num_exprs(t1.get_expr()); return sz1 < sz2; } @@ -560,9 +564,9 @@ namespace qe { term *r = &t; for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { 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 (r != &t) { r->mk_root(); @@ -572,47 +576,47 @@ namespace qe { /// Choose better roots for equivalence classes void term_graph::pick_roots() { for (term* t : m_terms) { - if (!t->is_marked() && t->is_root()) + if (!t->is_marked() && t->is_root()) pick_root(*t); } reset_marks(); } - + void term_graph::display(std::ostream &out) { 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() << " term " << t << "\n"; } } - + void term_graph::to_lits (expr_ref_vector &lits, bool all_equalities) { pick_roots(); - + for (expr * a : m_lits) { if (is_internalized(a)) { lits.push_back (::to_app(mk_app(a))); } } - + for (term * t : m_terms) { - if (!t->is_root()) + if (!t->is_root()) continue; - else if (all_equalities) - mk_all_equalities (*t, lits); - else + else if (all_equalities) + mk_all_equalities (*t, lits); + else mk_equalities(*t, lits); } } - - + + expr_ref term_graph::to_app() { expr_ref_vector lits(m); to_lits(lits); return mk_and(lits); } - + void term_graph::reset() { m_term2app.reset(); m_pinned.reset(); @@ -622,9 +626,10 @@ namespace qe { m_lits.reset(); m_cg_table.reset(); } - + 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 (!is_app(e)) return nullptr; app* a = ::to_app(e); @@ -638,35 +643,35 @@ namespace qe { m_term2app.insert(t.get_id(), result); return result; } - + expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) { u_map _decls; for (func_decl* f : decls) _decls.insert(f->get_id(), true); // . propagate representatives up over parents. // use work-list + marking to propagate. // . 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) - + expr_ref_vector result(m); m_term2app.reset(); m_pinned.reset(); - + obj_hashtable eqs; expr_ref eq(m); ptr_vector worklist; for (term * t : m_terms) { worklist.push_back(t); - t->set_mark(true); + 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())) + if (m_term2app.contains(t->get_id())) continue; - if (!t->is_theory() && exclude == _decls.contains(t->get_decl_id())) + if (!t->is_theory() && exclude == _decls.contains(t->get_decl_id())) continue; term& root = t->get_root(); @@ -675,7 +680,7 @@ namespace qe { if (!pure) continue; // 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 // inheriting pure. expr* rep = nullptr; @@ -691,7 +696,7 @@ namespace qe { } 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 // pure makes a better representative. 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. if (!has_rep || update_rep) { 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)) { result.push_back(e); } - } + } // 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 + // these disequalities are implied and can be mined using other means, such as // theory aware core minimization m_term2app.reset(); m_pinned.reset(); diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 4c2c2c6ff..e32f7271c 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -33,11 +33,11 @@ namespace qe { virtual ~term_graph_plugin() {} family_id get_family_id() const {return m_id;} - + /// Process (and potentially augment) a literal virtual expr_ref process_lit (expr *lit) = 0; }; - + class term_graph { struct term_hash { unsigned operator()(term const* t) const; }; @@ -45,62 +45,62 @@ namespace qe { ast_manager & m; ptr_vector m_terms; expr_ref_vector m_lits; // NSB: expr_ref_vector? - u_map m_app2term; + u_map m_app2term; ast_ref_vector m_pinned; u_map m_term2app; plugin_manager m_plugins; ptr_hashtable m_cg_table; vector> m_merge; - + void merge(term &t1, term &t2); void merge_flush(); - + term *mk_term(expr *t); term *get_term(expr *t); - + term *internalize_term(expr *t); void internalize_eq(expr *a1, expr *a2); void internalize_lit(expr *lit); - + 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_roots(); - + void reset_marks(); - + expr* mk_app_core(expr* a); expr_ref mk_app(term const &t); expr* mk_pure(term& t); expr_ref mk_app(expr *a); void mk_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: term_graph(ast_manager &m); ~term_graph(); - + 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_eq(expr* a, expr* b) { internalize_eq(a, b); } - + void reset(); // deprecate? 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 - * onto the vocabulary of decls (if exclude is false) or outside the + * Return literals obtained by projecting added literals + * onto the vocabulary of decls (if exclude is false) or outside the * vocabulary of decls (if exclude is true). */ expr_ref_vector project(func_decl_ref_vector const& decls, bool exclude); - + }; }