mirror of
https://github.com/Z3Prover/z3
synced 2025-10-30 19:22:28 +00:00
use iterators on goal and other refactoring
This commit is contained in:
Nikolaj Bjorner
parent
eb97fcc273
commit
2e2a2e28df
8 changed files with 77 additions and 53 deletions
|
|
@ -256,22 +256,19 @@ public:
|
|||
void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result) override {
|
||||
tactic_report report("elim-small-bv", *g);
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
fail_if_proof_generation("elim-small-bv", g);
|
||||
fail_if_unsat_core_generation("elim-small-bv", g);
|
||||
m_rw.cfg().m_produce_models = g->models_enabled();
|
||||
|
||||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
unsigned size = g->size();
|
||||
for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) {
|
||||
expr * curr = g->form(idx);
|
||||
unsigned idx = 0;
|
||||
for (auto [curr, dep, pr] : *g) {
|
||||
if (g->inconsistent())
|
||||
break;
|
||||
m_rw(curr, new_curr, new_pr);
|
||||
if (produce_proofs) {
|
||||
proof * pr = g->pr(idx);
|
||||
new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
}
|
||||
g->update(idx, new_curr, new_pr, g->dep(idx));
|
||||
new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
g->update(idx++, new_curr, new_pr, dep);
|
||||
}
|
||||
g->add(m_rw.m_cfg.m_mc.get());
|
||||
|
||||
|
|
|
|||
|
|
@ -29,14 +29,13 @@ class cofactor_term_ite_tactic : public tactic {
|
|||
|
||||
void process(goal & g) {
|
||||
ast_manager & m = g.m();
|
||||
unsigned sz = g.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
unsigned idx = 0;
|
||||
for (auto [f, dep, pr] : g) {
|
||||
if (g.inconsistent())
|
||||
break;
|
||||
expr * f = g.form(i);
|
||||
expr_ref new_f(m);
|
||||
m_elim_ite(f, new_f);
|
||||
g.update(i, new_f, nullptr, g.dep(i));
|
||||
g.update(idx++, new_f, nullptr, dep);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -569,16 +569,15 @@ struct ctx_simplify_tactic::imp {
|
|||
m_occs.reset();
|
||||
m_occs(g);
|
||||
m_num_steps = 0;
|
||||
unsigned sz = g.size();
|
||||
tactic_report report("ctx-simplify", g);
|
||||
if (g.proofs_enabled()) {
|
||||
expr_ref r(m);
|
||||
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
|
||||
expr * t = g.form(i);
|
||||
unsigned idx = 0;
|
||||
for (auto [t, dep, pr] : g) {
|
||||
process(t, r);
|
||||
proof_ref new_pr(m.mk_rewrite(t, r), m);
|
||||
new_pr = m.mk_modus_ponens(g.pr(i), new_pr);
|
||||
g.update(i, r, new_pr, g.dep(i));
|
||||
new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
g.update(idx++, r, new_pr, dep);
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
|
|
|||
|
|
@ -34,21 +34,16 @@ class der_tactic : public tactic {
|
|||
}
|
||||
|
||||
void operator()(goal & g) {
|
||||
bool proofs_enabled = g.proofs_enabled();
|
||||
tactic_report report("der", g);
|
||||
expr_ref new_curr(m());
|
||||
proof_ref new_pr(m());
|
||||
unsigned size = g.size();
|
||||
for (unsigned idx = 0; idx < size; idx++) {
|
||||
unsigned idx = 0;
|
||||
for (auto [curr, dep, pr] : g) {
|
||||
if (g.inconsistent())
|
||||
break;
|
||||
expr * curr = g.form(idx);
|
||||
m_r(curr, new_curr, new_pr);
|
||||
if (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));
|
||||
new_pr = m().mk_modus_ponens(pr, new_pr);
|
||||
g.update(idx++, new_curr, new_pr, dep);
|
||||
}
|
||||
g.elim_redundancies();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -486,22 +486,21 @@ void goal::shrink(unsigned j) {
|
|||
/**
|
||||
\brief Eliminate true formulas.
|
||||
*/
|
||||
void goal::elim_true() {
|
||||
unsigned sz = size();
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * f = form(i);
|
||||
if (m().is_true(f))
|
||||
continue;
|
||||
if (i == j) {
|
||||
j++;
|
||||
void goal::elim_true() {
|
||||
unsigned i = 0, j = 0;
|
||||
for (auto [f, dep, pr] : *this) {
|
||||
if (m().is_true(f)) {
|
||||
++i;
|
||||
continue;
|
||||
}
|
||||
m().set(m_forms, j, f);
|
||||
m().set(m_proofs, j, m().get(m_proofs, i));
|
||||
if (unsat_core_enabled())
|
||||
m().set(m_dependencies, j, m().get(m_dependencies, i));
|
||||
j++;
|
||||
if (i != j) {
|
||||
m().set(m_forms, j, f);
|
||||
m().set(m_proofs, j, pr);
|
||||
if (unsat_core_enabled())
|
||||
m().set(m_dependencies, j, dep);
|
||||
}
|
||||
++i;
|
||||
++j;
|
||||
}
|
||||
shrink(j);
|
||||
}
|
||||
|
|
@ -539,7 +538,7 @@ void goal::elim_redundancies() {
|
|||
expr_ref_fast_mark1 neg_lits(m());
|
||||
expr_ref_fast_mark2 pos_lits(m());
|
||||
unsigned sz = size();
|
||||
unsigned j = 0;
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * f = form(i);
|
||||
if (m().is_true(f))
|
||||
|
|
|
|||
|
|
@ -165,6 +165,41 @@ public:
|
|||
bool is_cnf() const;
|
||||
|
||||
goal * translate(ast_translation & translator) const;
|
||||
|
||||
class iterator {
|
||||
public:
|
||||
using value_type = std::tuple<expr*, expr_dependency*, proof*>;
|
||||
using reference = value_type&;
|
||||
using pointer = value_type*;
|
||||
using difference_type = std::ptrdiff_t;
|
||||
using iterator_category = std::forward_iterator_tag;
|
||||
|
||||
iterator(goal const* g, unsigned idx) : m_goal(g), m_idx(idx) {}
|
||||
|
||||
value_type operator*() const {
|
||||
return std::make_tuple(m_goal->form(m_idx), m_goal->dep(m_idx), m_goal->pr(m_idx));
|
||||
}
|
||||
|
||||
iterator& operator++() {
|
||||
++m_idx;
|
||||
return *this;
|
||||
}
|
||||
|
||||
bool operator==(const iterator& other) const {
|
||||
return m_goal == other.m_goal && m_idx == other.m_idx;
|
||||
}
|
||||
|
||||
bool operator!=(const iterator& other) const {
|
||||
return !(*this == other);
|
||||
}
|
||||
|
||||
private:
|
||||
goal const* m_goal;
|
||||
unsigned m_idx;
|
||||
};
|
||||
|
||||
iterator begin() const { return iterator(this, 0); }
|
||||
iterator end() const { return iterator(this, size()); }
|
||||
};
|
||||
|
||||
std::ostream & operator<<(std::ostream & out, goal::precision p);
|
||||
|
|
|
|||
|
|
@ -25,18 +25,18 @@ Notes:
|
|||
static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
|
||||
out << "numbers in decimal:\n";
|
||||
algebraic_numbers::manager & m = rs.m();
|
||||
for (const auto& r : rs) {
|
||||
m.display_decimal(out, r, 10);
|
||||
for (unsigned i = 0; i < rs.size(); i++) {
|
||||
m.display_decimal(out, rs[i], 10);
|
||||
out << "\n";
|
||||
}
|
||||
out << "numbers as root objects\n";
|
||||
for (const auto& r : rs) {
|
||||
m.display_root(out, r);
|
||||
for (unsigned i = 0; i < rs.size(); i++) {
|
||||
m.display_root(out, rs[i]);
|
||||
out << "\n";
|
||||
}
|
||||
out << "numbers as intervals\n";
|
||||
for (const auto& r : rs) {
|
||||
m.display_interval(out, r);
|
||||
for (unsigned i = 0; i < rs.size(); i++) {
|
||||
m.display_interval(out, rs[i]);
|
||||
out << "\n";
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -158,8 +158,8 @@ struct gomory_test {
|
|||
TRACE("gomory_cut_detail", tout << "pol.size() > 1" << std::endl;);
|
||||
lcm_den = lcm(lcm_den, denominator(k));
|
||||
TRACE("gomory_cut_detail", tout << "k: " << k << " lcm_den: " << lcm_den << "\n";
|
||||
for (const auto& p : pol) {
|
||||
tout << p.first << " " << p.second << "\n";
|
||||
for (unsigned i = 0; i < pol.size(); i++) {
|
||||
tout << pol[i].first << " " << pol[i].second << "\n";
|
||||
}
|
||||
tout << "k: " << k << "\n";);
|
||||
lp_assert(lcm_den.is_pos());
|
||||
|
|
@ -172,8 +172,8 @@ struct gomory_test {
|
|||
k *= lcm_den;
|
||||
}
|
||||
TRACE("gomory_cut_detail", tout << "after *lcm\n";
|
||||
for (const auto& p : pol) {
|
||||
tout << p.first << " * v" << p.second << "\n";
|
||||
for (unsigned i = 0; i < pol.size(); i++) {
|
||||
tout << pol[i].first << " * v" << pol[i].second << "\n";
|
||||
}
|
||||
tout << "k: " << k << "\n";);
|
||||
|
||||
|
|
@ -210,7 +210,7 @@ struct gomory_test {
|
|||
bool some_int_columns = false;
|
||||
mpq f_0 = fractional_part(get_value(inf_col));
|
||||
mpq one_min_f_0 = 1 - f_0;
|
||||
for (const auto& pp : row) {
|
||||
for ( auto pp : row) {
|
||||
a = pp.first;
|
||||
x_j = pp.second;
|
||||
if (x_j == inf_col)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue