Make regular options access const (#8754)

One of the loose ends of the options refactor is that internal code can write to options at will, even when the accessing it via Env::getOptions() which returns a const reference. There are technical reasons for this, C++ does not propagate the constness into reference members.
This PR changes this behaviour by making the references members we use all over the place (options().smt.foo) const references and adding new functions writeSmt() which allow write access -- if you have a non-const handle to the options object.
In order to do that, this PR also changes all places that legitimately change the options (options handlers, set defaults, solver engine and places where we spawn subsolvers) to use the new syntax. After that, only a single place remains: the solver engine attempts to write the filename (from Solver::setInfo("filename", "...");) into the original options (that are restored to the new solver object after a reset. As only the API solver has write access to this, it is moved to the Solver::setInfo() method.

With this PR, all internal code is properly guarded against erroneous (and reckless) changing of options.
Fixes cvc5/cvc5-projects#12.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index a69d1f6418ebd48d9ce44199931935934abd629a..e0999dbff92402b059b06fbb8e7d481d30dfc699 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7347,6 +7347,11 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const
                               value)
       << "'sat', 'unsat' or 'unknown'";
   //////// all checks before this line
+  if (keyword == "filename")
+  {
+    // only the Solver object has non-const access to the original options
+    d_originalOptions->writeDriver().filename = value;
+  }
   d_slv->setInfo(keyword, value);
   ////////
   CVC5_API_TRY_CATCH_END;

diff --git a/src/options/README.md b/src/options/README.md
index 2f89f04eefc5a20f24b831df961cb23480506669..9227cc35c73e4c624fe5b235fd0595d91bfe669a 100644 (file)
--- a/src/options/README.md
+++ b/src/options/README.md
@@ -16,6 +16,8 @@ After parsing, a module is extended to have the following attributes:
 
 * `id`: lower-case version of the parsed `id`
 * `id_cap`: upper-case version of `id` (used for the `Holder{id_cap}` class)
+* `id_capitalized`: `id` with first letter upper-cased (used for the
+  `write{id_capitalized}()` method)
 * `filename`: base filename for generated files (`"{id}_options"`)
 * `header`: generated header name (`"options/{filename}.h"`)
 
@@ -166,8 +168,10 @@ consists of the following components:
 
 The `Options` class is the central entry point for regular usage of options. It
 holds a `std::unique_ptr` to an "option holder" for every option module, that
-can be accessed using references `{module}` (either as `const&` or `&`). These
-holders hold the actual option data for the specific module.
+can be accessed using references `const {module}&`. These holders hold the actual
+option data for the specific module. For non-const accesses, there are methods
+`write{module}()` which can only be used from a non-const handle to the `Options`
+object.
 
 The holder types are forward declared and can thus only be accessed if one also
 includes the appropriate `{module}_options.h`, which contains the proper

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index e30f7093ccbfe84d46185cad34e03c5ef01586fd..b4c1aeed9e82cd0037f438017ad3050dd1d0d3e1 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -157,6 +157,7 @@ class Module(object):
         self.options = []
         self.id = self.id.lower()
         self.id_cap = self.id.upper()
+        self.id_capitalized = self.id.capitalize()
         self.filename = os.path.splitext(os.path.split(filename)[-1])[0]
         self.header = os.path.join('options', '{}.h'.format(self.filename))
 
@@ -220,7 +221,8 @@ def generate_holder_mem_decls(modules):
 
 def generate_holder_ref_decls(modules):
     """Render reference declarations for holder members of the Option class"""
-    return concat_format('  options::Holder{id_cap}& {id};', modules)
+    return concat_format('''  const options::Holder{id_cap}& {id};
+  options::Holder{id_cap}& write{id_capitalized}();''', modules)
 
 
 ################################################################################
@@ -244,6 +246,15 @@ def generate_holder_ref_inits(modules):
     return concat_format('        {id}(*d_{id}),', modules)
 
 
+def generate_write_functions(modules):
+    """Render write functions for holders within the Option class"""
+    return concat_format('''  options::Holder{id_cap}& Options::write{id_capitalized}()
+  {{
+    return *d_{id};
+  }}
+''', modules)
+
+
 def generate_holder_mem_copy(modules):
     """Render copy operation of holder members of the Option class"""
     return concat_format('      *d_{id} = *options.d_{id};', modules)
@@ -334,10 +345,10 @@ def generate_set_impl(modules):
         for pred in _set_predicates(option):
             res.append('  {}'.format(pred))
         if option.name:
-            res.append('  opts.{module}.{name} = value;'.format(
-                module=module.id, name=option.name))
-            res.append('  opts.{module}.{name}WasSetByUser = true;'.format(
-                module=module.id, name=option.name))
+            res.append('  opts.write{module}().{name} = value;'.format(
+                module=module.id_capitalized, name=option.name))
+            res.append('  opts.write{module}().{name}WasSetByUser = true;'.format(
+                module=module.id_capitalized, name=option.name))
     return '\n    '.join(res)
 
 
@@ -873,6 +884,7 @@ def codegen_all_modules(modules, src_dir, build_dir, dst_dir, tpls):
         'headers_module': generate_module_headers(modules),
         'holder_mem_inits': generate_holder_mem_inits(modules),
         'holder_ref_inits': generate_holder_ref_inits(modules),
+        'write_functions': generate_write_functions(modules),
         'holder_mem_copy': generate_holder_mem_copy(modules),
         # options/options_public.cpp
         'options_includes': generate_public_includes(modules),

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 839a848d69513a028159a545fe8ff6ed603110bf..fd4d5be063119a5937109581c543d2b050ae5716 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -177,13 +177,13 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value)
 
 void OptionsHandler::decreaseVerbosity(const std::string& flag, bool value)
 {
-  d_options->base.verbosity -= 1;
+  d_options->writeBase().verbosity -= 1;
   setVerbosity(flag, d_options->base.verbosity);
 }
 
 void OptionsHandler::increaseVerbosity(const std::string& flag, bool value)
 {
-  d_options->base.verbosity += 1;
+  d_options->writeBase().verbosity += 1;
   setVerbosity(flag, d_options->base.verbosity);
 }
 
@@ -201,9 +201,9 @@ void OptionsHandler::setStats(const std::string& flag, bool value)
 #endif /* CVC5_STATISTICS_ON */
   if (!value)
   {
-    d_options->base.statisticsAll = false;
-    d_options->base.statisticsEveryQuery = false;
-    d_options->base.statisticsInternal = false;
+    d_options->writeBase().statisticsAll = false;
+    d_options->writeBase().statisticsEveryQuery = false;
+    d_options->writeBase().statisticsInternal = false;
   }
 }
 
@@ -221,7 +221,7 @@ void OptionsHandler::setStatsDetail(const std::string& flag, bool value)
 #endif /* CVC5_STATISTICS_ON */
   if (value)
   {
-    d_options->base.statistics = true;
+    d_options->writeBase().statistics = true;
   }
 }
 
