mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

update distribute forall

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-06 17:59:33 -08:00
parent 80033e8744
commit c33e58ee1a
5 changed files with 39 additions and 162 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/simplifiers/CMakeLists.txt
View file

@ -5,6 +5,7 @@ z3_add_component(simplifiers
card2bv.cpp
demodulator_simplifier.cpp
dependent_expr_state.cpp
distribute_forall.cpp
elim_unconstrained.cpp
eliminate_predicates.cpp
euf_completion.cpp

26
src/ast/simplifiers/distribute_forall.h
View file

@ -15,31 +15,23 @@ Author:
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/rewriter/distribute_forall.h"
class distribute_forall_simplifier : public dependent_expr_simplifier {
distribute_forall m_dist;
struct rw_cfg;
struct rw;
public:
distribute_forall_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
dependent_expr_simplifier(m, fmls),
m_dist(m) {
dependent_expr_simplifier(m, fmls) {
}
char const* name() const override { return "distribute-forall"; }
void reduce() override {
if (!m_fmls.has_quantifiers())
return;
expr_ref r(m);
for (unsigned idx : indices()) {
auto const& d = m_fmls[idx];
if (!has_quantifiers(d.fml()))
continue;
m_dist(d.fml(), r);
m_fmls.update(idx, dependent_expr(m, r, nullptr, d.dep()));
}
}
bool supports_proofs() const override { return true; }
void reduce() override;
};

1
src/tactic/core/CMakeLists.txt
View file

@ -6,7 +6,6 @@ z3_add_component(core_tactics
collect_statistics_tactic.cpp
ctx_simplify_tactic.cpp
der_tactic.cpp
distribute_forall_tactic.cpp
dom_simplify_tactic.cpp
elim_term_ite_tactic.cpp
elim_uncnstr_tactic.cpp

141
src/tactic/core/distribute_forall_tactic.cpp
View file

@ -1,141 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
distribute_forall_tactic.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2012-02-18.
--*/
#include "tactic/tactical.h"
#include "ast/ast_util.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/var_subst.h"
class distribute_forall_tactic : public tactic {
struct rw_cfg : public default_rewriter_cfg {
ast_manager & m;
rw_cfg(ast_manager & _m):m(_m) {}
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) {
if (!is_forall(old_q)) {
return false;
}
if (m.is_not(new_body) && m.is_or(to_app(new_body)->get_arg(0))) {
// (forall X (not (or F1 ... Fn)))
// -->
// (and (forall X (not F1))
// ...
// (forall X (not Fn)))
app * or_e = to_app(to_app(new_body)->get_arg(0));
unsigned num_args = or_e->get_num_args();
expr_ref_buffer new_args(m);
for (unsigned i = 0; i < num_args; i++) {
expr * arg = or_e->get_arg(i);
expr * not_arg = mk_not(m, arg);
quantifier_ref tmp_q(m);
tmp_q = m.update_quantifier(old_q, not_arg);
new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));
}
result = m.mk_and(new_args.size(), new_args.data());
if (m.proofs_enabled()) {
result_pr = m.mk_push_quant(old_q, result);
}
return true;
}
if (m.is_and(new_body)) {
// (forall X (and F1 ... Fn))
// -->
// (and (forall X F1)
// ...
// (forall X Fn)
unsigned num_args = to_app(new_body)->get_num_args();
expr_ref_buffer new_args(m);
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(new_body)->get_arg(i);
quantifier_ref tmp_q(m);
tmp_q = m.update_quantifier(old_q, arg);
new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));
}
result = m.mk_and(new_args.size(), new_args.data());
if (m.proofs_enabled()) {
result_pr = m.mk_push_quant(old_q, result);
}
return true;
}
return false;
}
};
struct rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg;
rw(ast_manager & m, bool proofs_enabled):
rewriter_tpl<rw_cfg>(m, proofs_enabled, m_cfg),
m_cfg(m) {
}
};
rw * m_rw;
public:
distribute_forall_tactic():m_rw(nullptr) {}
tactic * translate(ast_manager & m) override {
return alloc(distribute_forall_tactic);
}
char const* name() const override { return "distribute_forall"; }
void operator()(goal_ref const & g,
goal_ref_buffer & result) override {
ast_manager & m = g->m();
bool produce_proofs = g->proofs_enabled();
rw r(m, produce_proofs);
m_rw = &r;
result.reset();
tactic_report report("distribute-forall", *g);
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) {
if (g->inconsistent())
break;
expr * curr = g->form(idx);
r(curr, new_curr, new_pr);
if (g->proofs_enabled()) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
g->inc_depth();
result.push_back(g.get());
m_rw = nullptr;
}
void cleanup() override {}
};
tactic * mk_distribute_forall_tactic(ast_manager & m, params_ref const & p) {
return alloc(distribute_forall_tactic);
}

32
src/tactic/core/distribute_forall_tactic.h
View file

@ -13,14 +13,40 @@ Author:
Leonardo de Moura (leonardo) 2012-02-18.
Tactic Documentation:
## Tactic distribute-forall
### Short Description:
Distribute $\forall$ over conjunctions (and distribute $\exists$ over disjunctions)
### Example
```z3
(declare-const x Int)
(declare-fun p (Int) Bool)
(declare-fun q (Int) Bool)
(assert (forall ((x Int)) (and (p x) (q x))))
(apply distribute-forall)
```
### Notes
* supports unsat cores, proof terms
--*/
#pragma once
#include "util/params.h"
class ast_manager;
class tactic;
#include "tactic/dependent_expr_state_tactic.h"
#include "ast/simplifiers/distribute_forall.h"
tactic * mk_distribute_forall_tactic(ast_manager & m, params_ref const & p);
inline tactic * mk_distribute_forall_tactic(ast_manager& m, params_ref const& p = params_ref()) {
return alloc(dependent_expr_state_tactic, m, p,
[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(distribute_forall_simplifier, m, p, s); });
}
/*
ADD_TACTIC("distribute-forall", "distribute forall over conjunctions.", "mk_distribute_forall_tactic(m, p)")