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.

2 files changed, 1 insertions, 55 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;
 }
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c319e20e6..04d8c34c4 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1294,16 +1294,6 @@ void Smt2Printer::toStreamModelSort(std::ostream& out,
   }
   const theory::TheoryModel* tm = m.getTheoryModel();
   std::vector<Node> elements = tm->getDomainElements(tn);
-  if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum)
-  {
-    out << "(declare-datatypes ((" << tn << " 0)) (";
-    for (const Node& type_ref : elements)
-    {
-      out << "(" << type_ref << ")";
-    }
-    out << ")))" << endl;
-    return;
-  }
   // print the cardinality
   out << "; cardinality of " << tn << " is " << elements.size() << endl;
   if (options::modelUninterpPrint()
@@ -1350,19 +1340,6 @@ void Smt2Printer::toStreamModelTerm(std::ostream& out,
   }
   else
   {
-    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());