From aeec3bb6df346244479ee999addcd89f9c66c6e1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Jul 2021 10:20:01 -0700
Subject: [PATCH] viable

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/bigfix/u256.cpp | 33 ++++++++++++++++++++++++++++++---
 src/math/bigfix/u256.h   |  9 +++++++--
 2 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/src/math/bigfix/u256.cpp b/src/math/bigfix/u256.cpp
index d9c05e34c..35182b1d2 100644
--- a/src/math/bigfix/u256.cpp
+++ b/src/math/bigfix/u256.cpp
@@ -93,8 +93,6 @@ u256 u256::operator&(u256 const& other) const {
     return r;
 }
 
-
-
 u256& u256::operator*=(u256 const& other) {
     uint64_t result[8];
     Hacl_Bignum256_mul(const_cast<uint64_t*>(m_num), const_cast<uint64_t*>(other.m_num), result);
@@ -112,7 +110,7 @@ u256& u256::operator-=(u256 const& other) {
     return *this;
 }
 
-u256& u256::inv() {
+u256& u256::uminus() {
     uint64_t zero[4];
     zero[0] = zero[1] = zero[2] = zero[3] = 0;
     Hacl_Bignum256_sub(zero, const_cast<uint64_t*>(m_num), m_num);
@@ -146,6 +144,35 @@ u256 u256::mod(u256 const& other) const {
 }
 
 u256 u256::mul_inverse() const {
+    if (is_zero())
+        return *this;
+    if (is_one())
+        return *this;
+    if (is_even()) 
+        return (*this >> trailing_zeros()).mul_inverse();
+
+    u256 t0(1);
+    u256 t1(-t0);
+    u256 r0(*this);
+    u256 r1(-r0); 
+    while (!r1.is_zero()) {
+        auto tmp = t1;
+    }
+#if 0
+    numeral t0 = 1, t1 = 0 - 1;
+    numeral r0 = x, r1 = 0 - x;
+    while (r1 != 0) {
+        numeral q = r0 / r1;
+        numeral tmp = t1;
+        t1 = t0 - q * t1;
+        t0 = tmp;
+        tmp = r1;
+        r1 = r0 - q * r1;
+        r0 = tmp;
+    }
+    return t0;
+#endif
+    
     NOT_IMPLEMENTED_YET();
     return *this;
 }
diff --git a/src/math/bigfix/u256.h b/src/math/bigfix/u256.h
index 3b13d841c..0f38e362c 100644
--- a/src/math/bigfix/u256.h
+++ b/src/math/bigfix/u256.h
@@ -13,7 +13,7 @@ public:
     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; }
-    u256 operator-() const { u256 r = *this; return r.inv(); }
+    u256 operator-() const { u256 r = *this; return r.uminus(); }
     u256 operator<<(uint64_t sh) const;
     u256 operator>>(uint64_t sh) const;
     u256 operator&(u256 const& other) const;
@@ -28,7 +28,7 @@ public:
     u256& operator+=(u256 const& other);
     u256& operator*=(u256 const& other);
     u256& operator-=(u256 const& other);
-    u256& inv();  /* unary minus */
+    u256& uminus();  /* unary minus */
 
     // comparisons
     bool operator==(u256 const& other) const { return m_num[0] == other.m_num[0] && m_num[1] == other.m_num[1] && m_num[2] == other.m_num[2] && m_num[3] == other.m_num[3]; } 
@@ -54,3 +54,8 @@ public:
 inline std::ostream& operator<<(std::ostream& out, u256 const& u) {
     return u.display(out);
 }
+
+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 bool operator>=(uint64_t n, u256 const& y) { return y <= n; }