Skip to content

Commit 8eb8a91

Browse files
CopilotNikolajBjorner
Copilot
and
NikolajBjorner
committed
Rename structured binding variables from app1/app2/app3 to a1/a2/a3
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
1 parent 819329e commit 8eb8a91

File tree

1 file changed

+51
-51
lines changed

1 file changed

+51
-51
lines changed

‎src/smt/dyn_ack.cpp‎

Lines changed: 51 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -175,9 +175,9 @@ namespace smt {
175175

176176
void dyn_ack_manager::reset_app_pairs() {
177177
for (app_pair& p : m_app_pairs) {
178-
auto [app1, app2] = p;
179-
m.dec_ref(app1);
180-
m.dec_ref(app2);
178+
auto [a1, a2] = p;
179+
m.dec_ref(a1);
180+
m.dec_ref(a2);
181181
}
182182
m_app_pairs.reset();
183183
}
@@ -283,12 +283,12 @@ namespace smt {
283283
}
284284

285285
bool operator()(app_pair const & p1, app_pair const & p2) const {
286-
auto [app1_1, app1_2] = p1;
287-
auto [app2_1, app2_2] = p2;
286+
auto [a1_1, a1_2] = p1;
287+
auto [a2_1, a2_2] = p2;
288288
unsigned n1 = 0;
289289
unsigned n2 = 0;
290-
m_app_pair2num_occs.find(app1_1, app1_2, n1);
291-
m_app_pair2num_occs.find(app2_1, app2_2, n2);
290+
m_app_pair2num_occs.find(a1_1, a1_2, n1);
291+
m_app_pair2num_occs.find(a2_1, a2_2, n2);
292292
SASSERT(n1 > 0);
293293
SASSERT(n2 > 0);
294294
return n1 > n2;
@@ -304,33 +304,33 @@ namespace smt {
304304
svector<app_pair>::iterator it2 = it;
305305
for (; it != end; ++it) {
306306
app_pair & p = *it;
307-
auto [app1, app2] = p;
307+
auto [a1, a2] = p;
308308
if (m_instantiated.contains(p)) {
309-
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n";);
310-
m.dec_ref(app1);
311-
m.dec_ref(app2);
312-
SASSERT(!m_app_pair2num_occs.contains(app1, app2));
309+
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
310+
m.dec_ref(a1);
311+
m.dec_ref(a2);
312+
SASSERT(!m_app_pair2num_occs.contains(a1, a2));
313313
continue;
314314
}
315315
unsigned num_occs = 0;
316-
m_app_pair2num_occs.find(app1, app2, num_occs);
317-
// The following invariant is not true. app1 and
318-
// app2 may have been instantiated, and removed from
316+
m_app_pair2num_occs.find(a1, a2, num_occs);
317+
// The following invariant is not true. a1 and
318+
// a2 may have been instantiated, and removed from
319319
// m_app_pair2num_occs, but not from m_app_pairs.
320320
//
321321
// SASSERT(num_occs > 0);
322322
num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
323323
if (num_occs <= 1) {
324-
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n";);
325-
m_app_pair2num_occs.erase(app1, app2);
326-
m.dec_ref(app1);
327-
m.dec_ref(app2);
324+
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
325+
m_app_pair2num_occs.erase(a1, a2);
326+
m.dec_ref(a1);
327+
m.dec_ref(a2);
328328
continue;
329329
}
330330
*it2 = p;
331331
++it2;
332332
SASSERT(num_occs > 0);
333-
m_app_pair2num_occs.insert(app1, app2, num_occs);
333+
m_app_pair2num_occs.insert(a1, a2, num_occs);
334334
if (num_occs >= m_params.m_dack_threshold)
335335
m_to_instantiate.push_back(p);
336336
}
@@ -357,20 +357,20 @@ namespace smt {
357357
m_context.m_stats.m_num_del_dyn_ack++;
358358
app_pair p((app*)nullptr,(app*)nullptr);
359359
if (m_clause2app_pair.find(cls, p)) {
360-
auto [app1, app2] = p;
361-
SASSERT(app1 && app2);
360+
auto [a1, a2] = p;
361+
SASSERT(a1 && a2);
362362
m_instantiated.erase(p);
363363
m_clause2app_pair.erase(cls);
364-
SASSERT(!m_app_pair2num_occs.contains(app1, app2));
364+
SASSERT(!m_app_pair2num_occs.contains(a1, a2));
365365
return;
366366
}
367367
app_triple tr(0,0,0);
368368
if (m_triple.m_clause2apps.find(cls, tr)) {
369-
auto [app1, app2, app3] = tr;
370-
SASSERT(app1 && app2 && app3);
369+
auto [a1, a2, a3] = tr;
370+
SASSERT(a1 && a2 && a3);
371371
m_triple.m_instantiated.erase(tr);
372372
m_triple.m_clause2apps.erase(cls);
373-
SASSERT(!m_triple.m_app2num_occs.contains(app1, app2, app3));
373+
SASSERT(!m_triple.m_app2num_occs.contains(a1, a2, a3));
374374
return;
375375
}
376376
}
@@ -456,10 +456,10 @@ namespace smt {
456456

457457
void dyn_ack_manager::reset_app_triples() {
458458
for (app_triple& p : m_triple.m_apps) {
459-
auto [app1, app2, app3] = p;
460-
m.dec_ref(app1);
461-
m.dec_ref(app2);
462-
m.dec_ref(app3);
459+
auto [a1, a2, a3] = p;
460+
m.dec_ref(a1);
461+
m.dec_ref(a2);
462+
m.dec_ref(a3);
463463
}
464464
m_triple.m_apps.reset();
465465
}
@@ -517,12 +517,12 @@ namespace smt {
517517
}
518518

519519
bool operator()(app_triple const & p1, app_triple const & p2) const {
520-
auto [app1_1, app1_2, app1_3] = p1;
521-
auto [app2_1, app2_2, app2_3] = p2;
520+
auto [a1_1, a1_2, a1_3] = p1;
521+
auto [a2_1, a2_2, a2_3] = p2;
522522
unsigned n1 = 0;
523523
unsigned n2 = 0;
524-
m_app_triple2num_occs.find(app1_1, app1_2, app1_3, n1);
525-
m_app_triple2num_occs.find(app2_1, app2_2, app2_3, n2);
524+
m_app_triple2num_occs.find(a1_1, a1_2, a1_3, n1);
525+
m_app_triple2num_occs.find(a2_1, a2_2, a2_3, n2);
526526
SASSERT(n1 > 0);
527527
SASSERT(n2 > 0);
528528
return n1 > n2;
@@ -538,35 +538,35 @@ namespace smt {
538538
svector<app_triple>::iterator it2 = it;
539539
for (; it != end; ++it) {
540540
app_triple & p = *it;
541-
auto [app1, app2, app3] = p;
541+
auto [a1, a2, a3] = p;
542542
if (m_triple.m_instantiated.contains(p)) {
543-
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n";);
544-
m.dec_ref(app1);
545-
m.dec_ref(app2);
546-
m.dec_ref(app3);
547-
SASSERT(!m_triple.m_app2num_occs.contains(app1, app2, app3));
543+
TRACE(dyn_ack, tout << "1) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
544+
m.dec_ref(a1);
545+
m.dec_ref(a2);
546+
m.dec_ref(a3);
547+
SASSERT(!m_triple.m_app2num_occs.contains(a1, a2, a3));
548548
continue;
549549
}
550550
unsigned num_occs = 0;
551-
m_triple.m_app2num_occs.find(app1, app2, app3, num_occs);
552-
// The following invariant is not true. app1 and
553-
// app2 may have been instantiated, and removed from
551+
m_triple.m_app2num_occs.find(a1, a2, a3, num_occs);
552+
// The following invariant is not true. a1 and
553+
// a2 may have been instantiated, and removed from
554554
// m_app_triple2num_occs, but not from m_app_triples.
555555
//
556556
// SASSERT(num_occs > 0);
557557
num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
558558
if (num_occs <= 1) {
559-
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n";);
560-
m_triple.m_app2num_occs.erase(app1, app2, app3);
561-
m.dec_ref(app1);
562-
m.dec_ref(app2);
563-
m.dec_ref(app3);
559+
TRACE(dyn_ack, tout << "2) erasing:\n" << mk_pp(a1, m) << "\n" << mk_pp(a2, m) << "\n";);
560+
m_triple.m_app2num_occs.erase(a1, a2, a3);
561+
m.dec_ref(a1);
562+
m.dec_ref(a2);
563+
m.dec_ref(a3);
564564
continue;
565565
}
566566
*it2 = p;
567567
++it2;
568568
SASSERT(num_occs > 0);
569-
m_triple.m_app2num_occs.insert(app1, app2, app3, num_occs);
569+
m_triple.m_app2num_occs.insert(a1, a2, a3, num_occs);
570570
if (num_occs >= m_params.m_dack_threshold)
571571
m_triple.m_to_instantiate.push_back(p);
572572
}
@@ -582,9 +582,9 @@ namespace smt {
582582
bool dyn_ack_manager::check_invariant() const {
583583
for (auto const& kv : m_clause2app_pair) {
584584
app_pair const & p = kv.get_value();
585-
auto [app1, app2] = p;
585+
auto [a1, a2] = p;
586586
SASSERT(m_instantiated.contains(p));
587-
SASSERT(!m_app_pair2num_occs.contains(app1, app2));
587+
SASSERT(!m_app_pair2num_occs.contains(a1, a2));
588588
}
589589

590590
return true;

0 commit comments

Comments
 (0)