seq

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

src/ast/rewriter/seq_rewriter.cpp

@@ -74,7 +74,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_SEQ_INDEX:
         if (num_args == 2) {
             expr_ref arg3(m_autil.mk_int(0), m());
-            return mk_seq_index(args[0], args[1], arg3, result);
+            result = m_util.str.mk_index(args[0], args[1], arg3);
+            return BR_REWRITE1;
         }
         SASSERT(num_args == 3);
         return mk_seq_index(args[0], args[1], args[2], result);
@@ -202,19 +203,19 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
 br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
     std::string c, d;
     if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) {
-        result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str()));
+        result = m().mk_bool_val(0 != strstr(c.c_str(), d.c_str()));
         return BR_DONE;
     }
-    // check if subsequence of a is in b.
+    // check if subsequence of b is in a.
     ptr_vector<expr> as, bs;
     m_util.str.get_concat(a, as);
     m_util.str.get_concat(b, bs);
     bool found = false;
-    for (unsigned i = 0; !found && i < bs.size(); ++i) {
+    for (unsigned i = 0; !found && i < as.size(); ++i) {
-        if (as.size() > bs.size() - i) break;
+        if (bs.size() > as.size() - i) break;
         unsigned j = 0;
-        for (; j < as.size() && as[j] == bs[i+j]; ++j) {};
+        for (; j < bs.size() && as[j] == bs[i+j]; ++j) {};
-        found = j == as.size();
+        found = j == bs.size();
     }
     if (found) {
         result = m().mk_true();
@@ -260,7 +261,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
         return BR_DONE;
     }
     
-    if (m_util.str.is_empty(b)) {
+    if (m_util.str.is_empty(b) && m_autil.is_numeral(c, r) && r.is_zero()) {
         result = c;
         return BR_DONE;
     }
@@ -380,6 +381,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE3;
     }
     if (i > 0) {
+        SASSERT(i < as.size() && i < bs.size());
         a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
         b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i); 
         result = m_util.str.mk_prefix(a, b);
@@ -657,54 +659,127 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
     }
 
     bool is_sat;
-    if (!change) {
+    unsigned szl = m_lhs.size() - head1, szr = m_rhs.size() - head2;
-        if (is_subsequence(m_lhs.size(), m_lhs.c_ptr(), m_rhs.size(), m_rhs.c_ptr(), lhs, rhs, is_sat)) {
+    expr* const* ls = m_lhs.c_ptr() + head1, * const*rs = m_rhs.c_ptr() + head2;
+    if (length_constrained(szl, ls, szr, rs, lhs, rhs, is_sat)) {
         return is_sat;
     }
-        lhs.push_back(l);
+    if (is_subsequence(szl, ls, szr, rs, lhs, rhs, is_sat)) {
-        rhs.push_back(r);
-    }
-    else if (head1 == m_lhs.size() && head2 == m_rhs.size()) {
-        // skip
-    }
-    else if (head1 == m_lhs.size()) {
-        return set_empty(m_rhs.size() - head2, m_rhs.c_ptr() + head2, lhs, rhs);
-    }
-    else if (head2 == m_rhs.size()) {
-        return set_empty(m_lhs.size() - head1, m_lhs.c_ptr() + head1, lhs, rhs);
-    }
-    else { // could solve if either side is fixed size.
-        SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size());
-        if (is_subsequence(m_lhs.size() - head1, m_lhs.c_ptr() + head1, 
-                           m_rhs.size() - head2, m_rhs.c_ptr() + head2, lhs, rhs, is_sat)) {
         return is_sat;
     }
 
-        lhs.push_back(m_util.str.mk_concat(m_lhs.size() - head1, m_lhs.c_ptr() + head1));
+	if (szl == 0 && szr == 0) {
-        rhs.push_back(m_util.str.mk_concat(m_rhs.size() - head2, m_rhs.c_ptr() + head2));
+		return true;
+	}
+    else if (!change) {
+        lhs.push_back(l);
+        rhs.push_back(r);
+    }
+    else {
+        // could solve if either side is fixed size.
+        SASSERT(szl > 0 && szr > 0);
+
+        lhs.push_back(m_util.str.mk_concat(szl, ls));
+        rhs.push_back(m_util.str.mk_concat(szr, rs));
     }
     return true;
 }
 
-bool seq_rewriter::set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs) {
+expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
+    SASSERT(n > 0);
+    ptr_vector<expr> bs;
+    for (unsigned i = 0; i < n; ++i) {
+        if (m_util.str.is_unit(as[i]) ||
+            m_util.str.is_string(as[i])) {
+            bs.push_back(as[i]);
+        }
+    }    
+    if (bs.empty()) {
+        return m_util.str.mk_empty(m().get_sort(as[0]));
+    }
+    else {
+        return m_util.str.mk_concat(bs.size(), bs.c_ptr());
+    }
+}
+
+bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) {
     std::string s;
     for (unsigned i = 0; i < sz; ++i) {
         if (m_util.str.is_unit(es[i])) {
-            return false;
+            if (all) return false;
         }
-        if (m_util.str.is_empty(es[i])) {
+        else if (m_util.str.is_empty(es[i])) {
             continue;
         }
-        if (m_util.str.is_string(es[i], s)) {
+        else if (m_util.str.is_string(es[i], s)) {
+            if (all) {
                 SASSERT(s.length() > 0);
                 return false;
             }
+        }
+        else {
             lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i])));
             rhs.push_back(es[i]);
         }
