From 02345ee5f190d7033373523743329ec5de016b78 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 3 Sep 2015 00:17:05 -0400 Subject: [PATCH] fix string constant representation in parser spec1 loopback OK --- src/ast/ast.h | 4 +++- src/ast/ast_smt_pp.cpp | 9 +++++++++ src/ast/str_decl_plugin.cpp | 8 ++++++++ src/ast/str_decl_plugin.h | 2 ++ src/parsers/smt2/smt2parser.cpp | 9 +++++++-- src/test/smt2print_parse.cpp | 13 +++++++++---- 6 files changed, 38 insertions(+), 7 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 9c1044ec7..14b869e51 100644 --- a/src/ast/ast.h +++ b/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&); diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 805f3070f..0785c7bfc 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/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 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"); } diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index 540cd89c0..66b6c23fc 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/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) { diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index 2fd1db022..2d629e006 100644 --- a/src/ast/str_decl_plugin.h +++ b/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 }; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index af752c82d..5c8d60700 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/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(); } diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 349a3c9c8..1b491a022 100644 --- a/src/test/smt2print_parse.cpp +++ b/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); }