@@ -237,7 +237,7 @@ void OptionsHandler::enableTraceTag(const std::string& flag,
   {
     if (optarg == "help")
     {
-      d_options->driver.showTraceTags = true;
+      d_options->writeDriver().showTraceTags = true;
       showTraceTags("", true);
       return;
     }
@@ -268,7 +268,7 @@ void OptionsHandler::enableDebugTag(const std::string& flag,
   {
     if (optarg == "help")
     {
-      d_options->driver.showDebugTags = true;
+      d_options->writeDriver().showDebugTags = true;
       showDebugTags("", true);
       return;
     }
@@ -288,7 +288,7 @@ void OptionsHandler::enableOutputTag(const std::string& flag,
   size_t tagid = static_cast<size_t>(optarg);
   Assert(d_options->base.outputTagHolder.size() > tagid)
       << "Output tag is larger than the bitset that holds it.";
-  d_options->base.outputTagHolder.set(tagid);
+  d_options->writeBase().outputTagHolder.set(tagid);
 }
 
 void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)
@@ -301,7 +301,7 @@ void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)
 void OptionsHandler::setResourceWeight(const std::string& flag,
                                        const std::string& optarg)
 {
-  d_options->base.resourceWeightHolder.emplace_back(optarg);
+  d_options->writeBase().resourceWeightHolder.emplace_back(optarg);
 }
 
 void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m)
@@ -352,7 +352,7 @@ void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m)
     }
     if (!d_options->bv.bitvectorToBoolWasSetByUser)
     {
-      d_options->bv.bitvectorToBool = true;
+      d_options->writeBv().bitvectorToBool = true;
     }
   }
 }

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 4783441fd44195dea7f3e5ccf2c02fa8fcc441e8..cea6a2139007b8eb2daa4af71f53147fa492a4cd 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -40,6 +40,10 @@ ${holder_ref_inits}$
 
   Options::~Options() {}
 
+// clang-format off
+${write_functions}$
+// clang-format on
+
   void Options::copyValues(const Options& options)
   {
     if (this != &options)

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 4f54310e7b75ae723c9edc183cf8b1e1118bd071..dc26303adfe5d9642baff82b227dd58689cb7f34 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -71,26 +71,26 @@ void SetDefaults::setDefaultsPre(Options& opts)
   // implied options
   if (opts.smt.debugCheckModels)
   {
-    opts.smt.checkModels = true;
+    opts.writeSmt().checkModels = true;
   }
   if (opts.smt.checkModels || opts.driver.dumpModels)
   {
-    opts.smt.produceModels = true;
+    opts.writeSmt().produceModels = true;
   }
   if (opts.smt.checkModels)
   {
-    opts.smt.produceAssignments = true;
+    opts.writeSmt().produceAssignments = true;
   }
   // unsat cores and proofs shenanigans
   if (opts.driver.dumpDifficulty)
   {
-    opts.smt.produceDifficulty = true;
+    opts.writeSmt().produceDifficulty = true;
   }
   if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores
       || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores
       || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)
   {
-    opts.smt.unsatCores = true;
+    opts.writeSmt().unsatCores = true;
   }
   if (opts.smt.unsatCores
       && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
@@ -100,21 +100,21 @@ void SetDefaults::setDefaultsPre(Options& opts)
       notifyModifyOption(
           "unsatCoresMode", "assumptions", "enabling unsat cores");
     }
-    opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
+    opts.writeSmt().unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
   }
   // if check-proofs, dump-proofs, or proof-mode=full, then proofs being fully
   // enabled is implied
   if (opts.smt.checkProofs || opts.driver.dumpProofs
       || opts.smt.proofMode == options::ProofMode::FULL)
   {
-    opts.smt.produceProofs = true;
+    opts.writeSmt().produceProofs = true;
   }
 
   // this check assumes the user has requested *full* proofs
   if (opts.smt.produceProofs)
   {
     // if the user requested proofs, proof mode is full
-    opts.smt.proofMode = options::ProofMode::FULL;
+    opts.writeSmt().proofMode = options::ProofMode::FULL;
     // unsat cores are available due to proofs being enabled
     if (opts.smt.unsatCoresMode != options::UnsatCoresMode::SAT_PROOF)
     {
@@ -122,8 +122,8 @@ void SetDefaults::setDefaultsPre(Options& opts)
       {
         notifyModifyOption("unsatCoresMode", "sat-proof", "enabling proofs");
       }
-      opts.smt.unsatCores = true;
-      opts.smt.unsatCoresMode = options::UnsatCoresMode::SAT_PROOF;
+      opts.writeSmt().unsatCores = true;
+      opts.writeSmt().unsatCoresMode = options::UnsatCoresMode::SAT_PROOF;
     }
   }
   if (!opts.smt.produceProofs)
@@ -132,32 +132,32 @@ void SetDefaults::setDefaultsPre(Options& opts)
     {
       // if (expert) user set proof mode to something other than off, enable
       // proofs
-      opts.smt.produceProofs = true;
+      opts.writeSmt().produceProofs = true;
     }
     // if proofs weren't enabled by user, and we are producing difficulty
     if (opts.smt.produceDifficulty)
     {
-      opts.smt.produceProofs = true;
+      opts.writeSmt().produceProofs = true;
       // ensure at least preprocessing proofs are enabled
       if (opts.smt.proofMode == options::ProofMode::OFF)
       {
-        opts.smt.proofMode = options::ProofMode::PP_ONLY;
+        opts.writeSmt().proofMode = options::ProofMode::PP_ONLY;
       }
     }
     // if proofs weren't enabled by user, and we are producing unsat cores
     if (opts.smt.unsatCores)
     {
-      opts.smt.produceProofs = true;
+      opts.writeSmt().produceProofs = true;
       if (opts.smt.unsatCoresMode == options::UnsatCoresMode::SAT_PROOF)
       {
         // if requested to be based on proofs, we produce (preprocessing +) SAT
         // proofs
-        opts.smt.proofMode = options::ProofMode::SAT;
+        opts.writeSmt().proofMode = options::ProofMode::SAT;
       }
       else if (opts.smt.proofMode == options::ProofMode::OFF)
       {
         // otherwise, we always produce preprocessing proofs
-        opts.smt.proofMode = options::ProofMode::PP_ONLY;
+        opts.writeSmt().proofMode = options::ProofMode::PP_ONLY;
       }
     }
   }
@@ -184,10 +184,10 @@ void SetDefaults::setDefaultsPre(Options& opts)
   {
     // these options must be disabled on internal subsolvers, as they are
     // used by the user to rephrase the input.
-    opts.quantifiers.sygusInference = false;
-    opts.quantifiers.sygusRewSynthInput = false;
+    opts.writeQuantifiers().sygusInference = false;
+    opts.writeQuantifiers().sygusRewSynthInput = false;
     // deep restart does not work with internal subsolvers?
-    opts.smt.deepRestartMode = options::DeepRestartMode::NONE;
+    opts.writeSmt().deepRestartMode = options::DeepRestartMode::NONE;
   }
 }
 
@@ -208,7 +208,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
                    && logic.areIntegersUsed()))
            && !opts.base.incrementalSolving)
   {
-    opts.quantifiers.sygusInst = true;
+    opts.writeQuantifiers().sygusInst = true;
   }
 
   if (opts.bv.bitblastMode == options::BitblastMode::EAGER)
