optimization of sls-arith and fix build warnings

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Jan 12, 2025 · b780b54 · b780b54
1 parent 49dba33
commit b780b54
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 13 deletions.
diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
@@ -189,7 +189,7 @@ class var_shifter : public var_shifter_core {
 */
 class inv_var_shifter : public var_shifter_core {
 protected:
-    unsigned m_shift;
+    unsigned m_shift = 0;
     void process_var(var * v) override;
 public:
     inv_var_shifter(ast_manager & m):var_shifter_core(m) {}

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
@@ -2372,8 +2372,10 @@ namespace sls {
 
     template<typename num_t>
     typename arith_base<num_t>::bool_info& arith_base<num_t>::get_bool_info(expr* e) {   
-        m_bool_info.reserve(e->get_id() + 1, bool_info(m_config.paws_init));
-        return m_bool_info[e->get_id()];
+        unsigned id = e->get_id();
+        if (id >= m_bool_info.size())
+            m_bool_info.reserve(id + 1, bool_info(m_config.paws_init));
+        return m_bool_info[id];
     }
 
     template<typename num_t>
@@ -2648,10 +2650,6 @@ namespace sls {
     void arith_base<num_t>::lookahead_num(var_t v, num_t const& delta) {       
         num_t old_value = value(v);
 
-        if (!update_num(v, delta))
-            return;
-
-        num_t new_value = old_value + delta;
         expr* e = m_vars[v].m_expr;
         if (m_last_expr != e) {
             if (m_last_expr)
@@ -2660,6 +2658,14 @@ namespace sls {
             insert_update_stack_rec(e);
             m_last_expr = e;
         }
+        else if (m_last_delta == delta)
+            return;
+        m_last_delta = delta;
+
+        num_t new_value = old_value + delta;
+
+        if (!update_num(v, delta))
+            return;
         auto score = lookahead(e, false);
         TRACE("arith_verbose", tout << "lookahead " << v << " " << mk_bounded_pp(e, m) << " := " << delta + old_value << " " << score << " (" << m_best_score << ")\n";);
         if (score > m_best_score) {
@@ -2844,7 +2850,7 @@ namespace sls {
                 add_lookahead(info, vars[(start + i) % sz]);
             if (m_updates.empty())
                 return false;
-            std::stable_sort(m_updates.begin(), m_updates.end(), [](auto const& a, auto const& b) { return a.m_var < b.m_var; });
+            std::stable_sort(m_updates.begin(), m_updates.end(), [](auto const& a, auto const& b) { return a.m_var < b.m_var || (a.m_var == b.m_var && a.m_delta < b.m_delta); });
             m_last_expr = nullptr;
             sz = m_updates.size();
             for (unsigned i = 0; i < sz; ++i) {

diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
@@ -379,7 +379,8 @@ namespace sls {
                     ev.val0.svalue = str;
                     return ev.val0.svalue;
                 }
-                NOT_IMPLEMENTED_YET();                
+                NOT_IMPLEMENTED_YET();  
+                return ev.val0.svalue;
             }
             case OP_SEQ_EMPTY: {
                 ev.val0.svalue = zstring();
@@ -626,8 +627,8 @@ namespace sls {
         IF_VERBOSE(3, verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n");
         if (ctx.is_true(e)) {
             // equality
-            if (false && ctx.rand(2) != 0 && repair_down_str_eq_edit_distance_incremental(e))
-                return true;
+            //if (false && ctx.rand(2) != 0 && repair_down_str_eq_edit_distance_incremental(e))
+            //    return true;
             if (ctx.rand(2) != 0 && repair_down_str_eq_edit_distance(e))
                 return true;
             if (ctx.rand(2) != 0 && repair_down_str_eq_unify(e))
@@ -693,7 +694,7 @@ namespace sls {
         hashtable<zstring, zstring_hash_proc, default_eq<zstring>> set;
         set.insert(zstring(""));
         for (unsigned i = 0; i < val_other.length(); ++i) {
-            for (unsigned j = val_other.length(); j > 0; ++j) {
+            for (unsigned j = val_other.length(); j-- > 0; ) {
                 zstring sub = val_other.extract(i, j);
                 if (set.contains(sub))
                     break;
@@ -1890,7 +1891,9 @@ namespace sls {
                 if (min_length < UINT_MAX && s.length() < str.length()) {
                     // reward small lengths
                     // penalize size differences (unless min_length decreases)
-                    score = 1 << (current_min_length - min_length);
+                    // TODO: fix this. this is pow(2.0, min_length - current_min_length) for double precision
+                    // but heuristic could be reconsidered
+                    score = 1 << (current_min_length - min_length); 
                     score /= ((double)abs((int)s.length() - (int)str.length()) + 1);
                 }
                 IF_VERBOSE(3, verbose_stream() << "prefix " << score << " " << min_length << ": " << str << "\n");