diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 23ffe61bd..5e0abcb74 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -811,6 +811,61 @@ namespace Microsoft.Z3 /// the expression should be a string constant, (IsString should be true). public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } } + /// + /// Check whether expression is a concatentation. + /// + /// a Boolean + public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } } + + /// + /// Check whether expression is a prefix. + /// + /// a Boolean + public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } } + + /// + /// Check whether expression is a suffix. + /// + /// a Boolean + public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } } + + /// + /// Check whether expression is a contains. + /// + /// a Boolean + public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } } + + /// + /// Check whether expression is an extract. + /// + /// a Boolean + public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } } + + /// + /// Check whether expression is a replace. + /// + /// a Boolean + public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } } + + /// + /// Check whether expression is an at. + /// + /// a Boolean + public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } } + + /// + /// Check whether expression is a sequence length. + /// + /// a Boolean + public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } } + + /// + /// Check whether expression is a sequence index. + /// + /// a Boolean + public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } } + + #endregion #region Proof Terms diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index caafbfb8c..af16f5796 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -15,6 +15,7 @@ Author: Notes: --*/ + #include #include"tptr.h" #include"cmd_context.h"