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.

4 files changed, 1 insertions, 90 deletions

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"