From 7a1a2b25252b265f43f5cfca96efa064a0b28128 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 20 May 2021 15:28:26 -0700
Subject: [PATCH] make unit types generic

---
 src/math/polysat/fixplex.h         | 11 +++++++----
 src/math/polysat/linear_solver.cpp |  6 +++---
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index 67e48839d..9219fa3c0 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -254,11 +254,12 @@ namespace polysat {
     };
 
 
-    struct uint64_ext {
-        typedef uint64_t numeral;
+    template<typename uint_type>
+    struct generic_uint_ext {
+        typedef uint_type numeral;
 
         struct manager {
-            typedef uint64_t numeral;
+            typedef uint_type numeral;
             struct hash {
                 unsigned operator()(numeral const& n) const { 
                     return static_cast<unsigned>(n); 
@@ -269,7 +270,7 @@ namespace polysat {
                     return a == b;
                 }
             };
-            numeral from_rational(rational const& n) { return n.get_uint64(); }
+            numeral from_rational(rational const& n) { return static_cast<uint_type>(n.get_uint64()); }
             void reset() {}
             void reset(numeral& n) { n = 0; }
             void del(numeral const& n) {}
@@ -333,6 +334,8 @@ namespace polysat {
         typedef _scoped_numeral<manager> scoped_numeral;
     };
 
+    typedef generic_uint_ext<uint64_t> uint64_ext;
+
 
     template<typename Ext>
     inline std::ostream& operator<<(std::ostream& out, fixplex<Ext> const& fp) {
diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp
index 3e06e2019..b01ee45ba 100644
--- a/src/math/polysat/linear_solver.cpp
+++ b/src/math/polysat/linear_solver.cpp
@@ -64,12 +64,12 @@ namespace polysat {
         fixplex_base* b = m_fix.get(sz, nullptr);
         if (!b) {
             switch (sz) {
+            case 32:
+                b = alloc(fixplex<generic_uint_ext<unsigned>>, s.m_lim);
+                break;
             case 64:
                 b = alloc(fixplex<uint64_ext>, s.m_lim);
                 break;
-            case 8:
-            case 16:
-            case 32:
             case 128:
             case 256:
             default: