seq, API

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

src/api/dotnet/Context.cs

@@ -2286,6 +2286,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 +4672,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)
         {

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

@@ -209,7 +209,7 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>branch_variable\n";);
         return FC_CONTINUE;
     }
-    if (!check_length_coherence()) {
+    if (check_length_coherence()) {
         ++m_stats.m_check_length_coherence;
         TRACE("seq", tout << ">>check_length_coherence\n";);
         return FC_CONTINUE;
@@ -374,29 +374,36 @@ bool theory_seq::propagate_length_coherence(expr* e) {
         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));
     }
-    m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
     return true;
 }
 
+bool theory_seq::check_length_coherence(expr* e) {
+    if (is_var(e) && m_rep.is_root(e)) {
+        expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
+        expr_ref head(m), tail(m);
+        if (!propagate_length_coherence(e) &&
+            l_false == assume_equality(e, emp)) {
+            // e = emp \/ e = unit(head.elem(e))*tail(e)
+            mk_decompose(e, head, tail);
+            expr_ref conc(m_util.str.mk_concat(head, tail), m);
+            propagate_is_conc(e, conc);
+            assume_equality(tail, emp);
+        }
+        m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
+        return true;
+    }
+    return false;
+}
+
 bool theory_seq::check_length_coherence() {
     obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
     for (; it != end; ++it) {
         expr* e = *it;
-        if (is_var(e) && m_rep.is_root(e)) {
-            expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
-            expr_ref head(m), tail(m);
-            if (!propagate_length_coherence(e) &&
-                l_false == assume_equality(e, emp)) {
-                // e = emp \/ e = unit(head.elem(e))*tail(e)
-                mk_decompose(e, head, tail);
-                expr_ref conc(m_util.str.mk_concat(head, tail), m);
-                propagate_is_conc(e, conc);
-                assume_equality(tail, emp);
-            }
-            return false;
+        if (check_length_coherence(e)) {
+            return true;
         }
     }
-    return true;
+    return false;
 }    
 
 /*
@@ -936,6 +943,12 @@ 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;
+    }
+     
     unsigned num_args = term->get_num_args();
     expr* arg;
     for (unsigned i = 0; i < num_args; i++) {
@@ -947,6 +960,7 @@ bool theory_seq::internalize_term(app* term) {
         ctx.set_var_theory(bv, get_id());
         ctx.mark_as_relevant(bv);
     }
+
     enode* e = 0;
     if (ctx.e_internalized(term)) {
         e = ctx.get_enode(term);
@@ -1049,7 +1063,9 @@ void theory_seq::display_disequation(std::ostream& out, ne const& e) const {
     for (unsigned j = 0; j < e.m_lhs.size(); ++j) {
         out << mk_pp(e.m_lhs[j], m) << " != " << mk_pp(e.m_rhs[j], m) << "\n";
     }
-    display_deps(out, e.m_dep);        
+    if (e.m_dep) {
+        display_deps(out, e.m_dep);        
+    }
 }
 
 void theory_seq::display_deps(std::ostream& out, dependency* dep) const {
@@ -1063,8 +1079,7 @@ void theory_seq::display_deps(std::ostream& out, dependency* dep) const {
         literal lit = lits[i];
         get_context().display_literals_verbose(out << "\n   ", 1, &lit);
     }
-    out << "\n";
-    
+    out << "\n";        
 }
 
 void theory_seq::collect_statistics(::statistics & st) const {
@@ -1287,7 +1302,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     m_rep.add_cache(e0, edr);
     eqs = m_dm.mk_join(eqs, deps);
     TRACE("seq_verbose", tout << mk_pp(e0, m) << " |--> " << result << "\n";
-          display_deps(tout, eqs););
+          if (eqs) display_deps(tout, eqs););
     return result;
 }
 

src/smt/theory_seq.h

@@ -257,7 +257,7 @@ namespace smt {
         public:
             replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
             virtual void operator()(theory_seq& th) {
-                th.propagate_length_coherence(m_e);
+                th.check_length_coherence(m_e);
             }
         };
 
@@ -348,6 +348,7 @@ namespace smt {
         bool split_variable();           // split a variable
         bool is_solved(); 
         bool check_length_coherence();
+        bool check_length_coherence(expr* e);
         bool propagate_length_coherence(expr* e);  
 
         bool solve_eqs(unsigned start);