mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 18:20:22 +00:00
Code Activity

Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-04-07 21:19:20 +01:00
parent 9a757ffffe
commit 27a1758857
19 changed files with 795 additions and 776 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -36,7 +36,7 @@ static bool is_neg_var(ast_manager & m, expr * e, unsigned 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
The last case can be viewed
*/
bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
// (not (= VAR t)) and (not (iff VAR t)) cases
@ -49,7 +49,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
return false;
if (!is_var(lhs, num_decls))
std::swap(lhs, rhs);
SASSERT(is_var(lhs, num_decls));
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;
@ -67,7 +67,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
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));
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;
@ -83,11 +83,11 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
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);
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";);
@ -134,11 +134,11 @@ void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
pr = m_manager.mk_transitivity(pr, curr_pr);
}
} while (q != r && is_quantifier(r));
// Eliminate variables that have become unused
if (reduced && is_forall(r)) {
quantifier * q = to_quantifier(r);
elim_unused_vars(m_manager, q, r);
elim_unused_vars(m_manager, q, params_ref(), r);
if (m_manager.proofs_enabled()) {
proof * p1 = m_manager.mk_elim_unused_vars(q, r);
pr = m_manager.mk_transitivity(pr, p1);
@ -153,24 +153,24 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
r = q;
return;
}
expr * e = q->get_expr();
unsigned num_decls = q->get_num_decls();
var * v = 0;
expr_ref t(m_manager);
expr_ref t(m_manager);
if (m_manager.is_or(e)) {
unsigned num_args = to_app(e)->get_num_args();
unsigned i = 0;
unsigned diseq_count = 0;
unsigned largest_vinx = 0;
m_map.reset();
m_pos2var.reset();
m_inx2var.reset();
m_pos2var.reserve(num_args, -1);
// Find all disequalities
for (; i < num_args; i++) {
if (is_var_diseq(to_app(e)->get_arg(i), num_decls, v, t)) {
@ -192,7 +192,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
get_elimination_order();
SASSERT(m_order.size() <= diseq_count); // some might be missing because of cycles
if (!m_order.empty()) {
if (!m_order.empty()) {
create_substitution(largest_vinx + 1);
apply_substitution(q, r);
}
@ -202,22 +202,22 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
r = q;
}
}
// Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses.
// 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();
}
else
else
r = q;
if (m_manager.proofs_enabled()) {
pr = r == q ? 0 : m_manager.mk_der(q, r);
}
}
}
void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
order.reset();
// eliminate self loops, and definitions containing quantifiers.
bool found = false;
for (unsigned i = 0; i < definitions.size(); i++) {
@ -228,7 +228,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
else
found = true; // found at least one candidate
}
if (!found)
return;
@ -329,14 +329,14 @@ void der::get_elimination_order() {
// der::top_sort ts(m_manager);
der_sort_vars(m_inx2var, m_map, m_order);
TRACE("der",
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 << std::endl;
);
}
@ -359,24 +359,24 @@ void der::create_substitution(unsigned sz) {
void der::apply_substitution(quantifier * q, expr_ref & r) {
expr * e = q->get_expr();
unsigned num_args=to_app(e)->get_num_args();
unsigned num_args=to_app(e)->get_num_args();
// get a new expression
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[x] != 0)
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 new_e(m_manager);
expr_ref new_e(m_manager);
m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e);
// don't forget to update the quantifier patterns
expr_ref_buffer new_patterns(m_manager);
expr_ref_buffer new_no_patterns(m_manager);
@ -392,7 +392,7 @@ void der::apply_substitution(quantifier * q, expr_ref & r) {
new_no_patterns.push_back(new_nopat);
}
r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.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);
}
@ -404,9 +404,9 @@ struct der_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m() const { return m_der.m(); }
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {

3
src/ast/rewriter/rewriter_params.pyg
View file

@ -8,5 +8,6 @@ def_module_params('rewriter',
("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."),
("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),
("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."),
("cache_all", BOOL, False, "cache all intermediate results.")))
("cache_all", BOOL, False, "cache all intermediate results."),
("ignore_patterns_on_ground_qbody", BOOL, True, "ignores patterns on quantifiers that don't mention their bound variables.")))

72
src/ast/rewriter/th_rewriter.cpp
View file

