From e799ab0164722e8a4f192ee13223d0eeec6ec004 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Jun 2018 13:53:36 -0500 Subject: [PATCH] Do not rename uninterpreted constants (#2098) --- src/expr/uninterpreted_constant.cpp | 10 +--------- src/printer/smt2/smt2_printer.cpp | 4 +++- 2 files changed, 4 insertions(+), 10 deletions(-) diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index 2187d9cdf..9898bcb3f 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -34,15 +34,7 @@ UninterpretedConstant::UninterpretedConstant(Type type, Integer index) } std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { - stringstream ss; - ss << uc.getType(); - string t = ss.str(); - size_t i = 0; - // replace everything that isn't in [a-zA-Z0-9_] with an _ - while((i = t.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ1234567890_", i)) != string::npos) { - t.replace(i, 1, 1, '_'); - } - return out << "uc_" << t << '_' << uc.getIndex(); + return out << "uc_" << uc.getType() << '_' << uc.getIndex(); } }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f6d3cc743..0e1df15b5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -267,7 +267,9 @@ void Smt2Printer::toStream(std::ostream& out, case kind::UNINTERPRETED_CONSTANT: { const UninterpretedConstant& uc = n.getConst(); - out << '@' << uc; + std::stringstream ss; + ss << '@' << uc; + out << maybeQuoteSymbol(ss.str()); break; } -- 2.30.2