Merge pull request #396 from NikolajBjorner/master

Basic Sequence/String and regular expression support, congruence propagation for bit-vectors, tuned bit-vector multiplier encodings for small numerals.

scripts/mk_project.py

@@ -16,11 +16,12 @@ def init_project_def():
     add_lib('nlsat', ['polynomial', 'sat'])
     add_lib('hilbert', ['util'], 'math/hilbert')
     add_lib('simplex', ['util'], 'math/simplex')
+    add_lib('automata', ['util'], 'math/automata')
     add_lib('interval', ['util'], 'math/interval')
     add_lib('realclosure', ['interval'], 'math/realclosure')
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
-    add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter')
+    add_lib('rewriter', ['ast', 'polynomial', 'automata'], 'ast/rewriter')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
     add_lib('model', ['rewriter'])
     add_lib('tactic', ['ast', 'model'])

scripts/update_api.py

@@ -1079,7 +1079,7 @@ def def_API(name, result, params):
 def mk_bindings():
     exe_c.write("void register_z3_replayer_cmds(z3_replayer & in) {\n")
     for key, val in API2Id.items():
-        exe_c.write("  in.register_cmd(%s, exec_%s);\n" % (key, val))
+        exe_c.write("  in.register_cmd(%s, exec_%s, \"%s\");\n" % (key, val, val))
     exe_c.write("}\n")
 
 def ml_method_name(name):

src/api/api_ast.cpp

@@ -641,6 +641,12 @@ extern "C" {
         else if (fid == mk_c(c)->get_fpa_fid() && k == ROUNDING_MODE_SORT) {
             return Z3_ROUNDING_MODE_SORT;
         }
+        else if (fid == mk_c(c)->get_seq_fid() && k == SEQ_SORT) {
+            return Z3_SEQ_SORT;
+        }
+        else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) {
+            return Z3_RE_SORT;
+        }
         else {
             return Z3_UNKNOWN_SORT;
         }
@@ -776,6 +782,8 @@ extern "C" {
                 SET_ERROR_CODE(Z3_SORT_ERROR);
                 RETURN_Z3(of_expr(0));
             }
+            SASSERT(from[i]->get_ref_count() > 0);
+            SASSERT(to[i]->get_ref_count() > 0);
         }
         expr_safe_replace subst(m);
         for (unsigned i = 0; i < num_exprs; i++) {
@@ -1106,6 +1114,32 @@ extern "C" {
             }
         }
 
+        if (mk_c(c)->get_seq_fid() == _d->get_family_id()) {
+            switch (_d->get_decl_kind()) {
+            case Z3_OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
+            case Z3_OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
+            case Z3_OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
+            case Z3_OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
+            case Z3_OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
+            case Z3_OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
+            case Z3_OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
+            case Z3_OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
+            case Z3_OP_SEQ_AT: return Z3_OP_SEQ_AT;
+            case Z3_OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
+            case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
+            case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
+            case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
+                    
+            case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS;
+            case Z3_OP_RE_STAR: return Z3_OP_RE_STAR;
+            case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION;
+            case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
+            case Z3_OP_RE_UNION: return Z3_OP_RE_UNION;
+            default:
+                return Z3_OP_UNINTERPRETED;
+            }
+        }
+
         if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
             switch (_d->get_decl_kind()) {
             case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;

src/api/api_context.cpp

@@ -73,6 +73,7 @@ namespace api {
         m_datalog_util(m()),
         m_fpa_util(m()),
         m_dtutil(m()),
+        m_sutil(m()),
         m_last_result(m()),
         m_ast_trail(m()),
         m_replay_stack(),
@@ -97,6 +98,7 @@ namespace api {
         m_dt_fid    = m().mk_family_id("datatype");
         m_datalog_fid = m().mk_family_id("datalog_relation");
         m_fpa_fid   = m().mk_family_id("fpa");
+        m_seq_fid   = m().mk_family_id("seq");
         m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
 
         if (!m_user_ref_count) {

src/api/api_context.h

@@ -25,6 +25,7 @@ Revision History:
 #include"api_util.h"
 #include"arith_decl_plugin.h"
 #include"bv_decl_plugin.h"
+#include"seq_decl_plugin.h"
 #include"datatype_decl_plugin.h"
 #include"dl_decl_plugin.h"
 #include"fpa_decl_plugin.h"
@@ -58,6 +59,7 @@ namespace api {
         datalog::dl_decl_util      m_datalog_util;
         fpa_util                   m_fpa_util;
 	datatype_util              m_dtutil;
+        seq_util                   m_sutil;
 
         // Support for old solver API
         smt_params                 m_fparams;
@@ -78,6 +80,7 @@ namespace api {
         family_id                  m_datalog_fid;
         family_id                  m_pb_fid;
         family_id                  m_fpa_fid;
+        family_id                  m_seq_fid;
         datatype_decl_plugin *     m_dt_plugin;
         
         std::string                m_string_buffer; // temporary buffer used to cache strings sent to the "external" world.
@@ -121,6 +124,7 @@ namespace api {
         datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
         fpa_util & fpautil() { return m_fpa_util; }
 	datatype_util& dtutil() { return m_dtutil; }
+        seq_util& sutil() { return m_sutil; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return m_arith_fid; }
@@ -129,6 +133,7 @@ namespace api {
         family_id get_datalog_fid() const { return m_datalog_fid; }
         family_id get_pb_fid() const { return m_pb_fid; }
         family_id get_fpa_fid() const { return m_fpa_fid; }
+        family_id get_seq_fid() const { return m_seq_fid; }
         datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
 
         Z3_error_code get_error_code() const { return m_error_code; }

src/api/api_seq.cpp

@@ -0,0 +1,151 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    api_seq.cpp
+
+Abstract:
+
+    API for sequences and regular expressions.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-01-02.
+
+Revision History:
+
+--*/
+#include<iostream>
+#include"z3.h"
+#include"api_log_macros.h"
+#include"api_context.h"
+#include"api_util.h"
+#include"ast_pp.h"
+
+extern "C" {
+
+    Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort domain) {
+        Z3_TRY;
+        LOG_Z3_mk_seq_sort(c, domain);
+        RESET_ERROR_CODE();  
+        sort * ty =  mk_c(c)->sutil().str.mk_seq(to_sort(domain));
+        mk_c(c)->save_ast_trail(ty);
+        RETURN_Z3(of_sort(ty));
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort domain) {
+        Z3_TRY;
+        LOG_Z3_mk_re_sort(c, domain);
+        RESET_ERROR_CODE();  
+        sort * ty =  mk_c(c)->sutil().re.mk_re(to_sort(domain));
+        mk_c(c)->save_ast_trail(ty);
+        RETURN_Z3(of_sort(ty));
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string str) {
+        Z3_TRY;
+        LOG_Z3_mk_string(c, str);
+        RESET_ERROR_CODE();  
+        zstring s(str, zstring::ascii);
+        app* a = mk_c(c)->sutil().str.mk_string(s);
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+    
+    Z3_sort Z3_API Z3_mk_string_sort(Z3_context c) {
+        Z3_TRY;
+        LOG_Z3_mk_string_sort(c);
+        RESET_ERROR_CODE();
+        sort* ty = mk_c(c)->sutil().str.mk_string_sort();
+        mk_c(c)->save_ast_trail(ty);
+        RETURN_Z3(of_sort(ty));
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_is_seq_sort(c, s);
+        RESET_ERROR_CODE();
+        bool result = mk_c(c)->sutil().is_seq(to_sort(s));
+        return result?Z3_TRUE:Z3_FALSE;        
+        Z3_CATCH_RETURN(Z3_FALSE);        
+    }
+
+    Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_is_re_sort(c, s);
+        RESET_ERROR_CODE();
+        bool result = mk_c(c)->sutil().is_re(to_sort(s));
+        return result?Z3_TRUE:Z3_FALSE;        
+        Z3_CATCH_RETURN(Z3_FALSE);        
+    }
+
+    Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_is_string_sort(c, s);
+        RESET_ERROR_CODE();
+        bool result = mk_c(c)->sutil().is_string(to_sort(s));
+        return result?Z3_TRUE:Z3_FALSE;        
+        Z3_CATCH_RETURN(Z3_FALSE);        
+    }
+
+    Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s) {
+        Z3_TRY;
+        LOG_Z3_is_string(c, s);
+        RESET_ERROR_CODE();
+        bool result = mk_c(c)->sutil().str.is_string(to_expr(s));
+        return result?Z3_TRUE:Z3_FALSE;        
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s) {
+        Z3_TRY;
+        LOG_Z3_get_string(c, s);
+        RESET_ERROR_CODE();
+        zstring str;
+        if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return "";
+        }
+        std::string result = str.encode();
+        return mk_c(c)->mk_external_string(result);
+        Z3_CATCH_RETURN("");
+    }
+
+    Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq) {
+        Z3_TRY;
+        LOG_Z3_mk_seq_empty(c, seq);
+        RESET_ERROR_CODE();  
+        app* a = mk_c(c)->sutil().str.mk_empty(to_sort(seq));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
+    MK_UNARY(Z3_mk_seq_unit, mk_c(c)->get_seq_fid(), OP_SEQ_UNIT, SKIP);
+    MK_NARY(Z3_mk_seq_concat, mk_c(c)->get_seq_fid(), OP_SEQ_CONCAT, SKIP);
+    MK_BINARY(Z3_mk_seq_prefix, mk_c(c)->get_seq_fid(), OP_SEQ_PREFIX, SKIP);
+    MK_BINARY(Z3_mk_seq_suffix, mk_c(c)->get_seq_fid(), OP_SEQ_SUFFIX, SKIP);
+    MK_BINARY(Z3_mk_seq_contains, mk_c(c)->get_seq_fid(), OP_SEQ_CONTAINS, SKIP);
+    MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP);
+    MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP);
+    MK_BINARY(Z3_mk_seq_at, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP);
+    MK_UNARY(Z3_mk_seq_length, mk_c(c)->get_seq_fid(), OP_SEQ_LENGTH, SKIP);
+    MK_TERNARY(Z3_mk_seq_index, mk_c(c)->get_seq_fid(), OP_SEQ_INDEX, SKIP);
+    MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP);
+    MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP);
+
+
+    MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP);
+    MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP);
+    MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP);
+    MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP);
+    MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP);
+
+
+
+};

src/api/api_util.h

@@ -135,6 +135,23 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) {        \
     MK_BINARY_BODY(NAME, FID, OP, EXTRA_CODE);                  \
 }
 
+#define MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE)               \
+    Z3_TRY;                                                     \
+    RESET_ERROR_CODE();                                         \
+    EXTRA_CODE;                                                 \
+    expr * args[3] = { to_expr(n1), to_expr(n2), to_expr(n3) }; \
+    ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 3, args);       \
+    mk_c(c)->save_ast_trail(a);                                 \
+    check_sorts(c, a);                                          \
+    RETURN_Z3(of_ast(a));                                       \
+    Z3_CATCH_RETURN(0);
+ 
+#define MK_TERNARY(NAME, FID, OP, EXTRA_CODE)                            \
+    Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_ast n3) { \
+    LOG_ ## NAME(c, n1, n2, n3);                                        \
+    MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE);                          \
+}
+
 #define MK_NARY(NAME, FID, OP, EXTRA_CODE)                              \
 Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \
     Z3_TRY;                                                             \

src/api/c++/z3++.h

@@ -205,6 +205,18 @@ namespace z3 {
            \brief Return the Bit-vector sort of size \c sz. That is, the sort for bit-vectors of size \c sz.
         */
         sort bv_sort(unsigned sz);
+        /**
+           \brief Return the sort for ASCII strings.
+         */
+        sort string_sort();
+        /**
+           \brief Return a sequence sort over base sort \c s.
+         */
+        sort seq_sort(sort& s);
+        /**
+           \brief Return a regular expression sort over sequences \c seq_sort.
+         */
+        sort re_sort(sort& seq_sort);
         /**
            \brief Return an array sort for arrays from \c d to \c r.
 
@@ -261,6 +273,9 @@ namespace z3 {
         expr bv_val(__uint64 n, unsigned sz);
         expr bv_val(char const * n, unsigned sz);
 
+        expr string_val(char const* s);
+        expr string_val(std::string const& s);
+
         expr num_val(int n, sort const & s);
 
         /**
@@ -425,6 +440,14 @@ namespace z3 {
             \brief Return true if this sort is a Relation sort.
         */
         bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
+        /**
+            \brief Return true if this sort is a Sequence sort.
+        */
+        bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
+        /**
+            \brief Return true if this sort is a regular expression sort.
+        */
+        bool is_re() const { return sort_kind() == Z3_RE_SORT; }
         /**
             \brief Return true if this sort is a Finite domain sort.
         */
@@ -532,6 +555,15 @@ namespace z3 {
            \brief Return true if this is a Relation expression.
         */
         bool is_relation() const { return get_sort().is_relation(); }
+        /**
+           \brief Return true if this is a sequence expression.
+        */
+        bool is_seq() const { return get_sort().is_seq(); }
+        /**
+           \brief Return true if this is a regular expression.
+        */
+        bool is_re() const { return get_sort().is_re(); }
+        
         /**
            \brief Return true if this is a Finite-domain expression.
 
@@ -663,6 +695,7 @@ namespace z3 {
 
         friend expr distinct(expr_vector const& args);
         friend expr concat(expr const& a, expr const& b);
+        friend expr concat(expr_vector const& args);
 
         friend expr operator==(expr const & a, expr const & b);
         friend expr operator==(expr const & a, int b);
@@ -728,10 +761,50 @@ namespace z3 {
         friend expr operator|(int a, expr const & b);
 
         friend expr operator~(expr const & a);
-        expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
+        expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }        
         unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
         unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
 
+        /**
+           \brief sequence and regular expression operations.
+           + is overloaeded as sequence concatenation and regular expression union.
+           concat is overloaded to handle sequences and regular expressions
+        */
+        expr extract(expr const& offset, expr const& length) const { 
+            check_context(*this, offset); check_context(offset, length);
+            Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r); 
+        }
+        expr replace(expr const& src, expr const& dst) const {
+            check_context(*this, src); check_context(src, dst);
+            Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr unit() const {
+            Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr contains(expr const& s) {
+            check_context(*this, s);
+            Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr at(expr const& index) const {
+            check_context(*this, index);
+            Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr length() const {
+            Z3_ast r = Z3_mk_seq_length(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+
+
+
         /**
            \brief Return a simplified version of this expression.
         */
@@ -835,6 +908,13 @@ namespace z3 {
         else if (a.is_bv() && b.is_bv()) {
             r = Z3_mk_bvadd(a.ctx(), a, b);
         }
+        else if (a.is_seq() && b.is_seq()) {
+            return concat(a, b);
+        }
+        else if (a.is_re() && b.is_re()) {
+            Z3_ast _args[2] = { a, b };
+            r = Z3_mk_re_union(a.ctx(), 2, _args);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1219,11 +1299,48 @@ namespace z3 {
 
     inline expr concat(expr const& a, expr const& b) {
         check_context(a, b);
-        Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
+        Z3_ast r;
+        if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
+            Z3_ast _args[2] = { a, b };
+            r = Z3_mk_seq_concat(a.ctx(), 2, _args);
+        }
+        else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
+            Z3_ast _args[2] = { a, b };
+            r = Z3_mk_re_concat(a.ctx(), 2, _args);
+        }
+        else {
+            r = Z3_mk_concat(a.ctx(), a, b);
+        }
         a.ctx().check_error();
         return expr(a.ctx(), r);
     }
 
+    inline expr concat(expr_vector const& args) {
+        Z3_ast r;
+        assert(args.size() > 0);
+        if (args.size() == 1) {
+            return args[0];
+        }
+        context& ctx = args[0].ctx();
+        array<Z3_ast> _args(args);
+        if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
+            r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
+        }
+        else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
+            r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
+        }
+        else {
+            r = _args[args.size()-1];
+            for (unsigned i = args.size()-1; i > 0; ) {
+                --i;
+                r = Z3_mk_concat(ctx, _args[i], r);
+                ctx.check_error();
+            }
+        }
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
     class func_entry : public object {
         Z3_func_entry m_entry;
         void init(Z3_func_entry e) {
@@ -1762,6 +1879,10 @@ namespace z3 {
     inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
     inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
     inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
+    inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
+    inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
+    inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
+
     inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
     inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
         array<Z3_symbol> _enum_names(n);
@@ -1885,6 +2006,9 @@ namespace z3 {
     inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
     inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
 
+    inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
+    inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
+
     inline expr context::num_val(int n, sort const & s) { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
 
     inline expr func_decl::operator()(unsigned n, expr const * args) const {
@@ -2017,6 +2141,62 @@ namespace z3 {
         d.check_error();
         return expr(d.ctx(), r);
     }
+
+    // sequence and regular expression operations.
+    // union is +
+    // concat is overloaded to handle sequences and regular expressions
+
+    inline expr empty(sort const& s) {
+        Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+    inline expr suffixof(expr const& a, expr const& b) {
+        check_context(a, b);
+        Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+    inline expr prefixof(expr const& a, expr const& b) {
+        check_context(a, b);
+        Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+    inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
+        check_context(s, substr); check_context(s, offset);
+        Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+    inline expr to_re(expr const& s) {
+        Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+    inline expr in_re(expr const& s, expr const& re) {
+        check_context(s, re);
+        Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+    inline expr plus(expr const& re) {
+        Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
+        re.check_error();
+        return expr(re.ctx(), r);
+    }
+    inline expr option(expr const& re) {
+        Z3_ast r = Z3_mk_re_option(re.ctx(), re);
+        re.check_error();
+        return expr(re.ctx(), r);
+    }
+    inline expr star(expr const& re) {
+        Z3_ast r = Z3_mk_re_star(re.ctx(), re);
+        re.check_error();
+        return expr(re.ctx(), r);
+    }
+
+
     inline expr interpolant(expr const& a) {
         return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
     }

src/api/dotnet/Context.cs

@@ -125,6 +125,7 @@ namespace Microsoft.Z3
         private BoolSort m_boolSort = null;
         private IntSort m_intSort = null;
         private RealSort m_realSort = null;
+	private SeqSort m_stringSort = null;
 
         /// <summary>
         /// Retrieves the Boolean sort of the context.
@@ -163,6 +164,20 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Retrieves the String sort of the context.
+        /// </summary>
+        public SeqSort StringSort
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<SeqSort>() != null);
+                if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
+                return m_stringSort;
+            }
+        }
+
+
         /// <summary>
         /// Create a new Boolean sort.
         /// </summary>
@@ -223,6 +238,27 @@ namespace Microsoft.Z3
             return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
         }
 
+
+        /// <summary>
+        /// Create a new sequence sort.
+        /// </summary>
+        public SeqSort MkSeqSort(Sort s)
+        {
+            Contract.Requires(s != null);
+            Contract.Ensures(Contract.Result<SeqSort>() != null);
+            return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a new regular expression sort.
+        /// </summary>
+        public ReSort MkReSort(SeqSort s)
+        {
+            Contract.Requires(s != null);
+            Contract.Ensures(Contract.Result<ReSort>() != null);
+            return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
+        }
+
         /// <summary>
         /// Create a new array sort.
         /// </summary>
@@ -2286,6 +2322,230 @@ namespace Microsoft.Z3
 
         #endregion
 
+        #region Sequence, string and regular expresions
+
+        /// <summary>
+        /// Create the empty sequence.
+        /// </summary>
+        public SeqExpr MkEmptySeq(Sort s) 
+        {
+            Contract.Requires(s != null);
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+            return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create the singleton sequence.
+        /// </summary>
+        public SeqExpr MkUnit(Expr elem) 
+        {
+            Contract.Requires(elem != null);
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+            return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a string constant.
+        /// </summary>
+        public SeqExpr MkString(string s) 
+        {
+            Contract.Requires(s != null);
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+            return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
+        }
+
+        /// <summary>
+        /// Concatentate sequences.
+        /// </summary>
+        public SeqExpr MkConcat(params SeqExpr[] t)
+        {
+            Contract.Requires(t != null);
+            Contract.Requires(Contract.ForAll(t, a => a != null));
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+
+            CheckContextMatch(t);
+            return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+        }
+
+
+        /// <summary>
+        /// Retrieve the length of a given sequence.
+        /// </summary>
+        public IntExpr MkLength(SeqExpr s)
+        {
+            Contract.Requires(s != null);
+            Contract.Ensures(Contract.Result<IntExpr>() != null);
+            return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Check for sequence prefix.
+        /// </summary>
+        public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2) 
+        {
+            Contract.Requires(s1 != null);
+            Contract.Requires(s2 != null);
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            CheckContextMatch(s1, s2);
+            return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
+        }
+
+        /// <summary>
+        /// Check for sequence suffix.
+        /// </summary>
+        public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2) 
+        {
+            Contract.Requires(s1 != null);
+            Contract.Requires(s2 != null);
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            CheckContextMatch(s1, s2);
+            return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
+        }
+
+        /// <summary>
+        /// Check for sequence containment of s2 in s1.
+        /// </summary>
+        public BoolExpr MkContains(SeqExpr s1, SeqExpr s2) 
+        {
+            Contract.Requires(s1 != null);
+            Contract.Requires(s2 != null);
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            CheckContextMatch(s1, s2);
+            return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
+        }
+
+        /// <summary>
+        /// Retrieve sequence of length one at index.
+        /// </summary>
+        public SeqExpr MkAt(SeqExpr s, IntExpr index)
+        {
+            Contract.Requires(s != null);
+            Contract.Requires(index != null);
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+            CheckContextMatch(s, index);
+            return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
+        }
+
+        /// <summary>
+        /// Extract subsequence.
+        /// </summary>
+        public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
+        {
+            Contract.Requires(s != null);
+            Contract.Requires(offset != null);
+            Contract.Requires(length != null);
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+            CheckContextMatch(s, offset, length);
+            return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
+        }
+
+        /// <summary>
+        /// Extract index of sub-string starting at offset.
+        /// </summary>
+        public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
+        {
+            Contract.Requires(s != null);
+            Contract.Requires(offset != null);
+            Contract.Requires(substr != null);
+            Contract.Ensures(Contract.Result<IntExpr>() != null);
+            CheckContextMatch(s, substr, offset);
+            return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
+        }
+
+        /// <summary>
+        /// Replace the first occurrence of src by dst in s.
+        /// </summary>
+        public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
+        {
+            Contract.Requires(s != null);
+            Contract.Requires(src != null);
+            Contract.Requires(dst != null);
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+            CheckContextMatch(s, src, dst);
+            return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
+        }
+
+        /// <summary>
+        /// Convert a regular expression that accepts sequence s.
+        /// </summary>
+        public ReExpr MkToRe(SeqExpr s) 
+        {
+            Contract.Requires(s != null);
+            Contract.Ensures(Contract.Result<ReExpr>() != null);
+            return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));            
+        }
+
+
+        /// <summary>
+        /// Check for regular expression membership.
+        /// </summary>
+        public BoolExpr MkInRe(SeqExpr s, ReExpr re)
+        {
+            Contract.Requires(s != null);
+            Contract.Requires(re != null);
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            CheckContextMatch(s, re);
+            return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));            
+        }
+
+        /// <summary>
+        /// Take the Kleene star of a regular expression.
+        /// </summary>
+        public ReExpr MkStar(ReExpr re)
+        {
+            Contract.Requires(re != null);
+            Contract.Ensures(Contract.Result<ReExpr>() != null);
+            return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));            
+        }
+
+        /// <summary>
+        /// Take the Kleene plus of a regular expression.
+        /// </summary>
+        public ReExpr MPlus(ReExpr re)
+        {
+            Contract.Requires(re != null);
+            Contract.Ensures(Contract.Result<ReExpr>() != null);
+            return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));            
+        }
+
+        /// <summary>
+        /// Create the optional regular expression.
+        /// </summary>
+        public ReExpr MOption(ReExpr re)
+        {
+            Contract.Requires(re != null);
+            Contract.Ensures(Contract.Result<ReExpr>() != null);
+            return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));            
+        }
+
+        /// <summary>
+        /// Create the concatenation of regular languages.
+        /// </summary>
+        public ReExpr MkConcat(params ReExpr[] t)
+        {
+            Contract.Requires(t != null);
+            Contract.Requires(Contract.ForAll(t, a => a != null));
+            Contract.Ensures(Contract.Result<ReExpr>() != null);
+
+            CheckContextMatch(t);
+            return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+        }
+
+        /// <summary>
+        /// Create the union of regular languages.
+        /// </summary>
+        public ReExpr MkUnion(params ReExpr[] t)
+        {
+            Contract.Requires(t != null);
+            Contract.Requires(Contract.ForAll(t, a => a != null));
+            Contract.Ensures(Contract.Result<ReExpr>() != null);
+
+            CheckContextMatch(t);
+            return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+        }
+    
+        #endregion
+
         #region Pseudo-Boolean constraints
 
         /// <summary>
@@ -4448,6 +4708,26 @@ namespace Microsoft.Z3
                 throw new Z3Exception("Context mismatch");
         }
 
+        [Pure]
+        internal void CheckContextMatch(Z3Object other1, Z3Object other2)
+        {
+            Contract.Requires(other1 != null);
+            Contract.Requires(other2 != null);
+            CheckContextMatch(other1);
+            CheckContextMatch(other2);
+        }
+
+        [Pure]
+        internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
+        {
+            Contract.Requires(other1 != null);
+            Contract.Requires(other2 != null);
+            Contract.Requires(other3 != null);
+            CheckContextMatch(other1);
+            CheckContextMatch(other2);
+            CheckContextMatch(other3);
+        }
+
         [Pure]
         internal void CheckContextMatch(Z3Object[] arr)
         {
@@ -4628,6 +4908,7 @@ namespace Microsoft.Z3
             m_boolSort = null;
             m_intSort = null;
             m_realSort = null;
+            m_stringSort = null;
         }
         #endregion
     }

src/api/dotnet/Expr.cs

@@ -1826,6 +1826,8 @@ namespace Microsoft.Z3
                 case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj);
                 case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
                 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj);
+                case Z3_sort_kind.Z3_RE_SORT: return new ReExpr(ctx, obj);
+                case Z3_sort_kind.Z3_SEQ_SORT: return new SeqExpr(ctx, obj);
             }
 
             return new Expr(ctx, obj);

src/api/dotnet/ReExpr.cs

@@ -0,0 +1,42 @@
+/*++
+Copyright (<c>) 2016 Microsoft Corporation
+
+Module Name:
+
+    ReExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Regular Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Regular expression expressions
+    /// </summary>
+    public class ReExpr : Expr
+    {
+        #region Internal
+        /// <summary> Constructor for ReExpr </summary>
+        internal ReExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/ReSort.cs

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    ReSort.cs
+
+Abstract:
+
+    Z3 Managed API: Regular expression Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    ///  A regular expression sort
+    /// </summary>
+    public class ReSort : Sort
+    {
+        #region Internal
+        internal ReSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal ReSort(Context ctx)
+            : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/SeqExpr.cs

@@ -0,0 +1,42 @@
+/*++
+Copyright (<c>) 2016 Microsoft Corporation
+
+Module Name:
+
+    SeqExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Sequence Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Sequence expressions
+    /// </summary>
+    public class SeqExpr : Expr
+    {
+        #region Internal
+        /// <summary> Constructor for SeqExpr </summary>
+        internal SeqExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/SeqSort.cs

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    SeqSort.cs
+
+Abstract:
+
+    Z3 Managed API: Sequence Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    ///  A Sequence sort
+    /// </summary>
+    public class SeqSort : Sort
+    {
+        #region Internal
+        internal SeqSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal SeqSort(Context ctx)
+            : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/Sort.cs

@@ -147,6 +147,8 @@ namespace Microsoft.Z3
                 case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
                 case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPSort(ctx, obj);
                 case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj);
+                case Z3_sort_kind.Z3_SEQ_SORT: return new SeqSort(ctx, obj);
+                case Z3_sort_kind.Z3_RE_SORT: return new ReSort(ctx, obj);
                 default:
                     throw new Z3Exception("Unknown sort kind");
             }

src/api/java/Context.java

@@ -103,6 +103,7 @@ public class Context extends IDisposable
     private BoolSort m_boolSort = null;
     private IntSort m_intSort = null;
     private RealSort m_realSort = null;
+    private SeqSort m_stringSort = null;
 
     /**
      * Retrieves the Boolean sort of the context.
@@ -142,6 +143,16 @@ public class Context extends IDisposable
         return new BoolSort(this);
     }
 
+    /**
+     * Retrieves the Integer sort of the context.
+     **/
+    public SeqSort getStringSort()
+    {
+        if (m_stringSort == null)
+            m_stringSort = mkStringSort();
+        return m_stringSort;
+    }
+
     /**
      * Create a new uninterpreted sort.
      **/
@@ -193,6 +204,31 @@ public class Context extends IDisposable
         return new ArraySort(this, domain, range);
     }
 
+    /**
+     * Create a new string sort
+     **/
+    public SeqSort mkStringSort()
+    {
+        return new SeqSort(this, Native.mkStringSort(nCtx()));
+    }
+
+    /**
+     * Create a new sequence sort
+     **/
+    public SeqSort mkSeqSort(Sort s)
+    {
+        return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
+    }
+
+    /**
+     * Create a new regular expression sort
+     **/
+    public ReSort mkReSort(Sort s)
+    {
+        return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
+    }
+
+
     /**
      * Create a new tuple sort.
      **/
@@ -1849,6 +1885,184 @@ public class Context extends IDisposable
                         arg2.getNativeObject()));
     }
 
+
+    /**
+     * Sequences, Strings and regular expressions.
+     */
+
+    /**
+     * Create the empty sequence.
+    */
+    public SeqExpr MkEmptySeq(Sort s) 
+    {
+	checkContextMatch(s);
+	return new SeqExpr(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
+    }
+
+    /**
+     * Create the singleton sequence.
+     */
+    public SeqExpr MkUnit(Expr elem) 
+    {
+	checkContextMatch(elem);
+	return new SeqExpr(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
+    }
+    
+    /**
+     * Create a string constant.
+     */
+    public SeqExpr MkString(String s) 
+    {
+	return new SeqExpr(this, Native.mkString(nCtx(), s));
+    }
+    
+    /**
+     * Concatentate sequences.
+     */
+    public SeqExpr MkConcat(SeqExpr... t)
+    {
+	checkContextMatch(t);
+	return new SeqExpr(this, Native.mkSeqConcat(nCtx(), (int)t.length, AST.arrayToNative(t)));
+    }
+    
+    
+    /**
+     * Retrieve the length of a given sequence.
+     */
+    public IntExpr MkLength(SeqExpr s)
+    {
+	checkContextMatch(s);
+	return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
+    }
+    
+    /**
+     * Check for sequence prefix.
+     */
+    public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2) 
+    {
+	checkContextMatch(s1, s2);
+	return new BoolExpr(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+    }
+    
+    /**
+     * Check for sequence suffix.
+     */
+    public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2) 
+    {
+	checkContextMatch(s1, s2);
+	return new BoolExpr(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+    }
+    
+    /**
+     * Check for sequence containment of s2 in s1.
+     */
+    public BoolExpr MkContains(SeqExpr s1, SeqExpr s2) 
+    {
+	checkContextMatch(s1, s2);
+	return new BoolExpr(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+    }
+    
+    /**
+     * Retrieve sequence of length one at index.
+     */
+    public SeqExpr MkAt(SeqExpr s, IntExpr index)
+    {
+	checkContextMatch(s, index);
+	return new SeqExpr(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
+    }
+    
+    /**
+     * Extract subsequence.
+     */
+    public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
+    {
+	checkContextMatch(s, offset, length);
+	return new SeqExpr(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
+    }
+    
+    /**
+     * Extract index of sub-string starting at offset.
+     */
+    public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
+    {
+	checkContextMatch(s, substr, offset);
+	return new IntExpr(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
+    }
+    
+    /**
+     * Replace the first occurrence of src by dst in s.
+     */
+    public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
+    {
+	checkContextMatch(s, src, dst);
+	return new SeqExpr(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
+    }
+    
+    /**
+     * Convert a regular expression that accepts sequence s.
+     */
+    public ReExpr MkToRe(SeqExpr s) 
+    {
+	checkContextMatch(s);
+	return new ReExpr(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));            
+    }
+    
+    
+    /**
+     * Check for regular expression membership.
+     */
+    public BoolExpr MkInRe(SeqExpr s, ReExpr re)
+    {
+	checkContextMatch(s, re);
+	return new BoolExpr(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));            
+    }
+    
+    /**
+     * Take the Kleene star of a regular expression.
+     */
+    public ReExpr MkStar(ReExpr re)
+    {
+	checkContextMatch(re);
+	return new ReExpr(this, Native.mkReStar(nCtx(), re.getNativeObject()));            
+    }
+    
+    /**
+     * Take the Kleene plus of a regular expression.
+     */
+    public ReExpr MPlus(ReExpr re)
+    {
+	checkContextMatch(re);
+	return new ReExpr(this, Native.mkRePlus(nCtx(), re.getNativeObject()));            
+    }
+    
+    /**
+     * Create the optional regular expression.
+     */
+    public ReExpr MOption(ReExpr re)
+    {
+	checkContextMatch(re);
+	return new ReExpr(this, Native.mkReOption(nCtx(), re.getNativeObject()));            
+    }
+    
+    /**
+     * Create the concatenation of regular languages.
+     */
+    public ReExpr MkConcat(ReExpr... t)
+    {
+	checkContextMatch(t);
+	return new ReExpr(this, Native.mkReConcat(nCtx(), (int)t.length, AST.arrayToNative(t)));
+    }
+    
+    /**
+     * Create the union of regular languages.
+     */
+    public ReExpr MkUnion(ReExpr... t)
+    {
+	checkContextMatch(t);
+	return new ReExpr(this, Native.mkReUnion(nCtx(), (int)t.length, AST.arrayToNative(t)));
+    }
+    
+
     /**
      * Create a Term of a given sort. 
      * @param v A string representing the term value in decimal notation. If the given sort is a real, then the
@@ -3683,6 +3897,19 @@ public class Context extends IDisposable
             throw new Z3Exception("Context mismatch");
     }
 
+    void checkContextMatch(Z3Object other1, Z3Object other2)
+    {
+	checkContextMatch(other1);
+	checkContextMatch(other2);
+    }
+
+    void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
+    {
+	checkContextMatch(other1);
+	checkContextMatch(other2);
+	checkContextMatch(other3);
+    }
+
     void checkContextMatch(Z3Object[] arr)
     {
         if (arr != null)
@@ -3822,6 +4049,7 @@ public class Context extends IDisposable
         m_Params_DRQ.clear(this);
         m_Probe_DRQ.clear(this);
         m_Solver_DRQ.clear(this);
+	m_Optimize_DRQ.clear(this);
         m_Statistics_DRQ.clear(this);
         m_Tactic_DRQ.clear(this);
         m_Fixedpoint_DRQ.clear(this);
@@ -3829,6 +4057,7 @@ public class Context extends IDisposable
         m_boolSort = null;
         m_intSort = null;
         m_realSort = null;
+        m_stringSort = null;
 
         synchronized (creation_lock) {
             if (m_refCount.get() == 0 && m_ctx != 0) {

src/api/java/Expr.java

@@ -2186,6 +2186,10 @@ public class Expr extends AST
             return new FPRMExpr(ctx, obj);
         case Z3_FINITE_DOMAIN_SORT:
             return new FiniteDomainExpr(ctx, obj);
+	case Z3_SEQ_SORT:
+	    return new SeqExpr(ctx, obj);
+	case Z3_RE_SORT:
+	    return new ReExpr(ctx, obj);
         default: ;
         }
 

src/api/java/Sort.java

@@ -141,6 +141,10 @@ public class Sort extends AST
             return new FPSort(ctx, obj);
         case Z3_ROUNDING_MODE_SORT:
             return new FPRMSort(ctx, obj);
+	case Z3_SEQ_SORT:
+	    return new SeqSort(ctx, obj);
+	case Z3_RE_SORT:
+	    return new ReSort(ctx, obj);
         default:
             throw new Z3Exception("Unknown sort kind");
         }

src/api/ml/z3.ml

@@ -87,6 +87,8 @@ struct
     (z3obj_sno res ctx no) ;
     (z3obj_create res) ;
     res               
+ 
+
 end
 
 open Internal
@@ -833,6 +835,13 @@ end = struct
       let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (List.length args) (expr_lton args) in
       expr_of_ptr ctx o
 
+   let apply1 ctx f t = expr_of_ptr ctx (f (context_gno ctx) (gno t)) in
+
+   let apply2 ctx f t1 t2 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) in
+
+   let apply3 ctx f t1 t2 t3 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) in
+
+
   let simplify ( x : expr ) ( p : Params.params option ) = match p with 
     | None -> expr_of_ptr (Expr.gc x) (Z3native.simplify (gnc x) (gno x))
     | Some pp -> expr_of_ptr (Expr.gc x) (Z3native.simplify_ex (gnc x) (gno x) (z3obj_gno pp))
@@ -854,13 +863,13 @@ end = struct
     if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then
       raise (Z3native.Exception "Number of arguments does not match")
     else
-      expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args))
-
+      expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) 
+      
   let substitute ( x : expr ) from to_ = 
     if (List.length from) <> (List.length to_) then
       raise (Z3native.Exception "Argument sizes do not match")
     else
-      expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_))
+      expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) 
      
   let substitute_one ( x : expr ) from to_ =
     substitute ( x : expr ) [ from ] [ to_ ]
@@ -872,7 +881,7 @@ end = struct
     if (Expr.gc x) == to_ctx then
       x
     else
-      expr_of_ptr to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx))
+      expr_of_ptr to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx)) 
 
   let to_string ( x : expr ) = Z3native.ast_to_string (gnc x) (gno x)
 
@@ -933,34 +942,33 @@ struct
   let mk_val ( ctx : context ) ( value : bool ) =
     if value then mk_true ctx else mk_false ctx
       
-  let mk_not ( ctx : context ) ( a : expr ) =
-    expr_of_ptr ctx (Z3native.mk_not (context_gno ctx) (gno a))
+  let mk_not ( ctx : context ) ( a : expr ) = apply1 ctx Z3native.mk_not a
 
-  let mk_ite ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_ite (context_gno ctx) (gno t1) (gno t2) (gno t3))
+  let mk_ite ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) = 
+    apply3 ctx Z3native.mk_ite t1 t2 t3
       
   let mk_iff ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_iff (context_gno ctx) (gno t1) (gno t2))
+    apply2 ctx Z3native.mk_iff t1 t2
 
   let mk_implies ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_implies (context_gno ctx) (gno t1) (gno t2))
+    apply2 ctx Z3native.mk_implies t1 t2
 
   let mk_xor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_xor (context_gno ctx) (gno t1) (gno t2))
+    apply2 ctx Z3native.mk_xor t1 t2
 
   let mk_and ( ctx : context ) ( args : expr list ) =
     let f x = (Expr.gno (x)) in
-    expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (List.length args) (Array.of_list (List.map f args)))
+    expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (List.length args) (Array.of_list (List.map f args))) 
 
   let mk_or ( ctx : context ) ( args : expr list ) =
     let f x = (Expr.gno (x)) in
-    expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args)))
+    expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args))) 
 
   let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) =
-    expr_of_ptr ctx (Z3native.mk_eq (context_gno ctx) (Expr.gno x) (Expr.gno y))
+    apply2 ctx Z3native.mk_eq x y
 
   let mk_distinct ( ctx : context ) ( args : expr list ) =
-    expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args))
+    expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args)) 
 
   let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (gnc x) (gno x))
 
@@ -1066,10 +1074,10 @@ struct
     mk_list f n
       
   let get_body ( x : quantifier ) =
-    expr_of_ptr (gc x) (Z3native.get_quantifier_body (gnc x) (gno x))  
+    apply1 (gc x) Z3native.get_quantifier_body x
 
   let mk_bound ( ctx : context ) ( index : int ) ( ty : Sort.sort ) =
-    expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty))
+    expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty)) 
 
   let mk_pattern ( ctx : context ) ( terms : expr list ) =
     if (List.length terms) == 0 then
@@ -1194,23 +1202,23 @@ struct
     mk_const ctx (Symbol.mk_string ctx name) domain range
       
   let mk_select ( ctx : context ) ( a : expr ) ( i : expr ) =
-    expr_of_ptr ctx (Z3native.mk_select (context_gno ctx) (Expr.gno a) (Expr.gno i))      
+    apply2 ctx Z3native.mk_select a i
 
   let mk_store ( ctx : context ) ( a : expr ) ( i : expr ) ( v : expr ) =
-    expr_of_ptr ctx (Z3native.mk_store (context_gno ctx) (Expr.gno a) (Expr.gno i) (Expr.gno v))
+    apply3 ctx Z3native.mk_store a i v
 
   let mk_const_array ( ctx : context ) ( domain : Sort.sort ) ( v : expr ) =
-    expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v))
+    expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v)) 
 
   let mk_map ( ctx : context ) ( f : func_decl ) ( args : expr list ) =
     let m x = (Expr.gno x) in    
     expr_of_ptr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (List.length args) (Array.of_list (List.map m args)))
 
   let mk_term_array  ( ctx : context ) ( arg : expr ) =
-    expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (Expr.gno arg))
+    apply1 ctx Z3native.mk_array_default arg
 
   let mk_array_ext ( ctx : context) ( arg1 : expr ) ( arg2 : expr ) =
-     expr_of_ptr ctx (Z3native.mk_array_ext (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2))
+    apply2 ctx Z3native.mk_array_ext arg1 arg2
 end
 
 
@@ -1233,13 +1241,14 @@ struct
     expr_of_ptr ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain))
 
   let mk_set_add  ( ctx : context ) ( set : expr ) ( element : expr ) =
-    expr_of_ptr ctx (Z3native.mk_set_add (context_gno ctx) (Expr.gno set) (Expr.gno element))
+    apply2 ctx Z3native.mk_set_add set element
       
   let mk_del  ( ctx : context ) ( set : expr ) ( element : expr ) =
-    expr_of_ptr ctx (Z3native.mk_set_del (context_gno ctx) (Expr.gno set) (Expr.gno element))
+    apply2 Z3native.mk_set_del set element
       
   let mk_union  ( ctx : context ) ( args : expr list ) =
-    expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args))
+    let r = expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) in
+    r
       
   let mk_intersection  ( ctx : context ) ( args : expr list ) =
     expr_of_ptr ctx (Z3native.mk_set_intersect (context_gno ctx) (List.length args) (expr_lton args))

src/api/python/z3.py

@@ -930,6 +930,10 @@ def _to_expr_ref(a, ctx):
             return FiniteDomainRef(a, ctx)
     if sk == Z3_ROUNDING_MODE_SORT:
         return FPRMRef(a, ctx)
+    if sk == Z3_SEQ_SORT:
+        return SeqRef(a, ctx)
+    if sk == Z3_RE_SORT:
+        return ReRef(a, ctx)
     return ExprRef(a, ctx)
 
 def _coerce_expr_merge(s, a):
@@ -3562,24 +3566,56 @@ def Concat(*args):
     121
     """
     args = _get_args(args)
+    sz = len(args)
+    if __debug__:
+        _z3_assert(sz >= 2, "At least two arguments expected.")
+
+    ctx = args[0].ctx
+    
+    if is_seq(args[0]):
+       if __debug__:
+         _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
+       v = (Ast * sz)()
+        for i in range(sz):
+            v[i] = args[i].as_ast()
+       return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
+    
+    if is_re(args[0]):
+       if __debug__:
+           _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
+       v = (Ast * sz)()
+       for i in range(sz):
+           v[i] = args[i].as_ast()
+       return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
+    
     if __debug__:
         _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
-        _z3_assert(len(args) >= 2, "At least two arguments expected.")
-    ctx = args[0].ctx
     r   = args[0]
-    for i in range(len(args) - 1):
+    for i in range(sz - 1):
         r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
     return r
 
 def Extract(high, low, a):
-    """Create a Z3 bit-vector extraction expression.
+    """Create a Z3 bit-vector extraction expression, or create a string extraction expression.
 
     >>> x = BitVec('x', 8)
     >>> Extract(6, 2, x)
     Extract(6, 2, x)
     >>> Extract(6, 2, x).sort()
     BitVec(5)
+    >>> simplify(Extract(StringVal("abcd"),2,1))
+    "c"
     """
+    if isinstance(high, str):
+        high = StringVal(high)
+    if is_seq(high):
+        s = high
+        offset = _py2expr(low, high.ctx)
+        length = _py2expr(a, high.ctx)
+        
+        if __debug__:
+            _z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers")
+            return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
     if __debug__:
         _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
         _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
@@ -7781,7 +7817,7 @@ def binary_interpolant(a,b,p=None,ctx=None):
     solver that determines satisfiability.
 
     x = Int('x')
-    print binary_interpolant(x<0,x>2)
+    print(binary_interpolant(x<0,x>2))
     Not(x >= 0)
     """
     f = And(Interpolant(a),b)
@@ -7821,6 +7857,7 @@ def sequence_interpolant(v,p=None,ctx=None):
         f = And(Interpolant(f),v[i])
     return tree_interpolant(f,p,ctx)
 
+
 #########################################
 #
 # Floating-Point Arithmetic
@@ -8901,3 +8938,339 @@ def fpToIEEEBV(x):
     if __debug__:
         _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
     return BitVecRef(Z3_mk_fpa_to_ieee_bv(x.ctx_ref(), x.ast), x.ctx)
+
+
+
+#########################################
+#
+# Strings, Sequences and Regular expressions
+#
+#########################################
+
+class SeqSortRef(SortRef):
+    """Sequence sort."""
+
+    def is_string(self):
+        """Determine if sort is a string
+        >>> s = StringSort()
+        >>> s.is_string()
+        True
+        >>> s = SeqSort(IntSort())
+        >>> s.is_string()
+        False
+        """
+        return Z3_is_string_sort(self.ctx_ref(), self.ast)
+    
+def StringSort(ctx=None):
+    """Create a string sort
+    >>> s = StringSort()
+    >>> print(s)
+    String
+    """
+    ctx = _get_ctx(ctx)
+    return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx)
+
+
+def SeqSort(s):
+    """Create a sequence sort over elements provided in the argument
+    >>> s = SeqSort(IntSort())
+    >>> s == Unit(IntVal(1)).sort()
+    True
+    """
+    return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx)
+
+class SeqRef(ExprRef):
+    """Sequence expression."""
+
+    def sort(self):
+        return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
+
+    def __add__(self, other):
+        return Concat(self, other)
+
+    def __getitem__(self, i):
+        return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
+        
+    def is_string(self):
+        return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
+
+    def is_string_value(self):
+        return Z3_is_string(self.ctx_ref(), self.as_ast())
+
+    def as_string(self):
+        """Return a string representation of sequence expression."""
+        return Z3_ast_to_string(self.ctx_ref(), self.as_ast())    
+
+
+def _coerce_seq(s, ctx=None):
+    if isinstance(s, str):
+        ctx = _get_ctx(ctx)
+        s = StringVal(s, ctx)
+    return s
+
+def _get_ctx2(a, b, ctx=None):
+    if is_expr(a):
+        return a.ctx
+    if is_expr(b):
+        return b.ctx
+    if ctx is None:
+        ctx = main_ctx()
+    return ctx
+
+def is_seq(a):
+    """Return `True` if `a` is a Z3 sequence expression.
+    >>> print (is_seq(Unit(IntVal(0))))
+    True
+    >>> print (is_seq(StringVal("abc")))
+    True
+    """
+    return isinstance(a, SeqRef)
+
+def is_string(a):
+    """Return `True` if `a` is a Z3 string expression.
+    >>> print (is_string(StringVal("ab")))
+    True
+    """
+    return isinstance(a, SeqRef) and a.is_string()
+
+def is_string_value(a):
+    """return 'True' if 'a' is a Z3 string constant expression.
+    >>> print (is_string_value(StringVal("a")))
+    True
+    >>> print (is_string_value(StringVal("a") + StringVal("b")))
+    False
+    """
+    return isinstance(a, SeqRef) and a.is_string_value()
+
+
+def StringVal(s, ctx=None):
+    """create a string expression"""
+    ctx = _get_ctx(ctx)
+    return SeqRef(Z3_mk_string(ctx.ref(), s), ctx)
+
+def String(name, ctx=None):
+    """Return a string constant named `name`. If `ctx=None`, then the global context is used.
+
+    >>> x = String('x')
+    """
+    ctx = _get_ctx(ctx)
+    return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)
+
+def Strings(names, ctx=None):
+    """Return a tuple of String constants. """
+    ctx = _get_ctx(ctx)
+    if isinstance(names, str):
+        names = names.split(" ")
+    return [String(name, ctx) for name in names]
+
+def Empty(s):
+    """Create the empty sequence of the given sort
+    >>> e = Empty(StringSort())
+    >>> print(e)
+    ""
+    >>> e2 = StringVal("")
+    >>> print(e.eq(e2))
+    True
+    >>> e3 = Empty(SeqSort(IntSort()))
+    >>> print(e3)
+    seq.empty
+    """
+    return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
+
+def Unit(a):
+    """Create a singleton sequence"""
+    return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx)
+
+def PrefixOf(a, b):
+    """Check if 'a' is a prefix of 'b'
+    >>> s1 = PrefixOf("ab", "abc")
+    >>> simplify(s1)
+    True
+    >>> s2 = PrefixOf("bc", "abc")
+    >>> simplify(s2)
+    False
+    """
+    ctx = _get_ctx2(a, b)
+    a = _coerce_seq(a, ctx)
+    b = _coerce_seq(b, ctx)
+    return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+def SuffixOf(a, b):
+    """Check if 'a' is a suffix of 'b'
+    >>> s1 = SuffixOf("ab", "abc")
+    >>> simplify(s1)
+    False
+    >>> s2 = SuffixOf("bc", "abc")
+    >>> simplify(s2)
+    True
+    """
+    ctx = _get_ctx2(a, b)
+    a = _coerce_seq(a, ctx)
+    b = _coerce_seq(b, ctx)    
+    return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+def Contains(a, b):
+    """Check if 'a' contains 'b'
+    >>> s1 = Contains("abc", "ab")
+    >>> simplify(s1)
+    True
+    >>> s2 = Contains("abc", "bc")
+    >>> simplify(s2)
+    True
+    >>> x, y, z = Strings('x y z')
+    >>> s3 = Contains(Concat(x,y,z), y)
+    >>> simplify(s3)
+    True
+    """
+    ctx = _get_ctx2(a, b)
+    a = _coerce_seq(a, ctx)
+    b = _coerce_seq(b, ctx)    
+    return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
+
+def Replace(s, src, dst):
+    """Replace the first occurrence of 'src' by 'dst' in 's'
+    >>> r = Replace("aaa", "a", "b")
+    >>> simplify(r)
+    "baa"
+    """
+    ctx = _get_ctx2(dst, s)
+    if ctx is None and is_expr(src):
+        ctx = src.ctx
+    src = _coerce_seq(src, ctx)
+    dst = _coerce_seq(dst, ctx)
+    s   = _coerce_seq(s, ctx)
+    return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)
+
+def IndexOf(s, substr):
+    return IndexOf(s, substr, IntVal(0))
+
+def IndexOf(s, substr, offset):
+    """Retrieve the index of substring within a string starting at a specified offset.
+    >>> simplify(IndexOf("abcabc", "bc", 0))
+    1
+    >>> simplify(IndexOf("abcabc", "bc", 2))
+    4
+    """
+    ctx = None
+    if is_expr(offset):
+        ctx = offset.ctx
+    ctx = _get_ctx2(s, substr, ctx)
+    s = _coerce_seq(s, ctx)
+    substr = _coerce_seq(substr, ctx)
+    if isinstance(offset, int):
+        offset = IntVal(offset, ctx)    
+    return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
+
+def Length(s):
+    """Obtain the length of a sequence 's'
+    >>> l = Length(StringVal("abc"))
+    >>> simplify(l)
+    3
+    """
+    s = _coerce_seq(s)
+    return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
+
+def Re(s, ctx=None):
+    """The regular expression that accepts sequence 's'
+    >>> s1 = Re("ab")
+    >>> s2 = Re(StringVal("ab"))
+    >>> s3 = Re(Unit(BoolVal(True)))
+    """
+    s = _coerce_seq(s, ctx)
+    return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx)
+
+
+
+
+## Regular expressions
+
+class ReSortRef(SortRef):
+    """Regular expression sort."""
+
+
+def ReSort(s):
+    if is_ast(s):
+        return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx)
+    if s is None or isinstance(s, Context):
+        ctx = _get_ctx(s)
+        return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx)
+    raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument")
+
+
+class ReRef(ExprRef):
+    """Regular expressions."""
+
+    def __add__(self, other):
+        return Union(self, other)
+
+
+def is_re(s):
+    return isinstance(s, ReRef)
+
+
+def InRe(s, re):
+    """Create regular expression membership test
+    >>> re = Union(Re("a"),Re("b"))
+    >>> print (simplify(InRe("a", re)))
+    True
+    >>> print (simplify(InRe("b", re)))
+    True
+    >>> print (simplify(InRe("c", re)))
+    False
+    """
+    s = _coerce_seq(s, re.ctx)
+    return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
+
+def Union(*args):
+    """Create union of regular expressions.
+    >>> re = Union(Re("a"), Re("b"), Re("c"))
+    >>> print (simplify(InRe("d", re)))
+    False
+    """    
+    args = _get_args(args)
+    sz = len(args)
+    if __debug__:
+        _z3_assert(sz >= 2, "At least two arguments expected.")
+        _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
+    ctx = args[0].ctx    
+    v = (Ast * sz)()
+    for i in range(sz):
+        v[i] = args[i].as_ast()
+    return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx)
+
+def Plus(re):
+    """Create the regular expression accepting one or more repetitions of argument.
+    >>> re = Plus(Re("a"))
+    >>> print(simplify(InRe("aa", re)))
+    True
+    >>> print(simplify(InRe("ab", re)))
+    False
+    >>> print(simplify(InRe("", re)))
+    False
+    """    
+    return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
+
+def Option(re):
+    """Create the regular expression that optionally accepts the argument.
+    >>> re = Option(Re("a"))
+    >>> print(simplify(InRe("a", re)))
+    True
+    >>> print(simplify(InRe("", re)))
+    True
+    >>> print(simplify(InRe("aa", re)))
+    False
+    """
+    return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
+
+def Star(re):
+    """Create the regular expression accepting zero or more repetitions of argument.
+    >>> re = Star(Re("a"))
+    >>> print(simplify(InRe("aa", re)))
+    True
+    >>> print(simplify(InRe("ab", re)))
+    False
+    >>> print(simplify(InRe("", re)))
+    True
+    """    
+    return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)

src/api/python/z3printer.py

@@ -570,6 +570,9 @@ class Formatter:
     def pp_algebraic(self, a):
         return to_format(a.as_decimal(self.precision))
 
+    def pp_string(self, a):
+	return to_format(a.as_string())
+
     def pp_bv(self, a):
         return to_format(a.as_string())
 
@@ -875,6 +878,8 @@ class Formatter:
             return self.pp_fp_value(a)
         elif z3.is_fp(a):
             return self.pp_fp(a, d, xs)
+	elif z3.is_string_value(a):
+	    return self.pp_string(a)	
         elif z3.is_const(a):
             return self.pp_const(a)
         else:

src/api/z3_api.h

@@ -161,6 +161,8 @@ typedef enum
     Z3_FINITE_DOMAIN_SORT,
     Z3_FLOATING_POINT_SORT,
     Z3_ROUNDING_MODE_SORT,
+    Z3_SEQ_SORT,
+    Z3_RE_SORT,
     Z3_UNKNOWN_SORT = 1000
 } Z3_sort_kind;
 
@@ -1098,7 +1100,7 @@ typedef enum {
     Z3_OP_PR_TH_LEMMA,
     Z3_OP_PR_HYPER_RESOLVE,
 
-    // Sequences
+    // Relational algebra
     Z3_OP_RA_STORE = 0x600,
     Z3_OP_RA_EMPTY,
     Z3_OP_RA_IS_EMPTY,
@@ -1115,6 +1117,28 @@ typedef enum {
     Z3_OP_FD_CONSTANT,
     Z3_OP_FD_LT,
 
+    // Sequences
+    Z3_OP_SEQ_UNIT,
+    Z3_OP_SEQ_EMPTY,
+    Z3_OP_SEQ_CONCAT,
+    Z3_OP_SEQ_PREFIX,
+    Z3_OP_SEQ_SUFFIX,
+    Z3_OP_SEQ_CONTAINS,
+    Z3_OP_SEQ_EXTRACT,
+    Z3_OP_SEQ_REPLACE,
+    Z3_OP_SEQ_AT,
+    Z3_OP_SEQ_LENGTH,    
+    Z3_OP_SEQ_INDEX,
+    Z3_OP_SEQ_TO_RE,
+    Z3_OP_SEQ_IN_RE,
+
+    // regular expressions
+    Z3_OP_RE_PLUS,
+    Z3_OP_RE_STAR,
+    Z3_OP_RE_OPTION,
+    Z3_OP_RE_CONCAT,
+    Z3_OP_RE_UNION,
+
     // Auxiliary
     Z3_OP_LABEL = 0x700,
     Z3_OP_LABEL_LIT,
@@ -3093,6 +3117,222 @@ extern "C" {
 
     /*@}*/
 
+    /** @name Sequences and regular expressions */
+    /*@{*/
+
+    /**
+       \brief Create a sequence sort out of the sort for the elements.
+
+       def_API('Z3_mk_seq_sort', SORT, (_in(CONTEXT), _in(SORT)))
+     */
+    Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);
+
+    /**
+       \brief Check if \c s is a sequence sort.
+
+       def_API('Z3_is_seq_sort', BOOL, (_in(CONTEXT), _in(SORT)))
+     */
+    Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
+
+    /**
+       \brief Create a regular expression sort out of a sequence sort.
+
+       def_API('Z3_mk_re_sort', SORT, (_in(CONTEXT), _in(SORT)))
+     */
+    Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);
+
+    /**
+       \brief Check if \c s is a regular expression sort.
+
+       def_API('Z3_is_re_sort', BOOL, (_in(CONTEXT), _in(SORT)))
+     */
+    Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
+
+    /**
+       \brief Create a sort for 8 bit strings.
+
+       This function creates a sort for ASCII strings.
+       Each character is 8 bits.
+
+       def_API('Z3_mk_string_sort', SORT ,(_in(CONTEXT), ))
+     */
+    Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
+
+    /**
+       \brief Check if \c s is a string sort.
+
+       def_API('Z3_is_string_sort', BOOL, (_in(CONTEXT), _in(SORT)))
+     */
+    Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
+
+    /**
+       \brief Create a string constant out of the string that is passed in
+       def_API('Z3_mk_string' ,AST ,(_in(CONTEXT), _in(STRING)))
+     */
+    Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
+
+    /**
+       \brief Determine if \c s is a string constant.
+
+       def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST)))
+     */
+    Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s); 
+
+    /**
+       \brief Retrieve the string constant stored in \c s.
+       
+       \pre  Z3_is_string(c, s)
+
+       def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST)))
+     */
+    Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
+
+    /**
+       \brief Create an empty sequence of the sequence sort \c seq.
+
+       \pre s is a sequence sort.
+
+       def_API('Z3_mk_seq_empty' ,AST ,(_in(CONTEXT), _in(SORT)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq);
+
+    /**
+       \brief Create a unit sequence of \c a.
+
+       def_API('Z3_mk_seq_unit' ,AST ,(_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a);
+
+    /**
+       \brief Concatenate sequences.
+
+       \pre n > 0
+
+       def_API('Z3_mk_seq_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]);
+
+    /**
+       \brief Check if \c prefix is a prefix of \c s.
+
+       \pre prefix and s are the same sequence sorts.
+
+       def_API('Z3_mk_seq_prefix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);
+
+    /**
+       \brief Check if \c suffix is a suffix of \c s.
+
+       \pre \c suffix and \c s are the same sequence sorts.
+
+       def_API('Z3_mk_seq_suffix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);
+
+    /**
+       \brief Check if \c container contains \c containee.
+
+       \pre \c container and \c containee are the same sequence sorts.
+
+       def_API('Z3_mk_seq_contains' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
+
+    /**
+       \brief Extract subsequence starting at \c offset of \c length.
+
+       def_API('Z3_mk_seq_extract' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);
+
+    /**
+       \brief Replace the first occurrence of \c src with \c dst in \c s.
+
+       def_API('Z3_mk_seq_replace' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
+
+    /**
+       \brief Retrieve from \s the unit sequence positioned at position \c index.
+
+       def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
+
+    /**
+       \brief Return the length of the sequence \c s.
+
+       def_API('Z3_mk_seq_length' ,AST ,(_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s);
+
+
+    /**
+       \brief Return index of first occurrence of \c substr in \c s starting from offset \c offset.
+       If \c s does not contain \c substr, then the value is -1, if \c offset is the length of \c s, then the value is -1 as well.
+       The function is under-specified if \c offset is negative or larger than the length of \c s.
+
+       def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
+    
+    /**
+       \brief Create a regular expression that accepts the sequence \c seq.
+
+       def_API('Z3_mk_seq_to_re' ,AST ,(_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);
+
+    /**
+       \brief Check if \c seq is in the language generated by the regular expression \c re.
+
+       def_API('Z3_mk_seq_in_re' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);
+
+    /**
+       \brief Create the regular language \c re+.
+
+       def_API('Z3_mk_re_plus' ,AST ,(_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re);
+
+    /**
+       \brief Create the regular language \c re*.
+
+       def_API('Z3_mk_re_star' ,AST ,(_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re);
+
+    /**
+       \brief Create the regular language \c [re].
+
+       def_API('Z3_mk_re_option' ,AST ,(_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re);
+
+    /**
+       \brief Create the union of the regular languages.
+
+       \pre n > 0
+
+       def_API('Z3_mk_re_union' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST)))
+     */
+    Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]);
+
+    /**
+       \brief Create the concatenation of the regular languages.
+
+       \pre n > 0
+
+       def_API('Z3_mk_re_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST)))
+     */
+    Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]);
+
+    /*@}*/
+
+
     /** @name Quantifiers */
     /*@{*/
     /**

src/api/z3_replayer.cpp

@@ -46,6 +46,7 @@ struct z3_replayer::imp {
     size_t                   m_ptr;
     size_t_map<void *>       m_heap;
     svector<z3_replayer_cmd> m_cmds;
+    vector<std::string>      m_cmds_names;
 
     enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
 
@@ -509,6 +510,7 @@ struct z3_replayer::imp {
                 if (idx >= m_cmds.size())
                     throw z3_replayer_exception("invalid command");
                 try {
+                    TRACE("z3_replayer_cmd", tout << m_cmds_names[idx] << "\n";);
                     m_cmds[idx](m_owner);
                 }
                 catch (z3_error & ex) {
@@ -672,9 +674,11 @@ struct z3_replayer::imp {
         m_result = obj;
     }
 
-    void register_cmd(unsigned id, z3_replayer_cmd cmd) {
+    void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) {
         m_cmds.reserve(id+1, 0);
+        m_cmds_names.reserve(id+1, "");
         m_cmds[id] = cmd;
+        m_cmds_names[id] = name;
     }
 
     void reset() {
@@ -786,8 +790,8 @@ void z3_replayer::store_result(void * obj) {
     return m_imp->store_result(obj);
 }
 
-void z3_replayer::register_cmd(unsigned id, z3_replayer_cmd cmd) {
-    return m_imp->register_cmd(id, cmd);
+void z3_replayer::register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) {
+    return m_imp->register_cmd(id, cmd, name);
 }
 
 void z3_replayer::parse() {

src/api/z3_replayer.h

@@ -62,7 +62,7 @@ public:
     void ** get_obj_addr(unsigned pos);
 
     void store_result(void * obj);
-    void register_cmd(unsigned id, z3_replayer_cmd cmd);
+    void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name);
 };
 
 #endif

src/ast/ast.cpp

@@ -1656,6 +1656,7 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
+    
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
     // increment reference counters

src/ast/rewriter/bit_blaster/bit_blaster_tpl.h

@@ -121,8 +121,11 @@ public:
     void mk_comp(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
 
     void mk_carry_save_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr * const * c_bits, expr_ref_vector & sum_bits, expr_ref_vector & carry_bits);
-    void mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
+    bool mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
+    bool mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
+    void mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits);
 
+    bool is_bool_const(expr* e) const { return m().is_true(e) || m().is_false(e); }
     void mk_abs(unsigned sz, expr * const * a_bits, expr_ref_vector & out_bits);
 };
 

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -38,7 +38,7 @@ void bit_blaster_tpl<Cfg>::checkpoint() {
 template<typename Cfg>
 bool bit_blaster_tpl<Cfg>::is_numeral(unsigned sz, expr * const * bits) const {
     for (unsigned i = 0; i < sz; i++)
-        if (!m().is_true(bits[i]) && !m().is_false(bits[i]))
+        if (!is_bool_const(bits[i])) 
             return false;
     return true;
 }
@@ -158,30 +158,24 @@ void bit_blaster_tpl<Cfg>::mk_subtracter(unsigned sz, expr * const * a_bits, exp
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
     SASSERT(sz > 0);
-    
-    if (!m_use_bcm) {
-        numeral n_a, n_b;
-        if (is_numeral(sz, a_bits, n_b))
-            std::swap(a_bits, b_bits);
-        if (is_minus_one(sz, b_bits)) {
-            mk_neg(sz, a_bits, out_bits);
-            return;
-        }
-        if (is_numeral(sz, a_bits, n_a)) {
-            n_a *= n_b;
-            num2bits(n_a, sz, out_bits);
-            return;
-        }
+    numeral n_a, n_b;
+    if (is_numeral(sz, a_bits, n_b))
+        std::swap(a_bits, b_bits);
+    if (is_minus_one(sz, b_bits)) {
+        mk_neg(sz, a_bits, out_bits);
+        return;
     }
-    else {
-        numeral n_a, n_b;
-        if (is_numeral(sz, a_bits, n_a)) {
-            mk_const_multiplier(sz, a_bits, b_bits, out_bits);
-            return;
-        } else if (is_numeral(sz, b_bits, n_b)) {
-            mk_const_multiplier(sz, b_bits, a_bits, out_bits);
-            return;
-        }
+    if (is_numeral(sz, a_bits, n_a)) {
+        n_a *= n_b;
+        num2bits(n_a, sz, out_bits);
+        return;
+    }
+    
+    if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
+        return;
+    }
+    if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) {
+        return;
     }
 
     if (!m_use_wtm) {
@@ -1171,13 +1165,74 @@ void bit_blaster_tpl<Cfg>::mk_carry_save_adder(unsigned sz, expr * const * a_bit
 }
 
 template<typename Cfg>
-void bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
-    DEBUG_CODE({
-        numeral x;
-        SASSERT(is_numeral(sz, a_bits, x));
-        SASSERT(out_bits.empty());        
-    });    
+bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
+    unsigned nb = 0;
+    unsigned case_size = 1;
+    unsigned circuit_size = sz*sz*5;
+    for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) {
+        if (!is_bool_const(a_bits[i])) {
+            case_size *= 2;
+        }
+        if (!is_bool_const(b_bits[i])) {
+            case_size *= 2;
+        }
+    }
+    if (case_size >= circuit_size) {
+        return false;
+    }
+    SASSERT(out_bits.empty());
     
+    ptr_buffer<expr, 128> na_bits;
+    na_bits.append(sz, a_bits);
+    ptr_buffer<expr, 128> nb_bits;
+    nb_bits.append(sz, b_bits);
+    mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits); 
+    return false;
+}
+ 
+template<typename Cfg>
+void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits) {
+    while (is_a && i < sz && is_bool_const(a_bits[i])) ++i;
+    if (is_a && i == sz) { is_a = false; i = 0; }
+    while (!is_a && i < sz && is_bool_const(b_bits[i])) ++i;
+    if (i < sz) {
+        expr_ref_vector out1(m()), out2(m());
+        expr_ref x(m());
+        x = is_a?a_bits[i]:b_bits[i];
+        if (is_a) a_bits[i] = m().mk_true(); else b_bits[i] = m().mk_true();
+        mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out1);
+        if (is_a) a_bits[i] = m().mk_false(); else b_bits[i] = m().mk_false();
+        mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out2);
+        if (is_a) a_bits[i] = x; else b_bits[i] = x;
+        SASSERT(out_bits.empty());
+        for (unsigned j = 0; j < sz; ++j) {
+            out_bits.push_back(m().mk_ite(x, out1[j].get(), out2[j].get()));
+        }        
+    }
+    else {
+        numeral n_a, n_b;
+        SASSERT(i == sz && !is_a);
+        VERIFY(is_numeral(sz, a_bits.c_ptr(), n_a));
+        VERIFY(is_numeral(sz, b_bits.c_ptr(), n_b));
+        n_a *= n_b;
+        num2bits(n_a, sz, out_bits);
+    }
+}
+
+template<typename Cfg>
+bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
+    numeral n_a;
+    if (!is_numeral(sz, a_bits, n_a)) {
+        return false;
+    }
+    SASSERT(out_bits.empty());
+    
+    if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
+        return true;
+    }    
+    if (!m_use_bcm) {
+        return false;
+    }
     expr_ref_vector minus_b_bits(m()), tmp(m());
     mk_neg(sz, b_bits, minus_b_bits);
         
@@ -1255,4 +1310,6 @@ void bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
 
     TRACE("bit_blaster_tpl_booth", for (unsigned i=0; i<out_bits.size(); i++)
                                      tout << "Booth encoding: " << mk_pp(out_bits[i].get(), m()) << "\n"; );
+
+    return true;
 }

src/ast/rewriter/bv_rewriter.cpp

@@ -1968,7 +1968,63 @@ void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & r
         result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2));
 }
 
+#include "ast_pp.h"
+
+bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) {
+    if (!m_util.is_numeral(lhs) || !is_add(rhs)) {
+        std::swap(lhs, rhs);
+    }
+    if (!m_util.is_numeral(lhs) || !is_add(rhs)) {
+        return false;
+    }
+    unsigned sz = to_app(rhs)->get_num_args();
+    expr_ref t1(m()), t2(m());
+    t1 = to_app(rhs)->get_arg(0);
+    if (sz > 2) {
+        t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1);
+    }
+    else {
+        SASSERT(sz == 2);
+        t2 = to_app(rhs)->get_arg(1);
+    }
+    mk_t1_add_t2_eq_c(t1, t2, lhs, result);
+    return true;
+}
+
+bool bv_rewriter::is_add_mul_const(expr* e) const {
+    if (!m_util.is_bv_add(e)) {
+        return false;
+    }
+    unsigned num = to_app(e)->get_num_args();
+    for (unsigned i = 0; i < num; i++) {
+        expr * arg = to_app(e)->get_arg(i);
+        expr * c2, * x2;
+        if (m_util.is_numeral(arg))
+            continue;
+        if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2))
+            continue;
+        return false;
+    }
+    return true;
+}
+
+bool bv_rewriter::is_concat_target(expr* lhs, expr* rhs) const {
+    return
+        m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs))) ||
+        m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs)));
+}
+
+bool bv_rewriter::has_numeral(app* a) const {
+    for (unsigned i = 0; i < a->get_num_args(); ++i) {
+        if (is_numeral(a->get_arg(i))) {
+            return true;
+        }
+    }
+    return false;
+}
+
 br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
+        
     expr * c, * x;
     numeral c_val, c_inv_val;
     unsigned sz;
@@ -2001,24 +2057,30 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
 
         // c * x =  t_1 + ... + t_n
         // and t_i's have non-unary coefficients (this condition is used to make sure we are actually reducing the number of multipliers).
-        if (m_util.is_bv_add(rhs)) {
+        if (is_add_mul_const(rhs)) {
             // Potential problem: this simplification may increase the number of adders by reducing the amount of sharing.
-            unsigned num = to_app(rhs)->get_num_args();
-            unsigned i;
-            for (i = 0; i < num; i++) {
-                expr * arg = to_app(rhs)->get_arg(i);
-                expr * c2, * x2;
-                if (m_util.is_numeral(arg))
-                    continue;
-                if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2))
-                    continue;
-                break;
-            }
-            if (i == num) {
-                result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs));
-                return BR_REWRITE2;
+            result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs));
+            return BR_REWRITE2;
+        }
+    }
+    if (m_util.is_numeral(lhs, c_val, sz) && is_add_mul_const(rhs)) {
+        unsigned sz = to_app(rhs)->get_num_args();
+        unsigned i = 0;
+        expr* c2, *x2;
+        numeral c2_val, c2_inv_val;
+        bool found = false;
+        for (; !found && i < sz; ++i) {
+            expr* arg = to_app(rhs)->get_arg(i);
+            if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) &&
+                m_util.mult_inverse(c2_val, sz, c2_inv_val)) {
+                found = true;
             }
         }
+        if (found) {
+            result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz), 
+                               m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs));
+            return BR_REWRITE3;
+        }
     }
     return BR_FAILED;
 }
@@ -2065,9 +2127,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             return st;
     }
 
+    expr_ref new_lhs(m());
+    expr_ref new_rhs(m());
+
     if (m_util.is_bv_add(lhs) || m_util.is_bv_mul(lhs) || m_util.is_bv_add(rhs) || m_util.is_bv_mul(rhs)) {
-        expr_ref new_lhs(m());
-        expr_ref new_rhs(m());
         st = cancel_monomials(lhs, rhs, false, new_lhs, new_rhs);
         if (st != BR_FAILED) {
             if (is_numeral(new_lhs) && is_numeral(new_rhs)) {
@@ -2080,28 +2143,27 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             new_rhs = rhs;
         }
         
+        lhs = new_lhs;
+        rhs = new_rhs;
         // Try to rewrite t1 + t2 = c --> t1 = c - t2   
         // Reason: it is much cheaper to bit-blast.
-        expr * t1, * t2;
-        if (m_util.is_bv_add(new_lhs, t1, t2) && is_numeral(new_rhs)) {
-            mk_t1_add_t2_eq_c(t1, t2, new_rhs, result);
+        if (isolate_term(lhs, rhs, result)) {
             return BR_REWRITE2;
         }
-        if (m_util.is_bv_add(new_rhs, t1, t2) && is_numeral(new_lhs)) {
-            mk_t1_add_t2_eq_c(t1, t2, new_lhs, result);
-            return BR_REWRITE2;
+        if (is_concat_target(lhs, rhs)) {
+            return mk_eq_concat(lhs, rhs, result);
         }
-        
+
         if (st != BR_FAILED) {
-            result = m().mk_eq(new_lhs, new_rhs); 
+            result = m().mk_eq(lhs, rhs); 
             return BR_DONE;
         }
     }
 
-    if ((m_util.is_concat(lhs) && is_concat_split_target(rhs)) || 
-        (m_util.is_concat(rhs) && is_concat_split_target(lhs)))
+    if (is_concat_target(lhs, rhs)) {
         return mk_eq_concat(lhs, rhs, result);
-   
+    }
+
     if (swapped) {
         result = m().mk_eq(lhs, rhs);
         return BR_DONE;

src/ast/rewriter/bv_rewriter.h

@@ -137,6 +137,10 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool is_concat_split_target(expr * t) const;
 
     br_status mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result);
+    bool is_add_mul_const(expr* e) const;
+    bool isolate_term(expr* lhs, expr* rhs, expr_ref & result);
+    bool has_numeral(app* e) const;
+    bool is_concat_target(expr* lhs, expr* rhs) const;
 
     void updt_local_params(params_ref const & p);
 

src/ast/rewriter/expr_safe_replace.cpp

@@ -20,9 +20,11 @@ Revision History:
 
 #include "expr_safe_replace.h"
 #include "rewriter.h"
+#include "ast_pp.h"
 
 
 void expr_safe_replace::insert(expr* src, expr* dst) {
+    SASSERT(m.get_sort(src) == m.get_sort(dst));
     m_src.push_back(src);
     m_dst.push_back(dst);
     m_subst.insert(src, dst);
@@ -30,7 +32,7 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
 
 void expr_safe_replace::operator()(expr* e, expr_ref& res) {
     m_todo.push_back(e);
-    expr* a, *b, *d;
+    expr* a, *b;
     
     while (!m_todo.empty()) {
         a = m_todo.back();
@@ -39,7 +41,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
         }
         else if (m_subst.find(a, b)) {
             m_cache.insert(a, b);
-            m_todo.pop_back();
+            m_todo.pop_back();            
         }
         else if (is_var(a)) {
             m_cache.insert(a, a);
@@ -51,18 +53,21 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
             m_args.reset();
             bool arg_differs = false;
             for (unsigned i = 0; i < n; ++i) {
-                if (m_cache.find(c->get_arg(i), d)) {
+                expr* d = 0, *arg = c->get_arg(i);
+                if (m_cache.find(arg, d)) {
                     m_args.push_back(d);
-                    arg_differs |= c->get_arg(i) != d;
+                    arg_differs |= arg != d;
+                    SASSERT(m.get_sort(arg) == m.get_sort(d));
                 }
                 else {
-                    m_todo.push_back(c->get_arg(i));
+                    m_todo.push_back(arg);
                 }
             }
             if (m_args.size() == n) {
                 if (arg_differs) {
                     b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
                     m_refs.push_back(b);
+                    SASSERT(m.get_sort(a) == m.get_sort(b));
                 } else {
                     b = a;
                 }

src/ast/rewriter/seq_rewriter.cpp

@@ -22,30 +22,144 @@ Notes:
 #include"ast_pp.h"
 #include"ast_util.h"
 #include"uint_set.h"
+#include"automaton.h"
+#include"well_sorted.h"
 
 
+struct display_expr1 {
+    ast_manager& m;
+    display_expr1(ast_manager& m): m(m) {}
+    std::ostream& display(std::ostream& out, expr* e) const {
+        return out << mk_pp(e, m);
+    }
+};
+
+
+re2automaton::re2automaton(ast_manager& m): m(m), u(m) {}
+
+eautomaton* re2automaton::operator()(expr* e) { 
+    eautomaton* r = re2aut(e); 
+    if (r) {
+        //display_expr1 disp(m);
+        //r->display(std::cout, disp);
+        r->compress(); 
+        //r->display(std::cout, disp);
+    }
+    return r;
+} 
+
+
+eautomaton* re2automaton::re2aut(expr* e) {
+    SASSERT(u.is_re(e));
+    expr* e1, *e2;
+    scoped_ptr<eautomaton> a, b;
+    if (u.re.is_to_re(e, e1)) {
+        return seq2aut(e1);
+    }
+    else if (u.re.is_concat(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
+        return eautomaton::mk_concat(*a, *b);
+    }
+    else if (u.re.is_union(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
+        return eautomaton::mk_union(*a, *b);
+    }
+    else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
+        a->add_final_to_init_moves();
+        a->add_init_to_final_states();
+        
+        return a.detach();            
+    }
+    else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
+        a->add_final_to_init_moves();
+        return a.detach();            
+    }
+    else if (u.re.is_opt(e, e1) && (a = re2aut(e1))) {
+        a = eautomaton::mk_opt(*a);
+        return a.detach();                    
+    }
+    else if (u.re.is_range(e)) {
+
+    }
+    else if (u.re.is_loop(e)) {
+
+    }
+#if 0
+    else if (u.re.is_intersect(e, e1, e2)) {
+
+    }
+    else if (u.re.is_empty(e)) {
+
+    }
+#endif
+    
+    return 0;
+}
+
+eautomaton* re2automaton::seq2aut(expr* e) {
+    SASSERT(u.is_seq(e));
+    zstring s;
+    expr* e1, *e2;
+    scoped_ptr<eautomaton> a, b;
+    if (u.str.is_concat(e, e1, e2) && (a = seq2aut(e1)) && (b = seq2aut(e2))) {
+        return eautomaton::mk_concat(*a, *b);
+    }
+    else if (u.str.is_unit(e, e1)) {
+        return alloc(eautomaton, m, e1);
+    }
+    else if (u.str.is_empty(e)) {
+        return eautomaton::mk_epsilon(m);
+    }
+    else if (u.str.is_string(e, s)) {        
+        unsigned init = 0;
+        eautomaton::moves mvs;        
+        unsigned_vector final;
+        final.push_back(s.length());
+        for (unsigned k = 0; k < s.length(); ++k) {
+            // reference count?
+            mvs.push_back(eautomaton::move(m, k, k+1, u.str.mk_char(s, k)));
+        }
+        return alloc(eautomaton, m, init, final, mvs);
+    }
+    return 0;
+}
+
 br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(f->get_family_id() == get_fid());
     
     switch(f->get_decl_kind()) {
 
     case OP_SEQ_UNIT:
-    case OP_SEQ_EMPTY:
-
-    case OP_RE_PLUS:
-    case OP_RE_STAR:
-    case OP_RE_OPTION:
-    case OP_RE_RANGE:
-    case OP_RE_CONCAT:
-    case OP_RE_UNION:
-    case OP_RE_INTERSECT:
-    case OP_RE_LOOP:
-    case OP_RE_EMPTY_SET:
-    case OP_RE_FULL_SET:
-    case OP_RE_OF_PRED:
-    case _OP_SEQ_SKOLEM:
         return BR_FAILED;
-    
+    case OP_SEQ_EMPTY:
+        return BR_FAILED;
+    case OP_RE_PLUS:
+        SASSERT(num_args == 1);
+        return mk_re_plus(args[0], result);
+    case OP_RE_STAR:
+        SASSERT(num_args == 1);
+        return mk_re_star(args[0], result);
+    case OP_RE_OPTION:
+        SASSERT(num_args == 1);
+        return mk_re_opt(args[0], result);
+    case OP_RE_CONCAT:
+        SASSERT(num_args == 2);
+        return mk_re_concat(args[0], args[1], result);
+    case OP_RE_UNION:
+        SASSERT(num_args == 2);
+        return mk_re_union(args[0], args[1], result);
+    case OP_RE_RANGE:
+        return BR_FAILED;    
+    case OP_RE_INTERSECT:
+        return BR_FAILED;    
+    case OP_RE_LOOP:
+        return BR_FAILED;    
+    case OP_RE_EMPTY_SET:
+        return BR_FAILED;    
+    case OP_RE_FULL_SET:
+        return BR_FAILED;    
+    case OP_RE_OF_PRED:
+        return BR_FAILED;    
+    case _OP_SEQ_SKOLEM:
+        return BR_FAILED;    
     case OP_SEQ_CONCAT: 
         if (num_args == 1) {
             result = args[0];
@@ -83,10 +197,11 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 3);
         return mk_seq_replace(args[0], args[1], args[2], result);
     case OP_SEQ_TO_RE:
-        return BR_FAILED;
+        SASSERT(num_args == 1);
+        return mk_str_to_regexp(args[0], result);
     case OP_SEQ_IN_RE:
-        return BR_FAILED;
-
+        SASSERT(num_args == 2);
+        return mk_str_in_regexp(args[0], args[1], result);
     case OP_STRING_CONST:
         return BR_FAILED;
     case OP_STRING_ITOS: 
@@ -129,8 +244,8 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
         result = m_util.str.mk_string(s1 + s2);
         return BR_DONE;
     }
-    if (m_util.str.is_concat(b, c, d)) {
-        result = m_util.str.mk_concat(m_util.str.mk_concat(a, c), d);
+    if (m_util.str.is_concat(a, c, d)) {
+        result = m_util.str.mk_concat(c, m_util.str.mk_concat(d, b));
         return BR_REWRITE2;
     }
     if (m_util.str.is_empty(a)) {
@@ -141,11 +256,15 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
         result = a;
         return BR_DONE;
     }
-    if (m_util.str.is_concat(a, c, d) && 
-        m_util.str.is_string(d, s1) && isc2) {
+    // TBD concatenation is right-associative
+    if (isc2 && m_util.str.is_concat(a, c, d) && m_util.str.is_string(d, s1)) {
         result = m_util.str.mk_concat(c, m_util.str.mk_string(s1 + s2));
         return BR_DONE;
     }
+    if (isc1 && m_util.str.is_concat(b, c, d) && m_util.str.is_string(c, s2)) {
+        result = m_util.str.mk_concat(m_util.str.mk_string(s1 + s2), d);
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 
@@ -156,17 +275,17 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
     unsigned len = 0;
     unsigned j = 0;
     for (unsigned i = 0; i < m_es.size(); ++i) {
-        if (m_util.str.is_string(m_es[i], b)) {
+        if (m_util.str.is_string(m_es[i].get(), b)) {
             len += b.length();
         }
-        else if (m_util.str.is_unit(m_es[i])) {
+        else if (m_util.str.is_unit(m_es[i].get())) {
             len += 1;
         }
-        else if (m_util.str.is_empty(m_es[i])) {
+        else if (m_util.str.is_empty(m_es[i].get())) {
             // skip
         }
         else {
-            m_es[j] = m_es[i];
+            m_es[j] = m_es[i].get();
             ++j;
         }
     }
@@ -177,7 +296,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
     if (j != m_es.size() || j != 1) {
         expr_ref_vector es(m());        
         for (unsigned i = 0; i < j; ++i) {
-            es.push_back(m_util.str.mk_length(m_es[i]));
+            es.push_back(m_util.str.mk_length(m_es[i].get()));
         }
         if (len != 0) {
             es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true));
@@ -207,20 +326,31 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
         return BR_DONE;
     }
     // check if subsequence of b is in a.
-    ptr_vector<expr> as, bs;
+    expr_ref_vector as(m()), bs(m());
     m_util.str.get_concat(a, as);
     m_util.str.get_concat(b, bs);
+    bool all_values = true;
+    
+    for (unsigned i = 0; all_values && i < bs.size(); ++i) { 
+        all_values = m().is_value(bs[i].get());
+    }
+
     bool found = false;
     for (unsigned i = 0; !found && i < as.size(); ++i) {
         if (bs.size() > as.size() - i) break;
+        all_values &= m().is_value(as[i].get());
         unsigned j = 0;
-        for (; j < bs.size() && as[j+i] == bs[j]; ++j) {};
+        for (; j < bs.size() && as[j+i].get() == bs[j].get(); ++j) {};
         found = j == bs.size();
     }
     if (found) {
         result = m().mk_true();
         return BR_DONE;
     }
+    if (all_values) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 
@@ -292,7 +422,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     expr* b1 = m_util.str.get_leftmost_concat(b);
     isc1 = m_util.str.is_string(a1, s1);
     isc2 = m_util.str.is_string(b1, s2);
-    ptr_vector<expr> as, bs;
+    expr_ref_vector as(m()), bs(m());
 
     if (a1 != b1 && isc1 && isc2) {
         if (s1.length() <= s2.length()) {
@@ -342,15 +472,26 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     m_util.str.get_concat(a, as);
     m_util.str.get_concat(b, bs);
     unsigned i = 0;
-    for (; i < as.size() && i < bs.size() && as[i] == bs[i]; ++i) {};
+    bool all_values = true;    
+    for (; i < as.size() && i < bs.size(); ++i) {
+        all_values &= m().is_value(as[i].get()) && m().is_value(bs[i].get());
+        if (as[i].get() != bs[i].get()) {
+            if (all_values) {
+                result = m().mk_false();
+                return BR_DONE;
+            }
+            break;
+        }
+    };
     if (i == as.size()) {
         result = m().mk_true();
         return BR_DONE;
     }
+    SASSERT(i < as.size());
     if (i == bs.size()) {
         expr_ref_vector es(m());
         for (unsigned j = i; j < as.size(); ++j) {
-            es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j]));
+            es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
         }
         result = mk_and(es);
         return BR_REWRITE3;
@@ -380,20 +521,10 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), a);
         return BR_REWRITE3;
     }
-    // concatenation is left-associative, so a2, b2 are not concatenations
-    expr* a1, *a2, *b1, *b2;
-    if (m_util.str.is_concat(a, a1, a2) && 
-        m_util.str.is_concat(b, b1, b2) && a2 == b2) {
-        result = m_util.str.mk_suffix(a1, b1);
-        return BR_REWRITE1;
-    }
-    if (m_util.str.is_concat(b, b1, b2) && b2 == a) {
-        result = m().mk_true();
-        return BR_DONE;
-    }
+
     bool isc1 = false;
     bool isc2 = false;
-    
+    expr* a1, *a2, *b1, *b2;
     if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
         isc1 = true;
     }
@@ -453,6 +584,37 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
             }            
         }
     }
+    expr_ref_vector as(m()), bs(m());
+    m_util.str.get_concat(a, as);
+    m_util.str.get_concat(b, bs);
+    bool change = false;
+    while (as.size() > 0 && bs.size() > 0 && as.back() == bs.back()) {
+        as.pop_back();
+        bs.pop_back();
+        change = true;
+    }
+    if (as.size() > 0 && bs.size() > 0 && m().is_value(as.back()) && m().is_value(bs.back())) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    if (change) {
+        // suffix("", bs) <- true
+        if (as.empty()) {
+            result = m().mk_true();
+            return BR_DONE;
+        }
+        // suffix(as, "") iff as = ""
+        if (bs.empty()) {            
+            for (unsigned j = 0; j < as.size(); ++j) {
+                bs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
+            }
+            result = mk_and(bs);
+            return BR_REWRITE3;
+        }
+        result = m_util.str.mk_suffix(m_util.str.mk_concat(as.size(), as.c_ptr()),
+                                     m_util.str.mk_concat(bs.size(), bs.c_ptr()));
+        return BR_DONE;
+    }
 
     return BR_FAILED;
 }
@@ -480,26 +642,190 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     }
     return BR_FAILED;
 }
+
+void seq_rewriter::add_next(u_map<expr*>& next, unsigned idx, expr* cond) {
+    expr* acc;
+    if (m().is_true(cond) || !next.find(idx, acc)) {              
+        next.insert(idx, cond);                   
+    }                                                   
+    else {                                              
+        next.insert(idx, m().mk_or(cond, acc));   
+    }
+}
+
+bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
+    zstring s;
+    ptr_vector<expr> todo;
+    expr *e1, *e2;
+    todo.push_back(e);
+    while (!todo.empty()) {
+        e = todo.back();
+        todo.pop_back();
+        if (m_util.str.is_string(e, s)) {
+            for (unsigned i = s.length(); i > 0; ) {
+                --i;
+                seq.push_back(m_util.str.mk_char(s, i));
+            }
+        }
+        else if (m_util.str.is_empty(e)) {
+            continue;
+        }
+        else if (m_util.str.is_unit(e)) {
+            seq.push_back(e);
+        }
+        else if (m_util.str.is_concat(e, e1, e2)) {
+            todo.push_back(e1);
+            todo.push_back(e2);
+        }
+        else {
+            return false;
+        }
+    }
+    seq.reverse();
+    return true;
+}
+
 br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
+    scoped_ptr<eautomaton> aut;
+    expr_ref_vector seq(m());
+    if (is_sequence(a, seq) && (aut = re2automaton(m())(b))) {
+        expr_ref_vector trail(m());
+        u_map<expr*> maps[2];
+        bool select_map = false;
+        expr_ref ch(m()), cond(m());
+        eautomaton::moves mvs;
+        maps[0].insert(aut->init(), m().mk_true());
+        // is_accepted(a, aut) & some state in frontier is final.
+
+        for (unsigned i = 0; i < seq.size(); ++i) {
+            u_map<expr*>& frontier = maps[select_map];
+            u_map<expr*>& next = maps[!select_map];
+            select_map = !select_map;
+            ch = seq[i].get();
+            next.reset();
+            u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
+            for (; it != end; ++it) {
+                mvs.reset();
+                unsigned state = it->m_key;
+                expr*    acc  = it->m_value;
+                aut->get_moves_from(state, mvs, false);
+                for (unsigned j = 0; j < mvs.size(); ++j) {
+                    eautomaton::move const& mv = mvs[j];
+                    if (m().is_value(mv.t()) && m().is_value(ch)) {
+                        if (mv.t() == ch) {
+                            add_next(next, mv.dst(), acc);
+                        }
+                        else {
+                            continue;
+                        }
+                    }
+                    else {
+                        cond = m().mk_eq(mv.t(), ch);
+                        if (!m().is_true(acc)) cond = m().mk_and(acc, cond);
+                        add_next(next, mv.dst(), cond);
+                    }
+                }                
+            }
+        }
+        u_map<expr*> const& frontier = maps[select_map];
+        u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
+        expr_ref_vector ors(m());
+        for (; it != end; ++it) {
+            unsigned_vector states;
+            bool has_final = false;
+            aut->get_epsilon_closure(it->m_key, states);
+            for (unsigned i = 0; i < states.size() && !has_final; ++i) {
+                has_final = aut->is_final_state(states[i]);
+            }
+            if (has_final) {
+                ors.push_back(it->m_value);
+            }
+        }
+        result = mk_or(ors);
+        return BR_REWRITE_FULL;
+    }
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
+    if (is_epsilon(a)) {
+        result = b;
+        return BR_DONE;
+    }
+    if (is_epsilon(b)) {
+        result = a;
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
+/*
+  (a + a) = a
+  (a + eps) = a
+  (eps + a) = a
+*/
 br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
+    if (a == b) {
+        result = a;
+        return BR_DONE;
+    }
+    if (m_util.re.is_star(a) && is_epsilon(b)) {
+        result = a;
+        return BR_DONE;
+    }
+    if (m_util.re.is_star(b) && is_epsilon(a)) {
+        result = b;
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
+/*
+  a** = a*
+  (a* + b)* = (a + b)*
+  (a + b*)* = (a + b)*
+  (a*b*)*   = (a + b)*
+*/
 br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
+    expr* b, *c, *b1, *c1;
+    if (m_util.re.is_star(a)) {
+        result = a;
+        return BR_DONE;
+    }
+    if (m_util.re.is_union(a, b, c)) {
+        if (m_util.re.is_star(b, b1)) {
+            result = m_util.re.mk_star(m_util.re.mk_union(b1, c));
+            return BR_REWRITE2;
+        }
+        if (m_util.re.is_star(c, c1)) {
+            result = m_util.re.mk_star(m_util.re.mk_union(b, c1));
+            return BR_REWRITE2;
+        }
+    }
+    if (m_util.re.is_concat(a, b, c) &&
+        m_util.re.is_star(b, b1) && m_util.re.is_star(c, c1)) {
+        result = m_util.re.mk_star(m_util.re.mk_union(b1, c1));
+        return BR_REWRITE2;
+    }
+
     return BR_FAILED;
 }
