Use symbol manager for printing responses get-model (#5516)

This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags.

This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model.

This is one of the last remaining steps for migrating the parser to the new API.

The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc.

1 files changed, 13 insertions, 6 deletions

diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index c93f3593a..f9384b0cb 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -54,20 +54,27 @@ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const
                                         : "CandidateFiniteModel");
   out << "% SZS output start " << statusName << " for " << m.getInputName()
       << endl;
-  for(size_t i = 0; i < m.getNumCommands(); ++i) {
-    this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i));
-  }
+  this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m);
   out << "% SZS output end " << statusName << " for " << m.getInputName()
       << endl;
 }
 
-void TptpPrinter::toStream(std::ostream& out,
-                           const smt::Model& m,
-                           const NodeCommand* c) const
+void TptpPrinter::toStreamModelSort(std::ostream& out,
+                                    const smt::Model& m,
+                                    TypeNode tn) const
+{
+  // shouldn't be called; only the non-Command* version above should be
+  Unreachable();
+}
+
+void TptpPrinter::toStreamModelTerm(std::ostream& out,
+                                    const smt::Model& m,
+                                    Node n) const
 {
   // shouldn't be called; only the non-Command* version above should be
   Unreachable();
 }
+
 void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const
 {
   out << "% SZS output start UnsatCore " << std::endl;