fix string constant representation in parser

spec1 loopback OK

src/ast/ast.h

@@ -118,7 +118,9 @@ public:
     explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); }
     explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); }
     explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
-    explicit parameter(const char *s):m_kind(PARAM_STRING), m_string(s) {}
+    explicit parameter(const char *s):m_kind(PARAM_STRING), m_string(s) {
+        TRACE("parse_string", tout << "parameter(const char *): " << s << "\n";);
+    }
     explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
     parameter(parameter const&);
 

src/ast/ast_smt_pp.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include"ast_smt_pp.h"
 #include"arith_decl_plugin.h"
 #include"bv_decl_plugin.h"
+#include"str_decl_plugin.h"
 #include"array_decl_plugin.h"
 #include"datatype_decl_plugin.h"
 #include"vector.h"
@@ -160,8 +161,10 @@ class smt_printer {
     unsigned         m_num_lets;
     arith_util       m_autil;
     bv_util          m_bvutil;
+    str_util         m_strutil;
     family_id        m_basic_fid;
     family_id        m_bv_fid;
+    family_id        m_str_fid;
     family_id        m_arith_fid;
     family_id        m_array_fid;
     family_id        m_dt_fid;
@@ -394,6 +397,7 @@ class smt_printer {
 
     void visit_app(app* n) {
         rational val;
+        const char *str;
         bool is_int, pos;
         buffer<symbol> names;
         unsigned bv_size;
@@ -436,6 +440,9 @@ class smt_printer {
                 m_out << ") bv1[1])";
             }
         }
+        else if (m_strutil.is_string(n, &str)) {
+            m_out << "\"" << str << "\"";
+        }
         else if (m_manager.is_label(n, pos, names) && names.size() >= 1) {
             if (m_is_smt2) {
                 m_out << "(! "; 
@@ -797,6 +804,7 @@ public:
         m_num_lets(0),
         m_autil(m),
         m_bvutil(m),
+        m_strutil(m),
         m_logic(logic),
         m_AUFLIRA("AUFLIRA"),
         // It's much easier to read those testcases with that.
@@ -809,6 +817,7 @@ public:
         m_bv_fid    = m.mk_family_id("bv");
         m_arith_fid = m.mk_family_id("arith");
         m_array_fid = m.mk_family_id("array");
+        m_str_fid   = m.mk_family_id("str");
         m_dt_fid    = m.mk_family_id("datatype");
     }
     

src/ast/str_decl_plugin.cpp

@@ -66,6 +66,14 @@ app * str_decl_plugin::mk_string(const char * val) {
     return m_manager->mk_const(d);
 }
 
+bool str_recognizers::is_string(expr const * n, const char ** val) const {
+    if (!is_app_of(n, m_afid, OP_STR))
+            return false;
+    func_decl * decl = to_app(n)->get_decl();
+    *val    = decl->get_parameter(0).get_string();
+    return true;
+}
+
 str_util::str_util(ast_manager &m) :
     str_recognizers(m.mk_family_id(symbol("str"))),
     m_manager(m) {

src/ast/str_decl_plugin.h

@@ -55,6 +55,8 @@ public:
     str_recognizers(family_id fid):m_afid(fid) {}
     family_id get_fid() const { return m_afid; }
     family_id get_family_id() const { return get_fid(); }
+
+    bool is_string(expr const * n, const char ** val) const;
     // TODO
 };
 

src/parsers/smt2/smt2parser.cpp

@@ -1064,8 +1064,13 @@ namespace smt2 {
 
         void parse_string() {
             SASSERT(curr() == scanner::STRING_TOKEN);
-            TRACE("parse_string", tout << "new string constant: " << m_scanner.get_string() << "\n";);
-            expr_stack().push_back(strutil().mk_string(m_scanner.get_string()));
+            char const *original_token = m_scanner.get_string();
+            size_t bufsize = strlen(original_token);
+            char * buf = alloc_svect(char, bufsize + 1);
+            strncpy(buf, original_token, bufsize);
+            buf[bufsize] = '\0';
+            TRACE("parse_string", tout << "new string constant: " << buf << " length=" << bufsize << "\n";);
+            expr_stack().push_back(strutil().mk_string(buf));
             next();
         }
 

src/test/smt2print_parse.cpp

@@ -7,8 +7,9 @@
 void test_print(Z3_context ctx, Z3_ast a) {
     Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
     char const* spec1 = Z3_benchmark_to_smtlib_string(ctx, "test", 0, 0, 0, 0, 0, a);
-    std::cout << spec1 << "\n";
+    std::cout << "spec1: benchmark->string\n" << spec1 << "\n";
 
+    std::cout << "attempting to parse spec1...\n";
     Z3_ast b = 
         Z3_parse_smtlib2_string(ctx, 
                                 spec1,
@@ -18,14 +19,14 @@ void test_print(Z3_context ctx, Z3_ast a) {
                                 0,
                                 0,
                                 0);
-
+    std::cout << "parse successful, converting ast->string\n";
     char const* spec2 = Z3_ast_to_string(ctx, b);
-    std::cout << spec2 << "\n";    
+    std::cout << "spec2: string->ast->string\n" << spec2 << "\n";
 }
 
 void test_parseprint(char const* spec) {
     Z3_context ctx = Z3_mk_context(0);
-    std::cout << spec << "\n";
+    std::cout << "spec:\n" << spec << "\n";
 
     Z3_ast a = 
         Z3_parse_smtlib2_string(ctx, 
@@ -37,8 +38,12 @@ void test_parseprint(char const* spec) {
                                 0,
                                 0);
     
+    std::cout << "done parsing\n";
+
     test_print(ctx, a);
 
+    std::cout << "done printing\n";
+
     Z3_del_context(ctx);
 }