From f0c23f9b7b7b8ace3d3354cecdf1dd8df09772f6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 25 Dec 2023 11:19:37 -0800
Subject: [PATCH] make offset_claim structured similar to fixed_claim

---
 src/sat/smt/polysat/fixed_bits.cpp |  5 +++--
 src/sat/smt/polysat/types.h        | 20 +++++++++++++++++---
 src/sat/smt/polysat_solver.cpp     |  8 ++++----
 3 files changed, 24 insertions(+), 9 deletions(-)

diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp
index 515f0d019..4aec4740e 100644
--- a/src/sat/smt/polysat/fixed_bits.cpp
+++ b/src/sat/smt/polysat/fixed_bits.cpp
@@ -41,11 +41,12 @@ namespace polysat {
     // val          1011
     // next         1100
 
-    // algorith: Let i be the most significant index where fixed bits disagree with val.
+    // algorithm: Let i be the most significant index where fixed bits disagree with val.
+    // Set non-fixed values below i to 0.
     // If m_fixed[i] == l_true; then updating val to mask by fixed bits sufficies.
     // Otherwise, the range above the disagreement has to be incremented.
     // Increment the non-fixed bits by 1
-    // The first non-fixed 0 position is set to 1, non-fixed positions below are set to 0.s
+    // The first non-fixed 0 position is set to 1, non-fixed positions below are set to 0.
     // If there are none, then the value is maximal and we return false.
 
     bool fixed_bits::next(rational& val) {
diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h
index 7e5bf5e38..9acb96901 100644
--- a/src/sat/smt/polysat/types.h
+++ b/src/sat/smt/polysat/types.h
@@ -29,7 +29,7 @@ namespace polysat {
 
     using pvar_vector = unsigned_vector;
     using theory_var_pair = std::pair<theory_var, theory_var>;
-    using offset_claim = std::tuple<pvar, pvar, unsigned>;
+    
     inline const pvar null_var = UINT_MAX;
 
     class signed_constraint;
@@ -54,6 +54,12 @@ namespace polysat {
         unsigned offset;
     };
 
+    struct offset_claim : public offset_slice {
+        pvar w;
+        offset_claim() = default;
+        offset_claim(pvar w, offset_slice const& s) : offset_slice(s), w(w) {}
+    };
+
     class dependency {
         struct axiom_t {};
         std::variant<axiom_t, sat::bool_var, theory_var_pair, offset_claim, fixed_claim> m_data;
@@ -87,9 +93,17 @@ namespace polysat {
             return out << d.bool_var();
         else if (d.is_eq())
             return out << "v" << d.eq().first << " == v" << d.eq().second;
+        else if (d.is_offset_claim()) {
+            auto offs = d.offset();
+            return out << "v" << offs.v << " == v" << offs.w << " offset " << offs.offset;
+        }
+        else if (d.is_fixed_claim()) {
+            auto fixed = d.fixed();
+            return out << fixed.value << " == v" << fixed.v << " [" << fixed.hi << ":" << fixed.lo << "]";
+        }
         else {
-            auto [v1, v2, offset] = d.offset();
-            return out << "v" << v1 << " == v" << v2 << " offset " << offset;
+            UNREACHABLE();
+            return out;
         }
     }
 
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 956ecf535..4d10039e7 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -212,12 +212,12 @@ namespace polysat {
             return level;
         }
         else if (d.is_offset_claim()) {
-            auto [v, w, offset] = d.offset();
+            auto const& offs = d.offset();
             sat::literal_vector lits;
             std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
                 ctx.get_eq_antecedents(a, b, lits);                
                 };
-            explain_slice(v, w, offset, consume);
+            explain_slice(offs.v, offs.w, offs.offset, consume);
             unsigned level = 0;
             for (auto lit : lits)
                 level = std::max(level, s().lvl(lit));
@@ -287,11 +287,11 @@ namespace polysat {
                     lits.push_back(~eq_internalize(var2enode(v1), var2enode(v2)));
                 }
                 else if (d.is_offset_claim()) {
-                    auto [v, w, offset] = d.offset();
+                    auto const& o = d.offset();
                     std::function<void(euf::enode*, euf::enode*)> consume = [&](auto* a, auto* b) {
                         lits.push_back(~eq_internalize(a, b));
                     };
-                    explain_slice(v, w, offset, consume);
+                    explain_slice(o.v, o.w, o.offset, consume);
                 }
                 else if (d.is_fixed_claim()) {
                     auto const& f = d.fixed();