@@ -226,12 +226,12 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
             "functions. Try --bitblast=lazy"));
       }
       notifyModifyOption("bitblastMode", "lazy", "model generation");
-      opts.bv.bitblastMode = options::BitblastMode::LAZY;
+      opts.writeBv().bitblastMode = options::BitblastMode::LAZY;
     }
     else if (!opts.base.incrementalSolving)
     {
       // if not incremental, we rely on ackermann to eliminate other theories.
-      opts.smt.ackermann = true;
+      opts.writeSmt().ackermann = true;
     }
     else if (logic.isQuantified() || !logic.isPure(THEORY_BV))
     {
@@ -291,7 +291,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
           "Ackermannization currently does not support model generation."));
     }
     notifyModifyOption("ackermann", "false", "model generation");
-    opts.smt.ackermann = false;
+    opts.writeSmt().ackermann = false;
     // we are not relying on ackermann to eliminate theories in this case
     Assert(opts.bv.bitblastMode != options::BitblastMode::EAGER);
   }
@@ -325,7 +325,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
   {
     // If the user explicitly set a logic that includes strings, but is not
     // the generic "ALL" logic, then enable stringsExp.
-    opts.strings.stringExp = true;
+    opts.writeStrings().stringExp = true;
     Trace("smt") << "Turning stringExp on since logic does not have everything "
                     "and string theory is enabled\n";
   }
@@ -399,7 +399,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   if (!opts.smt.produceAssertions)
   {
     verbose(1) << "SolverEngine: turning on produce-assertions." << std::endl;
-    opts.smt.produceAssertions = true;
+    opts.writeSmt().produceAssertions = true;
   }
 
   if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
@@ -410,7 +410,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
      * Therefore, we enable bv-to-bool, which runs before
      * the translation to integers.
      */
-    opts.bv.bitvectorToBool = true;
+    opts.writeBv().bitvectorToBool = true;
   }
 
   // Disable options incompatible with incremental solving, or output an error
@@ -457,7 +457,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
                      && !logic.isTheoryEnabled(THEORY_ARITH);
       Trace("smt") << "setting unconstrained simplification to " << uncSimp
                    << std::endl;
-      opts.smt.unconstrainedSimp = uncSimp;
+      opts.writeSmt().unconstrainedSimp = uncSimp;
     }
 
     // by default, nonclausal simplification is off for QF_SAT
@@ -470,8 +470,9 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       // quantifiers, not others opts.set(options::simplificationMode, qf_sat ||
       // quantifiers ? options::SimplificationMode::NONE :
       // options::SimplificationMode::BATCH);
-      opts.smt.simplificationMode = qf_sat ? options::SimplificationMode::NONE
-                                           : options::SimplificationMode::BATCH;
+      opts.writeSmt().simplificationMode =
+          qf_sat ? options::SimplificationMode::NONE
+                 : options::SimplificationMode::BATCH;
     }
   }
 
@@ -488,7 +489,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       verbose(1)
           << "SolverEngine: turning off bool-to-bitvector to support CBQI BV"
           << std::endl;
-      opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
+      opts.writeBv().boolToBitvector = options::BoolToBVMode::OFF;
     }
   }
 
@@ -497,7 +498,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       && (opts.smt.produceAssignments || usesSygus(opts)))
   {
     verbose(1) << "SolverEngine: turning on produce-models" << std::endl;
-    opts.smt.produceModels = true;
+    opts.writeSmt().produceModels = true;
   }
 
   // --ite-simp is an experimental option designed for QF_LIA/nec. This
@@ -508,7 +509,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   {
     if (!opts.smt.earlyIteRemovalWasSetByUser)
     {
-      opts.smt.earlyIteRemoval = true;
+      opts.writeSmt().earlyIteRemoval = true;
     }
   }
 
@@ -523,7 +524,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
              && !logic.isQuantified()))
     {
       Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
-      opts.theory.theoryOfMode = options::TheoryOfMode::THEORY_OF_TERM_BASED;
+      opts.writeTheory().theoryOfMode =
+          options::TheoryOfMode::THEORY_OF_TERM_BASED;
     }
   }
 
@@ -535,7 +537,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
                        && !safeUnsatCores(opts);
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
                  << std::endl;
-    opts.uf.ufSymmetryBreaker = qf_uf_noinc;
+    opts.writeUf().ufSymmetryBreaker = qf_uf_noinc;
   }
 
   // If in arrays, set the UF handler to arrays
@@ -560,7 +562,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     bool withCare = qf_aufbv;
     Trace("smt") << "setting ite simplify with care to " << withCare
                  << std::endl;
-    opts.smt.simplifyWithCareEnabled = withCare;
+    opts.writeSmt().simplifyWithCareEnabled = withCare;
   }
   // Turn off array eager index splitting for QF_AUFLIA
   if (!opts.arrays.arraysEagerIndexSplittingWasSetByUser)
@@ -571,7 +573,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     {
       Trace("smt") << "setting array eager index splitting to false"
                    << std::endl;
-      opts.arrays.arraysEagerIndexSplitting = false;
+      opts.writeArrays().arraysEagerIndexSplitting = false;
     }
   }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
@@ -584,13 +586,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
                       && !safeUnsatCores(opts);
     Trace("smt") << "setting repeat simplification to " << repeatSimp
                  << std::endl;
-    opts.smt.repeatSimp = repeatSimp;
+    opts.writeSmt().repeatSimp = repeatSimp;
   }
 
   /* Disable bit-level propagation by default for the BITBLAST solver. */
   if (opts.bv.bvSolver == options::BVSolver::BITBLAST)
   {
-    opts.bv.bitvectorPropagate = false;
+    opts.writeBv().bitvectorPropagate = false;
   }
 
   if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL
@@ -603,7 +605,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     }
     verbose(1) << "SolverEngine: turning off bool-to-bv for non-bv logic: "
                << logic.getLogicString() << std::endl;
-    opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
+    opts.writeBv().boolToBitvector = options::BoolToBVMode::OFF;
   }
 
   // Turn on arith rewrite equalities only for pure arithmetic
@@ -613,7 +615,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
         logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified();
     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
                  << std::endl;
-    opts.arith.arithRewriteEq = arithRewriteEq;
+    opts.writeArith().arithRewriteEq = arithRewriteEq;
   }
   if (!opts.arith.arithHeuristicPivotsWasSetByUser)
   {
@@ -631,7 +633,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     }
     Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots
                  << std::endl;
-    opts.arith.arithHeuristicPivots = heuristicPivots;
+    opts.writeArith().arithHeuristicPivots = heuristicPivots;
   }
   if (!opts.arith.arithPivotThresholdWasSetByUser)
   {
@@ -645,7 +647,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     }
     Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold
                  << std::endl;
-    opts.arith.arithPivotThreshold = pivotThreshold;
+    opts.writeArith().arithPivotThreshold = pivotThreshold;
   }
   if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser)
   {
@@ -656,7 +658,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     }
     Trace("smt") << "setting arithStandardCheckVarOrderPivots  "
                  << varOrderPivots << std::endl;
-    opts.arith.arithStandardCheckVarOrderPivots = varOrderPivots;
+    opts.writeArith().arithStandardCheckVarOrderPivots = varOrderPivots;
   }
   if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed())
   {
@@ -664,14 +666,14 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     {
       Trace("smt") << "setting nlExtTangentPlanesInterleave to true"
                    << std::endl;
-      opts.arith.nlExtTangentPlanesInterleave = true;
+      opts.writeArith().nlExtTangentPlanesInterleave = true;
     }
   }
   if (!opts.arith.nlRlvAssertBoundsWasSetByUser)
   {
     // use bound inference to determine when bounds are irrelevant only when
     // the logic is quantifier-free
-    opts.arith.nlRlvAssertBounds = !logic.isQuantified();
+    opts.writeArith().nlRlvAssertBounds = !logic.isQuantified();
   }
 
   // set the default decision mode
@@ -683,7 +685,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     if (!opts.arith.arithEqSolverWasSetByUser)
     {
       // use the arithmetic equality solver by default
-      opts.arith.arithEqSolver = true;
+      opts.writeArith().arithEqSolver = true;
     }
   }
 
@@ -692,7 +694,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     if (!opts.theory.assignFunctionValues)
     {
       // must assign function values
-      opts.theory.assignFunctionValues = true;
+      opts.writeTheory().assignFunctionValues = true;
     }
   }
 
@@ -708,7 +710,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       Trace("smt")
           << "Disabling shared selectors for quantified logic without SyGuS"
           << std::endl;
-      opts.datatypes.dtSharedSelectors = false;
+      opts.writeDatatypes().dtSharedSelectors = false;
     }
   }
 
@@ -728,7 +730,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
         || opts.smt.checkModels
         || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
     {
-      opts.prop.minisatSimpMode = options::MinisatSimpMode::CLAUSE_ELIM;
+      opts.writeProp().minisatSimpMode = options::MinisatSimpMode::CLAUSE_ELIM;
     }
   }
 
@@ -744,7 +746,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
                   << opts.arith.nlRlvMode << std::endl;
       }
       // must use relevance filtering techniques
-      opts.theory.relevanceFilter = true;
+      opts.writeTheory().relevanceFilter = true;
     }
   }
 
@@ -752,7 +754,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   if (opts.smt.produceModels || opts.smt.produceAssignments
       || opts.smt.checkModels)
   {
-    opts.arrays.arraysOptimizeLinear = false;
+    opts.writeArrays().arraysOptimizeLinear = false;
   }
 
   if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser)
@@ -760,7 +762,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
                     "--strings-fmf enabled"
                  << std::endl;
-    opts.strings.stringProcessLoopMode = options::ProcessLoopMode::SIMPLE;
+    opts.writeStrings().stringProcessLoopMode =
+        options::ProcessLoopMode::SIMPLE;
   }
 
   // !!! All options that require disabling models go here
@@ -778,7 +781,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       }
       verbose(1) << "SolverEngine: turning off produce-models to support "
                  << sOptNoModel << std::endl;
-      opts.smt.produceModels = false;
+      opts.writeSmt().produceModels = false;
     }
     if (opts.smt.produceAssignments)
     {
@@ -791,7 +794,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       }
       verbose(1) << "SolverEngine: turning off produce-assignments to support "
                  << sOptNoModel << std::endl;
-      opts.smt.produceAssignments = false;
+      opts.writeSmt().produceAssignments = false;
     }
     if (opts.smt.checkModels)
     {
@@ -804,7 +807,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       }
       verbose(1) << "SolverEngine: turning off check-models to support "
                  << sOptNoModel << std::endl;
-      opts.smt.checkModels = false;
+      opts.writeSmt().checkModels = false;
     }
   }
 
@@ -824,14 +827,14 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   {
     if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser)
     {
-      opts.arith.nlCov = true;
+      opts.writeArith().nlCov = true;
       if (!opts.arith.nlExtWasSetByUser)
       {
-        opts.arith.nlExt = options::NlExtMode::LIGHT;
+        opts.writeArith().nlExt = options::NlExtMode::LIGHT;
       }
       if (!opts.arith.nlRlvModeWasSetByUser)
       {
-        opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE;
+        opts.writeArith().nlRlvMode = options::NlRlvMode::INTERLEAVE;
       }
     }
   }
@@ -841,10 +844,10 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   {
     if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser)
     {
-      opts.arith.nlCov = true;
+      opts.writeArith().nlCov = true;
       if (!opts.arith.nlExtWasSetByUser)
       {
-        opts.arith.nlExt = options::NlExtMode::LIGHT;
+        opts.writeArith().nlExt = options::NlExtMode::LIGHT;
       }
     }
   }
@@ -860,8 +863,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     {
       verbose(1) << "Cannot use --nl-cov without configuring with --poly."
                  << std::endl;
-      opts.arith.nlCov = false;
-      opts.arith.nlExt = options::NlExtMode::FULL;
+      opts.writeArith().nlCov = false;
+      opts.writeArith().nlExt = options::NlExtMode::FULL;
     }
   }
 #endif
@@ -869,7 +872,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   {
       if (!opts.arith.nlExtWasSetByUser)
       {
-        opts.arith.nlExt = options::NlExtMode::FULL;
+        opts.writeArith().nlExt = options::NlExtMode::FULL;
       }
   }
 }
@@ -953,7 +956,7 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
     verbose(1)
         << "Disabling bv-assert-input since it is incompatible with proofs."
         << std::endl;
-    opts.bv.bvAssertInput = false;
+    opts.writeBv().bvAssertInput = false;
   }
   // If proofs are required and the user did not specify a specific BV solver,
   // we make sure to use the proof producing BITBLAST_INTERNAL solver.
@@ -962,14 +965,14 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
   {
     verbose(1) << "Forcing internal bit-vector solver due to proof production."
                << std::endl;
-    opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
+    opts.writeBv().bvSolver = options::BVSolver::BITBLAST_INTERNAL;
   }
   if (opts.arith.nlCovVarElim && !opts.arith.nlCovVarElimWasSetByUser)
   {
     verbose(1)
         << "Disabling nl-cov-var-elim since it is incompatible with proofs."
         << std::endl;
-    opts.arith.nlCovVarElim = false;
+    opts.writeArith().nlCovVarElim = false;
   }
   if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
   {
@@ -1033,7 +1036,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       return true;
     }
     notifyModifyOption("unconstrainedSimp", "false", "incremental solving");
-    opts.smt.unconstrainedSimp = false;
+    opts.writeSmt().unconstrainedSimp = false;
   }
   if (opts.bv.bitblastMode == options::BitblastMode::EAGER
       && !logic.isPure(THEORY_BV))
@@ -1050,7 +1053,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       return true;
     }
     notifyModifyOption("sygusInference", "false", "incremental solving");
-    opts.quantifiers.sygusInference = false;
+    opts.writeQuantifiers().sygusInference = false;
   }
   if (opts.quantifiers.sygusInst)
   {
@@ -1060,7 +1063,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       return true;
     }
     notifyModifyOption("sygusInst", "false", "incremental solving");
-    opts.quantifiers.sygusInst = false;
+    opts.writeQuantifiers().sygusInst = false;
   }
   if (opts.smt.solveIntAsBV > 0)
   {
@@ -1080,13 +1083,13 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
 
   // disable modes not supported by incremental
   notifyModifyOption("sortInference", "false", "incremental solving");
-  opts.smt.sortInference = false;
-  opts.uf.ufssFairnessMonotone = false;
+  opts.writeSmt().sortInference = false;
+  opts.writeUf().ufssFairnessMonotone = false;
   notifyModifyOption("globalNegate", "false", "incremental solving");
-  opts.quantifiers.globalNegate = false;
+  opts.writeQuantifiers().globalNegate = false;
   notifyModifyOption("cegqiNestedQE", "false", "incremental solving");
-  opts.quantifiers.cegqiNestedQE = false;
-  opts.arith.arithMLTrick = false;
+  opts.writeQuantifiers().cegqiNestedQE = false;
+  opts.writeArith().arithMLTrick = false;
   return false;
 }
 
@@ -1101,13 +1104,13 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("simplificationMode", "none", "unsat cores");
-    opts.smt.simplificationMode = options::SimplificationMode::NONE;
+    opts.writeSmt().simplificationMode = options::SimplificationMode::NONE;
     if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
     {
       verbose(1) << "SolverEngine: turning off deep restart to support unsat "
                     "cores"
                  << std::endl;
-      opts.smt.deepRestartMode = options::DeepRestartMode::NONE;
+      opts.writeSmt().deepRestartMode = options::DeepRestartMode::NONE;
     }
   }
 
@@ -1119,7 +1122,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("learnedRewrite", "false", "unsat cores");
-    opts.smt.learnedRewrite = false;
+    opts.writeSmt().learnedRewrite = false;
   }
 
   if (opts.arith.pbRewrites)
@@ -1130,7 +1133,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("pbRewrites", "false", "unsat cores");
-    opts.arith.pbRewrites = false;
+    opts.writeArith().pbRewrites = false;
   }
 
   if (opts.smt.sortInference)
@@ -1141,7 +1144,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("sortInference", "false", "unsat cores");
-    opts.smt.sortInference = false;
+    opts.writeSmt().sortInference = false;
   }
 
   if (opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
@@ -1152,7 +1155,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("preSkolemQuant", "off", "unsat cores");
-    opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::OFF;
+    opts.writeQuantifiers().preSkolemQuant = options::PreSkolemQuantMode::OFF;
   }
 
   if (opts.bv.bitvectorToBool)
@@ -1163,7 +1166,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("bitvectorToBool", "false", "unsat cores");
-    opts.bv.bitvectorToBool = false;
+    opts.writeBv().bitvectorToBool = false;
   }
 
   if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
@@ -1174,7 +1177,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("boolToBitvector", "off", "unsat cores");
-    opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
+    opts.writeBv().boolToBitvector = options::BoolToBVMode::OFF;
   }
 
   if (opts.bv.bvIntroducePow2)
@@ -1185,7 +1188,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("bvIntroducePow2", "false", "unsat cores");
-    opts.bv.bvIntroducePow2 = false;
+    opts.writeBv().bvIntroducePow2 = false;
   }
 
   if (opts.smt.repeatSimp)
@@ -1196,7 +1199,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("repeatSimp", "false", "unsat cores");
-    opts.smt.repeatSimp = false;
+    opts.writeSmt().repeatSimp = false;
   }
 
   if (opts.quantifiers.globalNegate)
@@ -1207,7 +1210,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("globalNegate", "false", "unsat cores");
-    opts.quantifiers.globalNegate = false;
+    opts.writeQuantifiers().globalNegate = false;
   }
 
   if (opts.smt.doITESimp)
@@ -1223,7 +1226,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       return true;
     }
     notifyModifyOption("unconstrainedSimp", "false", "unsat cores");
-    opts.smt.unconstrainedSimp = false;
+    opts.writeSmt().unconstrainedSimp = false;
   }
   if (opts.smt.deepRestartMode != options::DeepRestartMode::NONE)
   {
@@ -1280,7 +1283,7 @@ bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
 bool SetDefaults::incompatibleWithSeparationLogic(Options& opts,
                                                   std::ostream& reason) const
 {
-  if (options().smt.simplificationBoolConstProp)
+  if (opts.smt.simplificationBoolConstProp)
   {
     // Spatial formulas in separation logic have a semantics that depends on
     // their position in the AST (e.g. their nesting beneath separation
@@ -1288,7 +1291,7 @@ bool SetDefaults::incompatibleWithSeparationLogic(Options& opts,
     // predicates to the input formula. We disable this option altogether to
     // ensure this is the case
     notifyModifyOption("simplification-bcp", "false", "separation logic");
-    options().smt.simplificationBoolConstProp = false;
+    opts.writeSmt().simplificationBoolConstProp = false;
   }
   return false;
 }
@@ -1381,7 +1384,7 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   if (opts.quantifiers.fullSaturateQuant)
   {
     Trace("smt") << "enabling enum-inst for full-saturate-quant" << std::endl;
-    opts.quantifiers.enumInst = true;
+    opts.writeQuantifiers().enumInst = true;
   }
   if (opts.arrays.arraysExp)
   {
@@ -1389,26 +1392,26 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     if (!opts.quantifiers.fmfBoundWasSetByUser)
     {
       notifyModifyOption("fmfBound", "true", "arrays-exp");
-      opts.quantifiers.fmfBound = true;
+      opts.writeQuantifiers().fmfBound = true;
     }
   }
   if (logic.hasCardinalityConstraints())
   {
     // must have finite model finding on
-    opts.quantifiers.finiteModelFind = true;
+    opts.writeQuantifiers().finiteModelFind = true;
   }
 
   if (opts.quantifiers.instMaxLevel != -1)
   {
     verbose(1) << "SolverEngine: turning off cbqi to support instMaxLevel"
                << std::endl;
-    opts.quantifiers.cegqi = false;
+    opts.writeQuantifiers().cegqi = false;
   }
 
   if (opts.quantifiers.fmfBoundLazyWasSetByUser
        && opts.quantifiers.fmfBoundLazy)
   {
-    opts.quantifiers.fmfBound = true;
+    opts.writeQuantifiers().fmfBound = true;
     Trace("smt")
         << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n";
   }
@@ -1421,11 +1424,11 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
             && opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::FMC))
     {
       // if bounded integers are set, use no MBQI by default
-      opts.quantifiers.fmfMbqiMode = options::FmfMbqiMode::NONE;
+      opts.writeQuantifiers().fmfMbqiMode = options::FmfMbqiMode::NONE;
     }
     if (!opts.quantifiers.prenexQuantUserWasSetByUser)
     {
-      opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
+      opts.writeQuantifiers().prenexQuant = options::PrenexQuantMode::NONE;
     }
   }
   if (logic.isHigherOrder())
@@ -1434,32 +1437,32 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     // cannot be used
     if (opts.quantifiers.fmfMbqiMode != options::FmfMbqiMode::NONE)
     {
-      opts.quantifiers.fmfMbqiMode = options::FmfMbqiMode::NONE;
+      opts.writeQuantifiers().fmfMbqiMode = options::FmfMbqiMode::NONE;
     }
     if (!opts.quantifiers.hoElimStoreAxWasSetByUser)
     {
       // by default, use store axioms only if --ho-elim is set
-      opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim;
+      opts.writeQuantifiers().hoElimStoreAx = opts.quantifiers.hoElim;
     }
     // Cannot use macros, since lambda lifting and macro elimination are inverse
     // operations.
     if (opts.quantifiers.macrosQuant)
     {
-      opts.quantifiers.macrosQuant = false;
+      opts.writeQuantifiers().macrosQuant = false;
     }
   }
   if (opts.quantifiers.fmfFunWellDefinedRelevant)
   {
     if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser)
     {
-      opts.quantifiers.fmfFunWellDefined = true;
+      opts.writeQuantifiers().fmfFunWellDefined = true;
     }
   }
   if (opts.quantifiers.fmfFunWellDefined)
   {
     if (!opts.quantifiers.finiteModelFindWasSetByUser)
     {
-      opts.quantifiers.finiteModelFind = true;
+      opts.writeQuantifiers().finiteModelFind = true;
     }
   }
 
@@ -1470,20 +1473,21 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     // apply conservative quantifiers splitting
     if (!opts.quantifiers.quantDynamicSplitWasSetByUser)
     {
-      opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT;
+      opts.writeQuantifiers().quantDynamicSplit =
+          options::QuantDSplitMode::DEFAULT;
     }
     if (!opts.quantifiers.eMatchingWasSetByUser)
     {
       // do not use E-matching by default. For E-matching + FMF, the user should
       // specify --finite-model-find --e-matching.
-      opts.quantifiers.eMatching = false;
+      opts.writeQuantifiers().eMatching = false;
     }
     if (!opts.quantifiers.instWhenModeWasSetByUser)
     {
       // instantiate only on last call
       if (opts.quantifiers.eMatching)
       {
-        opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
+        opts.writeQuantifiers().instWhenMode = options::InstWhenMode::LAST_CALL;
       }
     }
   }
@@ -1513,14 +1517,14 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   {
     if (!opts.quantifiers.cegqiWasSetByUser)
     {
-      opts.quantifiers.cegqi = true;
+      opts.writeQuantifiers().cegqi = true;
     }
     // check whether we should apply full cbqi
     if (logic.isPure(THEORY_BV))
     {
       if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
       {
-        opts.quantifiers.cegqiFullEffort = true;
+        opts.writeQuantifiers().cegqiFullEffort = true;
       }
     }
   }
@@ -1530,42 +1534,42 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     {
       if (!opts.quantifiers.conflictBasedInstWasSetByUser)
       {
-        opts.quantifiers.conflictBasedInst = false;
+        opts.writeQuantifiers().conflictBasedInst = false;
       }
       if (!opts.quantifiers.instNoEntailWasSetByUser)
       {
-        opts.quantifiers.instNoEntail = false;
+        opts.writeQuantifiers().instNoEntail = false;
       }
       if (!opts.quantifiers.instWhenModeWasSetByUser)
       {
         // only instantiation should happen at last call when model is avaiable
-        opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
+        opts.writeQuantifiers().instWhenMode = options::InstWhenMode::LAST_CALL;
       }
     }
     else
     {
       // only supported in pure arithmetic or pure BV
-      opts.quantifiers.cegqiNestedQE = false;
+      opts.writeQuantifiers().cegqiNestedQE = false;
     }
     if (opts.quantifiers.globalNegate)
     {
       if (!opts.quantifiers.prenexQuantWasSetByUser)
       {
-        opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
+        opts.writeQuantifiers().prenexQuant = options::PrenexQuantMode::NONE;
       }
     }
   }
   // implied options...
   if (opts.quantifiers.cbqiModeWasSetByUser || opts.quantifiers.cbqiTConstraint)
   {
-    opts.quantifiers.conflictBasedInst = true;
+    opts.writeQuantifiers().conflictBasedInst = true;
   }
   if (opts.quantifiers.cegqiNestedQE)
   {
-    opts.quantifiers.prenexQuantUser = true;
+    opts.writeQuantifiers().prenexQuantUser = true;
     if (!opts.quantifiers.preSkolemQuantWasSetByUser)
     {
-      opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::ON;
+      opts.writeQuantifiers().preSkolemQuant = options::PreSkolemQuantMode::ON;
     }
   }
   // for induction techniques
@@ -1573,11 +1577,11 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   {
     if (!opts.quantifiers.dtStcInductionWasSetByUser)
     {
-      opts.quantifiers.dtStcInduction = true;
+      opts.writeQuantifiers().dtStcInduction = true;
     }
     if (!opts.quantifiers.intWfInductionWasSetByUser)
     {
-      opts.quantifiers.intWfInduction = true;
+      opts.writeQuantifiers().intWfInduction = true;
     }
   }
   if (opts.quantifiers.dtStcInduction)
@@ -1585,29 +1589,29 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     // try to remove ITEs from quantified formulas
     if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser)
     {
-      opts.quantifiers.iteDtTesterSplitQuant = true;
+      opts.writeQuantifiers().iteDtTesterSplitQuant = true;
     }
     if (!opts.quantifiers.iteLiftQuantWasSetByUser)
     {
-      opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL;
+      opts.writeQuantifiers().iteLiftQuant = options::IteLiftQuantMode::ALL;
     }
   }
   if (opts.quantifiers.intWfInduction)
   {
     if (!opts.quantifiers.purifyTriggersWasSetByUser)
     {
-      opts.quantifiers.purifyTriggers = true;
+      opts.writeQuantifiers().purifyTriggers = true;
     }
   }
   if (opts.quantifiers.conjectureGenPerRoundWasSetByUser)
   {
     if (opts.quantifiers.conjectureGenPerRound > 0)
     {
-      opts.quantifiers.conjectureGen = true;
+      opts.writeQuantifiers().conjectureGen = true;
     }
     else
     {
-      opts.quantifiers.conjectureGen = false;
+      opts.writeQuantifiers().conjectureGen = false;
     }
   }
   // can't pre-skolemize nested quantifiers without UF theory
@@ -1616,17 +1620,17 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   {
     if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
     {
-      opts.quantifiers.preSkolemQuantNested = false;
+      opts.writeQuantifiers().preSkolemQuantNested = false;
     }
   }
   if (!logic.isTheoryEnabled(THEORY_DATATYPES))
   {
-    opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::NONE;
+    opts.writeQuantifiers().quantDynamicSplit = options::QuantDSplitMode::NONE;
   }
   if (opts.quantifiers.globalNegate)
   {
     notifyModifyOption("deep-restart", "false", "global-negate");
-    opts.smt.deepRestartMode = options::DeepRestartMode::NONE;
+    opts.writeSmt().deepRestartMode = options::DeepRestartMode::NONE;
   }
 }
 
@@ -1635,24 +1639,24 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
   if (!opts.quantifiers.sygus)
   {
     notifyModifyOption("sygus", "true", "");
-    opts.quantifiers.sygus = true;
+    opts.writeQuantifiers().sygus = true;
   }
   // must use Ferrante/Rackoff for real arithmetic
   if (!opts.quantifiers.cegqiMidpointWasSetByUser)
   {
-    opts.quantifiers.cegqiMidpoint = true;
+    opts.writeQuantifiers().cegqiMidpoint = true;
   }
   // must disable cegqi-bv since it may introduce witness terms, which
   // cannot appear in synthesis solutions
   if (!opts.quantifiers.cegqiBvWasSetByUser)
   {
-    opts.quantifiers.cegqiBv = false;
+    opts.writeQuantifiers().cegqiBv = false;
   }
   if (opts.quantifiers.sygusRepairConst)
   {
     if (!opts.quantifiers.cegqiWasSetByUser)
     {
-      opts.quantifiers.cegqi = true;
+      opts.writeQuantifiers().cegqi = true;
     }
   }
   if (opts.quantifiers.sygusInference)
@@ -1660,42 +1664,43 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
     // optimization: apply preskolemization, makes it succeed more often
     if (!opts.quantifiers.preSkolemQuantWasSetByUser)
     {
-      opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::ON;
+      opts.writeQuantifiers().preSkolemQuant = options::PreSkolemQuantMode::ON;
     }
     if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
     {
-      opts.quantifiers.preSkolemQuantNested = true;
+      opts.writeQuantifiers().preSkolemQuantNested = true;
     }
   }
   // counterexample-guided instantiation for sygus
   if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
   {
-    opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE;
+    opts.writeQuantifiers().cegqiSingleInvMode =
+        options::CegqiSingleInvMode::USE;
   }
   if (!opts.quantifiers.conflictBasedInstWasSetByUser)
   {
-    opts.quantifiers.conflictBasedInst = false;
+    opts.writeQuantifiers().conflictBasedInst = false;
   }
   if (!opts.quantifiers.instNoEntailWasSetByUser)
   {
-    opts.quantifiers.instNoEntail = false;
+    opts.writeQuantifiers().instNoEntail = false;
   }
   if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
   {
     // should use full effort cbqi for single invocation and repair const
-    opts.quantifiers.cegqiFullEffort = true;
+    opts.writeQuantifiers().cegqiFullEffort = true;
   }
   if (opts.quantifiers.sygusRewSynthInput)
   {
     // If we are using synthesis rewrite rules from input, we use
     // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
     // details on this technique.
-    opts.quantifiers.sygusRewSynth = true;
+    opts.writeQuantifiers().sygusRewSynth = true;
     // we should not use the extended rewriter, since we are interested
     // in rewrites that are not in the main rewriter
     if (!opts.datatypes.sygusRewriterWasSetByUser)
     {
-      opts.datatypes.sygusRewriter = options::SygusRewriterMode::BASIC;
+      opts.writeDatatypes().sygusRewriter = options::SygusRewriterMode::BASIC;
     }
   }
   // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
@@ -1709,7 +1714,8 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
     // if doing abduction, we should filter strong solutions
     if (!opts.quantifiers.sygusFilterSolModeWasSetByUser)
     {
-      opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG;
+      opts.writeQuantifiers().sygusFilterSolMode =
+          options::SygusFilterSolMode::STRONG;
     }
     // we must use basic sygus algorithms, since e.g. we require checking
     // a sygus side condition for consistency with axioms.
@@ -1719,7 +1725,7 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
       || opts.quantifiers.sygusQueryGen != options::SygusQueryGenMode::NONE)
   {
     // rewrite rule synthesis implies that sygus stream must be true
-    opts.quantifiers.sygusStream = true;
+    opts.writeQuantifiers().sygusStream = true;
   }
   if (opts.quantifiers.sygusStream || opts.base.incrementalSolving)
   {
@@ -1732,30 +1738,32 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
   {
     if (!opts.quantifiers.sygusUnifPbeWasSetByUser)
     {
-      opts.quantifiers.sygusUnifPbe = false;
+      opts.writeQuantifiers().sygusUnifPbe = false;
     }
     if (opts.quantifiers.sygusUnifPiWasSetByUser)
     {
-      opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE;
+      opts.writeQuantifiers().sygusUnifPi = options::SygusUnifPiMode::NONE;
     }
     if (!opts.quantifiers.sygusInvTemplModeWasSetByUser)
     {
-      opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE;
+      opts.writeQuantifiers().sygusInvTemplMode =
+          options::SygusInvTemplMode::NONE;
     }
     if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
     {
-      opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE;
+      opts.writeQuantifiers().cegqiSingleInvMode =
+          options::CegqiSingleInvMode::NONE;
     }
   }
   // do not miniscope
   if (!opts.quantifiers.miniscopeQuantWasSetByUser)
   {
-    opts.quantifiers.miniscopeQuant = options::MiniscopeQuantMode::OFF;
+    opts.writeQuantifiers().miniscopeQuant = options::MiniscopeQuantMode::OFF;
   }
   // do not do macros
   if (!opts.quantifiers.macrosQuantWasSetByUser)
   {
-    opts.quantifiers.macrosQuant = false;
+    opts.writeQuantifiers().macrosQuant = false;
   }
 }
 void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic,
@@ -1817,12 +1825,12 @@ void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic,
                     ? true
                     : false);
 
-  opts.decision.decisionMode = decMode;
+  opts.writeDecision().decisionMode = decMode;
   if (stoponly)
   {
     if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION)
     {
-      opts.decision.decisionMode = options::DecisionMode::STOPONLY;
+      opts.writeDecision().decisionMode = options::DecisionMode::STOPONLY;
     }
     else
     {

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 2e11da69e128c21e3d8c50f6aabec3d483c5ba5c..6c7b3d419fc37f183ad09c43ee378f4ad7a6f53c 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -346,8 +346,7 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value)
 
   if (key == "filename")
   {
-    d_env->d_options.driver.filename = value;
-    d_env->d_originalOptions->driver.filename = value;
+    d_env->d_options.writeDriver().filename = value;
     d_env->getStatisticsRegistry().registerValue<std::string>(
         "driver::filename", value);
   }
@@ -360,12 +359,12 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value)
                 << " unsupported, defaulting to language (and semantics of) "
                    "SMT-LIB 2.6\n";
     }
-    getOptions().base.inputLanguage = Language::LANG_SMTLIB_V2_6;
+    getOptions().writeBase().inputLanguage = Language::LANG_SMTLIB_V2_6;
     // also update the output language
     if (!getOptions().base.outputLanguageWasSetByUser)
     {
       setOption("output-language", "smtlib2.6");
-      getOptions().base.outputLanguageWasSetByUser = false;
+      getOptions().writeBase().outputLanguageWasSetByUser = false;
     }
   }
   else if (key == "status")
@@ -1391,10 +1390,10 @@ std::vector<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& core)
     std::unique_ptr<SolverEngine> coreChecker;
     initializeSubsolver(coreChecker, *d_env.get());
     coreChecker->setLogic(getLogicInfo());
-    coreChecker->getOptions().smt.checkUnsatCores = false;
+    coreChecker->getOptions().writeSmt().checkUnsatCores = false;
     // disable all proof options
-    coreChecker->getOptions().smt.produceProofs = false;
-    coreChecker->getOptions().smt.checkProofs = false;
+    coreChecker->getOptions().writeSmt().produceProofs = false;
+    coreChecker->getOptions().writeSmt().checkProofs = false;
 
     for (const Node& ucAssertion : core)
     {
@@ -1458,10 +1457,10 @@ void SolverEngine::checkUnsatCore()
   // initialize the core checker
   std::unique_ptr<SolverEngine> coreChecker;
   initializeSubsolver(coreChecker, *d_env.get());
-  coreChecker->getOptions().smt.checkUnsatCores = false;
+  coreChecker->getOptions().writeSmt().checkUnsatCores = false;
   // disable all proof options
-  coreChecker->getOptions().smt.produceProofs = false;
-  coreChecker->getOptions().smt.checkProofs = false;
+  coreChecker->getOptions().writeSmt().produceProofs = false;
+  coreChecker->getOptions().writeSmt().checkProofs = false;
 
   // set up separation logic heap if necessary
   TypeNode sepLocType, sepDataType;
@@ -1910,16 +1909,16 @@ void SolverEngine::setResourceLimit(uint64_t units, bool cumulative)
 {
   if (cumulative)
   {
-    d_env->d_options.base.cumulativeResourceLimit = units;
+    d_env->d_options.writeBase().cumulativeResourceLimit = units;
   }
   else
   {
-    d_env->d_options.base.perCallResourceLimit = units;
+    d_env->d_options.writeBase().perCallResourceLimit = units;
   }
 }
 void SolverEngine::setTimeLimit(uint64_t millis)
 {
-  d_env->d_options.base.perCallMillisecondLimit = millis;
+  d_env->d_options.writeBase().perCallMillisecondLimit = millis;
 }
 
 unsigned long SolverEngine::getResourceUsage() const

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 2a5bf1b51e0a86604c115549955cb23070cc1ebc..e14c6041b67549357e2dd9da04f75cff1352020d 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -376,8 +376,8 @@ void SygusSolver::checkSynthSolution(Assertions& as,
     // Start new SMT engine to check solutions
     std::unique_ptr<SolverEngine> solChecker;
     initializeSygusSubsolver(solChecker, as);
-    solChecker->getOptions().smt.checkSynthSol = false;
-    solChecker->getOptions().quantifiers.sygusRecFun = false;
+    solChecker->getOptions().writeSmt().checkSynthSol = false;
+    solChecker->getOptions().writeQuantifiers().sygusRecFun = false;
     Assert(conj.getKind() == FORALL);
     Node conjBody = conj[1];
     // we must expand definitions here, since define-fun may contain the

diff --git a/src/theory/quantifiers/query_generator_unsat.cpp b/src/theory/quantifiers/query_generator_unsat.cpp
index 67a3667c37eb81611e8a593733f56c6ddff7a47b..a8f248e05c657bbad5c72668d779f56c7afd4b6a 100644 (file)
--- a/src/theory/quantifiers/query_generator_unsat.cpp
+++ b/src/theory/quantifiers/query_generator_unsat.cpp
@@ -32,11 +32,11 @@ QueryGeneratorUnsat::QueryGeneratorUnsat(Env& env) : QueryGenerator(env)
   // determine the options to use for the verification subsolvers we spawn
   // we start with the provided options
   d_subOptions.copyValues(d_env.getOriginalOptions());
-  d_subOptions.quantifiers.sygus = false;
-  d_subOptions.smt.produceProofs = true;
-  d_subOptions.smt.checkProofs = true;
-  d_subOptions.smt.produceModels = true;
-  d_subOptions.smt.checkModels = true;
+  d_subOptions.writeQuantifiers().sygus = false;
+  d_subOptions.writeSmt().produceProofs = true;
+  d_subOptions.writeSmt().checkProofs = true;
+  d_subOptions.writeSmt().produceModels = true;
+  d_subOptions.writeSmt().checkModels = true;
 }
 
 bool QueryGeneratorUnsat::addTerm(Node n, std::ostream& out)

diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index a6b0512750bae8d69709a2b444867aefd60c687b..a217fc7e8cdb1110cdb1c305a323a8070c90a391 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -40,24 +40,24 @@ SynthVerify::SynthVerify(Env& env, TermDbSygus* tds)
   // we start with the provided options
   d_subOptions.copyValues(options());
   // limit the number of instantiation rounds on subcalls
-  d_subOptions.quantifiers.instMaxRounds =
+  d_subOptions.writeQuantifiers().instMaxRounds =
       d_subOptions.quantifiers.sygusVerifyInstMaxRounds;
   // Disable sygus on the subsolver. This is particularly important since it
   // ensures that recursive function definitions have the standard ownership
   // instead of being claimed by sygus in the subsolver.
-  d_subOptions.base.inputLanguage = Language::LANG_SMTLIB_V2_6;
-  d_subOptions.quantifiers.sygus = false;
+  d_subOptions.writeBase().inputLanguage = Language::LANG_SMTLIB_V2_6;
+  d_subOptions.writeQuantifiers().sygus = false;
   // use tangent planes by default, since we want to put effort into
   // the verification step for sygus queries with non-linear arithmetic
   if (!d_subOptions.arith.nlExtTangentPlanesWasSetByUser)
   {
-    d_subOptions.arith.nlExtTangentPlanes = true;
+    d_subOptions.writeArith().nlExtTangentPlanes = true;
   }
   // we must use the same setting for datatype selectors, since shared selectors
   // can appear in solutions
-  d_subOptions.datatypes.dtSharedSelectors =
+  d_subOptions.writeDatatypes().dtSharedSelectors =
       options().datatypes.dtSharedSelectors;
-  d_subOptions.datatypes.dtSharedSelectorsWasSetByUser = true;
+  d_subOptions.writeDatatypes().dtSharedSelectorsWasSetByUser = true;
 }
 
 SynthVerify::~SynthVerify() {}

diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index f0e8d0be83df0a940bd3cd18e389e81cc8dd798b..95e5faf6b2fa037b34379f9494016f815e1c553b 100644 (file)
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -68,8 +68,8 @@ class TestNodeBlackNode : public TestNode
     TestNode::SetUp();
     // setup an SMT engine so that options are in scope
     Options opts;
-    opts.base.outputLanguage = Language::LANG_AST;
-    opts.base.outputLanguageWasSetByUser = true;
+    opts.writeBase().outputLanguage = Language::LANG_AST;
+    opts.writeBase().outputLanguageWasSetByUser = true;
     d_slvEngine.reset(new SolverEngine(d_nodeManager, &opts));
   }
 

diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp
index 912e21147cb94775dbc822b876c3b782e32fc569..da828a0cb80b5a2044956141a3165c86887f1bbd 100644 (file)
--- a/test/unit/theory/theory_arith_coverings_white.cpp
+++ b/test/unit/theory/theory_arith_coverings_white.cpp
@@ -383,8 +383,8 @@ TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1)
 {
   Options opts;
   // enable proofs
-  opts.smt.proofMode = options::ProofMode::FULL;
-  opts.smt.produceProofs = true;
+  opts.writeSmt().proofMode = options::ProofMode::FULL;
+  opts.writeSmt().produceProofs = true;
   Env env(NodeManager::currentNM(), &opts);
   opts.handler().setDefaultDagThresh("--dag-thresh", 0);
   smt::PfManager pfm(env);