+
+/*
+   a+ = aa*
+*/
 br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
     return BR_FAILED;
+//  result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
+//  return BR_REWRITE2;
 }
+
 br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
-    return BR_FAILED;
+    sort* s;
+    VERIFY(m_util.is_re(a, s));
+    sort_ref seq(m_util.str.mk_seq(s), m());
+    result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(seq)), a);
+    return BR_REWRITE1;
 }
 
 br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
@@ -518,38 +844,33 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
     return BR_REWRITE3;
 }
 
-bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) {
+bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs) {
     expr* a, *b;
     zstring s;
     bool change = false;
-    expr_ref_vector trail(m());
-    m_lhs.reset();
-    m_rhs.reset();
-    m_util.str.get_concat(l, m_lhs);
-    m_util.str.get_concat(r, m_rhs);
  
     // solve from back
     while (true) {
-        while (!m_rhs.empty() && m_util.str.is_empty(m_rhs.back())) {
-            m_rhs.pop_back();
+        while (!rs.empty() && m_util.str.is_empty(rs.back())) {
+            rs.pop_back();
             change = true;
         }
-        while (!m_lhs.empty() && m_util.str.is_empty(m_lhs.back())) {
-            m_lhs.pop_back();
+        while (!ls.empty() && m_util.str.is_empty(ls.back())) {
+            ls.pop_back();
             change = true;
         }
-        if (m_lhs.empty() || m_rhs.empty()) {
+        if (ls.empty() || rs.empty()) {
             break;
         }
-        expr* l = m_lhs.back();
-        expr* r = m_rhs.back();
+        expr* l = ls.back();
+        expr* r = rs.back();
         if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
             std::swap(l, r);
-            std::swap(m_lhs, m_rhs);
+            ls.swap(rs);
         }
         if (l == r) {
-            m_lhs.pop_back();
-            m_rhs.pop_back();
+            ls.pop_back();
+            rs.pop_back();
         }
         else if(m_util.str.is_unit(l, a) &&
                 m_util.str.is_unit(r, b)) {
@@ -558,8 +879,8 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
             }
             lhs.push_back(a);
             rhs.push_back(b);
-            m_lhs.pop_back();
-            m_rhs.pop_back();
+            ls.pop_back();
+            rs.pop_back();
         }
         else if (m_util.str.is_unit(l, a) && m_util.str.is_string(r, s)) {
             SASSERT(s.length() > 0);
@@ -568,14 +889,13 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
             SASSERT(m().get_sort(ch) == m().get_sort(a));
             lhs.push_back(ch);
             rhs.push_back(a);
-            m_lhs.pop_back();
+            ls.pop_back();
             if (s.length() == 1) {
-                m_rhs.pop_back();
+                rs.pop_back();
             }
             else {
                 expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-2)), m());
-                m_rhs[m_rhs.size()-1] = s2;
-                trail.push_back(s2);
+                rs[rs.size()-1] = s2;
             }
         }
         else {
@@ -587,22 +907,22 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
     // solve from front
     unsigned head1 = 0, head2 = 0;
     while (true) {
-        while (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) {
+        while (head1 < ls.size() && m_util.str.is_empty(ls[head1].get())) {
             ++head1;
         }
-        while (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) {
+        while (head2 < rs.size() && m_util.str.is_empty(rs[head2].get())) {
             ++head2;
         }
-        if (head1 == m_lhs.size() || head2 == m_rhs.size()) {
+        if (head1 == ls.size() || head2 == rs.size()) {
             break;
         }
-        SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size());
+        SASSERT(head1 < ls.size() && head2 < rs.size());
 
-        expr* l = m_lhs[head1];
-        expr* r = m_rhs[head2];
+        expr* l = ls[head1].get();
+        expr* r = rs[head2].get();
         if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
             std::swap(l, r);
-            std::swap(m_lhs, m_rhs);
+            ls.swap(rs);
         }
         if (l == r) {
             ++head1;
@@ -624,14 +944,13 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
             SASSERT(m().get_sort(ch) == m().get_sort(a));
             lhs.push_back(ch);
             rhs.push_back(a);
-            m_lhs.pop_back();
+            ls.pop_back();
             if (s.length() == 1) {
-                m_rhs.pop_back();
+                rs.pop_back();
             }
             else {
                 expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m());
-                m_rhs[m_rhs.size()-1] = s2;
-                trail.push_back(s2);
+                rs[rs.size()-1] = s2;
             }            
         }
         else {
@@ -641,10 +960,10 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
     }
     // reduce strings
     zstring s1, s2;
-    while (head1 < m_lhs.size() && 
-           head2 < m_rhs.size() && 
-           m_util.str.is_string(m_lhs[head1], s1) &&
-           m_util.str.is_string(m_rhs[head2], s2)) {
+    while (head1 < ls.size() && 
+           head2 < rs.size() && 
+           m_util.str.is_string(ls[head1].get(), s1) &&
+           m_util.str.is_string(rs[head2].get(), s2)) {
         unsigned l = std::min(s1.length(), s2.length());
         for (unsigned i = 0; i < l; ++i) {
             if (s1[i] != s2[i]) {
@@ -655,68 +974,88 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
             ++head1;            
         }
         else {
-            m_lhs[head1] = m_util.str.mk_string(s1.extract(l, s1.length()-l));
-            trail.push_back(m_lhs[head1]);
+            ls[head1] = m_util.str.mk_string(s1.extract(l, s1.length()-l));
         }
         if (l == s2.length()) {
             ++head2;            
         }
         else {
-            m_rhs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l));
-            trail.push_back(m_rhs[head2]);
+            rs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l));
         }
         change = true;
     }
