mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

fix #3735

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 16:36:54 -07:00
parent 7838e99f47
commit 9fbe178de4
2 changed files with 93 additions and 122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

203
src/tactic/ufbv/ufbv_rewriter.cpp
View file

@ -27,7 +27,7 @@ Revision History:
#include "tactic/ufbv/ufbv_rewriter.h"
ufbv_rewriter::ufbv_rewriter(ast_manager & m):
m_manager(m),
m(m),
m_match_subst(m),
m_bsimp(m),
m_todo(m),
@ -42,27 +42,25 @@ ufbv_rewriter::ufbv_rewriter(ast_manager & m):
ufbv_rewriter::~ufbv_rewriter() {
reset_dealloc_values(m_fwd_idx);
reset_dealloc_values(m_back_idx);
for (demodulator2lhs_rhs::iterator it = m_demodulator2lhs_rhs.begin(); it != m_demodulator2lhs_rhs.end(); it++) {
m_manager.dec_ref(it->m_key);
m_manager.dec_ref(it->m_value.first);
m_manager.dec_ref(it->m_value.second);
for (auto & kv : m_demodulator2lhs_rhs) {
m.dec_ref(kv.m_key);
m.dec_ref(kv.m_value.first);
m.dec_ref(kv.m_value.second);
}
}
bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) const {
if (e->get_kind() == AST_QUANTIFIER) {
if (is_quantifier(e)) {
quantifier * q = to_quantifier(e);
if (is_forall(q)) {
expr * qe = q->get_expr();
if ((m_manager.is_eq(qe) || m_manager.is_iff(qe))) {
app * eq = to_app(q->get_expr());
expr * lhs = eq->get_arg(0);
expr * rhs = eq->get_arg(1);
expr * lhs = nullptr, *rhs = nullptr;
if (m.is_eq(qe, lhs, rhs)) {
int subset = is_subset(lhs, rhs);
int smaller = is_smaller(lhs, rhs);
TRACE("demodulator", tout << "testing is_demodulator:\n"
<< mk_pp(lhs, m_manager) << "\n"
<< mk_pp(rhs, m_manager) << "\n"
<< mk_pp(lhs, m) << "\n"
<< mk_pp(rhs, m) << "\n"
<< "subset: " << subset << ", smaller: " << smaller << "\n";);
// We only track uninterpreted functions, everything else is likely too expensive.
if ((subset == +1 || subset == +2) && smaller == +1) {
@ -74,9 +72,9 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
#if 1
// lhs = (not rhs) --> (not lhs) = rhs
expr * not_rhs;
if (m_manager.is_not(rhs, not_rhs) && is_uninterp(not_rhs)) {
if (m.is_not(rhs, not_rhs) && is_uninterp(not_rhs)) {
large = not_rhs;
small = m_manager.mk_not(lhs);
small = m.mk_not(lhs);
return true;
}
#endif
@ -91,23 +89,23 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
#if 1
// (not lhs) = rhs --> lhs = (not rhs)
expr * not_lhs;
if (m_manager.is_not(lhs, not_lhs) && is_uninterp(not_lhs)) {
if (m.is_not(lhs, not_lhs) && is_uninterp(not_lhs)) {
large = not_lhs;
small = m_manager.mk_not(rhs);
small = m.mk_not(rhs);
return true;
}
#endif
}
} else if (m_manager.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0))) {
} else if (m.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0))) {
// this is like (not (f ... )) --> (= (f ...) false)
large = to_app(qe)->get_arg(0);
small = m_manager.mk_false();
small = m.mk_false();
return true;
} else if (is_uninterp(qe)) {
// this is like (f ... ) --> (= (f ...) true)
large = to_app(qe);
small = m_manager.mk_true();
small = m.mk_true();
return true;
}
}
@ -128,7 +126,7 @@ public:
int ufbv_rewriter::is_subset(expr * e1, expr * e2) const {
uint_set ev1, ev2;
if (m_manager.is_value(e1))
if (m.is_value(e1))
return 1; // values are always a subset!
var_set_proc proc1(ev1);
@ -146,9 +144,9 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const {
unsigned sz1 = 0, sz2 = 0;
// values are always smaller!
if (m_manager.is_value(e1))
if (m.is_value(e1))
return +1;
else if (m_manager.is_value(e2))
else if (m.is_value(e2))
return -1;
// interpreted stuff is always better than uninterpreted.
@ -217,7 +215,7 @@ void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demo
SASSERT(large->get_kind() == AST_APP);
SASSERT(demodulator);
SASSERT(large && small);
TRACE("demodulator_fwd", tout << "INSERT: " << mk_pp(demodulator, m_manager) << std::endl; );
TRACE("demodulator_fwd", tout << "INSERT: " << mk_pp(demodulator, m) << std::endl; );
func_decl * fd = to_app(large)->get_decl();
@ -231,9 +229,9 @@ void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demo
SASSERT(it->m_value);
it->m_value->insert(demodulator);
m_manager.inc_ref(demodulator);
m_manager.inc_ref(large);
m_manager.inc_ref(small);
m.inc_ref(demodulator);
m.inc_ref(large);
m.inc_ref(small);
m_demodulator2lhs_rhs.insert(demodulator, expr_pair(large, small));
}
@ -243,9 +241,9 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) {
fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f);
if (it != m_fwd_idx.end()) {
demodulator2lhs_rhs::iterator fit = m_demodulator2lhs_rhs.find_iterator(demodulator);
m_manager.dec_ref(fit->m_value.first);
m_manager.dec_ref(fit->m_value.second);
m_manager.dec_ref(demodulator);
m.dec_ref(fit->m_value.first);
m.dec_ref(fit->m_value.second);
m.dec_ref(demodulator);
m_demodulator2lhs_rhs.erase(demodulator);
it->m_value->erase(demodulator);
} else {
@ -254,12 +252,12 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) {
}
bool ufbv_rewriter::check_fwd_idx_consistency() {
for (fwd_idx_map::iterator it = m_fwd_idx.begin(); it != m_fwd_idx.end() ; it++ ) {
quantifier_set * set = it->m_value;
for (auto & kv : m_fwd_idx) {
quantifier_set * set = kv.m_value;
SASSERT(set);
for (quantifier_set::iterator sit = set->begin(); sit != set->end(); sit++) {
if (!m_demodulator2lhs_rhs.contains(*sit)) return false;
for (auto e : *set) {
if (!m_demodulator2lhs_rhs.contains(e))
return false;
}
}
@ -267,20 +265,20 @@ bool ufbv_rewriter::check_fwd_idx_consistency() {
}
void ufbv_rewriter::show_fwd_idx(std::ostream & out) {
for (fwd_idx_map::iterator it = m_fwd_idx.begin(); it != m_fwd_idx.end() ; it++ ) {
quantifier_set * set = it->m_value;
for (auto & kv : m_fwd_idx) {
quantifier_set * set = kv.m_value;
SASSERT(!set);
out << it->m_key->get_name() << ": " << std::endl;
out << kv.m_key->get_name() << ": " << std::endl;
for (quantifier_set::iterator sit = set->begin(); sit != set->end(); sit++) {
out << std::hex << (size_t)*sit << std::endl;
for (auto e : *set) {
out << std::hex << (size_t)e << std::endl;
}
}
out << "D2LR: " << std::endl;
for (demodulator2lhs_rhs::iterator it = m_demodulator2lhs_rhs.begin(); it != m_demodulator2lhs_rhs.end() ; it++) {
out << (size_t) it->m_key << std::endl;
for (auto & kv : m_demodulator2lhs_rhs) {
out << (size_t) kv.m_key << std::endl;
}
}
@ -288,11 +286,8 @@ bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector<expr> & m_new_args, expr_
fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f);
if (it != m_fwd_idx.end()) {
TRACE("demodulator_bug", tout << "trying to rewrite: " << f->get_name() << " args:\n";
for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m_manager) << "\n"; });
quantifier_set::iterator dit = it->m_value->begin();
quantifier_set::iterator dend = it->m_value->end();
for ( ; dit != dend ; dit++ ) {
quantifier * d = *dit;
for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m) << "\n"; });
for (quantifier* d : *it->m_value) {
SASSERT(m_demodulator2lhs_rhs.contains(d));
expr_pair l_s;
@ -302,12 +297,12 @@ bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector<expr> & m_new_args, expr_
if (large->get_num_args() != m_new_args.size())
continue;
TRACE("demodulator_bug", tout << "Matching with demodulator: " << mk_pp(d, m_manager) << std::endl; );
TRACE("demodulator_bug", tout << "Matching with demodulator: " << mk_pp(d, m) << std::endl; );
SASSERT(large->get_decl() == f);
if (m_match_subst(large, l_s.second, m_new_args.c_ptr(), np)) {
TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(l_s.second, m_manager) << "\n===>\n" << mk_pp(np, m_manager) << "\n";);
TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(l_s.second, m) << "\n===>\n" << mk_pp(np, m) << "\n";);
return true;
}
}
@ -334,7 +329,7 @@ bool ufbv_rewriter::rewrite_visit_children(app * a) {
if (m_rewrite_todo[i - 1] == v) {
recursive = true;
TRACE("demodulator", tout << "Detected demodulator cycle: " <<
mk_pp(a, m_manager) << " --> " << mk_pp(v, m_manager) << std::endl;);
mk_pp(a, m) << " --> " << mk_pp(v, m) << std::endl;);
m_rewrite_cache.insert(e, expr_bool_pair(v, true));
break;
}
@ -356,7 +351,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
if (m_fwd_idx.empty())
return n;
TRACE("demodulator", tout << "rewrite: " << mk_pp(n, m_manager) << std::endl; );
TRACE("demodulator", tout << "rewrite: " << mk_pp(n, m) << std::endl; );
app * a;
SASSERT(m_rewrite_todo.empty());
@ -367,7 +362,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
TRACE("demodulator_stack", tout << "STACK: " << std::endl;
for ( unsigned i = 0; i<m_rewrite_todo.size(); i++)
tout << std::dec << i << ": " << std::hex << (size_t)m_rewrite_todo[i] <<
" = " << mk_pp(m_rewrite_todo[i], m_manager) << std::endl;
" = " << mk_pp(m_rewrite_todo[i], m) << std::endl;
);
expr * e = m_rewrite_todo.back();
@ -406,7 +401,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
all_untouched = false;
m_new_args.push_back(n_child);
}
expr_ref np(m_manager);
expr_ref np(m);
if (rewrite1(f, m_new_args, np)) {
rewrite_cache(e, np, false);
// No pop.
@ -415,15 +410,15 @@ expr * ufbv_rewriter::rewrite(expr * n) {
rewrite_cache(e, actual, true);
}
else {
expr_ref na(m_manager);
if (f->get_family_id() != m_manager.get_basic_family_id())
na = m_manager.mk_app(f, m_new_args.size(), m_new_args.c_ptr());
expr_ref na(m);
if (f->get_family_id() != m.get_basic_family_id())
na = m.mk_app(f, m_new_args.size(), m_new_args.c_ptr());
else
m_bsimp.mk_app(f, m_new_args.size(), m_new_args.c_ptr(), na);
TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m_manager) << "\nnew_args: \n";
for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m_manager) << "\n"; }
TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m) << "\nnew_args: \n";
for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m) << "\n"; }
tout << "=====>\n";
tout << "na:\n " << mk_pp(na, m_manager) << "\n";);
tout << "na:\n " << mk_pp(na, m) << "\n";);
rewrite_cache(e, na, true);
}
m_rewrite_todo.pop_back();
@ -436,10 +431,10 @@ expr * ufbv_rewriter::rewrite(expr * n) {
const expr_bool_pair ebp = m_rewrite_cache.get(body);
SASSERT(ebp.second);
expr * new_body = ebp.first;
quantifier_ref q(m_manager);
q = m_manager.update_quantifier(to_quantifier(actual), new_body);
quantifier_ref q(m);
q = m.update_quantifier(to_quantifier(actual), new_body);
m_new_exprs.push_back(q);
expr_ref new_q = elim_unused_vars(m_manager, q, params_ref());
expr_ref new_q = elim_unused_vars(m, q, params_ref());
m_new_exprs.push_back(new_q);
rewrite_cache(e, new_q, true);
m_rewrite_todo.pop_back();
@ -458,7 +453,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
SASSERT(ebp.second);
expr * r = ebp.first;
TRACE("demodulator", tout << "rewrite result: " << mk_pp(r, m_manager) << std::endl; );
TRACE("demodulator", tout << "rewrite result: " << mk_pp(r, m) << std::endl; );
return r;
}
@ -517,18 +512,12 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) {
SASSERT(it->m_value);
expr_set temp;
expr_set::iterator sit = it->m_value->begin();
expr_set::iterator send = it->m_value->end();
for ( ; sit != send ; sit++ ) {
expr * p = *sit;
for (expr* p : *it->m_value) {
if (m_processed.contains(p))
temp.insert(p);
}
sit = temp.begin();
send = temp.end();
for ( ; sit != send; sit++) {
expr * p = *sit;
for (expr * p : temp) {
// remove p from m_processed and m_back_idx
m_processed.remove(p);
remove_back_idx_proc proc(m_back_idx, p); // this could change it->m_value, thus we need the `temp' set.
@ -605,18 +594,13 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
if (it != m_back_idx.end()) {
SASSERT(it->m_value);
expr_set all_occurrences;
expr_ref l(m_manager);
expr_ref l(m);
expr_set::iterator esit = it->m_value->begin();
expr_set::iterator esend = it->m_value->end();
for ( ; esit != esend ; esit++)
all_occurrences.insert(*esit);
for (auto s : *it->m_value)
all_occurrences.insert(s);
// Run over all f-demodulators
esit = all_occurrences.begin();
esend = all_occurrences.end();
for ( ; esit != esend ; esit++ ) {
expr * occ = *esit;
for (expr* occ : all_occurrences) {
if (!is_quantifier(occ))
continue;
@ -625,15 +609,15 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
demodulator2lhs_rhs::iterator d2lr_it = m_demodulator2lhs_rhs.find_iterator(to_quantifier(occ));
if (d2lr_it != m_demodulator2lhs_rhs.end()) {
l = d2lr_it->m_value.first;
quantifier_ref d(m_manager);
func_decl_ref df(m_manager);
quantifier_ref d(m);
func_decl_ref df(m);
d = to_quantifier(occ);
df = to_app(l)->get_decl();
// Now we know there is an occurrence of f in d
// if n' can rewrite d {
if (can_rewrite(d, lhs)) {
TRACE("demodulator", tout << "Rescheduling: " << std::endl << mk_pp(d, m_manager) << std::endl; );
TRACE("demodulator", tout << "Rescheduling: " << std::endl << mk_pp(d, m) << std::endl; );
// remove d from m_fwd_idx
remove_fwd_idx(df, d);
// remove d from m_back_idx
@ -647,16 +631,11 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
}
}
}
//for (ptr_vector<expr>::iterator it = to_remove.begin(); it != to_remove.end(); it++) {
// expr * d = *it;
// remove_back_idx_proc proc(m_manager, m_back_idx, d);
// for_each_expr(proc, d);
//}
}
void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
if (m_manager.proofs_enabled()) {
void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs,
expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
if (m.proofs_enabled()) {
TRACE("tactic", tout << "PRE_DEMODULATOR=true is not supported when proofs are enabled.";);
// Let us not waste time with proof production
new_exprs.append(n, exprs);
@ -666,7 +645,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
TRACE("demodulator", tout << "before demodulator:\n";
for ( unsigned i = 0 ; i < n ; i++ )
tout << mk_pp(exprs[i], m_manager) << std::endl; );
tout << mk_pp(exprs[i], m) << std::endl; );
// Initially, m_todo contains all formulas. That is, it contains the argument exprs. m_fwd_idx, m_processed, m_back_idx are empty.
unsigned max_vid = 0;
@ -679,17 +658,18 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
while (!m_todo.empty()) {
// let n be the next formula in m_todo.
expr_ref cur(m_manager);
expr_ref cur(m);
cur = m_todo.back();
m_todo.pop_back();
// rewrite cur using m_fwd_idx, and let n' be the result.
expr * np = rewrite(cur);
expr_ref np(rewrite(cur), m);
// at this point, it should be the case that there is no demodulator in m_fwd_idx that can rewrite n'.
SASSERT(rewrite(np)==np);
// unless there is a demodulator cycle
// SASSERT(rewrite(np)==np);
// if (n' is not a demodulator) {
expr_ref large(m_manager), small(m_manager);
expr_ref large(m), small(m);
if (!is_demodulator(np, large, small)) {
// insert n' into m_processed
m_processed.insert(np);
@ -699,8 +679,8 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
} else {
// np is a demodulator that allows us to replace 'large' with 'small'.
TRACE("demodulator", tout << "Found demodulator: " << std::endl;
tout << mk_pp(large.get(), m_manager) << std::endl << " ---> " <<
std::endl << mk_pp(small.get(), m_manager) << std::endl; );
tout << mk_pp(large.get(), m) << std::endl << " ---> " <<
std::endl << mk_pp(small.get(), m) << std::endl; );
TRACE("demodulator_s", tout << "Found demodulator: " << std::endl;
tout << to_app(large)->get_decl()->get_name() <<
@ -709,7 +689,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
tout << to_app(small)->get_decl()->get_name() <<
"[" << to_app(small)->get_depth() << "]" << std::endl;
else
tout << mk_pp(small.get(), m_manager) << std::endl; );
tout << mk_pp(small.get(), m) << std::endl; );
// let f be the top symbol of n'
SASSERT(is_app(large));
@ -728,35 +708,26 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
}
// the result is the contents of m_processed + all demodulators in m_fwd_idx.
obj_hashtable<expr>::iterator pit = m_processed.begin();
obj_hashtable<expr>::iterator pend = m_processed.end();
for ( ; pit != pend ; pit++ ) {
new_exprs.push_back(*pit);
TRACE("demodulator", tout << mk_pp(*pit, m_manager) << std::endl; );
for (expr* e : m_processed) {
new_exprs.push_back(e);
TRACE("demodulator", tout << mk_pp(e, m) << std::endl; );
}
fwd_idx_map::iterator fit = m_fwd_idx.begin();
fwd_idx_map::iterator fend = m_fwd_idx.end();
for ( ; fit != fend ; fit++ ) {
if (fit->m_value) {
quantifier_set::iterator dit = fit->m_value->begin();
quantifier_set::iterator dend = fit->m_value->end();
for ( ; dit != dend ; dit++ ) {
expr * e = *dit;
for (auto const& kv : m_fwd_idx) {
if (kv.m_value) {
for (expr* e : *kv.m_value) {
new_exprs.push_back(e);
TRACE("demodulator", tout << mk_pp(*dit, m_manager) << std::endl; );
TRACE("demodulator", tout << mk_pp(e, m) << std::endl; );
}
}
}
TRACE("demodulator", tout << "after demodulator:\n";
for ( unsigned i = 0 ; i < new_exprs.size() ; i++ )
tout << mk_pp(new_exprs[i].get(), m_manager) << std::endl; );
TRACE("demodulator", tout << "after demodulator:\n" << new_exprs << "\n";);
}
ufbv_rewriter::match_subst::match_subst(ast_manager & m):
m_manager(m),
m(m),
m_subst(m) {
}

12
src/tactic/ufbv/ufbv_rewriter.h
View file

@ -101,11 +101,11 @@ class ufbv_rewriter {
typedef std::pair<expr *, bool> expr_bool_pair;
class plugin {
ast_manager& m_manager;
ast_manager& m;
public:
plugin(ast_manager& m): m_manager(m) { }
void ins_eh(expr* k, expr_bool_pair v) { m_manager.inc_ref(k); m_manager.inc_ref(v.first); }
void del_eh(expr* k, expr_bool_pair v) { m_manager.dec_ref(k); m_manager.dec_ref(v.first); }
plugin(ast_manager& m): m(m) { }
void ins_eh(expr* k, expr_bool_pair v) { m.inc_ref(k); m.inc_ref(v.first); }
void del_eh(expr* k, expr_bool_pair v) { m.dec_ref(k); m.dec_ref(v.first); }
static unsigned to_int(expr const * k) { return k->get_id(); }
};
typedef array_map<expr*, expr_bool_pair, plugin> expr_map;
@ -127,7 +127,7 @@ class ufbv_rewriter {
void reset();
ast_manager & m_manager;
ast_manager & m;
substitution m_subst;
cache m_cache;
svector<expr_pair> m_todo;
@ -157,7 +157,7 @@ class ufbv_rewriter {
bool operator()(expr * t, expr * i);
};
ast_manager & m_manager;
ast_manager & m;
match_subst m_match_subst;
bool_rewriter m_bsimp;
fwd_idx_map m_fwd_idx;