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.

2 files changed, 19 insertions, 4 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 717d423fe..154166eb7 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1091,6 +1091,8 @@ void DeclareFunctionCommand::setPrintInModel(bool p)
 
 void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
+  // mark that it will be printed in the model
+  sm->addModelDeclarationTerm(d_func);
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -1132,6 +1134,8 @@ size_t DeclareSortCommand::getArity() const { return d_arity; }
 api::Sort DeclareSortCommand::getSort() const { return d_sort; }
 void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
+  // mark that it will be printed in the model
+  sm->addModelDeclarationSort(d_sort);
   d_commandStatus = CommandSuccess::instance();
 }
 
@@ -1150,8 +1154,8 @@ void DeclareSortCommand::toStream(std::ostream& out,
                                   size_t dag,
                                   OutputLanguage language) const
 {
-  Printer::getPrinter(language)->toStreamCmdDeclareType(
-      out, d_sort.toString(), d_arity, d_sort.getTypeNode());
+  Printer::getPrinter(language)->toStreamCmdDeclareType(out,
+                                                        d_sort.getTypeNode());
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1693,6 +1697,18 @@ void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
   try
   {
     d_result = solver->getSmtEngine()->getModel();
+    // set the model declarations, which determines what is printed in the model
+    d_result->clearModelDeclarations();
+    std::vector<api::Sort> declareSorts = sm->getModelDeclareSorts();
+    for (const api::Sort& s : declareSorts)
+    {
+      d_result->addDeclarationSort(s.getTypeNode());
+    }
+    std::vector<api::Term> declareTerms = sm->getModelDeclareTerms();
+    for (const api::Term& t : declareTerms)
+    {
+      d_result->addDeclarationTerm(t.getNode());
+    }
     d_commandStatus = CommandSuccess::instance();
   }
   catch (RecoverableModalException& e)
diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index eb2493c87..91184d27d 100644
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -104,8 +104,7 @@ void DeclareTypeNodeCommand::toStream(std::ostream& out,
                                       size_t dag,
                                       OutputLanguage language) const
 {
-  Printer::getPrinter(language)->toStreamCmdDeclareType(
-      out, d_id, d_arity, d_type);
+  Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type);
 }
 
 NodeCommand* DeclareTypeNodeCommand::clone() const