-    while (head1 < m_lhs.size() && 
-           head2 < m_rhs.size() &&
-           m_util.str.is_string(m_lhs.back(), s1) &&
-           m_util.str.is_string(m_rhs.back(), s2)) {
+    while (head1 < ls.size() && 
+           head2 < rs.size() &&
+           m_util.str.is_string(ls.back(), s1) &&
+           m_util.str.is_string(rs.back(), s2)) {
         unsigned l = std::min(s1.length(), s2.length());
         for (unsigned i = 0; i < l; ++i) {
             if (s1[s1.length()-i-1] != s2[s2.length()-i-1]) {
                 return false;
             }
         }
-        m_lhs.pop_back();          
-        m_rhs.pop_back();
+        ls.pop_back();          
+        rs.pop_back();
         if (l < s1.length()) {
-            m_lhs.push_back(m_util.str.mk_string(s1.extract(0, s1.length()-l)));
-            trail.push_back(m_lhs.back());
+            ls.push_back(m_util.str.mk_string(s1.extract(0, s1.length()-l)));
         }
         if (l < s2.length()) {
-            m_rhs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l)));
-            trail.push_back(m_rhs.back());
-        }
+            rs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l)));
+        }        
         change = true;
     }
 
     bool is_sat;
-    unsigned szl = m_lhs.size() - head1, szr = m_rhs.size() - head2;
-    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)) {
+    unsigned szl = ls.size() - head1, szr = rs.size() - head2;
+    expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2;
+    if (length_constrained(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
+        ls.reset(); rs.reset();
         return is_sat;
     }
-    if (is_subsequence(szl, ls, szr, rs, lhs, rhs, is_sat)) {
+    if (is_subsequence(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
+        ls.reset(); rs.reset();
         return is_sat;
     }
 
-	if (szl == 0 && szr == 0) {
-		return true;
-	}
+    if (szl == 0 && szr == 0) {
+        ls.reset(); rs.reset();
+        return true;
+    }
     else if (!change) {
-        lhs.push_back(l);
-        rhs.push_back(r);
+        // skip
+        SASSERT(lhs.empty());
     }
     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));
+        lhs.push_back(m_util.str.mk_concat(szl, ls.c_ptr() + head1));
+        rhs.push_back(m_util.str.mk_concat(szr, rs.c_ptr() + head2));
+        ls.reset();
+        rs.reset();
     }
+    SASSERT(lhs.empty() || ls.empty());
     return true;
 }
 
+bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) {
+    m_lhs.reset();
+    m_rhs.reset();
+    m_util.str.get_concat(l, m_lhs);
+    m_util.str.get_concat(r, m_rhs);
+    if (reduce_eq(m_lhs, m_rhs, lhs, rhs)) {
+        SASSERT(lhs.size() == rhs.size());
+        if (lhs.empty()) {
+            lhs.push_back(l);
+            rhs.push_back(r);
+        }
+        return true;
+    }
+    else {
+        TRACE("seq", tout << mk_pp(l, m()) << " != " << mk_pp(r, m()) << "\n";);
+        return false;
+    }
+}
+
 expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
     SASSERT(n > 0);
     ptr_vector<expr> bs;
@@ -812,6 +1151,11 @@ bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr
     return false;
 }
 
+bool seq_rewriter::is_epsilon(expr* e) const {
+    expr* e1;
+    return m_util.re.is_to_re(e, e1) && m_util.str.is_empty(e1);
+}
+
 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;

src/ast/rewriter/seq_rewriter.h

@@ -24,15 +24,27 @@ Notes:
 #include"rewriter_types.h"
 #include"params.h"
 #include"lbool.h"
+#include"automaton.h"
 
 
+typedef automaton<expr, ast_manager> eautomaton;
+class re2automaton {
+    ast_manager& m;
+    seq_util     u;       
+    eautomaton* re2aut(expr* e);
+    eautomaton* seq2aut(expr* e);
+ public:
+    re2automaton(ast_manager& m);
+    eautomaton* operator()(expr* e);
+};
+
 /**
    \brief Cheap rewrite rules for seq constraints
 */
 class seq_rewriter {
     seq_util       m_util;
     arith_util     m_autil;
-    ptr_vector<expr> m_es, m_lhs, m_rhs;
+    expr_ref_vector m_es, m_lhs, m_rhs;
 
     br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_length(expr* a, expr_ref& result);
@@ -61,9 +73,13 @@ class seq_rewriter {
     bool min_length(unsigned n, expr* const* es, unsigned& len);
     expr* concat_non_empty(unsigned n, expr* const* es);
 
+    void add_next(u_map<expr*>& next, unsigned idx, expr* cond);
+    bool is_sequence(expr* e, expr_ref_vector& seq);
+    bool is_epsilon(expr* e) const;
+
 public:    
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m), m_autil(m) {
+        m_util(m), m_autil(m), m_es(m), m_lhs(m), m_rhs(m) {
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
@@ -76,6 +92,8 @@ public:
 
     bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs);
 
+    bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
+
 };
 
 #endif

src/ast/seq_decl_plugin.cpp

@@ -25,7 +25,6 @@ Revision History:
 zstring::zstring(encoding enc): m_encoding(enc) {}
 
 zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
-    // TBD: epply decoding
     while (*s) {
         m_buffer.push_back(*s);
         ++s;
@@ -42,7 +41,7 @@ zstring::zstring(unsigned num_bits, bool const* ch) {
     m_encoding = (num_bits == 8)?ascii:unicode;
     unsigned n = 0;    
     for (unsigned i = 0; i < num_bits; ++i) {
-        n |= (((unsigned)ch[i]) << num_bits);
+        n |= (((unsigned)ch[i]) << i);
     }
     m_buffer.push_back(n);
 }
@@ -81,12 +80,23 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
     return result;
 }
 
+static char* esc_table[32] = { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N",
+                               "^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"};
+ 
 std::string zstring::encode() const {
-    // TBD apply encodings.
     SASSERT(m_encoding == ascii);
     std::ostringstream strm;
     for (unsigned i = 0; i < m_buffer.size(); ++i) {
-        strm << (char)(m_buffer[i]);
+        unsigned char ch = m_buffer[i];
+        if (0 <= ch && ch < 32) {
+            strm << esc_table[ch];
+        }
+        else if (ch == 127) {
+            strm << "^?";
+        }
+        else {
+            strm << (char)(ch);
+        }
     }
     return strm.str();
 }
@@ -163,6 +173,7 @@ std::ostream& zstring::operator<<(std::ostream& out) const {
 
 seq_decl_plugin::seq_decl_plugin(): m_init(false), 
                                     m_stringc_sym("String"),
+                                    m_charc_sym("Char"),
                                     m_string(0),
                                     m_char(0) {}
 
@@ -211,9 +222,9 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
 }
 
 /*
-  \brief match left associative operator.
+  \brief match right associative operator.
 */
-void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
+void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
     ptr_vector<sort> binding;
     ast_manager& m = *m_manager;
     TRACE("seq_verbose", 
@@ -369,7 +380,8 @@ void seq_decl_plugin::init() {
 
 void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
     decl_plugin::set_manager(m, id);
-    m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, _CHAR_SORT, 0, (parameter const*)0));
+    bv_util bv(*m);
+    m_char = bv.mk_sort(8);
     m->inc_ref(m_char);
     parameter param(m_char);
     m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, &param));
@@ -391,18 +403,18 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
             return m_string;
         }
         return m.mk_sort(symbol("Seq"), sort_info(m_family_id, SEQ_SORT, num_parameters, parameters));
