diff options
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/options/options_handler.h | 6 | ||||
-rw-r--r-- | src/options/printer_modes.cpp | 35 | ||||
-rw-r--r-- | src/options/printer_modes.h | 45 | ||||
-rw-r--r-- | src/options/smt_options.toml | 5 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 33 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 23 |
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()); |