From 65e6d942ac013ef9e3c88022d79de051f089f717 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2020 01:55:13 -0700 Subject: [PATCH] euf Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 3 +- src/CMakeLists.txt | 1 + src/api/c++/z3++.h | 4 +- src/ast/euf/CMakeLists.txt | 9 + src/ast/euf/euf_egraph.cpp | 302 ++++++++++++++++++++++++++++++++ src/ast/euf/euf_egraph.h | 109 ++++++++++++ src/ast/euf/euf_enode.cpp | 101 +++++++++++ src/ast/euf/euf_enode.h | 154 ++++++++++++++++ src/ast/euf/euf_etable.cpp | 252 ++++++++++++++++++++++++++ src/ast/euf/euf_etable.h | 217 +++++++++++++++++++++++ src/ast/euf/euf_justification.h | 59 +++++++ src/sat/tactic/CMakeLists.txt | 1 + src/sat/tactic/goal2sat.cpp | 30 +++- src/smt/mam.h | 3 + src/smt/smt_context.cpp | 5 +- src/smt/smt_context.h | 4 - src/smt/smt_enode.h | 21 --- src/smt/smt_justification.h | 1 + src/smt/smt_quantifier.h | 1 + src/smt/smt_types.h | 2 - src/test/CMakeLists.txt | 1 + src/test/egraph.cpp | 96 ++++++++++ src/test/main.cpp | 1 + 23 files changed, 1338 insertions(+), 39 deletions(-) create mode 100644 src/ast/euf/CMakeLists.txt create mode 100644 src/ast/euf/euf_egraph.cpp create mode 100644 src/ast/euf/euf_egraph.h create mode 100644 src/ast/euf/euf_enode.cpp create mode 100644 src/ast/euf/euf_enode.h create mode 100644 src/ast/euf/euf_etable.cpp create mode 100644 src/ast/euf/euf_etable.h create mode 100644 src/ast/euf/euf_justification.h create mode 100644 src/test/egraph.cpp diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 4040af0dc..3d041b126 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -23,6 +23,7 @@ def init_project_def(): add_lib('realclosure', ['interval'], 'math/realclosure') add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('ast', ['util', 'polynomial']) + add_lib('euf' ['ast','util'], 'ast/euf') add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner') add_lib('sat', ['util','dd', 'grobner']) add_lib('nlsat', ['polynomial', 'sat']) @@ -79,7 +80,7 @@ def init_project_def(): includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'qe', 'arith_tactics'], 'cmd_context/extra_cmds') add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3') - add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False) + add_exe('test', ['api', 'fuzzing', 'simplex', 'euf'], exe_name='test-z3', install=False) _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', reexports=['api'], dll_name='libz3', diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f8e8c53b1..5e1ea8f51 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -49,6 +49,7 @@ add_subdirectory(ast/normal_forms) add_subdirectory(model) add_subdirectory(tactic) add_subdirectory(ast/substitution) +add_subdirectory(ast/euf) add_subdirectory(parsers/util) add_subdirectory(math/grobner) add_subdirectory(sat) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9ee9edba1..1e297cf05 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3733,7 +3733,9 @@ namespace z3 { Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, 0, nullptr, nullptr, conseq); } - void propagate(unsigned num_fixed, unsigned const* fixed, unsigned num_eqs, unsigned const* lhs, unsigned const * rhs, expr const& conseq) { + void propagate(unsigned num_fixed, unsigned const* fixed, + unsigned num_eqs, unsigned const* lhs, unsigned const * rhs, + expr const& conseq) { assert(cb); assert(conseq.ctx() == ctx()); Z3_solver_propagate_consequence(ctx(), cb, num_fixed, fixed, num_eqs, lhs, rhs, conseq); diff --git a/src/ast/euf/CMakeLists.txt b/src/ast/euf/CMakeLists.txt new file mode 100644 index 000000000..8d3fa2e74 --- /dev/null +++ b/src/ast/euf/CMakeLists.txt @@ -0,0 +1,9 @@ +z3_add_component(euf + SOURCES + euf_enode.cpp + euf_etable.cpp + euf_egraph.cpp + COMPONENT_DEPENDENCIES + ast + util +) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp new file mode 100644 index 000000000..020e50440 --- /dev/null +++ b/src/ast/euf/euf_egraph.cpp @@ -0,0 +1,302 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + euf_egraph.cpp + +Abstract: + + E-graph layer + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-23 + +--*/ + +#include "ast/euf/euf_egraph.h" + +namespace euf { + + void egraph::undo_eq(enode* r1, enode* n1, unsigned r2_num_parents) { + enode* r2 = r1->get_root(); + r2->dec_class_size(r1->class_size()); + std::swap(r1->m_next, r2->m_next); + auto begin = r2->begin_parents() + r2_num_parents, end = r2->end_parents(); + for (auto it = begin; it != end; ++it) + m_table.erase(*it); + for (enode* c : enode_class(r1)) + c->m_root = r1; + for (auto it = begin; it != end; ++it) + m_table.insert(*it); + r2->m_parents.shrink(r2_num_parents); + unmerge_justification(n1); + } + + enode* egraph::mk_enode(expr* f, enode * const* args) { + unsigned num_args = is_app(f) ? to_app(f)->get_num_args() : 0; + enode* n = enode::mk(m_region, f, num_args, args); + m_nodes.push_back(n); + m_exprs.push_back(f); + return n; + } + + void egraph::reinsert(enode* n) { + unsigned num_parents = n->m_parents.size(); + for (unsigned i = 0; i < num_parents; ++i) { + enode* p = n->m_parents[i]; + if (is_equality(p)) { + reinsert_equality(p); + } + else { + auto rc = m_table.insert(p); + merge(rc.first, p, justification::congruence(rc.second)); + if (inconsistent()) + break; + } + } + } + + void egraph::reinsert_equality(enode* p) { + if (p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) + m_new_eqs.push_back(p); + } + + bool egraph::is_equality(enode* p) const { + return m.is_eq(p->get_owner()); + } + + void egraph::dedup_equalities() { + unsigned j = 0; + for (enode* p : m_new_eqs) { + if (!p->is_marked1()) + m_new_eqs[j++] = p; + p->mark1(); + } + for (enode* p : m_new_eqs) + p->unmark1(); + m_new_eqs.shrink(j); + } + + void egraph::force_push() { + for (; m_num_scopes > 0; --m_num_scopes) { + scope s; + s.m_inconsistent = m_inconsistent; + s.m_num_eqs = m_eqs.size(); + s.m_num_nodes = m_nodes.size(); + m_scopes.push_back(s); + m_region.push_scope(); + } + } + + void egraph::update_children(enode* n) { + for (enode* child : enode_args(n)) + child->get_root()->add_parent(n); + n->set_update_children(); + } + + enode* egraph::mk(expr* f, enode *const* args) { + SASSERT(!find(f)); + force_push(); + enode *n = mk_enode(f, args); + SASSERT(n->class_size() == 1); + m_expr2enode.setx(f->get_id(), n, nullptr); + if (n->num_args() == 0 && m.is_unique_value(f)) + n->mark_interpreted(); + if (n->num_args() == 0) + return n; + if (is_equality(n)) { + update_children(n); + return n; + } + enode_bool_pair p = m_table.insert(n); + enode* r = p.first; + if (r == n) { + update_children(n); + } + else { + SASSERT(r->get_owner() != n->get_owner()); + merge_justification(n, r, justification::congruence(p.second)); + std::swap(n->m_next, r->m_next); + n->m_root = r; + r->inc_class_size(n->class_size()); + push_eq(n, n, r->num_parents()); + } + return n; + } + + void egraph::pop(unsigned num_scopes) { + if (num_scopes <= m_num_scopes) { + m_num_scopes -= num_scopes; + return; + } + num_scopes -= m_num_scopes; + unsigned old_lim = m_scopes.size() - num_scopes; + scope s = m_scopes[old_lim]; + for (unsigned i = m_eqs.size(); i-- > s.m_num_eqs; ) { + auto const& p = m_eqs[i]; + undo_eq(p.r1, p.n1, p.r2_num_parents); + } + for (unsigned i = m_nodes.size(); i-- > s.m_num_nodes; ) { + enode* n = m_nodes[i]; + if (n->num_args() > 1) + m_table.erase(n); + m_expr2enode[n->get_owner_id()] = nullptr; + n->~enode(); + } + m_inconsistent = s.m_inconsistent; + m_eqs.shrink(s.m_num_eqs); + m_nodes.shrink(s.m_num_nodes); + m_exprs.shrink(s.m_num_nodes); + m_scopes.shrink(old_lim); + m_region.pop_scope(num_scopes); + } + + void egraph::merge(enode* n1, enode* n2, justification j) { + SASSERT(m.get_sort(n1->get_owner()) == m.get_sort(n2->get_owner())); + TRACE("euf", tout << n1->get_owner_id() << " == " << n2->get_owner_id() << "\n";); + force_push(); + enode* r1 = n1->get_root(); + enode* r2 = n2->get_root(); + if (r1 == r2) + return; + if (r1->interpreted() && r2->interpreted()) { + set_conflict(r1, r2, j); + return; + } + if ((r1->class_size() > r2->class_size() && !r1->interpreted()) || r2->interpreted()) { + std::swap(r1, r2); + std::swap(n1, n2); + } + for (enode* p : enode_parents(n1)) + m_table.erase(p); + for (enode* p : enode_parents(n2)) + m_table.erase(p); + push_eq(r1, n1, r2->num_parents()); + merge_justification(n1, n2, j); + for (enode* c : enode_class(n1)) + c->m_root = r2; + std::swap(r1->m_next, r2->m_next); + r2->inc_class_size(r1->class_size()); + r2->m_parents.append(r1->m_parents); + m_worklist.push_back(r2); + } + + void egraph::propagate() { + m_new_eqs.reset(); + SASSERT(m_num_scopes == 0 || m_worklist.empty()); + unsigned head = 0, tail = m_worklist.size(); + while (head < tail && m.limit().inc() && !inconsistent()) { + TRACE("euf", tout << "iterate: " << head << " " << tail << "\n";); + for (unsigned i = head; i < tail && !inconsistent(); ++i) { + enode* n = m_worklist[i]->get_root(); + if (!n->is_marked1()) { + n->mark1(); + m_worklist[i] = n; + reinsert(n); + } + } + for (unsigned i = head; i < tail; ++i) + m_worklist[i]->unmark1(); + head = tail; + tail = m_worklist.size(); + } + m_worklist.reset(); + dedup_equalities(); + } + + void egraph::set_conflict(enode* n1, enode* n2, justification j) { + if (m_inconsistent) + return; + m_inconsistent = true; + m_n1 = n1; + m_n2 = n2; + m_justification = j; + } + + void egraph::merge_justification(enode* n1, enode* n2, justification j) { + SASSERT(n1->reaches(n1->get_root())); + n1->reverse_justification(); + n1->m_target = n2; + n1->m_justification = j; + SASSERT(n1->get_root()->reaches(n1)); + } + + void egraph::unmerge_justification(enode* n1) { + // r1 -> .. -> n1 -> n2 -> ... -> r2 + // where n2 = n1->m_target + SASSERT(n1->get_root()->reaches(n1)); + n1->m_target = nullptr; + n1->m_justification = justification::axiom(); + n1->get_root()->reverse_justification(); + // --------------- + // n1 -> ... -> r1 + // n2 -> ... -> r2 + SASSERT(n1->reaches(n1->get_root())); + SASSERT(n1->get_root()->m_target == nullptr); + } + + template + void egraph::explain(ptr_vector& justifications) { + SASSERT(m_inconsistent); + SASSERT(m_todo.empty()); + m_todo.push_back(m_n1); + m_todo.push_back(m_n2); + auto push_congruence = [&](enode* p, enode* q) { + SASSERT(p->get_decl() == q->get_decl()); + for (enode* arg : enode_args(p)) + m_todo.push_back(arg); + for (enode* arg : enode_args(q)) + m_todo.push_back(arg); + }; + auto explain_node = [&](enode* n) { + if (!n->m_target) + return; + if (n->is_marked1()) + return; + n->mark1(); + if (n->m_justification.is_external()) + justifications.push_back(n->m_justification.ext()); + else if (n->m_justification.is_congruence()) + push_congruence(n, n->m_target); + n = n->m_target; + if (!n->is_marked1()) + m_todo.push_back(n); + }; + if (m_justification.is_external()) + justifications.push_back(m_justification.ext()); + for (unsigned i = 0; i < m_todo.size(); ++i) + explain_node(m_todo[i]); + for (enode* n : m_todo) + n->unmark1(); + } + + void egraph::invariant() { + for (enode* n : m_nodes) + n->invariant(); + } + + std::ostream& egraph::display(std::ostream& out) const { + m_table.display(out); + for (enode* n : m_nodes) { + out << std::setw(5) + << n->get_owner_id() << " := "; + out << n->get_root()->get_owner_id() << " "; + expr* f = n->get_owner(); + if (is_app(f)) + out << to_app(f)->get_decl()->get_name() << " "; + else if (is_quantifier(f)) + out << "q "; + else + out << "v "; + for (enode* arg : enode_args(n)) + out << arg->get_owner_id() << " "; + out << std::setw(20) << " parents: "; + for (enode* p : enode_parents(n)) + out << p->get_owner_id() << " "; + out << "\n"; + } + return out; + } +} diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h new file mode 100644 index 000000000..327023850 --- /dev/null +++ b/src/ast/euf/euf_egraph.h @@ -0,0 +1,109 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + euf_egraph.h + +Abstract: + + E-graph layer + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-23 + +Notes: + + It relies on + - data structures form the (legacy) SMT solver. + - it still uses eager path compression. + - delayed congruence table reconstruction from egg. + - it does not deduplicate parents. + +--*/ + +#pragma once +#include "ast/euf/euf_enode.h" +#include "ast/euf/euf_etable.h" + +namespace euf { + + struct add_eq_record { + enode* r1; + enode* n1; + unsigned r2_num_parents; + add_eq_record(enode* r1, enode* n1, unsigned r2_num_parents): + r1(r1), n1(n1), r2_num_parents(r2_num_parents) {} + }; + + class egraph { + struct scope { + bool m_inconsistent; + unsigned m_num_eqs; + unsigned m_num_nodes; + }; + ast_manager& m; + region m_region; + enode_vector m_worklist; + etable m_table; + svector m_eqs; + svector m_scopes; + enode_vector m_expr2enode; + enode_vector m_nodes; + expr_ref_vector m_exprs; + unsigned m_num_scopes { 0 }; + bool m_inconsistent { false }; + enode *m_n1 { nullptr }; + enode *m_n2 { nullptr }; + justification m_justification; + enode_vector m_new_eqs; + enode_vector m_todo; + + void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) { + m_eqs.push_back(add_eq_record(r1, n1, r2_num_parents)); + } + void undo_eq(enode* r1, enode* n1, unsigned r2_num_parents); + enode* mk_enode(expr* f, enode * const* args); + void reinsert(enode* n); + void force_push(); + void set_conflict(enode* n1, enode* n2, justification j); + void merge(enode* n1, enode* n2, justification j); + void merge_justification(enode* n1, enode* n2, justification j); + void unmerge_justification(enode* n1); + void dedup_equalities(); + bool is_equality(enode* n) const; + void reinsert_equality(enode* p); + void update_children(enode* n); + public: + egraph(ast_manager& m): m(m), m_table(m), m_exprs(m) {} + enode* find(expr* f) { return m_expr2enode.get(f->get_id(), nullptr); } + enode* mk(expr* f, enode *const* args); + void push() { ++m_num_scopes; } + void pop(unsigned num_scopes); + /** + \brief merge nodes, all effects are deferred to the propagation step. + */ + void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); } + + /** + \brief propagate set of merges. + This call may detect an inconsistency. Then inconsistent() is true. + Use then explain() to extract an explanation for the conflict. + + It may also infer new implied equalities, when the roots of the + equated nodes are merged. Use then new_eqs() to extract the vector + of new equalities. + */ + void propagate(); + bool inconsistent() const { return m_inconsistent; } + enode_vector const& new_eqs() const { return m_new_eqs; } + template + void explain(ptr_vector& justifications); + + void invariant(); + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, egraph const& g) { return g.display(out); } +} diff --git a/src/ast/euf/euf_enode.cpp b/src/ast/euf/euf_enode.cpp new file mode 100644 index 000000000..a9c101afe --- /dev/null +++ b/src/ast/euf/euf_enode.cpp @@ -0,0 +1,101 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + euf_enode.cpp + +Abstract: + + enode layer + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-23 + +--*/ + +#include "ast/euf/euf_enode.h" + +#pragma once + +namespace euf { + + void enode::invariant() { + unsigned class_size = 0; + bool found_root = false; + bool found_this = false; + for (enode* c : enode_class(this)) { + VERIFY(c->m_root == m_root); + found_root |= c == m_root; + found_this |= c == this; + } + VERIFY(found_root); + VERIFY(found_this); + VERIFY(this != m_root || class_size == m_class_size); + if (this == m_root) { + for (enode* p : enode_parents(this)) { + bool found = false; + for (enode* arg : enode_args(p)) { + found |= arg->get_root() == this; + } + VERIFY(found); + } + for (enode* c : enode_class(this)) { + if (c == this) + continue; + for (enode* p : enode_parents(c)) { + bool found = false; + for (enode* q : enode_parents(this)) { + found |= p->congruent(q); + } + VERIFY(found); + } + } + } + } + + bool enode::congruent(enode* n) const { + if (get_decl() != n->get_decl()) + return false; + if (num_args() != n->num_args()) + return false; + SASSERT(!m_commutative || num_args() == 2); + if (m_commutative && + get_arg(0)->get_root() == n->get_arg(1)->get_root() && + get_arg(1)->get_root() == n->get_arg(0)->get_root()) + return true; + for (unsigned i = num_args(); i-- > 0; ) + if (get_arg(i)->get_root() != n->get_arg(i)->get_root()) + return false; + return true; + } + + bool enode::reaches(enode* n) const { + enode const* r = this; + while (r) { + if (r == n) + return true; + r = r->m_target; + } + return false; + } + + void enode::reverse_justification() { + enode* curr = m_target; + enode* prev = this; + justification js = m_justification; + prev->m_target = nullptr; + prev->m_justification = justification::axiom(); + while (curr != nullptr) { + + enode* new_curr = curr->m_target; + justification new_js = curr->m_justification; + curr->m_target = prev; + curr->m_justification = js; + prev = curr; + js = new_js; + curr = new_curr; + } + } +} diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h new file mode 100644 index 000000000..008c5953b --- /dev/null +++ b/src/ast/euf/euf_enode.h @@ -0,0 +1,154 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + euf_enode.h + +Abstract: + + enode layer + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-23 + +--*/ + +#include "util/vector.h" +#include "ast/ast.h" +#include "ast/euf/euf_justification.h" + +#pragma once + +namespace euf { + + class enode; + + typedef ptr_vector enode_vector; + typedef std::pair enode_pair; + typedef svector enode_pair_vector; + + class enode { + expr* m_owner; + bool m_mark1 { false }; + bool m_mark2 { false }; + bool m_commutative { false }; + bool m_update_children { false }; + bool m_interpreted { false }; + unsigned m_class_size { 1 }; + unsigned m_table_id { UINT_MAX }; + enode_vector m_parents; + enode* m_next; + enode* m_root; + enode* m_target { nullptr }; + justification m_justification; + enode* m_args[0]; + + friend class enode_args; + friend class enode_parents; + friend class enode_class; + friend class etable; + friend class egraph; + + static unsigned get_enode_size(unsigned num_args) { + return sizeof(enode) + num_args * sizeof(enode*); + } + + static enode* mk(region& r, expr* f, unsigned num_args, enode* const* args) { + void* mem = r.allocate(get_enode_size(num_args)); + enode* n = new (mem) enode(); + n->m_owner = f; + n->m_next = n; + n->m_root = n; + n->m_commutative = num_args == 2 && is_app(f) && to_app(f)->get_decl()->is_commutative(); + for (unsigned i = 0; i < num_args; ++i) { + n->m_args[i] = args[i]; + } + return n; + } + + void set_update_children() { m_update_children = true; } + public: + ~enode() { + SASSERT(m_root == this); + SASSERT(class_size() == 1); + if (m_update_children) { + for (unsigned i = 0; i < num_args(); ++i) { + SASSERT(m_args[i]->get_root()->m_parents.back() == this); + m_args[i]->get_root()->m_parents.pop_back(); + } + } + } + + enode* const* args() const { return m_args; } + unsigned num_args() const { return is_app(m_owner) ? to_app(m_owner)->get_num_args() : 0; } + unsigned num_parents() const { return m_parents.size(); } + bool interpreted() const { return m_interpreted; } + void mark_interpreted() { SASSERT(num_args() == 0); m_interpreted = true; } + + enode* get_arg(unsigned i) const { SASSERT(i < num_args()); return m_args[i]; } + unsigned hash() const { return m_owner->hash(); } + func_decl* get_decl() const { return is_app(m_owner) ? to_app(m_owner)->get_decl() : nullptr; } + unsigned get_table_id() const { return m_table_id; } + void set_table_id(unsigned t) { m_table_id = t; } + + void mark1() { m_mark1 = true; } + void unmark1() { m_mark1 = false; } + bool is_marked1() { return m_mark1; } + void add_parent(enode* p) { m_parents.push_back(p); } + unsigned class_size() const { return m_class_size; } + enode* get_root() const { return m_root; } + expr* get_owner() const { return m_owner; } + unsigned get_owner_id() const { return m_owner->get_id(); } + void inc_class_size(unsigned n) { m_class_size += n; } + void dec_class_size(unsigned n) { m_class_size -= n; } + + void reverse_justification(); + bool reaches(enode* n) const; + + enode* const* begin_parents() const { return m_parents.begin(); } + enode* const* end_parents() const { return m_parents.end(); } + + void invariant(); + bool congruent(enode* n) const; + }; + + class enode_args { + enode& n; + public: + enode_args(enode& _n):n(_n) {} + enode_args(enode* _n):n(*_n) {} + enode* const* begin() const { return n.m_args; } + enode* const* end() const { return n.m_args + n.num_args(); } + }; + + class enode_parents { + enode const& n; + public: + enode_parents(enode const& _n):n(_n) {} + enode_parents(enode const* _n):n(*_n) {} + enode* const* begin() const { return n.m_parents.begin(); } + enode* const* end() const { return n.m_parents.end(); } + }; + + class enode_class { + enode & n; + public: + class iterator { + enode* m_first; + enode* m_last; + public: + iterator(enode* n, enode* m): m_first(n), m_last(m) {} + enode* operator*() { return m_first; } + iterator& operator++() { if (!m_last) m_last = m_first; m_first = m_first->m_next; return *this; } + iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; } + bool operator==(iterator const& other) const { return m_last == other.m_last && m_first == other.m_first; } + bool operator!=(iterator const& other) const { return !(*this == other); } + }; + enode_class(enode & _n):n(_n) {} + enode_class(enode * _n):n(*_n) {} + iterator begin() const { return iterator(&n, nullptr); } + iterator end() const { return iterator(&n, &n); } + }; +} diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp new file mode 100644 index 000000000..3b6ec8273 --- /dev/null +++ b/src/ast/euf/euf_etable.cpp @@ -0,0 +1,252 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + euf_etable.cpp + +Author: + + Leonardo de Moura (leonardo) 2008-02-19. + +Revision History: + + Ported from smt_cg_table.cpp + +--*/ +#include "ast/euf/euf_etable.h" +#include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" + +namespace euf { + + // one table per func_decl implementation + unsigned etable::cg_hash::operator()(enode * n) const { + SASSERT(n->get_decl()->is_flat_associative() || n->num_args() >= 3); + unsigned a, b, c; + a = b = 0x9e3779b9; + c = 11; + + unsigned i = n->num_args(); + while (i >= 3) { + i--; + a += n->get_arg(i)->get_root()->hash(); + i--; + b += n->get_arg(i)->get_root()->hash(); + i--; + c += n->get_arg(i)->get_root()->hash(); + mix(a, b, c); + } + + switch (i) { + case 2: + b += n->get_arg(1)->get_root()->hash(); + Z3_fallthrough; + case 1: + c += n->get_arg(0)->get_root()->hash(); + } + mix(a, b, c); + return c; + } + + bool etable::cg_eq::operator()(enode * n1, enode * n2) const { + SASSERT(n1->get_decl() == n2->get_decl()); + unsigned num = n1->num_args(); + if (num != n2->num_args()) { + return false; + } + for (unsigned i = 0; i < num; i++) + if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) + return false; + return true; + } + + etable::etable(ast_manager & m): + m_manager(m) { + } + + etable::~etable() { + reset(); + } + + void * etable::mk_table_for(func_decl * d) { + void * r; + SASSERT(d->get_arity() >= 1); + switch (d->get_arity()) { + case 1: + r = TAG(void*, alloc(unary_table), UNARY); + SASSERT(GET_TAG(r) == UNARY); + return r; + case 2: + if (d->is_flat_associative()) { + // applications of declarations that are flat-assoc (e.g., +) may have many arguments. + r = TAG(void*, alloc(table), NARY); + SASSERT(GET_TAG(r) == NARY); + return r; + } + else if (d->is_commutative()) { + r = TAG(void*, alloc(comm_table, cg_comm_hash(), cg_comm_eq(m_commutativity)), BINARY_COMM); + SASSERT(GET_TAG(r) == BINARY_COMM); + return r; + } + else { + r = TAG(void*, alloc(binary_table), BINARY); + SASSERT(GET_TAG(r) == BINARY); + return r; + } + default: + r = TAG(void*, alloc(table), NARY); + SASSERT(GET_TAG(r) == NARY); + return r; + } + } + + unsigned etable::set_table_id(enode * n) { + func_decl * f = n->get_decl(); + unsigned tid; + if (!m_func_decl2id.find(f, tid)) { + tid = m_tables.size(); + m_func_decl2id.insert(f, tid); + m_manager.inc_ref(f); + SASSERT(tid <= m_tables.size()); + m_tables.push_back(mk_table_for(f)); + } + SASSERT(tid < m_tables.size()); + n->set_table_id(tid); + DEBUG_CODE({ + unsigned tid_prime; + SASSERT(m_func_decl2id.find(n->get_decl(), tid_prime) && tid == tid_prime); + }); + return tid; + } + + void etable::reset() { + for (void* t : m_tables) { + switch (GET_TAG(t)) { + case UNARY: + dealloc(UNTAG(unary_table*, t)); + break; + case BINARY: + dealloc(UNTAG(binary_table*, t)); + break; + case BINARY_COMM: + dealloc(UNTAG(comm_table*, t)); + break; + case NARY: + dealloc(UNTAG(table*, t)); + break; + } + } + m_tables.reset(); + for (auto const& kv : m_func_decl2id) { + m_manager.dec_ref(kv.m_key); + } + m_func_decl2id.reset(); + } + + void etable::display(std::ostream & out) const { + for (auto const& kv : m_func_decl2id) { + void * t = m_tables[kv.m_value]; + out << mk_pp(kv.m_key, m_manager) << ": "; + switch (GET_TAG(t)) { + case UNARY: + display_unary(out, t); + break; + case BINARY: + display_binary(out, t); + break; + case BINARY_COMM: + display_binary_comm(out, t); + break; + case NARY: + display_nary(out, t); + break; + } + } + } + + void etable::display_binary(std::ostream& out, void* t) const { + binary_table* tb = UNTAG(binary_table*, t); + out << "b "; + for (enode* n : *tb) { + out << n->get_owner_id() << " " << cg_binary_hash()(n) << " "; + } + out << "\n"; + } + + void etable::display_binary_comm(std::ostream& out, void* t) const { + comm_table* tb = UNTAG(comm_table*, t); + out << "bc "; + for (enode* n : *tb) { + out << n->get_owner_id() << " "; + } + out << "\n"; + } + + void etable::display_unary(std::ostream& out, void* t) const { + unary_table* tb = UNTAG(unary_table*, t); + out << "un "; + for (enode* n : *tb) { + out << n->get_owner_id() << " "; + } + out << "\n"; + } + + void etable::display_nary(std::ostream& out, void* t) const { + table* tb = UNTAG(table*, t); + out << "nary "; + for (enode* n : *tb) { + out << n->get_owner_id() << " "; + } + out << "\n"; + } + + + enode_bool_pair etable::insert(enode * n) { + // it doesn't make sense to insert a constant. + SASSERT(n->num_args() > 0); + SASSERT(!m_manager.is_and(n->get_owner())); + SASSERT(!m_manager.is_or(n->get_owner())); + enode * n_prime; + void * t = get_table(n); + switch (static_cast(GET_TAG(t))) { + case UNARY: + n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, false); + case BINARY: + n_prime = UNTAG(binary_table*, t)->insert_if_not_there(n); + TRACE("euf", tout << "insert: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " inserted: " << (n == n_prime) << " " << n_prime->get_owner_id() << "\n"; + display_binary(tout, t); tout << "contains_ptr: " << contains_ptr(n) << "\n";); + return enode_bool_pair(n_prime, false); + case BINARY_COMM: + m_commutativity = false; + n_prime = UNTAG(comm_table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, m_commutativity); + default: + n_prime = UNTAG(table*, t)->insert_if_not_there(n); + return enode_bool_pair(n_prime, false); + } + } + + void etable::erase(enode * n) { + SASSERT(n->num_args() > 0); + void * t = get_table(n); + switch (static_cast(GET_TAG(t))) { + case UNARY: + UNTAG(unary_table*, t)->erase(n); + break; + case BINARY: + TRACE("euf", tout << "erase: " << n->get_owner_id() << " " << cg_binary_hash()(n) << " contains: " << contains_ptr(n) << "\n";); + UNTAG(binary_table*, t)->erase(n); + break; + case BINARY_COMM: + UNTAG(comm_table*, t)->erase(n); + break; + default: + UNTAG(table*, t)->erase(n); + break; + } + } + +}; + diff --git a/src/ast/euf/euf_etable.h b/src/ast/euf/euf_etable.h new file mode 100644 index 000000000..5981f7aec --- /dev/null +++ b/src/ast/euf/euf_etable.h @@ -0,0 +1,217 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + euf_etable.h + +Author: + + Leonardo de Moura (leonardo) 2008-02-19. + +Revision History: + + copied from smt_cg_table + +--*/ + +#pragma once + +#include "ast/euf/euf_enode.h" +#include "util/hashtable.h" +#include "util/chashtable.h" + +namespace euf { + + typedef std::pair enode_bool_pair; + + // one table per function symbol + + /** + \brief Congruence table. + */ + class etable { + struct cg_unary_hash { + unsigned operator()(enode * n) const { + SASSERT(n->num_args() == 1); + return n->get_arg(0)->get_root()->hash(); + } + }; + + struct cg_unary_eq { + bool operator()(enode * n1, enode * n2) const { + SASSERT(n1->num_args() == 1); + SASSERT(n2->num_args() == 1); + SASSERT(n1->get_decl() == n2->get_decl()); + return n1->get_arg(0)->get_root() == n2->get_arg(0)->get_root(); + } + }; + + typedef chashtable unary_table; + + struct cg_binary_hash { + unsigned operator()(enode * n) const { + SASSERT(n->num_args() == 2); + return combine_hash(n->get_arg(0)->get_root()->hash(), n->get_arg(1)->get_root()->hash()); + } + }; + + struct cg_binary_eq { + bool operator()(enode * n1, enode * n2) const { + SASSERT(n1->num_args() == 2); + SASSERT(n2->num_args() == 2); + SASSERT(n1->get_decl() == n2->get_decl()); + return + n1->get_arg(0)->get_root() == n2->get_arg(0)->get_root() && + n1->get_arg(1)->get_root() == n2->get_arg(1)->get_root(); + } + }; + + typedef chashtable binary_table; + + struct cg_comm_hash { + unsigned operator()(enode * n) const { + SASSERT(n->num_args() == 2); + unsigned h1 = n->get_arg(0)->get_root()->hash(); + unsigned h2 = n->get_arg(1)->get_root()->hash(); + if (h1 > h2) + std::swap(h1, h2); + return hash_u((h1 << 16) | (h2 & 0xFFFF)); + } + }; + + struct cg_comm_eq { + bool & m_commutativity; + cg_comm_eq(bool & c):m_commutativity(c) {} + bool operator()(enode * n1, enode * n2) const { + SASSERT(n1->num_args() == 2); + SASSERT(n2->num_args() == 2); + SASSERT(n1->get_decl() == n2->get_decl()); + enode * c1_1 = n1->get_arg(0)->get_root(); + enode * c1_2 = n1->get_arg(1)->get_root(); + enode * c2_1 = n2->get_arg(0)->get_root(); + enode * c2_2 = n2->get_arg(1)->get_root(); + if (c1_1 == c2_1 && c1_2 == c2_2) { + return true; + } + if (c1_1 == c2_2 && c1_2 == c2_1) { + m_commutativity = true; + return true; + } + return false; + } + }; + + typedef chashtable comm_table; + + struct cg_hash { + unsigned operator()(enode * n) const; + }; + + struct cg_eq { + bool operator()(enode * n1, enode * n2) const; + }; + + typedef chashtable table; + + ast_manager & m_manager; + bool m_commutativity; //!< true if the last found congruence used commutativity + ptr_vector m_tables; + obj_map m_func_decl2id; + + enum table_kind { + UNARY, + BINARY, + BINARY_COMM, + NARY + }; + + void * mk_table_for(func_decl * d); + unsigned set_table_id(enode * n); + + void * get_table(enode * n) { + unsigned tid = n->get_table_id(); + if (tid == UINT_MAX) + tid = set_table_id(n); + SASSERT(tid < m_tables.size()); + return m_tables[tid]; + } + + void display_binary(std::ostream& out, void* t) const; + void display_binary_comm(std::ostream& out, void* t) const; + void display_unary(std::ostream& out, void* t) const; + void display_nary(std::ostream& out, void* t) const; + + public: + etable(ast_manager & m); + + ~etable(); + + /** + \brief Try to insert n into the table. If the table already + contains an element n' congruent to n, then do nothing and + return n' and a boolean indicating whether n and n' are congruence + modulo commutativity, otherwise insert n and return (n,false). + */ + enode_bool_pair insert(enode * n); + + void erase(enode * n); + + bool contains(enode * n) const { + SASSERT(n->num_args() > 0); + void * t = const_cast(this)->get_table(n); + switch (static_cast(GET_TAG(t))) { + case UNARY: + return UNTAG(unary_table*, t)->contains(n); + case BINARY: + return UNTAG(binary_table*, t)->contains(n); + case BINARY_COMM: + return UNTAG(comm_table*, t)->contains(n); + default: + return UNTAG(table*, t)->contains(n); + } + } + + enode * find(enode * n) const { + SASSERT(n->num_args() > 0); + enode * r = nullptr; + void * t = const_cast(this)->get_table(n); + switch (static_cast(GET_TAG(t))) { + case UNARY: + return UNTAG(unary_table*, t)->find(n, r) ? r : nullptr; + case BINARY: + return UNTAG(binary_table*, t)->find(n, r) ? r : nullptr; + case BINARY_COMM: + return UNTAG(comm_table*, t)->find(n, r) ? r : nullptr; + default: + return UNTAG(table*, t)->find(n, r) ? r : nullptr; + } + } + + bool contains_ptr(enode * n) const { + enode * r; + SASSERT(n->num_args() > 0); + void * t = const_cast(this)->get_table(n); + switch (static_cast(GET_TAG(t))) { + case UNARY: + return UNTAG(unary_table*, t)->find(n, r) && n == r; + case BINARY: + return UNTAG(binary_table*, t)->find(n, r) && n == r; + case BINARY_COMM: + return UNTAG(comm_table*, t)->find(n, r) && n == r; + default: + return UNTAG(table*, t)->find(n, r) && n == r; + } + } + + void reset(); + + void display(std::ostream & out) const; + + }; + +}; + + + + diff --git a/src/ast/euf/euf_justification.h b/src/ast/euf/euf_justification.h new file mode 100644 index 000000000..dff67a4d5 --- /dev/null +++ b/src/ast/euf/euf_justification.h @@ -0,0 +1,59 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + euf_justification.h + +Abstract: + + justification structure for euf + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-23 + +--*/ + +#pragma once + +namespace euf { + + class justification { + enum kind_t { + axiom_t, + congruence_t, + external_t + }; + kind_t m_kind; + bool m_comm; + void* m_external; + justification(bool comm): + m_kind(congruence_t), + m_comm(comm), + m_external(nullptr) + {} + + justification(void* ext): + m_kind(external_t), + m_comm(false), + m_external(ext) + {} + + public: + justification(): + m_kind(axiom_t), + m_comm(false), + m_external(nullptr) + {} + + static justification axiom() { return justification(); } + static justification congruence(bool c) { return justification(c); } + static justification external(void* ext) { return justification(ext); } + + bool is_external() const { return m_kind == external_t; } + bool is_congruence() const { return m_kind == congruence_t; } + template + T* ext() const { SASSERT(is_external()); return static_cast(m_external); } + }; +} diff --git a/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt index dbbfbe753..848bf814b 100644 --- a/src/sat/tactic/CMakeLists.txt +++ b/src/sat/tactic/CMakeLists.txt @@ -7,6 +7,7 @@ z3_add_component(sat_tactic sat tactic solver + euf TACTIC_HEADERS sat_tactic.h ) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 47ac5a355..664563cc2 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -637,7 +637,6 @@ struct goal2sat::imp { } m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned()); - if (root && !sign) { m_result_stack.reset(); } @@ -769,15 +768,14 @@ struct goal2sat::imp { return t->get_arg(idx); } } - - void process(expr * n) { - //SASSERT(m_result_stack.empty()); - TRACE("goal2sat", tout << "converting: " << mk_bounded_pp(n, m, 2) << "\n";); - if (visit(n, true, false)) { + + void process(expr* n, bool is_root) { + unsigned sz = m_frame_stack.size(); + if (visit(n, is_root, false)) { SASSERT(m_result_stack.empty()); return; } - while (!m_frame_stack.empty()) { + while (m_frame_stack.size() > sz) { loop: if (!m.inc()) throw tactic_exception(m.limit().get_cancel_msg()); @@ -812,6 +810,20 @@ struct goal2sat::imp { convert(t, root, sign); m_frame_stack.pop_back(); } + } + + sat::literal internalize(expr* n) { + SASSERT(m_result_stack.empty()); + process(n, false); + SASSERT(m_result_stack.size() == 1); + sat::literal result = m_result_stack.back(); + m_result_stack.reset(); + return result; + } + + void process(expr * n) { + m_result_stack.reset(); + process(n, true); CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";); SASSERT(m_result_stack.empty()); } @@ -868,7 +880,7 @@ struct goal2sat::imp { } fmls.push_back(d_new); } - f = m.mk_or(fmls.size(), fmls.c_ptr()); + f = m.mk_or(fmls); } TRACE("goal2sat", tout << mk_bounded_pp(f, m, 2) << "\n";); process(f); @@ -1187,7 +1199,7 @@ struct sat2goal::imp { for (sat::literal l : c) { lits.push_back(lit2expr(mc, l)); } - r.assert_expr(m.mk_or(lits.size(), lits.c_ptr())); + r.assert_expr(m.mk_or(lits)); } } } diff --git a/src/smt/mam.h b/src/smt/mam.h index 7e10440c9..bf23b24a6 100644 --- a/src/smt/mam.h +++ b/src/smt/mam.h @@ -23,6 +23,9 @@ Revision History: #include namespace smt { + + class context; + /** \brief Matching Abstract Machine (MAM) */ diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index a215fb6ef..37ac66518 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -623,7 +623,10 @@ namespace smt { */ void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) { enode_vector & r2_parents = r2->m_parents; - for (enode * parent : enode::parents(r1)) { + enode_vector & r1_parents = r1->m_parents; + unsigned num_r1_parents = r1_parents.size(); + for (unsigned i = 0; i < num_r1_parents; ++i) { + enode* parent = r1_parents[i]; if (!parent->is_marked()) continue; parent->unset_mark(); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3b566b905..c499ae7ee 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -57,11 +57,7 @@ Revision History: // the case that each context only references a few expressions. // Using a map instead of a vector for the literals can compress space // consumption. -#ifdef SPARSE_MAP -#define USE_BOOL_VAR_VECTOR 0 -#else #define USE_BOOL_VAR_VECTOR 1 -#endif namespace smt { diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 7047c97c4..500604569 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -44,21 +44,7 @@ namespace smt { referencing few nodes from a large ast manager. There is some unknown performance penalty for this. */ - // #define SPARSE_MAP - -#ifndef SPARSE_MAP typedef ptr_vector app2enode_t; // app -> enode -#else - class app2enode_t : public u_map { - public: - void setx(unsigned x, enode *val, enode *def){ - if (val == 0) - erase(x); - else - insert(x,val); - } - }; -#endif class tmp_enode; @@ -111,7 +97,6 @@ namespace smt { enode * m_args[0]; //!< Cached args friend class context; - friend class euf_manager; friend class conflict_resolution; friend class quantifier_manager; @@ -245,12 +230,6 @@ namespace smt { const_args get_const_args() const { return const_args(this); } - // args get_args() { return args(this); } - - // unsigned get_id() const { - // return m_id; - // } - unsigned get_class_size() const { return m_class_size; } diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h index 7d057d95c..848cf26e9 100644 --- a/src/smt/smt_justification.h +++ b/src/smt/smt_justification.h @@ -26,6 +26,7 @@ Revision History: namespace smt { class conflict_resolution; + class context; typedef ptr_vector justification_vector; diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index cf083daf0..abe84916b 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -30,6 +30,7 @@ struct smt_params; namespace smt { class quantifier_manager_plugin; class quantifier_stat; + class context; class quantifier_manager { struct imp; diff --git a/src/smt/smt_types.h b/src/smt/smt_types.h index 510885d67..edbca06c5 100644 --- a/src/smt/smt_types.h +++ b/src/smt/smt_types.h @@ -47,8 +47,6 @@ namespace smt { typedef std::pair enode_pair; typedef svector enode_pair_vector; - class context; - class theory; class justification; diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 7bfc0569c..816d1a848 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -36,6 +36,7 @@ add_executable(test-z3 dl_table.cpp dl_util.cpp doc.cpp + egraph.cpp escaped.cpp ex.cpp expr_rand.cpp diff --git a/src/test/egraph.cpp b/src/test/egraph.cpp new file mode 100644 index 000000000..c4fb249a2 --- /dev/null +++ b/src/test/egraph.cpp @@ -0,0 +1,96 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +--*/ + +#include "util/timer.h" +#include "ast/euf/euf_egraph.h" +#include "ast/reg_decl_plugins.h" +#include "ast/ast_pp.h" + +static expr_ref mk_const(ast_manager& m, char const* name, sort* s) { + return expr_ref(m.mk_const(symbol(name), s), m); +} + +static expr_ref mk_app(char const* name, expr_ref const& arg, sort* s) { + ast_manager& m = arg.m(); + func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg), s), m); + return expr_ref(m.mk_app(f, arg), m); +} + +static expr_ref mk_app(char const* name, expr_ref const& arg1, expr_ref const& arg2, sort* s) { + ast_manager& m = arg1.m(); + func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg1), m.get_sort(arg2), s), m); + return expr_ref(m.mk_app(f, arg1, arg2), m); +} + +static void test1() { + ast_manager m; + reg_decl_plugins(m); + euf::egraph g(m); + sort_ref S(m.mk_uninterpreted_sort(symbol("S")), m); + expr_ref a = mk_const(m, "a", S); + expr_ref fa = mk_app("f", a, S); + expr_ref ffa = mk_app("f", fa, S); + expr_ref fffa = mk_app("f", ffa, S); + euf::enode* na = g.mk(a, nullptr); + euf::enode* nfa = g.mk(fa, &na); + euf::enode* nffa = g.mk(ffa, &nfa); + euf::enode* nfffa = g.mk(fffa, &nffa); + std::cout << g << "\n"; + g.merge(na, nffa, nullptr); + g.merge(na, nfffa, nullptr); + std::cout << g << "\n"; + g.propagate(); + std::cout << g << "\n"; +} + +static void test2() { + ast_manager m; + reg_decl_plugins(m); + euf::egraph g(m); + sort_ref S(m.mk_uninterpreted_sort(symbol("S")), m); + unsigned d = 100, w = 100; + euf::enode_vector nodes, top_nodes; + expr_ref_vector pinned(m); + for (unsigned i = 0; i < w; ++i) { + std::string xn("x"); + xn += std::to_string(i); + expr_ref x = mk_const(m, xn.c_str(), S); + euf::enode* n = g.mk(x, nullptr); + nodes.push_back(n); + for (unsigned j = 0; j < d; ++j) { + std::string f("f"); + f += std::to_string(j); + x = mk_app(f.c_str(), x, S); + n = g.mk(x, &n); + } + top_nodes.push_back(n); + pinned.push_back(x); + } + std::cout << "merge\n"; + timer t; + for (euf::enode* n : nodes) { + g.merge(n, nodes[0], nullptr); + } + std::cout << "merged " << t.get_seconds() << "\n"; + g.propagate(); + std::cout << "propagated " << t.get_seconds() << "\n"; + for (euf::enode* n : top_nodes) { + SASSERT(n->get_root() == top_nodes[0]->get_root()); + } +} + +static void test3() { + ast_manager m; + reg_decl_plugins(m); + euf::egraph g(m); + sort_ref S(m.mk_uninterpreted_sort(symbol("S")), m); + +} + +void tst_egraph() { + enable_trace("euf"); + test1(); + test2(); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index 002fc920d..cf7ae8acc 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -196,6 +196,7 @@ int main(int argc, char ** argv) { TST(escaped); TST(buffer); TST(chashtable); + TST(egraph); TST(ex); TST(nlarith_util); TST(api_bug);