mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 19:47:52 +00:00
Code Activity

some more copilot aided updated

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-03-16 21:14:29 -07:00
parent 2ecf6dc53c
commit 03f18c148e
5 changed files with 39 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/arith/add_bounds_tactic.cpp
View file

@ -41,8 +41,8 @@ struct is_unbounded_proc {
bool is_unbounded(goal const & g) {
ast_manager & m = g.m();
bound_manager bm(m);
for (unsigned i = 0; i < g.size(); ++i)
bm(g.form(i), g.dep(i), g.pr(i));
for (auto [f, d, p] : g)
bm(f, d, p);
is_unbounded_proc proc(bm);
return test(g, proc);
}

57
src/tactic/arith/degree_shift_tactic.cpp
View file

@ -161,11 +161,9 @@ class degree_shift_tactic : public tactic {
void display_candidates(std::ostream & out) {
out << "candidates:\n";
for (auto const& kv : m_var2degree) {
if (!kv.m_value.is_one()) {
out << "POWER: " << kv.m_value << "\n" << mk_ismt2_pp(kv.m_key, m) << "\n";
}
}
for (auto const& [k, v] : m_var2degree)
if (!v.is_one())
out << "POWER: " << v << "\n" << mk_ismt2_pp(k, m) << "\n";
}
void collect(goal const & g) {
@ -182,12 +180,11 @@ class degree_shift_tactic : public tactic {
void discard_non_candidates() {
m_pinned.reset();
ptr_vector<app> to_delete;
for (auto const& kv : m_var2degree) {
if (kv.m_value.is_one())
to_delete.push_back(kv.m_key);
for (auto const& [k, v] : m_var2degree)
if (v.is_one())
to_delete.push_back(k);
else
m_pinned.push_back(kv.m_key); // make sure it is not deleted during simplifications
}
m_pinned.push_back(k); // make sure it is not deleted during simplifications
for (app* a : to_delete)
m_var2degree.erase(a);
}
@ -199,23 +196,23 @@ class degree_shift_tactic : public tactic {
xmc = alloc(generic_model_converter, m, "degree_shift");
mc = xmc;
}
for (auto const& kv : m_var2degree) {
SASSERT(kv.m_value.is_int());
SASSERT(kv.m_value >= rational(2));
app * fresh = m.mk_fresh_const(nullptr, kv.m_key->get_decl()->get_range());
for (auto const& [k, v] : m_var2degree) {
SASSERT(v.is_int());
SASSERT(v >= rational(2));
app * fresh = m.mk_fresh_const(nullptr, k->get_decl()->get_range());
m_pinned.push_back(fresh);
m_var2var.insert(kv.m_key, fresh);
m_var2var.insert(k, fresh);
if (m_produce_models) {
xmc->hide(fresh->get_decl());
xmc->add(kv.m_key->get_decl(), mk_power(fresh, rational(1)/kv.m_value));
xmc->add(k->get_decl(), mk_power(fresh, rational(1)/v));
}
if (m_produce_proofs) {
expr * s = mk_power(kv.m_key, kv.m_value);
expr * s = mk_power(k, v);
expr * eq = m.mk_eq(fresh, s);
proof * pr1 = m.mk_def_intro(eq);
proof * result_pr = m.mk_apply_def(fresh, s, pr1);
m_pinned.push_back(result_pr);
m_var2pr.insert(kv.m_key, result_pr);
m_var2pr.insert(k, result_pr);
}
}
}
@ -235,28 +232,24 @@ class degree_shift_tactic : public tactic {
// substitute
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) {
checkpoint();
expr * curr = g->form(idx);
(*m_rw)(curr, new_curr, new_pr);
if (m_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);
}
// add >= 0 constraints for variables with even degree
for (auto const& kv : m_var2degree) {
SASSERT(kv.m_value.is_int());
SASSERT(kv.m_value >= rational(2));
if (kv.m_value.is_even()) {
app * new_var = m_var2var.find(kv.m_key);
for (auto const& [k,v] : m_var2degree) {
SASSERT(v.is_int());
SASSERT(v >= rational(2));
if (v.is_even()) {
app * new_var = m_var2var.find(k);
app * new_c = m_autil.mk_ge(new_var, m_autil.mk_numeral(rational(0), false));
proof * new_pr = nullptr;
if (m_produce_proofs) {
proof * pr = m_var2pr.find(kv.m_key);
proof * pr = m_var2pr.find(k);
new_pr = m.mk_th_lemma(m_autil.get_family_id(), new_c, 1, &pr);
}
g->assert_expr(new_c, new_pr, nullptr);