-    case RE_SORT:
+    case RE_SORT: {
         if (num_parameters != 1) {
             m.raise_exception("Invalid regex sort, expecting one parameter");
         }
         if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) {
             m.raise_exception("invalid regex sort, parameter is not a sort");
         }
+        sort * s = to_sort(parameters[0].get_ast());
         return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
+    }
     case _STRING_SORT:
         return m_string;
-    case _CHAR_SORT:
-        return m_char;
     default:
         UNREACHABLE();
         return 0;
@@ -430,9 +442,9 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons
     if (arity == 0) {
         m.raise_exception("Invalid function application. At least one argument expected");
     }
-    match_left_assoc(*m_sigs[k], arity, domain, range, rng);
+    match_right_assoc(*m_sigs[k], arity, domain, range, rng);
     func_decl_info info(m_family_id, k_seq);
-    info.set_left_associative();
+    info.set_right_associative();
     return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info);    
 }
 
@@ -470,6 +482,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         }
         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");
@@ -583,7 +597,7 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
 app* seq_decl_plugin::mk_string(symbol const& s) {
     parameter param(s);
     func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
-                                   func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
+                                            func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
     return m_manager->mk_const(f);
 }
 
@@ -591,12 +605,16 @@ app* seq_decl_plugin::mk_string(zstring const& s) {
     symbol sym(s.encode().c_str());
     parameter param(sym);
     func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
-                                   func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
+                                            func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
     return m_manager->mk_const(f);
 }
 
+
 bool seq_decl_plugin::is_value(app* e) const {
-    return is_app_of(e, m_family_id, OP_STRING_CONST);
+    return 
+        is_app_of(e, m_family_id, OP_SEQ_EMPTY) || 
+        (is_app_of(e, m_family_id, OP_SEQ_UNIT) &&
+         m_manager->is_value(e->get_arg(0)));
 }
 
 app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
@@ -609,11 +627,26 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort
 app* seq_util::str::mk_string(zstring const& s) { return u.seq.mk_string(s); }
 
 
+
 app*  seq_util::str::mk_char(zstring const& s, unsigned idx) {
     bv_util bvu(m);
     return bvu.mk_numeral(s[idx], s.num_bits());
 }
 
+app*  seq_util::str::mk_char(char ch) {
+    zstring s(ch, zstring::ascii);
+    return mk_char(s, 0);
+}
+    
+bool seq_util::str::is_char(expr* n, zstring& c) const {
+    if (u.is_char(n)) {
+        c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());
+        return true;
+    }
+    else {
+        return false;
+    }
+}
 
 bool seq_util::str::is_string(expr const* n, zstring& s) const {
     if (is_string(n)) {
@@ -626,7 +659,7 @@ bool seq_util::str::is_string(expr const* n, zstring& s) const {
 }
 
 
-void seq_util::str::get_concat(expr* e, ptr_vector<expr>& es) const {
+void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {
     expr* e1, *e2;
     while (is_concat(e, e1, e2)) {
         get_concat(e1, es);

src/ast/seq_decl_plugin.h

@@ -22,13 +22,13 @@ Revision History:
 #define SEQ_DECL_PLUGIN_H_
 
 #include "ast.h"
+#include "bv_decl_plugin.h"
 
 
 enum seq_sort_kind {
     SEQ_SORT,
     RE_SORT,
-    _STRING_SORT,  // internal only
-    _CHAR_SORT     // internal only
+    _STRING_SORT  // internal only
 };
 
 enum seq_op_kind {
@@ -131,12 +131,13 @@ class seq_decl_plugin : public decl_plugin {
     ptr_vector<psig> m_sigs;
     bool             m_init;
     symbol           m_stringc_sym;
+    symbol           m_charc_sym;
     sort*            m_string;
     sort*            m_char;
 
     void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
 
-    void match_left_assoc(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
+    void match_right_assoc(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
 
     bool match(ptr_vector<sort>& binding, sort* s, sort* sP);
 
@@ -187,6 +188,7 @@ public:
 
     ast_manager& get_manager() const { return m; }
 
+    bool is_char(sort* s) const { return seq.is_char(s); }
     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); }
@@ -195,6 +197,7 @@ public:
     bool is_seq(sort* s, sort*& seq) { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
     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); }
+    bool is_char(expr* e) const { return is_char(m.get_sort(e)); }
 
     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); }
@@ -212,13 +215,13 @@ public:
         str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
 
         sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, &param); }
+        sort* mk_string_sort() { return m.mk_sort(m_fid, _STRING_SORT, 0, 0); }
         app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
         app* mk_string(zstring const& s);
         app* mk_string(symbol const& s) { return u.seq.mk_string(s); }
+        app* mk_char(char ch);
         app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
-        app* mk_concat(expr* a, expr* b, expr* c) {
-            return mk_concat(mk_concat(a, b), c);
-        }
+        app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(a, mk_concat(b, c)); }
         expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
         app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
         app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }
@@ -229,8 +232,6 @@ public:
         app* mk_unit(expr* u) { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); }
         app* mk_char(zstring const& s, unsigned idx);
 
-
-
         bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
 
         bool is_string(expr const* n, symbol& s) const {
@@ -238,6 +239,7 @@ public:
         }
         
         bool is_string(expr const* n, zstring& s) const;
+        bool is_char(expr* n, zstring& s) const;
 
         bool is_empty(expr const* n) const { symbol s; 
             return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); 
@@ -271,8 +273,9 @@ public:
         MATCH_BINARY(is_in_re);        
         MATCH_UNARY(is_unit);
 
-        void get_concat(expr* e, ptr_vector<expr>& es) const;
+        void get_concat(expr* e, expr_ref_vector& es) const;
         expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; }
+        expr* get_rightmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e2; return e; }
     };
 
     class re {
@@ -281,6 +284,8 @@ public:
     public:
         re(seq_util& u): m(u.m), m_fid(u.m_fid) {}
 
+        sort* mk_re(sort* seq) { parameter param(seq); return m.mk_sort(m_fid, RE_SORT, 1, &param); }
+
         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); }

src/math/automata/automaton.cpp

@@ -0,0 +1,23 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    automaton.cpp
+
+Abstract:
+
+    Symbolic Automaton, a la Margus Veanes Automata library.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-12-23.
+
+Revision History:
+
+
+--*/
+
+#include "automaton.h"
+
+template class automaton<unsigned>;

src/math/automata/automaton.h

@@ -0,0 +1,608 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    automaton.h
+
+Abstract:
+
+    Symbolic Automaton, a la Margus Veanes Automata library.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-12-23.
+
+Revision History:
+
+
+--*/
+
+#ifndef AUTOMATON_H_
+#define AUTOMATON_H_
+
+
+#include "util.h"
+#include "vector.h"
+#include "uint_set.h"
+
+template<class T>
+class default_value_manager {
+public:
+    void inc_ref(T* t) {}
+    void dec_ref(T* t) {}
+};
+
+template<class T, class M = default_value_manager<T> >
+class automaton {
+public:
+    class move {
+        M&       m;
+        T*       m_t;
+        unsigned m_src;
+        unsigned m_dst;        
+    public:
+        move(M& m, unsigned s, unsigned d, T* t = 0): m(m), m_t(t), m_src(s), m_dst(d) {
+            if (t) m.inc_ref(t);
+        }
+        ~move() {
+            if (m_t) m.dec_ref(m_t);
+        }
+
+        move(move const& other): m(other.m), m_t(other.m_t), m_src(other.m_src), m_dst(other.m_dst) {
+            if (m_t) m.inc_ref(m_t);
+        }
+
+        move& operator=(move const& other) {
+            SASSERT(&m == &other.m);
+            T* t = other.m_t;
+            if (t) m.inc_ref(t);
+            if (m_t) m.dec_ref(m_t);
+            m_t = t;
+            m_src = other.m_src;
+            m_dst = other.m_dst;
+            return *this;
+        }
+
+        unsigned dst() const { return m_dst; }
+        unsigned src() const { return m_src; }
+        T* t() const { return m_t; }
+
+        bool is_epsilon() const { return m_t == 0; }
+    };
+    typedef vector<move> moves;
+private:
+    M&              m;
+    vector<moves>   m_delta;
+    vector<moves>   m_delta_inv;
+    unsigned        m_init;
+    uint_set        m_final_set;
+    unsigned_vector m_final_states;
+    
+
+    // local data-structures
+    mutable uint_set        m_visited;
+    mutable unsigned_vector m_todo;
+
+    struct default_display {
+        std::ostream& display(std::ostream& out, T* t) {
+            return out << t;
+        }
+    };
+
+public:
+
+    // The empty automaton:
+    automaton(M& m):
+        m(m), 
+        m_init(0)
+    {
+        m_delta.push_back(moves());
+        m_delta_inv.push_back(moves());
+    }
+
+
+    // create an automaton from initial state, final states, and moves
+    automaton(M& m, unsigned init, unsigned_vector const& final, moves const& mvs): m(m) {
+        m_init = init;
+        for (unsigned i = 0; i < final.size(); ++i) {
+            add_to_final_states(final[i]);
+        }
+        for (unsigned i = 0; i < mvs.size(); ++i) {
+            move const& mv = mvs[i];
+            unsigned n = std::max(mv.src(), mv.dst());
+            if (n >= m_delta.size()) {
+                m_delta.resize(n+1, moves());
+                m_delta_inv.resize(n+1, moves());
+            }
+            add(mv);
+        }
+    }
+
+    // create an automaton that accepts a sequence.
+    automaton(M& m, ptr_vector<T> const& seq):
+        m(m),
+        m_init(0) {
+        m_delta.resize(seq.size()+1, moves());
+        m_delta_inv.resize(seq.size()+1, moves());
+        for (unsigned i = 0; i < seq.size(); ++i) {
+            m_delta[i].push_back(move(m, i, i + 1, seq[i]));
+            m_delta[i + 1].push_back(move(m, i, i + 1, seq[i]));
+        }
+        add_to_final_states(seq.size());
+    }
+
+    // The automaton that accepts t
+    automaton(M& m, T* t):
+        m(m), 
+        m_init(0) {
+        m_delta.resize(2, moves());
+        m_delta_inv.resize(2, moves());
+        add_to_final_states(1);
+        add(move(m, 0, 1, t));
+    }    
+
+    automaton(automaton const& other):
+        m(other.m), 
+        m_delta(other.m_delta),
+        m_delta_inv(other.m_delta_inv),        
+        m_init(other.m_init),
+        m_final_set(other.m_final_set),
+        m_final_states(other.m_final_states)
+    {}
+
+    // create the automaton that accepts the empty string only.
+    static automaton* mk_epsilon(M& m) {
+        moves mvs;
+        unsigned_vector final;
+        final.push_back(0);        
+        return alloc(automaton, m, 0, final, mvs);
+    }
+
+    // create the automaton with a single state on condition t.
+    static automaton* mk_loop(M& m, T* t) {
+        moves mvs;
+        unsigned_vector final;
+        final.push_back(0);       
+        mvs.push_back(move(m, 0, 0, t));
+        return alloc(automaton, m, 0, final, mvs);
+    }
+
+    // create the sum of disjoint automata
+    static automaton* mk_union(automaton const& a, automaton const& b) {
+        SASSERT(&a.m == &b.m);
+        M& m = a.m;
+        moves mvs;
+        unsigned_vector final;
+        unsigned offset1 = 1;
+        unsigned offset2 = a.num_states() + 1;
+        mvs.push_back(move(m, 0, a.init() + offset1));
+        mvs.push_back(move(m, 0, b.init() + offset2));
+        append_moves(offset1, a, mvs);
+        append_moves(offset2, b, mvs);
+        append_final(offset1, a, final);
+        append_final(offset2, b, final);
+        return alloc(automaton, m, 0, final, mvs);
+    }
+
+    static automaton* mk_opt(automaton const& a) {       
+        M& m = a.m;
+        moves mvs;
+        unsigned_vector final;
+        unsigned offset = 0;
+        unsigned init = a.init();
+        if (!a.initial_state_is_source()) {
+            offset = 1;
+            init = 0;
+            mvs.push_back(move(m, 0, a.init() + offset));
+        }
+        mvs.push_back(move(m, init, a.final_state() + offset));
+        append_moves(offset, a, mvs);
+        append_final(offset, a, final);
+        return alloc(automaton, m, init, final, mvs);        
+    }
+
+    // concatenate accepting languages
+    static automaton* mk_concat(automaton const& a, automaton const& b) {
+        SASSERT(&a.m == &b.m);
+        M& m = a.m;
+        moves mvs;
+        unsigned_vector final;
+        unsigned init = 0;
+        unsigned offset1 = 1;
+        unsigned offset2 = a.num_states() + offset1;
+        mvs.push_back(move(m, 0, a.init() + offset1));
+        append_moves(offset1, a, mvs);
+        for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
+            mvs.push_back(move(m, a.m_final_states[i] + offset1, b.init() + offset2));
+        }
+        append_moves(offset2, b, mvs);
+        append_final(offset2, b, final);
+        
+        return alloc(automaton, m, init, final, mvs);
+    }
+
+    static automaton* mk_reverse(automaton const& a) {
+        M& m = a.m;
+        if (a.is_empty()) {
+            return alloc(automaton, m);
+        }
+        moves mvs;
+        for (unsigned i = 0; i < a.m_delta.size(); ++i) {
+            moves const& mvs1 = a.m_delta[i];
+            for (unsigned j = 0; j < mvs1.size(); ++j) {
+                move const& mv = mvs1[j];
+                mvs.push_back(move(m, mv.dst(), mv.src(), mv.t()));
+            }
+        }
+        unsigned_vector final;
+        unsigned init;
+        final.push_back(a.init());
+        if (a.m_final_states.size() == 1) {
+            init = a.m_final_states[0];
+        }
+        else {
+            init = a.num_states();
+            for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
+                mvs.push_back(move(m, init, a.m_final_states[i]));
+            }
+        }
+        return alloc(automaton, m, init, final, mvs);        
+    }
+
+    void add_to_final_states(unsigned s) {
+        if (!is_final_state(s)) {
+            m_final_set.insert(s);
+            m_final_states.push_back(s);
+        }
+    }
+
+    void remove_from_final_states(unsigned s) {
+        if (is_final_state(s)) {
+            m_final_set.remove(s);
+            m_final_states.erase(s);
+        }
+    }
+
+    void add_init_to_final_states() {
+        add_to_final_states(init());
+    }
+
+    void add_final_to_init_moves() {
+        for (unsigned i = 0; i < m_final_states.size(); ++i) {
+            unsigned state = m_final_states[i];
+            bool found = false;
+            moves const& mvs = m_delta[state];
+            for (unsigned j = 0; found && j < mvs.size(); ++j) {
+                found = (mvs[j].dst() == m_init) && mvs[j].is_epsilon();
+            }
+            if (!found && state != m_init) {
+                add(move(m, state, m_init));
+            }
+        }
+    }
+
+    // remove epsilon transitions
+    // src - e -> dst
+    // in_degree(src) = 1, final(src) => final(dst), src0 != src
+    //    src0 - t -> src - e -> dst => src0 - t -> dst
+    // out_degree(dst) = 1, final(dst) => final(src), dst != dst1
+    //    src - e -> dst - t -> dst1 => src - t -> dst1
+
+    // Generalized: 
+    // Src - E -> dst - t -> dst1 => Src - t -> dst1   if dst is final => each Src is final
+    //
+    // src - e -> dst - ET -> Dst1 => src - ET -> Dst1  if in_degree(dst) = 1, src != dst
+    // Src - E -> dst - et -> dst1 => Src - et -> dst1  if out_degree(dst) = 1, src != dst
+    // 
+    void compress() {
+        for (unsigned i = 0; i < m_delta.size(); ++i) {
+            for (unsigned j = 0; j < m_delta[i].size(); ++j) {
+                move const& mv = m_delta[i][j];
+                unsigned src = mv.src();
+                unsigned dst = mv.dst();
+                SASSERT(src == i);
+                if (mv.is_epsilon()) {
+                    if (src == dst) {
+                        // just remove this edge.                        
+                    }
+                    else if (1 == in_degree(src) && 1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
+                        move const& mv0 = m_delta_inv[src][0];
+                        unsigned src0 = mv0.src();                        
+                        T* t = mv0.t();
+                        SASSERT(mv0.dst() == src);
+                        if (src0 == src) {
+                            continue;
+                        }
+                        add(move(m, src0, dst, t));
+                        remove(src0, src, t);
+
+                    }
+                    else if (1 == out_degree(dst) && 1 == in_degree(dst) && init() != dst && (!is_final_state(dst) || is_final_state(src))) {
+                        move const& mv1 = m_delta[dst][0];
+                        unsigned dst1 = mv1.dst();
+                        T* t = mv1.t();
+                        SASSERT(mv1.src() == dst);
+                        if (dst1 == dst) {
+                            continue;
+                        }
+                        add(move(m, src, dst1, t));
+                        remove(dst, dst1, t);
+                    }
+                    else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) {
+                        moves const& mvs = m_delta[dst];
+                        moves mvs1;
+                        for (unsigned k = 0; k < mvs.size(); ++k) {
+                            mvs1.push_back(move(m, src, mvs[k].dst(), mvs[k].t()));
+                        }
+                        for (unsigned k = 0; k < mvs1.size(); ++k) {
+                            remove(dst, mvs1[k].dst(), mvs1[k].t());
+                            add(mvs1[k]);
+                        }
+                    }
+                    //
+                    // Src - E -> dst - et -> dst1 => Src - et -> dst1  if out_degree(dst) = 1, src != dst
+                    //
+                    else if (1 == out_degree(dst) && all_epsilon_in(dst) && init() != dst && !is_final_state(dst)) {
+                        move const& mv = m_delta[dst][0];
+                        unsigned dst1 = mv.dst();
+                        T* t = mv.t();
+                        unsigned_vector src0s;
+                        moves const& mvs = m_delta_inv[dst];
+                        moves mvs1;
+                        for (unsigned k = 0; k < mvs.size(); ++k) {
+                            SASSERT(mvs[k].is_epsilon());
+                            mvs1.push_back(move(m, mvs[k].src(), dst1, t));
+                        }
+                        for (unsigned k = 0; k < mvs1.size(); ++k) {
+                            remove(mvs1[k].src(), dst, 0);
+                            add(mvs1[k]);
+                        }
+                        remove(dst, dst1, t);    
+                        --j;
+                        continue;
+                    }
+                    //
+                    // Src1 - ET -> src - e -> dst => Src1 - ET -> dst  if out_degree(src) = 1, src != init() 
+                    //
+                    else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
+                        moves const& mvs = m_delta_inv[src];
+                        moves mvs1;
+                        for (unsigned k = 0; k < mvs.size(); ++k) {
+                            mvs1.push_back(move(m, mvs[k].src(), dst, mvs[k].t()));
+                        }
+                        for (unsigned k = 0; k < mvs1.size(); ++k) {
+                            remove(mvs1[k].src(), src, mvs1[k].t());
+                            add(mvs1[k]);
+                        }
+                    }
+                    else {
+                        continue;
+                    }                    
+                    remove(src, dst, 0);
+                    --j;
+                }
+            }
+        }
+        while (true) {
+            SASSERT(!m_delta.empty());
+            unsigned src = m_delta.size() - 1;            
+            if (in_degree(src) == 0 && init() != src) {
+                remove_from_final_states(src);
+                m_delta.pop_back();
+            }
+            else {
+                break;
+            }
+        }
+    }
+
+    bool is_sequence(unsigned& length) const {
+        if (is_final_state(m_init) && (out_degree(m_init) == 0 || (out_degree(m_init) == 1 && is_loop_state(m_init)))) {
+            length = 0;
+            return true;
+        }
+        if (is_empty() || in_degree(m_init) != 0 || out_degree(m_init) != 1) {
+            return false;
+        }
+        
+        length = 1;
+        unsigned s = get_move_from(m_init).dst();
+        while (!is_final_state(s)) {  
+            if (out_degree(s) != 1 || in_degree(s) != 1) {
+                return false;
+            }
+            s = get_move_from(s).dst();
+            ++length;
+        }
+        return out_degree(s) == 0 || (out_degree(s) == 1 && is_loop_state(s));
+    }
+
+    unsigned init() const { return m_init; }
+    unsigned in_degree(unsigned state) const { return m_delta_inv[state].size(); }
+    unsigned out_degree(unsigned state) const { return m_delta[state].size(); }
+    move const& get_move_from(unsigned state) const { SASSERT(m_delta[state].size() == 1); return m_delta[state][0]; }
+    move const& get_move_to(unsigned state) const { SASSERT(m_delta_inv[state].size() == 1); return m_delta_inv[state][0]; }
+    moves const& get_moves_from(unsigned state) const { return m_delta[state]; }
+    moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; }
+    bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); }
+    bool is_final_state(unsigned s) const { return m_final_set.contains(s); }
+    bool is_epsilon_free() const {
+        for (unsigned i = 0; i < m_delta.size(); ++i) {
+            moves const& mvs = m_delta[i];
+            for (unsigned j = 0; j < mvs.size(); ++j) {
+                if (!mvs[j].t()) return false;
+            }
+        }
+        return true;
+    }
+
+    bool all_epsilon_in(unsigned s) {
+        moves const& mvs = m_delta_inv[s];
+        for (unsigned j = 0; j < mvs.size(); ++j) {
+            if (mvs[j].t()) return false;
+        }
+        return true;
+    }
+
+    bool is_empty() const { return m_final_states.empty(); }
+    unsigned final_state() const { return m_final_states[0]; }
+    bool has_single_final_sink() const { return m_final_states.size() == 1 && m_delta[final_state()].empty(); }
+    unsigned num_states() const { return m_delta.size(); }
+    bool is_loop_state(unsigned s) const {
+        moves mvs;
+        get_moves_from(s, mvs);
+        for (unsigned i = 0; i < mvs.size(); ++i) {
+            if (s == mvs[i].dst()) return true;
+        }
+        return false;
+    }
+
+    unsigned move_count() const {
+        unsigned result = 0;
+        for (unsigned i = 0; i < m_delta.size(); result += m_delta[i].size(), ++i) {}
+        return result;
+    }
+    void get_epsilon_closure(unsigned state, unsigned_vector& states) {
+        get_epsilon_closure(state, m_delta, states);
+    }
+    void get_inv_epsilon_closure(unsigned state, unsigned_vector& states) {
+        get_epsilon_closure(state, m_delta_inv, states);
+    }
+    void get_moves_from(unsigned state, moves& mvs, bool epsilon_closure = true) const {
+        get_moves(state, m_delta, mvs, epsilon_closure);
+    }
+    void get_moves_to(unsigned state, moves& mvs, bool epsilon_closure = true) {
+        get_moves(state, m_delta_inv, mvs, epsilon_closure);
+    }
+
+    template<class D = default_display>
+    std::ostream& display(std::ostream& out, D& displayer = D()) const {
+        out << "init: " << init() << "\n";
+        out << "final: ";
+        for (unsigned i = 0; i < m_final_states.size(); ++i) out << m_final_states[i] << " ";
+        out << "\n";
+        for (unsigned i = 0; i < m_delta.size(); ++i) {
+            moves const& mvs = m_delta[i];
+            for (unsigned j = 0; j < mvs.size(); ++j) {
+                move const& mv = mvs[j];
+                out << i << " -> " << mv.dst() << " ";
+                if (mv.t()) {
+                    out << "if "; 
+                    displayer.display(out, mv.t());
+                }
+                out << "\n";
+            }
+        }
+        return out;
+    }
+private:
+
+    void remove_dead_states() {
+        unsigned_vector remap;
+        for (unsigned i = 0; i < m_delta.size(); ++i) {
+            
+        }
+    }    
+
+
+    void add(move const& mv) {
+        m_delta[mv.src()].push_back(mv);
+        m_delta_inv[mv.dst()].push_back(mv);
+    }
+
+
+    unsigned find_move(unsigned src, unsigned dst, T* t, moves const& mvs) {
+        for (unsigned i = 0; i < mvs.size(); ++i) {
+            move const& mv = mvs[i];
+            if (mv.src() == src && mv.dst() == dst && t == mv.t()) {
+                return i;
+            }
+        }
+        UNREACHABLE();
+        return UINT_MAX;
+    }
+
+    void remove(unsigned src, unsigned dst, T* t, moves& mvs) {
+        remove(find_move(src, dst, t, mvs), mvs);
+    }
+
+    void remove(unsigned src, unsigned dst, T* t) {
+        remove(src, dst, t, m_delta[src]);
+        remove(src, dst, t, m_delta_inv[dst]);
+    }
+
+    void remove(unsigned index, moves& mvs) {
+        mvs[index] = mvs.back();
+        mvs.pop_back();
+    }     
+
+    mutable unsigned_vector m_states1, m_states2;
+    
+    void get_moves(unsigned state, vector<moves> const& delta, moves& mvs, bool epsilon_closure) const {
+        m_states1.reset(); 
+        m_states2.reset();
+        get_epsilon_closure(state, delta, m_states1);
+        for (unsigned i = 0; i < m_states1.size(); ++i) {
+            state = m_states1[i];
+            moves const& mv1 = delta[state];
+            for (unsigned j = 0; j < mv1.size(); ++j) {
+                move const& mv = mv1[j];
+                if (!mv.is_epsilon()) {
+                    if (epsilon_closure) {
+                        m_states2.reset();
+                        get_epsilon_closure(mv.dst(), delta, m_states2);
+                        for (unsigned k = 0; k < m_states2.size(); ++k) {
+                            mvs.push_back(move(m, state, m_states2[k], mv.t()));                            
+                        }
+                    }
+                    else {
+                        mvs.push_back(move(m, state, mv.dst(), mv.t()));
+                    }
+                }
+            }
+        }
+    }
+
+    void get_epsilon_closure(unsigned state, vector<moves> const& delta, unsigned_vector& states) const {
+        m_todo.push_back(state);
+        m_visited.insert(state);
+        while (!m_todo.empty()) {
+            state = m_todo.back();
+            states.push_back(state);
+            m_todo.pop_back();
+            moves const& mvs = delta[state];
+            for (unsigned i = 0; i < mvs.size(); ++i) {
+                unsigned tgt = mvs[i].dst();
+                if (mvs[i].is_epsilon() && !m_visited.contains(tgt)) {
+                    m_visited.insert(tgt);
+                    m_todo.push_back(tgt);
+                }
+            }
+        }
+        m_visited.reset();
+        SASSERT(m_todo.empty());   
+    }
+
+    static void append_moves(unsigned offset, automaton const& a, moves& mvs) {
+        for (unsigned i = 0; i < a.num_states(); ++i) {
+            moves const& mvs1 = a.m_delta[i];
+            for (unsigned j = 0; j < mvs1.size(); ++j) {
+                move const& mv = mvs1[j];
+                mvs.push_back(move(a.m, mv.src() + offset, mv.dst() + offset, mv.t()));
+            }
+        }
+    }
+
+    static void append_final(unsigned offset, automaton const& a, unsigned_vector& final) {
+        for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
+            final.push_back(a.m_final_states[i]+offset);
+        }
+    }
+ 
+};
+
+typedef automaton<unsigned> uautomaton;
+
+
+#endif 

