add API to access unescaped strings, update documentation of Z3_get_l…

…string, #5615 Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Oct 21, 2021 · 05e7ed9 · 05e7ed9
1 parent 6eed885
commit 05e7ed9
Show file tree

Hide file tree

Showing 2 changed files with 53 additions and 1 deletion.
diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
@@ -215,6 +215,38 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
+    unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s) {
+        Z3_TRY;
+        LOG_Z3_get_string_length(c, s);
+        RESET_ERROR_CODE();
+        zstring str;
+        if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal");
+        }
+        return str.length();
+        Z3_CATCH_RETURN(0);
+    }    
+
+    void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned* contents) {
+        Z3_TRY;
+        LOG_Z3_get_string_contents(c, s, length, contents);
+        RESET_ERROR_CODE();
+        zstring str;
+        if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal");
+            return;
+        }
+        if (str.length() != length) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, "string size disagrees with supplied buffer length");
+            return;
+        }
+        for (unsigned i = 0; i < length; ++i)
+            contents[i] = str[i];
+
+        Z3_CATCH;
+    }
+
+
 #define MK_SORTED(NAME, FN )                                    \
     Z3_ast Z3_API NAME(Z3_context c, Z3_sort s) {               \
     Z3_TRY;                                                     \

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
@@ -3510,14 +3510,34 @@ extern "C" {
     Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
 
     /**
-       \brief Retrieve the unescaped string constant stored in \c s.
+       \brief Retrieve the string constant stored in \c s. The string can contain escape sequences.
 
        \pre  Z3_is_string(c, s)
 
        def_API('Z3_get_lstring', CHAR_PTR, (_in(CONTEXT), _in(AST), _out(UINT)))
      */
     Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length);
+
+    /**
+       \brief Retrieve the length of the unescaped string constant stored in \c s. 
+
+       \pre  Z3_is_string(c, s)
 
+       def_API('Z3_get_string_length', UINT, (_in(CONTEXT), _in(AST)))
+    */
+    unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s);
+
+    /**
+       \brief Retrieve the unescaped string constant stored in \c s. 
+
+       \pre  Z3_is_string(c, s)
+
+       \pre length contains the number of characters in s
+
+       def_API('Z3_get_string_contents', VOID, (_in(CONTEXT), _in(AST), _in(UINT), _out_array(2, UINT)))
+     */
+    void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned* buffer);
+
     /**
        \brief Create an empty sequence of the sequence sort \c seq.