+    }
     return true;
 }
 
+bool seq_rewriter::min_length(unsigned n, expr* const* es, size_t& len) {
+    std::string s;
+    bool bounded = true;
+    len = 0;
+    for (unsigned i = 0; i < n; ++i) {
+        if (m_util.str.is_unit(es[i])) {
+            ++len;
+        }
+        else if (m_util.str.is_empty(es[i])) {
+            continue;
+        }
+        else if (m_util.str.is_string(es[i], s)) {
+            len += s.length();
+        }
+        else {
+            bounded = false;
+        }
+    }
+    return bounded;
+}
+
+bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr, expr* const* r, 
+                                      expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
+    is_sat = true;
+    size_t len1 = 0, len2 = 0;
+    bool bounded1 = min_length(szl, l, len1);
+    bool bounded2 = min_length(szr, r, len2);
+    if (bounded1 && len1 < len2) {
+        is_sat = false;
+        return true;
+    }
+    if (bounded2 && len2 < len1) {
+        is_sat = false;
+        return true;
+    }
+    if (bounded1 && len1 == len2 && len1 > 0) {
+        is_sat = set_empty(szr, r, false, lhs, rhs);
+        if (is_sat) {
+            lhs.push_back(concat_non_empty(szl, l));
+            rhs.push_back(concat_non_empty(szr, r));
+        }
+        return true;
+    }
+    if (bounded2 && len1 == len2 && len1 > 0) {
+        is_sat = set_empty(szl, l, false, lhs, rhs);
+        if (is_sat) {
+            lhs.push_back(concat_non_empty(szl, l));
+            rhs.push_back(concat_non_empty(szr, r));
+        }
+        return true;
+    }
+    
+    return false;
+}
+
 bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, expr* const* r, 
                                   expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
     is_sat = true;
@@ -733,13 +808,15 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex
         if (rpos.contains(j)) {
             rs.push_back(r[j]);
         }
-        else if (!set_empty(1, r + j, lhs, rhs)) {
+        else if (!set_empty(1, r + j, true, lhs, rhs)) {
             is_sat = false;
             return true;
         }
     }
     SASSERT(szl == rs.size());
+    if (szl > 0) {
         lhs.push_back(m_util.str.mk_concat(szl, l));
         rhs.push_back(m_util.str.mk_concat(szl, rs.c_ptr()));
+    }
     return true;
 } 

src/ast/rewriter/seq_rewriter.h