src/muz/rel/dl_mk_simple_joins.cpp

@@ -302,8 +302,6 @@ namespace datalog {
         }
 
         void remove_rule_from_pair(app_pair key, rule * r, unsigned original_len) {
-            SASSERT(m_costs.contains(key));
-            SASSERT(m_costs.find(key));
             pair_info * ptr = 0;
             if (m_costs.find(key, ptr) && ptr &&
                 ptr->remove_rule(r, original_len)) {

src/parsers/smt2/smt2scanner.cpp

@@ -169,24 +169,16 @@ namespace smt2 {
             char c = curr();
             if (c == EOF) 
                 throw scanner_exception("unexpected end of string", m_line, m_spos);
-            if (c == '\"') {
+            if (c == '\n') {
+                new_line();
+            }
+            else if (c == '\"') {
                 next();
                 if (curr() != '\"') {
                     m_string.push_back(0);
                     return STRING_TOKEN;
                 }
             }
-            else if (c == '\n') {
-                new_line();
-            }
-            else if (c == '\\') {
-                next();
-                c = curr();
-                if (c == EOF) 
-                    throw scanner_exception("unexpected end of string", m_line, m_spos);
-                if (c != '\\' && c != '\"')
-                    throw scanner_exception("invalid escape sequence", m_line, m_spos);
-            }
             m_string.push_back(c);
             next();
         }

src/smt/smt_context.cpp

@@ -1382,7 +1382,8 @@ namespace smt {
             bool_var v = l.var();
             bool_var_data & d = get_bdata(v);
             lbool val  = get_assignment(v);
-            TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() << " " << l << "\n";);
+            TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() 
+                  << " tag: " << (d.is_eq()?"eq":"") << (d.is_theory_atom()?"th":"") << (d.is_quantifier()?"q":"") << " " << l << "\n";);
             SASSERT(val != l_undef);
             if (d.is_enode())
                 propagate_bool_var_enode(v);

src/smt/smt_model_generator.cpp

@@ -90,7 +90,9 @@ namespace smt {
                 sort * s      = m_manager.get_sort(r->get_owner());
                 model_value_proc * proc = 0;
                 if (m_manager.is_bool(s)) {
-                    SASSERT(m_context->get_assignment(r) == l_true || m_context->get_assignment(r) == l_false);
+                    CTRACE("func_interp_bug", m_context->get_assignment(r) == l_undef, 
+                           tout << mk_pp(r->get_owner(), m_manager) << "\n";);
+                    SASSERT(m_context->get_assignment(r) != l_undef);
                     if (m_context->get_assignment(r) == l_true)
                         proc = alloc(expr_wrapper_proc, m_manager.mk_true());
                     else
@@ -359,6 +361,7 @@ namespace smt {
                     }
                     else {
                         enode * child = d.get_enode();
+                        TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m_manager) << "): " << mk_pp(child->get_owner(), m_manager) << " " << mk_pp(child->get_root()->get_owner(), m_manager) << "\n";);
                         child = child->get_root();
                         app * val = 0;
                         m_root2value.find(child, val);

src/smt/smt_setup.cpp

@@ -815,7 +815,7 @@ namespace smt {
     }
 
     void setup::setup_seq() {
-        m_context.register_plugin(alloc(theory_seq_empty, m_manager));
+        m_context.register_plugin(alloc(theory_seq, m_manager));
     }
 
     void setup::setup_card() {

src/smt/theory_arith.h

@@ -1056,6 +1056,10 @@ namespace smt {
         // -----------------------------------
         virtual bool get_value(enode * n, expr_ref & r);
 
+        bool get_lower(enode* n, expr_ref& r);
+        bool get_upper(enode* n, expr_ref& r);
+        bool to_expr(inf_numeral const& val, bool is_int, expr_ref& r);
+
 
         // -----------------------------------
         //
@@ -1071,6 +1075,8 @@ namespace smt {
                           unsigned num_eqs, enode_pair const * eqs,
                           unsigned num_params, parameter* params);
         inf_eps_rational<inf_rational> conflict_minimize();
+
+
     private:
         virtual expr_ref mk_gt(theory_var v);
 

src/smt/theory_arith_aux.h

@@ -2157,6 +2157,7 @@ namespace smt {
         enode * r      = n->get_root();
         enode_vector::const_iterator it  = r->begin_parents();
         enode_vector::const_iterator end = r->end_parents();
+        TRACE("shared", tout << get_context().get_scope_level() << " " <<  v << " " << r->get_num_parents() << "\n";);
         for (; it != end; ++it) {
             enode * parent = *it;
             app *   o = parent->get_owner();

src/smt/theory_arith_core.h

@@ -3089,20 +3089,35 @@ namespace smt {
     // -----------------------------------
 
     template<typename Ext>
-    bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
-        theory_var v = n->get_th_var(get_id());
-        if (v == null_theory_var) {
-            // TODO: generate fresh value different from other get_value(v) for all v.
-            return false; 
+    bool theory_arith<Ext>::to_expr(inf_numeral const& val, bool is_int, expr_ref & r) {
+        if (val.get_infinitesimal().is_zero()) {            
+            numeral _val = val.get_rational();
+            r = m_util.mk_numeral(_val.to_rational(), is_int);
+            return true;
         }
-        inf_numeral const & val = get_value(v);
-        if (!val.get_infinitesimal().is_zero()) {
-            // TODO: add support for infinitesimals
+        else {
             return false;
         }
-        numeral _val = val.get_rational();
-        r = m_util.mk_numeral(_val.to_rational(), is_int(v));
-        return true;
+    }
+
+    template<typename Ext>
+    bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
+        theory_var v = n->get_th_var(get_id());
+        return v != null_theory_var && to_expr(get_value(v), is_int(v), r);
+    }
+
+    template<typename Ext>
+    bool theory_arith<Ext>::get_lower(enode * n, expr_ref & r) {        
+        theory_var v = n->get_th_var(get_id());
+        bound* b = (v == null_theory_var) ? 0 : lower(v);
+        return b && to_expr(b->get_value(), is_int(v), r);
+    }
+    
+    template<typename Ext>
+    bool theory_arith<Ext>::get_upper(enode * n, expr_ref & r) {        
+        theory_var v = n->get_th_var(get_id());
+        bound* b = (v == null_theory_var) ? 0 : upper(v);
+        return b && to_expr(b->get_value(), is_int(v), r);
     }
     
     // -----------------------------------

src/smt/theory_bv.cpp

@@ -424,6 +424,39 @@ namespace smt {
 
     };
 
+    void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) {
+        ++m_stats.m_num_eq_dynamic;
+        if (v1 > v2) {
+            std::swap(v1, v2);
+        }
+        unsigned sz = get_bv_size(v1);
+        ast_manager& m = get_manager();
+        context & ctx = get_context();
+        app* o1 = get_enode(v1)->get_owner();
+        app* o2 = get_enode(v2)->get_owner();
+        literal oeq = mk_eq(o1, o2, true);
+        TRACE("bv", 
+              tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " " 
+              << ctx.get_scope_level() << "\n";);
+        literal_vector eqs;
+        for (unsigned i = 0; i < sz; ++i) {
+            literal l1 = m_bits[v1][i];
+            literal l2 = m_bits[v2][i];
+            expr_ref e1(m), e2(m);
+            e1 = mk_bit2bool(o1, i);
+            e2 = mk_bit2bool(o2, i);
+            literal eq = mk_eq(e1, e2, true);
+            ctx.mk_th_axiom(get_id(),  l1, ~l2, ~eq);
+            ctx.mk_th_axiom(get_id(), ~l1,  l2, ~eq);
+            ctx.mk_th_axiom(get_id(),  l1,  l2,  eq);
+            ctx.mk_th_axiom(get_id(), ~l1, ~l2,  eq);
+            ctx.mk_th_axiom(get_id(), eq, ~oeq);
+            eqs.push_back(~eq);
+        }
+        eqs.push_back(oeq);
+        ctx.mk_th_axiom(get_id(), eqs.size(), eqs.c_ptr());
+    }
+
     void theory_bv::fixed_var_eh(theory_var v) {
         numeral val;
         bool r      = get_fixed_value(v, val);
@@ -443,7 +476,9 @@ namespace smt {
                           display_var(tout, v);
                           display_var(tout, v2););
                     m_stats.m_num_th2core_eq++;
-                    ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
+                    add_fixed_eq(v, v2);
+                    ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));                    
+                    m_fixed_var_table.insert(key, v2);
                 }
             }
             else {
@@ -1177,6 +1212,7 @@ namespace smt {
     }
 
     void theory_bv::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
+
         m_stats.m_num_bit2core++;
         context & ctx = get_context();
         SASSERT(ctx.get_assignment(antecedent) == l_true);
@@ -1192,6 +1228,12 @@ namespace smt {
         }
         else {
             ctx.assign(consequent, mk_bit_eq_justification(v1, v2, consequent, antecedent));
+            literal_vector lits;
+            lits.push_back(~consequent);
+            lits.push_back(antecedent);
+            lits.push_back(~mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false));
+            ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+     
             if (m_wpos[v2] == idx)
                 find_wpos(v2);
             // REMARK: bit_eq_justification is marked as a theory_bv justification.
@@ -1601,6 +1643,7 @@ namespace smt {
         st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
         st.update("bv bit2core", m_stats.m_num_bit2core);
         st.update("bv->core eq", m_stats.m_num_th2core_eq);
+        st.update("bv dynamic eqs", m_stats.m_num_eq_dynamic);
     }
 
 #ifdef Z3DEBUG

src/smt/theory_bv.h

@@ -34,6 +34,7 @@ namespace smt {
     
     struct theory_bv_stats {
         unsigned   m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
+        unsigned   m_num_eq_dynamic;
         void reset() { memset(this, 0, sizeof(theory_bv_stats)); }
         theory_bv_stats() { reset(); }
     };
@@ -124,8 +125,9 @@ namespace smt {
         typedef std::pair<numeral, unsigned> value_sort_pair;
         typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
         typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
-        value2var                m_fixed_var_table;
 
+        value2var                m_fixed_var_table;
+        
         literal_vector           m_tmp_literals;
         svector<var_pos>         m_prop_queue;
         bool                     m_approximates_large_bvs;
@@ -166,6 +168,7 @@ namespace smt {
         void find_wpos(theory_var v);
         friend class fixed_eq_justification;
         void fixed_var_eh(theory_var v);
+        void add_fixed_eq(theory_var v1, theory_var v2);
         bool get_fixed_value(theory_var v, numeral & result) const;
         void internalize_num(app * n);
         void internalize_add(app * n);

src/smt/theory_seq.h

@@ -25,15 +25,24 @@ Revision History:
 #include "th_rewriter.h"
 #include "ast_trail.h"
 #include "scoped_vector.h"
+#include "scoped_ptr_vector.h"
+#include "automaton.h"
+#include "seq_rewriter.h"
 
 namespace smt {
 
     class theory_seq : public theory {
-        typedef scoped_dependency_manager<enode_pair> enode_pair_dependency_manager;
-        typedef enode_pair_dependency_manager::dependency enode_pair_dependency;
-        
+        struct assumption {
+            enode* n1, *n2;
+            literal lit;
+            assumption(enode* n1, enode* n2): n1(n1), n2(n2), lit(null_literal) {}
+            assumption(literal lit): n1(0), n2(0), lit(lit) {}
+        };
+        typedef scoped_dependency_manager<assumption> dependency_manager;
+        typedef dependency_manager::dependency dependency;        
+
         typedef trail_stack<theory_seq> th_trail_stack;
-        typedef std::pair<expr*, enode_pair_dependency*> expr_dep;
+        typedef std::pair<expr*, dependency*> expr_dep;
         typedef obj_map<expr, expr_dep> eqdep_map_t; 
 
         // cache to track evaluations under equalities
@@ -52,27 +61,30 @@ namespace smt {
         class solution_map {
             enum map_update { INS, DEL };
             ast_manager&                      m;
-            enode_pair_dependency_manager&    m_dm;
+            dependency_manager&    m_dm;
             eqdep_map_t                       m_map;            
             eval_cache                        m_cache;
             expr_ref_vector                   m_lhs, m_rhs;
-            ptr_vector<enode_pair_dependency> m_deps;
+            ptr_vector<dependency> m_deps;
             svector<map_update>               m_updates;
             unsigned_vector                   m_limit;
 
-            void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d);
+            void add_trail(map_update op, expr* l, expr* r, dependency* d);
         public:
-            solution_map(ast_manager& m, enode_pair_dependency_manager& dm): 
+            solution_map(ast_manager& m, dependency_manager& dm): 
                 m(m),  m_dm(dm), m_cache(m), m_lhs(m), m_rhs(m) {}
-            bool empty() const { return m_map.empty(); }
-            void  update(expr* e, expr* r, enode_pair_dependency* d);
+            bool  empty() const { return m_map.empty(); }
+            void  update(expr* e, expr* r, dependency* d);
             void  add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); }
             bool  find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
-            expr* find(expr* e, enode_pair_dependency*& d);
-            void  cache(expr* e, expr* r, enode_pair_dependency* d);
-            void push_scope() { m_limit.push_back(m_updates.size()); }
-            void pop_scope(unsigned num_scopes);
-            void display(std::ostream& out) const;
+            expr* find(expr* e, dependency*& d);
+            expr* find(expr* e);
+            bool  is_root(expr* e) const;
+            void  cache(expr* e, expr* r, dependency* d);
+            void  reset_cache() { m_cache.reset(); }
+            void  push_scope() { m_limit.push_back(m_updates.size()); }
+            void  pop_scope(unsigned num_scopes);
+            void  display(std::ostream& out) const;
         };
 
         // Table of current disequalities
@@ -97,52 +109,235 @@ namespace smt {
         struct eq {
             expr_ref               m_lhs;
             expr_ref               m_rhs;
-            enode_pair_dependency* m_dep;
-            eq(expr_ref& l, expr_ref& r, enode_pair_dependency* d):
+            dependency*            m_dep;
+            eq(expr_ref& l, expr_ref& r, dependency* d):
                 m_lhs(l), m_rhs(r), m_dep(d) {}
             eq(eq const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {}
             eq& operator=(eq const& other) { m_lhs = other.m_lhs; m_rhs = other.m_rhs; m_dep = other.m_dep; return *this; }
         };
 
+            
+        // asserted or derived disqequality with dependencies
+        struct ne {
+            bool                   m_solved;
+            expr_ref               m_l, m_r;
+            expr_ref_vector        m_lhs;
+            expr_ref_vector        m_rhs;
+            literal_vector         m_lits;
+            dependency* m_dep;
+            ne(expr_ref& l, expr_ref& r):
+                m_solved(false), m_l(l), m_r(r), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(0) {
+                m_lhs.push_back(l);
+                m_rhs.push_back(r);
+            }
+            ne(ne const& other): 
+                m_solved(other.m_solved), m_l(other.m_l), m_r(other.m_r), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
+            ne& operator=(ne const& other) { 
+                m_solved = other.m_solved;
+                m_l = other.m_l;
+                m_r = other.m_r;
+                m_lhs.reset();  m_lhs.append(other.m_lhs);
+                m_rhs.reset();  m_rhs.append(other.m_rhs); 
+                m_lits.reset(); m_lits.append(other.m_lits); 
+                m_dep = other.m_dep; 
+                return *this; 
+            }            
+            bool is_solved() const { return m_solved; }
+        };
+
+        class pop_lit : public trail<theory_seq> { 
+            unsigned m_idx;
+            literal  m_lit;
+        public:
+            pop_lit(theory_seq& th, unsigned idx): m_idx(idx), m_lit(th.m_nqs[idx].m_lits.back()) {
+                th.m_nqs.ref(m_idx).m_lits.pop_back();
+            }
+            virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.push_back(m_lit); }
+        };
+        class push_lit : public trail<theory_seq> {
+            unsigned m_idx;
+        public:
+            push_lit(theory_seq& th, unsigned idx, literal lit): m_idx(idx) {
+                th.m_nqs.ref(m_idx).m_lits.push_back(lit);
+            }
+            virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.pop_back(); }
+        };  
+        class set_lit : public trail<theory_seq> {
+            unsigned m_idx;
+            unsigned m_i;
+            literal  m_lit;
+        public:
+            set_lit(theory_seq& th, unsigned idx, unsigned i, literal lit): 
+                m_idx(idx), m_i(i), m_lit(th.m_nqs[idx].m_lits[i]) {
+                th.m_nqs.ref(m_idx).m_lits[i] = lit;
+            }
+            virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits[m_i] = m_lit; }            
+        };
+
+        class solved_ne : public trail<theory_seq> {
+            unsigned m_idx;
+        public:
+            solved_ne(theory_seq& th, unsigned idx) : m_idx(idx) { th.m_nqs.ref(idx).m_solved = true; }
+            virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_solved = false;  }
+        };
+        void mark_solved(unsigned idx);
+
+        class push_ne : public trail<theory_seq> {
+            unsigned m_idx;
+        public:
+            push_ne(theory_seq& th, unsigned idx, expr* l, expr* r) : m_idx(idx) {
+                th.m_nqs.ref(m_idx).m_lhs.push_back(l);
+                th.m_nqs.ref(m_idx).m_rhs.push_back(r);
+            }
+            virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_lhs.pop_back(); th.m_nqs.ref(m_idx).m_rhs.pop_back(); }
+        };
+
+        class pop_ne : public trail<theory_seq> {
+            expr_ref m_lhs;
+            expr_ref m_rhs;
+            unsigned m_idx;
+        public:
+            pop_ne(theory_seq& th, unsigned idx): 
+                m_lhs(th.m_nqs[idx].m_lhs.back(), th.m),
+                m_rhs(th.m_nqs[idx].m_rhs.back(), th.m),
+                m_idx(idx) {
+                th.m_nqs.ref(idx).m_lhs.pop_back();
+                th.m_nqs.ref(idx).m_rhs.pop_back();
+            }
+            virtual void undo(theory_seq& th) { 
+                th.m_nqs.ref(m_idx).m_lhs.push_back(m_lhs);
+                th.m_nqs.ref(m_idx).m_rhs.push_back(m_rhs); 
+                m_lhs.reset();
+                m_rhs.reset();
+            }
+        };
+
+        class set_ne : public trail<theory_seq> {
+            expr_ref m_lhs;
+            expr_ref m_rhs;
+            unsigned m_idx;
+            unsigned m_i;
+        public:
+            set_ne(theory_seq& th, unsigned idx, unsigned i, expr* l, expr* r): 
+                m_lhs(th.m_nqs[idx].m_lhs[i], th.m),
+                m_rhs(th.m_nqs[idx].m_rhs[i], th.m),
+                m_idx(idx),
+                m_i(i) {
+                th.m_nqs.ref(idx).m_lhs[i] = l;
+                th.m_nqs.ref(idx).m_rhs[i] = r;
+            }
+            virtual void undo(theory_seq& th) { 
+                th.m_nqs.ref(m_idx).m_lhs[m_i] = m_lhs;
+                th.m_nqs.ref(m_idx).m_rhs[m_i] = m_rhs;
+                m_lhs.reset();
+                m_rhs.reset();
+            }
+        };
+
+        class push_dep : public trail<theory_seq> {
+            dependency* m_dep;
+            unsigned m_idx;
+        public:
+            push_dep(theory_seq& th, unsigned idx, dependency* d): m_dep(th.m_nqs[idx].m_dep), m_idx(idx) {
+                th.m_nqs.ref(idx).m_dep = d;
+            }
+            virtual void undo(theory_seq& th) {
+                th.m_nqs.ref(m_idx).m_dep = m_dep;
+            }
+        };
+
+        class apply {
+        public:
+            virtual ~apply() {}
+            virtual void operator()(theory_seq& th) = 0;
+        };
+
+        class replay_length_coherence : public apply {
+            expr_ref m_e;
+        public:
+            replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
+            virtual void operator()(theory_seq& th) {
+                th.check_length_coherence(m_e);
+            }
+        };
+
+        class replay_axiom : public apply {
+            expr_ref m_e;
+        public:
+            replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
+            virtual void operator()(theory_seq& th) {
+                th.enque_axiom(m_e);
+            }
+        };
+
+        class push_replay : public trail<theory_seq> {
+            apply* m_apply;
+        public:
+            push_replay(apply* app): m_apply(app) {}
+            virtual void undo(theory_seq& th) {
+                th.m_replay.push_back(m_apply);
+            }
+        };
+
+        void erase_index(unsigned idx, unsigned i);
+
         struct stats {
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(stats)); }
             unsigned m_num_splits;
             unsigned m_num_reductions;
+            unsigned m_propagate_automata;
+            unsigned m_check_length_coherence;
+            unsigned m_branch_variable;
+            unsigned m_solve_nqs;
+            unsigned m_solve_eqs;
+            unsigned m_add_axiom;
         };
-        ast_manager&                        m;
-        enode_pair_dependency_manager       m_dm;
-        solution_map                        m_rep;        // unification representative.
-        scoped_vector<eq>                   m_eqs;        // set of current equations.
+        ast_manager&               m;
+        dependency_manager         m_dm;
+        solution_map               m_rep;        // unification representative.
+        scoped_vector<eq>          m_eqs;        // set of current equations.
+        scoped_vector<ne>          m_nqs;        // set of current disequalities.
 
-        seq_factory*    m_factory;               // value factory
-        expr_ref_vector m_ineqs;                 // inequalities to check solution against
-        exclusion_table m_exclude;               // set of asserted disequalities.
-        expr_ref_vector m_axioms;                // list of axioms to add.
-        unsigned        m_axioms_head;           // index of first axiom to add.
-        unsigned        m_branch_variable_head;  // index of first equation to examine.
-        bool            m_incomplete;            // is the solver (clearly) incomplete for the fragment.
-        bool            m_has_length;            // is length applied
-        bool            m_model_completion;      // during model construction, invent values in canonizer
-        th_rewriter     m_rewrite;
-        seq_util        m_util;
-        arith_util      m_autil;
-        th_trail_stack  m_trail_stack;
-        stats           m_stats;
-        symbol          m_prefix_sym;
-        symbol          m_suffix_sym;
-        symbol          m_contains_left_sym;
-        symbol          m_contains_right_sym;
-        symbol          m_left_sym;               // split variable left part
-        symbol          m_right_sym;              // split variable right part
+        seq_factory*               m_factory;    // value factory
+        exclusion_table            m_exclude;    // set of asserted disequalities.
+        expr_ref_vector            m_axioms;     // list of axioms to add.
+        obj_hashtable<expr>        m_axiom_set;
+        unsigned                   m_axioms_head; // index of first axiom to add.
+        unsigned        m_branch_variable_head;   // index of first equation to examine.
+        bool            m_incomplete;             // is the solver (clearly) incomplete for the fragment.
+        obj_hashtable<expr> m_length;             // is length applied
+        scoped_ptr_vector<apply> m_replay;        // set of actions to replay
+        model_generator* m_mg;
+        th_rewriter      m_rewrite;
+        seq_util         m_util;
+        arith_util       m_autil;
+        th_trail_stack   m_trail_stack;
+        stats            m_stats;
+        symbol           m_prefix, m_suffix, m_contains_left, m_contains_right, m_accept, m_reject;
+        symbol           m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
+        symbol           m_extract_prefix, m_at_left, m_at_right;
+        ptr_vector<expr> m_todo;
+        expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
+
+        // maintain automata with regular expressions.
+        scoped_ptr_vector<eautomaton>  m_automata;
+        obj_map<expr, eautomaton*>     m_re2aut;
+
+        // queue of asserted atoms
+        ptr_vector<expr>               m_atoms;
+        unsigned_vector                m_atoms_lim;
+        unsigned                       m_atoms_qhead;
+        bool                           m_new_solution;     // new solution added
+        bool                           m_new_propagation;  // new propagation to core
 
         virtual final_check_status final_check_eh();
-        virtual bool internalize_atom(app*, bool);
+        virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
         virtual bool internalize_term(app*);
-        virtual void internalize_eq_eh(app * atom, bool_var v);
+        virtual void internalize_eq_eh(app * atom, bool_var v) {}
         virtual void new_eq_eh(theory_var, theory_var);
         virtual void new_diseq_eh(theory_var, theory_var);
-        virtual void assign_eq(bool_var v, bool is_true);        
+        virtual void assign_eh(bool_var v, bool is_true);        
         virtual bool can_propagate();
         virtual void propagate();
         virtual void push_scope_eh();
@@ -159,40 +354,56 @@ namespace smt {
         virtual void init_model(model_generator & mg);
 
         // final check 
-        bool check_ineqs();              // check if inequalities are violated.
         bool simplify_and_solve_eqs();   // solve unitary equalities
         bool branch_variable();          // branch on a variable
         bool split_variable();           // split a variable
         bool is_solved(); 
-        bool check_length_coherence();  
-        bool check_length_coherence_tbd();  
-        bool check_ineq_coherence(); 
+        bool check_length_coherence();
+        bool check_length_coherence(expr* e);
+        bool propagate_length_coherence(expr* e);  
 
-        bool pre_process_eqs(bool simplify_or_solve);
-        bool simplify_eqs();
-        bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep);
-        bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep);
-        bool solve_basic_eqs();
+        bool solve_eqs(unsigned start);
+        bool solve_eq(expr* l, expr* r, dependency* dep);
+        bool simplify_eq(expr* l, expr* r, dependency* dep);
+        bool solve_unit_eq(expr* l, expr* r, dependency* dep);
+        bool is_binary_eq(expr* l, expr* r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr*& y);
+        bool solve_binary_eq(expr* l, expr* r, dependency* dep);
+        bool propagate_max_length(expr* l, expr* r, dependency* dep);
+
+        bool solve_nqs(unsigned i);
+        void solve_ne(unsigned i);
+        bool unchanged(expr* e, expr_ref_vector& es) const { return es.size() == 1 && es[0] == e; }
+        bool unchanged(expr* e, expr_ref_vector& es, expr* f, expr_ref_vector& fs) const { 
+            return 
+                (unchanged(e, es) && unchanged(f, fs)) ||
+                (unchanged(e, fs) && unchanged(e, fs));
+        }
 
         // asserting consequences
-        void propagate_lit(enode_pair_dependency* dep, literal lit);
-        void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2);
-        void propagate_eq(bool_var v, expr* e1, expr* e2);
-        void set_conflict(enode_pair_dependency* dep);
+        void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
+        void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
+        void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
+        void propagate_eq(dependency* dep, enode* n1, enode* n2);
+        void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
+        void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
 
-        bool find_branch_candidate(expr* l, ptr_vector<expr> const& rs);
-        bool assume_equality(expr* l, expr* r);
+        bool find_branch_candidate(dependency* dep, expr* l, expr_ref_vector const& rs);
+        lbool assume_equality(expr* l, expr* r);
 
         // variable solving utilities
         bool occurs(expr* a, expr* b);
         bool is_var(expr* b);
-        void add_solution(expr* l, expr* r, enode_pair_dependency* dep);
-        bool is_left_select(expr* a, expr*& b);
-        bool is_right_select(expr* a, expr*& b);
-        expr_ref canonize(expr* e, enode_pair_dependency*& eqs);
-        expr_ref expand(expr* e, enode_pair_dependency*& eqs);
-        void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b);
+        bool add_solution(expr* l, expr* r, dependency* dep);
+        bool is_nth(expr* a) const;
+        bool is_tail(expr* a, expr*& s, unsigned& idx) const;
+        expr_ref mk_nth(expr* s, expr* idx);
+        expr_ref mk_last(expr* e);
+        expr_ref canonize(expr* e, dependency*& eqs);
+        void canonize(expr* e, expr_ref_vector& es, dependency*& eqs);
+        expr_ref expand(expr* e, dependency*& eqs);
+        void add_dependency(dependency*& dep, enode* a, enode* b);
 
+        void get_concat(expr* e, ptr_vector<expr>& concats);
     
         // terms whose meaning are encoded using axioms.
         void enque_axiom(expr* e);
@@ -202,28 +413,80 @@ namespace smt {
         void add_replace_axiom(expr* e);
         void add_extract_axiom(expr* e);
         void add_length_axiom(expr* n);
-        void add_length_unit_axiom(expr* n);
-        void add_length_empty_axiom(expr* n);
-        void add_length_concat_axiom(expr* n);
-        void add_length_string_axiom(expr* n);
+
+        bool has_length(expr *e) const { return m_length.contains(e); }
+        void add_length(expr* e);
+        void enforce_length(enode* n);
+        void enforce_length_coherence(enode* n1, enode* n2);
+
         void add_elim_string_axiom(expr* n);
         void add_at_axiom(expr* n);
+        void add_in_re_axiom(expr* n);
         literal mk_literal(expr* n);
+        literal mk_eq_empty(expr* n);
+        literal mk_equals(expr* a, expr* b);
         void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
-        expr* mk_sub(expr* a, expr* b);
+        expr_ref mk_sub(expr* a, expr* b);
         enode* ensure_enode(expr* a);
 
+        // arithmetic integration
+        bool lower_bound(expr* s, rational& lo);
+        bool upper_bound(expr* s, rational& hi);
+        bool get_length(expr* s, rational& val);
+
+        void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
         expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0);
+        bool is_skolem(symbol const& s, expr* e) const;
 
         void set_incomplete(app* term);
 
+        // automata utilities
+        void propagate_in_re(expr* n, bool is_true);
+        eautomaton* get_automaton(expr* e);
+        literal mk_accept(expr* s, expr* idx, expr* re, expr* state);
+        literal mk_accept(expr* s, expr* idx, expr* re, unsigned i) { return mk_accept(s, idx, re, m_autil.mk_int(i)); }
+        bool is_accept(expr* acc) const {  return is_skolem(m_accept, acc); }
+        bool is_accept(expr* acc, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
+            return is_acc_rej(m_accept, acc, s, idx, re, i, aut);
+        }
+        literal mk_reject(expr* s, expr* idx, expr* re, expr* state);
+        literal mk_reject(expr* s, expr* idx, expr* re, unsigned i) { return mk_reject(s, idx, re, m_autil.mk_int(i)); }
+        bool is_reject(expr* rej) const {  return is_skolem(m_reject, rej); }
+        bool is_reject(expr* rej, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
+            return is_acc_rej(m_reject, rej, s, idx, re, i, aut);
+        }
+        bool is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut);
+        expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t);
+        bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
+        bool is_step(expr* e) const;
+        void propagate_step(literal lit, expr* n);
+        bool add_reject2reject(expr* rej);
+        bool add_accept2step(expr* acc);       
+        bool add_step2accept(expr* step);
+        bool add_prefix2prefix(expr* e);
+        bool add_suffix2suffix(expr* e);
+        bool add_contains2contains(expr* e);
+        void ensure_nth(literal lit, expr* s, expr* idx);
+        bool canonizes(bool sign, expr* e);
+        void propagate_non_empty(literal lit, expr* s);
+        void propagate_is_conc(expr* e, expr* conc);
+        void propagate_acc_rej_length(literal lit, expr* acc_rej);
+        bool propagate_automata();
+        void add_atom(expr* e);
+        void new_eq_eh(dependency* dep, enode* n1, enode* n2);
+
         // diagnostics
         void display_equations(std::ostream& out) const;
