updates to some_string_in_re per code review comments

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

src/ast/converters/expr_inverter.cpp

@@ -882,14 +882,13 @@ class seq_expr_inverter : public iexpr_inverter {
             return false;
         case OP_SEQ_IN_RE:
             if (uncnstr(args[0]) && seq.re.is_ground(args[1]) && seq.is_string(args[0]->get_sort())) {
-#if 1
                 zstring s1;
                 expr* re = args[1];
-                if (!rw.some_string_in_re(re, s1))
+                if (l_true != rw.some_string_in_re(re, s1))
                     return false;
                 zstring s2;
                 expr_ref not_re(seq.re.mk_complement(re), m);
-                if (!rw.some_string_in_re(not_re, s2))
+                if (l_true != rw.some_string_in_re(not_re, s2))
                     return false;
 
                 mk_fresh_uncnstr_var_for(f, r);
@@ -898,7 +897,6 @@ class seq_expr_inverter : public iexpr_inverter {
                 if (m_mc)
                     add_def(args[0], m.mk_ite(r, witness1, witness2));
                 return true;
-#endif
             }
             return false;
         default:

src/ast/rewriter/seq_rewriter.cpp

@@ -9,7 +9,7 @@ Module Name:
 
     Basic rewriting rules for sequences constraints.
 
-Author:
+Authors:
 
     Nikolaj Bjorner (nbjorner) 2015-12-5
     Murphy Berzish 2017-02-21
@@ -6146,17 +6146,17 @@ void seq_rewriter::op_cache::cleanup() {
     }
 }
 
-bool seq_rewriter::some_string_in_re(expr* r, zstring& s) {
+lbool seq_rewriter::some_string_in_re(expr* r, zstring& s) {
     sort* rs;
     (void)rs;
     // SASSERT(re().is_re(r, rs) && m_util.is_string(rs));
     expr_mark visited;
     unsigned_vector str;
 
-    if (!some_string_in_re(visited, r, str))
-        return false;
-    s = zstring(str.size(), str.data());
-    return true;
+    auto result = some_string_in_re(visited, r, str);
+    if (result == l_true)
+        s = zstring(str.size(), str.data());
+    return result;
 }
 
 struct re_eval_pos {
@@ -6166,7 +6166,7 @@ struct re_eval_pos {
     bool needs_derivation;
 };
 
-bool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vector& str) {
+lbool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vector& str) {
     SASSERT(str.empty());
     vector<re_eval_pos> todo;
     todo.push_back({ expr_ref(r, m()), 0, {}, true });
@@ -6184,7 +6184,7 @@ bool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vecto
                 continue;
             auto info = re().get_info(r);
             if (info.nullable == l_true)
-                return true;
+                return l_true;
             visited.mark(r);
             if (re().is_union(r)) {
                 for (expr* arg : *to_app(r)) {
@@ -6210,12 +6210,13 @@ bool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vecto
         }
         if (m().is_ite(r, c, th, el)) {
             unsigned low = 0, high = zstring::unicode_max_char();
-            bool hasBounds = get_bounds(c, low, high);
+            bool has_bounds = get_bounds(c, low, high);
             if (!re().is_empty(el)) {
-                exclude.push_back({ low, high });
+                if (has_bounds)
+                    exclude.push_back({ low, high });
                 todo.push_back({ expr_ref(el, m()), str.size(), std::move(exclude), false });
             }
-            if (hasBounds) {
+            if (has_bounds) {
                 // I want this case to be processed first => push it last
                 // reason: current string is only pruned
                 SASSERT(low <= high);
@@ -6256,9 +6257,9 @@ bool seq_rewriter::some_string_in_re(expr_mark& visited, expr* r, unsigned_vecto
             continue;
         }
 
-        UNREACHABLE();
+        return l_undef;
     }
-    return false;
+    return l_false;
 }
 
 bool seq_rewriter::get_bounds(expr* e, unsigned& low, unsigned& high) {

src/ast/rewriter/seq_rewriter.h

@@ -354,7 +354,7 @@ class seq_rewriter {
     void intersect(unsigned lo, unsigned hi, svector<std::pair<unsigned, unsigned>>& ranges);
 
     bool get_bounds(expr* e, unsigned& low, unsigned& high);
-    bool some_string_in_re(expr_mark& visited, expr* r, unsigned_vector& str);
+    lbool some_string_in_re(expr_mark& visited, expr* r, unsigned_vector& str);
 
 public:
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
@@ -441,6 +441,6 @@ class seq_rewriter {
     * Return true if a valid string was extracted.
     * Return false when giving up or the regular expression is empty.
     */
-    bool some_string_in_re(expr* r, zstring& s);
+    lbool some_string_in_re(expr* r, zstring& s);
 };
 

src/ast/sls/sls_seq_plugin.cpp

@@ -1847,7 +1847,7 @@ namespace sls {
 
         {
             zstring s1;
-            if (ctx.is_true(e) && rw.some_string_in_re(y, s1)) {
+            if (ctx.is_true(e) && l_true == rw.some_string_in_re(y, s1)) {
                 m_str_updates.push_back({ x, s1, 1 });
                 return apply_update();
             }