@@ -53,9 +53,14 @@ class seq_rewriter {
     br_status mk_re_plus(expr* a, expr_ref& result);
     br_status mk_re_opt(expr* a, expr_ref& result);
 
-    bool set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs);
+    bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
     bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, 
                         expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
+    bool length_constrained(unsigned n, expr* const* l, unsigned m, expr* const* r, 
+                        expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
+    bool min_length(unsigned n, expr* const* es, size_t& len);
+    expr* concat_non_empty(unsigned n, expr* const* es);
+
 public:    
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         m_util(m), m_autil(m) {

src/ast/seq_decl_plugin.cpp

@@ -289,6 +289,18 @@ func_decl* seq_decl_plugin::mk_str_fun(decl_kind k, unsigned arity, sort* const*
     return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k_seq));
 }
 
+func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string) {
+    ast_manager& m = *m_manager;
+    sort_ref rng(m);
+    if (arity == 0) {
+        m.raise_exception("Invalid function application. At least one argument expected");
+    }
+    match_left_assoc(*m_sigs[k], arity, domain, range, rng);
+    func_decl_info info(m_family_id, k_seq);
+    info.set_left_associative();
+    return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info);    
+}
+
 func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                           unsigned arity, sort * const * domain, sort * range) {
     init();
@@ -308,18 +320,21 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_STAR:
     case OP_RE_OPTION:
     case OP_RE_RANGE:
-    case OP_RE_UNION:
     case OP_RE_EMPTY_SET:
-
     case OP_RE_OF_PRED:
+    case OP_STRING_ITOS:
+    case OP_STRING_STOI:
+    case OP_REGEXP_LOOP:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+
     case OP_RE_LOOP:
         match(*m_sigs[k], arity, domain, range, rng);
         if (num_parameters != 2 || !parameters[0].is_int() || !parameters[1].is_int()) {
             m.raise_exception("Expecting two numeral parameters to function re-loop");
         }
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));   
+
     case OP_STRING_CONST:
         if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
             m.raise_exception("invalid string declaration");
@@ -327,33 +342,17 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_const_decl(m_stringc_sym, m_string,
                                func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
         
-    case OP_SEQ_CONCAT: {
+    case OP_RE_UNION:
-        if (arity == 0) {
+        return mk_assoc_fun(k, arity, domain, range, k, k);
-            m.raise_exception("invalid concatenation. At least one argument expected");
+
-        }
+    case OP_RE_CONCAT:  
-        match_left_assoc(*m_sigs[k], arity, domain, range, rng);        
+        return mk_assoc_fun(k, arity, domain, range, k, k);
-        func_decl_info info(m_family_id, k);
+
-        info.set_left_associative();
+    case OP_SEQ_CONCAT: 
-        return m.mk_func_decl(m_sigs[(rng == m_string)?_OP_STRING_CONCAT:k]->m_name, rng, rng, rng, info);
+        return mk_assoc_fun(k, arity, domain, range, k, _OP_STRING_CONCAT);
-    } 
+
-    case OP_RE_CONCAT:  {
+    case _OP_STRING_CONCAT: 
-        if (arity == 0) {
+        return mk_assoc_fun(k, arity, domain, range, OP_SEQ_CONCAT, k);
-            m.raise_exception("invalid concatenation. At least one argument expected");
-        }
-        match_left_assoc(*m_sigs[k], arity, domain, range, rng);
-        func_decl_info info(m_family_id, k);
-        info.set_left_associative();
-        return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
-    }
-    case _OP_STRING_CONCAT: {
-        if (arity == 0) {
-            m.raise_exception("invalid concatenation. At least one argument expected");
-        }
-        match_left_assoc(*m_sigs[k], arity, domain, range, rng);
-        func_decl_info info(m_family_id, OP_SEQ_CONCAT);
-        info.set_left_associative();
-        return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
-    }
 
     case OP_SEQ_REPLACE:
         return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRREPL);
