mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 23:14:40 +00:00
Code Activity

Standardize for-loop increments to prefix form (++i) (#8199)

Browse source 
* Initial plan

* Convert postfix to prefix increment in for loops

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix member variable increment conversion bug

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update API generator to produce prefix increments

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-14 19:55:31 -08:00 • committed by Nikolaj Bjorner
parent 851b8ea31c
commit 317dd92105
475 changed files with 3237 additions and 3237 deletions
Download patch file Download diff file Expand all files Collapse all files

70
src/smt/smt_context.cpp
View file

@ -1213,7 +1213,7 @@ namespace smt {
TRACE(is_ext_diseq, tout << "p2: " << enode_pp(p2, *this) << "\n";);
if (p1->get_root() != p2->get_root() && p2->get_decl() == f && p2->get_num_args() == num_args) {
unsigned j = 0;
for (j = 0; j < num_args; j++) {
for (j = 0; j < num_args; ++j) {
enode * arg1 = p1->get_arg(j)->get_root();
enode * arg2 = p2->get_arg(j)->get_root();
if (arg1 == arg2)
@ -1236,7 +1236,7 @@ namespace smt {
if (depth >= m_almost_cg_tables.size()) {
unsigned old_sz = m_almost_cg_tables.size();
m_almost_cg_tables.resize(depth+1);
for (unsigned i = old_sz; i < depth + 1; i++)
for (unsigned i = old_sz; i < depth + 1; ++i)
m_almost_cg_tables[i] = alloc(almost_cg_table);
}
almost_cg_table & table = *(m_almost_cg_tables[depth]);
@ -1285,7 +1285,7 @@ namespace smt {
// TODO
}
else {
for (unsigned i = 0; i < num_args; i++) {
for (unsigned i = 0; i < num_args; ++i) {
expr * arg = r->get_expr()->get_arg(i);
SASSERT(e_internalized(arg));
enode * _arg = get_enode(arg);
@ -1309,7 +1309,7 @@ namespace smt {
*/
bool context::propagate_eqs() {
unsigned i = 0;
for (; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
for (; i < m_eq_propagation_queue.size() && !get_cancel_flag(); ++i) {
new_eq & entry = m_eq_propagation_queue[i];
add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification);
if (inconsistent()) {
@ -1327,7 +1327,7 @@ namespace smt {
bool context::propagate_atoms() {
SASSERT(!inconsistent());
CTRACE(propagate_atoms, !m_atom_propagation_queue.empty(), tout << m_atom_propagation_queue << "\n";);
for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); i++) {
for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); ++i) {
SASSERT(!inconsistent());
literal l = m_atom_propagation_queue[i];
bool_var v = l.var();
@ -1663,7 +1663,7 @@ namespace smt {
}
void context::propagate_th_eqs() {
for (unsigned i = 0; i < m_th_eq_propagation_queue.size() && !inconsistent(); i++) {
for (unsigned i = 0; i < m_th_eq_propagation_queue.size() && !inconsistent(); ++i) {
new_th_eq curr = m_th_eq_propagation_queue[i];
theory * th = get_theory(curr.m_th_id);
SASSERT(th);
@ -1676,7 +1676,7 @@ namespace smt {
}
void context::propagate_th_diseqs() {
for (unsigned i = 0; i < m_th_diseq_propagation_queue.size() && !inconsistent(); i++) {
for (unsigned i = 0; i < m_th_diseq_propagation_queue.size() && !inconsistent(); ++i) {
new_th_eq curr = m_th_diseq_propagation_queue[i];
theory * th = get_theory(curr.m_th_id);
SASSERT(th);
@ -1884,7 +1884,7 @@ namespace smt {
counter++;
if (counter % 100 == 0) {
TRACE(activity_profile,
for (unsigned i=0; i<get_num_bool_vars(); i++) {
for (unsigned i=0; i<get_num_bool_vars(); ++i) {
tout << get_activity(i) << " ";
}
tout << "\n";);
@ -2135,7 +2135,7 @@ namespace smt {
*/
bool context::is_empty_clause(clause const * c) const {
unsigned num_lits = c->get_num_literals();
for(unsigned i = 0; i < num_lits; i++) {
for(unsigned i = 0; i < num_lits; ++i) {
literal l = c->get_literal(i);
if (get_assignment(l) != l_false)
return false;
@ -2149,7 +2149,7 @@ namespace smt {
bool context::is_unit_clause(clause const * c) const {
bool found = false;
unsigned num_lits = c->get_num_literals();
for(unsigned i = 0; i < num_lits; i++) {
for(unsigned i = 0; i < num_lits; ++i) {
literal l = c->get_literal(i);
switch (get_assignment(l)) {
case l_false:
@ -2182,7 +2182,7 @@ namespace smt {
SASSERT(!m_clauses_to_reinit.empty());
lim = m_clauses_to_reinit.size() - 1;
}
for (unsigned i = new_scope_lvl; i <= lim; i++) {
for (unsigned i = new_scope_lvl; i <= lim; ++i) {
clause_vector & v = m_clauses_to_reinit[i];
for (clause* cls : v) {
cache_generation(cls, new_scope_lvl);
@ -2193,7 +2193,7 @@ namespace smt {
scope & s = m_scopes[new_scope_lvl];
unsigned i = s.m_units_to_reassert_lim;
unsigned sz = m_units_to_reassert.size();
for (; i < sz; i++) {
for (; i < sz; ++i) {
expr* unit = m_units_to_reassert[i].m_unit.get();
cache_generation(unit, new_scope_lvl);
}
@ -2211,7 +2211,7 @@ namespace smt {
\brief See cache_generation(unsigned new_scope_lvl)
*/
void context::cache_generation(unsigned num_lits, literal const * lits, unsigned new_scope_lvl) {
for(unsigned i = 0; i < num_lits; i++) {
for(unsigned i = 0; i < num_lits; ++i) {
bool_var v = lits[i].var();
unsigned ilvl = get_intern_level(v);
if (ilvl > new_scope_lvl)
@ -2276,7 +2276,7 @@ namespace smt {
SASSERT(!m_clauses_to_reinit.empty());
lim = m_clauses_to_reinit.size() - 1;
}
for (unsigned i = m_scope_lvl+1; i <= lim; i++) {
for (unsigned i = m_scope_lvl+1; i <= lim; ++i) {
clause_vector & v = m_clauses_to_reinit[i];
for (clause* cls : v) {
if (cls->deleted()) {
@ -2289,7 +2289,7 @@ namespace smt {
bool keep = false;
if (cls->reinternalize_atoms()) {
SASSERT(cls->get_num_atoms() == cls->get_num_literals());
for (unsigned j = 0; j < 2; j++) {
for (unsigned j = 0; j < 2; ++j) {
literal l = cls->get_literal(j);
if (l.var() < num_bool_vars) {
// This boolean variable was not deleted during backtracking
@ -2306,7 +2306,7 @@ namespace smt {
unsigned ilvl = 0;
(void)ilvl;
for (unsigned j = 0; j < num; j++) {
for (unsigned j = 0; j < num; ++j) {
expr * atom = cls->get_atom(j);
bool sign = cls->get_atom_sign(j);
// Atom can be (NOT foo). This can happen, for example, when
@ -2389,7 +2389,7 @@ namespace smt {
void context::reassert_units(unsigned units_to_reassert_lim) {
unsigned i = units_to_reassert_lim;
unsigned sz = m_units_to_reassert.size();
for (; i < sz; i++) {
for (; i < sz; ++i) {
auto [unit, sign, is_relevant] = m_units_to_reassert[i];
bool gate_ctx = true;
internalize(unit, gate_ctx);
@ -2542,7 +2542,7 @@ namespace smt {
unsigned i = 2;
unsigned j = i;
bool is_taut = false;
for(; i < s; i++) {
for(; i < s; ++i) {
literal l = cls[i];
switch(get_assignment(l)) {
case l_false:
@ -2609,7 +2609,7 @@ namespace smt {
}
else if (simplify_clause(*cls)) {
TRACE(simplify_clauses_bug, display_clause_smt2(tout << "simplified\n", *cls) << "\n";);
for (unsigned idx = 0; idx < 2; idx++) {
for (unsigned idx = 0; idx < 2; ++idx) {
literal l0 = (*cls)[idx];
b_justification l0_js = get_justification(l0.var());
if (l0_js != null_b_justification &&
@ -2623,7 +2623,7 @@ namespace smt {
SASSERT(m_search_lvl == m_base_lvl);
literal_buffer simp_lits;
unsigned num_lits = cls->get_num_literals();
for(unsigned i = 0; i < num_lits; i++) {
for(unsigned i = 0; i < num_lits; ++i) {
if (i != idx) {
literal l = (*cls)[i];
SASSERT(l != l0);
@ -2767,7 +2767,7 @@ namespace smt {
unsigned num_del_cls = 0;
TRACE(del_inactive_lemmas, tout << "sz: " << sz << ", start_at: " << start_at << ", end_at: " << end_at
<< ", start_del_at: " << start_del_at << "\n";);
for (; i < end_at; i++) {
for (; i < end_at; ++i) {
clause * cls = m_lemmas[i];
if (can_delete(cls)) {
TRACE(del_inactive_lemmas, tout << "deleting: "; display_clause(tout, cls); tout << ", activity: " <<
@ -2781,7 +2781,7 @@ namespace smt {
}
}
// keep recent clauses
for (; i < sz; i++) {
for (; i < sz; ++i) {
clause * cls = m_lemmas[i];
if (cls->deleted() && can_delete(cls)) {
del_clause(true, cls);
@ -2794,7 +2794,7 @@ namespace smt {
m_lemmas.shrink(j);
if (m_fparams.m_clause_decay > 1) {
// rescale activity
for (i = start_at; i < j; i++) {
for (i = start_at; i < j; ++i) {
clause * cls = m_lemmas[i];
cls->set_activity(cls->get_activity() / m_fparams.m_clause_decay);
}
@ -2821,7 +2821,7 @@ namespace smt {
unsigned i = start_at;
unsigned j = i;
unsigned num_del_cls = 0;
for (; i < sz; i++) {
for (; i < sz; ++i) {
clause * cls = m_lemmas[i];
if (can_delete(cls)) {
if (cls->deleted()) {
@ -2884,7 +2884,7 @@ namespace smt {
expr_mark visited;
family_id fid = th->get_id();
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
for (unsigned i = 0; i < sz; ++i) {
expr * n = s.get(i);
if (uses_theory(n, fid, visited)) {
return true;
@ -4205,7 +4205,7 @@ namespace smt {
void context::forget_phase_of_vars_in_current_level() {
unsigned head = m_scope_lvl == 0 ? 0 : m_scopes[m_scope_lvl - 1].m_assigned_literals_lim;
unsigned sz = m_assigned_literals.size();
for (unsigned i = head; i < sz; i++) {
for (unsigned i = head; i < sz; ++i) {
literal l = m_assigned_literals[i];
bool_var v = l.var();
TRACE(forget_phase, tout << "forgetting phase of l: " << l << "\n";);
@ -4272,7 +4272,7 @@ namespace smt {
TRACE(resolve_conflict_bug,
tout << "m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " << m_conflict_resolution->get_lemma_intern_lvl() << "\n";
tout << "num_lits: " << num_lits << "\n";
for (unsigned i = 0; i < num_lits; i++) {
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
tout << l << " ";
display_literal_smt2(tout, l);
@ -4289,7 +4289,7 @@ namespace smt {
#ifdef Z3DEBUG
expr_ref_vector expr_lits(m);
bool_vector expr_signs;
for (unsigned i = 0; i < num_lits; i++) {
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
if (get_assignment(l) != l_false) {
std::cout << l << " " << get_assignment(l) << "\n";
@ -4318,7 +4318,7 @@ namespace smt {
// clauses are reinitialized in pop_scope.
if (m_conflict_resolution->get_lemma_intern_lvl() > m_scope_lvl) {
expr * * atoms = m_conflict_resolution->get_lemma_atoms();
for (unsigned i = 0; i < num_lits; i++) {
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
if (l.var() >= num_bool_vars) {
// This boolean variable was deleted during backtracking, it need to be recreated.
@ -4350,7 +4350,7 @@ namespace smt {
tout << "AFTER m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " <<
m_conflict_resolution->get_lemma_intern_lvl() << "\n";
tout << "num_lits: " << num_lits << "\n";
for (unsigned i = 0; i < num_lits; i++) {
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
tout << l << " ";
display_literal(tout, l);
@ -4358,7 +4358,7 @@ namespace smt {
<< mk_pp(bool_var2expr(l.var()), m) << "\n";
});
#ifdef Z3DEBUG
for (unsigned i = 0; i < num_lits; i++) {
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
if (expr_signs[i] != l.sign()) {
expr* real_atom;
@ -4388,7 +4388,7 @@ namespace smt {
}
if (counter % 1000 == 0) {
verbose_stream() << "[sat] avg. clause size: " << ((double) total/(double) counter) << ", max: " << max << std::endl;
for (unsigned i = 0; i < num_lits; i++) {
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
verbose_stream() << l.sign() << " " << mk_pp(bool_var2expr(l.var()), m) << "\n";
}
@ -4410,7 +4410,7 @@ namespace smt {
TRACE(context_lemma, tout << "new lemma: ";
literal_vector v(num_lits, lits);
std::sort(v.begin(), v.end());
for (unsigned i = 0; i < num_lits; i++) {
for (unsigned i = 0; i < num_lits; ++i) {
display_literal(tout, v[i]);
tout << "\n";
smt::display(tout, v[i], m, m_bool_var2expr.data());
@ -4519,7 +4519,7 @@ namespace smt {
void context::get_relevant_literals(expr_ref_vector & result) {
SASSERT(!inconsistent());
unsigned sz = m_b_internalized_stack.size();
for (unsigned i = 0; i < sz; i++) {
for (unsigned i = 0; i < sz; ++i) {
expr * curr = m_b_internalized_stack.get(i);
if (is_relevant(curr)) {
switch (get_assignment(curr)) {
@ -4545,7 +4545,7 @@ namespace smt {
if (m_search_lvl == m_scopes.size()) {
// do nothing... there are guesses...
}
for (unsigned i = m_search_lvl; i < m_scope_lvl; i++) {
for (unsigned i = m_search_lvl; i < m_scope_lvl; ++i) {
// This method assumes the first literal assigned in a non base scope level is a guess.
scope & s = m_scopes[i];
unsigned guess_idx = s.m_assigned_literals_lim;