Allow changing certain options while solving (#6945)

This PR allows changing some select options ever after the smt engine has been fully initialized, following the SMT-LIB standard (section 4.1.7).

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 9b920b8753248ede5d0c9fd6230b865e4ca15696..4252cd45e5f313f669de2821a1351148bcd9af48 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7421,8 +7421,18 @@ void Solver::setOption(const std::string& option,
                        const std::string& value) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(!d_smtEngine->isFullyInited())
-      << "Invalid call to 'setOption', solver is already fully initialized";
+  static constexpr auto mutableOpts = {"diagnostic-output-channel",
+                                       "print-success",
+                                       "regular-output-channel",
+                                       "reproducible-resource-limit",
+                                       "verbosity"};
+  if (std::find(mutableOpts.begin(), mutableOpts.end(), option)
+      == mutableOpts.end())
+  {
+    CVC5_API_CHECK(!d_smtEngine->isFullyInited())
+        << "Invalid call to 'setOption' for option '" << option
+        << "', solver is already fully initialized";
+  }
   //////// all checks before this line
   d_smtEngine->setOption(option, value);
   ////////

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 90203708855a2b068ca31f8d30d10fabb9983dbb..87512e35b80b55d0ed16dded6ff74d2f8dc0e2fb 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -760,6 +760,7 @@ set(regress_0_tests
   regress0/opt-abd-no-use.smt2
   regress0/options/ast-and-sexpr.smt2
   regress0/options/invalid_dump.smt2
+  regress0/options/set-after-init.smt2
   regress0/options/set-and-get-options.smt2
   regress0/options/statistics.smt2
   regress0/parallel-let.smt2

diff --git a/test/regress/regress0/options/set-after-init.smt2 b/test/regress/regress0/options/set-after-init.smt2
new file mode 100644 (file)
index 0000000..5c1fce9
--- /dev/null
+++ b/test/regress/regress0/options/set-after-init.smt2
@@ -0,0 +1,25 @@
+; EXPECT: 0
+; EXPECT: 1
+; EXPECT: 0
+; EXPECT: 2
+; EXPECT: sat
+; EXPECT: 0
+; EXPECT: (error "Invalid call to 'setOption' for option 'random-seed', solver is already fully initialized")
+; EXIT: 1
+
+(get-option :verbosity)
+(set-option :verbosity 1)
+(get-option :verbosity)
+(set-option :verbosity 0)
+(get-option :random-seed)
+(set-option :random-seed 2)
+(get-option :random-seed)
+
+(set-logic QF_UF)
+(declare-fun x () Bool)
+(assert (or x (not x)))
+(check-sat)
+
+(set-option :verbosity 0)
+(get-option :verbosity)
+(set-option :random-seed 1)
\ No newline at end of file