add notes and additional functions to sls-seq

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/ast/sls/sls_arith_base.cpp

@@ -1952,6 +1952,8 @@ namespace sls {
             for (unsigned j = i + 1; j < args.get_num_args(); ++j) {
                 auto v1 = mk_term(args.get_arg(i));
                 auto v2 = mk_term(args.get_arg(j));
+                verbose_stream() << "repair " << v1 << " " << v2 << " " 
+                    << value(v1) << " " << value(v2) << "\n";
                 if (value(v1) == value(v2)) {
                     auto new_value = value(v1) + num_t(1);
                     if (new_value == value(v2))

src/ast/sls/sls_seq_plugin.cpp

@@ -72,6 +72,19 @@ Alternate to lookahead strategy:
 Revert bias on long strings:
 - give preference to reset leaves that are assigned to long strings
 - bake in bias for shorter strings into equation solving?
+
+Equality solving using stochastic Nelson.
+- Given equality where current assignment does not satisfy it:
+  - Xw = v:
+     - let X' range over prefixes of X that matches v.
+     - non-deterministic set X <- strval0(X')
+     - non-deterministic set X <- strval0(X') + 'a' where strval0(X') + 'a' matches prefix of strval0(v), and X' is longest prefix of X that matches v.
+  - If X fully matches a prefix of v, then, in addition to the rules above:
+    - consume constant character from strval0(X)w = v
+    - reveal the next variable to solve for.
+
+  - What scores make sense to use for partial solutions?
+
 --*/
 
 #include "ast/sls/sls_seq_plugin.h"
@@ -411,23 +424,29 @@ namespace sls {
         if (m.is_bool(e))
             return;
 
-        if (seq.is_string(e->get_sort())) {
-            if (is_value(e))
-                return;
-            strval0(e) = strval1(e);
-            ctx.new_value_eh(e);
+        if (seq.str.is_itos(e)) {
+            repair_up_str_itos(e);
+            return;
+        }
+        if (seq.str.is_stoi(e)) {
+            repair_up_str_stoi(e);
             return;
         }
-
         if (seq.str.is_length(e)) {
             repair_up_str_length(e);
             return;
         }
-
         if (seq.str.is_index(e)) {
             repair_up_str_indexof(e);
             return;
         }
+        if (seq.is_string(e->get_sort())) {
+            if (is_value(e))
+                return;
+            strval0(e) = strval1(e);
+            ctx.new_value_eh(e);
+            return;
+        }
 
         verbose_stream() << "repair up nyi: " << mk_bounded_pp(e, m) << "\n";
     }
@@ -471,6 +490,35 @@ namespace sls {
         return apply_update();
     }
 
+    void seq_plugin::repair_up_str_stoi(app* e) {
+        expr* x;
+        VERIFY(seq.str.is_stoi(e, x));
+
+        rational val_e;
+        rational val_x(strval0(x).encode().c_str());
+        VERIFY(a.is_numeral(ctx.get_value(e), val_e));
+        if (val_e.is_unsigned() && val_e == val_x)
+            return;
+        if (val_x < 0)
+            update(e, rational(0));
+        else
+            update(e, val_x);
+    }
+
+    void seq_plugin::repair_up_str_itos(app* e) {
+        expr* x;
+        VERIFY(seq.str.is_itos(e, x));
+        rational val_x;
+        VERIFY(a.is_numeral(ctx.get_value(x), val_x));
+        rational val_e(strval0(e).encode().c_str());        
+        if (val_x.is_unsigned() && val_x == val_e)
+            return;
+        if (val_x < 0)
+            update(e, zstring());
+        else
+            update(e, zstring(val_x.to_string()));
+    }
+
     void seq_plugin::repair_up_str_length(app* e) {
         expr* x;
         VERIFY(seq.str.is_length(e, x));
@@ -566,21 +614,33 @@ namespace sls {
             if (seq.is_string(to_app(e)->get_arg(0)->get_sort()))
                 return repair_down_str_indexof(e);
             break;
+        case OP_STRING_CONST:
+            UNREACHABLE();
+            break;
+        case OP_STRING_ITOS:
+            return repair_down_str_itos(e);
+        case OP_STRING_STOI:
+            return repair_down_str_stoi(e);
+        case OP_STRING_UBVTOS:
+        case OP_STRING_SBVTOS:
+        case OP_STRING_TO_CODE:
+        case OP_STRING_FROM_CODE:
         case OP_SEQ_UNIT:
-        case OP_SEQ_REPLACE:
         case OP_SEQ_NTH:
         case OP_SEQ_NTH_I:
         case OP_SEQ_NTH_U:
-        case OP_SEQ_LAST_INDEX:
-        case OP_SEQ_TO_RE:
-        case OP_SEQ_IN_RE:
+        case OP_SEQ_REPLACE:
         case OP_SEQ_REPLACE_RE_ALL:
         case OP_SEQ_REPLACE_RE:
         case OP_SEQ_REPLACE_ALL:
         case OP_SEQ_MAP:
         case OP_SEQ_MAPI:
         case OP_SEQ_FOLDL:
-        case OP_SEQ_FOLDLI:           
+        case OP_SEQ_FOLDLI:
+
+        case OP_SEQ_TO_RE:
+        case OP_SEQ_IN_RE:
+
         case OP_RE_PLUS:            
         case OP_RE_STAR:
         case OP_RE_OPTION:
@@ -598,23 +658,43 @@ namespace sls {
         case OP_RE_OF_PRED:
         case OP_RE_REVERSE:
         case OP_RE_DERIVATIVE:
-        case OP_STRING_CONST:
-        case OP_STRING_ITOS:
-        case OP_STRING_STOI:
-        case OP_STRING_UBVTOS:
-        case OP_STRING_SBVTOS:
         case OP_STRING_LT:
         case OP_STRING_LE:
-        case OP_STRING_IS_DIGIT:
-        case OP_STRING_TO_CODE:
-        case OP_STRING_FROM_CODE:
-        default:            
-            break;                      
+        case OP_STRING_IS_DIGIT:            
+            break;
+        default:    
+            verbose_stream() << "unexpected repair down " << mk_bounded_pp(e, m) << "\n";
+            UNREACHABLE();
         }
         verbose_stream() << "nyi repair down " << mk_bounded_pp(e, m) << "\n";
         return false;
     }
 
+    bool seq_plugin::repair_down_str_itos(app* e) {
+        expr* x;
+        VERIFY(seq.str.is_itos(e, x));
+        zstring se = strval0(e);
+        rational r(se.encode().c_str());
+        if (r.is_int())
+            m_int_updates.push_back({ x, r, 1 });
+        else
+            m_int_updates.push_back({ x, rational(-1 - ctx.rand(10)), 1 });
+
+        return apply_update();
+    }
+
+    bool seq_plugin::repair_down_str_stoi(app* e) {
+        expr* x;
+        rational r;
+        VERIFY(seq.str.is_stoi(e, x));
+        VERIFY(a.is_numeral(ctx.get_value(e), r) && r.is_int());
+        if (r < 0)
+            return false;
+        zstring r_val(r.to_string());
+        m_str_updates.push_back({ x, r_val, 1 });
+        return apply_update();        
+    }
+
     bool seq_plugin::repair_down_str_at(app* e) {
         expr* x, * y;
         VERIFY(seq.str.is_at(e, x, y));

src/ast/sls/sls_seq_plugin.h

@@ -79,9 +79,13 @@ namespace sls {
         bool repair_down_str_replace(app* e);
         bool repair_down_str_prefixof(app* e);
         bool repair_down_str_suffixof(app* e);
+        bool repair_down_str_itos(app* e);
+        bool repair_down_str_stoi(app* e);
 
         void repair_up_str_length(app* e);
         void repair_up_str_indexof(app* e);
+        void repair_up_str_itos(app* e);
+        void repair_up_str_stoi(app* e);
 
 
         bool is_seq_predicate(expr* e);

src/smt/theory_sls.cpp

@@ -76,6 +76,10 @@ namespace smt {
         return ctx.get_num_bool_vars();
     }
 
+    void theory_sls::init_search_eh() {
+        m_init_search = true;
+    }
+
     void theory_sls::finalize() {
         if (!m_smt_plugin)
             return;
@@ -84,11 +88,14 @@ namespace smt {
         m_smt_plugin->finalize(m_model);
         m_model = nullptr;
         m_smt_plugin = nullptr;        
+        m_init_search = false;
     }
 
     void theory_sls::propagate() {
-        if (!m_smt_plugin)
+        if (!m_init_search)
             return;
+        if (!m_smt_plugin)
+            m_smt_plugin = alloc(sls::smt_plugin, * this);
         if (!m_checking) {
             expr_ref_vector fmls(m);
             for (unsigned i = 0; i < ctx.get_num_asserted_formulas(); ++i)
@@ -104,6 +111,7 @@ namespace smt {
             m_smt_plugin->collect_statistics(m_st);
             m_smt_plugin->finalize(m_model);
             m_smt_plugin = nullptr;
+            m_init_search = false;
         }
     }    
 
@@ -183,8 +191,9 @@ namespace smt {
             finalize();
         smt_params p(ctx.get_fparams());
         m_parallel_mode = p.m_sls_parallel;
-        m_smt_plugin = alloc(sls::smt_plugin, *this);    
+        m_smt_plugin = nullptr;
         m_checking = false;
+        m_init_search = false;
     }
 
     void theory_sls::collect_statistics(::statistics& st) const {
@@ -216,6 +225,7 @@ namespace smt {
             m_smt_plugin->collect_statistics(m_st);
             m_smt_plugin->finalize(m_model);
             m_smt_plugin = nullptr;
+            m_init_search = false;
         }
     }
 

src/smt/theory_sls.h

@@ -72,6 +72,7 @@ namespace smt {
         unsigned m_after_resolve_decide_count = 0;
         unsigned m_resolve_count = 0;
         unsigned m_resolve_gap = 0;
+        bool     m_init_search = false;
         ::statistics m_st;
         vector<sat::literal_vector> m_shared_clauses;
 
@@ -125,6 +126,7 @@ namespace smt {
         void inc_activity(sat::bool_var v, double inc) override;
         bool parallel_mode() const override { return m_parallel_mode; }
         bool get_smt_value(expr* v, expr_ref& value) override;
+        void init_search_eh() override;
 
     };