Add Driver options (#7078)

This PR adds a new API function Solver::getDriverOptions() which is used to communicate special options that (a) can not be properly communicated via getOption() and (b) need to be available in the driver (in a type-safe manner).
As of now, this concerns the input stream and output streams.
Furthermore, this PR refactors the driver to obtain them via the driver options instead of using the (deprecated) Solver::getOptions() method.

1 files changed, 35 insertions, 0 deletions

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 9f805fa65..d86fed14a 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2593,6 +2593,33 @@ struct CVC5_EXPORT hash<cvc5::api::RoundingMode>
 namespace cvc5::api {
 
 /* -------------------------------------------------------------------------- */
+/* Options                                                                    */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Provides access to options that can not be communicated via the regular
+ * getOption() or getOptionInfo() methods. This class does not store the options
+ * itself, but only acts as a wrapper to the solver object. It can thus no
+ * longer be used after the solver object has been destroyed.
+ */
+class CVC5_EXPORT DriverOptions
+{
+  friend class Solver;
+
+ public:
+  /** Access the solvers input stream */
+  std::istream& in() const;
+  /** Access the solvers error output stream */
+  std::ostream& err() const;
+  /** Access the solvers output stream */
+  std::ostream& out() const;
+
+ private:
+  DriverOptions(const Solver& solver);
+  const Solver& d_solver;
+};
+
+/* -------------------------------------------------------------------------- */
 /* Statistics                                                                 */
 /* -------------------------------------------------------------------------- */
 
@@ -2774,6 +2801,7 @@ class CVC5_EXPORT Solver
   friend class DatatypeConstructor;
   friend class DatatypeConstructorDecl;
   friend class DatatypeSelector;
+  friend class DriverOptions;
   friend class Grammar;
   friend class Op;
   friend class cvc5::Command;
@@ -3748,6 +3776,13 @@ class CVC5_EXPORT Solver
   std::vector<std::string> getOptionNames() const;
 
   /**
+   * Get the driver options, which provide access to options that can not be
+   * communicated properly via getOption() and getOptionInfo().
+   * @return a DriverOptions object.
+   */
+  DriverOptions getDriverOptions() const;
+
+  /**
    * Get the set of unsat ("failed") assumptions.
    * SMT-LIB:
    * \verbatim