Refactor managed streams (#6934)

This PR introduces a new ManagedStream class that replaces the previous ManagedOstream. It allows to directly store the (wrapped) stream objects in the options. Handling the stream options is moved from the options manager to option predicates and the different options for input and output streams are combined into a single one.
Some associated utilities (open_ostream.h and update_ostream.h) are now obsolete and thus removed.

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;