diff options
| -rw-r--r-- | src/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | src/api/cpp/cvc5.h | 3 | ||||
| -rw-r--r-- | src/options/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/options/base_options.toml | 23 | ||||
| -rw-r--r-- | src/options/managed_streams.cpp | 136 | ||||
| -rw-r--r-- | src/options/managed_streams.h | 139 | ||||
| -rw-r--r-- | src/options/open_ostream.cpp | 104 | ||||
| -rw-r--r-- | src/options/open_ostream.h | 61 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 34 | ||||
| -rw-r--r-- | src/options/options_handler.h | 13 | ||||
| -rw-r--r-- | src/options/options_public_template.cpp | 40 | ||||
| -rw-r--r-- | src/options/smt_options.toml | 18 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
| -rw-r--r-- | src/smt/managed_ostreams.cpp | 169 | ||||
| -rw-r--r-- | src/smt/managed_ostreams.h | 147 | ||||
| -rw-r--r-- | src/smt/options_manager.cpp | 24 | ||||
| -rw-r--r-- | src/smt/options_manager.h | 7 | ||||
| -rw-r--r-- | src/smt/set_defaults.cpp | 1 | ||||
| -rw-r--r-- | src/smt/update_ostream.h | 122 | ||||
| -rw-r--r-- | test/unit/main/interactive_shell_black.cpp | 5 |
20 files changed, 386 insertions, 669 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9eb7ec3c4..5ea99144b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -282,8 +282,6 @@ libcvc5_add_sources( smt/logic_exception.h smt/interpolation_solver.cpp smt/interpolation_solver.h - smt/managed_ostreams.cpp - smt/managed_ostreams.h smt/model.cpp smt/model.h smt/model_core_builder.cpp @@ -332,7 +330,6 @@ libcvc5_add_sources( smt/term_formula_removal.h smt/unsat_core_manager.cpp smt/unsat_core_manager.h - smt/update_ostream.h smt/witness_form.cpp smt/witness_form.h smt_util/boolean_simplification.cpp diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 0d8a268ae..25057ff2f 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4181,7 +4181,8 @@ class CVC5_EXPORT Solver void resetStatistics(); /** - * Print the statistics to the given file descriptor, suitable for usage in signal handlers. + * Print the statistics to the given file descriptor, suitable for usage in + * signal handlers. */ void printStatisticsSafe(int fd) const; diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index a548717f3..a75806504 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -22,8 +22,8 @@ libcvc5_add_sources( didyoumean.h language.cpp language.h - open_ostream.cpp - open_ostream.h + managed_streams.cpp + managed_streams.h option_exception.cpp option_exception.h options_handler.cpp diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 5eda4bb18..bdc369b60 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -5,23 +5,28 @@ public = true [[option]] name = "in" category = "undocumented" - type = "std::istream*" - default = "&std::cin" - includes = ["<iostream>"] + long = "in=input" + type = "ManagedIn" + predicates = ["setInStream"] + includes = ["<iostream>", "options/managed_streams.h"] [[option]] name = "out" category = "undocumented" - type = "std::ostream*" - default = "&std::cout" - includes = ["<iostream>"] + long = "out=output" + type = "ManagedOut" + alias = ["regular-output-channel"] + predicates = ["setOutStream"] + includes = ["<iostream>", "options/managed_streams.h"] [[option]] name = "err" category = "undocumented" - type = "std::ostream*" - default = "&std::cerr" - includes = ["<iostream>"] + long = "err=erroutput" + type = "ManagedErr" + alias = ["diagnostic-output-channel"] + predicates = ["setErrStream"] + includes = ["<iostream>", "options/managed_streams.h"] [[option]] name = "inputLanguage" diff --git a/src/options/managed_streams.cpp b/src/options/managed_streams.cpp new file mode 100644 index 000000000..5053db9a8 --- /dev/null +++ b/src/options/managed_streams.cpp @@ -0,0 +1,136 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Wrappers to handle memory management of streams. + * + * This file contains wrappers to handle special cases of managing memory + * related to streams stored in options. + */ + +#include "options/managed_streams.h" + +#include <string.h> + +#include <cerrno> +#include <fstream> +#include <iostream> +#include <sstream> + +#include "options/option_exception.h" + +namespace cvc5 { + +namespace detail { + +std::string cvc5_errno_failreason() +{ +#if HAVE_STRERROR_R +#if STRERROR_R_CHAR_P + if (errno != 0) + { + // GNU version of strerror_r: *might* use the given buffer, + // or might not. It returns a pointer to buf, or not. + char buf[80]; + return std::string(strerror_r(errno, buf, sizeof buf)); + } + else + { + return "unknown reason"; + } +#else /* STRERROR_R_CHAR_P */ + if (errno != 0) + { + // XSI version of strerror_r: always uses the given buffer. + // Returns an error code. + char buf[80]; + if (strerror_r(errno, buf, sizeof buf) == 0) + { + return std::string(buf); + } + else + { + // some error occurred while getting the error string + return "unknown reason"; + } + } + else + { + return "unknown reason"; + } +#endif /* STRERROR_R_CHAR_P */ +#else /* HAVE_STRERROR_R */ + return "unknown reason"; +#endif /* HAVE_STRERROR_R */ +} + +std::ostream* openOStream(const std::string& filename) +{ + errno = 0; + std::ostream* res; + res = new std::ofstream(filename); + if (res == nullptr || !*res) + { + std::stringstream ss; + ss << "Cannot open file: `" << filename << "': " << cvc5_errno_failreason(); + throw OptionException(ss.str()); + } + return res; +} +std::istream* openIStream(const std::string& filename) +{ + errno = 0; + std::istream* res; + res = new std::ifstream(filename); + if (res == nullptr || !*res) + { + std::stringstream ss; + ss << "Cannot open file: `" << filename << "': " << cvc5_errno_failreason(); + throw OptionException(ss.str()); + } + return res; +} +} // namespace detail + +std::ostream* ManagedErr::defaultValue() const { return &std::cerr; } +bool ManagedErr::specialCases(const std::string& value) +{ + if (value == "stderr" || value == "--") + { + d_stream.reset(); + return true; + } + return false; +} + +std::istream* ManagedIn::defaultValue() const { return &std::cin; } +bool ManagedIn::specialCases(const std::string& value) +{ + if (value == "stdin" || value == "--") + { + d_stream.reset(); + return true; + } + return false; +} + +std::ostream* ManagedOut::defaultValue() const { return &std::cout; } +bool ManagedOut::specialCases(const std::string& value) +{ + if (value == "stdout" || value == "--") + { + d_stream.reset(); + return true; + } + return false; +} + +} // namespace cvc5 diff --git a/src/options/managed_streams.h b/src/options/managed_streams.h new file mode 100644 index 000000000..f6fddc064 --- /dev/null +++ b/src/options/managed_streams.h @@ -0,0 +1,139 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Wrappers to handle memory management of streams. + * + * This file contains wrappers to handle special cases of managing memory + * related to streams stored in options. + */ + +#include "cvc5_public.h" + +#ifndef CVC5__OPTIONS__MANAGED_STREAMS_H +#define CVC5__OPTIONS__MANAGED_STREAMS_H + +#include <memory> +#include <ostream> + +#include "options/options_public.h" + +namespace cvc5 { + +namespace detail { +/* + * Open a file as an output stream and return it as a pointer. The caller + * assumes the ownership of the returned pointer. + */ +std::ostream* openOStream(const std::string& filename); +/* + * Open a file as an input stream and return it as a pointer. The caller + * assumes the ownership of the returned pointer. + */ +std::istream* openIStream(const std::string& filename); +} // namespace detail + +/** + * Implements memory management for streams, both input and output. It is + * intended to be subclassed, where a subclass can provide a default value and + * special cases. Usually, users should use one of these subclasses. + * The template argument type should be either std::istream or std::ostream, + * indicating whether the type wraps an input or output stream. + */ +template <typename Stream> +class ManagedStream +{ + public: + ManagedStream() {} + virtual ~ManagedStream() {} + + /** + * Open the stream from the given value. First check the special cases and + * then fall back to using `std::ofstream` or `std::ifstream`. + */ + void open(const std::string& value) + { + if (specialCases(value)) return; + if constexpr (std::is_same<Stream, std::ostream>::value) + { + d_stream.reset(detail::openOStream(value)); + } + else if constexpr (std::is_same<Stream, std::istream>::value) + { + d_stream.reset(detail::openIStream(value)); + } + } + + Stream& operator*() const { return *getPtr(); } + Stream* operator->() const { return getPtr(); } + operator Stream&() const { return *getPtr(); } + operator Stream*() const { return getPtr(); } + + protected: + std::shared_ptr<Stream> d_stream; + + private: + /** Returns the value to be used if d_stream is not set. */ + virtual Stream* defaultValue() const = 0; + /** + * Check if there is a special case for this value. If so, the implementation + * should set d_stream appropriately and return true to skip the default + * methods for opening a stream. + */ + virtual bool specialCases(const std::string& value) = 0; + + /** Return the pointer, either from d_stream of from defaultValue(). */ + Stream* getPtr() const + { + if (d_stream) return d_stream.get(); + return defaultValue(); + } +}; + +template <typename Stream> +std::ostream& operator<<(std::ostream& os, const ManagedStream<Stream>& ms) +{ + return os << "ManagedStream"; +} + +/** + * Managed error output. It recognizes "stderr" and "--" as special valued for + * std::cerr. + */ +class ManagedErr : public ManagedStream<std::ostream> +{ + std::ostream* defaultValue() const override final; + bool specialCases(const std::string& value) override final; +}; + +/** + * Managed standard input. It recognizes "stdin" and "--" as special valued for + * std::cin. + */ +class ManagedIn : public ManagedStream<std::istream> +{ + std::istream* defaultValue() const override final; + bool specialCases(const std::string& value) override final; +}; + +/** + * Managed standard output. It recognizes "stdout" and "--" as special valued + * for std::cout. + */ +class ManagedOut : public ManagedStream<std::ostream> +{ + std::ostream* defaultValue() const override final; + bool specialCases(const std::string& value) override final; +}; + +} // namespace cvc5 + +#endif /* CVC5__OPTIONS__MANAGED_STREAMS_H */ diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp deleted file mode 100644 index bb6efb5bc..000000000 --- a/src/options/open_ostream.cpp +++ /dev/null @@ -1,104 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, 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 "options/open_ostream.h" - -#include <cerrno> -#include <fstream> -#include <iostream> -#include <ostream> -#include <sstream> -#include <string> -#include <utility> - -#include "lib/strtok_r.h" -#include "options/option_exception.h" -#include "options/parser_options.h" - -namespace cvc5 { - -OstreamOpener::OstreamOpener(const char* channelName) - : d_channelName(channelName) - , d_specialCases() -{} - -void OstreamOpener::addSpecialCase(const std::string& name, std::ostream* out){ - d_specialCases[name] = out; -} - - - -std::pair< bool, std::ostream* > OstreamOpener::open(const std::string& optarg) const -{ - if(optarg == "") { - std::stringstream ss; - ss << "Bad file name setting for " << d_channelName; - throw OptionException(ss.str()); - } - if(d_specialCases.find(optarg) != d_specialCases.end()){ - return std::make_pair(false, (*d_specialCases.find(optarg)).second); - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - std::ostream* outStream; - outStream = new std::ofstream(optarg.c_str(), - std::ofstream::out | std::ofstream::trunc); - if(outStream == NULL || !*outStream) { - std::stringstream ss; - ss << "Cannot open " << d_channelName << " file: `" << optarg - << "': " << cvc5_errno_failreason(); - throw OptionException(ss.str()); - } - return make_pair(true, outStream); - } -} - -std::string cvc5_errno_failreason() -{ -#if HAVE_STRERROR_R -#if STRERROR_R_CHAR_P - if(errno != 0) { - // GNU version of strerror_r: *might* use the given buffer, - // or might not. It returns a pointer to buf, or not. - char buf[80]; - return std::string(strerror_r(errno, buf, sizeof buf)); - } else { - return "unknown reason"; - } -#else /* STRERROR_R_CHAR_P */ - if(errno != 0) { - // XSI version of strerror_r: always uses the given buffer. - // Returns an error code. - char buf[80]; - if(strerror_r(errno, buf, sizeof buf) == 0) { - return std::string(buf); - } else { - // some error occurred while getting the error string - return "unknown reason"; - } - } else { - return "unknown reason"; - } -#endif /* STRERROR_R_CHAR_P */ -#else /* HAVE_STRERROR_R */ - return "unknown reason"; -#endif /* HAVE_STRERROR_R */ -} - -} // namespace cvc5 diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h deleted file mode 100644 index 162bf3f11..000000000 --- a/src/options/open_ostream.h +++ /dev/null @@ -1,61 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Mathias Preiner - * - * 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_private.h" - -#ifndef CVC5__OPEN_OSTREAM_H -#define CVC5__OPEN_OSTREAM_H - -#include <iosfwd> -#include <map> -#include <string> -#include <utility> - -namespace cvc5 { - -class OstreamOpener { - public: - OstreamOpener(const char* channelName); - - void addSpecialCase(const std::string& name, std::ostream* out); - - /** - * If name == "", this throws OptionException with the message, messageIfEmpty. - * If name is a special case, this return <false, out> where out is the - * special case that was added. - * If name == "std::cerr", this return <false, &cerr>. - * If none of the previous conditions hold and !options::filesystemAccess(), - * this throws an OptionException. - * Otherwise, this attempts to open a ofstream using the filename, name. - * If this fails, this throws and OptionException. If this succeeds, this - * returns <true, stream> where stream is a ostream allocated by new. - * The caller is in this case the owner of the allocated memory. - */ - std::pair<bool, std::ostream*> open(const std::string& name) const; - - private: - const char* d_channelName; - std::map< std::string, std::ostream* > d_specialCases; - -}; /* class OstreamOpener */ - -std::string cvc5_errno_failreason(); - -} // namespace cvc5 - -#endif /* CVC5__OPEN_OSTREAM_H */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 7a80c4d7a..f5c80a758 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -35,6 +35,7 @@ #include "options/option_exception.h" #include "options/smt_options.h" #include "options/theory_options.h" +#include "smt/dump.h" namespace cvc5 { namespace options { @@ -549,6 +550,39 @@ InputLanguage OptionsHandler::stringToInputLanguage(const std::string& option, Unreachable(); } +void OptionsHandler::setDumpStream(const std::string& option, + const std::string& flag, + const ManagedOut& mo) +{ +#ifdef CVC5_DUMPING + Dump.setStream(mo); +#else /* CVC5_DUMPING */ + throw OptionException( + "The dumping feature was disabled in this build of cvc5."); +#endif /* CVC5_DUMPING */ +} +void OptionsHandler::setErrStream(const std::string& option, + const std::string& flag, + const ManagedErr& me) +{ + Debug.setStream(me); + Warning.setStream(me); + CVC5Message.setStream(me); + Notice.setStream(me); + Chat.setStream(me); + Trace.setStream(me); +} +void OptionsHandler::setInStream(const std::string& option, + const std::string& flag, + const ManagedIn& mi) +{ +} +void OptionsHandler::setOutStream(const std::string& option, + const std::string& flag, + const ManagedOut& mo) +{ +} + /* options/base_options_handlers.h */ void OptionsHandler::setVerbosity(const std::string& option, const std::string& flag, diff --git a/src/options/options_handler.h b/src/options/options_handler.h index a6fc97234..867d48a44 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -25,6 +25,7 @@ #include "options/bv_options.h" #include "options/decision_options.h" #include "options/language.h" +#include "options/managed_streams.h" #include "options/option_exception.h" #include "options/printer_modes.h" #include "options/quantifiers_options.h" @@ -137,6 +138,18 @@ public: void threadN(const std::string& option, const std::string& flag); /* options/base_options_handlers.h */ + void setDumpStream(const std::string& option, + const std::string& flag, + const ManagedOut& mo); + void setErrStream(const std::string& option, + const std::string& flag, + const ManagedErr& me); + void setInStream(const std::string& option, + const std::string& flag, + const ManagedIn& mi); + void setOutStream(const std::string& option, + const std::string& flag, + const ManagedOut& mo); void setVerbosity(const std::string& option, const std::string& flag, int value); diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp index 220445327..a744cf0a9 100644 --- a/src/options/options_public_template.cpp +++ b/src/options/options_public_template.cpp @@ -286,6 +286,46 @@ struct OptionHandler<T, false, false> { } };/* struct OptionHandler<T, false, false> */ +/** Specialization for ManagedErr */ +template <> +struct OptionHandler<ManagedErr, false, false> +{ + static ManagedErr handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { + ManagedErr res; + res.open(optionarg); + return res; + } +}; +/** Specialization for ManagedIn */ +template <> +struct OptionHandler<ManagedIn, false, false> +{ + static ManagedIn handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { + ManagedIn res; + res.open(optionarg); + return res; + } +}; +/** Specialization for ManagedOut */ +template <> +struct OptionHandler<ManagedOut, false, false> +{ + static ManagedOut handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { + ManagedOut res; + res.open(optionarg); + return res; + } +}; + /** Handle an option of type T in the default way. */ template <class T> T handleOption(const std::string& option, const std::string& flag, const std::string& optionarg) { diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index f7bd70a36..3a0e3e9f5 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -12,8 +12,10 @@ name = "SMT Layer" name = "dumpToFileName" category = "common" long = "dump-to=FILE" - type = "std::string" + type = "ManagedOut" help = "all dumping goes to FILE (instead of stdout)" + predicates = ["setDumpStream"] + includes = ["<iostream>", "options/managed_streams.h"] [[option]] name = "ackermann" @@ -375,20 +377,6 @@ name = "SMT Layer" help = "in models, use a witness constant for choice functions" [[option]] - name = "regularChannelName" - long = "regular-output-channel=CHANNEL" - category = "regular" - type = "std::string" - help = "set the regular output channel of the solver" - -[[option]] - name = "diagnosticChannelName" - long = "diagnostic-output-channel=CHANNEL" - category = "regular" - type = "std::string" - help = "set the diagnostic output channel of the solver" - -[[option]] name = "foreignTheoryRewrite" category = "regular" long = "foreign-theory-rewrite" diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c51d00b5d..c319e20e6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -648,7 +648,7 @@ void Smt2Printer::toStream(std::ostream& out, const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>(); out << "(_ root_predicate " << irp.d_index << ")"; break; - } + } // string theory case kind::REGEXP_REPEAT: diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp deleted file mode 100644 index b09448c11..000000000 --- a/src/smt/managed_ostreams.cpp +++ /dev/null @@ -1,169 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Aina Niemetz - * - * 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. - * **************************************************************************** - * - * Wrappers to handle memory management of ostreams. - * - * This file contains wrappers to handle special cases of managing memory - * related to ostreams. - */ - -#include "smt/managed_ostreams.h" - -#include <ostream> - -#include "base/check.h" -#include "options/open_ostream.h" -#include "options/option_exception.h" -#include "options/smt_options.h" -#include "smt/update_ostream.h" - -namespace cvc5 { - -ManagedOstream::ManagedOstream() : d_managed(NULL) {} - -ManagedOstream::~ManagedOstream() { - manage(NULL); - Assert(d_managed == NULL); -} - -void ManagedOstream::set(const std::string& filename) { - std::pair<bool, std::ostream*> pair = open(filename); - initialize(pair.second); - manage(pair.first ? pair.second : NULL); -} - -std::pair<bool, std::ostream*> ManagedOstream::open(const std::string& filename) - const { - OstreamOpener opener(getName()); - addSpecialCases(&opener); - return opener.open(filename); -} - -void ManagedOstream::manage(std::ostream* new_managed_value) { - if(d_managed == new_managed_value){ - // This is a no-op. - } else { - Assert(d_managed != new_managed_value); - std::ostream* old_managed_value = d_managed; - d_managed = new_managed_value; - if(old_managed_value != NULL){ - delete old_managed_value; - } - } -} - -ManagedDumpOStream::~ManagedDumpOStream() { - if(Dump.getStreamPointer() == getManagedOstream()) { - Dump.setStream(&null_os); - } -} - -std::string ManagedDumpOStream::defaultSource() const{ - return options::dumpToFileName(); -} - - -void ManagedDumpOStream::initialize(std::ostream* outStream) { -#ifdef CVC5_DUMPING - DumpOstreamUpdate dumpGetStream; - dumpGetStream.apply(outStream); -#else /* CVC5_DUMPING */ - throw OptionException( - "The dumping feature was disabled in this build of cvc5."); -#endif /* CVC5_DUMPING */ -} - -void ManagedDumpOStream::addSpecialCases(OstreamOpener* opener) const { - opener->addSpecialCase("-", &DumpOutC::dump_cout); -} - -ManagedRegularOutputChannel::~ManagedRegularOutputChannel() { - // Set all ostream that may still be using the old value of this channel - // to null_os. Consult RegularOutputChannelListener for the list of - // channels. - if(options::err() == getManagedOstream()){ - Options::current().base.err = &null_os; - } -} - -std::string ManagedRegularOutputChannel::defaultSource() const { - return options::regularChannelName(); -} - -void ManagedRegularOutputChannel::initialize(std::ostream* outStream) { - OptionsErrOstreamUpdate optionsErrOstreamUpdate; - optionsErrOstreamUpdate.apply(outStream); -} - -void ManagedRegularOutputChannel::addSpecialCases(OstreamOpener* opener) - const { - opener->addSpecialCase("stdout", &std::cout); - opener->addSpecialCase("stderr", &std::cerr); -} - -ManagedDiagnosticOutputChannel::~ManagedDiagnosticOutputChannel() { - // Set all ostreams that may still be using the old value of this channel - // to null_os. Consult DiagnosticOutputChannelListener for the list of - // channels. - if(options::err() == getManagedOstream()){ - Options::current().base.err = &null_os; - } - - if(Debug.getStreamPointer() == getManagedOstream()) { - Debug.setStream(&null_os); - } - if(Warning.getStreamPointer() == getManagedOstream()){ - Warning.setStream(&null_os); - } - if (CVC5Message.getStreamPointer() == getManagedOstream()) - { - CVC5Message.setStream(&null_os); - } - if(Notice.getStreamPointer() == getManagedOstream()){ - Notice.setStream(&null_os); - } - if(Chat.getStreamPointer() == getManagedOstream()){ - Chat.setStream(&null_os); - } - if(Trace.getStreamPointer() == getManagedOstream()){ - Trace.setStream(&null_os); - } -} - - -std::string ManagedDiagnosticOutputChannel::defaultSource() const { - return options::diagnosticChannelName(); -} -void ManagedDiagnosticOutputChannel::initialize(std::ostream* outStream) { - DebugOstreamUpdate debugOstreamUpdate; - debugOstreamUpdate.apply(outStream); - WarningOstreamUpdate warningOstreamUpdate; - warningOstreamUpdate.apply(outStream); - MessageOstreamUpdate messageOstreamUpdate; - messageOstreamUpdate.apply(outStream); - NoticeOstreamUpdate noticeOstreamUpdate; - noticeOstreamUpdate.apply(outStream); - ChatOstreamUpdate chatOstreamUpdate; - chatOstreamUpdate.apply(outStream); - TraceOstreamUpdate traceOstreamUpdate; - traceOstreamUpdate.apply(outStream); - OptionsErrOstreamUpdate optionsErrOstreamUpdate; - optionsErrOstreamUpdate.apply(outStream); -} - -void ManagedDiagnosticOutputChannel::addSpecialCases(OstreamOpener* opener) - const { - opener->addSpecialCase("stdout", &std::cout); - opener->addSpecialCase("stderr", &std::cerr); -} - -} // namespace cvc5 diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h deleted file mode 100644 index e04d7e9ba..000000000 --- a/src/smt/managed_ostreams.h +++ /dev/null @@ -1,147 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Mathias Preiner, Gereon Kremer - * - * 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. - * **************************************************************************** - * - * Wrappers to handle memory management of ostreams. - * - * This file contains wrappers to handle special cases of managing memory - * related to ostreams. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__MANAGED_OSTREAMS_H -#define CVC5__MANAGED_OSTREAMS_H - -#include <ostream> - -namespace cvc5 { - -class OstreamOpener; - -/** This abstracts the management of ostream memory and initialization. */ -class ManagedOstream { - public: - /** Initially getManagedOstream() == NULL. */ - ManagedOstream(); - virtual ~ManagedOstream(); - - /** Returns the pointer to the managed ostream. */ - std::ostream* getManagedOstream() const { return d_managed; } - - /** Returns the name of the ostream geing managed. */ - virtual const char* getName() const = 0; - - /** - * Set opens a file with filename, initializes the stream. - * If the opened ostream is marked as managed, this calls manage(stream). - * If the opened ostream is not marked as managed, this calls manage(NULL). - */ - void set(const std::string& filename); - - /** If this is associated with an option, return the string value. */ - virtual std::string defaultSource() const { return ""; } - - protected: - - /** - * Opens an ostream using OstreamOpener with the name getName() with the - * special cases added by addSpecialCases(). - */ - std::pair<bool, std::ostream*> open(const std::string& filename) const; - - /** - * Updates the value of managed pointer. Whenever this changes, - * beforeRelease() is called on the old value. - */ - void manage(std::ostream* new_managed_value); - - /** Initializes an output stream. Not necessarily managed. */ - virtual void initialize(std::ostream* outStream) {} - - /** Adds special cases to an ostreamopener. */ - virtual void addSpecialCases(OstreamOpener* opener) const {} - - private: - std::ostream* d_managed; -}; /* class ManagedOstream */ - -/** - * This controls the memory associated with --dump-to. - * This is is assumed to recieve a set whenever diagnosticChannelName - * is updated. - */ -class ManagedDumpOStream : public ManagedOstream { - public: - ManagedDumpOStream(){} - ~ManagedDumpOStream(); - - const char* getName() const override { return "dump-to"; } - std::string defaultSource() const override; - - protected: - /** Initializes an output stream. Not necessarily managed. */ - void initialize(std::ostream* outStream) override; - - /** Adds special cases to an ostreamopener. */ - void addSpecialCases(OstreamOpener* opener) const override; -};/* class ManagedDumpOStream */ - -/** - * When d_managedRegularChannel is non-null, it owns the memory allocated - * with the regular-output-channel. This is set when - * options::regularChannelName is set. - */ -class ManagedRegularOutputChannel : public ManagedOstream { - public: - ManagedRegularOutputChannel(){} - - /** Assumes Options are in scope. */ - ~ManagedRegularOutputChannel(); - - const char* getName() const override { return "regular-output-channel"; } - std::string defaultSource() const override; - - protected: - /** Initializes an output stream. Not necessarily managed. */ - void initialize(std::ostream* outStream) override; - - /** Adds special cases to an ostreamopener. */ - void addSpecialCases(OstreamOpener* opener) const override; -};/* class ManagedRegularOutputChannel */ - - -/** - * This controls the memory associated with diagnostic-output-channel. - * This is is assumed to recieve a set whenever options::diagnosticChannelName - * is updated. - */ -class ManagedDiagnosticOutputChannel : public ManagedOstream { - public: - ManagedDiagnosticOutputChannel(){} - - /** Assumes Options are in scope. */ - ~ManagedDiagnosticOutputChannel(); - - const char* getName() const override { return "diagnostic-output-channel"; } - std::string defaultSource() const override; - - protected: - /** Initializes an output stream. Not necessarily managed. */ - void initialize(std::ostream* outStream) override; - - /** Adds special cases to an ostreamopener. */ - void addSpecialCases(OstreamOpener* opener) const override; -};/* class ManagedRegularOutputChannel */ - -} // namespace cvc5 - -#endif /* CVC5__MANAGED_OSTREAMS_H */ diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 4d6be68b8..8bdbd7755 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -47,18 +47,6 @@ OptionsManager::OptionsManager(Options* opts) : d_options(opts) { notifySetOption(options::base::printSuccess__name); } - if (opts->smt.diagnosticChannelNameWasSetByUser) - { - notifySetOption(options::smt::diagnosticChannelName__name); - } - if (opts->smt.regularChannelNameWasSetByUser) - { - notifySetOption(options::smt::regularChannelName__name); - } - if (opts->smt.dumpToFileNameWasSetByUser) - { - notifySetOption(options::smt::dumpToFileName__name); - } // set this as a listener to be notified of options changes from now on opts->setListener(this); } @@ -107,18 +95,6 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << Command::printsuccess(value); *options::out() << Command::printsuccess(value); } - else if (key == options::smt::regularChannelName__name) - { - d_managedRegularChannel.set(options::regularChannelName()); - } - else if (key == options::smt::diagnosticChannelName__name) - { - d_managedDiagnosticChannel.set(options::diagnosticChannelName()); - } - else if (key == options::smt::dumpToFileName__name) - { - d_managedDumpChannel.set(options::dumpToFileName()); - } // otherwise, no action is necessary } diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h index 2201ceb40..e7c9d61cb 100644 --- a/src/smt/options_manager.h +++ b/src/smt/options_manager.h @@ -17,7 +17,6 @@ #define CVC5__SMT__OPTIONS_MANAGER_H #include "options/options_listener.h" -#include "smt/managed_ostreams.h" namespace cvc5 { @@ -65,12 +64,6 @@ class OptionsManager : public OptionsListener private: /** Reference to the options object */ Options* d_options; - /** Manager for the memory of regular-output-channel. */ - ManagedRegularOutputChannel d_managedRegularChannel; - /** Manager for the memory of diagnostic-output-channel. */ - ManagedDiagnosticOutputChannel d_managedDiagnosticChannel; - /** Manager for the memory of --dump-to. */ - ManagedDumpOStream d_managedDumpChannel; }; } // namespace smt diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 0a5c399ec..e23323e6d 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -27,7 +27,6 @@ #include "options/decision_options.h" #include "options/language.h" #include "options/main_options.h" -#include "options/open_ostream.h" #include "options/option_exception.h" #include "options/printer_options.h" #include "options/proof_options.h" diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h deleted file mode 100644 index 578fe5290..000000000 --- a/src/smt/update_ostream.h +++ /dev/null @@ -1,122 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Mathias Preiner, Aina Niemetz - * - * 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_private.h" - -#ifndef CVC5__UPDATE_OSTREAM_H -#define CVC5__UPDATE_OSTREAM_H - -#include <ostream> - -#include "base/check.h" -#include "base/output.h" -#include "expr/expr_iomanip.h" -#include "options/base_options.h" -#include "options/language.h" -#include "options/set_language.h" -#include "smt/dump.h" - -namespace cvc5 { - -class ChannelSettings { - public: - ChannelSettings(std::ostream& out) - : d_dagSetting(expr::ExprDag::getDag(out)), - d_exprDepthSetting(expr::ExprSetDepth::getDepth(out)), - d_languageSetting(language::SetLanguage::getLanguage(out)) - {} - - void apply(std::ostream& out) { - out << expr::ExprDag(d_dagSetting); - out << expr::ExprSetDepth(d_exprDepthSetting); - out << language::SetLanguage(d_languageSetting); - } - - private: - const int d_dagSetting; - const size_t d_exprDepthSetting; - const OutputLanguage d_languageSetting; -}; /* class ChannelSettings */ - -class OstreamUpdate { -public: - virtual ~OstreamUpdate(){} - - virtual std::ostream& get() = 0; - virtual void set(std::ostream* setTo) = 0; - - void apply(std::ostream* setTo) { - PrettyCheckArgument(setTo != NULL, setTo); - - ChannelSettings initialSettings(get()); - set(setTo); - initialSettings.apply(get()); - } -}; /* class OstreamUpdate */ - -class OptionsErrOstreamUpdate : public OstreamUpdate { - public: - std::ostream& get() override { return *(options::err()); } - void set(std::ostream* setTo) override { Options::current().base.err = setTo; } -}; /* class OptionsErrOstreamUpdate */ - -class DumpOstreamUpdate : public OstreamUpdate { - public: - std::ostream& get() override { return Dump.getStream(); } - void set(std::ostream* setTo) override { Dump.setStream(setTo); } -}; /* class DumpOstreamUpdate */ - -class DebugOstreamUpdate : public OstreamUpdate { - public: - std::ostream& get() override { return Debug.getStream(); } - void set(std::ostream* setTo) override { Debug.setStream(setTo); } -}; /* class DebugOstreamUpdate */ - -class WarningOstreamUpdate : public OstreamUpdate { - public: - std::ostream& get() override { return Warning.getStream(); } - void set(std::ostream* setTo) override { Warning.setStream(setTo); } -}; /* class WarningOstreamUpdate */ - -class MessageOstreamUpdate : public OstreamUpdate { - public: - std::ostream& get() override { return CVC5Message.getStream(); } - void set(std::ostream* setTo) override { CVC5Message.setStream(setTo); } -}; /* class MessageOstreamUpdate */ - -class NoticeOstreamUpdate : public OstreamUpdate { - public: - std::ostream& get() override { return Notice.getStream(); } - void set(std::ostream* setTo) override { Notice.setStream(setTo); } -}; /* class NoticeOstreamUpdate */ - -class ChatOstreamUpdate : public OstreamUpdate { - public: - std::ostream& get() override { return Chat.getStream(); } - void set(std::ostream* setTo) override { Chat.setStream(setTo); } -}; /* class ChatOstreamUpdate */ - -class TraceOstreamUpdate : public OstreamUpdate { - public: - std::ostream& get() override { return Trace.getStream(); } - void set(std::ostream* setTo) override { Trace.setStream(setTo); } -}; /* class TraceOstreamUpdate */ - -} // namespace cvc5 - -#endif /* CVC5__UPDATE_OSTREAM_H */ diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index 9c842adac..7b5f39f48 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -44,8 +44,8 @@ class TestMainBlackInteractiveShell : public TestInternal d_stdout = std::cout.rdbuf(); std::cout.rdbuf(d_sout->rdbuf()); - d_options.base.inputLanguage = language::input::LANG_CVC; - d_solver.reset(new cvc5::api::Solver(&d_options)); + d_solver.reset(new cvc5::api::Solver()); + d_solver->setOption("input-language", "cvc"); d_symman.reset(new SymbolManager(d_solver.get())); } @@ -87,7 +87,6 @@ class TestMainBlackInteractiveShell : public TestInternal std::unique_ptr<std::stringstream> d_sout; std::unique_ptr<SymbolManager> d_symman; std::unique_ptr<cvc5::api::Solver> d_solver; - Options d_options; std::streambuf* d_stdin; std::streambuf* d_stdout; |