From 1d3891f8d67c87b3c98669457aaedb88049c206f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 6 Sep 2024 01:06:52 -0700
Subject: [PATCH] Refactor sls bv evaluation and fix logic checks for bit
 operations

---
 src/ast/sls/sls_bv_eval.cpp      |  8 +++++---
 src/ast/sls/sls_bv_fixed.cpp     | 26 ++++++++++++++++----------
 src/ast/sls/sls_bv_valuation.cpp |  5 +----
 3 files changed, 22 insertions(+), 17 deletions(-)

diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index c137cf166..9b1800108 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -926,15 +926,15 @@ namespace sls {
             m_tmp.set_bw(a.bw);
             if (try_above) {
                 a.set_add(m_tmp, b.bits(), m_one);
-                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp,  m_rand))
+                if (a.set_random_at_least(m_tmp,  m_rand) && m_tmp != b.bits())
                     return true;
             }
             a.set_sub(m_tmp, b.bits(), m_one);
-            if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_rand))
+            if (a.set_random_at_most(m_tmp, m_rand) && m_tmp != b.bits())
                 return true;
             if (!try_above) {
                 a.set_add(m_tmp, b.bits(), m_one);
-                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand))
+                if (a.set_random_at_least(m_tmp, m_rand) && m_tmp != b.bits())
                     return true;
             }
             return false;
@@ -1001,9 +1001,11 @@ namespace sls {
         };
         fold_oper(m_tmp2, t, i, f);
         bvval& a = wval(t, i);
+        m_tmp.set_bw(a.bw);
         for (unsigned j = 0; j < a.nw; ++j)
             m_tmp[j] = e[j] & (~m_tmp2[j] | random_bits());
 
+        //verbose_stream() << wval(t) << " " << m_tmp << "\n";
         return a.set_repair(random_bool(), m_tmp);
     }
 
diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp
index c564a26e8..784576992 100644
--- a/src/ast/sls/sls_bv_fixed.cpp
+++ b/src/ast/sls/sls_bv_fixed.cpp
@@ -32,6 +32,8 @@ namespace sls {
         for (auto e : ctx.subterms())
             set_fixed(e);
 
+        //ctx.display(verbose_stream());
+
         for (auto lit : ctx.unit_literals()) {
             auto a = ctx.atom(lit.var());
             if (!a)
@@ -40,9 +42,12 @@ namespace sls {
                 init_range(to_app(a), lit.sign());
             ev.m_fixed.setx(a->get_id(), true, false);
         }
+        //ctx.display(verbose_stream());
 
         for (auto e : ctx.subterms())
-            propagate_range_up(e);    
+            propagate_range_up(e);  
+
+        //ctx.display(verbose_stream());
     }
 
     void bv_fixed::propagate_range_up(expr* e) {
@@ -150,17 +155,17 @@ namespace sls {
         return false;
     }
 
-    bool bv_fixed::init_eq(expr* t, rational const& a, bool sign) {        
+    bool bv_fixed::init_eq(expr* t, rational const& a, bool sign) {     
         unsigned lo, hi;
         rational b(0);
-        // verbose_stream() << mk_bounded_pp(t, m) << " == " << a << "\n";
         expr* s = nullptr;        
-        if (sign)
+        if (sign && true)
             // 1 <= t - a
             init_range(nullptr, rational(1), t, -a, false);
-        else
+        if (!sign)
             // t - a <= 0
             init_range(t, -a, nullptr, rational::zero(), false);
+
         if (!sign && bv.is_bv_not(t, s)) {
             for (unsigned i = 0; i < bv.get_bv_size(s); ++i)
                 if (!a.get_bit(i))
@@ -178,11 +183,13 @@ namespace sls {
         }
         if (bv.is_extract(t, lo, hi, s)) {
             if (hi == lo) {
-                sign = sign ? a == 1 : a == 0;
+                auto sign1 = sign ? a == 1 : a == 0;
                 auto& val = ev.wval(s);
-                if (val.try_set_bit(lo, !sign)) 
-                    val.fixed.set(lo, true);                                    
+                if (val.try_set_bit(lo, !sign1)) 
+                    val.fixed.set(lo, true);
+
                 val.tighten_range();
+
             }
             else if (!sign) {
                 auto& val = ev.wval(s);
@@ -190,8 +197,7 @@ namespace sls {
                     if (val.try_set_bit(i, a.get_bit(i - lo)))
                         val.fixed.set(i, true);                
                 val.tighten_range();
-                // verbose_stream() << lo << " " << hi << " " << val << " := " << a << "\n";
-            }
+            }            
 
             if (!sign && hi + 1 == bv.get_bv_size(s)) {
                 // s < 2^lo * (a + 1) 
diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp
index cc4b13a31..29fc6b517 100644
--- a/src/ast/sls/sls_bv_valuation.cpp
+++ b/src/ast/sls/sls_bv_valuation.cpp
@@ -673,10 +673,7 @@ namespace sls {
         
         // verbose_stream() << "tighten " << m_lo << " " << m_hi << " " << m_bits << "\n";
         if (m_lo == m_hi)
-            return;
-
-        if (is_zero(m_hi)) 
-            return;        
+            return;     
 
         inf_feasible(m_lo);