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

Fixed issues with the pretty printer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-13 15:19:37 -08:00
parent c98f0c8307
commit 6958b9cdb6
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
RELEASE_NOTES
View file

@ -28,6 +28,8 @@ Version 4.3.2
- Removed auxiliary constants created by the nnf tactic from Z3 models.
- Fixed problem in the pretty printer. It was not introducing quotes for attribute names such as |foo:10|.
Version 4.3.1
=============

9
src/ast/ast_smt2_pp.cpp
View file

@ -501,7 +501,12 @@ class smt2_printer {
}
format * pp_simple_attribute(char const * attr, symbol const & s) {
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), s.str().c_str()));
std::string str;
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()));
}
format * pp_labels(bool is_pos, buffer<symbol> const & names, format * f) {
@ -851,7 +856,7 @@ class smt2_printer {
buf.push_back(pp_simple_attribute(":weight ", q->get_weight()));
}
if (q->get_skid() != symbol::null) {
buf.push_back(pp_simple_attribute(":skid ", q->get_skid()));
buf.push_back(pp_simple_attribute(":skolemid ", q->get_skid()));
}
if (q->get_qid() != symbol::null) {
#if 0