diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-03 11:56:51 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-03 11:56:51 -0500 |
commit | 243a1d58a139077ecf19ac8a68573e51c08e4621 (patch) | |
tree | 8fa7ae926032b6c6d7c10b269ba4b32afbf6af62 /src | |
parent | fbc61a7bbe75c99b29cd238f552c18542deb5c32 (diff) |
Fix printing issue related to nested quotes (#3154)
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/uninterpreted_constant.cpp | 14 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 | ||||
-rw-r--r-- | src/theory/theory_model_builder.cpp | 2 |
3 files changed, 16 insertions, 3 deletions
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index 5c9daf784..64180c377 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -16,6 +16,7 @@ #include "expr/uninterpreted_constant.h" +#include <algorithm> #include <iostream> #include <sstream> #include <string> @@ -34,7 +35,18 @@ UninterpretedConstant::UninterpretedConstant(Type type, Integer index) } std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { - return out << "uc_" << uc.getType() << '_' << uc.getIndex(); + std::stringstream ss; + ss << uc.getType(); + std::string st(ss.str()); + // must remove delimiting quotes from the name of the type + // this prevents us from printing symbols like |@uc_|T|_n| + std::string q("|"); + size_t pos; + while ((pos = st.find(q)) != std::string::npos) + { + st.replace(pos, 1, ""); + } + return out << "uc_" << st.c_str() << "_" << uc.getIndex(); } }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index fd8b4ce85..dbb89d857 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1760,7 +1760,8 @@ static void toStreamRational(std::ostream& out, static void toStream(std::ostream& out, const DeclareTypeCommand* c) { - out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")"; + out << "(declare-sort " << maybeQuoteSymbol(c->getSymbol()) << " " + << c->getArity() << ")"; } static void toStream(std::ostream& out, const DefineTypeCommand* c) diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index b032dfec4..c4be41084 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1005,7 +1005,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) ufmt.simplify(); } std::stringstream ss; - ss << "_arg_" << f << "_"; + ss << "_arg_"; Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues); m->assignFunctionDefinition(f, val); // ufmt.debugPrint( std::cout, m ); |