fix #4006

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/muz/base/rule_properties.cpp

@@ -28,7 +28,7 @@ Notes:
 using namespace datalog;
 rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p): 
     m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), 
-    m_dt(m), m_dl(m), m_a(m), m_bv(m), m_ar(m), 
+    m_dt(m), m_dl(m), m_a(m), m_bv(m), m_ar(m), m_rec(m), 
     m_generate_proof(false), m_collected(false), m_is_monotone(true) {}
 
 rule_properties::~rule_properties() {}
@@ -207,19 +207,20 @@ void rule_properties::operator()(quantifier* n) {
 void rule_properties::operator()(app* n) {
     func_decl_ref f_out(m);
     expr* n1 = nullptr, *n2 = nullptr;
+    func_decl* f = n->get_decl();
     rational r;
     if (m_is_predicate(n)) {
         insert(m_interp_pred, m_rule);
     }    
-    else if (is_uninterp(n) && !m_dl.is_rule_sort(n->get_decl()->get_range())) {
+    else if (is_uninterp(n) && !m_dl.is_rule_sort(f->get_range())) {
-        m_uninterp_funs.insert(n->get_decl(), m_rule);
+        m_uninterp_funs.insert(f, m_rule);
     }
     else if (m_dt.is_accessor(n)) {
         sort* s = m.get_sort(n->get_arg(0));
         SASSERT(m_dt.is_datatype(s));
         if (m_dt.get_datatype_constructors(s)->size() > 1) {
             bool found = false;
-            func_decl * c = m_dt.get_accessor_constructor(n->get_decl());
+            func_decl * c = m_dt.get_accessor_constructor(f);
             unsigned ut_size = m_rule->get_uninterpreted_tail_size();
             unsigned t_size  = m_rule->get_tail_size();  
             for (unsigned i = ut_size; !found && i < t_size; ++i) {
@@ -229,17 +230,20 @@ void rule_properties::operator()(app* n) {
                 }
             }
             if (!found) {
-                m_uninterp_funs.insert(n->get_decl(), m_rule);
+                m_uninterp_funs.insert(f, m_rule);
             }
         }
     }
-    else if (m_a.is_considered_uninterpreted(n->get_decl(), n->get_num_args(), n->get_args(), f_out)) {
+    else if (m_a.is_considered_uninterpreted(f, n->get_num_args(), n->get_args(), f_out)) {
-        m_uninterp_funs.insert(n->get_decl(), m_rule);
+        m_uninterp_funs.insert(f, m_rule);
     }
     else if ((m_a.is_mod(n, n1, n2) || m_a.is_div(n, n1, n2) ||
               m_a.is_idiv(n, n1, n2) || m_a.is_rem(n, n1, n2))
              && (!evaluates_to_numeral(n2, r) || r.is_zero())) {
-        m_uninterp_funs.insert(n->get_decl(), m_rule);
+        m_uninterp_funs.insert(f, m_rule);
+    }
+    else if (m_rec.is_defined(f)) {
+        m_uninterp_funs.insert(f, m_rule);
     }
     check_sort(m.get_sort(n));
 }

src/muz/base/rule_properties.h

@@ -26,6 +26,7 @@ Notes:
 #include "ast/bv_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
+#include "ast/recfun_decl_plugin.h"
 #include "muz/base/dl_rule.h"
 #include "ast/expr_functors.h"
 
@@ -40,6 +41,7 @@ namespace datalog {
         arith_util    m_a;
         bv_util       m_bv;
         array_util    m_ar;
+        recfun::util  m_rec;
         bool          m_generate_proof;
         rule*         m_rule;
         obj_map<quantifier, rule*> m_quantifiers;

src/smt/seq_eq_solver.cpp

@@ -1618,3 +1618,158 @@ bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
     return true;
 }
 
+/**
+   match X abc = defg Y, for abc, defg non-empty
+*/
+
+bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
+    if (ls.size() > 1 && is_var(ls[0]) &&
+        rs.size() > 1 && is_var(rs.back())) {
+        xs.reset();
+        ys.reset();
+        x = ls[0];
+        y = rs.back();
+        for (unsigned i = 1; i < ls.size(); ++i) {
+            if (!m_util.str.is_unit(ls[i])) return false;
+        }
+        for (unsigned i = 0; i < rs.size()-1; ++i) {
+            if (!m_util.str.is_unit(rs[i])) return false;
+        }
+        xs.append(ls.size()-1, ls.c_ptr() + 1);
+        ys.append(rs.size()-1, rs.c_ptr());
+        return true;
+    }
+    return false;
+}
+
+/*
+  match: Description TBD
+*/
+
+bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                            expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, 
+                            expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
+    if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
+        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+        unsigned l_start = 1;
+        for (; l_start < ls.size()-1; ++l_start) {
+            if (m_util.str.is_unit(ls[l_start])) break;
+        }
+        if (l_start == ls.size()-1) return false;
+        unsigned l_end = l_start;
+        for (; l_end < ls.size()-1; ++l_end) {
+            if (!m_util.str.is_unit(ls[l_end])) break;
+        }
+        --l_end;
+        unsigned r_start = 1;
+        for (; r_start < rs.size()-1; ++r_start) {
+            if (m_util.str.is_unit(rs[r_start])) break;
+        }
+        if (r_start == rs.size()-1) return false;
+        unsigned r_end = r_start;
+        for (; r_end < rs.size()-1; ++r_end) {
+            if (!m_util.str.is_unit(rs[r_end])) break;
+        }
+        --r_end;
+        for (unsigned i = l_start; i < l_end+1; ++i) {
+            if (!m_util.str.is_unit(ls[i])) return false;
+        }
+        for (unsigned i = r_start; i < r_end+1; ++i) {
+            if (!m_util.str.is_unit(rs[i])) return false;
+        }
+        xs.reset();
+        xs.append(l_end-l_start+1, ls.c_ptr()+l_start);
+        x1 = m_util.str.mk_concat(l_start, ls.c_ptr());
+        x2 = m_util.str.mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1);
+        ys.reset();
+        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+        return true;
+    }
+    return false;
+}
+
+/*
+  match: Description TBD
+*/
+
+bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                               expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
+    if (ls.size() > 1 && (is_var(ls[0]) || flag1) &&
+        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+        unsigned l_start = ls.size()-1;
+        for (; l_start > 0; --l_start) {
+            if (!m_util.str.is_unit(ls[l_start])) break;
+        }
+        if (l_start == ls.size()-1) return false;
+        ++l_start;
+        unsigned r_end = rs.size()-2;
+        for (; r_end > 0; --r_end) {
+            if (m_util.str.is_unit(rs[r_end])) break;
+        }
+        if (r_end == 0) return false;
+        unsigned r_start = r_end;
+        for (; r_start > 0; --r_start) {
+            if (!m_util.str.is_unit(rs[r_start])) break;
+        }
+        ++r_start;
+        for (unsigned i = l_start; i < ls.size(); ++i) {
+            if (!m_util.str.is_unit(ls[i])) return false;
+        }
+        for (unsigned i = r_start; i < r_end+1; ++i) {
+            if (!m_util.str.is_unit(rs[i])) return false;
+        }
+        xs.reset();
+        xs.append(ls.size()-l_start, ls.c_ptr()+l_start);
+        x = m_util.str.mk_concat(l_start, ls.c_ptr());
+        ys.reset();
+        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+        return true;
+    }
+    return false;
+}
+
+/*
+  match: Description TBD
+*/
+
+bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                                expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
+    if (ls.size() > 1 && (is_var(ls.back()) || flag1) &&
+        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
+        unsigned l_start = 0;
+        for (; l_start < ls.size()-1; ++l_start) {
+            if (!m_util.str.is_unit(ls[l_start])) break;
+        }
+        if (l_start == 0) return false;
+        unsigned r_start = 1;
+        for (; r_start < rs.size()-1; ++r_start) {
+            if (m_util.str.is_unit(rs[r_start])) break;
+        }
+        if (r_start == rs.size()-1) return false;
+        unsigned r_end = r_start;
+        for (; r_end < rs.size()-1; ++r_end) {
+            if (!m_util.str.is_unit(rs[r_end])) break;
+        }
+        --r_end;
+        for (unsigned i = 0; i < l_start; ++i) {
+            if (!m_util.str.is_unit(ls[i])) return false;
+        }
+        for (unsigned i = r_start; i < r_end+1; ++i) {
+            if (!m_util.str.is_unit(rs[i])) return false;
+        }
+        xs.reset();
+        xs.append(l_start, ls.c_ptr());
+        x = m_util.str.mk_concat(ls.size()-l_start, ls.c_ptr()+l_start);
+        ys.reset();
+        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
+        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
+        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
+        return true;
+    }
+    return false;
+}
+

