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.

7 files changed, 2 insertions, 147 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2aa91f61b..9d887cc63 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -65,8 +65,6 @@ libcvc5_add_sources(
   options/options_public.h
   options/outputc.cpp
   options/outputc.h
-  options/printer_modes.cpp
-  options/printer_modes.h
   options/set_language.cpp
   options/set_language.h
   preprocessing/assertion_pipeline.cpp
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index d6b81525d..ba3951c00 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -27,7 +27,6 @@
 #include "options/language.h"
 #include "options/managed_streams.h"
 #include "options/option_exception.h"
-#include "options/printer_modes.h"
 #include "options/quantifiers_options.h"
 
 namespace cvc5 {
@@ -100,11 +99,6 @@ public:
                       const std::string& flag,
                       bool arg);
 
-  // printer/options_handlers.h
-  InstFormatMode stringToInstFormatMode(const std::string& option,
-                                        const std::string& flag,
-                                        const std::string& optarg);
-
   /**
    * Throws a ModalException if this option is being set after final
    * initialization.
diff --git a/src/options/printer_modes.cpp b/src/options/printer_modes.cpp
deleted file mode 100644
index b2d8ec79a..000000000
--- a/src/options/printer_modes.cpp
+++ /dev/null
@@ -1,35 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Mathias Preiner, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "options/printer_modes.h"
-
-namespace cvc5::options {
-
-std::ostream& operator<<(std::ostream& out, InstFormatMode mode)
-{
-  out << "InstFormatMode::";
-  switch (mode)
-  {
-    case options::InstFormatMode::DEFAULT: out << "DEFAULT"; break;
-    case options::InstFormatMode::SZS: out << "SZS"; break;
-    default: out << "UNKNOWN![" << unsigned(mode) << "]";
-  }
-  return out;
-}
-
-}  // namespace cvc5
diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h
deleted file mode 100644
index 093bff7d9..000000000
--- a/src/options/printer_modes.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Mathias Preiner, Andrew Reynolds, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__PRINTER__MODES_H
-#define CVC5__PRINTER__MODES_H
-
-#include <iostream>
-
-namespace cvc5 {
-namespace options {
-
-/** Enumeration of inst_format modes (how to print models from get-model
- * command). */
-enum class InstFormatMode
-{
-  /** default mode (print expressions in the output language format) */
-  DEFAULT,
-  /** print as SZS proof */
-  SZS,
-};
-
-std::ostream& operator<<(std::ostream& out, InstFormatMode mode);
-
-}  // namespace options
-
-}  // namespace cvc5
-
-#endif /* CVC5__PRINTER__MODEL_FORMAT_H */
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 8094b5a6b..e461b803a 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -354,10 +354,7 @@ name   = "SMT Layer"
   type       = "ModelUninterpPrintMode"
   default    = "None"
   help       = "determines how to print uninterpreted elements in models"
-  help_mode  = "uninterpreted elements in models printing  modes."
-[[option.mode.DtEnum]]
-  name = "dtenum"
-  help = "print uninterpreted elements as datatype enumerations, where the sort is the datatype"
+  help_mode  = "uninterpreted elements in models printing modes."
 [[option.mode.DeclSortAndFun]]
   name = "decl-sort-and-fun"
   help = "print uninterpreted elements declare-fun, and also include a declare-sort for the sort"
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());