Simplify model printing modes (#7049)

This removes the model printing mode options::ModelUninterpPrintMode::DtEnum which was previously used to print uninterpreted sorts as enumeration datatypes in the model. This mode was to my knowledge never used and moreover will not be easy to implement in the API.

This is work towards finalizing the API for models.

This PR also removes a file that I failed to delete in a recent PR.

1 files changed, 1 insertions, 32 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index be6cdd907..11959f37b 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1040,22 +1040,7 @@ void CvcPrinter::toStreamModelSort(std::ostream& out,
   }
   const theory::TheoryModel* tm = m.getTheoryModel();
   const std::vector<Node>* type_reps = tm->getRepSet()->getTypeRepsOrNull(tn);
-  if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
-      && type_reps != nullptr)
-  {
-    out << "DATATYPE" << std::endl;
-    out << "  " << tn << " = ";
-    for (size_t i = 0; i < type_reps->size(); i++)
-    {
-      if (i > 0)
-      {
-        out << "| ";
-      }
-      out << (*type_reps)[i] << " ";
-    }
-    out << std::endl << "END;" << std::endl;
-  }
-  else if (type_reps != nullptr)
+  if (type_reps != nullptr)
   {
     out << "% cardinality of " << tn << " is " << type_reps->size()
         << std::endl;
@@ -1105,22 +1090,6 @@ void CvcPrinter::toStreamModelTerm(std::ostream& out,
   // 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 (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum
-      && val.getKind() == kind::STORE)
-  {
-    TypeNode type_node = val[1].getType();
-    if (tn.isSort())
-    {
-      const std::vector<Node>* type_reps =
-          tm->getRepSet()->getTypeRepsOrNull(type_node);
-      if (type_reps != nullptr)
-      {
-        Cardinality indexCard(type_reps->size());
-        val = theory::arrays::TheoryArraysRewriter::normalizeConstant(
-            val, indexCard);
-      }
-    }
-  }
   out << " = " << val << ";" << std::endl;
 }