mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
spread a few anonymous namespaces and remove some m_imp idioms
This commit is contained in:
Nuno Lopes
parent
178e5b31e8
commit
3104291b80
2 changed files with 179 additions and 201 deletions
|
|
@ -25,224 +25,206 @@ Revision History:
|
|||
#include "tactic/goal_shared_occs.h"
|
||||
#include "ast/pb_decl_plugin.h"
|
||||
|
||||
namespace {
|
||||
class propagate_values_tactic : public tactic {
|
||||
struct imp {
|
||||
ast_manager & m;
|
||||
th_rewriter m_r;
|
||||
scoped_ptr<expr_substitution> m_subst;
|
||||
goal * m_goal;
|
||||
goal_shared_occs m_occs;
|
||||
unsigned m_idx;
|
||||
unsigned m_max_rounds;
|
||||
bool m_modified;
|
||||
|
||||
imp(ast_manager & m, params_ref const & p):
|
||||
m(m),
|
||||
m_r(m, p),
|
||||
m_goal(nullptr),
|
||||
m_occs(m, true /* track atoms */) {
|
||||
updt_params_core(p);
|
||||
}
|
||||
ast_manager & m;
|
||||
th_rewriter m_r;
|
||||
scoped_ptr<expr_substitution> m_subst;
|
||||
goal * m_goal;
|
||||
goal_shared_occs m_occs;
|
||||
unsigned m_idx;
|
||||
unsigned m_max_rounds;
|
||||
bool m_modified;
|
||||
params_ref m_params;
|
||||
|
||||
~imp() { }
|
||||
void updt_params_core(params_ref const & p) {
|
||||
m_max_rounds = p.get_uint("max_rounds", 4);
|
||||
}
|
||||
|
||||
void updt_params_core(params_ref const & p) {
|
||||
m_max_rounds = p.get_uint("max_rounds", 4);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_r.updt_params(p);
|
||||
updt_params_core(p);
|
||||
}
|
||||
|
||||
|
||||
bool is_shared(expr * t) {
|
||||
return m_occs.is_shared(t);
|
||||
}
|
||||
|
||||
bool is_shared_neg(expr * t, expr * & atom) {
|
||||
if (!m.is_not(t, atom))
|
||||
return false;
|
||||
return is_shared(atom);
|
||||
}
|
||||
bool is_shared(expr * t) {
|
||||
return m_occs.is_shared(t);
|
||||
}
|
||||
|
||||
bool is_shared_eq(expr * t, expr * & lhs, expr * & value) {
|
||||
expr* arg1, *arg2;
|
||||
if (!m.is_eq(t, arg1, arg2))
|
||||
return false;
|
||||
if (m.is_value(arg1) && is_shared(arg2)) {
|
||||
lhs = arg2;
|
||||
value = arg1;
|
||||
return true;
|
||||
}
|
||||
if (m.is_value(arg2) && is_shared(arg1)) {
|
||||
lhs = arg1;
|
||||
value = arg2;
|
||||
return true;
|
||||
}
|
||||
bool is_shared_neg(expr * t, expr * & atom) {
|
||||
if (!m.is_not(t, atom))
|
||||
return false;
|
||||
return is_shared(atom);
|
||||
}
|
||||
|
||||
bool is_shared_eq(expr * t, expr * & lhs, expr * & value) {
|
||||
expr* arg1, *arg2;
|
||||
if (!m.is_eq(t, arg1, arg2))
|
||||
return false;
|
||||
if (m.is_value(arg1) && is_shared(arg2)) {
|
||||
lhs = arg2;
|
||||
value = arg1;
|
||||
return true;
|
||||
}
|
||||
if (m.is_value(arg2) && is_shared(arg1)) {
|
||||
lhs = arg1;
|
||||
value = arg2;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void push_result(expr * new_curr, proof * new_pr) {
|
||||
if (m_goal->proofs_enabled()) {
|
||||
proof * pr = m_goal->pr(m_idx);
|
||||
new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
}
|
||||
|
||||
void push_result(expr * new_curr, proof * new_pr) {
|
||||
if (m_goal->proofs_enabled()) {
|
||||
proof * pr = m_goal->pr(m_idx);
|
||||
new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
expr_dependency_ref new_d(m);
|
||||
if (m_goal->unsat_core_enabled()) {
|
||||
new_d = m_goal->dep(m_idx);
|
||||
expr_dependency * used_d = m_r.get_used_dependencies();
|
||||
if (used_d != nullptr) {
|
||||
new_d = m.mk_join(new_d, used_d);
|
||||
m_r.reset_used_dependencies();
|
||||
}
|
||||
|
||||
expr_dependency_ref new_d(m);
|
||||
if (m_goal->unsat_core_enabled()) {
|
||||
new_d = m_goal->dep(m_idx);
|
||||
expr_dependency * used_d = m_r.get_used_dependencies();
|
||||
if (used_d != nullptr) {
|
||||
new_d = m.mk_join(new_d, used_d);
|
||||
m_r.reset_used_dependencies();
|
||||
}
|
||||
|
||||
m_goal->update(m_idx, new_curr, new_pr, new_d);
|
||||
|
||||
if (is_shared(new_curr)) {
|
||||
m_subst->insert(new_curr, m.mk_true(), m.mk_iff_true(new_pr), new_d);
|
||||
}
|
||||
expr * atom;
|
||||
if (is_shared_neg(new_curr, atom)) {
|
||||
m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d);
|
||||
}
|
||||
expr * lhs, * value;
|
||||
if (is_shared_eq(new_curr, lhs, value)) {
|
||||
TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n";);
|
||||
m_subst->insert(lhs, value, new_pr, new_d);
|
||||
}
|
||||
}
|
||||
|
||||
void process_current() {
|
||||
expr * curr = m_goal->form(m_idx);
|
||||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
|
||||
if (!m_subst->empty()) {
|
||||
m_r(curr, new_curr, new_pr);
|
||||
}
|
||||
else {
|
||||
new_curr = curr;
|
||||
if (m.proofs_enabled())
|
||||
new_pr = m.mk_reflexivity(curr);
|
||||
}
|
||||
|
||||
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
|
||||
if (new_curr != curr) {
|
||||
m_modified = true;
|
||||
//if (has_pb(curr))
|
||||
// IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n");
|
||||
}
|
||||
push_result(new_curr, new_pr);
|
||||
}
|
||||
|
||||
bool has_pb(expr* e) {
|
||||
pb_util pb(m);
|
||||
if (pb.is_ge(e)) return true;
|
||||
if (m.is_or(e)) {
|
||||
for (expr* a : *to_app(e)) {
|
||||
if (pb.is_ge(a)) return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void run(goal_ref const & g, goal_ref_buffer & result) {
|
||||
SASSERT(g->is_well_sorted());
|
||||
tactic_report report("propagate-values", *g);
|
||||
m_goal = g.get();
|
||||
|
||||
bool forward = true;
|
||||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
unsigned size = m_goal->size();
|
||||
m_idx = 0;
|
||||
m_modified = false;
|
||||
unsigned round = 0;
|
||||
|
||||
|
||||
if (m_goal->inconsistent())
|
||||
goto end;
|
||||
|
||||
if (m_max_rounds == 0)
|
||||
goto end;
|
||||
|
||||
m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled());
|
||||
m_r.set_substitution(m_subst.get());
|
||||
m_occs(*m_goal);
|
||||
|
||||
while (true) {
|
||||
TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display_with_dependencies(tout););
|
||||
if (forward) {
|
||||
for (; m_idx < size; m_idx++) {
|
||||
process_current();
|
||||
if (m_goal->inconsistent())
|
||||
goto end;
|
||||
}
|
||||
}
|
||||
|
||||
m_goal->update(m_idx, new_curr, new_pr, new_d);
|
||||
|
||||
if (is_shared(new_curr)) {
|
||||
m_subst->insert(new_curr, m.mk_true(), m.mk_iff_true(new_pr), new_d);
|
||||
}
|
||||
expr * atom;
|
||||
if (is_shared_neg(new_curr, atom)) {
|
||||
m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d);
|
||||
}
|
||||
expr * lhs, * value;
|
||||
if (is_shared_eq(new_curr, lhs, value)) {
|
||||
TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n";);
|
||||
m_subst->insert(lhs, value, new_pr, new_d);
|
||||
}
|
||||
}
|
||||
|
||||
void process_current() {
|
||||
expr * curr = m_goal->form(m_idx);
|
||||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
|
||||
if (!m_subst->empty()) {
|
||||
m_r(curr, new_curr, new_pr);
|
||||
if (m_subst->empty() && !m_modified)
|
||||
goto end;
|
||||
m_occs(*m_goal);
|
||||
m_idx = m_goal->size();
|
||||
forward = false;
|
||||
m_subst->reset();
|
||||
m_r.set_substitution(m_subst.get()); // reset, but keep substitution
|
||||
}
|
||||
else {
|
||||
new_curr = curr;
|
||||
if (m.proofs_enabled())
|
||||
new_pr = m.mk_reflexivity(curr);
|
||||
}
|
||||
|
||||
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
|
||||
if (new_curr != curr) {
|
||||
m_modified = true;
|
||||
//if (has_pb(curr))
|
||||
// IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n");
|
||||
}
|
||||
push_result(new_curr, new_pr);
|
||||
}
|
||||
|
||||
bool has_pb(expr* e) {
|
||||
pb_util pb(m);
|
||||
if (pb.is_ge(e)) return true;
|
||||
if (m.is_or(e)) {
|
||||
for (expr* a : *to_app(e)) {
|
||||
if (pb.is_ge(a)) return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result) {
|
||||
SASSERT(g->is_well_sorted());
|
||||
tactic_report report("propagate-values", *g);
|
||||
m_goal = g.get();
|
||||
|
||||
bool forward = true;
|
||||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
unsigned size = m_goal->size();
|
||||
m_idx = 0;
|
||||
m_modified = false;
|
||||
unsigned round = 0;
|
||||
|
||||
|
||||
if (m_goal->inconsistent())
|
||||
goto end;
|
||||
|
||||
if (m_max_rounds == 0)
|
||||
goto end;
|
||||
|
||||
m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled());
|
||||
m_r.set_substitution(m_subst.get());
|
||||
m_occs(*m_goal);
|
||||
|
||||
while (true) {
|
||||
TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display_with_dependencies(tout););
|
||||
if (forward) {
|
||||
for (; m_idx < size; m_idx++) {
|
||||
process_current();
|
||||
if (m_goal->inconsistent())
|
||||
goto end;
|
||||
}
|
||||
if (m_subst->empty() && !m_modified)
|
||||
while (m_idx > 0) {
|
||||
m_idx--;
|
||||
process_current();
|
||||
if (m_goal->inconsistent())
|
||||
goto end;
|
||||
m_occs(*m_goal);
|
||||
m_idx = m_goal->size();
|
||||
forward = false;
|
||||
m_subst->reset();
|
||||
m_r.set_substitution(m_subst.get()); // reset, but keep substitution
|
||||
}
|
||||
else {
|
||||
while (m_idx > 0) {
|
||||
m_idx--;
|
||||
process_current();
|
||||
if (m_goal->inconsistent())
|
||||
goto end;
|
||||
}
|
||||
if (!m_modified)
|
||||
goto end;
|
||||
m_subst->reset();
|
||||
m_r.set_substitution(m_subst.get()); // reset, but keep substitution
|
||||
m_modified = false;
|
||||
m_occs(*m_goal);
|
||||
m_idx = 0;
|
||||
size = m_goal->size();
|
||||
forward = true;
|
||||
}
|
||||
round++;
|
||||
if (round >= m_max_rounds)
|
||||
break;
|
||||
IF_VERBOSE(100, verbose_stream() << "starting new round, goal size: " << m_goal->num_exprs() << std::endl;);
|
||||
TRACE("propagate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";);
|
||||
if (!m_modified)
|
||||
goto end;
|
||||
m_subst->reset();
|
||||
m_r.set_substitution(m_subst.get()); // reset, but keep substitution
|
||||
m_modified = false;
|
||||
m_occs(*m_goal);
|
||||
m_idx = 0;
|
||||
size = m_goal->size();
|
||||
forward = true;
|
||||
}
|
||||
end:
|
||||
m_goal->elim_redundancies();
|
||||
m_goal->inc_depth();
|
||||
result.push_back(m_goal);
|
||||
SASSERT(m_goal->is_well_sorted());
|
||||
TRACE("propagate_values", tout << "end\n"; m_goal->display(tout););
|
||||
TRACE("propagate_values_core", m_goal->display_with_dependencies(tout););
|
||||
m_goal = nullptr;
|
||||
round++;
|
||||
if (round >= m_max_rounds)
|
||||
break;
|
||||
IF_VERBOSE(100, verbose_stream() << "starting new round, goal size: " << m_goal->num_exprs() << std::endl;);
|
||||
TRACE("propagate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";);
|
||||
}
|
||||
};
|
||||
end:
|
||||
m_goal->elim_redundancies();
|
||||
m_goal->inc_depth();
|
||||
result.push_back(m_goal);
|
||||
SASSERT(m_goal->is_well_sorted());
|
||||
TRACE("propagate_values", tout << "end\n"; m_goal->display(tout););
|
||||
TRACE("propagate_values_core", m_goal->display_with_dependencies(tout););
|
||||
m_goal = nullptr;
|
||||
}
|
||||
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
public:
|
||||
propagate_values_tactic(ast_manager & m, params_ref const & p):
|
||||
m(m),
|
||||
m_r(m, p),
|
||||
m_goal(nullptr),
|
||||
m_occs(m, true /* track atoms */),
|
||||
m_params(p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
updt_params_core(p);
|
||||
}
|
||||
|
||||
tactic * translate(ast_manager & m) override {
|
||||
return alloc(propagate_values_tactic, m, m_params);
|
||||
}
|
||||
|
||||
~propagate_values_tactic() override {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) override {
|
||||
m_params = p;
|
||||
m_imp->updt_params(p);
|
||||
m_r.updt_params(p);
|
||||
updt_params_core(p);
|
||||
}
|
||||
|
||||
void collect_param_descrs(param_descrs & r) override {
|
||||
|
|
@ -252,7 +234,7 @@ public:
|
|||
|
||||
void operator()(goal_ref const & in, goal_ref_buffer & result) override {
|
||||
try {
|
||||
(*m_imp)(in, result);
|
||||
run(in, result);
|
||||
}
|
||||
catch (rewriter_exception & ex) {
|
||||
throw tactic_exception(ex.msg());
|
||||
|
|
@ -260,15 +242,14 @@ public:
|
|||
}
|
||||
|
||||
void cleanup() override {
|
||||
ast_manager & m = m_imp->m;
|
||||
params_ref p = std::move(m_params);
|
||||
m_imp->~imp();
|
||||
new (m_imp) imp(m, p);
|
||||
m_r.cleanup();
|
||||
m_subst = nullptr;
|
||||
m_occs.cleanup();
|
||||
}
|
||||
|
||||
};
|
||||
}
|
||||
|
||||
tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p) {
|
||||
return alloc(propagate_values_tactic, m, p);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -17,8 +17,7 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef PROPAGATE_VALUES_TACTIC_H_
|
||||
#define PROPAGATE_VALUES_TACTIC_H_
|
||||
#pragma once
|
||||
|
||||
#include "util/params.h"
|
||||
class ast_manager;
|
||||
|
|
@ -29,5 +28,3 @@ tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p = para
|
|||
/*
|
||||
ADD_TACTIC("propagate-values", "propagate constants.", "mk_propagate_values_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue