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, 16 insertions, 11 deletions

diff --git a/src/printer/printer.h b/src/printer/printer.h
index d32418deb..5bcccedb8 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -86,8 +86,6 @@ class Printer
 
   /** Print declare-sort command */
   virtual void toStreamCmdDeclareType(std::ostream& out,
-                                      const std::string& id,
-                                      size_t arity,
                                       TypeNode type) const;
 
   /** Print define-sort command */
@@ -266,19 +264,26 @@ class Printer
   /** Derived classes can construct, but no one else. */
   Printer() {}
 
-  /** write model response to command */
-  virtual void toStream(std::ostream& out,
-                        const smt::Model& m,
-                        const NodeCommand* c) const = 0;
+  /**
+   * To stream model sort. This prints the appropriate output for type
+   * tn declared via declare-sort or declare-datatype.
+   */
+  virtual void toStreamModelSort(std::ostream& out,
+                                 const smt::Model& m,
+                                 TypeNode tn) const = 0;
+
+  /**
+   * To stream model term. This prints the appropriate output for term
+   * n declared via declare-fun.
+   */
+  virtual void toStreamModelTerm(std::ostream& out,
+                                 const smt::Model& m,
+                                 Node n) const = 0;
 
   /** write model response to command using another language printer */
   void toStreamUsing(OutputLanguage lang,
                      std::ostream& out,
-                     const smt::Model& m,
-                     const NodeCommand* c) const
-  {
-    getPrinter(lang)->toStream(out, m, c);
-  }
+                     const smt::Model& m) const;
 
   /**
    * Write an error to `out` stating that command `name` is not supported by