From a18236bc7f2a9037ccd1d7d078cb54c132328474 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 00:07:53 +0100 Subject: [PATCH] have quantifier equality take names into account Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 3 ++ src/ast/expr_abstract.cpp | 9 ++++ src/ast/expr_substitution.cpp | 7 +++ src/ast/expr_substitution.h | 3 ++ src/tactic/core/dom_simplify_tactic.cpp | 65 ++++++++++++++++++++----- src/tactic/core/dom_simplify_tactic.h | 5 +- 6 files changed, 78 insertions(+), 14 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c98307ee0..cac12413e 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -471,6 +471,9 @@ bool compare_nodes(ast const * n1, ast const * n2) { compare_arrays(to_quantifier(n1)->get_decl_sorts(), to_quantifier(n2)->get_decl_sorts(), to_quantifier(n1)->get_num_decls()) && + compare_arrays(to_quantifier(n1)->get_decl_names(), + to_quantifier(n2)->get_decl_names(), + to_quantifier(n1)->get_num_decls()) && to_quantifier(n1)->get_expr() == to_quantifier(n2)->get_expr() && to_quantifier(n1)->get_weight() == to_quantifier(n2)->get_weight() && to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() && diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp index 46682eed6..43035e203 100644 --- a/src/ast/expr_abstract.cpp +++ b/src/ast/expr_abstract.cpp @@ -19,6 +19,7 @@ Notes: #include "ast/expr_abstract.h" #include "util/map.h" +#include "ast/ast_pp.h" void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { @@ -109,6 +110,9 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { expr_abstractor abs(m); abs(base, num_bound, bound, n, result); + TRACE("expr_abstract", + tout << expr_ref(n, m) << "\n"; + tout << result << "\n";); } expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) { @@ -123,6 +127,11 @@ expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* } result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result); } + TRACE("expr_abstract", + tout << expr_ref(n, m) << "\n"; + for (unsigned i = 0; i < num_bound; ++i) tout << expr_ref(bound[i], m) << " "; + tout << "\n"; + tout << result << "\n";); return result; } diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp index 149a59ce5..3ce038250 100644 --- a/src/ast/expr_substitution.cpp +++ b/src/ast/expr_substitution.cpp @@ -56,6 +56,13 @@ expr_substitution::~expr_substitution() { reset(); } +std::ostream& expr_substitution::display(std::ostream& out) { + for (auto & kv : m_subst) { + out << expr_ref(kv.m_key, m()) << " |-> " << expr_ref(kv.m_value, m()) << "\n"; + } + return out; +} + void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) { obj_map::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0); if (entry->get_data().m_value == 0) { diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index d360356eb..90154d163 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -50,6 +50,8 @@ public: bool contains(expr * s); void reset(); void cleanup(); + + std::ostream& display(std::ostream& out); }; class scoped_expr_substitution { @@ -84,6 +86,7 @@ public: bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); } bool contains(expr * s) { return m_subst.contains(s); } void cleanup() { m_subst.cleanup(); } + std::ostream& display(std::ostream& out) { return m_subst.display(out); } }; #endif diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 99f83799b..60207e823 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -91,23 +91,42 @@ bool expr_dominators::compute_dominators() { unsigned iterations = 1; while (change) { change = false; + TRACE("simplify", + for (auto & kv : m_doms) { + tout << expr_ref(kv.m_key, m) << " |-> " << expr_ref(kv.m_value, m) << "\n"; + }); + SASSERT(m_post2expr.empty() || m_post2expr.back() == e); for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; SASSERT(!p.empty()); - expr * new_idom = 0, *idom2 = 0; - for (unsigned j = 0; j < p.size(); ++j) { - if (!new_idom) { - m_doms.find(p[j], new_idom); - } - else if (m_doms.find(p[j], idom2)) { - new_idom = intersect(new_idom, idom2); - } + if (p.size() == 1) { + if (!m_doms.contains(child)) { + m_doms.insert(child, p[0]); + change = true; + } } - if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) { - m_doms.insert(child, new_idom); - change = true; + else { + expr * new_idom = 0, *idom2 = 0; + for (unsigned j = 0; j < p.size(); ++j) { + if (!new_idom) { + m_doms.find(p[j], new_idom); + } + else if (m_doms.find(p[j], idom2)) { + new_idom = intersect(new_idom, idom2); + } + } + if (!new_idom) { + m_doms.insert(child, p[0]); + TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(p[0], m) << "\n";); + change = true; + } + else if (!m_doms.find(child, idom2) || idom2 != new_idom) { + m_doms.insert(child, new_idom); + TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(new_idom, m) << "\n";); + change = true; + } } } iterations *= 2; @@ -130,6 +149,7 @@ bool expr_dominators::compile(expr * e) { compute_post_order(); if (!compute_dominators()) return false; extract_tree(); + TRACE("simplify", display(tout);); return true; } @@ -147,6 +167,22 @@ void expr_dominators::reset() { m_root.reset(); } +std::ostream& expr_dominators::display(std::ostream& out) { + return display(out, 0, m_root); +} + +std::ostream& expr_dominators::display(std::ostream& out, unsigned indent, expr* r) { + for (unsigned i = 0; i < indent; ++i) out << " "; + out << expr_ref(r, m); + if (m_tree.contains(r)) { + for (expr* child : m_tree[r]) { + if (child != r) + display(out, indent + 1, child); + } + } + out << "\n"; + return out; +} // ----------------------- @@ -200,7 +236,6 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { simplify(child); } } - pop(scope_level() - old_lvl); expr_ref new_t = simplify(t); if (!assert_expr(new_c, true)) { @@ -230,6 +265,8 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr_ref dom_simplify_tactic::simplify(expr * e0) { expr_ref r(m); expr* e = 0; + + TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); if (!m_result.find(e0, e)) { e = e0; } @@ -254,7 +291,9 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { if (is_app(e)) { m_args.reset(); for (expr* arg : *to_app(e)) { - m_args.push_back(get_cached(arg)); // TBD is cache really applied to all sub-terms? + r = get_cached(arg); + (*m_simplifier)(r); + m_args.push_back(r); } r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr()); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index c1660a941..d99f799b4 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -48,6 +48,8 @@ private: bool compute_dominators(); void extract_tree(); + std::ostream& display(std::ostream& out, unsigned indent, expr* r); + public: expr_dominators(ast_manager& m): m(m), m_root(m) {} @@ -55,7 +57,8 @@ public: bool compile(unsigned sz, expr * const* es); tree_t const& get_tree() { return m_tree; } void reset(); - + + std::ostream& display(std::ostream& out); }; class dom_simplifier {