mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

pretty-printing of string constants in AST

Browse source 
spec2 looks good now
This commit is contained in:
Murphy Berzish 2015-09-03 01:12:08 -04:00
parent 02345ee5f1
commit 744d2e3c9c
5 changed files with 31 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/ast_smt2_pp.cpp
View file

@ -298,6 +298,18 @@ format * smt2_pp_environment::mk_float(rational const & val) const {
return mk_string(get_manager(), s.c_str());
}
format * smt2_pp_environment::pp_str_literal(app * t) {
TRACE("parse_string", tout << "pp_str_literal\n";);
str_util & u = get_strutil();
SASSERT(u.is_string(t));
const char * val;
u.is_string(t, &val);
ast_manager & m = get_manager();
string_buffer<> buf;
buf << "\"" << val << "\"";
return mk_string(m, buf.c_str());
}
format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned decimal_prec) {
arith_util & u = get_autil();
SASSERT(u.is_numeral(t) || u.is_irrational_algebraic_numeral(t));
@ -581,6 +593,9 @@ class smt2_printer {
else if (m_env.get_dlutil().is_numeral(c)) {
f = m_env.pp_datalog_literal(c);
}
else if (m_env.get_strutil().is_string(c)) {
f = m_env.pp_str_literal(c);
}
else {
buffer<symbol> names;
if (m().is_label_lit(c, names)) {

7
src/ast/ast_smt2_pp.h
View file

@ -29,6 +29,7 @@ Revision History:
#include"array_decl_plugin.h"
#include"fpa_decl_plugin.h"
#include"dl_decl_plugin.h"
#include"str_decl_plugin.h"
#include"smt2_util.h"
class smt2_pp_environment {
@ -47,12 +48,14 @@ public:
virtual bv_util & get_bvutil() = 0;
virtual array_util & get_arutil() = 0;
virtual fpa_util & get_futil() = 0;
virtual str_util & get_strutil() = 0;
virtual datalog::dl_decl_util& get_dlutil() = 0;
virtual bool uses(symbol const & s) const = 0;
virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len);
virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg);
virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec);
virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits);
virtual format_ns::format * pp_str_literal(app * t);
virtual format_ns::format * pp_datalog_literal(app * t);
virtual format_ns::format * pp_sort(sort * s);
virtual format_ns::format * pp_fdecl_ref(func_decl * f);
@ -70,14 +73,16 @@ class smt2_pp_environment_dbg : public smt2_pp_environment {
bv_util m_bvutil;
array_util m_arutil;
fpa_util m_futil;
str_util m_strutil;
datalog::dl_decl_util m_dlutil;
public:
smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_dlutil(m) {}
smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_strutil(m), m_dlutil(m) {}
virtual ast_manager & get_manager() const { return m_manager; }
virtual arith_util & get_autil() { return m_autil; }
virtual bv_util & get_bvutil() { return m_bvutil; }
virtual array_util & get_arutil() { return m_arutil; }
virtual fpa_util & get_futil() { return m_futil; }
virtual str_util & get_strutil() { return m_strutil; }
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
virtual bool uses(symbol const & s) const { return false; }
};

5
src/ast/str_decl_plugin.cpp
View file

@ -74,6 +74,11 @@ bool str_recognizers::is_string(expr const * n, const char ** val) const {
return true;
}
bool str_recognizers::is_string(expr const * n) const {
const char * tmp = 0;
return is_string(n, & tmp);
}
str_util::str_util(ast_manager &m) :
str_recognizers(m.mk_family_id(symbol("str"))),
m_manager(m) {

1
src/ast/str_decl_plugin.h
View file

@ -57,6 +57,7 @@ public:
family_id get_family_id() const { return get_fid(); }
bool is_string(expr const * n, const char ** val) const;
bool is_string(expr const * n) const;
// TODO
};

5
src/cmd_context/cmd_context.cpp
View file

@ -25,6 +25,7 @@ Notes:
#include"datatype_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"fpa_decl_plugin.h"
#include"str_decl_plugin.h"
#include"ast_pp.h"
#include"var_subst.h"
#include"pp.h"
@ -241,6 +242,7 @@ protected:
bv_util m_bvutil;
array_util m_arutil;
fpa_util m_futil;
str_util m_strutil;
datalog::dl_decl_util m_dlutil;
format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) {
@ -261,13 +263,14 @@ protected:
}
public:
pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_dlutil(o.m()) {}
pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_strutil(o.m()), m_dlutil(o.m()) {}
virtual ~pp_env() {}
virtual ast_manager & get_manager() const { return m_owner.m(); }
virtual arith_util & get_autil() { return m_autil; }
virtual bv_util & get_bvutil() { return m_bvutil; }
virtual array_util & get_arutil() { return m_arutil; }
virtual fpa_util & get_futil() { return m_futil; }
virtual str_util & get_strutil() { return m_strutil; }
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
virtual bool uses(symbol const & s) const {
return