From 69e54b62c5fec780c94ac9e11fd3369b375c6c6b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 19 Jul 2023 12:56:35 +0200
Subject: [PATCH] no need to store bit-width separately

---
 src/math/polysat/slicing.cpp | 23 ++++++++++++-----------
 src/math/polysat/slicing.h   |  7 +++----
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index 13ab9ad2d..e95cb2bc3 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -119,6 +119,11 @@ namespace polysat {
         return i.is_slice() ? i : info(i.slice);
     }
 
+    unsigned slicing::width(enode* s) const {
+        SASSERT(!s->is_equality());
+        return m_bv->get_bv_size(s->get_expr());
+    }
+
     func_decl* slicing::mk_concat_decl(ptr_vector<expr> const& args) {
         SASSERT(args.size() >= 2);
         ptr_vector<sort> domain;
@@ -186,31 +191,29 @@ namespace polysat {
         return eqn;
     }
 
-    slicing::enode* slicing::alloc_enode(expr* e, unsigned num_args, enode* const* args, unsigned width, pvar var) {
-        SASSERT(width > 0);
+    slicing::enode* slicing::alloc_enode(expr* e, unsigned num_args, enode* const* args, pvar var) {
         SASSERT(!m_egraph.find(e));
         euf::enode* n = m_egraph.mk(e, 0, num_args, args);  // NOTE: the egraph keeps a strong reference to 'e'
         m_info.reserve(n->get_id() + 1);
         slice_info& i = info(n);
         i.reset();
-        i.width = width;
         i.var = var;
         return n;
     }
 
-    slicing::enode* slicing::find_or_alloc_enode(expr* e, unsigned num_args, enode* const* args, unsigned width, pvar var) {
+    slicing::enode* slicing::find_or_alloc_enode(expr* e, unsigned num_args, enode* const* args, pvar var) {
         enode* n = m_egraph.find(e);
         if (n) {
-            SASSERT_EQ(info(n).width, width);
             SASSERT_EQ(info(n).var, var);
             return n;
         }
-        return alloc_enode(e, num_args, args, width, var);
+        return alloc_enode(e, num_args, args, var);
     }
 
     slicing::enode* slicing::alloc_slice(unsigned width, pvar var) {
+        SASSERT(width > 0);
         app* a = m_ast.mk_fresh_const("s", m_bv->mk_sort(width), false);
-        return alloc_enode(a, 0, nullptr, width, var);
+        return alloc_enode(a, 0, nullptr, var);
     }
 
     void slicing::add_congruence(pvar v) {
@@ -223,7 +226,7 @@ namespace polysat {
         for (enode* n : base)
             args.push_back(n->get_expr());
         app* a = m_ast.mk_app(mk_concat_decl(args), args);
-        enode* concat = find_or_alloc_enode(a, base.size(), base.data(), width(sv), null_var);
+        enode* concat = find_or_alloc_enode(a, base.size(), base.data(), null_var);
         info(concat).slice = sv;
         base.clear();
         m_egraph.merge(sv, concat, encode_dep(dep_t()));
@@ -365,7 +368,7 @@ namespace polysat {
     slicing::enode* slicing::mk_value_slice(rational const& val, unsigned bit_width) {
         SASSERT(0 <= val && val < rational::power_of_two(bit_width));
         app* a = m_bv->mk_numeral(val, bit_width);
-        enode* s = find_or_alloc_enode(a, 0, nullptr, bit_width, null_var);
+        enode* s = find_or_alloc_enode(a, 0, nullptr, null_var);
         s->mark_interpreted();
         SASSERT(s->interpreted());
         SASSERT_EQ(get_value(s), val);
@@ -832,8 +835,6 @@ namespace polysat {
                     VERIFY(has_value(sub_lo(s)));
                 }
             }
-            // we don't need to store the width separately anymore
-            VERIFY_EQ(width(s), m_bv->get_bv_size(s->get_expr()));
             // properties below only matter for representatives
             if (!s->is_root())
                 continue;
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index a360f5025..dce54c03b 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -69,7 +69,6 @@ namespace polysat {
         // - virtual concat(...) expressions
         // - equalities between enodes (to track disequalities; currently not represented in slice_info)
         struct slice_info {
-            unsigned    width   = 0;            // number of bits in the slice
             // Cut point: if not null_cut, the slice s has been subdivided into s[|s|-1:cut+1] and s[cut:0].
             // The cut point is relative to the parent slice (rather than a root variable, which might not be unique)
             unsigned    cut     = null_cut;     // cut point, or null_cut if no subslices
@@ -112,15 +111,15 @@ namespace polysat {
         slice_info& info(euf::enode* n);
         slice_info const& info(euf::enode* n) const;
 
-        enode* alloc_enode(expr* e, unsigned num_args, enode* const* args, unsigned width, pvar var);
-        enode* find_or_alloc_enode(expr* e, unsigned num_args, enode* const* args, unsigned width, pvar var);
+        enode* alloc_enode(expr* e, unsigned num_args, enode* const* args, pvar var);
+        enode* find_or_alloc_enode(expr* e, unsigned num_args, enode* const* args, pvar var);
         enode* alloc_slice(unsigned width, pvar var = null_var);
         enode* find_or_alloc_disequality(enode* x, enode* y, sat::literal lit);
 
         enode* var2slice(pvar v) const { return m_var2slice[v]; }
         pvar slice2var(enode* s) const { return info(s).var; }
 
-        unsigned width(enode* s) const { return info(s).width; }
+        unsigned width(enode* s) const;
 
         enode* parent(enode* s) const { return info(s).parent; }