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

fix #3752

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 22:56:35 -07:00
parent 2f80acb1bc
commit 7ae9734db2
2 changed files with 99 additions and 130 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

222
src/ast/rewriter/der.cpp
View file

@ -22,6 +22,7 @@ Revision History:
#include "ast/occurs.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
@ -30,85 +31,65 @@ static bool is_var(expr * e, unsigned num_decls) {
return is_var(e) && to_var(e)->get_idx() < num_decls;
}
static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) {
return m.is_not(e) && is_var(to_app(e)->get_arg(0)) && to_var(to_app(e)->get_arg(0))->get_idx() < num_decls;
static bool is_neg_var(ast_manager & m, expr * e, var*& v, unsigned num_decls) {
expr* n = nullptr;
return m.is_not(e, n) && is_var(n) && (v = to_var(n), v->get_idx() < num_decls);
}
/**
\brief Return true if \c e is of the form (not (= VAR t)) or (not (iff VAR t)) or (iff VAR t) or (iff (not VAR) t) or (VAR IDX) or (not (VAR IDX)).
The last case can be viewed
Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles...
*/
bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
// (not (= VAR t)) and (not (iff VAR t)) cases
expr *eq, * lhs, *rhs;
if (m_manager.is_not(e, eq) && m_manager.is_eq(eq, lhs, rhs)) {
if (!is_var(lhs, num_decls) && !is_var(rhs, num_decls))
return false;
auto set_result = [&](var *w, expr* s) {
v = w;
t = s;
TRACE("der", tout << mk_pp(e, m) << "\n";);
return true;
};
// (not (= VAR t))
if (m.is_not(e, eq) && m.is_eq(eq, lhs, rhs)) {
if (!is_var(lhs, num_decls))
std::swap(lhs, rhs);
SASSERT(is_var(lhs, num_decls));
// Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles...
// if (occurs(lhs, rhs)) {
// return false;
// }
v = to_var(lhs);
t = rhs;
TRACE("der", tout << mk_pp(e, m_manager) << "\n";);
return true;
if (!is_var(lhs, num_decls))
return false;
return set_result(to_var(lhs), rhs);
}
// (iff VAR t) and (iff (not VAR) t) cases
else if (m_manager.is_eq(e, lhs, rhs) && m_manager.is_bool(lhs)) {
// (= VAR t)
if (m.is_eq(e, lhs, rhs) && m.is_bool(lhs)) {
// (iff VAR t) case
if (is_var(lhs, num_decls) || is_var(rhs, num_decls)) {
if (!is_var(lhs, num_decls))
std::swap(lhs, rhs);
SASSERT(is_var(lhs, num_decls));
// Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles...
// if (occurs(lhs, rhs)) {
// return false;
// }
v = to_var(lhs);
t = m_manager.mk_not(rhs);
m_new_exprs.push_back(t);
TRACE("der", tout << mk_pp(e, m_manager) << "\n";);
return true;
if (!is_var(lhs, num_decls))
std::swap(lhs, rhs);
if (is_var(lhs, num_decls)) {
rhs = mk_not(m, rhs);
m_new_exprs.push_back(rhs);
return set_result(to_var(lhs), rhs);
}
// (iff (not VAR) t) case
else if (is_neg_var(m_manager, lhs, num_decls) || is_neg_var(m_manager, rhs, num_decls)) {
if (!is_neg_var(m_manager, lhs, num_decls))
std::swap(lhs, rhs);
SASSERT(is_neg_var(m_manager, lhs, num_decls));
expr * lhs_var = to_app(lhs)->get_arg(0);
// Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles...
// if (occurs(lhs_var, rhs)) {
// return false;
// }
v = to_var(lhs_var);
t = rhs;
TRACE("der", tout << mk_pp(e, m_manager) << "\n";);
return true;
}
else {
return false;
if (!is_neg_var(m, lhs, v, num_decls))
std::swap(lhs, rhs);
if (is_neg_var(m, lhs, v, num_decls)) {
return set_result(v, rhs);
}
return false;
}
// VAR != false case
else if (is_var(e, num_decls)) {
t = m_manager.mk_false();
v = to_var(e);
TRACE("der", tout << mk_pp(e, m_manager) << "\n";);
return true;
// VAR
if (is_var(e, num_decls)) {
return set_result(to_var(e), m.mk_false());
}
// VAR != true case
else if (is_neg_var(m_manager, e, num_decls)) {
t = m_manager.mk_true();
v = to_var(to_app(e)->get_arg(0));
TRACE("der", tout << mk_pp(e, m_manager) << "\n";);
return true;
}
else {
return false;
// (not VAR)
if (is_neg_var(m, e, v, num_decls)) {
return set_result(v, m.mk_true());
}
return false;
}
void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
@ -116,27 +97,28 @@ void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
pr = nullptr;
r = q;
TRACE("der", tout << mk_pp(q, m_manager) << "\n";);
TRACE("der", tout << mk_pp(q, m) << "\n";);
// Keep applying it until r doesn't change anymore
do {
proof_ref curr_pr(m_manager);
proof_ref curr_pr(m);
q = to_quantifier(r);
reduce1(q, r, curr_pr);
if (q != r)
reduced = true;
if (m_manager.proofs_enabled()) {
pr = m_manager.mk_transitivity(pr, curr_pr);
if (m.proofs_enabled()) {
pr = m.mk_transitivity(pr, curr_pr);
}
} while (q != r && is_quantifier(r));
}
while (q != r && is_quantifier(r));
// Eliminate variables that have become unused
if (reduced && is_forall(r)) {
quantifier * q = to_quantifier(r);
r = elim_unused_vars(m_manager, q, params_ref());
if (m_manager.proofs_enabled()) {
proof * p1 = m_manager.mk_elim_unused_vars(q, r);
pr = m_manager.mk_transitivity(pr, p1);
r = elim_unused_vars(m, q, params_ref());
if (m.proofs_enabled()) {
proof * p1 = m.mk_elim_unused_vars(q, r);
pr = m.mk_transitivity(pr, p1);
}
}
m_new_exprs.reset();
@ -152,11 +134,10 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
expr * e = q->get_expr();
unsigned num_decls = q->get_num_decls();
var * v = nullptr;
expr_ref t(m_manager);
expr_ref t(m);
if (m_manager.is_or(e)) {
if (m.is_or(e)) {
unsigned num_args = to_app(e)->get_num_args();
unsigned i = 0;
unsigned diseq_count = 0;
unsigned largest_vinx = 0;
@ -167,11 +148,11 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
m_pos2var.reserve(num_args, -1);
// Find all disequalities
for (; i < num_args; i++) {
for (unsigned i = 0; i < num_args; i++) {
if (is_var_diseq(to_app(e)->get_arg(i), num_decls, v, t)) {
unsigned idx = v->get_idx();
if(m_map.get(idx, 0) == 0) {
m_map.reserve(idx + 1, 0);
if (m_map.get(idx, nullptr) == nullptr) {
m_map.reserve(idx + 1);
m_inx2var.reserve(idx + 1, 0);
m_map[idx] = t;
@ -193,33 +174,33 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
}
}
else {
TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m_manager) << "\n";);
TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";);
r = q;
}
}
// Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses.
// So, we must perform a occurs check here.
else if (is_var_diseq(e, num_decls, v, t) && !occurs(v, t)) {
r = m_manager.mk_false();
r = m.mk_false();
}
else
r = q;
if (m_manager.proofs_enabled()) {
pr = r == q ? nullptr : m_manager.mk_der(q, r);
if (m.proofs_enabled()) {
pr = r == q ? nullptr : m.mk_der(q, r);
}
}
void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
static void der_sort_vars(ptr_vector<var> & vars, expr_ref_vector & definitions, unsigned_vector & order) {
order.reset();
// eliminate self loops, and definitions containing quantifiers.
bool found = false;
for (unsigned i = 0; i < definitions.size(); i++) {
var * v = vars[i];
expr * t = definitions[i];
expr * t = definitions.get(i);
if (t == nullptr || has_quantifiers(t) || occurs(v, t))
definitions[i] = 0;
definitions[i] = nullptr;
else
found = true; // found at least one candidate
}
@ -236,7 +217,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
unsigned vidx, num;
for (unsigned i = 0; i < definitions.size(); i++) {
if (definitions[i] == 0)
if (!definitions.get(i))
continue;
var * v = vars[i];
SASSERT(v->get_idx() == i);
@ -246,7 +227,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
start:
frame & fr = todo.back();
expr * t = fr.first;
if (t->get_ref_count() > 1 && done.is_marked(t)) {
if (done.is_marked(t)) {
todo.pop_back();
continue;
}
@ -256,23 +237,23 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
if (fr.second == 0) {
CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
// Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
if (definitions.get(vidx, 0) != 0) {
if (definitions.get(vidx, nullptr) != nullptr) {
if (visiting.is_marked(t)) {
// cycle detected: remove t
visiting.reset_mark(t);
definitions[vidx] = 0;
definitions[vidx] = nullptr;
}
else {
visiting.mark(t);
fr.second = 1;
todo.push_back(frame(definitions[vidx], 0));
todo.push_back(frame(definitions.get(vidx), 0));
goto start;
}
}
}
else {
SASSERT(fr.second == 1);
if (definitions.get(vidx, 0) != 0) {
if (definitions.get(vidx, nullptr) != nullptr) {
visiting.reset_mark(t);
order.push_back(vidx);
}
@ -281,8 +262,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
// do nothing
}
}
if (t->get_ref_count() > 1)
done.mark(t);
done.mark(t);
todo.pop_back();
break;
case AST_QUANTIFIER:
@ -294,13 +274,12 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
while (fr.second < num) {
expr * arg = to_app(t)->get_arg(fr.second);
fr.second++;
if (arg->get_ref_count() > 1 && done.is_marked(arg))
if (done.is_marked(arg))
continue;
todo.push_back(frame(arg, 0));
goto start;
}
if (t->get_ref_count() > 1)
done.mark(t);
done.mark(t);
todo.pop_back();
break;
default:
@ -316,23 +295,20 @@ void der::get_elimination_order() {
m_order.reset();
TRACE("top_sort",
tout << "DEFINITIONS: " << std::endl;
for(unsigned i = 0; i < m_map.size(); i++)
if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m_manager) << std::endl;
tout << "DEFINITIONS: " << std::endl;
unsigned i = 0;
for (expr* e : m_map) {
if (e) tout << "VAR " << i << " = " << mk_pp(e, m) << std::endl;
++i;
}
);
// der::top_sort ts(m_manager);
// der::top_sort ts(m);
der_sort_vars(m_inx2var, m_map, m_order);
TRACE("der",
tout << "Elimination m_order:" << std::endl;
for(unsigned i=0; i<m_order.size(); i++)
{
if (i != 0) tout << ",";
tout << m_order[i];
}
tout << std::endl;
);
tout << "Elimination m_order:" << "\n";
tout << m_order << "\n";);
}
void der::create_substitution(unsigned sz) {
@ -340,7 +316,7 @@ void der::create_substitution(unsigned sz) {
m_subst_map.resize(sz, nullptr);
for(unsigned i = 0; i < m_order.size(); i++) {
expr_ref cur(m_map[m_order[i]], m_manager);
expr_ref cur(m_map.get(m_order[i]), m);
// do all the previous substitutions before inserting
expr_ref r = m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr());
@ -359,20 +335,20 @@ void der::apply_substitution(quantifier * q, expr_ref & r) {
m_new_args.reset();
for(unsigned i = 0; i < num_args; i++) {
int x = m_pos2var[i];
if (x != -1 && m_map[x] != 0)
if (x != -1 && m_map.get(x) != nullptr)
continue; // this is a disequality with definition (vanishes)
m_new_args.push_back(to_app(e)->get_arg(i));
}
unsigned sz = m_new_args.size();
expr_ref t(m_manager);
t = (sz == 1) ? m_new_args[0] : m_manager.mk_or(sz, m_new_args.c_ptr());
expr_ref t(m);
t = (sz == 1) ? m_new_args[0] : m.mk_or(sz, m_new_args.c_ptr());
expr_ref new_e = m_subst(t, m_subst_map.size(), m_subst_map.c_ptr());
// don't forget to update the quantifier patterns
expr_ref_buffer new_patterns(m_manager);
expr_ref_buffer new_no_patterns(m_manager);
expr_ref_buffer new_patterns(m);
expr_ref_buffer new_no_patterns(m);
for (unsigned j = 0; j < q->get_num_patterns(); j++) {
new_patterns.push_back(m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()));
}
@ -381,17 +357,16 @@ void der::apply_substitution(quantifier * q, expr_ref & r) {
new_no_patterns.push_back(m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()));
}
r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(),
new_no_patterns.size(), new_no_patterns.c_ptr(), new_e);
r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(),
new_no_patterns.size(), new_no_patterns.c_ptr(), new_e);
}
struct der_rewriter_cfg : public default_rewriter_cfg {
ast_manager& m;
der m_der;
der_rewriter_cfg(ast_manager & m):m_der(m) {}
ast_manager & m() const { return m_der.m(); }
der_rewriter_cfg(ast_manager & m): m(m), m_der(m) {}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
@ -399,8 +374,9 @@ struct der_rewriter_cfg : public default_rewriter_cfg {
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
quantifier_ref q1(m());
q1 = m().update_quantifier(old_q, old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns, new_body);
quantifier_ref q1(m);
q1 = m.update_quantifier(old_q, old_q->get_num_patterns(), new_patterns,
old_q->get_num_no_patterns(), new_no_patterns, new_body);
m_der(q1, result, result_pr);
return true;
}
@ -424,18 +400,12 @@ der_rewriter::~der_rewriter() {
dealloc(m_imp);
}
ast_manager & der_rewriter::m() const {
return m_imp->m();
}
void der_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr) {
m_imp->operator()(t, result, result_pr);
}
void der_rewriter::cleanup() {
ast_manager & m = m_imp->m();
ast_manager & m = m_imp->m_cfg.m;
dealloc(m_imp);
m_imp = alloc(imp, m);
}

7
src/ast/rewriter/der.h
View file

@ -123,11 +123,11 @@ Revision History:
(forall (X Y) (or X /= s C[X])) --> (forall (Y) C[Y])
*/
class der {
ast_manager & m_manager;
ast_manager & m;
var_subst m_subst;
expr_ref_buffer m_new_exprs;
ptr_vector<expr> m_map;
expr_ref_vector m_map;
int_vector m_pos2var;
ptr_vector<var> m_inx2var;
unsigned_vector m_order;
@ -153,8 +153,7 @@ class der {
void reduce1(quantifier * q, expr_ref & r, proof_ref & pr);
public:
der(ast_manager & m):m_manager(m),m_subst(m),m_new_exprs(m),m_subst_map(m),m_new_args(m) {}
ast_manager & m() const { return m_manager; }
der(ast_manager & m):m(m),m_subst(m),m_new_exprs(m),m_map(m), m_subst_map(m),m_new_args(m) {}
void operator()(quantifier * q, expr_ref & r, proof_ref & pr);
};