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

fix quotation bug reported by Arie Gurfinkel

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-04 17:18:49 -08:00
parent b1b349f496
commit 601cb43f78
1 changed files with 22 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/ast/ast_smt2_pp.cpp
View file

@ -472,6 +472,25 @@ class smt2_printer {
ast_manager & m() const { return m_manager; } ast_manager & m() const { return m_manager; }
ast_manager & fm() const { return format_ns::fm(m()); } ast_manager & fm() const { return format_ns::fm(m()); }
std::string ensure_quote(symbol const& s) {
std::string str;
if (is_smt2_quoted_symbol(s))
str = mk_smt2_quoted_symbol(s);
else
str = s.str();
return str;
}
symbol ensure_quote_sym(symbol const& s) {
if (is_smt2_quoted_symbol(s)) {
std::string str;
str = mk_smt2_quoted_symbol(s);
return symbol(str.c_str());
}
else
return s;
}
void pp_var(var * v) { void pp_var(var * v) {
format * f; format * f;
if (v->get_idx() < m_var_names.size()) { if (v->get_idx() < m_var_names.size()) {
@ -501,11 +520,7 @@ class smt2_printer {
} }
format * pp_simple_attribute(char const * attr, symbol const & s) { format * pp_simple_attribute(char const * attr, symbol const & s) {
std::string str; std::string str = ensure_quote(s);
if (is_smt2_quoted_symbol(s))
str = mk_smt2_quoted_symbol(s);
else
str = s.str();
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str())); return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str()));
} }
@ -773,7 +788,7 @@ class smt2_printer {
void register_var_names(quantifier * q) { void register_var_names(quantifier * q) {
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
for (unsigned i = 0; i < num_decls; i++) { for (unsigned i = 0; i < num_decls; i++) {
symbol name = q->get_decl_name(i); symbol name = ensure_quote_sym(q->get_decl_name(i));
if (name.is_numerical()) { if (name.is_numerical()) {
unsigned idx = 1; unsigned idx = 1;
name = next_name("x", idx); name = next_name("x", idx);
@ -997,6 +1012,7 @@ public:
unsigned idx = 1; unsigned idx = 1;
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
symbol name = next_name(var_prefix, idx); symbol name = next_name(var_prefix, idx);
name = ensure_quote_sym(name);
var_names.push_back(name); var_names.push_back(name);
m_var_names_set.insert(name); m_var_names_set.insert(name);
m_var_names.push_back(name); m_var_names.push_back(name);