diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index df44427cfa9..b807b00e384 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -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 diff --git a/src/ast/simplifiers/distribute_forall.h b/src/ast/simplifiers/distribute_forall.h index 3127a4ec87a..d5c511ab1e7 100644 --- a/src/ast/simplifiers/distribute_forall.h +++ b/src/ast/simplifiers/distribute_forall.h @@ -15,31 +15,23 @@ Module Name: #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; }; diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 8a86e9a0b38..d4a115dcc24 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -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 diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp deleted file mode 100644 index 1d171aae3fa..00000000000 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ /dev/null @@ -1,141 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - distribute_forall_tactic.cpp - -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 m_cfg; - - rw(ast_manager & m, bool proofs_enabled): - rewriter_tpl(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); -} diff --git a/src/tactic/core/distribute_forall_tactic.h b/src/tactic/core/distribute_forall_tactic.h index d7a030500aa..328a62b2f01 100644 --- a/src/tactic/core/distribute_forall_tactic.h +++ b/src/tactic/core/distribute_forall_tactic.h @@ -13,14 +13,40 @@ Module Name: 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)")