@@ -361,8 +360,20 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return mk_str_fun(k, arity, domain, range, OP_SEQ_REPLACE);
 
     case OP_SEQ_INDEX:
+        if (arity == 2) {
+            sort* dom[3] = { domain[0], domain[1], arith_util(m).mk_int() };
+            sort_ref rng(m);
+            match(*m_sigs[k], 3, dom, range, rng);
+            return m.mk_func_decl(m_sigs[(dom[0] == m_string)?_OP_STRING_STRIDOF:k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+        }
         return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRIDOF);
     case _OP_STRING_STRIDOF:
+        if (arity == 2) {
+            sort* dom[3] = { domain[0], domain[1], arith_util(m).mk_int() };
+            sort_ref rng(m);
+            match(*m_sigs[k], 3, dom, range, rng);
+            return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, OP_SEQ_INDEX));
+        }
         return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX);
 
     case OP_SEQ_PREFIX:
@@ -405,14 +416,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case _OP_STRING_SUBSTR:
         return mk_str_fun(k, arity, domain, range, OP_SEQ_EXTRACT);
 
-    case OP_STRING_ITOS:
+    case _OP_SEQ_SKOLEM: {
-    case OP_STRING_STOI:
+        if (num_parameters != 1 || !parameters[0].is_symbol()) {
-    case OP_REGEXP_LOOP:
+            m.raise_exception("one symbol parameter expected to skolem symbol");
-        match(*m_sigs[k], arity, domain, range, rng);
+        }
-        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+        symbol s = parameters[0].get_symbol();
-
+        return m.mk_func_decl(s, arity, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
-    case _OP_SEQ_SKOLEM: 
+    }
-        return m.mk_func_decl(symbol("seq.skolem"), arity, domain, range, func_decl_info(m_family_id, k));
     default:
         UNREACHABLE();
         return 0;

src/ast/seq_decl_plugin.h

@@ -116,6 +116,7 @@ class seq_decl_plugin : public decl_plugin {
 
     func_decl* mk_seq_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string);
     func_decl* mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq);
+    func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq);
 
     void init();
 
@@ -158,8 +159,10 @@ public:
     bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
     bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
     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(m.get_sort(e)); }
     bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
+    bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
 
     app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
     bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
@@ -186,6 +189,7 @@ public:
         app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
         app* mk_prefix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); }
         app* mk_suffix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); }
+        app* mk_index(expr* a, expr* b, expr* i) { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); }
 
 
         bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
@@ -239,6 +243,15 @@ public:
     public:
         re(seq_util& u): m(u.m), m_fid(u.m_fid) {}
 
+        app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); }
+        app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); }
+        app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); }
+        app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); }
+        app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); }
+        app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); }
+        app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); }
+        app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }        
+
         bool is_to_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
         bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
         bool is_union(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_UNION); }

src/cmd_context/basic_cmds.cpp

@@ -222,8 +222,10 @@ ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formula
 UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", CPK_SYMBOL, symbol const &, 
           if (ctx.set_logic(arg))
               ctx.print_success();