-        void display_deps(std::ostream& out, enode_pair_dependency* deps) const;
+        void display_disequations(std::ostream& out) const;
+        void display_disequation(std::ostream& out, ne const& e) const;
+        void display_deps(std::ostream& out, dependency* deps) const;
     public:
         theory_seq(ast_manager& m);
         virtual ~theory_seq();
 
+        // model building
+        app* mk_value(app* a);
+
     };
 };
 

src/smt/theory_seq_empty.h

@@ -30,6 +30,7 @@ namespace smt {
         seq_util     u;
         symbol_set   m_strings;
         unsigned     m_next;
+        char         m_char;
         std::string  m_unique_prefix;
         obj_map<sort, expr*> m_unique_sequences;
         expr_ref_vector m_trail;
@@ -41,6 +42,7 @@ namespace smt {
             m_model(md),
             u(m),
             m_next(0),
+            m_char(0),
             m_unique_prefix("#B"),
             m_trail(m)
         {
@@ -99,6 +101,11 @@ namespace smt {
                 expr* v0 = get_fresh_value(seq);
                 return u.re.mk_to_re(v0);
             }
+            if (u.is_char(s)) {
+                //char s[2] = { ++m_char, 0 };
+                //return u.str.mk_char(zstring(s), 0);
+                return u.str.mk_char(zstring("a"), 0);
+            }
             NOT_IMPLEMENTED_YET();
             return 0;
         }

src/tactic/bv/bit_blaster_tactic.h

@@ -1,32 +1,33 @@
-/*++
+ /*++
 Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
+ 
+ Module Name:
+ 
     bit_blaster_tactic.h
-
-Abstract:
-
+ 
+ Abstract:
+ 
     Apply bit-blasting to a given goal.
-
-Author:
-
+ 
+ Author:
+ 
     Leonardo (leonardo) 2011-10-25
-
-Notes:
-
---*/
+ 
+ Notes:
+ 
+ --*/
 #ifndef BIT_BLASTER_TACTIC_H_
 #define BIT_BLASTER_TACTIC_H_
-
-#include"params.h"
-#include"bit_blaster_rewriter.h"
-class ast_manager;
-class tactic;
-
+ 
+ #include"params.h"
+ #include"bit_blaster_rewriter.h"
+ class ast_manager;
+ class tactic;
+ 
 tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p = params_ref());
 tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p = params_ref());
-/*
+ /*
   ADD_TACTIC("bit-blast", "reduce bit-vector expressions into SAT.", "mk_bit_blaster_tactic(m, p)")
-*/
-#endif
+ */
+ #endif
+

src/tactic/core/solve_eqs_tactic.cpp

@@ -22,7 +22,7 @@ Revision History:
 #include"occurs.h"
 #include"cooperate.h"
 #include"goal_shared_occs.h"
-#include"ast_smt2_pp.h"
+#include"ast_pp.h"
 
 class solve_eqs_tactic : public tactic {
     struct imp {
@@ -92,21 +92,23 @@ class solve_eqs_tactic : public tactic {
         }
         
         // Use: (= x def) and (= def x)
-        bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
+
+        bool trivial_solve1(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) { 
+
             if (is_uninterp_const(lhs) && !m_candidate_vars.is_marked(lhs) && !occurs(lhs, rhs) && check_occs(lhs)) {
                 var = to_app(lhs); 
                 def = rhs;
                 pr  = 0;
                 return true;
             }
-            else if (is_uninterp_const(rhs) && !m_candidate_vars.is_marked(rhs) && !occurs(rhs, lhs) && check_occs(rhs)) {
-                var = to_app(rhs);
-                def = lhs;
-                if (m_produce_proofs)
-                    pr = m().mk_commutativity(m().mk_eq(lhs, rhs));
-                return true;
+            else {
+                return false;
             }
-            return false;
+        }
+        bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
+            return 
+                trivial_solve1(lhs, rhs, var, def, pr) ||
+                trivial_solve1(rhs, lhs, var, def, pr);
         }
         
         // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))

src/tactic/smtlogics/quant_tactics.cpp

@@ -102,7 +102,8 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
                            or_else(try_for(mk_smt_tactic(), 100), 
                                    try_for(qe::mk_sat_tactic(m), 1000), 
                                    try_for(mk_smt_tactic(), 1000),
-                                   and_then(mk_qe_tactic(m), mk_smt_tactic())));
+                                   and_then(mk_qe_tactic(m), mk_smt_tactic())
+                                   ));
 
     st->updt_params(p);
     return st;

src/util/ref_vector.h

@@ -89,9 +89,10 @@ public:
         m_nodes.shrink(sz);
     }
 
-    void push_back(T * n) {
+    ref_vector_core& push_back(T * n) {
         inc_ref(n);
         m_nodes.push_back(n);
+        return *this;
     }
 
     void pop_back() {

src/util/scoped_ptr_vector.h

@@ -30,6 +30,7 @@ public:
     ~scoped_ptr_vector() { reset(); }
     void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc<T>()); m_vector.reset(); }
     void push_back(T * ptr) { m_vector.push_back(ptr); }
+    void pop_back() { SASSERT(!empty()); set(size()-1, 0); m_vector.pop_back(); }
     T * operator[](unsigned idx) const { return m_vector[idx]; }
     void set(unsigned idx, T * ptr) { 
         if (m_vector[idx] == ptr) 

src/util/scoped_vector.h

@@ -46,7 +46,7 @@ public:
         m_elems_lim.push_back(m_elems_start);
     }
 
-    void pop_scopes(unsigned num_scopes) {
+    void pop_scope(unsigned num_scopes) {
         if (num_scopes == 0) return;
         unsigned new_size = m_sizes.size() - num_scopes;
         unsigned src_lim = m_src_lim[new_size];
@@ -72,6 +72,12 @@ public:
         return m_elems[m_index[idx]];
     }
 
+    // breaks abstraction, caller must ensure backtracking.
+    T& ref(unsigned idx) {
+        SASSERT(idx < m_size);
+        return m_elems[m_index[idx]];
+    }
+
     void set(unsigned idx, T const& t) {
         SASSERT(idx < m_size);
         unsigned n = m_index[idx];
@@ -102,6 +108,13 @@ public:
         SASSERT(invariant());
     }
 
+    void erase_and_swap(unsigned i) {
+        if (i + 1 < size()) {
+            set(i, m_elems[m_index[size()-1]]);
+        }
+        pop_back();
+    }
+
     unsigned size() const { return m_size; }
     
     bool empty() const { return m_size == 0; }