Remove `Options::wasSetByUser()` (#6682)

This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 73de9209bd38ccb56e66b2a6ddbf3ff12429cda0..7e1cf68e44d4915dc68e7e93b02a5598d12b85ef 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -75,7 +75,7 @@ void assign_{module}_{name}(Options& opts, const std::string& option, const std:
   auto value = {handler};
   {predicates}
   opts.{module}.{name} = value;
-  opts.{module}.{name}__setByUser = true;
+  opts.{module}.{name}WasSetByUser = true;
   Trace("options") << "user assigned option {name} = " << value << std::endl;
 }}'''
 
@@ -83,7 +83,7 @@ TPL_ASSIGN_BOOL = '''
 void assign_{module}_{name}(Options& opts, const std::string& option, bool value) {{
   {predicates}
   opts.{module}.{name} = value;
-  opts.{module}.{name}__setByUser = true;
+  opts.{module}.{name}WasSetByUser = true;
   Trace("options") << "user assigned option {name} = " << value << std::endl;
 }}'''
 
@@ -95,15 +95,15 @@ TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));'
 TPL_GETOPT_LONG = '{{ "{}", {}_argument, nullptr, {} }},'
 
 TPL_HOLDER_MACRO_ATTR = '''  {type} {name};
-  bool {name}__setByUser = false;'''
+  bool {name}WasSetByUser = false;'''
 
 TPL_HOLDER_MACRO_ATTR_DEF = '''  {type} {name} = {default};
-  bool {name}__setByUser = false;'''
+  bool {name}WasSetByUser = false;'''
 
 TPL_DECL_SET_DEFAULT = 'void setDefault{funcname}(Options& opts, {type} value);'
 TPL_IMPL_SET_DEFAULT = TPL_DECL_SET_DEFAULT[:-1] + '''
 {{
-    if (!opts.{module}.{name}__setByUser) {{
+    if (!opts.{module}.{name}WasSetByUser) {{
         opts.{module}.{name} = value;
     }}
 }}'''
@@ -117,15 +117,6 @@ TPL_OPTION_STRUCT_RW = \
   type operator()() const;
 }} thread_local {name};"""
 
-TPL_DECL_WAS_SET_BY_USER = \
-"""template <> bool Options::wasSetByUser(options::{name}__option_t) const;"""
-
-TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \
-"""
-{{
-  return {module}.{name}__setByUser;
-}}"""
-
 # Option specific methods
 
 TPL_IMPL_OP_PAR = \
@@ -556,7 +547,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
 
         # Generate module specialization
         default_decl.append(TPL_DECL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type))
-        specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name))
 
         if option.long and option.type not in ['bool', 'void'] and \
            '=' not in option.long:
@@ -577,7 +567,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
 
         # Accessors
         default_impl.append(TPL_IMPL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type))
-        accs.append(TPL_IMPL_WAS_SET_BY_USER.format(module=module.id, name=option.name))
 
         # Global definitions
         defs.append('thread_local struct {name}__option_t {name};'.format(name=option.name))
@@ -925,7 +914,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
                 if option.mode and option.type not in default:
                     default = '{}::{}'.format(option.type, default)
                 defaults.append('{}({})'.format(option.name, default))
-                defaults.append('{}__setByUser(false)'.format(option.name))
+                defaults.append('{}WasSetByUser(false)'.format(option.name))
 
     write_file(dst_dir, 'options.h', tpl_options_h.format(
         holder_fwd_decls=get_holder_fwd_decls(modules),

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 1178f205dfee74225bdff6a91be26e10c9b325b0..d06c64517c70034aabcede8ca61b6664c39d6328 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -159,7 +159,7 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
           || m == SatSolverMode::KISSAT))
   {
     if (options::bitblastMode() == options::BitblastMode::LAZY
-        && Options::current().wasSetByUser(options::bitblastMode))
+        && d_options->bv.bitblastModeWasSetByUser)
     {
       throwLazyBBUnsupported(m);
     }
@@ -189,7 +189,7 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m)
 void OptionsHandler::setBitblastAig(std::string option, bool arg)
 {
   if(arg) {
-    if(Options::current().wasSetByUser(options::bitblastMode)) {
+    if (d_options->bv.bitblastModeWasSetByUser) {
       if (options::bitblastMode() != options::BitblastMode::EAGER)
       {
         throw OptionException("bitblast-aig must be used with eager bitblaster");

diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
index f590ba0837029b87cab59ad203bd63276c55f8cd..7d72496aa94a43868797c0b9837e9cd11bae718c 100644 (file)
--- a/src/options/options_public.cpp
+++ b/src/options/options_public.cpp
@@ -120,19 +120,19 @@ void setOutputLanguage(OutputLanguage val, Options& opts)
 
 bool wasSetByUserEarlyExit(const Options& opts)
 {
-  return opts.driver.earlyExit__setByUser;
+  return opts.driver.earlyExitWasSetByUser;
 }
 bool wasSetByUserForceLogicString(const Options& opts)
 {
-  return opts.parser.forceLogicString__setByUser;
+  return opts.parser.forceLogicStringWasSetByUser;
 }
 bool wasSetByUserIncrementalSolving(const Options& opts)
 {
-  return opts.smt.incrementalSolving__setByUser;
+  return opts.smt.incrementalSolvingWasSetByUser;
 }
 bool wasSetByUserInteractive(const Options& opts)
 {
-  return opts.driver.interactive__setByUser;
+  return opts.driver.interactiveWasSetByUser;
 }
 
 }  // namespace cvc5::options

diff --git a/src/options/options_template.h b/src/options/options_template.h
index 6ce77d7a1377a5267c9b39c44a5d3d415b5f0426..76c599d23b14a98ccd4a95c7153977b2a98bc5e2 100644 (file)
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -136,15 +136,6 @@ public:
   // TODO: Document these.
   static std::ostream* currentGetOut();
 
-  /**
-   * Returns true iff the value of the given option was set
-   * by the user via a command-line option or SmtEngine::setOption().
-   * (Options::set() is low-level and doesn't count.)  Returns false
-   * otherwise.
-   */
-  template <class T>
-  bool wasSetByUser(T) const;
-
   /**
    * Get a description of the command-line flags accepted by
    * parseOptions.  The returned string will be escaped so that it is

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 048f5d06bb5c1d20019ea803637cbbbe98f68ec4..b733f62ce4e543d408a90d229847283439b68bc3 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -135,12 +135,12 @@ Printer* Printer::getPrinter(OutputLanguage lang)
     // the singleton "null" expr.  So we guard against segfault
     if (not Options::isCurrentNull())
     {
-      if (Options::current().wasSetByUser(options::outputLanguage))
+      if (Options::current().base.outputLanguageWasSetByUser)
       {
         lang = options::outputLanguage();
       }
       if (lang == language::output::LANG_AUTO
-          && Options::current().wasSetByUser(options::inputLanguage))
+          && Options::current().base.inputLanguageWasSetByUser)
       {
         lang = language::toOutputLanguage(options::inputLanguage());
       }

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 74cbadfc2f0b38362819be62ef3a63ca86a8668e..04db5e3cbc3a34431ddaa6c3684e08b50acb454f 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -76,7 +76,7 @@ SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy,
       n_touched(0)
 {
     if(options::minisatUseElim() &&
-       Options::current().wasSetByUser(options::minisatUseElim) &&
+       Options::current().prop.minisatUseElimWasSetByUser &&
        enableIncremental) {
         WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl;
     }

diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 37541751ee310156064abf381a2338336a32f665..4d6be68b855ab7d63a21f052cd14f737d90a89ef 100644 (file)
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -31,31 +31,31 @@ namespace smt {
 OptionsManager::OptionsManager(Options* opts) : d_options(opts)
 {
   // set options that must take effect immediately
-  if (opts->wasSetByUser(options::defaultExprDepth))
+  if (opts->expr.defaultExprDepthWasSetByUser)
   {
     notifySetOption(options::expr::defaultExprDepth__name);
   }
-  if (opts->wasSetByUser(options::defaultDagThresh))
+  if (opts->expr.defaultDagThreshWasSetByUser)
   {
     notifySetOption(options::expr::defaultDagThresh__name);
   }
-  if (opts->wasSetByUser(options::dumpModeString))
+  if (opts->smt.dumpModeStringWasSetByUser)
   {
     notifySetOption(options::smt::dumpModeString__name);
   }
-  if (opts->wasSetByUser(options::printSuccess))
+  if (opts->base.printSuccessWasSetByUser)
   {
     notifySetOption(options::base::printSuccess__name);
   }
-  if (opts->wasSetByUser(options::diagnosticChannelName))
+  if (opts->smt.diagnosticChannelNameWasSetByUser)
   {
     notifySetOption(options::smt::diagnosticChannelName__name);
   }
-  if (opts->wasSetByUser(options::regularChannelName))
+  if (opts->smt.regularChannelNameWasSetByUser)
   {
     notifySetOption(options::smt::regularChannelName__name);
   }
-  if (opts->wasSetByUser(options::dumpToFileName))
+  if (opts->smt.dumpToFileNameWasSetByUser)
   {
     notifySetOption(options::smt::dumpToFileName__name);
   }

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 96081e97b6e1170da90ffbf35e6a7c0916a80247..b9095c91b406369864be75ac30d67479f26aa0ed 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -77,7 +77,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::unsatCores()
       && options::unsatCoresMode() == options::UnsatCoresMode::OFF)
   {
-    if (opts.wasSetByUser(options::unsatCoresMode))
+    if (opts.smt.unsatCoresModeWasSetByUser)
     {
       Notice()
           << "Overriding OFF unsat-core mode since cores were requested.\n";
@@ -93,7 +93,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::produceProofs()
       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
   {
-    if (opts.wasSetByUser(options::unsatCoresMode))
+    if (opts.smt.unsatCoresModeWasSetByUser)
     {
       Notice() << "Forcing full-proof mode for unsat cores mode since proofs "
                   "were requested.\n";
@@ -106,7 +106,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // set proofs on if not yet set
   if (options::unsatCores() && !options::produceProofs())
   {
-    if (opts.wasSetByUser(options::produceProofs))
+    if (opts.smt.produceProofsWasSetByUser)
     {
       Notice()
           << "Forcing proof production since new unsat cores were requested.\n";
@@ -118,12 +118,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   Assert(options::unsatCores()
          == (options::unsatCoresMode() != options::UnsatCoresMode::OFF));
 
-  if (opts.wasSetByUser(options::bitvectorAigSimplifications))
+  if (opts.bv.bitvectorAigSimplificationsWasSetByUser)
   {
     Notice() << "SmtEngine: setting bitvectorAig" << std::endl;
     opts.bv.bitvectorAig = true;
   }
-  if (opts.wasSetByUser(options::bitvectorAlgebraicBudget))
+  if (opts.bv.bitvectorAlgebraicBudgetWasSetByUser)
   {
     Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl;
     opts.bv.bitvectorAlgebraicSolver = true;
@@ -138,8 +138,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
         && (logic.isTheoryEnabled(THEORY_ARRAYS)
             || logic.isTheoryEnabled(THEORY_UF)))
     {
-      if (opts.wasSetByUser(options::bitblastMode)
-          || opts.wasSetByUser(options::produceModels))
+      if (opts.bv.bitblastModeWasSetByUser
+          || opts.smt.produceModelsWasSetByUser)
       {
         throw OptionException(std::string(
             "Eager bit-blasting currently does not support model generation "
@@ -228,7 +228,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       && (logic.isTheoryEnabled(THEORY_ARRAYS)
           || logic.isTheoryEnabled(THEORY_UF)))
   {
-    if (opts.wasSetByUser(options::produceModels))
+    if (opts.smt.produceModelsWasSetByUser)
     {
       throw OptionException(std::string(
           "Ackermannization currently does not support model generation."));
@@ -271,7 +271,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // this by default.
   if (options::doITESimp())
   {
-    if (!opts.wasSetByUser(options::earlyIteRemoval))
+    if (!opts.smt.earlyIteRemovalWasSetByUser)
     {
       opts.smt.earlyIteRemoval = true;
     }
@@ -298,7 +298,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                    << std::endl;
     }
     // We require bounded quantifier handling.
-    if (!opts.wasSetByUser(options::fmfBound))
+    if (!opts.quantifiers.fmfBoundWasSetByUser)
     {
       opts.quantifiers.fmfBound = true;
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
@@ -320,7 +320,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
   {
     // no fine-graininess
-    if (!opts.wasSetByUser(options::proofGranularityMode))
+    if (!opts.proof.proofGranularityModeWasSetByUser)
     {
       opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF;
     }
@@ -335,7 +335,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       logic.lock();
     }
     // Allows to answer sat more often by default.
-    if (!opts.wasSetByUser(options::fmfBound))
+    if (!opts.quantifiers.fmfBoundWasSetByUser)
     {
       opts.quantifiers.fmfBound = true;
       Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl;
@@ -424,7 +424,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::unconstrainedSimp())
     {
-      if (opts.wasSetByUser(options::unconstrainedSimp))
+      if (opts.smt.unconstrainedSimpWasSetByUser)
       {
         throw OptionException(
             "unconstrained simplification not supported with old unsat "
@@ -439,7 +439,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   else
   {
     // Turn on unconstrained simplification for QF_AUFBV
-    if (!opts.wasSetByUser(options::unconstrainedSimp))
+    if (!opts.smt.unconstrainedSimpWasSetByUser)
     {
       bool uncSimp = !logic.isQuantified() && !options::produceModels()
                      && !options::produceAssignments()
@@ -457,7 +457,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::sygusInference())
     {
-      if (opts.wasSetByUser(options::sygusInference))
+      if (opts.quantifiers.sygusInferenceWasSetByUser)
       {
         throw OptionException(
             "sygus inference not supported with incremental solving");
@@ -486,7 +486,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::simplificationMode() != options::SimplificationMode::NONE)
     {
-      if (opts.wasSetByUser(options::simplificationMode))
+      if (opts.smt.simplificationModeWasSetByUser)
       {
         throw OptionException(
             "simplification not supported with old unsat cores");
@@ -499,7 +499,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     if (options::pbRewrites())
     {
-      if (opts.wasSetByUser(options::pbRewrites))
+      if (opts.arith.pbRewritesWasSetByUser)
       {
         throw OptionException(
             "pseudoboolean rewrites not supported with old unsat cores");
@@ -511,7 +511,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     if (options::sortInference())
     {
-      if (opts.wasSetByUser(options::sortInference))
+      if (opts.smt.sortInferenceWasSetByUser)
       {
         throw OptionException(
             "sort inference not supported with old unsat cores");
@@ -523,7 +523,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     if (options::preSkolemQuant())
     {
-      if (opts.wasSetByUser(options::preSkolemQuant))
+      if (opts.quantifiers.preSkolemQuantWasSetByUser)
       {
         throw OptionException(
             "pre-skolemization not supported with old unsat cores");
@@ -535,7 +535,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     if (options::bitvectorToBool())
     {
-      if (opts.wasSetByUser(options::bitvectorToBool))
+      if (opts.bv.bitvectorToBoolWasSetByUser)
       {
         throw OptionException("bv-to-bool not supported with old unsat cores");
       }
@@ -546,7 +546,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     if (options::boolToBitvector() != options::BoolToBVMode::OFF)
     {
-      if (opts.wasSetByUser(options::boolToBitvector))
+      if (opts.bv.boolToBitvectorWasSetByUser)
       {
         throw OptionException(
             "bool-to-bv != off not supported with old unsat cores");
@@ -558,7 +558,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     if (options::bvIntroducePow2())
     {
-      if (opts.wasSetByUser(options::bvIntroducePow2))
+      if (opts.bv.bvIntroducePow2WasSetByUser)
       {
         throw OptionException(
             "bv-intro-pow2 not supported with old unsat cores");
@@ -570,7 +570,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     if (options::repeatSimp())
     {
-      if (opts.wasSetByUser(options::repeatSimp))
+      if (opts.smt.repeatSimpWasSetByUser)
       {
         throw OptionException("repeat-simp not supported with old unsat cores");
       }
@@ -581,7 +581,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
     if (options::globalNegate())
     {
-      if (opts.wasSetByUser(options::globalNegate))
+      if (opts.quantifiers.globalNegateWasSetByUser)
       {
         throw OptionException(
             "global-negate not supported with old unsat cores");
@@ -604,7 +604,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   else
   {
     // by default, nonclausal simplification is off for QF_SAT
-    if (!opts.wasSetByUser(options::simplificationMode))
+    if (!opts.smt.simplificationModeWasSetByUser)
     {
       bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified();
       Trace("smt") << "setting simplification mode to <"
@@ -623,7 +623,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::boolToBitvector() != options::BoolToBVMode::OFF)
     {
-      if (opts.wasSetByUser(options::boolToBitvector))
+      if (opts.bv.boolToBitvectorWasSetByUser)
       {
         throw OptionException(
             "bool-to-bv != off not supported with CBQI BV for quantified "
@@ -682,7 +682,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     needsUf = true;
   }
   else if (options::preSkolemQuantNested()
-           && opts.wasSetByUser(options::preSkolemQuantNested))
+           && opts.quantifiers.preSkolemQuantNestedWasSetByUser)
   {
     // if pre-skolem nested is explictly set, then we require UF. If it is
     // not explicitly set, it is disabled below if UF is not present.
@@ -737,7 +737,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   /////////////////////////////////////////////////////////////////////////////
 
   // Set the options for the theoryOf
-  if (!opts.wasSetByUser(options::theoryOfMode))
+  if (!opts.theory.theoryOfModeWasSetByUser)
   {
     if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
         && !logic.isTheoryEnabled(THEORY_STRINGS)
@@ -752,7 +752,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // by default, symmetry breaker is on only for non-incremental QF_UF
-  if (!opts.wasSetByUser(options::ufSymmetryBreaker))
+  if (!opts.uf.ufSymmetryBreakerWasSetByUser)
   {
     bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
                        && !options::incrementalSolving() && !safeUnsatCores;
@@ -774,7 +774,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Theory::setUninterpretedSortOwner(THEORY_UF);
   }
 
-  if (!opts.wasSetByUser(options::simplifyWithCareEnabled))
+  if (!opts.smt.simplifyWithCareEnabledWasSetByUser)
   {
     bool qf_aufbv =
         !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
@@ -786,7 +786,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.smt.simplifyWithCareEnabled = withCare;
   }
   // Turn off array eager index splitting for QF_AUFLIA
-  if (!opts.wasSetByUser(options::arraysEagerIndexSplitting))
+  if (!opts.arrays.arraysEagerIndexSplittingWasSetByUser)
   {
     if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
         && logic.isTheoryEnabled(THEORY_UF)
@@ -798,7 +798,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
-  if (!opts.wasSetByUser(options::repeatSimp))
+  if (!opts.smt.repeatSimpWasSetByUser)
   {
     bool repeatSimp = !logic.isQuantified()
                       && (logic.isTheoryEnabled(THEORY_ARRAYS)
@@ -813,7 +813,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::boolToBitvector() == options::BoolToBVMode::ALL
       && !logic.isTheoryEnabled(THEORY_BV))
   {
-    if (opts.wasSetByUser(options::boolToBitvector))
+    if (opts.bv.boolToBitvectorWasSetByUser)
     {
       throw OptionException(
           "bool-to-bv=all not supported for non-bitvector logics.");
@@ -823,7 +823,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
   }
 
-  if (!opts.wasSetByUser(options::bvEagerExplanations)
+  if (!opts.bv.bvEagerExplanationsWasSetByUser
       && logic.isTheoryEnabled(THEORY_ARRAYS)
       && logic.isTheoryEnabled(THEORY_BV))
   {
@@ -832,7 +832,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // Turn on arith rewrite equalities only for pure arithmetic
-  if (!opts.wasSetByUser(options::arithRewriteEq))
+  if (!opts.arith.arithRewriteEqWasSetByUser)
   {
     bool arithRewriteEq =
         logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified();
@@ -840,7 +840,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                  << std::endl;
     opts.arith.arithRewriteEq = arithRewriteEq;
   }
-  if (!opts.wasSetByUser(options::arithHeuristicPivots))
+  if (!opts.arith.arithHeuristicPivotsWasSetByUser)
   {
     int16_t heuristicPivots = 5;
     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
@@ -858,7 +858,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                  << std::endl;
     opts.arith.arithHeuristicPivots = heuristicPivots;
   }
-  if (!opts.wasSetByUser(options::arithPivotThreshold))
+  if (!opts.arith.arithPivotThresholdWasSetByUser)
   {
     uint16_t pivotThreshold = 2;
     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
@@ -872,7 +872,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                  << std::endl;
     opts.arith.arithPivotThreshold = pivotThreshold;
   }
-  if (!opts.wasSetByUser(options::arithStandardCheckVarOrderPivots))
+  if (!opts.arith.arithStandardCheckVarOrderPivotsWasSetByUser)
   {
     int16_t varOrderPivots = -1;
     if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
@@ -885,7 +885,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed())
   {
-    if (!opts.wasSetByUser(options::nlExtTangentPlanesInterleave))
+    if (!opts.arith.nlExtTangentPlanesInterleaveWasSetByUser)
     {
       Trace("smt") << "setting nlExtTangentPlanesInterleave to true"
                    << std::endl;
@@ -894,7 +894,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // Set decision mode based on logic (if not set by user)
-  if (!opts.wasSetByUser(options::decisionMode))
+  if (!opts.decision.decisionModeWasSetByUser)
   {
     options::DecisionMode decMode =
         // anything that uses sygus uses internal
@@ -974,8 +974,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.quantifiers.cegqi = false;
   }
 
-  if ((opts.wasSetByUser(options::fmfBoundLazy) && options::fmfBoundLazy())
-      || (opts.wasSetByUser(options::fmfBoundInt) && options::fmfBoundInt()))
+  if ((opts.quantifiers.fmfBoundLazyWasSetByUser && options::fmfBoundLazy())
+      || (opts.quantifiers.fmfBoundIntWasSetByUser && options::fmfBoundInt()))
   {
     opts.quantifiers.fmfBound = true;
   }
@@ -983,14 +983,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // apply fmfBoundInt options
   if (options::fmfBound())
   {
-    if (!opts.wasSetByUser(options::mbqiMode)
+    if (!opts.quantifiers.mbqiModeWasSetByUser
         || (options::mbqiMode() != options::MbqiMode::NONE
             && options::mbqiMode() != options::MbqiMode::FMC))
     {
       // if bounded integers are set, use no MBQI by default
       opts.quantifiers.mbqiMode = options::MbqiMode::NONE;
     }
-    if (!opts.wasSetByUser(options::prenexQuant))
+    if (!opts.quantifiers.prenexQuantUserWasSetByUser)
     {
       opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
     }
@@ -1003,7 +1003,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       opts.quantifiers.mbqiMode = options::MbqiMode::NONE;
     }
-    if (!opts.wasSetByUser(options::hoElimStoreAx))
+    if (!opts.quantifiers.hoElimStoreAxWasSetByUser)
     {
       // by default, use store axioms only if --ho-elim is set
       opts.quantifiers.hoElimStoreAx = options::hoElim();
@@ -1022,14 +1022,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   if (options::fmfFunWellDefinedRelevant())
   {
-    if (!opts.wasSetByUser(options::fmfFunWellDefined))
+    if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser)
     {
       opts.quantifiers.fmfFunWellDefined = true;
     }
   }
   if (options::fmfFunWellDefined())
   {
-    if (!opts.wasSetByUser(options::finiteModelFind))
+    if (!opts.quantifiers.finiteModelFindWasSetByUser)
     {
       opts.quantifiers.finiteModelFind = true;
     }
@@ -1040,15 +1040,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::finiteModelFind())
   {
     // apply conservative quantifiers splitting
-    if (!opts.wasSetByUser(options::quantDynamicSplit))
+    if (!opts.quantifiers.quantDynamicSplitWasSetByUser)
     {
       opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT;
     }
-    if (!opts.wasSetByUser(options::eMatching))
+    if (!opts.quantifiers.eMatchingWasSetByUser)
     {
       opts.quantifiers.eMatching = options::fmfInstEngine();
     }
-    if (!opts.wasSetByUser(options::instWhenMode))
+    if (!opts.quantifiers.instWhenModeWasSetByUser)
     {
       // instantiate only on last call
       if (options::eMatching())
@@ -1068,19 +1068,19 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     opts.quantifiers.sygus = true;
     // must use Ferrante/Rackoff for real arithmetic
-    if (!opts.wasSetByUser(options::cegqiMidpoint))
+    if (!opts.quantifiers.cegqiMidpointWasSetByUser)
     {
       opts.quantifiers.cegqiMidpoint = true;
     }
     // must disable cegqi-bv since it may introduce witness terms, which
     // cannot appear in synthesis solutions
-    if (!opts.wasSetByUser(options::cegqiBv))
+    if (!opts.quantifiers.cegqiBvWasSetByUser)
     {
       opts.quantifiers.cegqiBv = false;
     }
     if (options::sygusRepairConst())
     {
-      if (!opts.wasSetByUser(options::cegqi))
+      if (!opts.quantifiers.cegqiWasSetByUser)
       {
         opts.quantifiers.cegqi = true;
       }
@@ -1088,29 +1088,29 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (options::sygusInference())
     {
       // optimization: apply preskolemization, makes it succeed more often
-      if (!opts.wasSetByUser(options::preSkolemQuant))
+      if (!opts.quantifiers.preSkolemQuantWasSetByUser)
       {
         opts.quantifiers.preSkolemQuant = true;
       }
-      if (!opts.wasSetByUser(options::preSkolemQuantNested))
+      if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
       {
         opts.quantifiers.preSkolemQuantNested = true;
       }
     }
     // counterexample-guided instantiation for sygus
-    if (!opts.wasSetByUser(options::cegqiSingleInvMode))
+    if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
     {
       opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE;
     }
-    if (!opts.wasSetByUser(options::quantConflictFind))
+    if (!opts.quantifiers.quantConflictFindWasSetByUser)
     {
       opts.quantifiers.quantConflictFind = false;
     }
-    if (!opts.wasSetByUser(options::instNoEntail))
+    if (!opts.quantifiers.instNoEntailWasSetByUser)
     {
       opts.quantifiers.instNoEntail = false;
     }
-    if (!opts.wasSetByUser(options::cegqiFullEffort))
+    if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
     {
       // should use full effort cbqi for single invocation and repair const
       opts.quantifiers.cegqiFullEffort = true;
@@ -1128,7 +1128,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.quantifiers.sygusRewSynth = true;
       // we should not use the extended rewriter, since we are interested
       // in rewrites that are not in the main rewriter
-      if (!opts.wasSetByUser(options::sygusExtRew))
+      if (!opts.quantifiers.sygusExtRewWasSetByUser)
       {
         opts.quantifiers.sygusExtRew = false;
       }
@@ -1142,7 +1142,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     if (options::produceAbducts())
     {
       // if doing abduction, we should filter strong solutions
-      if (!opts.wasSetByUser(options::sygusFilterSolMode))
+      if (!opts.quantifiers.sygusFilterSolModeWasSetByUser)
       {
         opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG;
       }
@@ -1165,48 +1165,48 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // Now, disable options for non-basic sygus algorithms, if necessary.
     if (reqBasicSygus)
     {
-      if (!opts.wasSetByUser(options::sygusUnifPbe))
+      if (!opts.quantifiers.sygusUnifPbeWasSetByUser)
       {
         opts.quantifiers.sygusUnifPbe = false;
       }
-      if (opts.wasSetByUser(options::sygusUnifPi))
+      if (opts.quantifiers.sygusUnifPiWasSetByUser)
       {
         opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE;
       }
-      if (!opts.wasSetByUser(options::sygusInvTemplMode))
+      if (!opts.quantifiers.sygusInvTemplModeWasSetByUser)
       {
         opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE;
       }
-      if (!opts.wasSetByUser(options::cegqiSingleInvMode))
+      if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
       {
         opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE;
       }
     }
-    if (!opts.wasSetByUser(options::dtRewriteErrorSel))
+    if (!opts.datatypes.dtRewriteErrorSelWasSetByUser)
     {
       opts.datatypes.dtRewriteErrorSel = true;
     }
     // do not miniscope
-    if (!opts.wasSetByUser(options::miniscopeQuant))
+    if (!opts.quantifiers.miniscopeQuantWasSetByUser)
     {
       opts.quantifiers.miniscopeQuant = false;
     }
-    if (!opts.wasSetByUser(options::miniscopeQuantFreeVar))
+    if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser)
     {
       opts.quantifiers.miniscopeQuantFreeVar = false;
     }
-    if (!opts.wasSetByUser(options::quantSplit))
+    if (!opts.quantifiers.quantSplitWasSetByUser)
     {
       opts.quantifiers.quantSplit = false;
     }
     // do not do macros
-    if (!opts.wasSetByUser(options::macrosQuant))
+    if (!opts.quantifiers.macrosQuantWasSetByUser)
     {
       opts.quantifiers.macrosQuant = false;
     }
     // use tangent planes by default, since we want to put effort into
     // the verification step for sygus queries with non-linear arithmetic
-    if (!opts.wasSetByUser(options::nlExtTangentPlanes))
+    if (!opts.arith.nlExtTangentPlanesWasSetByUser)
     {
       opts.arith.nlExtTangentPlanes = true;
     }
@@ -1220,14 +1220,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
            || logic.isTheoryEnabled(THEORY_FP)))
       || options::cegqiAll())
   {
-    if (!opts.wasSetByUser(options::cegqi))
+    if (!opts.quantifiers.cegqiWasSetByUser)
     {
       opts.quantifiers.cegqi = true;
     }
     // check whether we should apply full cbqi
     if (logic.isPure(THEORY_BV))
     {
-      if (!opts.wasSetByUser(options::cegqiFullEffort))
+      if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
       {
         opts.quantifiers.cegqiFullEffort = true;
       }
@@ -1242,15 +1242,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
     {
-      if (!opts.wasSetByUser(options::quantConflictFind))
+      if (!opts.quantifiers.quantConflictFindWasSetByUser)
       {
         opts.quantifiers.quantConflictFind = false;
       }
-      if (!opts.wasSetByUser(options::instNoEntail))
+      if (!opts.quantifiers.instNoEntailWasSetByUser)
       {
         opts.quantifiers.instNoEntail = false;
       }
-      if (!opts.wasSetByUser(options::instWhenMode) && options::cegqiModel())
+      if (!opts.quantifiers.instWhenModeWasSetByUser && options::cegqiModel())
       {
         // only instantiation should happen at last call when model is avaiable
         opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
@@ -1263,7 +1263,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     if (options::globalNegate())
     {
-      if (!opts.wasSetByUser(options::prenexQuant))
+      if (!opts.quantifiers.prenexQuantWasSetByUser)
       {
         opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
       }
@@ -1272,19 +1272,19 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // implied options...
   if (options::strictTriggers())
   {
-    if (!opts.wasSetByUser(options::userPatternsQuant))
+    if (!opts.quantifiers.userPatternsQuantWasSetByUser)
     {
       opts.quantifiers.userPatternsQuant = options::UserPatMode::TRUST;
     }
   }
-  if (opts.wasSetByUser(options::qcfMode) || options::qcfTConstraint())
+  if (opts.quantifiers.qcfModeWasSetByUser || options::qcfTConstraint())
   {
     opts.quantifiers.quantConflictFind = true;
   }
   if (options::cegqiNestedQE())
   {
     opts.quantifiers.prenexQuantUser = true;
-    if (!opts.wasSetByUser(options::preSkolemQuant))
+    if (!opts.quantifiers.preSkolemQuantWasSetByUser)
     {
       opts.quantifiers.preSkolemQuant = true;
     }
@@ -1292,11 +1292,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // for induction techniques
   if (options::quantInduction())
   {
-    if (!opts.wasSetByUser(options::dtStcInduction))
+    if (!opts.quantifiers.dtStcInductionWasSetByUser)
     {
       opts.quantifiers.dtStcInduction = true;
     }
-    if (!opts.wasSetByUser(options::intWfInduction))
+    if (!opts.quantifiers.intWfInductionWasSetByUser)
     {
       opts.quantifiers.intWfInduction = true;
     }
@@ -1304,38 +1304,38 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (options::dtStcInduction())
   {
     // try to remove ITEs from quantified formulas
-    if (!opts.wasSetByUser(options::iteDtTesterSplitQuant))
+    if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser)
     {
       opts.quantifiers.iteDtTesterSplitQuant = true;
     }
-    if (!opts.wasSetByUser(options::iteLiftQuant))
+    if (!opts.quantifiers.iteLiftQuantWasSetByUser)
     {
       opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL;
     }
   }
   if (options::intWfInduction())
   {
-    if (!opts.wasSetByUser(options::purifyTriggers))
+    if (!opts.quantifiers.purifyTriggersWasSetByUser)
     {
       opts.quantifiers.purifyTriggers = true;
     }
   }
   if (options::conjectureNoFilter())
   {
-    if (!opts.wasSetByUser(options::conjectureFilterActiveTerms))
+    if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser)
     {
       opts.quantifiers.conjectureFilterActiveTerms = false;
     }
-    if (!opts.wasSetByUser(options::conjectureFilterCanonical))
+    if (!opts.quantifiers.conjectureFilterCanonicalWasSetByUser)
     {
       opts.quantifiers.conjectureFilterCanonical = false;
     }
-    if (!opts.wasSetByUser(options::conjectureFilterModel))
+    if (!opts.quantifiers.conjectureFilterModelWasSetByUser)
     {
       opts.quantifiers.conjectureFilterModel = false;
     }
   }
-  if (opts.wasSetByUser(options::conjectureGenPerRound))
+  if (opts.quantifiers.conjectureGenPerRoundWasSetByUser)
   {
     if (options::conjectureGenPerRound() > 0)
     {
@@ -1349,7 +1349,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // can't pre-skolemize nested quantifiers without UF theory
   if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant())
   {
-    if (!opts.wasSetByUser(options::preSkolemQuantNested))
+    if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
     {
       opts.quantifiers.preSkolemQuantNested = false;
     }
@@ -1360,7 +1360,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // until bugs 371,431 are fixed
-  if (!opts.wasSetByUser(options::minisatUseElim))
+  if (!opts.prop.minisatUseElimWasSetByUser)
   {
     // cannot use minisat elimination for logics where a theory solver
     // introduces new literals into the search. This includes quantifiers
@@ -1382,7 +1382,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (!options::relevanceFilter())
     {
-      if (opts.wasSetByUser(options::relevanceFilter))
+      if (opts.theory.relevanceFilterWasSetByUser)
       {
         Warning() << "SmtEngine: turning on relevance filtering to support "
                      "--nl-ext-rlv="
@@ -1404,7 +1404,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::bvLazyRewriteExtf())
     {
-      if (opts.wasSetByUser(options::bvLazyRewriteExtf))
+      if (opts.bv.bvLazyRewriteExtfWasSetByUser)
       {
         throw OptionException(
             "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
@@ -1416,7 +1416,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.bv.bvLazyRewriteExtf = false;
   }
 
-  if (options::stringFMF() && !opts.wasSetByUser(options::stringProcessLoopMode))
+  if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser)
   {
     Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
                     "--strings-fmf enabled"
@@ -1427,7 +1427,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // !!! All options that require disabling models go here
   bool disableModels = false;
   std::string sOptNoModel;
-  if (opts.wasSetByUser(options::unconstrainedSimp) && options::unconstrainedSimp())
+  if (opts.smt.unconstrainedSimpWasSetByUser && options::unconstrainedSimp())
   {
     disableModels = true;
     sOptNoModel = "unconstrained-simp";
@@ -1451,7 +1451,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     if (options::produceModels())
     {
-      if (opts.wasSetByUser(options::produceModels))
+      if (opts.smt.produceModelsWasSetByUser)
       {
         std::stringstream ss;
         ss << "Cannot use " << sOptNoModel << " with model generation.";
@@ -1463,7 +1463,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     if (options::produceAssignments())
     {
-      if (opts.wasSetByUser(options::produceAssignments))
+      if (opts.smt.produceAssignmentsWasSetByUser)
       {
         std::stringstream ss;
         ss << "Cannot use " << sOptNoModel
@@ -1476,7 +1476,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     if (options::checkModels())
     {
-      if (opts.wasSetByUser(options::checkModels))
+      if (opts.smt.checkModelsWasSetByUser)
       {
         std::stringstream ss;
         ss << "Cannot use " << sOptNoModel
@@ -1503,14 +1503,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (logic == LogicInfo("QF_UFNRA"))
   {
 #ifdef CVC5_USE_POLY
-    if (!options::nlCad() && !opts.wasSetByUser(options::nlCad))
+    if (!options::nlCad() && !opts.arith.nlCadWasSetByUser)
     {
       opts.arith.nlCad = true;
-      if (!opts.wasSetByUser(options::nlExt))
+      if (!opts.arith.nlExtWasSetByUser)
       {
         opts.arith.nlExt = options::NlExtMode::LIGHT;
       }
-      if (!opts.wasSetByUser(options::nlRlvMode))
+      if (!opts.arith.nlRlvModeWasSetByUser)
       {
         opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE;
       }
@@ -1520,7 +1520,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 #ifndef CVC5_USE_POLY
   if (options::nlCad())
   {
-    if (opts.wasSetByUser(options::nlCad))
+    if (opts.arith.nlCadWasSetByUser)
     {
       std::stringstream ss;
       ss << "Cannot use " << options::arith::nlCad__name << " without configuring with --poly.";

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c84a290554bbd2f88bb49ee6a260fc7acdbb08b0..bd48fe0eacdcb76613fbb8d9b153ab69deb81cd7 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -444,7 +444,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
   {
     d_state->setFilename(value);
   }
-  else if (key == "smt-lib-version" && !Options::current().wasSetByUser(options::inputLanguage))
+  else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser)
   {
     language::input::Language ilang = language::input::LANG_SMTLIB_V2_6;
 
@@ -456,7 +456,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
     }
     getOptions().base.inputLanguage = ilang;
     // also update the output language
-    if (!Options::current().wasSetByUser(options::outputLanguage))
+    if (!getOptions().base.outputLanguageWasSetByUser)
     {
       language::output::Language olang = language::toOutputLanguage(ilang);
       if (d_env->getOptions().base.outputLanguage != olang)

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 6069745e0d48966ae1b0b73789b7f2fd822a8206..14bc05335adfb88d26395e2d540abc15214ee292 100644 (file)
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
                                   Node query)
 {
   Assert (!query.isNull());
-  if (Options::current().quantifiers.sygusExprMinerCheckTimeout__setByUser)
+  if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
   {
     initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
   }

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index d45a96d3bb741739437e8453841f57797d981703..0b5d06bd2a8c6045775f9d9eb7f52340ff019636 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -234,7 +234,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   std::unique_ptr<SmtEngine> repcChecker;
   // initialize the subsolver using the standard method
   initializeSubsolver(repcChecker,
-                      Options::current().wasSetByUser(options::sygusRepairConstTimeout),
+                      Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
                       options::sygusRepairConstTimeout());
   // renable options disabled by sygus
   repcChecker->setOption("miniscope-quant", "true");