mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #3679

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-02 15:04:05 -07:00
parent f98b94bdbc
commit 896a1b2048
17 changed files with 59 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ackermannization/ackr_info.h
View file

@ -36,7 +36,7 @@ class ackr_info {
public:
ackr_info(ast_manager& m) :
m(m),
m_er(mk_default_expr_replacer(m)),
m_er(mk_default_expr_replacer(m, false)),
m_subst(m),
m_ref_count(0),
m_sealed(false)

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -89,7 +89,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m());
for (unsigned i = 0; i < num_args; ++i) tout << mk_pp(args[i], m()) << " ";
tout << "\n==>\n" << mk_pp(result.get(), m()) << "\n";
tout << "args: " << to_app(result)->get_num_args() << "\n";
if (is_app(result)) tout << "args: " << to_app(result)->get_num_args() << "\n";
);
return st;
}

8
src/ast/rewriter/expr_replacer.cpp
View file

@ -83,9 +83,9 @@ class default_expr_replacer : public expr_replacer {
default_expr_replacer_cfg m_cfg;
rewriter_tpl<default_expr_replacer_cfg> m_replacer;
public:
default_expr_replacer(ast_manager & m):
default_expr_replacer(ast_manager & m, bool proofs_enabled):
m_cfg(m),
m_replacer(m, m.proofs_enabled(), m_cfg) {
m_replacer(m, m.proofs_enabled() && proofs_enabled, m_cfg) {
}
ast_manager & m() const override { return m_replacer.m(); }
@ -115,8 +115,8 @@ public:
}
};
expr_replacer * mk_default_expr_replacer(ast_manager & m) {
return alloc(default_expr_replacer, m);
expr_replacer * mk_default_expr_replacer(ast_manager & m, bool proofs_allowed) {
return alloc(default_expr_replacer, m, proofs_allowed);
}
/**

2
src/ast/rewriter/expr_replacer.h
View file

@ -49,7 +49,7 @@ public:
/**
\brief Create a vanilla replacer. It just applies the substitution.
*/
expr_replacer * mk_default_expr_replacer(ast_manager & m);
expr_replacer * mk_default_expr_replacer(ast_manager & m, bool proofs_allowed);
/**
\brief Apply substitution and simplify.

70
src/ast/rewriter/rewriter_def.h
View file

@ -35,47 +35,49 @@ void rewriter_tpl<Config>::process_var(var * v) {
m_r = nullptr;
return;
}
if (!ProofGen) {
// bindings are only used when Proof Generation is not enabled.
unsigned idx = v->get_idx();
unsigned idx = v->get_idx();
if (ProofGen) {
result_pr_stack().push_back(nullptr); // implicit reflexivity
if (idx < m_bindings.size()) {
unsigned index = m_bindings.size() - idx - 1;
expr * r = m_bindings[index];
if (r != nullptr) {
CTRACE("rewriter", v->get_sort() != m().get_sort(r),
tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m());
tout << "index " << index << " bindings " << m_bindings.size() << "\n";
display_bindings(tout););
SASSERT(v->get_sort() == m().get_sort(r));
if (!is_ground(r) && m_shifts[index] != m_bindings.size()) {
unsigned shift_amount = m_bindings.size() - m_shifts[index];
expr* c = get_cached(r, shift_amount);
if (c) {
result_stack().push_back(c);
set_new_child_flag(v);
return;
}
expr_ref tmp(m());
m_shifter(r, shift_amount, tmp);
result_stack().push_back(tmp);
TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n";
display_bindings(tout););
cache_shifted_result(r, shift_amount, tmp);
}
else {
result_stack().push_back(r);
TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";);
}
SASSERT(
true || // disabled for now
idx >= m_bindings.size() ||
!m_bindings[m_bindings.size() - idx - 1] ||
v == m_bindings[m_bindings.size() - idx - 1]);
}
unsigned index = 0;
expr * r;
if (!ProofGen && idx < m_bindings.size() &&
(index = m_bindings.size() - idx - 1, r = m_bindings[index])) {
CTRACE("rewriter", v->get_sort() != m().get_sort(r),
tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m());
tout << "index " << index << " bindings " << m_bindings.size() << "\n";
display_bindings(tout););
SASSERT(v->get_sort() == m().get_sort(r));
if (!is_ground(r) && m_shifts[index] != m_bindings.size()) {
unsigned shift_amount = m_bindings.size() - m_shifts[index];
expr* c = get_cached(r, shift_amount);
if (c) {
result_stack().push_back(c);
set_new_child_flag(v);
return;
}
expr_ref tmp(m());
m_shifter(r, shift_amount, tmp);
result_stack().push_back(tmp);
TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n";
display_bindings(tout););
cache_shifted_result(r, shift_amount, tmp);
}
else {
result_stack().push_back(r);
TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";);
}
set_new_child_flag(v);
return;
}
result_stack().push_back(v);
if (ProofGen)
result_pr_stack().push_back(nullptr); // implicit reflexivity
}
template<typename Config>

2
src/muz/fp/horn_tactic.cpp
View file

@ -334,7 +334,7 @@ class horn_tactic : public tactic {
expr_substitution sub(m);
sub.insert(q, m.mk_false());
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m, false);
rep->set_substitution(&sub);
g->inc_depth();
g->reset();

4
src/muz/spacer/spacer_context.cpp
View file

@ -1124,7 +1124,7 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
v = m.mk_var(i, sig(i)->get_range());
sub.insert(c, v);
}
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m, false);
rep->set_substitution(&sub);
(*rep)(result);
@ -1216,7 +1216,7 @@ void pred_transformer::add_cover(unsigned level, expr* property, bool bg)
v = m.mk_var(i, sig(i)->get_range());
sub.insert(v, c, pr);
}
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m, false);
rep->set_substitution(&sub);
(*rep)(result);
TRACE("spacer", tout << "cover:\n" << mk_pp(result, m) << "\n";);

2
src/muz/spacer/spacer_qe_project.cpp
View file

@ -1163,7 +1163,7 @@ namespace spacer_qe {
tout << "substituting " << mk_pp (m_var->x (), m) << " by " << mk_pp (x_term, m) << "\n";
);
}
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer (m);
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer (m, false);
rep->set_substitution (&sub);
(*rep)(fml);
}

4
src/qe/nlarith_util.cpp
View file

@ -546,7 +546,7 @@ namespace nlarith {
sqrt_form e0(*this, mk_uminus(c), 0, z(), b);
// a_i = 0 /\ b_i != 0 /\ phi[e_i/x]
TRACE("nlarith", display(tout << "a_i != 0 & b_i != 0 & hi[e_i / x]", p);tout<<"\n";);
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m());
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m(), false);
expr_substitution sub(m());
sub.insert(a, z());
rp->set_substitution(&sub);
@ -610,7 +610,7 @@ namespace nlarith {
sqrt_form e0(*this, mk_uminus(c), 0, z(), b);
es.reset();
subst.reset();
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m());
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m(), false);
expr_substitution sub(m());
sub.insert(a, z());
rp->set_substitution(&sub);

6
src/qe/qe.cpp
View file

@ -351,7 +351,7 @@ namespace qe {
scoped_ptr<expr_replacer> m_replace;
public:
lift_ite(ast_manager& m, i_expr_pred& is_relevant) :
m(m), m_is_relevant(is_relevant), m_rewriter(m), m_replace(mk_default_expr_replacer(m)) {}
m(m), m_is_relevant(is_relevant), m_rewriter(m), m_replace(mk_default_expr_replacer(m, false)) {}
bool operator()(expr* fml, expr_ref& result) {
if (m.is_ite(fml)) {
@ -1465,7 +1465,7 @@ namespace qe {
if (!is_sat) {
fml = m.mk_false();
if (m_fml.get() != m_subfml.get()) {
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m);
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml);
fml = m_fml;
}
@ -1497,7 +1497,7 @@ namespace qe {
if (!m_free_vars.empty() || m_solver.inconsistent()) {
if (m_fml.get() != m_subfml.get()) {
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m);
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml);
fml = m_fml;
}

1
src/smt/qi_queue.cpp
View file

@ -226,6 +226,7 @@ namespace smt {
return;
}
TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);
quantifier_stat * stat = m_qm.get_stat(q);
stat->inc_num_instances();
if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) {

2
src/smt/theory_str_mc.cpp
View file

@ -1136,7 +1136,7 @@ namespace smt {
}
// TODO insert length values into substitution table as well?
if (m_params.m_FixedLengthRefinement) {
scoped_ptr<expr_replacer> replacer = mk_default_expr_replacer(m);
scoped_ptr<expr_replacer> replacer = mk_default_expr_replacer(m, false);
replacer->set_substitution(&subst);
th_rewriter rw(m);
if (!abstracted_boolean_formulas.empty()) {

2
src/tactic/arith/nla2bv_tactic.cpp
View file

@ -184,7 +184,7 @@ class nla2bv_tactic : public tactic {
// substitute variables by bit-vectors
void substitute_vars(goal & g) {
scoped_ptr<expr_replacer> er = mk_default_expr_replacer(m_manager);
scoped_ptr<expr_replacer> er = mk_default_expr_replacer(m_manager, false);
er->set_substitution(&m_subst);
expr_ref r(m_manager);
for (unsigned i = 0; i < g.size(); ++i) {

2
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -753,7 +753,7 @@ struct purify_arith_proc {
unsigned idx = num_vars - i - 1;
subst.insert(c, m().mk_var(idx, s));
}
scoped_ptr<expr_replacer> replacer = mk_default_expr_replacer(m());
scoped_ptr<expr_replacer> replacer = mk_default_expr_replacer(m(), false);
replacer->set_substitution(&subst);
(*replacer)(new_body, new_body);
new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight());

2
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -47,7 +47,7 @@ public:
bv_size_reduction_tactic(ast_manager & m) :
m(m),
m_util(m),
m_replacer(mk_default_expr_replacer(m)) {
m_replacer(mk_default_expr_replacer(m, false)) {
}
tactic * translate(ast_manager & m) override {

2
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -67,7 +67,7 @@ class solve_eqs_tactic : public tactic {
m_marked_candidates(m) {
updt_params(p);
if (m_r == nullptr)
m_r = mk_default_expr_replacer(m);
m_r = mk_default_expr_replacer(m, true);
}
~imp() {

2
src/tactic/core/symmetry_reduce_tactic.cpp
View file

@ -114,7 +114,7 @@ class symmetry_reduce_tactic::imp {
ast_manager& m() const { return m_manager; }
public:
imp(ast_manager& m) : m_manager(m), m_rewriter(m) {
m_replace = mk_default_expr_replacer(m);
m_replace = mk_default_expr_replacer(m, false);
}
~imp() {}