From 6eb81fbb9d25535fc36598ad292bb41db653426b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 8 Aug 2023 17:19:46 +0200
Subject: [PATCH] use struct

---
 src/math/polysat/slicing.cpp |  8 +++-----
 src/math/polysat/slicing.h   | 10 +++++++++-
 src/math/polysat/viable.cpp  | 11 ++++-------
 3 files changed, 16 insertions(+), 13 deletions(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index 14e4215bb..e4f909480 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -1363,7 +1363,7 @@ namespace polysat {
         SASSERT(all_of(m_egraph.nodes(), [](enode* n) { return !n->is_marked1(); }));
     }
 
-    void slicing::collect_fixed(pvar v, fixed_bits_vector& out, euf::enode_vector& out_just) {
+    void slicing::collect_fixed(pvar v, justified_fixed_bits_vector& out) {
         enode_vector& base = m_tmp2;
         SASSERT(base.empty());
         get_base(var2slice(v), base);
@@ -1373,10 +1373,8 @@ namespace polysat {
             enode* r = n->get_root();
             unsigned const w = width(n);
             unsigned const hi = lo + w - 1;
-            if (try_get_value(r, a)) {
-                out.push_back({hi, lo, a});
-                out_just.push_back(n);
-            }
+            if (try_get_value(r, a))
+                out.push_back({hi, lo, a, n});
             lo += w;
         }
     }
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index d2d30a6b1..86cded54f 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -338,8 +338,16 @@ namespace polysat {
         /** For a given variable v, find the set of variables w such that w = v[|w|:0]. */
         void collect_simple_overlaps(pvar v, pvar_vector& out);
 
+        struct justified_fixed_bits : public fixed_bits {
+            enode* just;
+
+            justified_fixed_bits(unsigned hi, unsigned lo, rational value, enode* just): fixed_bits(hi, lo, value), just(just) {}
+        };
+
+        using justified_fixed_bits_vector = vector<justified_fixed_bits>;
+
         /** Collect fixed portions of the variable v */
-        void collect_fixed(pvar v, fixed_bits_vector& out, enode_vector& out_just);
+        void collect_fixed(pvar v, justified_fixed_bits_vector& out);
         void explain_fixed(euf::enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
 
         std::ostream& display(std::ostream& out) const;
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 342b53dfa..1294fe26d 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -975,18 +975,15 @@ namespace {
 
 #if 0
         // TODO: wip
-        fixed_bits_vector fbs;
-        euf::enode_vector fbs_just;
-        s.m_slicing.collect_fixed(v, fbs, fbs_just);
+        slicing::justified_fixed_bits_vector fbs;
+        s.m_slicing.collect_fixed(v, fbs);
 
-        for (unsigned idx = fbs.size(); idx-- > 0; ) {
-            fixed_bits const& fb = fbs[idx];
-            euf::enode_pair const& just = fbs_just[idx];
+        for (auto const& fb : fbs) {
             for (unsigned i = fb.lo; i <= fb.hi; ++i) {
                 SASSERT(out_fbi.just_src[i].empty());  // since we don't get overlapping ranges from collect_fixed.
                 SASSERT(out_fbi.just_side_cond[i].empty());
                 out_fbi.fixed[i] = to_lbool(fb.value.get_bit(i - fb.lo));
-                // TODO: can add an euf::enode_pair to the fixed_bits_info. then we do not have to call explain_fixed() here already.
+                // TODO: can add an euf::enode* to the fixed_bits_info. then we do not have to call explain_fixed() here already.
                 // TODO: s.m_slicing.explain_fixed( ... );  with  out_fbi.just_src[i].push_back(...)
             }
         }