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, 87 insertions, 107 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 747873bee..9e9500bdb 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1364,124 +1364,91 @@ void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const
   }
 }
 
-void Smt2Printer::toStream(std::ostream& out,
-                           const smt::Model& model,
-                           const NodeCommand* command) const
+void Smt2Printer::toStreamModelSort(std::ostream& out,
+                                    const smt::Model& m,
+                                    TypeNode tn) const
 {
-  const theory::TheoryModel* theory_model = model.getTheoryModel();
-  AlwaysAssert(theory_model != nullptr);
-  if (const DeclareTypeNodeCommand* dtc =
-          dynamic_cast<const DeclareTypeNodeCommand*>(command))
+  if (!tn.isSort())
   {
-    // print out the DeclareTypeCommand
-    TypeNode tn = dtc->getType();
-    if (!tn.isSort())
+    out << "ERROR: don't know how to print non uninterpreted sort in model: "
+        << tn << std::endl;
+    return;
+  }
+  const theory::TheoryModel* tm = m.getTheoryModel();
+  std::vector<Node> elements = tm->getDomainElements(tn);
+  if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum)
+  {
+    if (isVariant_2_6(d_variant))
     {
-      out << (*dtc) << endl;
+      out << "(declare-datatypes ((" << tn << " 0)) (";
     }
     else
     {
-      std::vector<Node> elements = theory_model->getDomainElements(tn);
-      if (options::modelUninterpPrint()
-          == options::ModelUninterpPrintMode::DtEnum)
-      {
-        if (isVariant_2_6(d_variant))
-        {
-          out << "(declare-datatypes ((" << (*dtc).getSymbol() << " 0)) (";
-        }
-        else
-        {
-          out << "(declare-datatypes () ((" << (*dtc).getSymbol() << " ";
-        }
-        for (const Node& type_ref : elements)
-        {
-          out << "(" << type_ref << ")";
-        }
-        out << ")))" << endl;
-      }
-      else
-      {
-        // print the cardinality
-        out << "; cardinality of " << tn << " is " << elements.size() << endl;
-        if (options::modelUninterpPrint()
-            == options::ModelUninterpPrintMode::DeclSortAndFun)
-        {
-          out << (*dtc) << endl;
-        }
-        // print the representatives
-        for (const Node& trn : elements)
-        {
-          if (trn.isVar())
-          {
-            out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")"
-                << endl;
-          }
-          else
-          {
-            out << "; rep: " << trn << endl;
-          }
-        }
-      }
-    }
-  }
-  else if (const DeclareFunctionNodeCommand* dfc =
-               dynamic_cast<const DeclareFunctionNodeCommand*>(command))
-  {
-    // print out the DeclareFunctionCommand
-    Node n = dfc->getFunction();
-    if ((*dfc).getPrintInModelSetByUser())
-    {
-      if (!(*dfc).getPrintInModel())
-      {
-        return;
-      }
+      out << "(declare-datatypes () ((" << tn << " ";
     }
-    else if (n.getKind() == kind::SKOLEM)
+    for (const Node& type_ref : elements)
     {
-      // don't print out internal stuff
-      return;
+      out << "(" << type_ref << ")";
     }
-    // We get the value from the theory model directly, which notice
-    // does not have to go through the standard SmtEngine::getValue interface.
-    Node val = theory_model->getValue(n);
-    if (val.getKind() == kind::LAMBDA)
+    out << ")))" << endl;
+    return;
+  }
+  // print the cardinality
+  out << "; cardinality of " << tn << " is " << elements.size() << endl;
+  if (options::modelUninterpPrint()
+      == options::ModelUninterpPrintMode::DeclSortAndFun)
+  {
+    toStreamCmdDeclareType(out, tn);
+  }
+  // print the representatives
+  for (const Node& trn : elements)
+  {
+    if (trn.isVar())
     {
-      TypeNode rangeType = n.getType().getRangeType();
-      out << "(define-fun " << n << " " << val[0] << " " << rangeType << " ";
-      // call toStream and force its type to be proper
-      toStreamCastToType(out, val[1], -1, rangeType);
-      out << ")" << endl;
+      out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")" << endl;
     }
     else
     {
-      if (options::modelUninterpPrint()
-              == options::ModelUninterpPrintMode::DtEnum
-          && val.getKind() == kind::STORE)
-      {
-        TypeNode tn = val[1].getType();
-        const std::vector<Node>* type_refs =
-            theory_model->getRepSet()->getTypeRepsOrNull(tn);
-        if (tn.isSort() && type_refs != nullptr)
-        {
-          Cardinality indexCard(type_refs->size());
-          val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
-              val, indexCard);
-        }
-      }
-      out << "(define-fun " << n << " () " << n.getType() << " ";
-      // call toStream and force its type to be proper
-      toStreamCastToType(out, val, -1, n.getType());
-      out << ")" << endl;
+      out << "; rep: " << trn << endl;
     }
   }
-  else if (const DeclareDatatypeNodeCommand* declare_datatype_command =
-               dynamic_cast<const DeclareDatatypeNodeCommand*>(command))
+}
+
+void Smt2Printer::toStreamModelTerm(std::ostream& out,
+                                    const smt::Model& m,
+                                    Node n) const
+{
+  const theory::TheoryModel* tm = m.getTheoryModel();
+  // We get the value from the theory model directly, which notice
+  // does not have to go through the standard SmtEngine::getValue interface.
+  Node val = tm->getValue(n);
+  if (val.getKind() == kind::LAMBDA)
   {
-    out << *declare_datatype_command;
+    TypeNode rangeType = n.getType().getRangeType();
+    out << "(define-fun " << n << " " << val[0] << " " << rangeType << " ";
+    // call toStream and force its type to be proper
+    toStreamCastToType(out, val[1], -1, rangeType);
+    out << ")" << endl;
   }
   else
   {
-    Unreachable();
+    if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
+        && val.getKind() == kind::STORE)
+    {
+      TypeNode tn = val[1].getType();
+      const std::vector<Node>* type_refs =
+          tm->getRepSet()->getTypeRepsOrNull(tn);
+      if (tn.isSort() && type_refs != nullptr)
+      {
+        Cardinality indexCard(type_refs->size());
+        val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
+            val, indexCard);
+      }
+    }
+    out << "(define-fun " << n << " () " << n.getType() << " ";
+    // call toStream and force its type to be proper
+    toStreamCastToType(out, val, -1, n.getType());
+    out << ")" << endl;
   }
 }
 
@@ -1694,11 +1661,13 @@ void Smt2Printer::toStreamCmdDefineFunctionRec(
 }
 
 void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
-                                         const std::string& id,
-                                         size_t arity,
                                          TypeNode type) const
 {
-  out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")"
+  Assert(type.isSort() || type.isSortConstructor());
+  std::stringstream id;
+  id << type;
+  size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0;
+  out << "(declare-sort " << CVC4::quoteSymbol(id.str()) << " " << arity << ")"
       << std::endl;
 }
 
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index c83a74d97..3d90cee06 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -78,8 +78,6 @@ class Smt2Printer : public CVC4::Printer
 
   /** Print declare-sort command */
   void toStreamCmdDeclareType(std::ostream& out,
-                              const std::string& id,
-                              size_t arity,
                               TypeNode type) const override;
 
   /** Print define-sort command */
@@ -243,12 +241,25 @@ class Smt2Printer : public CVC4::Printer
                           TNode n,
                           int toDepth,
                           TypeNode tn) const;
-  void toStream(std::ostream& out,
-                const smt::Model& m,
-                const NodeCommand* c) const override;
   void toStream(std::ostream& out, const SExpr& sexpr) const;
   void toStream(std::ostream& out, const DType& dt) const;
   /**
+   * To stream model sort. This prints the appropriate output for type
+   * tn declared via declare-sort or declare-datatype.
+   */
+  void toStreamModelSort(std::ostream& out,
+                         const smt::Model& m,
+                         TypeNode tn) const override;
+
+  /**
+   * To stream model term. This prints the appropriate output for term
+   * n declared via declare-fun.
+   */
+  void toStreamModelTerm(std::ostream& out,
+                         const smt::Model& m,
+                         Node n) const override;
+
+  /**
    * To stream with let binding. This prints n, possibly in the scope
    * of letification generated by this method based on lbind.
    */