From 91ac15d716d424135f7db8bb96179872aff98862 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 4 Aug 2021 10:32:18 -0700
Subject: [PATCH] add u256

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/bigfix/u256.cpp           |  6 ++++++
 src/math/bigfix/u256.h             | 15 +++++++++++++++
 src/math/polysat/fixplex_def.h     |  3 ---
 src/math/polysat/linear_solver.cpp |  5 +++++
 4 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/src/math/bigfix/u256.cpp b/src/math/bigfix/u256.cpp
index cd3dba633..c0cb61a68 100644
--- a/src/math/bigfix/u256.cpp
+++ b/src/math/bigfix/u256.cpp
@@ -13,6 +13,12 @@ u256::u256(uint64_t n) {
     m_num[1] = m_num[2] = m_num[3] = 0;
 }
 
+u256::u256(int n) {
+    SASSERT(n >= 0);
+    m_num[0] = n;
+    m_num[1] = m_num[2] = m_num[3] = 0;
+}
+
 u256::u256(rational const& n) {
 #if 1
     for (unsigned i = 0; i < 4; ++i) {
diff --git a/src/math/bigfix/u256.h b/src/math/bigfix/u256.h
index be60e6050..d0addf591 100644
--- a/src/math/bigfix/u256.h
+++ b/src/math/bigfix/u256.h
@@ -9,8 +9,13 @@ class u256 {
 public:
     u256();
     u256(uint64_t n);
+    u256(int n);
     u256(rational const& n);
     rational to_rational() const;
+    u256& operator=(uint64_t n) {
+        *this = u256(n);
+        return *this;
+    }
     u256 operator*(u256 const& other) const;
     u256 operator+(u256 const& other) const { u256 r = *this; return r += other; }
     u256 operator-(u256 const& other) const { u256 r = *this; return r -= other; }
@@ -43,6 +48,8 @@ public:
     bool operator>(u256 const& other) const { return other < *this; }
     bool operator>=(u256 const& other) const { return !(*this < other); }
 
+    bool operator==(uint64_t other) const { return m_num[0] == other && m_num[1] == 0 && m_num[2] == 0 && m_num[3] == 0; }
+    bool operator!=(uint64_t other) const { return !(m_num[0] == other && m_num[1] == 0 && m_num[2] == 0 && m_num[3] == 0); }
     bool operator<(uint64_t other) const;
     bool operator<=(uint64_t other) const { return !(*this > other); }
     bool operator>(uint64_t other) const;
@@ -63,4 +70,12 @@ inline std::ostream& operator<<(std::ostream& out, u256 const& u) {
 inline bool operator<(uint64_t n, u256 const& y) { return y > n; }
 inline bool operator<=(uint64_t n, u256 const& y) { return y >= n; }
 inline bool operator>(uint64_t n, u256 const& y) { return y < n; }
+inline unsigned trailing_zeros(u256 const& n) {
+    NOT_IMPLEMENTED_YET();
+    return 0;
+}
+inline u256 operator-(uint64_t n, u256 const& y) {
+    u256 x(n);
+    return x - y;
+}
 inline bool operator>=(uint64_t n, u256 const& y) { return y <= n; }
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index 878661362..f26f303b6 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -1224,7 +1224,4 @@ namespace polysat {
         st.update("fixplex num non-integral", m_num_non_integral);
         st.update("fixplex num approximated row additions", m_stats.m_num_approx);
     }
-
-
-
 }
diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp
index 5b94e9199..420c7d0ae 100644
--- a/src/math/polysat/linear_solver.cpp
+++ b/src/math/polysat/linear_solver.cpp
@@ -15,6 +15,7 @@ Author:
 #include "math/polysat/linear_solver.h"
 #include "math/polysat/fixplex_def.h"
 #include "math/polysat/solver.h"
+#include "math/bigfix/u256.h"
 
 namespace polysat {
 
@@ -77,7 +78,11 @@ namespace polysat {
                 b = alloc(fixplex<uint64_ext>, s.m_lim);
                 break;
             case 128:
+	        NOT_IMPLEMENTED_YET();
+                break;
             case 256:
+	        b = alloc(fixplex<generic_uint_ext<u256>>, s.m_lim);
+                break;
             default:
                 NOT_IMPLEMENTED_YET();
                 break;