fixing issue #4651 (#4666)

* fixing issue #4651 * regression fix * fix #4662 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate * removing temp testing variable * Allow to skip System.loadLibrary() calls from Java Native class (#4667) * using intended utility methods for sort detection * adding ack/model Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add smt params dependency Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing file Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * deps Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * order Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * persist fields Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * dbg build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * reset caches Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * sr Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix cmake build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * shuffle dependencies Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * warnings /errors Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * update include Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing cmakelists Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * update cmake Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add depend Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add depend Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * virtual method Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * path Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move parameters from ast/rewriter to params Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move fpa Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove pragma Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * dbg Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updated sat_smt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4651 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * encoding options #4665 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * expose name inclusion as optional Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix misc issues around #4661 introduced when adding lazy push/pop to selected theories Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove lazy push from theory_lra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix dotnet build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * release nodes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * free memory in egraph Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * avoid duplicate class names frame in sat_scc and sat_smt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding euf Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * elaborate on smt/drat format outline, expose euf mode as config Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * mk-var during copy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * with bounded Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Remove duplicate binary condition. Fixes #4668. * butterfly effect on fp? Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * prepare for theory plugins Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * file Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * build fix * remove SMTFD Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * SMTFD is back (#4676) * fixing issue #4651 * regression fix * reenabled lift_ites_throttled with an additional filter, without the filter finding the model in report #4651 goes from .02s to 20s, also updated pretty printing of regexes to be more accurate * removing temp testing variable * using intended utility methods for sort detection * misc edits related to nonground regexes * bug fix of state id off by 1 calculation error and improved pretty printing with regex tooltip generated in dgml state graph * removed unused method declaration * improved id to regex value map info in generated dgml * reorgd callback function for state pretty printer * updated some comments Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Sergey Vladimirov <vlsergey@gmail.com> Co-authored-by: Christoph M. Wintersteiger <cwinter@microsoft.com> Co-authored-by: Arie Gurfinkel <arie.gurfinkel@gmail.com>
Z3Prover · Sep 8, 2020 · af54a79 · af54a79
1 parent d02b0cd
commit af54a79
Show file tree

Hide file tree

Showing 8 changed files with 281 additions and 55 deletions.
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -860,24 +860,39 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
     used in the normal form for derivatives in mk_re_derivative.
 */
 br_status seq_rewriter::lift_ites_throttled(func_decl* f, unsigned n, expr* const* args, expr_ref& result) {
-    expr* c = nullptr, *t = nullptr, *e = nullptr;
-    for (unsigned i = 0; i < n; ++i) {        
-        if (m().is_ite(args[i], c, t, e) && 
+    expr* c = nullptr, * t = nullptr, * e = nullptr;
+    for (unsigned i = 0; i < n; ++i)
+        if (m().is_ite(args[i], c, t, e) &&
+            lift_ites_filter(f, args[i]) &&
             (get_depth(t) <= 2 || t->get_ref_count() == 1 ||
-             get_depth(e) <= 2 || e->get_ref_count() == 1)) {
+                get_depth(e) <= 2 || e->get_ref_count() == 1)) {
             ptr_buffer<expr> new_args;
             for (unsigned j = 0; j < n; ++j) new_args.push_back(args[j]);
             new_args[i] = t;
             expr_ref arg1(m().mk_app(f, new_args), m());
             new_args[i] = e;
             expr_ref arg2(m().mk_app(f, new_args), m());
             result = m().mk_ite(c, arg1, arg2);
+            TRACE("seq_verbose", tout << "lifting ite: " << mk_pp(result, m()) << std::endl;);
             return BR_REWRITE2;
         }
-    }
     return BR_FAILED;
 }
 
