fixes to handling signed operators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 27, 2024 · 677b5b4 · 677b5b4
1 parent b1f7965
commit 677b5b4
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 3 deletions.
diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
@@ -635,6 +635,28 @@ namespace bv {
     digit_t sls_eval::random_bits() {
         return sls_valuation::random_bits(m_rand);
     }
+
+
+    bool sls_eval::is_uninterpreted(app* e) const {
+        if (is_uninterp(e))
+            return true;
+        if (e->get_family_id() != bv.get_family_id())
+            return false;
+        switch (e->get_decl_kind()) {
+        case OP_BSREM:
+        case OP_BSREM_I:
+        case OP_BSREM0:
+        case OP_BSMOD:
+        case OP_BSMOD_I:
+        case OP_BSMOD0:
+        case OP_BSDIV:
+        case OP_BSDIV_I:
+        case OP_BSDIV0:
+            return true;
+        default:
+            return false;
+        }
+    }
 
     bool sls_eval::repair_down(app* e, unsigned i) {      
         if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
@@ -807,6 +829,7 @@ namespace bv {
         case OP_BSDIV:
         case OP_BSDIV_I:
         case OP_BSDIV0:
+            UNREACHABLE();
             // these are currently compiled to udiv and urem.
             // there is an equation that enforces equality between the semantics
             // of these operators.
@@ -1900,9 +1923,9 @@ namespace bv {
     void sls_eval::commit_eval(app* e) {
         if (!bv.is_bv(e))
             return;
-        //verbose_stream() << mk_bounded_pp(e, m) << " " << wval(e) << "\n";
+        // verbose_stream() << mk_bounded_pp(e, m) << " " << wval(e) << "\n";
         //
-        // SASSERT(wval(e).commit_eval());
+        SASSERT(wval(e).commit_eval());
         VERIFY(wval(e).commit_eval());
     }
 

diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h
@@ -160,6 +160,8 @@ namespace bv {
 
         bool eval_is_correct(app* e);
 
+        bool is_uninterpreted(app* e) const;
+
         expr_ref get_value(app* e);
 
         bool bval1(app* e) const;

diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp
@@ -107,7 +107,7 @@ namespace sls {
 
     bool bv_plugin::repair_down(app* e) {
         unsigned n = e->get_num_args();
-        if (n == 0 || m_eval.eval_is_correct(e)) 
+        if (n == 0 || m_eval.is_uninterpreted(e) || m_eval.eval_is_correct(e)) 
             return true;        
 
         if (n == 2) {