From 0d614b8c3642884ff3605b48006fa259399a4faa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Jan 2020 19:46:27 -0800
Subject: [PATCH] check underflows, aig fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_aig_simplifier.cpp | 21 ++++++++++++++-------
 src/util/mpq.h                 |  2 ++
 src/util/mpz.cpp               | 26 --------------------------
 3 files changed, 16 insertions(+), 33 deletions(-)

diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp
index fa792f220..835534ff1 100644
--- a/src/sat/sat_aig_simplifier.cpp
+++ b/src/sat/sat_aig_simplifier.cpp
@@ -361,6 +361,7 @@ namespace sat {
                 literal u(vt[j].first, false);
                 cut const& c1 = *vt[j].second;
                 cut nc1(c1);
+                nc1.negate();
                 uint64_t t1 = c1.table();
                 uint64_t n1 = nc1.table();
                 for (unsigned k = j + 1; k < vt.size(); ++k) {
@@ -368,8 +369,7 @@ namespace sat {
                     cut const& c2 = *vt[k].second;                
                     uint64_t t2 = c2.table();
                     uint64_t n2 = c2.ntable();
-                    // 
-                    if (u.var() == v.var() || t1 == t2 || t1 == n2) {
+                    if (t1 == t2 || t1 == n2) {
                         // already handled
                     }
                     else if ((t1 | t2) == t2) {
@@ -390,6 +390,13 @@ namespace sat {
     }
 
     void aig_simplifier::learn_implies(big& big, cut const& c, literal u, literal v) {
+        if (u == ~v) {
+            assign_unit(c, v);
+            return;
+        }
+        if (u == v) { 
+            return;
+        }
         bin_rel q, p(~u, v);
         if (m_bins.find(p, q) && q.op != none) 
             return;
@@ -497,11 +504,11 @@ namespace sat {
     }
 
     void aig_simplifier::add_dont_cares(vector<cut_set> const& cuts) {
-        if (m_config.m_enable_dont_cares) {
-            cuts2bins(cuts);
-            bins2dont_cares();
-            dont_cares2cuts(cuts);
-        }
+        if (!m_config.m_enable_dont_cares) 
+            return;
+        cuts2bins(cuts);
+        bins2dont_cares();
+        dont_cares2cuts(cuts);        
     }
 
     /**
diff --git a/src/util/mpq.h b/src/util/mpq.h
index db38d87b7..8c08fe988 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -640,6 +640,8 @@ public:
     void set(mpq & a, int n, int d) {
         SASSERT(d != 0);
         if (d < 0) {
+            SASSERT(d != INT_MIN);
+            SASSERT(n != INT_MIN);
             n = -n;
             d = -d;
         }
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 4edbdcfe9..729c5af0e 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -97,36 +97,10 @@ unsigned u_gcd(unsigned u, unsigned v) {
     if (u == v) return u << shift;
     do {
         v >>= _trailing_zeros32(v);        
-#if 1
         unsigned diff = u - v;
         unsigned mdiff = diff & (unsigned)((int)diff >> 31);
         u = v + mdiff; // min
         v = diff - 2 * mdiff;   // if v <= u: u - v, if v > u: v - u = u - v - 2 * (u - v)
-#endif
-#if 0
-        unsigned t = _bit_max(u, v);
-        u = _bit_min(u, v);
-        v = t;
-        v -= u;        
-#endif
-#if 0
-        unsigned t = std::max(u, v);
-        u = std::min(u,v);
-        v = t;
-        v -= u;        
-#endif
-#if 0
-        if (u > v) std::swap(u, v);
-        v -= u;        
-#endif
-#if 0
-        unsigned d1 = u - v;
-        unsigned d2 = v - u;
-        unsigned md21 = d2 & (unsigned)((int)d1 >> 31);
-        unsigned md12 = d1 & (unsigned)((int)d2 >> 31);
-        u = _bit_min(u, v);
-        v = md12 | md21;
-#endif
     }
     while (v != 0);
     return u << shift;