Merge remote-tracking branch 'origin' into c3

src/ast/rewriter/seq_range_collapse.cpp

@@ -21,6 +21,74 @@ Authors:
 
 namespace seq {
 
+    // Cofactor path condition `pred` (a Boolean over x = (:var 0)) -> the canonical
+    // range_predicate (union of ranges) of the characters satisfying it.  Returns
+    // false on a construct outside {true,false,and,or,not,=,char.<=} over x.
+    static bool pred_to_rp(ast_manager &m, seq_util &sq, expr *x, expr *pred,
+                           seq::range_predicate &out) {
+        unsigned maxc = sq.max_char();
+        expr *a = nullptr, *b = nullptr;
+        unsigned c = 0;
+        if (m.is_true(pred)) {
+            out = seq::range_predicate::top(maxc);
+            return true;
+        }
+        if (m.is_false(pred)) {
+            out = seq::range_predicate::empty(maxc);
+            return true;
+        }
+        if (m.is_eq(pred, a, b)) {
+            if (a == x && sq.is_const_char(b, c)) {
+                out = seq::range_predicate::singleton(c, maxc);
+                return true;
+            }
+            if (b == x && sq.is_const_char(a, c)) {
+                out = seq::range_predicate::singleton(c, maxc);
+                return true;
+            }
+            return false;
+        }
+        if (sq.is_char_le(pred, a, b)) {
+            if (b == x && sq.is_const_char(a, c)) {
+                out = seq::range_predicate::range(c, maxc, maxc);
+                return true;
+            }
+            if (a == x && sq.is_const_char(b, c)) {
+                out = seq::range_predicate::range(0, c, maxc);
+                return true;
+            }
+            return false;
+        }
+        if (m.is_not(pred, a)) {
+            seq::range_predicate s(maxc);
+            if (!pred_to_rp(m, sq, x, a, s))
+                return false;
+            out = ~s;
+            return true;
+        }
+        if (m.is_and(pred)) {
+            out = seq::range_predicate::top(maxc);
+            for (expr *arg : *to_app(pred)) {
+                seq::range_predicate s(maxc);
+                if (!pred_to_rp(m, sq, x, arg, s))
+                    return false;
+                out = out & s;
+            }
+            return true;
+        }
+        if (m.is_or(pred)) {
+            out = seq::range_predicate::empty(maxc);
+            for (expr *arg : *to_app(pred)) {
+                seq::range_predicate s(maxc);
+                if (!pred_to_rp(m, sq, x, arg, s))
+                    return false;
+                out = out | s;
+            }
+            return true;
+        }
+        return false;
+    }
+
     bool regex_to_range_predicate(seq_util& u, expr* r, range_predicate& out) {
         // The range algebra only models sets of single characters over the
         // unsigned character domain [0, max_char].  Guard against any regex
@@ -35,6 +103,7 @@ namespace seq {
 
         unsigned const max_char = u.max_char();
         auto& re = u.re;
+        auto &m = u.get_manager();
 
         if (re.is_empty(r)) {
             out = range_predicate::empty(max_char);
@@ -72,8 +141,10 @@ namespace seq {
         expr *a = nullptr, *b = nullptr, *c = nullptr;
         if (re.is_union(r, a, b)) {
             range_predicate pa(max_char), pb(max_char);
-            if (!regex_to_range_predicate(u, a, pa)) return false;
-            if (!regex_to_range_predicate(u, b, pb)) return false;
+            if (!regex_to_range_predicate(u, a, pa)) 
+                return false;
+            if (!regex_to_range_predicate(u, b, pb)) 
+                return false;
             out = pa | pb;
             return true;
         }
@@ -97,12 +168,25 @@ namespace seq {
         
         if (re.is_intersection(r, a, b)) {
             range_predicate pa(max_char), pb(max_char);
-            if (!regex_to_range_predicate(u, a, pa)) return false;
-            if (!regex_to_range_predicate(u, b, pb)) return false;
+            if (!regex_to_range_predicate(u, a, pa)) 
+                return false;
+            if (!regex_to_range_predicate(u, b, pb)) 
+                return false;
             out = pa & pb;
             return true;
         }
 
+        if (re.is_of_pred(r, a) && is_lambda(a)) {
+            auto q = to_quantifier(a);
+            if (q->get_num_decls() != 1)
+                return false;
+            auto body = q->get_expr();
+            sort *char_sort = q->get_decl_sort(0);
+            expr_ref var(m.mk_var(0, char_sort), m);
+            if (u.get_char_plugin().get_family_id() == char_sort->get_family_id() && pred_to_rp(m, u, var, body, out))
+                return true;
+        }
+
         
         // NOTE: re.complement is intentionally NOT handled here.
         //   re.complement is the SEQUENCE-level complement: its language
@@ -130,6 +214,8 @@ namespace seq {
     expr_ref range_predicate_to_regex(seq_util& u, range_predicate const& p, sort* seq_sort) {
         ast_manager& m = u.get_manager();
         sort* re_sort = u.re.mk_re(seq_sort);
+        sort *char_sort = nullptr;
+        VERIFY(u.is_seq(seq_sort, char_sort));
         if (p.is_empty())
             return expr_ref(u.re.mk_empty(re_sort), m);
         unsigned const n = p.num_ranges();
@@ -145,16 +231,40 @@ namespace seq {
         // when it has to combine our materialized output with another
         // (id-sorted) regex set.
         expr_ref_vector ranges(m);
+        expr_ref bound(m.mk_var(0, char_sort), m);
+        symbol char_sym("ch");
+        auto &ch = u.get_char_plugin();
         for (unsigned i = 0; i < n; ++i) {
             auto [lo, hi] = p[i];
-            ranges.push_back(mk_single_range_regex(u, lo, hi, re_sort));
+            ranges.push_back(m.mk_and(ch.mk_le(ch.mk_char(lo), bound), ch.mk_le(bound, ch.mk_char(hi))));
         }
-        std::sort(ranges.data(), ranges.data() + ranges.size(),
-                  [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
-        expr_ref acc(ranges.get(n - 1), m);
-        for (unsigned i = n - 1; i-- > 0; )
-            acc = expr_ref(u.re.mk_union(ranges.get(i), acc), m);
-        return acc;
+        expr_ref body(m.mk_or(ranges), m);
+        return expr_ref(m.mk_lambda(1, &char_sort, &char_sym, body), m);
+    }
+
+    expr_ref unfold_fold(seq_rewriter &rw, expr *r) {
+        auto &m = rw.m();
+        auto& u = rw.u();
+        expr_ref_pair_vector cofactors(m);  
+        rw.brz_derivative_cofactors(r, cofactors);
+        if (cofactors.empty()) 
+            return expr_ref(u.re.mk_empty(r->get_sort()), m);
+        
+        sort *seq_sort = nullptr, *char_sort = nullptr;
+        VERIFY(u.is_re(r, seq_sort));
+        VERIFY(u.is_seq(seq_sort, char_sort));
+        expr_ref var(m.mk_var(0, char_sort), m);
+        expr_ref result(m);
+        symbol ch("ch");
+        for (auto const &[c, cof] : cofactors) {
+            auto prefix = u.re.mk_of_pred(m.mk_lambda(1, &char_sort, &ch, c));
+            auto term = u.re.mk_concat(prefix, cof);
+            if (result) 
+                result = u.re.mk_union(term, result);            
+            else 
+                result = term;                   
+        }
+        return result;
     }
 
 }

src/ast/rewriter/seq_range_collapse.h

@@ -26,6 +26,7 @@ Authors:
 #pragma once
 
 #include "ast/rewriter/seq_range_predicate.h"
+#include "ast/rewriter/seq_rewriter.h"
 #include "ast/seq_decl_plugin.h"
 
 namespace seq {
@@ -68,4 +69,18 @@ namespace seq {
      */
     expr_ref range_predicate_to_regex(seq_util& u, range_predicate const& p, sort* seq_sort);
 
+    /**
+    * Unfolds and then folds the given regex expression.
+    * Unfolding, produces the symbolic derivative which is an expression with a free variable var 0
+    * of the character sort.
+     * Folding produces a regex expression that is equivalent to the original one.
+     * It is obtained by taking the cofactors of the unfold, and producing a range predicate
+     * from the conditions with var 0.
+     * Formally:
+     * cofactors F_i[var 0], r_i            <- unfold(r)
+     * of_pred(\lambda ch . F_i[ch]) . r_i  <- fold(F_i[var 0], r_i)
+     * union_i of_pred(\ ch. F_i[ch]) . r_i <- fold(unfold(r))
+    */
+    expr_ref unfold_fold(seq_rewriter &rw, expr *r);
+
 }

src/ast/seq_decl_plugin.h

@@ -229,6 +229,9 @@ public:
     unsigned max_mul(unsigned x, unsigned y) const;
 
     ast_manager& get_manager() const { return m; }
+    char_decl_plugin &get_char_plugin() const {
+        return ch;
+    }
 
     sort* mk_char_sort() const { return seq.char_sort(); }
     sort* mk_string_sort() const { return seq.string_sort(); }
@@ -240,7 +243,7 @@ public:
     bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
     bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT)  && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
     bool is_seq(expr* e) const  { return is_seq(e->get_sort()); }
-    bool is_seq(sort* s, sort*& seq) const { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
+    bool is_seq(sort* s, sort*& ch) const { return is_seq(s) && (ch = to_sort(s->get_parameter(0).get_ast()), true); }
     bool is_re(expr* e) const { return is_re(e->get_sort()); }
     bool is_re(expr* e, sort*& seq) const { return is_re(e->get_sort(), seq); }
     bool is_const_char(expr* e, unsigned& c) const;

src/smt/qi_queue.cpp

@@ -197,6 +197,9 @@ namespace smt {
     }
 
     void qi_queue::instantiate(entry & ent) {
+        if (m_context.inconsistent()) 
+            return;
+        
         // set temporary flag to enable quantifier-specific tracing in within smt_internalizer.
         flet<bool> _coming_from_quant(m_context.m_coming_from_quant, true);
 
@@ -265,7 +268,7 @@ namespace smt {
         }
 
         if (m_on_binding && !m_on_binding(q, instance)) {
-            verbose_stream() << "qi_queue: on_binding returned false, skipping instance.\n";
+            IF_VERBOSE(3, verbose_stream() << "qi_queue: on_binding returned false, skipping instance.\n";);
             return;
         }
         expr_ref lemma(m);

src/smt/smt_context.h

@@ -1781,15 +1781,16 @@ namespace smt {
         void internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy);
 
         void internalize_instance(expr * body, proof * pr, unsigned generation) {
+            if (inconsistent())
+                return;
             internalize_assertion(body, pr, generation);
             if (relevancy()) {
                 // if the instantiation creates a conflict, we backtrack immediately.
                 // to retain the conflict clause being relevant we mark it here.
                 // if the instantiation does not create a conflict, default relevancy propagation applies.
-                if (inconsistent() && is_app(body)) {
-                    for (auto arg : *to_app(body))
-                        mark_as_relevant(arg);
-                }
+                //if (inconsistent() && is_app(body)) 
+                //    for (auto arg: *to_app(body)) mark_as_relevant(arg);
+                
                 m_case_split_queue->internalize_instance_eh(body, generation);
             }
         }