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.
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
#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 {
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.
+++ /dev/null
-/******************************************************************************
- * 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
+++ /dev/null
-/******************************************************************************
- * 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 */
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"
}
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;
// 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;
}
}
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()
}
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());
projects / cvc5.git / commitdiff