Dump commands in internal code using command printing functions. (#5040)

This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.

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;
 }
 
 /*