-          else
+          else {
-              ctx.print_unsupported(symbol::null, m_line, m_pos);
+              std::string msg = "ignoring unsupported logic " + arg.str();
+              ctx.print_unsupported(symbol(msg.c_str()), m_line, m_pos);
+          }
           );
 
 UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, { 

src/cmd_context/check_logic.cpp

@@ -168,6 +168,11 @@ struct check_logic::imp {
             m_bvs         = true;
             m_quantifiers = true;
         }
+        else if (logic == "UF_S") {
+            m_uf          = true;
+            m_bvs         = true;
+            m_quantifiers = false;
+        }
         else {
             m_unknown_logic = true;
         }

src/cmd_context/cmd_context.cpp

@@ -576,7 +576,7 @@ bool cmd_context::logic_has_bv() const {
 }
 
 bool cmd_context::logic_has_seq_core(symbol const& s) const {
-    return s == "QF_BVRE";
+    return s == "QF_BVRE" || s == "QF_S";
 }
 
 bool cmd_context::logic_has_seq() const {
@@ -712,14 +712,8 @@ bool cmd_context::set_logic(symbol const & s) {
     if (has_manager() && m_main_ctx)
         throw cmd_exception("logic must be set before initialization");
     if (!supported_logic(s)) {
-        if (m_params.m_smtlib2_compliant) {
         return false;
     }
-        else {
-            warning_msg("unknown logic, ignoring set-logic command");
-            return true;
-        }
-    }
     m_logic = s;
     if (is_logic("QF_RDL") ||
         is_logic("QF_LRA") ||

src/smt/smt_theory.h

@@ -315,7 +315,7 @@ namespace smt {
         }
         
         virtual void display(std::ostream & out) const {
-            out << "Theory " << static_cast<int>(get_id()) << " does not have a display method\n";
+            out << "Theory " << static_cast<int>(get_id()) << typeid(*this).name() << " does not have a display method\n";
             display_var2enode(out);
         }
 

src/smt/theory_arith_pp.h

@@ -48,6 +48,7 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::display(std::ostream & out) const {
+        if (get_num_vars() == 0) return;
         out << "Theory arithmetic:\n";
         display_vars(out);
         display_nl_monomials(out);

src/smt/theory_array.cpp

@@ -431,8 +431,9 @@ namespace smt {
     }
 
     void theory_array::display(std::ostream & out) const {
-        out << "Theory array:\n";
         unsigned num_vars = get_num_vars();
+        if (num_vars == 0) return;
+        out << "Theory array:\n";
         for (unsigned v = 0; v < num_vars; v++) {
             display_var(out, v);
         }

src/smt/theory_bv.cpp

@@ -1586,8 +1586,9 @@ namespace smt {
     }
 
     void theory_bv::display(std::ostream & out) const {
-        out << "Theory bv:\n";
         unsigned num_vars = get_num_vars();
+        if (num_vars == 0) return;
+        out << "Theory bv:\n";
         for (unsigned v = 0; v < num_vars; v++) {
             display_var(out, v);
         }

src/smt/theory_datatype.cpp

@@ -522,8 +522,9 @@ namespace smt {
     }
 
     void theory_datatype::display(std::ostream & out) const {
-        out << "Theory datatype:\n";
         unsigned num_vars = get_num_vars();
+        if (num_vars == 0) return;
+        out << "Theory datatype:\n";
         for (unsigned v = 0; v < num_vars; v++) 
             display_var(out, v);
     }

src/smt/theory_dl.cpp

@@ -194,6 +194,9 @@ namespace smt {
             }
         }
 
+        virtual void display(std::ostream & out) const {
+        }
+
 
     private:
 

src/smt/theory_fpa.cpp

@@ -921,14 +921,20 @@ namespace smt {
         ast_manager & m = get_manager();
         context & ctx = get_context();
 
-        out << "fpa theory variables:" << std::endl;
+        bool first = true;
         ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
         ptr_vector<enode>::const_iterator end = ctx.end_enodes();
         for (; it != end; it++) {
             theory_var v = (*it)->get_th_var(get_family_id());
-            if (v != -1) out << v << " -> " <<
+            if (v != -1) {
+                if (first) out << "fpa theory variables:" << std::endl;
+                out << v << " -> " <<
                     mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
+                first = false;
             }
+        }
+        // if there are no fpa theory variables, was fp ever used?
+        if (first) return;
 
         out << "bv theory variables:" << std::endl;
         it = ctx.begin_enodes();

src/smt/theory_seq.cpp

@@ -136,12 +136,12 @@ theory_seq::theory_seq(ast_manager& m):
     m_lhs.push_back(expr_array());
     m_rhs.push_back(expr_array());
     m_deps.push_back(enode_pair_dependency_array());
-    m_prefix_sym = "prefix";
+    m_prefix_sym = "seq.prefix.suffix";
-    m_suffix_sym = "suffix";
+    m_suffix_sym = "seq.suffix.prefix";
-    m_left_sym = "left";
+    m_left_sym = "seq.left";
-    m_right_sym = "right";
+    m_right_sym = "seq.right";
-    m_contains_left_sym = "contains_left";
+    m_contains_left_sym = "seq.contains.left";
-    m_contains_right_sym = "contains_right";
+    m_contains_right_sym = "seq.contains.right";
 }
 
 theory_seq::~theory_seq() {
@@ -261,17 +261,19 @@ bool theory_seq::find_branch_candidate(expr* l, ptr_vector<expr> const& rs) {
 }
 
 bool theory_seq::assume_equality(expr* l, expr* r) {
-    TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";);
     context& ctx = get_context();
     if (m_exclude.contains(l, r)) {
         return false;
     }
     else {
-        SASSERT(ctx.e_internalized(l));
+        TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";);
+        if (!ctx.e_internalized(l)) ctx.internalize(l, false);
         if (!ctx.e_internalized(r)) ctx.internalize(r, false);
+        ctx.mark_as_relevant(ctx.get_enode(l));
+        ctx.mark_as_relevant(ctx.get_enode(r));
         ctx.assume_eq(ctx.get_enode(l), ctx.get_enode(r));            
-    }
         return true;
+    }
 }
 
 bool theory_seq::split_variable() {
@@ -519,26 +521,37 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
 }
 
 void theory_seq::display(std::ostream & out) const {
+    if (m.size(m_lhs.back()) == 0 &&
+        m_ineqs.empty() &&
+        m_rep.empty() && 
+        m_exclude.empty()) {
+        return;
+    }
+    out << "Theory seq\n";
+    if (m.size(m_lhs.back()) > 0) {
+        out << "Equations:\n";
         display_equations(out);
+    }
     if (!m_ineqs.empty()) {
         out << "Negative constraints:\n";
         for (unsigned i = 0; i < m_ineqs.size(); ++i) {
             out << mk_pp(m_ineqs[i], m) << "\n";
         }
     }
+    if (!m_rep.empty()) {
         out << "Solved equations:\n";
         m_rep.display(out);
+    }
+    if (!m_exclude.empty()) {
+        out << "Exclusions:\n";
         m_exclude.display(out);
+    }
 }
 
 void theory_seq::display_equations(std::ostream& out) const {
     expr_array const& lhs = m_lhs.back();
     expr_array const& rhs = m_rhs.back();
     enode_pair_dependency_array const& deps = m_deps.back();
-    if (m.size(lhs) == 0) {
-        return;
-    }
-    out << "Equations:\n";
     for (unsigned i = 0; i < m.size(lhs); ++i) {
         out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n";
         display_deps(out, m_dam.get(deps, i));
@@ -585,6 +598,10 @@ void theory_seq::set_incomplete(app* term) {
 }
 
 theory_var theory_seq::mk_var(enode* n) {
+    if (!m_util.is_seq(n->get_owner()) ||
+        !m_util.is_re(n->get_owner())) {
+        return null_theory_var;
+    }
     if (is_attached_to_var(n)) {
         return n->get_th_var(get_id());
     }
@@ -658,6 +675,7 @@ void theory_seq::propagate() {
 }
 
 void theory_seq::enque_axiom(expr* e) {
+    TRACE("seq", tout << "add axioms for: " << mk_pp(e, m) << "\n";);
     m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
     m_axioms.push_back(e);
 }
@@ -732,8 +750,8 @@ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) {
   lit or s = "" or !prefix(s, x*s1)
 */
 void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) {
-    expr_ref s1 = mk_skolem(symbol("first"), s);
+    expr_ref s1 = mk_skolem(symbol("seq.first"), s);
-    expr_ref c  = mk_skolem(symbol("last"),  s);
+    expr_ref c  = mk_skolem(symbol("seq.last"),  s);
     expr_ref s1c(m_util.str.mk_concat(s1, c), m);
     expr_ref lc(m_util.str.mk_length(c), m);
     expr_ref one(m_autil.mk_int(1), m);
@@ -745,13 +763,13 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) {
 }
 
 /*
-  let i = Index(s, t, offset)
+  let i = Index(t, s, offset)
 
   if offset = 0:
-    (!contains(s, t) -> i = -1)
+    (!contains(t, s) -> i = -1)
     (s = empty -> i = 0)
-    (contains(s, t) & s != empty -> t = xsy)
+    (contains(t, s) & s != empty -> t = xsy)
-    (contains(s, t) -> tightest_prefix(s, x))
+    (contains(t, s) -> tightest_prefix(s, x))
   if 0 <= offset < len(t):
      t = zt' & len(z) == offset
      add above constraints with t'
@@ -767,16 +785,16 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) {
 void theory_seq::add_indexof_axiom(expr* i) {
     expr* s, *t, *offset;
     rational r;
-    VERIFY(m_util.str.is_index(i, s, t, offset));
+    VERIFY(m_util.str.is_index(i, t, s, offset));
     expr_ref emp(m), minus_one(m), zero(m), xsy(m);
     minus_one   = m_autil.mk_int(-1);
     zero        = m_autil.mk_int(0);
     emp         = m_util.str.mk_empty(m.get_sort(s));
     if (m_autil.is_numeral(offset, r) && r.is_zero()) {
-        expr_ref x  = mk_skolem(m_contains_left_sym, s, t);
+        expr_ref x  = mk_skolem(m_contains_left_sym, t, s);
-        expr_ref y  = mk_skolem(m_contains_right_sym, s, t);    
+        expr_ref y  = mk_skolem(m_contains_right_sym, t, s);    
         xsy         = m_util.str.mk_concat(x,s,y);
-        literal cnt = mk_literal(m_util.str.mk_contains(s, t));
+        literal cnt = mk_literal(m_util.str.mk_contains(t, s));
         literal eq_empty = mk_eq(s, emp, false);
         add_axiom(cnt,  mk_eq(i, minus_one, false));
         add_axiom(~eq_empty, mk_eq(i, zero, false));
@@ -791,19 +809,19 @@ void theory_seq::add_indexof_axiom(expr* i) {
 /*
   let r = replace(a, s, t)
   
-  (contains(s, a) -> tightest_prefix(s,xs))
+  (contains(a, s) -> tightest_prefix(s,xs))
-  (contains(s, a) -> r = xty & a = xsy) & 
+  (contains(a, s) -> r = xty & a = xsy) & 
-  (!contains(s, a) -> r = a)
+  (!contains(a, s) -> r = a)
    
 */
 void theory_seq::add_replace_axiom(expr* r) {
     expr* a, *s, *t;
     VERIFY(m_util.str.is_replace(r, a, s, t));
-    expr_ref x  = mk_skolem(m_contains_left_sym, s, a);
+    expr_ref x  = mk_skolem(m_contains_left_sym, a, s);
-    expr_ref y  = mk_skolem(m_contains_right_sym, s, a);    
+    expr_ref y  = mk_skolem(m_contains_right_sym, a, s);    
     expr_ref xty(m_util.str.mk_concat(x, t, y), m);
     expr_ref xsy(m_util.str.mk_concat(x, s, y), m);
-    literal cnt = mk_literal(m_util.str.mk_contains(s, a));
+    literal cnt = mk_literal(m_util.str.mk_contains(a ,s));
     add_axiom(cnt,  mk_eq(r, a, false));
     add_axiom(~cnt, mk_eq(a, xsy, false));
     add_axiom(~cnt, mk_eq(r, xty, false));
@@ -871,7 +889,7 @@ expr* theory_seq::mk_sub(expr* a, expr* b) {
 void theory_seq::add_extract_axiom(expr* e) {
     expr* s, *i, *l;
     VERIFY(m_util.str.is_extract(e, s, i, l));
-    expr_ref x(mk_skolem(symbol("extract_prefix"), s, e), m);
+    expr_ref x(mk_skolem(symbol("seq.extract.prefix"), s, e), m);
     expr_ref ls(m_util.str.mk_length(s), m);
     expr_ref lx(m_util.str.mk_length(x), m);
     expr_ref le(m_util.str.mk_length(e), m);
@@ -901,8 +919,8 @@ void theory_seq::add_at_axiom(expr* e) {
     expr* s, *i;
     VERIFY(m_util.str.is_at(e, s, i));
     expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m);
-    x     = mk_skolem(symbol("at_left"), s);
+    x     = mk_skolem(symbol("seq.at.left"), s);
-    y     = mk_skolem(symbol("at_right"), s);
+    y     = mk_skolem(symbol("seq.at.right"), s);
     xey   = m_util.str.mk_concat(x, e, y);
     zero  = m_autil.mk_int(0);
     one   = m_autil.mk_int(1);
@@ -928,10 +946,10 @@ literal theory_seq::mk_literal(expr* _e) {
 void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) {
     context& ctx = get_context();
     literal_vector lits;
-    if (l1 != null_literal) lits.push_back(l1);
+    if (l1 != null_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); }
-    if (l2 != null_literal) lits.push_back(l2);
+    if (l2 != null_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); }
-    if (l3 != null_literal) lits.push_back(l3);
+    if (l3 != null_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
-    if (l4 != null_literal) lits.push_back(l4);
+    if (l4 != null_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
     TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
 }
@@ -981,11 +999,11 @@ void theory_seq::assign_eq(bool_var v, bool is_true) {
         else if (m_util.str.is_contains(e, e1, e2)) {
             expr_ref f1 = mk_skolem(m_contains_left_sym, e1, e2);
             expr_ref f2 = mk_skolem(m_contains_right_sym, e1, e2);
-            f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e1), f2);
+            f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e2), f2);
-            propagate_eq(v, f, e2);
+            propagate_eq(v, f, e1);
         }
         else if (m_util.str.is_in_re(e, e1, e2)) {
-            NOT_IMPLEMENTED_YET();
+            // TBD
         }
         else {
             UNREACHABLE();
@@ -1001,8 +1019,10 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
     enode* n1 = get_enode(v1);
     enode* n2 = get_enode(v2);
     if (n1 != n2) {
-        m.push_back(m_lhs.back(), n1->get_owner());
+        expr* o1 = n1->get_owner(), *o2 = n2->get_owner();
-        m.push_back(m_rhs.back(), n2->get_owner());
+        TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
+        m.push_back(m_lhs.back(), o1);
+        m.push_back(m_rhs.back(), o2);
         m_dam.push_back(m_deps.back(), m_dm.mk_leaf(enode_pair(n1, n2)));
 
         new_eq_len_concat(n1, n2);

src/smt/theory_seq.h

@@ -62,6 +62,7 @@ namespace smt {
             void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d);
         public:
             solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
+            bool empty() const { return m_map.empty(); }
             void  update(expr* e, expr* r, enode_pair_dependency* d);
             expr* find(expr* e, enode_pair_dependency*& d);
             void push_scope() { m_limit.push_back(m_updates.size()); }
@@ -78,6 +79,7 @@ namespace smt {
         public:
             exclusion_table(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {}
             ~exclusion_table() { }
+            bool empty() const { return m_table.empty(); }
             void update(expr* e, expr* r);
             bool contains(expr* e, expr* r) {
                 return m_table.contains(std::make_pair(e, r));

src/smt/theory_seq_empty.h

@@ -89,6 +89,11 @@ namespace smt {
                     return u.str.mk_string(sym);
                 }
             }
+            sort* seq = 0;
+            if (u.is_re(s, seq)) {
+                expr* v0 = get_fresh_value(seq);
+                return u.re.mk_to_re(v0);
+            }
             NOT_IMPLEMENTED_YET();
             return 0;
         }