updated C++ API for escaped and unescaped strings #5615

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

examples/c++/example.cpp

@@ -1249,10 +1249,14 @@ void recfun_example() {
 
 static void string_values() {
     context c;
+    std::cout << "string_values\n";
     expr s = c.string_val("abc\n\n\0\0", 7);
     std::cout << s << "\n";
     std::string s1 = s.get_string();
     std::cout << s1 << "\n";
+    std::vector<unsigned> buffer = s.get_wstring();
+    for (unsigned ch : buffer)
+        std::cout << "char: " << ch << "\n";
 }
 
 expr MakeStringConstant(context* context, std::string value) {

src/api/api_seq.cpp

@@ -187,10 +187,9 @@ extern "C" {
         svector<char> buff;
         for (unsigned i = 0; i < str.length(); ++i) {
             unsigned ch = str[i];
-            if (ch <= 32 || ch >= 127) {
+            if (ch <= 32 || ch >= 127 || (ch == '\\' && i + 1 < str.length() && str[i+1] == 'u')) {
                 buff.reset();
                 buffer.push_back('\\');
-//                buffer.push_back('\\');  // possibly replace by native non-escaped version?
                 buffer.push_back('u');
                 buffer.push_back('{');
                 while (ch > 0) {

src/api/c++/z3++.h

@@ -1100,23 +1100,24 @@ namespace z3 {
         bool is_string_value() const { return Z3_is_string(ctx(), m_ast); }
 
         /**
-           \brief for a string value expression return an escaped or unescaped string value.
+           \brief for a string value expression return an escaped string value.
            \pre expression is for a string value.
          */
 
-        std::string get_escaped_string() const {            
+        std::string get_string() const {            
             assert(is_string_value());
             char const* s = Z3_get_string(ctx(), m_ast);
             check_error();
             return std::string(s);
         }
 
-        std::string get_string() const {
+        std::vector<unsigned> get_wstring() const {
             assert(is_string_value());
-            unsigned n;
-            char const* s = Z3_get_lstring(ctx(), m_ast, &n);
-            check_error();
-            return std::string(s, n);
+            unsigned n = Z3_get_string_length(ctx(), m_ast);
+            std::vector<unsigned> buffer;
+            buffer.resize(n);
+            Z3_get_string_contents(ctx(), m_ast, n, buffer.data());
+            return buffer;
         }
 
         operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }

src/smt/user_propagator.h

@@ -48,7 +48,7 @@ namespace smt {
             void reset() { memset(this, 0, sizeof(*this)); }
         };
 
-        void*                  m_user_context;
+        void*                  m_user_context = nullptr;
         solver::push_eh_t      m_push_eh;
         solver::pop_eh_t       m_pop_eh;
         solver::fresh_eh_t     m_fresh_eh;
@@ -56,13 +56,13 @@ namespace smt {
         solver::fixed_eh_t     m_fixed_eh;
         solver::eq_eh_t        m_eq_eh;
         solver::eq_eh_t        m_diseq_eh;
-        solver::context_obj*   m_api_context { nullptr };
-        unsigned               m_qhead { 0 };
+        solver::context_obj*   m_api_context = nullptr;
+        unsigned               m_qhead = 0;
         uint_set               m_fixed;
         vector<prop_info>      m_prop;
         unsigned_vector        m_prop_lim;
         vector<literal_vector> m_id2justification;
-        unsigned               m_num_scopes { 0 };
+        unsigned               m_num_scopes = 0;
         literal_vector         m_lits;
         enode_pair_vector      m_eqs;
         stats                  m_stats;

src/solver/solver.h

@@ -51,7 +51,7 @@ class solver : public check_sat_result {
     params_ref  m_params;
     symbol      m_cancel_backup_file;
 public:
-     solver() {}
+    solver() {}
     ~solver() override {}
 
     /**