From 771d3b1349a255e2653023cfccf3a862f81d868d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 11 Jun 2018 17:38:14 -0700 Subject: [PATCH] wip: term_graph::project and term_graph::solve --- src/qe/qe_term_graph.cpp | 134 ++++++++++++++++++++++++++++++++------- src/qe/qe_term_graph.h | 43 +++++++------ 2 files changed, 136 insertions(+), 41 deletions(-) diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 4101d6d56..eccb7669f 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -22,6 +22,7 @@ Notes: #include "ast/ast_pp.h" #include "ast/ast_util.h" #include "ast/for_each_expr.h" +#include "ast/occurs.h" #include "qe/qe_term_graph.h" namespace qe { @@ -64,9 +65,9 @@ namespace qe { m_children.push_back(t); } } - + ~term() {} - + class parents { term const& t; public: @@ -167,9 +168,9 @@ namespace qe { 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; @@ -384,7 +385,7 @@ namespace qe { SASSERT(res); return res; } - + void term_graph::internalize_eq(expr *a1, expr* a2) { SASSERT(m_merge.empty()); merge(*internalize_term(a1), *internalize_term(a2)); @@ -414,17 +415,17 @@ namespace qe { void term_graph::merge(term &t1, term &t2) { // -- merge might invalidate term2app cache m_term2app.reset(); - m_pinned.reset(); - + m_pinned.reset(); + term *a = &t1.get_root(); term *b = &t2.get_root(); - + if (a == b) return; - + 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()) { @@ -630,7 +631,9 @@ namespace qe { return result; } - expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) { + void term_graph::project_core(func_decl_ref_vector const& decls, + bool exclude, + expr_ref_vector &result) { u_map _decls; for (func_decl* f : decls) _decls.insert(f->get_id(), true); // - propagate representatives up over parents. @@ -639,10 +642,6 @@ namespace qe { // - 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; @@ -666,7 +665,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; @@ -682,7 +681,10 @@ namespace qe { } bool update_rep = false; - // Add equations between pure and rep, + // AG: can rep be null at this point? + // AG: why mk_pure(root) is guaranteed to return non-null? + + // Add equations between pure and rep, // optionally swap the roles of rep and pure if // pure makes a better representative. if (rep != pure) { @@ -697,7 +699,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)) { @@ -709,19 +711,107 @@ namespace qe { } } } + // 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 + reset_marks(); + } + + expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) { + expr_ref_vector result(m); + m_term2app.reset(); + m_pinned.reset(); + project_core(decls, exclude, result); // walk other predicates than equalities for (expr* e : m_lits) { 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 - // theory aware core minimization + m_term2app.reset(); m_pinned.reset(); + return result; + } + + bool term_graph::is_solved_eq(expr *_lhs, expr* _rhs) { + if (!is_app(_lhs) || !is_app(_rhs)) return false; + app *lhs, *rhs; + lhs = ::to_app(_lhs); + rhs = ::to_app(_rhs); + + if (rhs->get_num_args() > 0) return false; + if (rhs->get_family_id() != null_family_id) return false; + + return !occurs(rhs, lhs); + } + void term_graph::solve_core(func_decl_ref_vector const &decls, bool exclude, + expr_ref_vector &result) { + u_map _decls; + for (func_decl* f : decls) _decls.insert(f->get_id(), true); + obj_hashtable eqs; + expr_ref eq(m); + ptr_vector worklist; + for (term * t : 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; + term &root = t->get_root(); + bool has_rep = m_term2app.contains(root.get_id()); + expr *pure = mk_pure(*t); + if (!pure) continue; + + if (has_rep) { + // add equality if needed + expr* rep = m_term2app.find(root.get_id()); + if (exclude != _decls.contains(t->get_decl_id()) || !is_solved_eq(rep, pure)) { + eq = m.mk_eq(rep, pure); + if (!eqs.contains(eq)) { + eqs.insert(eq); + result.push_back(eq); + } + } + } + else { + // let pure be the representative + m_term2app.insert(root.get_id(), pure); + // schedule parents of root to be processed again + for (term * p : term::parents(root)) { + if (!p->is_marked()) { + p->set_mark(true); + worklist.push_back(p); + } + } + SASSERT(false); + // TBD: deal with root + } + } + reset_marks(); + } + + + expr_ref_vector term_graph::solve(func_decl_ref_vector const &decls, bool exclude) { + expr_ref_vector result(m); + m_term2app.reset(); + m_pinned.reset(); + project_core(decls, exclude, result); + solve_core(decls, exclude, result); + // walk other predicates than equalities + for (expr* e : m_lits) { + if (!m.is_eq(e) && m_term2app.find(get_term(e)->get_root().get_id(), e)) { + result.push_back(e); + } + } + m_term2app.reset(); + m_pinned.reset(); return result; } diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index fbb2ceb16..f3564f0e9 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,67 @@ 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_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); + void project_core(func_decl_ref_vector const &decls, bool exclude, expr_ref_vector &result); + void solve_core(func_decl_ref_vector const &decls, bool exclude, expr_ref_vector &result); + bool is_solved_eq(expr *lhs, expr *rhs); 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); - + expr_ref_vector solve(func_decl_ref_vector const& decls, bool exclude); + + }; }