diff options
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 68 |
1 files changed, 41 insertions, 27 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 02afa715d..46b509388 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1203,12 +1203,18 @@ void CvcPrinter::toStream(std::ostream& out, void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const { - out << "ASSERT " << n << ';'; + out << "ASSERT " << n << ';' << std::endl; } -void CvcPrinter::toStreamCmdPush(std::ostream& out) const { out << "PUSH;"; } +void CvcPrinter::toStreamCmdPush(std::ostream& out) const +{ + out << "PUSH;" << std::endl; +} -void CvcPrinter::toStreamCmdPop(std::ostream& out) const { out << "POP;"; } +void CvcPrinter::toStreamCmdPop(std::ostream& out) const +{ + out << "POP;" << std::endl; +} void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const { @@ -1228,6 +1234,7 @@ void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const { out << " POP;"; } + out << std::endl; } void CvcPrinter::toStreamCmdCheckSatAssuming( @@ -1251,6 +1258,7 @@ void CvcPrinter::toStreamCmdCheckSatAssuming( { out << " POP;"; } + out << std::endl; } void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const @@ -1271,18 +1279,22 @@ void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const { out << " POP;"; } + out << std::endl; } -void CvcPrinter::toStreamCmdReset(std::ostream& out) const { out << "RESET;"; } +void CvcPrinter::toStreamCmdReset(std::ostream& out) const +{ + out << "RESET;" << std::endl; +} void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const { - out << "RESET ASSERTIONS;"; + out << "RESET ASSERTIONS;" << std::endl; } void CvcPrinter::toStreamCmdQuit(std::ostream& out) const { - // out << "EXIT;"; + // out << "EXIT;" << std::endl; } void CvcPrinter::toStreamCmdCommandSequence( @@ -1292,7 +1304,7 @@ void CvcPrinter::toStreamCmdCommandSequence( i != sequence.cend(); ++i) { - out << *i << endl; + out << *i; } } @@ -1314,13 +1326,14 @@ void CvcPrinter::toStreamCmdDeclarationSequence( break; } } + out << std::endl; } void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out, const std::string& id, TypeNode type) const { - out << id << " : " << type << ';'; + out << id << " : " << type << ';' << std::endl; } void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out, @@ -1353,7 +1366,7 @@ void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out, } out << "): "; } - out << formula << ';'; + out << formula << ';' << std::endl; } void CvcPrinter::toStreamCmdDeclareType(std::ostream& out, @@ -1370,7 +1383,7 @@ void CvcPrinter::toStreamCmdDeclareType(std::ostream& out, } else { - out << id << " : TYPE;"; + out << id << " : TYPE;" << std::endl; } } @@ -1387,7 +1400,7 @@ void CvcPrinter::toStreamCmdDefineType(std::ostream& out, } else { - out << id << " : TYPE = " << t << ';'; + out << id << " : TYPE = " << t << ';' << std::endl; } } @@ -1403,7 +1416,7 @@ void CvcPrinter::toStreamCmdDefineNamedFunction( void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const { - out << "TRANSFORM " << n << ';'; + out << "TRANSFORM " << n << ';' << std::endl; } void CvcPrinter::toStreamCmdGetValue(std::ostream& out, @@ -1414,44 +1427,44 @@ void CvcPrinter::toStreamCmdGetValue(std::ostream& out, copy(nodes.begin(), nodes.end() - 1, ostream_iterator<Node>(out, ";\nGET_VALUE ")); - out << nodes.back() << ';'; + out << nodes.back() << ';' << std::endl; } void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const { - out << "COUNTERMODEL;"; + out << "COUNTERMODEL;" << std::endl; } void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const { - out << "% (get-assignment)"; + out << "% (get-assignment)" << std::endl; } void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const { - out << "WHERE;"; + out << "WHERE;" << std::endl; } void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const { - out << "DUMP_PROOF;"; + out << "DUMP_PROOF;" << std::endl; } void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const { - out << "DUMP_UNSAT_CORE;"; + out << "DUMP_UNSAT_CORE;" << std::endl; } void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out, Result::Sat status) const { - out << "% (set-info :status " << status << ')'; + out << "% (set-info :status " << status << ')' << std::endl; } void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out, const std::string& logic) const { - out << "OPTION \"logic\" \"" << logic << "\";"; + out << "OPTION \"logic\" \"" << logic << "\";" << std::endl; } void CvcPrinter::toStreamCmdSetInfo(std::ostream& out, @@ -1462,13 +1475,13 @@ void CvcPrinter::toStreamCmdSetInfo(std::ostream& out, OutputLanguage language = d_cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4; SExpr::toStream(out, sexpr, language); - out << ')'; + out << ')' << std::endl; } void CvcPrinter::toStreamCmdGetInfo(std::ostream& out, const std::string& flag) const { - out << "% (get-info " << flag << ')'; + out << "% (get-info " << flag << ')' << std::endl; } void CvcPrinter::toStreamCmdSetOption(std::ostream& out, @@ -1477,13 +1490,13 @@ void CvcPrinter::toStreamCmdSetOption(std::ostream& out, { out << "OPTION \"" << flag << "\" "; SExpr::toStream(out, sexpr, language::output::LANG_CVC4); - out << ';'; + out << ';' << std::endl; } void CvcPrinter::toStreamCmdGetOption(std::ostream& out, const std::string& flag) const { - out << "% (get-option " << flag << ')'; + out << "% (get-option " << flag << ')' << std::endl; } void CvcPrinter::toStreamCmdDatatypeDeclaration( @@ -1552,25 +1565,26 @@ void CvcPrinter::toStreamCmdDatatypeDeclaration( } firstDatatype = false; } - out << endl << "END;"; + out << endl << "END;" << std::endl; } } void CvcPrinter::toStreamCmdComment(std::ostream& out, const std::string& comment) const { - out << "% " << comment; + out << "% " << comment << std::endl; } void CvcPrinter::toStreamCmdEmpty(std::ostream& out, const std::string& name) const { + out << std::endl; } void CvcPrinter::toStreamCmdEcho(std::ostream& out, const std::string& output) const { - out << "ECHO \"" << output << "\";"; + out << "ECHO \"" << output << "\";" << std::endl; } template <class T> |