fixes based on benchmarking UFDTLIA/NIA/BV

Z3Prover · Jan 30, 2025 · e356628 · e356628
1 parent f1e0950
commit e356628
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 6 deletions.
diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
@@ -390,7 +390,8 @@ namespace sls {
         if (bv.is_ule(a, x, y)) {
             auto const& vx = wval(x);
             auto const& vy = wval(y);
-
+            m_ev.m_tmp.set_bw(vx.bw);
+            m_ev.m_tmp2.set_bw(vx.bw);
             if (is_true) {
                 if (vx.bits() <= vy.bits())
                     return 1.0;
@@ -420,6 +421,8 @@ namespace sls {
             auto const& vy = wval(y);
             // x += 2^bw-1
             // y += 2^bw-1
+            m_ev.m_tmp.set_bw(vx.bw);
+            m_ev.m_tmp2.set_bw(vx.bw);
             vy.bits().copy_to(vy.nw, m_ev.m_tmp);
             vx.bits().copy_to(vx.nw, m_ev.m_tmp2);
             m_ev.m_tmp.set(vy.bw - 1, !m_ev.m_tmp.get(vy.bw - 1));

diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp
@@ -666,7 +666,6 @@ namespace sls {
 
     void bv_valuation::tighten_range() {
 
-        // verbose_stream() << "tighten " << m_lo << " " << m_hi << " " << m_bits << "\n";
         if (!has_range())
             return;     
 
@@ -683,7 +682,7 @@ namespace sls {
         if (!has_range())
             return;
 
-        if (!in_range(m_bits)) {
+        if (!in_range(m_bits) || !in_range(m_fixed_values)) {
             if (!can_set(m_lo))
                 return;
             m_lo.copy_to(nw, m_fixed_values);
@@ -698,7 +697,6 @@ namespace sls {
                 if (hi() < rational::power_of_two(i))
                     m_is_fixed.set(i, true);
 
-        // verbose_stream() << "post tighten " << m_lo << " " << m_hi << " " << m_bits << "\n";
         SASSERT(well_formed());
     }
 

diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
@@ -277,6 +277,15 @@ namespace sls {
         if (!dt.is_datatype(e) || !g)
             return expr_ref(m);
         if (m_axiomatic_mode) {
+
+            init_values();
+            TRACE("dt", tout << "get value " << mk_bounded_pp(e, m) << " " << m_values.size() << " " << g->find(e)->get_root_id() << "\n";);
+            for (auto n : euf::enode_class(g->find(e))) {
+                auto id = n->get_id();
+                if (m_values.get(id, nullptr))
+                    return expr_ref(m_values.get(id), m);
+            }
+            m_values.reset();
             init_values();
             return expr_ref(m_values.get(g->find(e)->get_root_id()), m);
         }
@@ -696,9 +705,9 @@ namespace sls {
         }
         for (unsigned j = 0; j < accs.size(); ++j) {
             if (i == j)
-                args[i] = v0;
+                args.push_back(v0);
             else
-                args[j] = m_model->get_some_value(accs[j]->get_range());
+                args.push_back(m_model->get_some_value(accs[j]->get_range()));
         }
         expr* new_val_t = m.mk_app(c, args);
         set_eval0(t, new_val_t);