src/smt/theory_seq.cpp

@@ -1168,143 +1168,6 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
     return false;
 }
 
-bool theory_seq::is_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr_ref& y) {
-    if (ls.size() > 1 && is_var(ls[0]) &&
-        rs.size() > 1 && is_var(rs.back())) {
-        xs.reset();
-        ys.reset();
-        x = ls[0];
-        y = rs.back();
-        for (unsigned i = 1; i < ls.size(); ++i) {
-            if (!m_util.str.is_unit(ls[i])) return false;
-        }
-        for (unsigned i = 0; i < rs.size()-1; ++i) {
-            if (!m_util.str.is_unit(rs[i])) return false;
-        }
-        xs.append(ls.size()-1, ls.c_ptr() + 1);
-        ys.append(rs.size()-1, rs.c_ptr());
-        return true;
-    }
-    return false;
-}
-
-bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                            expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
-    if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
-        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
-        unsigned l_start = 1;
-        for (; l_start < ls.size()-1; ++l_start) {
-            if (m_util.str.is_unit(ls[l_start])) break;
-        }
-        if (l_start == ls.size()-1) return false;
-        unsigned l_end = l_start;
-        for (; l_end < ls.size()-1; ++l_end) {
-            if (!m_util.str.is_unit(ls[l_end])) break;
-        }
-        --l_end;
-        unsigned r_start = 1;
-        for (; r_start < rs.size()-1; ++r_start) {
-            if (m_util.str.is_unit(rs[r_start])) break;
-        }
-        if (r_start == rs.size()-1) return false;
-        unsigned r_end = r_start;
-        for (; r_end < rs.size()-1; ++r_end) {
-            if (!m_util.str.is_unit(rs[r_end])) break;
-        }
-        --r_end;
-        for (unsigned i = l_start; i < l_end+1; ++i) {
-            if (!m_util.str.is_unit(ls[i])) return false;
-        }
-        for (unsigned i = r_start; i < r_end+1; ++i) {
-            if (!m_util.str.is_unit(rs[i])) return false;
-        }
-        xs.reset();
-        xs.append(l_end-l_start+1, ls.c_ptr()+l_start);
-        x1 = m_util.str.mk_concat(l_start, ls.c_ptr());
-        x2 = m_util.str.mk_concat(ls.size()-l_end-1, ls.c_ptr()+l_end+1);
-        ys.reset();
-        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
-        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
-        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
-        return true;
-    }
-    return false;
-}
-
-bool theory_seq::is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-                               expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
-    if (ls.size() > 1 && (is_var(ls[0]) || flag1) &&
-        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
-        unsigned l_start = ls.size()-1;
-        for (; l_start > 0; --l_start) {
-            if (!m_util.str.is_unit(ls[l_start])) break;
-        }
-        if (l_start == ls.size()-1) return false;
-        ++l_start;
-        unsigned r_end = rs.size()-2;
-        for (; r_end > 0; --r_end) {
-            if (m_util.str.is_unit(rs[r_end])) break;
-        }
-        if (r_end == 0) return false;
-        unsigned r_start = r_end;
-        for (; r_start > 0; --r_start) {
-            if (!m_util.str.is_unit(rs[r_start])) break;
-        }
-        ++r_start;
-        for (unsigned i = l_start; i < ls.size(); ++i) {
-            if (!m_util.str.is_unit(ls[i])) return false;
-        }
-        for (unsigned i = r_start; i < r_end+1; ++i) {
-            if (!m_util.str.is_unit(rs[i])) return false;
-        }
-        xs.reset();
-        xs.append(ls.size()-l_start, ls.c_ptr()+l_start);
-        x = m_util.str.mk_concat(l_start, ls.c_ptr());
-        ys.reset();
-        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
-        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
-        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
-        return true;
-    }
-    return false;
-}
-
-bool theory_seq::is_ternary_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, 
-        expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1) {
-    if (ls.size() > 1 && (is_var(ls.back()) || flag1) &&
-        rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
-        unsigned l_start = 0;
-        for (; l_start < ls.size()-1; ++l_start) {
-            if (!m_util.str.is_unit(ls[l_start])) break;
-        }
-        if (l_start == 0) return false;
-        unsigned r_start = 1;
-        for (; r_start < rs.size()-1; ++r_start) {
-            if (m_util.str.is_unit(rs[r_start])) break;
-        }
-        if (r_start == rs.size()-1) return false;
-        unsigned r_end = r_start;
-        for (; r_end < rs.size()-1; ++r_end) {
-            if (!m_util.str.is_unit(rs[r_end])) break;
-        }
-        --r_end;
-        for (unsigned i = 0; i < l_start; ++i) {
-            if (!m_util.str.is_unit(ls[i])) return false;
-        }
-        for (unsigned i = r_start; i < r_end+1; ++i) {
-            if (!m_util.str.is_unit(rs[i])) return false;
-        }
-        xs.reset();
-        xs.append(l_start, ls.c_ptr());
-        x = m_util.str.mk_concat(ls.size()-l_start, ls.c_ptr()+l_start);
-        ys.reset();
-        ys.append(r_end-r_start+1, rs.c_ptr()+r_start);
-        y1 = m_util.str.mk_concat(r_start, rs.c_ptr());
-        y2 = m_util.str.mk_concat(rs.size()-r_end-1, rs.c_ptr()+r_end+1);
-        return true;
-    }
-    return false;
-}
 
 bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {
     if (ls.empty() || rs.empty()) {
@@ -2521,7 +2384,18 @@ app* theory_seq::get_ite_value(expr* e) {
 model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
     app* e = n->get_owner();
     context& ctx = get_context();
-    TRACE("seq", tout << mk_pp(n->get_owner(), m) << "\n";);
+    TRACE("seq", tout << mk_pp(e, m) << "\n";);
+
+    // Shortcut for well-founded values to avoid some quadratic overhead
+    expr* x = nullptr, *y = nullptr, *z = nullptr;
+    if (m_util.str.is_concat(e, x, y) && m_util.str.is_unit(x, z) && 
+        ctx.e_internalized(z) && ctx.e_internalized(y)) {
+        sort* srt = m.get_sort(e);
+        seq_value_proc* sv = alloc(seq_value_proc, *this, n, srt);
+        sv->add_unit(ctx.get_enode(z));
+        sv->add_string(y);
+        return sv;
+    }
     e = get_ite_value(e);    
     if (m_util.is_seq(e)) {
         unsigned start = m_concat.size();