use some suggestions from #5615

Signed-off-by: Nikolaj Bjorner <[email protected]>

examples/c++/example.cpp

@@ -1254,7 +1254,7 @@ static void string_values() {
     std::cout << s << "\n";
     std::string s1 = s.get_string();
     std::cout << s1 << "\n";
-    std::vector<unsigned> buffer = s.get_wstring();
+    std::u32string buffer = s.get_u32string();
     for (unsigned ch : buffer)
         std::cout << "char: " << ch << "\n";
 }

src/api/api_seq.cpp

@@ -58,7 +58,7 @@ extern "C" {
 
     Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned sz, Z3_string str) {
         Z3_TRY;
-        LOG_Z3_mk_string(c, str);
+        LOG_Z3_mk_lstring(c, sz, str);
         RESET_ERROR_CODE();
         unsigned_vector chs;
         for (unsigned i = 0; i < sz; ++i) chs.push_back((unsigned char)str[i]);
@@ -69,6 +69,17 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned sz, unsigned const chars[]) {
+        Z3_TRY;
+        LOG_Z3_mk_u32string(c, sz, chars);
+        RESET_ERROR_CODE();
+        zstring s(sz, chars);
+        app* a = mk_c(c)->sutil().str.mk_string(s);
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     Z3_sort Z3_API Z3_mk_string_sort(Z3_context c) {
         Z3_TRY;
         LOG_Z3_mk_string_sort(c);

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

@@ -379,6 +379,7 @@ namespace z3 {
         expr string_val(char const* s);
         expr string_val(char const* s, unsigned n);
         expr string_val(std::string const& s);
+        expr string_val(std::u32string const& s);
 
         expr num_val(int n, sort const & s);
 
@@ -1111,13 +1112,21 @@ namespace z3 {
             return std::string(s);
         }
 
-        std::vector<unsigned> get_wstring() const {
+        /**
+           \brief for a string value expression return an unespaced string value.
+           \pre expression is for a string value.
+        */
+
+        std::u32string get_u32string() const {
             assert(is_string_value());
             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;
+            std::u32string s;
+            for (auto ch : buffer)
+                s.push_back(ch);
+            return s;
         }
 
         operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
@@ -3481,6 +3490,7 @@ namespace z3 {
     inline expr context::string_val(char const* s, unsigned n) { Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }
     inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
     inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
+    inline expr context::string_val(std::u32string const& s) { Z3_ast r = Z3_mk_u32string(m_ctx, (unsigned)s.size(), (unsigned const*)s.c_str()); check_error(); return expr(*this, r); }
 
     inline expr context::num_val(int n, sort const & s) { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
 

src/api/z3_api.h

@@ -3493,6 +3493,15 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s);
 
+    /**
+       \brief Create a string constant out of the string that is passed in
+       It takes the length of the string as well to take into account
+       0 characters. The string is unescaped.
+
+       def_API('Z3_mk_u32string', AST, (_in(CONTEXT), _in(UINT), _in_array(1, UINT)))
+     */
+    Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[]);
+
     /**
        \brief Determine if \c s is a string constant.
 

src/smt/smt_parallel.cpp

@@ -149,21 +149,18 @@ namespace smt {
                 expr_ref c(pm);
 
                 pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts);
-                if (num_rounds > 0 && (pctx.get_fparams().m_threads_cube_frequency % num_rounds) == 0) {
+                if (num_rounds > 0 && (pctx.get_fparams().m_threads_cube_frequency % num_rounds) == 0) 
                     cube(pctx, lasms, c);
-                }
                 IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; 
                            if (num_rounds > 0) verbose_stream() << " :round " << num_rounds;
                            if (c) verbose_stream() << " :cube " << mk_bounded_pp(c, pm, 3);
                            verbose_stream() << ")\n";);
                 lbool r = pctx.check(lasms.size(), lasms.data());
 
-                if (r == l_undef && pctx.m_num_conflicts >= max_conflicts) {
-                    // no-op
-                }
-                else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts) {
+                if (r == l_undef && pctx.m_num_conflicts >= max_conflicts) 
+                    ; // no-op
+                else if (r == l_undef && pctx.m_num_conflicts >= thread_max_conflicts) 
                     return;
-                }                
                 else if (r == l_false && pctx.unsat_core().contains(c)) {
                     IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")");
                     pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));