From 7fd4e7861f1b46cd59fa6a4c5a940465fc0b5902 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Feb 2013 21:19:32 -0800
Subject: [PATCH] tidy verbose mode a bit, ackermannize special cases of arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/muz_qe/dl_mk_array_blast.cpp | 100 +++++++++++++++++++++++++++++--
src/muz_qe/dl_mk_array_blast.h | 4 ++
src/muz_qe/pdr_context.cpp | 33 ++++++----
3 files changed, 119 insertions(+), 18 deletions(-)
diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp
index 880f196a2..b22fdf7ef 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz_qe/dl_mk_array_blast.cpp
@@ -49,6 +49,94 @@ namespace datalog {
}
return false;
}
+
+ bool mk_array_blast::ackermanize(expr_ref& body, expr_ref& head) {
+ expr_ref_vector conjs(m);
+ flatten_and(body, conjs);
+ defs_t defs;
+ expr_safe_replace sub(m);
+ ptr_vector<expr> todo;
+ todo.push_back(head);
+ for (unsigned i = 0; i < conjs.size(); ++i) {
+ expr* e = conjs[i].get();
+ expr* x, *y;
+ if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) {
+ if (a.is_select(y)) {
+ std::swap(x,y);
+ }
+ if (a.is_select(x) && is_var(y)) {
+ //
+ // For the Ackermann reduction we would like the arrays
+ // to be variables, so that variables can be
+ // assumed to represent difference (alias)
+ // classes.
+ //
+ if (!is_var(to_app(x)->get_arg(0))) {
+ return false;
+ }
+ sub.insert(x, y);
+ defs.insert(to_app(x), to_var(y));
+ }
+ }
+ todo.push_back(e);
+ }
+ // now check that all occurrences of select have been covered.
+ ast_mark mark;
+ while (!todo.empty()) {
+ expr* e = todo.back();
+ todo.pop_back();
+ if (mark.is_marked(e)) {
+ continue;
+ }
+ mark.mark(e, true);
+ if (is_var(e)) {
+ continue;
+ }
+ if (!is_app(e)) {
+ return false;
+ }
+ app* ap = to_app(e);
+ if (a.is_select(e) && !defs.contains(ap)) {
+ return false;
+ }
+ for (unsigned i = 0; i < ap->get_num_args(); ++i) {
+ todo.push_back(ap->get_arg(i));
+ }
+ }
+ sub(body);
+ sub(head);
+ conjs.reset();
+
+ // perform the Ackermann reduction by creating implications
+ // i1 = i2 => val1 = val2 for each equality pair:
+ // (= val1 (select a_i i1))
+ // (= val2 (select a_i i2))
+ defs_t::iterator it1 = defs.begin(), end = defs.end();
+ for (; it1 != end; ++it1) {
+ app* a1 = it1->m_key;
+ var* v1 = it1->m_value;
+ defs_t::iterator it2 = it1;
+ ++it2;
+ for (; it2 != end; ++it2) {
+ app* a2 = it2->m_key;
+ var* v2 = it2->m_value;
+ if (a1->get_arg(0) != a2->get_arg(0)) {
+ continue;
+ }
+ expr_ref_vector eqs(m);
+ for (unsigned j = 1; j < a1->get_num_args(); ++j) {
+ eqs.push_back(m.mk_eq(a1->get_arg(j), a2->get_arg(j)));
+ }
+ conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2)));
+ }
+ }
+ if (!conjs.empty()) {
+ conjs.push_back(body);
+ body = m.mk_and(conjs.size(), conjs.c_ptr());
+ }
+ m_rewriter(body);
+ return true;
+ }
bool mk_array_blast::blast(rule& r, rule_set& rules) {
unsigned utsz = r.get_uninterpreted_tail_size();
@@ -92,10 +180,6 @@ namespace datalog {
new_conjs.push_back(tmp);
}
}
- if (!inserted && !change) {
- rules.add_rule(&r);
- return false;
- }
rule_ref_vector new_rules(rm);
expr_ref fml1(m), fml2(m), body(m), head(m);
@@ -106,11 +190,17 @@ namespace datalog {
m_rewriter(body);
sub(head);
m_rewriter(head);
+ change = ackermanize(body, head) || change;
+ if (!inserted && !change) {
+ rules.add_rule(&r);
+ return false;
+ }
+
fml2 = m.mk_implies(body, head);
rm.mk_rule(fml2, new_rules, r.name());
SASSERT(new_rules.size() == 1);
- TRACE("dl", tout << "new body " << mk_pp(fml2, m) << "\n";);
+ TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n"););
rules.add_rule(new_rules[0].get());
if (m_pc) {
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h
index 858b9c778..1618e4fa8 100644
--- a/src/muz_qe/dl_mk_array_blast.h
+++ b/src/muz_qe/dl_mk_array_blast.h
@@ -39,10 +39,14 @@ namespace datalog {
th_rewriter m_rewriter;
equiv_proof_converter* m_pc;
+ typedef obj_map<app, var*> defs_t;
+
bool blast(rule& r, rule_set& new_rules);
bool is_store_def(expr* e, expr*& x, expr*& y);
+ bool ackermanize(expr_ref& body, expr_ref& head);
+
public:
/**
\brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 574d44fb5..47655ac7b 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -52,6 +52,20 @@ namespace pdr {
static bool is_infty_level(unsigned lvl) { return lvl == infty_level; }
static unsigned next_level(unsigned lvl) { return is_infty_level(lvl)?lvl:(lvl+1); }
+
+ struct pp_level {
+ unsigned m_level;
+ pp_level(unsigned l): m_level(l) {}
+ };
+
+ static std::ostream& operator<<(std::ostream& out, pp_level const& p) {
+ if (is_infty_level(p.m_level)) {
+ return out << "oo";
+ }
+ else {
+ return out << p.m_level;
+ }
+ }
// ----------------
// pred_tansformer
@@ -263,7 +277,7 @@ namespace pdr {
else if (is_invariant(tgt_level, curr, false, assumes_level)) {
add_property(curr, assumes_level?tgt_level:infty_level);
- TRACE("pdr", tout << "is invariant: "<< tgt_level << " " << mk_pp(curr, m) << "\n";);
+ TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";);
src[i] = src.back();
src.pop_back();
++m_stats.m_num_propagations;
@@ -273,14 +287,7 @@ namespace pdr {
++i;
}
}
- IF_VERBOSE(2, verbose_stream() << "propagate: ";
- if (is_infty_level(src_level)) {
- verbose_stream() << "infty";
- }
- else {
- verbose_stream() << src_level;
- }
- verbose_stream() << "\n";
+ IF_VERBOSE(3, verbose_stream() << "propagate: " << pp_level(src_level) << "\n";
for (unsigned i = 0; i < src.size(); ++i) {
verbose_stream() << mk_pp(src[i].get(), m) << "\n";
});
@@ -304,14 +311,14 @@ namespace pdr {
ensure_level(lvl);
unsigned old_level;
if (!m_prop2level.find(lemma, old_level) || old_level < lvl) {
- TRACE("pdr", tout << "property1: " << lvl << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
+ TRACE("pdr", tout << "property1: " << pp_level(lvl) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
m_levels[lvl].push_back(lemma);
m_prop2level.insert(lemma, lvl);
m_solver.add_level_formula(lemma, lvl);
return true;
}
else {
- TRACE("pdr", tout << "old-level: " << old_level << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
+ TRACE("pdr", tout << "old-level: " << pp_level(old_level) << " " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
return false;
}
}
@@ -337,7 +344,7 @@ namespace pdr {
for (unsigned i = 0; i < lemmas.size(); ++i) {
expr* lemma_i = lemmas[i].get();
if (add_property1(lemma_i, lvl)) {
- IF_VERBOSE(2, verbose_stream() << lvl << " " << mk_pp(lemma_i, m) << "\n";);
+ IF_VERBOSE(2, verbose_stream() << pp_level(lvl) << " " << mk_pp(lemma_i, m) << "\n";);
for (unsigned j = 0; j < m_use.size(); ++j) {
m_use[j]->add_child_property(*this, lemma_i, next_level(lvl));
}
@@ -1914,7 +1921,7 @@ namespace pdr {
model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1);
++m_stats.m_num_nodes;
m_search.add_leaf(*child);
- IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
+ IF_VERBOSE(3, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth());
}
check_pre_closed(n);