seq + API

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

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>
@@ -4872,6 +4908,7 @@ namespace Microsoft.Z3
             m_boolSort = null;
             m_intSort = null;
             m_realSort = null;
+            m_stringSort = null;
         }
         #endregion
     }

src/api/java/Context.java

@@ -1849,6 +1849,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.NativeObject));
+    }
+
+    /**
+     * Create the singleton sequence.
+     */
+    public SeqExpr MkUnit(Expr elem) 
+    {
+	checkContextMatch(elem);
+	return new SeqExpr(this, Native.mkSeqUnit(nCtx, elem.NativeObject));
+    }
+    
+    /**
+     * Create a string constant.
+     */
+    public SeqExpr MkString(string s) 
+    {
+	return new SeqExpr(this, Native.mkString(nCtx, s));
+    }
+    
+    /**
+     * Concatentate sequences.
+     */
+    public SeqExpr MkConcat(params SeqExpr[] t)
+    {
+	checkContextMatch(t);
+	return new SeqExpr(this, Native.mkSeqConcat(nCtx, (uint)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.NativeObject));
+    }
+    
+    /**
+     * Check for sequence prefix.
+     */
+    public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2) 
+    {
+	checkContextMatch(s1, s2);
+	return new BoolExpr(this, Native.mkSeqPrefix(nCtx, s1.NativeObject, s2.NativeObject));
+    }
+    
+    /**
+     * Check for sequence suffix.
+     */
+    public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2) 
+    {
+	checkContextMatch(s1, s2);
+	return new BoolExpr(this, Native.mkSeqSuffix(nCtx, s1.NativeObject, s2.NativeObject));
+    }
+    
+    /**
+     * 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.NativeObject, s2.NativeObject));
+    }
+    
+    /**
+     * 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.NativeObject, index.NativeObject));
+    }
+    
+    /**
+     * Extract subsequence.
+     */
+    public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
+    {
+	checkContextMatch(s, offset, length);
+	return new SeqExpr(this, Native.mkSeqExtract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
+    }
+    
+    /**
+     * 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.NativeObject, substr.NativeObject, offset.NativeObject));
+    }
+    
+    /**
+     * 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.NativeObject, src.NativeObject, dst.NativeObject));
+    }
+    
+    /**
+     * Convert a regular expression that accepts sequence s.
+     */
+    public ReExpr MkToRe(SeqExpr s) 
+    {
+	checkContextMatch(s);
+	return new ReExpr(this, Native.mkSeqToRe(nCtx, s.NativeObject));            
+    }
+    
+    
+    /**
+     * Check for regular expression membership.
+     */
+    public BoolExpr MkInRe(SeqExpr s, ReExpr re)
+    {
+	checkContextMatch(s, re);
+	return new BoolExpr(this, Native.mkSeqInRe(nCtx, s.NativeObject, re.NativeObject));            
+    }
+    
+    /**
+     * Take the Kleene star of a regular expression.
+     */
+    public ReExpr MkStar(ReExpr re)
+    {
+	checkContextMatch(re);
+	return new ReExpr(this, Native.mkReStar(nCtx, re.NativeObject));            
+    }
+    
+    /**
+     * Take the Kleene plus of a regular expression.
+     */
+    public ReExpr MPlus(ReExpr re)
+    {
+	checkContextMatch(re);
+	return new ReExpr(this, Native.mkRePlus(nCtx, re.NativeObject));            
+    }
+    
+    /**
+     * Create the optional regular expression.
+     */
+    public ReExpr MOption(ReExpr re)
+    {
+	checkContextMatch(re);
+	return new ReExpr(this, Native.mkReOption(nCtx, re.NativeObject));            
+    }
+    
+    /**
+     * Create the concatenation of regular languages.
+     */
+    public ReExpr MkConcat(ReExpr[] t)
+    {
+	checkContextMatch(t);
+	return new ReExpr(this, Native.mkReConcat(nCtx, (uint)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, (uint)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 +3861,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)

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/python/z3.py

@@ -8991,7 +8991,7 @@ class SeqRef(ExprRef):
     def __getitem__(self, i):
 	return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
 	
-    def is_string_sort(self):
+    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):
@@ -9026,12 +9026,12 @@ def is_seq(a):
     """
     return isinstance(a, SeqRef)
 
-def is_string_sort(a):
+def is_string(a):
     """Return `True` if `a` is a Z3 string expression.
-    >>> print (is_string_sort(StringVal("ab")))
+    >>> print (is_string(StringVal("ab")))
     True
     """
-    return isinstance(a, SeqRef) and a.is_string_sort()
+    return isinstance(a, SeqRef) and a.is_string()
 
 def is_string_value(a):
     """return 'True' if 'a' is a Z3 string constant expression.
@@ -9042,11 +9042,27 @@ def is_string_value(a):
     """
     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())
@@ -9101,6 +9117,10 @@ def Contains(a, b):
     >>> 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)

src/ast/rewriter/seq_rewriter.cpp

@@ -23,6 +23,7 @@ Notes:
 #include"ast_util.h"
 #include"uint_set.h"
 #include"automaton.h"
+#include"well_sorted.h"
 
 
 struct display_expr1 {
@@ -843,37 +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;
-    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);
-            m_lhs.swap(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)) {
@@ -882,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);
@@ -892,13 +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;
+                rs[rs.size()-1] = s2;
             }
         }
         else {
@@ -910,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].get())) {
+        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].get())) {
+        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].get();
-        expr* r = m_rhs[head2].get();
+        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);
-            m_lhs.swap(m_rhs);
+            ls.swap(rs);
         }
         if (l == r) {
             ++head1;
@@ -947,13 +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;
+                rs[rs.size()-1] = s2;
             }            
         }
         else {
@@ -963,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].get(), s1) &&
-           m_util.str.is_string(m_rhs[head2].get(), 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]) {
@@ -977,64 +974,105 @@ 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));
+            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));
+            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)));
+            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)));
+            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
     }
     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));
+        if (head1 > 0) {
+            for (unsigned i = 0; i < szl; ++i) {
+                ls[i] = ls[i + head1];
+            }			
+        }
+        ls.shrink(szl);
+        if (head2 > 0) {
+            for (unsigned i = 0; i < szr; ++i) {
+                rs[i] = rs[i + head2];
+            }
+        }
+        rs.shrink(szr);        
+        lhs.push_back(m_util.str.mk_concat(ls.size(), ls.c_ptr()));
+        rhs.push_back(m_util.str.mk_concat(rs.size(), rs.c_ptr()));
+        ls.reset();
+        rs.reset();
     }
     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 (!m_lhs.empty()) {
+            SASSERT(!m_rhs.empty());
+            lhs.push_back(m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr()));
+            rhs.push_back(m_util.str.mk_concat(m_rhs.size(), m_rhs.c_ptr()));            
+        }
+        for (unsigned i = 0; i < lhs.size(); ++i) {
+            SASSERT(is_well_sorted(m(), lhs[i].get()));
+            SASSERT(is_well_sorted(m(), rhs[i].get()));
+            SASSERT(m().get_sort(lhs[i].get()) == m().get_sort(rhs[i].get()));
+            TRACE("seq", tout << mk_pp(lhs[i].get(), m()) << " = " << mk_pp(rhs[i].get(), m()) << "\n";);
+        }
+        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;

src/ast/rewriter/seq_rewriter.h

@@ -92,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/smt/theory_seq.cpp

@@ -368,11 +368,19 @@ bool theory_seq::propagate_length_coherence(expr* e) {
     // len(e) >= low => e = tail;
     literal low(mk_literal(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true))));
     add_axiom(~low, mk_eq(e, tail, false));    
-    assume_equality(seq, emp);
     if (upper_bound(e, hi)) {
-        expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);
-        expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);     
-        add_axiom(~mk_literal(high1), mk_literal(high2));
+        // len(e) <= hi => len(tail) <= hi - lo
+        expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);       
+        if (hi == lo) {
+            add_axiom(~mk_literal(high1), mk_eq(seq, emp, false));
+        }
+        else {
+            expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);     
+            add_axiom(~mk_literal(high1), mk_literal(high2));
+        }
+    }
+    else {
+        assume_equality(seq, emp);
     }
     return true;
 }
@@ -428,6 +436,15 @@ bool theory_seq::is_nth(expr* e) const {
     return is_skolem(m_nth, e);
 }
 
+bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
+    rational r;
+    return 
+        is_skolem(m_tail, e) && 
+        m_autil.is_numeral(to_app(e)->get_arg(1), r) && 
+        (idx = r.get_unsigned(), s = to_app(e)->get_arg(0), true);
+}
+
+
 expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
     sort* char_sort = 0;
     VERIFY(m_util.is_seq(m.get_sort(s), char_sort));
@@ -602,9 +619,9 @@ bool theory_seq::simplify_eq(expr* l, expr* r, dependency* deps) {
         }
     }        
     TRACE("seq",
-          tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " => ";
+          tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " => \n";
           for (unsigned i = 0; i < lhs.size(); ++i) {
-              tout << mk_pp(lhs[i].get(), m) << " = " << mk_pp(rhs[i].get(), m) << "; ";
+              tout << mk_pp(lhs[i].get(), m) << "\n = \n" << mk_pp(rhs[i].get(), m) << "; \n";
           }
           tout << "\n";);
     return true;
@@ -614,6 +631,8 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
     if (l == r) {
         return true;
     }
+    //propagate_max_length(l, r, deps);
+    
     if (is_var(l) && !occurs(l, r) && add_solution(l, r, deps)) {
         return true;
     }
@@ -712,6 +731,21 @@ bool theory_seq::solve_eq(expr* _l, expr* _r, dependency* deps) {
     return false;
 }
 
+bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
+    unsigned idx;
+    expr* s;
+    if (m_util.str.is_empty(l)) {
+        std::swap(l, r);
+    }
+    rational hi;
+    if (is_tail(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
+        std::cout << "max length " << mk_pp(s, m) << " " << idx << "\n";
+        propagate_lit(deps, 0, 0, mk_literal(m_autil.mk_le(m_util.str.mk_length(s), m_autil.mk_int(idx+1))));
+        return true;
+    }
+    return false;
+}
+
 bool theory_seq::is_binary_eq(expr* l, expr* r, expr*& x, ptr_vector<expr>& xs, ptr_vector<expr>& ys, expr*& y) {    
     xs.reset();
     ys.reset();
@@ -889,13 +923,35 @@ void theory_seq::solve_ne(unsigned idx) {
             --i;
         }
     }
-    if (num_undef_lits == 0 && n.m_lhs.empty()) {
+    if (num_undef_lits == 1 && n.m_lhs.empty()) {
+        literal_vector lits;
+        literal undef_lit = null_literal;
+        for (unsigned i = 0; i < n.m_lits.size(); ++i) {
+            literal lit = n.m_lits[i];
+            switch (ctx.get_assignment(lit)) {
+            case l_true:
+                lits.push_back(lit);
+                break;
+            case l_false:
+                UNREACHABLE();
+                break;
+            case l_undef:
+                SASSERT(undef_lit == null_literal);
+                undef_lit = lit;
+                break;
+            }
+        }        
+        TRACE("seq", tout << "propagate: " << undef_lit << "\n";);
+        SASSERT(undef_lit != null_literal);
+        propagate_lit(n.m_dep, lits.size(), lits.c_ptr(), ~undef_lit); 
+    }
+    else if (num_undef_lits == 0 && n.m_lhs.empty()) {
         literal_vector lits(n.m_lits);
         lits.push_back(~mk_eq(n.m_l, n.m_r, false));
         set_conflict(n.m_dep, lits);
         SASSERT(m_new_propagation);
     }
-    if (num_undef_lits == 0 && n.m_lhs.size() == 1) {
+    else if (false && num_undef_lits == 0 && n.m_lhs.size() == 1) {
         expr* l = n.m_lhs[0];
         expr* r = n.m_rhs[0];
         if (m_util.str.is_empty(r)) {
@@ -903,13 +959,21 @@ void theory_seq::solve_ne(unsigned idx) {
         }
         if (m_util.str.is_empty(l) && is_var(r)) {
             literal lit = ~mk_eq_empty(r);
-            if (ctx.get_assignment(lit) == l_true) {
+            switch (ctx.get_assignment(lit)) {
+            case l_true: {
                 expr_ref head(m), tail(m);
                 mk_decompose(r, head, tail);
                 expr_ref conc(m_util.str.mk_concat(head, tail), m);
                 propagate_is_conc(r, conc);
+                m_new_propagation = true;
+                break;
+            }
+            case l_undef: 
+                m_new_propagation = true;
+                break;
+            case l_false:
+                break;
             }
-            m_new_propagation = true;            
         }
     }
 }
@@ -941,14 +1005,13 @@ bool theory_seq::simplify_and_solve_eqs() {
 
 
 bool theory_seq::internalize_term(app* term) { 
-    TRACE("seq", tout << mk_pp(term, m) << "\n";);
     context & ctx   = get_context();
     if (ctx.e_internalized(term)) {
         enode* e = ctx.get_enode(term);
         mk_var(e);
         return true;
     }
-     
+    TRACE("seq", tout << mk_pp(term, m) << "\n";);     
     unsigned num_args = term->get_num_args();
     expr* arg;
     for (unsigned i = 0; i < num_args; i++) {
@@ -1090,7 +1153,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq branch", m_stats.m_branch_variable);
     st.update("seq solve !=", m_stats.m_solve_nqs);
     st.update("seq solve =", m_stats.m_solve_eqs);
-
+    st.update("seq add axiom", m_stats.m_add_axiom);
 }
 
 void theory_seq::init_model(model_generator & mg) {
@@ -1266,6 +1329,29 @@ expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
     return result;
 }
 
+void theory_seq::canonize(expr* e0, expr_ref_vector& es, dependency*& eqs) {
+    dependency* dep = 0;
+    expr* e = m_rep.find(e0, dep);
+    expr* e1, *e2;
+    if (m_util.str.is_concat(e, e1, e2)) {
+        canonize(e1, es, eqs);
+        canonize(e2, es, eqs);
+    }       
+    else if (m_util.str.is_empty(e)) {
+        // skip
+    }
+    else {
+        expr_ref e3 = expand(e, eqs);
+        if (m_util.str.is_concat(e3) || m_util.str.is_empty(e3)) {
+            canonize(e3, es, eqs);
+        }
+        else {
+            es.push_back(e3);
+        }
+    }
+    eqs = m_dm.mk_join(eqs, dep);
+}
+
 expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     expr_ref result(m);
     dependency* deps = 0;
@@ -1516,10 +1602,12 @@ void theory_seq::add_length_axiom(expr* n) {
         if (n != len) {
             TRACE("seq", tout << "Add length coherence for " << mk_pp(n, m) << "\n";);
             add_axiom(mk_eq(n, len, false));
+            m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
         }
     }
     else {
         add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));        
+        m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
     }
 }
 
@@ -1753,7 +1841,14 @@ void theory_seq::propagate_step(literal lit, expr* step) {
     expr_ref nth = mk_nth(s, idx);
     TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(t, m) << " = " << nth << "\n";);
     propagate_eq(lit, t, nth);
-    propagate_lit(0, 1, &lit, ~mk_literal(m_autil.mk_le(m_util.str.mk_length(s), idx)));
+    rational lo;
+    rational _idx;
+    if (lower_bound(s, lo) && lo.is_unsigned() && m_autil.is_numeral(idx, _idx) && lo >= _idx) {
+        // skip
+    }
+    else {
+        propagate_lit(0, 1, &lit, ~mk_literal(m_autil.mk_le(m_util.str.mk_length(s), idx)));
+    }
     ensure_nth(lit, s, idx);
 }
 
@@ -1774,7 +1869,7 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
     expr_ref_vector elems(m);
     get_concat(s1, es);
     unsigned i = 0;
-    for (; i < _idx && i < es.size() && m_util.str.is_unit(es[i]); ++i) {};    
+    for (; i <= _idx && i < es.size() && m_util.str.is_unit(es[i]); ++i) {};    
     if (i == _idx && i < es.size() && m_util.str.is_unit(es[i], e1)) {
         dep = m_dm.mk_join(dep, m_dm.mk_leaf(assumption(lit)));
         propagate_eq(dep, ensure_enode(nth), ensure_enode(e1));
@@ -1792,7 +1887,9 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
     propagate_eq(lit, s, conc, true);
 
     // TBD: examine other places for enforcing constraints on tail
-    add_axiom(~lit, mk_eq(m_util.str.mk_length(s), m_util.str.mk_length(conc), false));
+    conc = m_autil.mk_add(m_autil.mk_int(_idx+1), m_util.str.mk_length(s2));
+    add_axiom(~lit, mk_eq(m_util.str.mk_length(s), conc, false));
+    //add_axiom(~lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), m_autil.mk_int(_idx + 1))));
 }
 
 literal theory_seq::mk_literal(expr* _e) {
@@ -1823,8 +1920,9 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) {
     if (l2 != null_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); }
     if (l3 != null_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
     if (l4 != null_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
-    TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
+    TRACE("seq", ctx.display_literals_verbose(tout << "axiom: ", lits.size(), lits.c_ptr()); tout << "\n";);
     m_new_propagation = true;
+    ++m_stats.m_add_axiom;
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
 }
 

src/smt/theory_seq.h

@@ -261,6 +261,15 @@ namespace smt {
             }
         };
 
+        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:
@@ -282,6 +291,7 @@ namespace smt {
             unsigned m_branch_variable;
             unsigned m_solve_nqs;
             unsigned m_solve_eqs;
+            unsigned m_add_axiom;
         };
         ast_manager&               m;
         dependency_manager         m_dm;
@@ -357,6 +367,7 @@ namespace smt {
         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);
@@ -383,9 +394,11 @@ namespace smt {
         bool is_var(expr* 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);