mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
have quantifier equality take names into account
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
31c6b3eb5b
commit
a18236bc7f
|
@ -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() &&
|
||||
|
|
|
@ -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;
|
||||
|
||||
}
|
||||
|
|
|
@ -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<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0);
|
||||
if (entry->get_data().m_value == 0) {
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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<expr> 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());
|
||||
}
|
||||
|
|
|
@ -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 {
|
||||
|
|
Loading…
Reference in a new issue