+/* returns false iff the ite must not be lifted */
+bool seq_rewriter::lift_ites_filter(func_decl* f, expr* ite) {
+    // do not lift ites from sequences over regexes
+    // for example DO NOT lift to_re(ite(c, s, t)) to ite(c, to_re(s), to_re(t))
+    if (u().is_re(f->get_range()) && u().is_seq(m().get_sort(ite)))
+        return false;
+    // The following check is intended to avoid lifting cases such as 
+    // substring(s,0,ite(c,e1,e2)) ==> ite(c, substring(s,0,e1), substring(s,0,e2))
+    // TBD: not sure if this is too restrictive though and may block cases when such lifting is desired
+    // if (m_autil.is_int(m().get_sort(ite)) && u().is_seq(f->get_range()))
+    //    return false;
+    return true;
+}
+
 
 bool seq_rewriter::is_suffix(expr* s, expr* offset, expr* len) {
     expr_ref_vector lens(m());
@@ -3246,11 +3261,12 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         result = m().mk_true();
         return BR_DONE;
     }
-    expr* b1 = nullptr;
-    if (re().is_to_re(b, b1)) {
-        result = m_br.mk_eq_rw(a, b1);
-        return BR_REWRITE1;
+    expr_ref b_s(m());
+    if (lift_str_from_to_re(b, b_s)) {
+       result = m_br.mk_eq_rw(a, b_s);
+       return BR_REWRITE_FULL;
     }
+    expr* b1 = nullptr;
     expr* eps = nullptr;
     if (re().is_opt(b, b1) ||
         (re().is_union(b, b1, eps) && re().is_epsilon(eps)) ||
@@ -3337,6 +3353,30 @@ bool seq_rewriter::has_fixed_length_constraint(expr* a, unsigned& len) {
     return minl == maxl;
 }
 
+bool seq_rewriter::lift_str_from_to_re_ite(expr* r, expr_ref& result)
+{
+    expr* cond = nullptr, * then_r = nullptr, * else_r = nullptr;
+    expr_ref then_s(m());
+    expr_ref else_s(m());
+    if (m().is_ite(r, cond, then_r, else_r) &&
+        lift_str_from_to_re(then_r, then_s) &&
+        lift_str_from_to_re(else_r, else_s)) {
+        result = m().mk_ite(cond, then_s, else_s);
+        return true;
+    }
+    return false;
+}
+
+bool seq_rewriter::lift_str_from_to_re(expr* r, expr_ref& result)
+{
+    expr* s = nullptr;
+    if (re().is_to_re(r, s)) {
+        result = s;
+        return true;
+    }
+    return lift_str_from_to_re_ite(r, result);
+}
+
 br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
@@ -3375,11 +3415,13 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
         result = a;
         return BR_DONE;
     }
-    expr* a1 = nullptr, *b1 = nullptr;
-    if (re().is_to_re(a, a1) && re().is_to_re(b, b1)) {
-        result = re().mk_to_re(str().mk_concat(a1, b1));
+    expr_ref a_str(m());
+    expr_ref b_str(m());
+    if (lift_str_from_to_re(a, a_str) && lift_str_from_to_re(b, b_str)) {
+        result = re().mk_to_re(str().mk_concat(a_str, b_str));
         return BR_REWRITE2;
     }
+    expr* a1 = nullptr, *b1 = nullptr;
     if (re().is_star(a, a1) && re().is_star(b, b1) && a1 == b1) {
         result = a;
         return BR_DONE;
@@ -3811,7 +3853,14 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
         result = re().mk_star(re().mk_union(b1, c1));
         return BR_REWRITE2;
     }
+    if (m().is_ite(a, c, b1, c1)) {
+        if ((re().is_full_char(b1) || re().is_full_seq(b1)) &&
+            (re().is_full_char(c1) || re().is_full_seq(c1))) {
+            result = re().mk_full_seq(m().get_sort(b1));
+            return BR_REWRITE2;
+        }
 
+    }
     return BR_FAILED;
 }
 

diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
@@ -249,6 +249,7 @@ class seq_rewriter {
     br_status mk_re_derivative(expr* ele, expr* r, expr_ref& result);
 
     br_status lift_ites_throttled(func_decl* f, unsigned n, expr* const* args, expr_ref& result);
+    bool lift_ites_filter(func_decl* f, expr* ite);
 
     br_status reduce_re_eq(expr* a, expr* b, expr_ref& result);
     br_status reduce_re_is_empty(expr* r, expr_ref& result);
@@ -257,6 +258,10 @@ class seq_rewriter {
     bool non_overlap(zstring const& p1, zstring const& p2) const;
     bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result);
     bool has_fixed_length_constraint(expr* a, unsigned& len);
+    /* r = ite(c1,ite(c2,to_re(s),to_re(t)),to_re(u)) ==> returns true, result = ite(c1,ite(c2,s,t),u)*/
+    bool lift_str_from_to_re_ite(expr * r, expr_ref & result);
+    /* same as lift_to_re_from_ite and also: r = to_re(u) ==> returns true, result = u */
+    bool lift_str_from_to_re(expr * r, expr_ref & result);
 
     br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result);
     br_status mk_eq_helper(expr* a, expr* b, expr_ref& result);

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
@@ -1452,20 +1452,21 @@ app* seq_util::rex::mk_epsilon(sort* seq_sort) {
 */
 std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) const {
     SASSERT(re.u.is_seq(s));
-    if (re.u.str.is_concat(s)) {
-        expr_ref_vector es(re.m);
-        re.u.str.get_concat(s, es);
-        for (expr* e : es) {
-            if (re.u.str.is_unit(e))
-                seq_unit(out, e);
-            else
-                out << mk_pp(e, re.m);
-        }
-    }
-    else if (re.u.str.is_empty(s))
+    if (re.u.str.is_empty(s))
         out << "()";
-    else
+    else if (re.u.str.is_unit(s))
         seq_unit(out, s);
+    else if (re.u.str.is_concat(s)) {
+        expr_ref_vector es(re.m);
+        re.u.str.get_concat(s, es);
+        for (expr* e : es)
+            compact_helper_seq(out, e);
+    }
+    //using braces to indicate 'full' output
+    //for example an uninterpreted constant X will be printed as {X}
+    //while a unit sequence "X" will be printed as X
+    //thus for example (concat "X" "Y" Z "W") where Z is uninterpreted is printed as XY{Z}W
+    else out << "{" << mk_pp(s, re.m) << "}";
     return out;
 }
 
@@ -1484,7 +1485,7 @@ std::ostream& seq_util::rex::pp::compact_helper_range(std::ostream& out, expr* s
 */
 bool seq_util::rex::pp::can_skip_parenth(expr* r) const {
     expr* s;
-    return ((re.is_to_re(r, s) && re.u.str.is_unit(s)) || re.is_range(r) || re.is_empty(r) || re.is_epsilon(r));
+    return ((re.is_to_re(r, s) && re.u.str.is_unit(s)) || re.is_range(r) || re.is_empty(r) || re.is_epsilon(r) || re.is_full_char(r));
 }
 
 /*
@@ -1494,15 +1495,44 @@ std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const {
     expr* e;
     unsigned n = 0;
     if (re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) {
-        if (32 < n && n < 127)
-            out << (char)n;
-        else if (n < 16)
+        char c = (char)n;
+        if (c == '\n')
+            out << "\\n";
+        else if (c == '\r')
+            out << "\\r";
+        else if (c == '\f')
+            out << "\\f";
+        else if (c == ' ')
+            out << "\\s";
+        else if (c == '(' || c == ')' || c == '{' || c == '}' || c == '[' || c == ']' || c == '.' || c == '\\')
+            out << "\\" << c;
+        else if (32 < n && n < 127) {
+            if (html_encode) {
+                if (c == '<')
+                    out << "&lt;";
+                else if (c == '>')
+                    out << "&gt;";
+                else if (c == '&')
+                    out << "&amp;";
+                else if (c == '\"')
+                    out << "&quot;";
+                else
+                    out << "\\x" << std::hex << n;
+            }
+            else
+                out << c;
+        }
+        else if (n <= 0xF)
             out << "\\x0" << std::hex << n;
-        else
+        else if (n <= 0xFF)
             out << "\\x" << std::hex << n;
+        else if (n <= 0xFFF)
+            out << "\\u0" << std::hex << n;
+        else 
+            out << "\\u" << std::hex << n;
     }
     else
-        out << mk_pp(s, re.m);
+        out << "{" << mk_pp(s, re.m) << "}";
     return out;
 }
 
@@ -1516,7 +1546,7 @@ std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
         return out << ".";
     else if (re.is_full_seq(e))
         return out << ".*";
-    else if (re.is_to_re(e, s)) 
+    else if (re.is_to_re(e, s))
         return compact_helper_seq(out, s);
     else if (re.is_range(e, s, s2)) 
         return compact_helper_range(out, s, s2);
@@ -1529,7 +1559,7 @@ std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
     else if (re.is_union(e, r1, r2)) 
         return out << pp(re, r1) << "|" << pp(re, r2);
     else if (re.is_intersection(e, r1, r2)) 
-        return out << "(" << pp(re, r1) << ")&(" << pp(re, r2) << ")";
+        return out << "(" << pp(re, r1) << (html_encode ? ")&amp;(": ")&(" ) << pp(re, r2) << ")";
     else if (re.is_complement(e, r1)) {
         if (can_skip_parenth(r1))
             return out << "~" << pp(re, r1);
@@ -1555,10 +1585,18 @@ std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
             return out << "(" << pp(re, r1) << "){" << lo << ",}";
     }
     else if (re.is_loop(e, r1, lo, hi)) {
-        if (can_skip_parenth(r1))
-            return out << pp(re, r1) << "{" << lo << "," << hi << "}";
-        else
-            return out << "(" << pp(re, r1) << "){" << lo << "," << hi << "}";
+        if (can_skip_parenth(r1)) {
+            if (lo == hi)
+                return out << pp(re, r1) << "{" << lo << "}";
+            else 
+                return out << pp(re, r1) << "{" << lo << "," << hi << "}";
+        }
+        else {
+            if (lo == hi)
+                return out << "(" << pp(re, r1) << "){" << lo << "}";
+            else
+                return out << "(" << pp(re, r1) << "){" << lo << "," << hi << "}";
+        }
     }
     else if (re.is_diff(e, r1, r2)) 
         return out << "(" << pp(re, r1) << ")\\(" << pp(re, r2) << ")";
@@ -1574,7 +1612,7 @@ std::ostream& seq_util::rex::pp::display(std::ostream& out) const {
         return out << "reverse(" << pp(re, r1) << ")";
     else
         // Else: derivative or is_of_pred
-        return out << mk_pp(e, re.m);
+        return out << "{" << mk_pp(e, re.m) << "}";
 }
 
 /*
@@ -1643,8 +1681,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
     bool is_value(false);
     bool normalized(false);
     if (e->get_family_id() == u.get_family_id()) {
-        switch (e->get_decl()->get_decl_kind())
-        {
+        switch (e->get_decl()->get_decl_kind()) {
         case OP_RE_EMPTY_SET:
             return info(true, true, true, true, true, true, false, l_false, UINT_MAX, 0);
         case OP_RE_FULL_SEQ_SET:

diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
@@ -576,13 +576,14 @@ class seq_util {
         class pp {
             seq_util::rex& re;
             expr* e;
+            bool html_encode;
             bool can_skip_parenth(expr* r) const;
             std::ostream& seq_unit(std::ostream& out, expr* s) const;
             std::ostream& compact_helper_seq(std::ostream& out, expr* s) const;
             std::ostream& compact_helper_range(std::ostream& out, expr* s1, expr* s2) const;
 
         public:
-            pp(seq_util::rex& r, expr* e) : re(r), e(e) {}
+            pp(seq_util::rex& r, expr* e, bool html = false) : re(r), e(e), html_encode(html) {}
             std::ostream& display(std::ostream&) const;
         };
     };