@ -54,6 +54,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
bool m_cache_all;
bool m_push_ite_arith;
bool m_push_ite_bv;
bool m_ignore_patterns_on_ground_qbody;
// substitution support
expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
@ -70,8 +71,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_cache_all = p.cache_all();
m_push_ite_arith = p.push_ite_arith();
m_push_ite_bv = p.push_ite_bv();
m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
}
void updt_params(params_ref const & p) {
m_b_rw.updt_params(p);
m_a_rw.updt_params(p);
@ -82,7 +84,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
updt_local_params(p);
}
bool flat_assoc(func_decl * f) const {
bool flat_assoc(func_decl * f) const {
if (!m_flat) return false;
family_id fid = f->get_family_id();
if (fid == null_family_id)
@ -98,10 +100,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
bool rewrite_patterns() const { return false; }
bool cache_all_results() const { return m_cache_all; }
bool max_steps_exceeded(unsigned num_steps) const {
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("simplifier");
if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(Z3_MAX_MEMORY_MSG);
@ -179,13 +181,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
st = m_ar_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
if (k == OP_EQ || k == OP_IFF) {
SASSERT(num == 2);
st = apply_tamagotchi(args[0], args[1], result);
st = apply_tamagotchi(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
@ -239,13 +241,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
else {
if (SWAP) {
result = m().mk_ite(ite->get_arg(0),
result = m().mk_ite(ite->get_arg(0),
m().mk_app(p, value, ite->get_arg(1)),
m().mk_app(p, value, ite->get_arg(2)));
return BR_REWRITE2;
}
else {
result = m().mk_ite(ite->get_arg(0),
result = m().mk_ite(ite->get_arg(0),
m().mk_app(p, ite->get_arg(1), value),
m().mk_app(p, ite->get_arg(2), value));
return BR_REWRITE2;
@ -257,7 +259,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// ite-value-tree := (ite c <subtree> <subtree>)
// subtree := value
// | (ite c <subtree> <subtree>)
//
//
bool is_ite_value_tree(expr * t) {
if (!m().is_ite(t))
return false;
@ -281,7 +283,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
return true;
}
br_status pull_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
if (num == 2 && m().is_bool(f->get_range()) && !m().is_bool(args[0])) {
if (m().is_ite(args[0])) {
@ -325,7 +327,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
if (!is_app(t))
return false;
family_id fid = to_app(t)->get_family_id();
return ((fid == m_a_rw.get_fid() && m_push_ite_arith) ||
return ((fid == m_a_rw.get_fid() && m_push_ite_arith) ||
(fid == m_bv_rw.get_fid() && m_push_ite_bv));
}
@ -349,7 +351,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
return false;
}
/**
\brief Try to "unify" t1 and t2
Examples
@ -463,7 +465,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
// terms matched...
bool is_int = m_a_util.is_int(t1);
if (!new_t1)
if (!new_t1)
new_t1 = m_a_util.mk_numeral(rational(0), is_int);
if (!new_t2)
new_t2 = m_a_util.mk_numeral(rational(0), is_int);
@ -476,7 +478,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
args.push_back(arg);
}
SASSERT(!args.empty());
if (args.size() == 1)
if (args.size() == 1)
c = args[0];
else
c = m_a_util.mk_add(args.size(), args.c_ptr());
@ -518,7 +520,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// Apply transformations of the form
//
// (ite c (+ k1 a) (+ k2 a)) --> (+ (ite c k1 k2) a)
// (ite c (+ k1 a) (+ k2 a)) --> (+ (ite c k1 k2) a)
// (ite c (* k1 a) (* k2 a)) --> (* (ite c k1 k2) a)
//
// These transformations are useful for bit-vector problems, since
@ -536,7 +538,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
if (unify(t, e, f_prime, new_t, new_e, common, first)) {
if (first)
result = m().mk_app(f_prime, common, m().mk_ite(c, new_t, new_e));
else
else
result = m().mk_app(f_prime, m().mk_ite(c, new_t, new_e), common);
return BR_DONE;
}
@ -558,7 +560,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
result_pr = 0;
br_status st = reduce_app_core(f, num, args, result);
if (st != BR_DONE && st != BR_FAILED) {
CTRACE("th_rewriter_step", st != BR_FAILED,
CTRACE("th_rewriter_step", st != BR_FAILED,
tout << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";);
@ -576,7 +578,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
else
st = pull_ite(result);
}
CTRACE("th_rewriter_step", st != BR_FAILED,
CTRACE("th_rewriter_step", st != BR_FAILED,
tout << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";);
@ -593,28 +595,28 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
quantifier_ref q1(m());
proof * p1 = 0;
if (is_quantifier(new_body) &&
if (is_quantifier(new_body) &&
to_quantifier(new_body)->is_forall() == old_q->is_forall() &&
!old_q->has_patterns() &&
!to_quantifier(new_body)->has_patterns()) {
quantifier * nested_q = to_quantifier(new_body);
ptr_buffer<sort> sorts;
buffer<symbol> names;
buffer<symbol> names;
sorts.append(old_q->get_num_decls(), old_q->get_decl_sorts());
names.append(old_q->get_num_decls(), old_q->get_decl_names());
sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
names.append(nested_q->get_num_decls(), nested_q->get_decl_names());
q1 = m().mk_quantifier(old_q->is_forall(),
sorts.size(),
sorts.c_ptr(),
@ -624,9 +626,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
old_q->get_qid(),
old_q->get_skid(),
0, 0, 0, 0);
SASSERT(is_well_sorted(m(), q1));
if (m().proofs_enabled()) {
SASSERT(old_q->get_expr() == new_body);
p1 = m().mk_pull_quant(old_q, q1);
@ -635,24 +637,24 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
else {
ptr_buffer<expr> new_patterns_buf;
ptr_buffer<expr> new_no_patterns_buf;
new_patterns_buf.append(old_q->get_num_patterns(), new_patterns);
new_no_patterns_buf.append(old_q->get_num_no_patterns(), new_no_patterns);
remove_duplicates(new_patterns_buf);
remove_duplicates(new_no_patterns_buf);
q1 = m().update_quantifier(old_q,
q1 = m().update_quantifier(old_q,
new_patterns_buf.size(), new_patterns_buf.c_ptr(), new_no_patterns_buf.size(), new_no_patterns_buf.c_ptr(),
new_body);
TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";);
SASSERT(is_well_sorted(m(), q1));
}
elim_unused_vars(m(), q1, result);
elim_unused_vars(m(), q1, params_ref(), result);
TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m()) << "\n";);
result_pr = 0;
if (m().proofs_enabled()) {
proof * p2 = 0;
@ -758,7 +760,7 @@ unsigned th_rewriter::get_num_steps() const {
void th_rewriter::cleanup() {
ast_manager & m = m_imp->m();
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
m_imp = alloc(imp, m, m_params);
}
void th_rewriter::reset() {

14
src/ast/rewriter/var_subst.cpp
View file

@ -39,10 +39,16 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp
tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";);
}
unused_vars_eliminator::unused_vars_eliminator(ast_manager & m, params_ref const & params) :
m(m), m_subst(m), m_params(params)
{
m_ignore_patterns_on_ground_qbody = m_params.get_bool("ignore_patterns_on_ground_qbody", true);
}
void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
SASSERT(is_well_sorted(m, q));
if (is_ground(q->get_expr())) {
// ignore patterns if the body is a ground formula.
if (m_ignore_patterns_on_ground_qbody && is_ground(q->get_expr())) {
// Ignore patterns if the body is a ground formula.
result = q->get_expr();
return;
}
@ -146,8 +152,8 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
SASSERT(is_well_sorted(m, result));
}
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
unused_vars_eliminator el(m);
void elim_unused_vars(ast_manager & m, quantifier * q, params_ref const & params, expr_ref & result) {
unused_vars_eliminator el(m, params);
el(q, result);
}

21
src/ast/rewriter/var_subst.h
View file

@ -21,6 +21,7 @@ Notes:
#include"rewriter.h"
#include"used_vars.h"
#include"params.h"
/**
\brief Alias for var_shifter class.
@ -31,7 +32,7 @@ typedef var_shifter shift_vars;
\brief Variable substitution functor. It substitutes variables by expressions.
The expressions may contain variables.
*/
class var_subst {
class var_subst {
beta_reducer m_reducer;
bool m_std_order;
public:
@ -39,7 +40,7 @@ public:
bool std_order() const { return m_std_order; }
/**
When std_order() == true,
When std_order() == true,
I'm using the same standard used in quantifier instantiation.
(VAR 0) is stored in the last position of the array.
...
@ -55,15 +56,17 @@ public:
\brief Eliminate the unused variables from \c q. Store the result in \c r.
*/
class unused_vars_eliminator {
ast_manager& m;
var_subst m_subst;
used_vars m_used;
ast_manager & m;
var_subst m_subst;
used_vars m_used;
params_ref m_params;
bool m_ignore_patterns_on_ground_qbody;
public:
unused_vars_eliminator(ast_manager& m): m(m), m_subst(m) {}
unused_vars_eliminator(ast_manager & m, params_ref const & params);
void operator()(quantifier* q, expr_ref& r);
};
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & r);
void elim_unused_vars(ast_manager & m, quantifier * q, params_ref const & params, expr_ref & r);
/**
\brief Instantiate quantifier q using the given exprs.
@ -86,7 +89,7 @@ class expr_free_vars {
expr_sparse_mark m_mark;
ptr_vector<sort> m_sorts;
ptr_vector<expr> m_todo;
public:
public:
void reset();
void operator()(expr* e);
void accumulate(expr* e);
@ -96,7 +99,7 @@ public:
bool contains(unsigned idx) const { return idx < m_sorts.size() && m_sorts[idx] != 0; }
void set_default_sort(sort* s);
void reverse() { m_sorts.reverse(); }
sort*const* c_ptr() const { return m_sorts.c_ptr(); }
sort*const* c_ptr() const { return m_sorts.c_ptr(); }
};
#endif