From 008f003aa0e575fefa42ad8dd20f11aecf6b12b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jun 2018 20:58:41 -0700 Subject: [PATCH] initial working version Signed-off-by: Nikolaj Bjorner --- src/cmd_context/extra_cmds/dbg_cmds.cpp | 1 + src/qe/qe_term_graph.cpp | 832 ++++++++++++------------ src/qe/qe_term_graph.h | 9 +- 3 files changed, 438 insertions(+), 404 deletions(-) diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 534e3740b..bedbf84aa 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -503,4 +503,5 @@ void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(set_next_id)); ctx.insert(alloc(mbp_cmd)); ctx.insert(alloc(mbi_cmd)); + ctx.insert(alloc(euf_project_cmd)); } diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 03d2f082e..5e8c22919 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -26,83 +26,80 @@ Notes: namespace qe { -class term { - // -- an app represented by this term - expr* m_app; // 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), - m_next(this), - m_class_size(1), - m_mark(false), - m_mark2(false), - m_interpreted(false) { - if (!is_app(a)) return; - for (expr* e : *to_app(a)) { - term* t = app2term[e->get_id()]; - t->m_parents.push_back(this); - m_children.push_back(t); + class term { + // -- an app represented by this term + expr* m_app; // 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), + m_next(this), + m_class_size(1), + m_mark(false), + m_mark2(false), + m_interpreted(false) { + if (!is_app(a)) return; + for (expr* e : *to_app(a)) { + term* t = app2term[e->get_id()]; + t->m_parents.push_back(this); + m_children.push_back(t); + } } - } - - ~term() {} - - class parents { + + ~term() {} + + class parents { + term const& t; + public: + parents(term const& _t):t(_t) {} + parents(term const* _t):t(*_t) {} + 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: - parents(term const& _t):t(_t) {} - parents(term const* _t):t(*_t) {} - 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: - children(term const& _t):t(_t) {} - children(term const* _t):t(*_t) {} - 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. - - struct cg_hash { - unsigned operator()(term const* t) const { + public: + children(term const& _t):t(_t) {} + children(term const* _t):t(*_t) {} + 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 = t->get_decl_id(); - for (term * ch : children(t)) { + a = b = c = get_decl_id(); + for (term * ch : children(this)) { a = ch->get_root().get_id(); mix(a, b, c); } return c; } - }; - - struct cg_eq { - bool operator()(term * t1, term * t2) const { + + 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; for (unsigned i = 0, sz = t1->m_children.size(); i < sz; ++ i) { @@ -110,348 +107,378 @@ public: } 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(); } + + 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;} + 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; } + + 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()) { + // found previous root + SASSERT(curr != this); + m_class_size = curr->get_class_size(); + curr->m_class_size = 0; + } + curr->set_root(*this); + curr = &curr->get_next(); + } + 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, app_ref &res) { + expr *e1, *e2; + e1 = _e1; + e2 = _e2; + + if (m_arith.is_zero(e1)) { + std::swap(e1, e2); + } + // y + -1*x == 0 --> y = x + expr *a0 = 0, *a1 = 0, *x = 0; + if (m_arith.is_zero(e2) && m_arith.is_add(e1, a0, a1)) { + if (m_arith.is_times_minus_one(a1, x)) { + e1 = a0; + e2 = x; + } + else if (m_arith.is_times_minus_one(a0, x)) { + e1 = a1; + e2 = x; + } + } + res = m.mk_eq(e1, e2); + return true; + } + + app* mk_le_zero(expr *arg) { + expr *e1, *e2, *e3; + // XXX currently disabled + if (m_arith.is_add(arg, e1, e2)) { + // e1-e2<=0 --> e1<=e2 + if (m_arith.is_times_minus_one(e2, e3)) { + return m_arith.mk_le(e1, e3); + } + // -e1+e2<=0 --> e2<=e1 + else if (m_arith.is_times_minus_one(e1, e3)) { + return m_arith.mk_le(e2, e3); + } + } + return m_arith.mk_le(arg, mk_zero()); + } + + app* mk_ge_zero(expr *arg) { + expr *e1, *e2, *e3; + // XXX currently disabled + if (m_arith.is_add(arg, e1, e2)) { + // e1-e2>=0 --> e1>=e2 + if (m_arith.is_times_minus_one(e2, e3)) { + return m_arith.mk_ge(e1, e3); + } + // -e1+e2>=0 --> e2>=e1 + else if (m_arith.is_times_minus_one(e1, e3)) { + return m_arith.mk_ge(e2, e3); + } + } + return m_arith.mk_ge(arg, mk_zero()); + } + + bool mk_le_core (expr *arg1, expr * arg2, app_ref &result) { + // t <= -1 ==> t < 0 ==> ! (t >= 0) + rational n; + if (m_arith.is_int (arg1) && m_arith.is_minus_one (arg2)) { + result = m.mk_not (mk_ge_zero (arg1)); + return true; + } + else if (m_arith.is_zero(arg2)) { + result = mk_le_zero(arg1); + return true; + } + else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n < 0) { + // t <= n ==> t < n + 1 ==> ! (t >= n + 1) + result = m.mk_not(m_arith.mk_ge(arg1, m_arith.mk_numeral(n+1, true))); + return true; + } + 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, app_ref &result) { + // t >= 1 ==> t > 0 ==> ! (t <= 0) + rational n; + if (m_arith.is_int (arg1) && is_one (arg2)) { + result = m.mk_not (mk_le_zero (arg1)); + return true; + } + else if (m_arith.is_zero(arg2)) { + result = mk_ge_zero(arg1); + return true; + } + else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n > 0) { + // t >= n ==> t > n - 1 ==> ! (t <= n - 1) + result = m.mk_not(m_arith.mk_le(arg1, m_arith.mk_numeral(n-1, true))); + return true; + } + return false; + } + + virtual app_ref process_lit (app *_lit) { + app *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)); + } + + app_ref res(m); + res = lit; + if (m.is_eq (lit, e1, e2)) { + mk_eq_core(e1, e2, res); + } + else if (m_arith.is_le(lit, e1, e2)) { + mk_le_core(e1, e2, res); + } + else if (m_arith.is_ge(lit, e1, e2)) { + mk_ge_core(e1, e2, res); + } + + // restore negation + if (is_neg) { + res = m.mk_not(res); + } + + return res; + } }; - unsigned get_id() const { return m_app->get_id();} + unsigned term_graph::term_hash::operator()(term const* t) const { return t->get_hash(); } - unsigned get_decl_id() const { return is_app(m_app) ? to_app(m_app)->get_decl()->get_id() : m_app->get_id(); } + bool term_graph::term_eq::operator()(term const* a, term const* b) const { return term::cg_eq(a, b); } - 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;} - 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; } - - 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;} - - 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; + 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)); } - - // -- make this term the root of its equivalence class - void mk_root() { - if (is_root()) return; - - term *curr = this; - do { - if (curr->is_root()) { - // found previous root - SASSERT(curr != this); - m_class_size = curr->get_class_size(); - curr->m_class_size = 0; - } - curr->set_root(*this); - curr = &curr->get_next(); - } - 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, app_ref &res) { - expr *e1, *e2; - e1 = _e1; - e2 = _e2; - - if (m_arith.is_zero(e1)) { - std::swap(e1, e2); - } - // y + -1*x == 0 --> y = x - expr *a0 = 0, *a1 = 0, *x = 0; - if (m_arith.is_zero(e2) && m_arith.is_add(e1, a0, a1)) { - if (m_arith.is_times_minus_one(a1, x)) { - e1 = a0; - e2 = x; - } - else if (m_arith.is_times_minus_one(a0, x)) { - e1 = a1; - e2 = x; - } - } - res = m.mk_eq(e1, e2); - return true; - } - - app* mk_le_zero(expr *arg) { - expr *e1, *e2, *e3; - // XXX currently disabled - if (m_arith.is_add(arg, e1, e2)) { - // e1-e2<=0 --> e1<=e2 - if (m_arith.is_times_minus_one(e2, e3)) { - return m_arith.mk_le(e1, e3); - } - // -e1+e2<=0 --> e2<=e1 - else if (m_arith.is_times_minus_one(e1, e3)) { - return m_arith.mk_le(e2, e3); - } - } - return m_arith.mk_le(arg, mk_zero()); - } - - app* mk_ge_zero(expr *arg) { - expr *e1, *e2, *e3; - // XXX currently disabled - if (m_arith.is_add(arg, e1, e2)) { - // e1-e2>=0 --> e1>=e2 - if (m_arith.is_times_minus_one(e2, e3)) { - return m_arith.mk_ge(e1, e3); - } - // -e1+e2>=0 --> e2>=e1 - else if (m_arith.is_times_minus_one(e1, e3)) { - return m_arith.mk_ge(e2, e3); - } - } - return m_arith.mk_ge(arg, mk_zero()); - } - - bool mk_le_core (expr *arg1, expr * arg2, app_ref &result) { - // t <= -1 ==> t < 0 ==> ! (t >= 0) - rational n; - if (m_arith.is_int (arg1) && m_arith.is_minus_one (arg2)) { - result = m.mk_not (mk_ge_zero (arg1)); - return true; - } - else if (m_arith.is_zero(arg2)) { - result = mk_le_zero(arg1); - return true; - } - else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n < 0) { - // t <= n ==> t < n + 1 ==> ! (t >= n + 1) - result = m.mk_not(m_arith.mk_ge(arg1, m_arith.mk_numeral(n+1, true))); - return true; - } - 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, app_ref &result) { - // t >= 1 ==> t > 0 ==> ! (t <= 0) - rational n; - if (m_arith.is_int (arg1) && is_one (arg2)) { - result = m.mk_not (mk_le_zero (arg1)); - return true; - } - else if (m_arith.is_zero(arg2)) { - result = mk_ge_zero(arg1); - return true; - } - else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n > 0) { - // t >= n ==> t > n - 1 ==> ! (t <= n - 1) - result = m.mk_not(m_arith.mk_le(arg1, m_arith.mk_numeral(n-1, true))); - return true; - } - return false; - } - - virtual app_ref process_lit (app *_lit) { - app *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)); - } - - app_ref res(m); - res = lit; - if (m.is_eq (lit, e1, e2)) { - mk_eq_core(e1, e2, res); - } - else if (m_arith.is_le(lit, e1, e2)) { - mk_le_core(e1, e2, res); - } - else if (m_arith.is_ge(lit, e1, e2)) { - mk_ge_core(e1, e2, res); - } - - // restore negation - if (is_neg) { - res = m.mk_not(res); - } - - return res; - } -}; - -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, app *lit) { - family_id fid = null_family_id; - - expr *e1 = nullptr, *e2 = nullptr, *e3 = nullptr; - // strip negation - if (!m.is_not (lit, e1)) { e1 = lit; } - - // deal with equality using sort of range - if (m.is_eq (e1, e2, e3)) { - fid = get_sort (e2)->get_family_id(); - } - // extract family_id of top level app - else { - fid = to_app(e1)->get_decl()->get_family_id(); - } - - return fid; -} - -void term_graph::add_lit(app *l) { - app_ref lit(m); - - family_id fid = get_family_id (m, l); - term_graph_plugin *pin = m_plugins.get_plugin(fid); - if (pin) { - lit = pin->process_lit(l); - } else { - lit = l; - } - 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)){ - t->mark_as_interpreted(); - } - - m_terms.push_back(t); - m_app2term.insert(a->get_id(), t); - return t; -} - -term* term_graph::internalize_term(expr *t) { - term* res = get_term(t); - if (res) return res; - ptr_buffer todo; - todo.push_back(t); - while (!todo.empty()) { + term_graph::~term_graph() { + reset(); + } + + static family_id get_family_id(ast_manager &m, app *lit) { + family_id fid = null_family_id; + + expr *e1 = nullptr, *e2 = nullptr, *e3 = nullptr; + // strip negation + if (!m.is_not (lit, e1)) { e1 = lit; } + + // deal with equality using sort of range + if (m.is_eq (e1, e2, e3)) { + fid = get_sort (e2)->get_family_id(); + } + // extract family_id of top level app + else { + fid = to_app(e1)->get_decl()->get_family_id(); + } + + return fid; + } + + void term_graph::add_lit(app *l) { + app_ref lit(m); + + family_id fid = get_family_id (m, l); + term_graph_plugin *pin = m_plugins.get_plugin(fid); + if (pin) { + lit = pin->process_lit(l); + } else { + lit = l; + } + 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)){ + t->mark_as_interpreted(); + } + + m_terms.push_back(t); + m_app2term.insert(a->get_id(), t); + return t; + } + + term* term_graph::internalize_term(expr *t) { term* res = get_term(t); - if (res) { - todo.pop_back(); - continue; - } - unsigned sz = todo.size(); - if (is_app(t)) { - for (expr * arg : *::to_app(t)) { - if (!get_term(arg)) - todo.push_back(arg); + if (res) return res; + ptr_buffer todo; + todo.push_back(t); + while (!todo.empty()) { + res = get_term(t); + if (res) { + todo.pop_back(); + continue; } + unsigned sz = todo.size(); + if (is_app(t)) { + for (expr * arg : *::to_app(t)) { + if (!get_term(arg)) + todo.push_back(arg); + } + } + if (sz < todo.size()) continue; + todo.pop_back(); + res = mk_term(t); } - if (sz < todo.size()) continue; - todo.pop_back(); - res = mk_term(t); - } - return res; -} - -void term_graph::internalize_eq(expr *a1, expr* a2) { - merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root()); -} - -void term_graph::internalize_lit(expr* lit) { - expr *e1 = nullptr, *e2 = nullptr; - if (m.is_eq (lit, e1, e2)) { - internalize_eq (e1, e2); - } - else { - internalize_term(lit); - } -} - -void term_graph::merge (term &t1, term &t2) { - 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); - } - - // 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()) { - // TBD: remove parents of it from the cg table. - it->set_root(*a); - } - - // merge equivalence classes - a->merge_eq_class(*b); - - // TBD: insert parents of b's old equilvalence class into the cg table - // and propagate equalities. - - // -- merge might have invalidated term2map cache - - // NSB: ??? what is ownership model of pinned in m_terms? - m_term2app.reset(); - m_pinned.reset(); -} - -expr* term_graph::mk_app_core (expr *e) { - if (is_app(e)) { - 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); + SASSERT(res); return res; } - else { - return e; + + void term_graph::internalize_eq(expr *a1, expr* a2) { + SASSERT(m_merge.empty()); + merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root()); + merge_flush(); + SASSERT(m_merge.empty()); + } + + void term_graph::internalize_lit(expr* lit) { + expr *e1 = nullptr, *e2 = nullptr; + if (m.is_eq (lit, e1, e2)) { + internalize_eq (e1, e2); + } + else { + internalize_term(lit); + } + } + + void term_graph::merge_flush() { + while (!m_merge.empty()) { + term* t1 = m_merge.back().first; + term* t2 = m_merge.back().second; + m_merge.pop_back(); + merge(*t1, *t2); + } + } + + void term_graph::merge(term &t1, term &t2) { + // -- merge might invalidate term2map cache + m_term2app.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()) { + p->set_mark(true); + m_cg_table.erase(p); + } + } + // 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()) { + term* p_old = m_cg_table.insert_if_not_there(p); + p->set_mark(false); + a->add_parent(p); + // propagate new equalities. + if (p->get_root().get_id() != p_old->get_root().get_id()) { + 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); + 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; + } + else { + return e; + } } -} expr_ref term_graph::mk_app(term const &r) { SASSERT(r.is_root()); @@ -598,6 +625,7 @@ void term_graph::reset() { std::for_each(m_terms.begin(), m_terms.end(), delete_proc()); m_terms.reset(); m_lits.reset(); + m_cg_table.reset(); } expr_ref term_graph::mk_pure(term& t) { @@ -631,7 +659,7 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl if (t->get_root().is_marked()) continue; // if exclude = true, but t in decls, then skip // if exclude = false, but t not in decls, then skip - if (exclude != _decls.contains(t->get_decl_id())) { + if (exclude == _decls.contains(t->get_decl_id())) { continue; } // @@ -662,7 +690,7 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl // walk each root. Then traverse each term in the equivalence class // create pure variant of the terms (if possible) // equate t0 (that comes from the root, which can be purified) - // with any other t1. + // with any other purifiable t1. expr_ref_vector result(m); m_term2app.reset(); m_pinned.reset(); @@ -675,7 +703,7 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl roots.insert(t0); for (term* r = &t->get_next(); r != t; r = &r->get_next()) { // main symbol of term must be consistent with what is included/excluded - if (exclude != _decls.contains(r->get_decl_id())) { + if (exclude == _decls.contains(r->get_decl_id())) { continue; } expr_ref t1 = mk_pure(*r); diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 8e8f54c8c..c3f1e21aa 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -37,18 +37,23 @@ namespace qe { /// Process (and potentially augment) a literal virtual app_ref process_lit (app *lit) = 0; }; - + + class term_graph { + struct term_hash { unsigned operator()(term const* t) const; }; + struct term_eq { bool operator()(term const* a, term const* b) const; }; ast_manager & m; ptr_vector m_terms; app_ref_vector m_lits; // NSB: expr_ref_vector? 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);