add string accessors to managed APIs #1051

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

src/api/dotnet/Expr.cs

@@ -797,6 +797,22 @@ namespace Microsoft.Z3
         public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
         #endregion
 
+        #region Sequences and Strings
+
+        /// <summary>
+        /// Check whether expression is a string constant.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+        public bool IsString  { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } }
+
+        /// <summary>
+        /// Retrieve string corresponding to string constant.
+        /// </summary>
+        /// <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); } }        
+
+        #endregion
+
         #region Proof Terms
         /// <summary>
         /// Indicates whether the term is a binary equivalence modulo namings.

src/api/java/Expr.java

@@ -1277,6 +1277,26 @@ public class Expr extends AST
         return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
     }
 
+    /**
+     * Check whether expression is a string constant.
+     * @return a boolean
+     */
+    public boolean isString() 
+    {
+        return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Retrieve string corresponding to string constant.
+     * Remark: the expression should be a string constant, (isString() should return true).
+     * @throws Z3Exception on error
+     * @return a string
+     */
+    public String getString()
+    {
+	return Native.getString(getContext().nCtx(), getNativeObject());
+    }
+
     /**
      * Indicates whether the term is a binary equivalence modulo namings.
      * Remarks: This binary predicate is used in proof terms. It captures

src/smt/theory_str.cpp

@@ -25,6 +25,7 @@
 #include<algorithm>
 #include"theory_seq_empty.h"
 #include"theory_arith.h"
+#include"ast_util.h"
 
 namespace smt {
     
@@ -98,7 +99,8 @@ namespace smt {
         if (defaultCharset) {
             // valid C strings can't contain the null byte ('\0')
             charSetSize = 255;
-            char_set = alloc_svect(char, charSetSize);
+            char_set.resize(256, 0);            
+            charSetLookupTable.resize(256, 0);
             int idx = 0;
             // small letters
             for (int i = 97; i < 123; i++) {
@@ -157,8 +159,8 @@ namespace smt {
         } else {
             const char setset[] = { 'a', 'b', 'c' };
             int fSize = sizeof(setset) / sizeof(char);
-
+            char_set.resize(fSize, 0);
-            char_set = alloc_svect(char, fSize);
+            charSetLookupTable.resize(fSize, 0);
             charSetSize = fSize;
             for (int i = 0; i < charSetSize; i++) {
                 char_set[i] = setset[i];
@@ -9123,7 +9125,7 @@ namespace smt {
 
     zstring theory_str::gen_val_string(int len, int_vector & encoding) {
         SASSERT(charSetSize > 0);
-        SASSERT(char_set != NULL);
+        SASSERT(!char_set.empty());
 
         std::string re(len, char_set[0]);
         for (int i = 0; i < (int) encoding.size() - 1; i++) {
@@ -9240,8 +9242,7 @@ namespace smt {
 
         // ----------------------------------------------------------------------------------------
         
-        ptr_vector<expr> orList;
+        expr_ref_vector orList(m), andList(m);
-        ptr_vector<expr> andList;
 
         for (long long i = l; i < h; i++) {
             orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) ));
@@ -9262,7 +9263,7 @@ namespace smt {
             } else {
                 strAst = mk_string(aStr);
             }
-            andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst)));
+            andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst)));
         }
         if (!coverAll) {
             orList.push_back(m.mk_eq(val_indicator, mk_string("more")));
@@ -9273,21 +9274,8 @@ namespace smt {
             }
         }
 
-        expr ** or_items = alloc_svect(expr*, orList.size());
+        andList.push_back(mk_or(orList));
-        expr ** and_items = alloc_svect(expr*, andList.size() + 1);
+        expr_ref valTestAssert = mk_and(andList);
-
-        for (int i = 0; i < (int) orList.size(); i++) {
-            or_items[i] = orList[i];
-        }
-        if (orList.size() > 1)
-            and_items[0] = m.mk_or(orList.size(), or_items);
-        else
-            and_items[0] = or_items[0];
-
-        for (int i = 0; i < (int) andList.size(); i++) {
-            and_items[i + 1] = andList[i];
-        }
-        expr * valTestAssert = m.mk_and(andList.size() + 1, and_items);
 
         // ---------------------------------------
         // If the new value tester is $$_val_x_16_i
@@ -9300,17 +9288,7 @@ namespace smt {
             if (vTester != val_indicator)
                 andList.push_back(m.mk_eq(vTester, mk_string("more")));
         }
-        expr * assertL = NULL;
+        expr_ref assertL = mk_and(andList);
-        if (andList.size() == 1) {
-            assertL = andList[0];
-        } else {
-            expr ** and_items = alloc_svect(expr*, andList.size());
-            for (int i = 0; i < (int) andList.size(); i++) {
-                and_items[i] = andList[i];
-            }
-            assertL = m.mk_and(andList.size(), and_items);
-        }
-
         // (assertL => valTestAssert) <=> (!assertL OR valTestAssert)
         valTestAssert = m.mk_or(m.mk_not(assertL), valTestAssert);
         return valTestAssert;

src/smt/theory_str.h

@@ -330,8 +330,8 @@ protected:
 
     std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
 
-    char * char_set;
+    svector<char> char_set;
-    std::map<char, int> charSetLookupTable;
+    svector<int>  charSetLookupTable;
     int           charSetSize;
 
     obj_pair_map<expr, expr, expr*> concat_astNode_map;