fixup tabu checks to revised representation

Z3Prover · Jan 5, 2025 · b3e410b · b3e410b
1 parent 71a4801
commit b3e410b
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 18 deletions.
diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp
@@ -217,10 +217,9 @@ namespace sls {
         SASSERT(!has_overflow(src));
         src.copy_to(nw, dst);
         sup_feasible(dst);
-        if (in_range(dst)) {
-            SASSERT(can_set(dst));
+        if (can_set(dst)) 
             return true;
-        }        
+
         if (dst < m_lo && m_lo < m_hi) // dst < lo < hi 
             return false;
         if (is_zero(m_hi))
@@ -238,10 +237,8 @@ namespace sls {
         src.copy_to(nw, dst);
         dst.set_bw(bw);
         inf_feasible(dst);
-        if (in_range(dst)) {
-            SASSERT(can_set(dst));
-            return true;
-        }
+        if (can_set(dst))
+            return true;        
 
         if (dst > m_lo)
             return false;
@@ -350,10 +347,8 @@ namespace sls {
             dst[i] = (~m_is_fixed[i] & dst[i]) | (m_is_fixed[i] & m_bits[i]);
         clear_overflow_bits(dst);
         repair_sign_bits(dst);
-        if (in_range(dst)) {
-            set(eval, dst);
+        if (try_set(dst))
             return true;
-        }
         bool repaired = false;
         dst.set_bw(bw);
         if (m_lo < m_hi) {
@@ -373,10 +368,7 @@ namespace sls {
                     dst.set(i, false);
         }
         repair_sign_bits(dst);
-        if (in_range(dst)) {
-            set(eval, dst);
-            repaired = true;
-        }
+        repaired = try_set(dst);
         dst.set_bw(0);
         return repaired;
     }
@@ -450,10 +442,9 @@ namespace sls {
     bool bv_valuation::set_random(random_gen& r) {
         get_variant(m_tmp, r);
         repair_sign_bits(m_tmp);
-        if (in_range(m_tmp)) {
-            set(eval, m_tmp);
+        if (try_set(m_tmp))
             return true;
-        }
+
         for (unsigned i = 0; i < nw; ++i)
             m_tmp[i] = random_bits(r);
         clear_overflow_bits(m_tmp);

diff --git a/src/ast/sls/sls_bv_valuation.h b/src/ast/sls/sls_bv_valuation.h
@@ -336,7 +336,7 @@ namespace sls {
             out << m_bits;
             out << " ev: " << eval;
             if (!is_zero(m_is_fixed)) 
-                out << " fix:" << m_is_fixed << " " << m_fixed_values;            
+                out << " fixed bits: " << m_is_fixed << " fixed value: " << m_fixed_values;            
             if (m_lo != m_hi) 
                 out << " [" << m_lo << ", " << m_hi << "[";            
             return out;