diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 95 |
1 files changed, 46 insertions, 49 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2cc6c8973..7ef02c576 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1451,15 +1451,18 @@ void Smt2Printer::toStream(std::ostream& out, void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const { - out << "(assert " << n << ')'; + out << "(assert " << n << ')' << std::endl; } void Smt2Printer::toStreamCmdPush(std::ostream& out) const { - out << "(push 1)"; + out << "(push 1)" << std::endl; } -void Smt2Printer::toStreamCmdPop(std::ostream& out) const { out << "(pop 1)"; } +void Smt2Printer::toStreamCmdPop(std::ostream& out) const +{ + out << "(pop 1)" << std::endl; +} void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const { @@ -1477,6 +1480,7 @@ void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const { out << "(check-sat)"; } + out << std::endl; } void Smt2Printer::toStreamCmdCheckSatAssuming( @@ -1484,7 +1488,7 @@ void Smt2Printer::toStreamCmdCheckSatAssuming( { out << "(check-sat-assuming ( "; copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " ")); - out << "))"; + out << "))" << std::endl; } void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const @@ -1508,34 +1512,25 @@ void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const void Smt2Printer::toStreamCmdReset(std::ostream& out) const { - out << "(reset)"; + out << "(reset)" << std::endl; } void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const { - out << "(reset-assertions)"; + out << "(reset-assertions)" << std::endl; } -void Smt2Printer::toStreamCmdQuit(std::ostream& out) const { out << "(exit)"; } +void Smt2Printer::toStreamCmdQuit(std::ostream& out) const +{ + out << "(exit)" << std::endl; +} void Smt2Printer::toStreamCmdCommandSequence( std::ostream& out, const std::vector<Command*>& sequence) const { - CommandSequence::const_iterator i = sequence.cbegin(); - if (i != sequence.cend()) + for (Command* i : sequence) { - for (;;) - { - out << *i; - if (++i != sequence.cend()) - { - out << endl; - } - else - { - break; - } - } + out << *i; } } @@ -1563,7 +1558,7 @@ void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out, type = type.getRangeType(); } - out << ") " << type << ')'; + out << ") " << type << ')' << std::endl; } void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out, @@ -1590,7 +1585,7 @@ void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out, } } } - out << ") " << range << ' ' << formula << ')'; + out << ") " << range << ' ' << formula << ')' << std::endl; } void Smt2Printer::toStreamCmdDefineFunctionRec( @@ -1659,7 +1654,7 @@ void Smt2Printer::toStreamCmdDefineFunctionRec( { out << ")"; } - out << ")"; + out << ")" << std::endl; } static void toStreamRational(std::ostream& out, @@ -1704,7 +1699,8 @@ void Smt2Printer::toStreamCmdDeclareType(std::ostream& out, size_t arity, TypeNode type) const { - out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")"; + out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")" + << std::endl; } void Smt2Printer::toStreamCmdDefineType(std::ostream& out, @@ -1719,7 +1715,7 @@ void Smt2Printer::toStreamCmdDefineType(std::ostream& out, params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " ")); out << params.back(); } - out << ") " << t << ")"; + out << ") " << t << ")" << std::endl; } void Smt2Printer::toStreamCmdDefineNamedFunction( @@ -1738,7 +1734,7 @@ void Smt2Printer::toStreamCmdDefineNamedFunction( void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const { - out << "(simplify " << n << ')'; + out << "(simplify " << n << ')' << std::endl; } void Smt2Printer::toStreamCmdGetValue(std::ostream& out, @@ -1746,49 +1742,49 @@ void Smt2Printer::toStreamCmdGetValue(std::ostream& out, { out << "(get-value ( "; copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " ")); - out << "))"; + out << "))" << std::endl; } void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const { - out << "(get-model)"; + out << "(get-model)" << std::endl; } void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const { - out << "(get-assignment)"; + out << "(get-assignment)" << std::endl; } void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const { - out << "(get-assertions)"; + out << "(get-assertions)" << std::endl; } void Smt2Printer::toStreamCmdGetProof(std::ostream& out) const { - out << "(get-proof)"; + out << "(get-proof)" << std::endl; } void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const { - out << "(get-unsat-assumptions)"; + out << "(get-unsat-assumptions)" << std::endl; } void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const { - out << "(get-unsat-core)"; + out << "(get-unsat-core)" << std::endl; } void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out, Result::Sat status) const { - out << "(set-info :status " << status << ')'; + out << "(set-info :status " << status << ')' << std::endl; } void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out, const std::string& logic) const { - out << "(set-logic " << logic << ')'; + out << "(set-logic " << logic << ')' << std::endl; } void Smt2Printer::toStreamCmdSetInfo(std::ostream& out, @@ -1797,13 +1793,13 @@ void Smt2Printer::toStreamCmdSetInfo(std::ostream& out, { out << "(set-info :" << flag << ' '; SExpr::toStream(out, sexpr, variantToLanguage(d_variant)); - out << ')'; + out << ')' << std::endl; } void Smt2Printer::toStreamCmdGetInfo(std::ostream& out, const std::string& flag) const { - out << "(get-info :" << flag << ')'; + out << "(get-info :" << flag << ')' << std::endl; } void Smt2Printer::toStreamCmdSetOption(std::ostream& out, @@ -1812,13 +1808,13 @@ void Smt2Printer::toStreamCmdSetOption(std::ostream& out, { out << "(set-option :" << flag << ' '; SExpr::toStream(out, sexpr, language::output::LANG_SMTLIB_V2_5); - out << ')'; + out << ')' << std::endl; } void Smt2Printer::toStreamCmdGetOption(std::ostream& out, const std::string& flag) const { - out << "(get-option :" << flag << ')'; + out << "(get-option :" << flag << ')' << std::endl; } void Smt2Printer::toStream(std::ostream& out, const DType& dt) const @@ -1951,7 +1947,7 @@ void Smt2Printer::toStreamCmdDatatypeDeclaration( } out << ")"; } - out << ")" << endl; + out << ")" << std::endl; } void Smt2Printer::toStreamCmdComment(std::ostream& out, @@ -1964,12 +1960,13 @@ void Smt2Printer::toStreamCmdComment(std::ostream& out, s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\""); pos += 2; } - out << "(set-info :notes \"" << s << "\")"; + out << "(set-info :notes \"" << s << "\")" << std::endl; } void Smt2Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const { + out << std::endl; } void Smt2Printer::toStreamCmdEcho(std::ostream& out, @@ -1983,7 +1980,7 @@ void Smt2Printer::toStreamCmdEcho(std::ostream& out, s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\""); pos += 2; } - out << "(echo \"" << s << "\")"; + out << "(echo \"" << s << "\")" << std::endl; } /* @@ -2084,31 +2081,31 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out, { toStreamSygusGrammar(out, sygusType); } - out << ')'; + out << ')' << std::endl; } void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out, Node var, TypeNode type) const { - out << "(declare-var " << var << ' ' << type << ')'; + out << "(declare-var " << var << ' ' << type << ')' << std::endl; } void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const { - out << "(constraint " << n << ')'; + out << "(constraint " << n << ')' << std::endl; } void Smt2Printer::toStreamCmdInvConstraint( std::ostream& out, Node inv, Node pre, Node trans, Node post) const { out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post - << ')'; + << ')' << std::endl; } void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const { - out << "(check-synth)"; + out << "(check-synth)" << std::endl; } void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out, @@ -2125,7 +2122,7 @@ void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out, { toStreamSygusGrammar(out, sygusType); } - out << ')'; + out << ')' << std::endl; } /* |