From 63bccca3e6e96e8e1ed92a25ca04f10d44858bff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 22 Aug 2021 15:03:08 -0500 Subject: [PATCH] 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. --- src/CMakeLists.txt | 2 -- src/options/options_handler.h | 6 ----- src/options/printer_modes.cpp | 35 ------------------------ src/options/printer_modes.h | 45 ------------------------------- src/options/smt_options.toml | 5 +--- src/printer/cvc/cvc_printer.cpp | 33 +---------------------- src/printer/smt2/smt2_printer.cpp | 23 ---------------- 7 files changed, 2 insertions(+), 147 deletions(-) delete mode 100644 src/options/printer_modes.cpp delete mode 100644 src/options/printer_modes.h 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 - -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* 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* 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 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* 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()); -- 2.30.2