add sequence recognizers

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

src/api/dotnet/Expr.cs

@@ -811,6 +811,61 @@ namespace Microsoft.Z3
         /// <remarks>the expression should be a string constant, (IsString should be true).</remarks>
         public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }        
 
+        /// <summary>
+        /// Check whether expression is a concatentation.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } }
+
+        /// <summary>
+        /// Check whether expression is a prefix.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } }
+
+        /// <summary>
+        /// Check whether expression is a suffix.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } }
+	
+        /// <summary>
+        /// Check whether expression is a contains.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } }
+	
+        /// <summary>
+        /// Check whether expression is an extract.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } }
+	
+        /// <summary>
+        /// Check whether expression is a replace.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } }
+	
+        /// <summary>
+        /// Check whether expression is an at.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }	
+
+        /// <summary>
+        /// Check whether expression is a sequence length.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } }
+	
+        /// <summary>
+        /// Check whether expression is a sequence index.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+	public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } }
+	
+
         #endregion
 
         #region Proof Terms

src/cmd_context/cmd_context.cpp

@@ -15,6 +15,7 @@ Author:
 Notes:
 
 --*/
+
 #include<signal.h>
 #include"tptr.h"
 #include"cmd_context.h"