summaryrefslogtreecommitdiff
path: root/src/options/printer_modes.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-08-22 15:03:08 -0500
committerGitHub <noreply@github.com>2021-08-22 20:03:08 +0000
commit63bccca3e6e96e8e1ed92a25ca04f10d44858bff (patch)
tree9f91abfd5d19bcc092a0582ba54f0d2a98618ef1 /src/options/printer_modes.h
parent78e84e867417642b04da5c136ef548dfde8ca7f0 (diff)
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.
Diffstat (limited to 'src/options/printer_modes.h')
-rw-r--r--src/options/printer_modes.h45
1 files changed, 0 insertions, 45 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback