From e7fdbc4d74ccb37efdd118eca519cb23bd350cad Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 30 Jul 2021 10:23:44 -0700
Subject: [PATCH] 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).
---
 src/api/cpp/cvc5.cpp                          | 14 +++++++++--
 test/regress/CMakeLists.txt                   |  1 +
 .../regress0/options/set-after-init.smt2      | 25 +++++++++++++++++++
 3 files changed, 38 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/options/set-after-init.smt2

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 9b920b875..4252cd45e 100644
--- 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 902037088..87512e35b 100644
--- 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
index 000000000..5c1fce9a7
--- /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
-- 
2.30.2