Clean up option usage in command executor (#6844)

This PR makes the CommandExecutor class use the options object from its SmtEngine instead of the driver one. This makes sure that options that are set via (set-option ...) are in effect for the CommandExecutor. It still stores the driver options, though, as they are used for resets.
The PR also does some minor cleanups along the way (remove unused pOptions, make things const).
Fixes #2376.

2 files changed, 7 insertions, 2 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 5a34f1453..4e14b8e34 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4742,7 +4742,7 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats)
 /* Solver                                                                     */
 /* -------------------------------------------------------------------------- */
 
-Solver::Solver(Options* opts)
+Solver::Solver(const Options* opts)
 {
   d_nodeMgr.reset(new NodeManager());
   d_originalOptions.reset(new Options());
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 161522654..0ee5990da 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -49,6 +49,10 @@ class Random;
 class Result;
 class StatisticsRegistry;
 
+namespace main {
+class CommandExecutor;
+}
+
 namespace api {
 
 class Solver;
@@ -2725,6 +2729,7 @@ class CVC5_EXPORT Solver
   friend class Grammar;
   friend class Op;
   friend class cvc5::Command;
+  friend class cvc5::main::CommandExecutor;
   friend class Sort;
   friend class Term;
 
@@ -2738,7 +2743,7 @@ class CVC5_EXPORT Solver
    * @param opts an optional pointer to a solver options object
    * @return the Solver
    */
-  Solver(Options* opts = nullptr);
+  Solver(const Options* opts = nullptr);
 
   /**
    * Destructor.