inherit from std::exception

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 27, 2024 · b7b611d · b7b611d
1 parent ab1be5c
commit b7b611d
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 16 deletions.
diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
@@ -1169,33 +1169,53 @@ namespace sls {
         if (is_value(x))
             return false;
 
-        vector<zstring> conts;
+        vector<lookahead> lookaheads;
         expr_ref d_r(y, m);
         seq_rewriter seqrw(m);
         for (unsigned i = 0; i < s.length(); ++i) {
             verbose_stream() << "Derivative " << s.extract(0, i) << ": " << d_r << "\n";
             if (seq.re.is_empty(d_r))
                 break;
             zstring prefix = s.extract(0, i);
-            choose(d_r, 2, prefix, conts);
+            choose(d_r, 2, prefix, lookaheads);
             expr_ref ch(seq.str.mk_char(s[i]), m);
             d_r = seqrw.mk_derivative(ch, d_r);            
         }
-        if (!seq.re.is_empty(d_r)) 
-            choose(d_r, 2, s, conts);        
+        unsigned current_min_length = UINT_MAX;
+        if (!seq.re.is_empty(d_r)) {
+            choose(d_r, 2, s, lookaheads);
+            current_min_length = info.min_length;
+        }
+
+        unsigned global_min_length = UINT_MAX;
+        for (auto& [str, min_length] : lookaheads)
+            global_min_length = std::max(min_length, global_min_length);
+
+        verbose_stream() << "repair in_re " << current_min_length << " " 
+            << global_min_length << " " << mk_pp(e, m) << " " << s << "\n";
 
-        verbose_stream() << "repair in_re " << mk_pp(e, m) << " " << s << "\n";
-        for (auto& str : conts) 
-            verbose_stream() << "prefix " << str << "\n";
 
         // TODO: do some length analysis to prune out short candidates when there are longer ones.
         // TODO: when matching .*"bcd" with string ab, the extension abc is more interesting than aba.
         if (ctx.is_true(e)) {
-            for (auto& str : conts)
-                m_str_updates.push_back({ x, str, 1 });
+            for (auto& [str, min_length] : lookaheads) {
+                if (min_length == UINT_MAX && current_min_length < UINT_MAX)
+                    continue;
+                if (global_min_length < min_length)
+                    continue;
+                double score = 0.001;
+                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);
+                    score /= ((double)abs((int)s.length() - (int)str.length()) + 1);
+                }
+                verbose_stream() << "prefix " << score << " " << min_length << ": " << str << "\n";
+                m_str_updates.push_back({ x, str, score });
+            }
         }
         else {
-            for (auto& str : conts)
+            for (auto& [str, min_length] : lookaheads)
                 m_str_updates.push_back({ x, str + zstring(m_chars[ctx.rand(m_chars.size())]), 1});
         }
         return apply_update();
@@ -1249,9 +1269,9 @@ namespace sls {
         }
     }
 
-    void seq_plugin::choose(expr* r, unsigned k, zstring& prefix, vector<zstring>& result) {
+    void seq_plugin::choose(expr* r, unsigned k, zstring& prefix, vector<lookahead>& result) {
         auto info = seq.re.get_info(r);
-        result.push_back(prefix);
+        result.push_back({ prefix, info.min_length });
         if (k == 0)
             return;
         unsigned_vector chars;

diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h
@@ -49,12 +49,12 @@ namespace sls {
         struct str_update {
             expr* e;
             zstring value;
-            unsigned m_score;
+            double m_score;
         };
         struct int_update {
             expr* e;
             rational value;
-            unsigned m_score;
+            double m_score;
         };
         vector<str_update> m_str_updates;
         vector<int_update> m_int_updates;
@@ -91,7 +91,11 @@ namespace sls {
         // regex functionality
 
         // enumerate set of strings that can match a prefix of regex r.
-        void choose(expr* r, unsigned k, zstring& prefix, vector<zstring>& result);
+        struct lookahead {
+            zstring s;
+            unsigned min_depth;
+        };
+        void choose(expr* r, unsigned k, zstring& prefix, vector<lookahead>& result);
 
         // enumerate set of possible next chars, including possibly sampling from m_chars for whild-cards.
         void next_char(expr* r, unsigned_vector& chars);

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
@@ -63,7 +63,9 @@ namespace smt {
     class model_generator;
     class context;
 
-    struct cancel_exception {};
+    struct cancel_exception : public std::exception {
+        char const * what() const noexcept override { return "smt-canceled"; }
+    };
 
     struct enode_pp {
         context const& ctx;