mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

tidy verbose mode a bit, ackermannize special cases of arrays

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-02-05 21:19:32 -08:00
parent 8e5581b4fe
commit 7fd4e7861f
3 changed files with 119 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

100
src/muz_qe/dl_mk_array_blast.cpp
View file

@ -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) {