summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/options/options_handler.h6
-rw-r--r--src/options/printer_modes.cpp35
-rw-r--r--src/options/printer_modes.h45
-rw-r--r--src/options/smt_options.toml5
-rw-r--r--src/printer/cvc/cvc_printer.cpp33
-rw-r--r--src/printer/smt2/smt2_printer.cpp23
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());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback