mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

distribute quantifiers over Booleans

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-14 09:56:43 -07:00
parent 46b1c68f59
commit e2b9e3a6dc
1 changed files with 62 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -767,6 +767,62 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
// Distribute a quantifier over the top-level boolean connective of its body:
// forall x . (A /\ B) --> (forall x. A) /\ (forall x. B)
// forall x . ~(A \/ B) --> (forall x. ~A) /\ (forall x. ~B)
// exists x . (A \/ B) --> (exists x. A) \/ (exists x. B)
// exists x . ~(A /\ B) --> (exists x. ~A) \/ (exists x. ~B)
// Each rule is a validity, and the distributed sub-quantifiers give the
// e-matching engine finer-grained instantiation targets.
bool distribute_quantifier(quantifier * old_q, expr * new_body, expr_ref & result) {
if (old_q->get_kind() == lambda_k)
return false;
if (old_q->has_patterns())
return false;
bool is_forall = old_q->get_kind() == forall_k;
expr_ref_vector args(m());
expr * arg = nullptr;
if (is_forall) {
if (m().is_and(new_body))
args.append(to_app(new_body)->get_num_args(), to_app(new_body)->get_args());
else if (m().is_not(new_body, arg) && m().is_or(arg))
for (expr * e : *to_app(arg))
args.push_back(m().mk_not(e));
else
return false;
}
else {
if (m().is_or(new_body))
args.append(to_app(new_body)->get_num_args(), to_app(new_body)->get_args());
else if (m().is_not(new_body, arg) && m().is_and(arg))
for (expr * e : *to_app(arg))
args.push_back(m().mk_not(e));
else
return false;
}
if (args.size() < 2)
return false;
expr_ref_vector quants(m());
for (expr * a : args) {
quantifier_ref sub(m());
sub = m().mk_quantifier(old_q->get_kind(),
old_q->get_num_decls(),
old_q->get_decl_sorts(),
old_q->get_decl_names(),
a,
old_q->get_weight(),
old_q->get_qid(),
old_q->get_skid(),
0, nullptr, 0, nullptr);
quants.push_back(m_elim_unused_vars(sub));
}
if (is_forall)
result = m().mk_and(quants);
else
result = m().mk_or(quants);
return true;
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
@ -822,6 +878,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
return true;
}
else if (distribute_quantifier(old_q, new_body, result)) {
if (m().proofs_enabled()) {
result_pr = m().mk_rewrite(old_q, result);
}
return true;
}
else {
ptr_buffer<expr> new_patterns_buf;
ptr_buffer<expr> new_no_patterns_buf;