mirror of
https://github.com/Z3Prover/z3
synced 2025-04-25 18:15:32 +00:00
remove buggy legacy code, rely on pull_cheap_ite option in rewriter, #1511
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
205d77d591
commit
a64fd7145c
8 changed files with 5 additions and 346 deletions
|
|
@ -25,7 +25,6 @@ z3_add_component(rewriter
|
|||
pb_rewriter.cpp
|
||||
pb2bv_rewriter.cpp
|
||||
push_app_ite.cpp
|
||||
pull_ite_tree.cpp
|
||||
quant_hoist.cpp
|
||||
rewriter.cpp
|
||||
seq_rewriter.cpp
|
||||
|
|
|
|||
|
|
@ -1,221 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
pull_ite_tree.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2008-06-22.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include "ast/rewriter/pull_ite_tree.h"
|
||||
#include "ast/recurse_expr_def.h"
|
||||
#include "ast/for_each_expr.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
||||
pull_ite_tree::pull_ite_tree(ast_manager & m):
|
||||
m_manager(m),
|
||||
m_rewriter(m),
|
||||
m_cache(m) {
|
||||
}
|
||||
|
||||
void pull_ite_tree::cache_result(expr * n, expr * r, proof * pr) {
|
||||
m_cache.insert(n, r, pr);
|
||||
}
|
||||
|
||||
void pull_ite_tree::visit(expr * n, bool & visited) {
|
||||
if (!is_cached(n)) {
|
||||
m_todo.push_back(n);
|
||||
visited = false;
|
||||
}
|
||||
}
|
||||
|
||||
bool pull_ite_tree::visit_children(expr * n) {
|
||||
if (m_manager.is_ite(n)) {
|
||||
bool visited = true;
|
||||
visit(to_app(n)->get_arg(1), visited);
|
||||
visit(to_app(n)->get_arg(2), visited);
|
||||
return visited;
|
||||
}
|
||||
else {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
void pull_ite_tree::reduce(expr * n) {
|
||||
// Remark: invoking the simplifier to build the new expression saves a lot of memory.
|
||||
if (m_manager.is_ite(n)) {
|
||||
expr * c = to_app(n)->get_arg(0);
|
||||
expr * t_old = to_app(n)->get_arg(1);
|
||||
expr * e_old = to_app(n)->get_arg(2);
|
||||
expr * t = nullptr;
|
||||
proof * t_pr = nullptr;
|
||||
expr * e = nullptr;
|
||||
proof * e_pr = nullptr;
|
||||
get_cached(t_old, t, t_pr);
|
||||
get_cached(e_old, e, e_pr);
|
||||
expr_ref r(m_manager);
|
||||
expr * args[3] = {c, t, e};
|
||||
r = m_rewriter.mk_app(to_app(n)->get_decl(), 3, args);
|
||||
if (!m_manager.proofs_enabled()) {
|
||||
// expr * r = m_manager.mk_ite(c, t, e);
|
||||
cache_result(n, r, nullptr);
|
||||
}
|
||||
else {
|
||||
// t_pr is a proof for (m_p ... t_old ...) == t
|
||||
// e_pr is a proof for (m_p ... e_old ...) == e
|
||||
expr_ref old(m_manager);
|
||||
expr_ref p_t_old(m_manager);
|
||||
expr_ref p_e_old(m_manager);
|
||||
old = mk_p_arg(n); // (m_p ... n ...) where n is (ite c t_old e_old)
|
||||
p_t_old = mk_p_arg(t_old); // (m_p ... t_old ...)
|
||||
p_e_old = mk_p_arg(e_old); // (m_p ... e_old ...)
|
||||
expr_ref tmp1(m_manager);
|
||||
tmp1 = m_manager.mk_ite(c, p_t_old, p_e_old); // (ite c (m_p ... t_old ...) (m_p ... e_old ...))
|
||||
proof * pr1 = m_manager.mk_rewrite(old, tmp1); // proof for (m_p ... (ite c t_old e_old) ...) = (ite c (m_p ... t_old ...) (m_p ... e_old ...))
|
||||
expr_ref tmp2(m_manager);
|
||||
tmp2 = m_manager.mk_ite(c, t, e); // (ite c t e)
|
||||
proof * pr2 = nullptr; // it will contain a proof for (ite c (m_p ... t_old ...) (m_p ... e_old ...)) = (ite c t e)
|
||||
proof * pr3 = nullptr; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = (ite c t e)
|
||||
proof * proofs[2];
|
||||
unsigned num_proofs = 0;
|
||||
if (t_pr != nullptr) {
|
||||
proofs[num_proofs] = t_pr;
|
||||
num_proofs++;
|
||||
}
|
||||
if (e_pr != nullptr) {
|
||||
proofs[num_proofs] = e_pr;
|
||||
num_proofs++;
|
||||
}
|
||||
if (num_proofs > 0) {
|
||||
pr2 = m_manager.mk_congruence(to_app(tmp1), to_app(tmp2), num_proofs, proofs);
|
||||
pr3 = m_manager.mk_transitivity(pr1, pr2);
|
||||
}
|
||||
else {
|
||||
pr3 = pr1;
|
||||
}
|
||||
proof * pr4 = nullptr; // it will contain a proof for (ite c t e) = r
|
||||
proof * pr5 = nullptr; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = r
|
||||
if (tmp2 != r) {
|
||||
pr4 = m_manager.mk_rewrite(tmp2, r);
|
||||
pr5 = m_manager.mk_transitivity(pr3, pr4);
|
||||
}
|
||||
else {
|
||||
pr5 = pr3;
|
||||
}
|
||||
cache_result(n, r, pr5);
|
||||
}
|
||||
}
|
||||
else {
|
||||
expr_ref r(m_manager);
|
||||
m_args[m_arg_idx] = n;
|
||||
r = m_rewriter.mk_app(m_p, m_args.size(), m_args.c_ptr());
|
||||
if (!m_manager.proofs_enabled()) {
|
||||
// expr * r = m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
|
||||
cache_result(n, r, nullptr);
|
||||
}
|
||||
else {
|
||||
expr_ref old(m_manager);
|
||||
proof * p;
|
||||
old = mk_p_arg(n);
|
||||
if (old == r)
|
||||
p = nullptr;
|
||||
else
|
||||
p = m_manager.mk_rewrite(old, r);
|
||||
cache_result(n, r, p);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) {
|
||||
unsigned num_args = n->get_num_args();
|
||||
m_args.resize(num_args);
|
||||
m_p = n->get_decl();
|
||||
expr * ite = nullptr;
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = n->get_arg(i);
|
||||
if (ite) {
|
||||
m_args[i] = arg;
|
||||
}
|
||||
else if (m_manager.is_ite(arg)) {
|
||||
m_arg_idx = i;
|
||||
m_args[i] = 0;
|
||||
ite = arg;
|
||||
}
|
||||
else {
|
||||
m_args[i] = arg;
|
||||
}
|
||||
}
|
||||
if (!ite) {
|
||||
r = n;
|
||||
pr = nullptr;
|
||||
return;
|
||||
}
|
||||
m_todo.push_back(ite);
|
||||
while (!m_todo.empty()) {
|
||||
expr * n = m_todo.back();
|
||||
if (is_cached(n))
|
||||
m_todo.pop_back();
|
||||
else if (visit_children(n)) {
|
||||
m_todo.pop_back();
|
||||
reduce(n);
|
||||
}
|
||||
}
|
||||
SASSERT(is_cached(ite));
|
||||
expr * _r = nullptr;
|
||||
proof * _pr = nullptr;
|
||||
get_cached(ite, _r, _pr);
|
||||
r = to_app(_r);
|
||||
pr = _pr;
|
||||
m_cache.reset();
|
||||
m_todo.reset();
|
||||
}
|
||||
|
||||
|
||||
|
||||
pull_ite_tree_cfg::pull_ite_tree_cfg(ast_manager & m):
|
||||
m(m),
|
||||
m_trail(m),
|
||||
m_proc(m) {
|
||||
}
|
||||
|
||||
bool pull_ite_tree_cfg::get_subst(expr * n, expr* & r, proof* & p) {
|
||||
if (is_app(n) && is_target(to_app(n))) {
|
||||
app_ref tmp(m);
|
||||
proof_ref pr(m);
|
||||
m_proc(to_app(n), tmp, pr);
|
||||
if (tmp != n) {
|
||||
r = tmp;
|
||||
p = pr;
|
||||
m_trail.push_back(r);
|
||||
m_trail.push_back(p);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool pull_cheap_ite_tree_cfg::is_target(app * n) const {
|
||||
bool r =
|
||||
n->get_num_args() == 2 &&
|
||||
n->get_family_id() != null_family_id &&
|
||||
m.is_bool(n) &&
|
||||
(m.is_value(n->get_arg(0)) || m.is_value(n->get_arg(1))) &&
|
||||
(m.is_term_ite(n->get_arg(0)) || m.is_term_ite(n->get_arg(1)));
|
||||
TRACE("pull_ite_target", tout << mk_pp(n, m) << "\nresult: " << r << "\n";);
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
@ -1,113 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
pull_ite_tree.h
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2008-06-22.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef PULL_ITE_TREE_H_
|
||||
#define PULL_ITE_TREE_H_
|
||||
|
||||
#include "ast/ast.h"
|
||||
#include "ast/rewriter/rewriter.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/expr_map.h"
|
||||
#include "ast/recurse_expr.h"
|
||||
#include "util/obj_hashtable.h"
|
||||
|
||||
/**
|
||||
\brief Functor for applying the following transformation
|
||||
F[(p (ite c t1 t2) args)] = F'[(ite c t1 t2), p, args]
|
||||
|
||||
F'[(ite c t1 t2), p, args] = (ite c F'[t1, p, args] F'[t2, p, args])
|
||||
F'[t, p, args] = (p t args)
|
||||
*/
|
||||
class pull_ite_tree {
|
||||
ast_manager & m_manager;
|
||||
th_rewriter m_rewriter;
|
||||
func_decl * m_p;
|
||||
ptr_vector<expr> m_args;
|
||||
unsigned m_arg_idx; //!< position of the ite argument
|
||||
expr_map m_cache;
|
||||
ptr_vector<expr> m_todo;
|
||||
|
||||
bool is_cached(expr * n) const { return m_cache.contains(n); }
|
||||
void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
|
||||
void cache_result(expr * n, expr * r, proof * pr);
|
||||
void visit(expr * n, bool & visited);
|
||||
bool visit_children(expr * n);
|
||||
void reduce(expr * n);
|
||||
/**
|
||||
\brief Creante an application (m_p ... n ...) where n is the argument m_arg_idx and the other arguments
|
||||
are in m_args.
|
||||
*/
|
||||
expr * mk_p_arg(expr * n) {
|
||||
m_args[m_arg_idx] = n;
|
||||
return m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
|
||||
}
|
||||
public:
|
||||
pull_ite_tree(ast_manager & m);
|
||||
/**
|
||||
\brief Apply the transformation above if n contains an ite-expression.
|
||||
Store the result in r. If n does not contain an ite-expression, then
|
||||
store n in r.
|
||||
|
||||
When proof generation is enabled, pr is a proof for n = r.
|
||||
*/
|
||||
void operator()(app * n, app_ref & r, proof_ref & pr);
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Functor for applying the pull_ite_tree on subexpressions n that
|
||||
satisfy the is_target virtual predicate.
|
||||
*/
|
||||
class pull_ite_tree_cfg : public default_rewriter_cfg {
|
||||
protected:
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_trail;
|
||||
pull_ite_tree m_proc;
|
||||
public:
|
||||
pull_ite_tree_cfg(ast_manager & m);
|
||||
virtual ~pull_ite_tree_cfg() {}
|
||||
virtual bool is_target(app * n) const = 0;
|
||||
bool get_subst(expr * n, expr* & r, proof* & p);
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Apply pull_ite_tree on predicates of the form
|
||||
(p ite v) and (p v ite)
|
||||
|
||||
where:
|
||||
- p is an interpreted predicate
|
||||
- ite is an ite-term expression
|
||||
- v is a value
|
||||
*/
|
||||
class pull_cheap_ite_tree_cfg : public pull_ite_tree_cfg {
|
||||
public:
|
||||
pull_cheap_ite_tree_cfg(ast_manager & m):pull_ite_tree_cfg(m) {}
|
||||
~pull_cheap_ite_tree_cfg() override {}
|
||||
bool is_target(app * n) const override;
|
||||
};
|
||||
|
||||
class pull_cheap_ite_tree_rw : public rewriter_tpl<pull_cheap_ite_tree_cfg> {
|
||||
pull_cheap_ite_tree_cfg m_cfg;
|
||||
public:
|
||||
pull_cheap_ite_tree_rw(ast_manager& m):
|
||||
rewriter_tpl<pull_cheap_ite_tree_cfg>(m, m.proofs_enabled(), m_cfg),
|
||||
m_cfg(m)
|
||||
{}
|
||||
};
|
||||
|
||||
#endif /* PULL_ITE_TREE_H_ */
|
||||
|
||||
|
|
@ -46,7 +46,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
|
|||
m_refine_inj_axiom(*this),
|
||||
m_max_bv_sharing_fn(*this),
|
||||
m_elim_term_ite(*this),
|
||||
m_pull_cheap_ite_trees(*this),
|
||||
m_pull_nested_quantifiers(*this),
|
||||
m_elim_bvs_from_quantifiers(*this),
|
||||
m_cheap_quant_fourier_motzkin(*this),
|
||||
|
|
@ -122,7 +121,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
|
|||
if (flag == m_elim_and) return;
|
||||
m_elim_and = flag;
|
||||
params_ref p;
|
||||
p.set_bool("pull_cheap_ite", false);
|
||||
if (m_params.m_pull_cheap_ite) p.set_bool("pull_cheap_ite", true);
|
||||
p.set_bool("elim_and", flag);
|
||||
p.set_bool("arith_ineq_lhs", true);
|
||||
p.set_bool("sort_sums", true);
|
||||
|
|
@ -241,7 +240,6 @@ void asserted_formulas::reduce() {
|
|||
if (!invoke(m_nnf_cnf)) return;
|
||||
set_eliminate_and(true);
|
||||
if (!invoke(m_reduce_asserted_formulas)) return;
|
||||
if (!invoke(m_pull_cheap_ite_trees)) return;
|
||||
if (!invoke(m_pull_nested_quantifiers)) return;
|
||||
if (!invoke(m_lift_ite)) return;
|
||||
if (!invoke(m_ng_lift_ite)) return;
|
||||
|
|
|
|||
|
|
@ -26,7 +26,6 @@ Revision History:
|
|||
#include "ast/rewriter/bit2int.h"
|
||||
#include "ast/rewriter/maximize_ac_sharing.h"
|
||||
#include "ast/rewriter/distribute_forall.h"
|
||||
#include "ast/rewriter/pull_ite_tree.h"
|
||||
#include "ast/rewriter/push_app_ite.h"
|
||||
#include "ast/rewriter/inj_axiom.h"
|
||||
#include "ast/rewriter/bv_elim.h"
|
||||
|
|
@ -172,7 +171,6 @@ class asserted_formulas {
|
|||
|
||||
#define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE)
|
||||
|
||||
MK_SIMPLIFIERF(pull_cheap_ite_trees, pull_cheap_ite_tree_rw, "pull-cheap-ite-trees", af.m_params.m_pull_cheap_ite_trees, false);
|
||||
MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
|
||||
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_params.m_eliminate_bounds && af.has_quantifiers(), true);
|
||||
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_params.m_bb_quantifiers, true);
|
||||
|
|
@ -187,7 +185,6 @@ class asserted_formulas {
|
|||
refine_inj_axiom_fn m_refine_inj_axiom;
|
||||
max_bv_sharing_fn m_max_bv_sharing_fn;
|
||||
elim_term_ite_fn m_elim_term_ite;
|
||||
pull_cheap_ite_trees m_pull_cheap_ite_trees;
|
||||
pull_nested_quantifiers m_pull_nested_quantifiers;
|
||||
elim_bvs_from_quantifiers m_elim_bvs_from_quantifiers;
|
||||
cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin;
|
||||
|
|
@ -219,7 +216,6 @@ class asserted_formulas {
|
|||
bool is_gt(expr* lhs, expr* rhs);
|
||||
void compute_depth(expr* e);
|
||||
unsigned depth(expr* e) { return m_expr2depth[e]; }
|
||||
bool pull_cheap_ite_trees();
|
||||
|
||||
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
|
||||
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@ void preprocessor_params::display(std::ostream & out) const {
|
|||
|
||||
DISPLAY_PARAM(m_lift_ite);
|
||||
DISPLAY_PARAM(m_ng_lift_ite);
|
||||
DISPLAY_PARAM(m_pull_cheap_ite_trees);
|
||||
DISPLAY_PARAM(m_pull_cheap_ite);
|
||||
DISPLAY_PARAM(m_pull_nested_quantifiers);
|
||||
DISPLAY_PARAM(m_eliminate_term_ite);
|
||||
DISPLAY_PARAM(m_macro_finder);
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ struct preprocessor_params : public pattern_inference_params,
|
|||
public bit_blaster_params {
|
||||
lift_ite_kind m_lift_ite;
|
||||
lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms
|
||||
bool m_pull_cheap_ite_trees;
|
||||
bool m_pull_cheap_ite;
|
||||
bool m_pull_nested_quantifiers;
|
||||
bool m_eliminate_term_ite;
|
||||
bool m_macro_finder;
|
||||
|
|
@ -54,7 +54,7 @@ public:
|
|||
preprocessor_params(params_ref const & p = params_ref()):
|
||||
m_lift_ite(LI_NONE),
|
||||
m_ng_lift_ite(LI_NONE),
|
||||
m_pull_cheap_ite_trees(false),
|
||||
m_pull_cheap_ite(false),
|
||||
m_pull_nested_quantifiers(false),
|
||||
m_eliminate_term_ite(false),
|
||||
m_macro_finder(false),
|
||||
|
|
|
|||
|
|
@ -507,7 +507,7 @@ namespace smt {
|
|||
m_params.m_nnf_cnf = false;
|
||||
if (st.m_max_ite_tree_depth > 50) {
|
||||
m_params.m_arith_eq2ineq = false;
|
||||
m_params.m_pull_cheap_ite_trees = true;
|
||||
m_params.m_pull_cheap_ite = true;
|
||||
m_params.m_arith_propagate_eqs = true;
|
||||
m_params.m_relevancy_lvl = 2;
|
||||
m_params.m_relevancy_lemma = false;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue