Add -o options-auto (cvc5#10620)

Used for debugging which options are automatically configured by cvc5 before solving.

src/api/cpp/cvc5.cpp

@@ -8316,7 +8316,7 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const
   if (keyword == "filename")
   {
     // only the Solver object has non-const access to the original options
-    d_originalOptions->writeDriver().filename = value;
+    d_originalOptions->write_driver().filename = value;
   }
   d_slv->setInfo(keyword, value);
   ////////

src/options/base_options.toml

@@ -255,6 +255,11 @@ name   = "Base"
   help = "prints the formulas used when block-model is run."
   description = "With ``-o block-model``, cvc5 prints the formulas used when block-model is run."
   example-file = "regress0/printer/block_model_out.smt2"
+[[option.mode.OPTIONS_AUTO]]
+  name = "options-auto"
+  help = "prints the options set during automatic configuration."
+  description = "With ``-o options-auto``, cvc5 prints the options set during automatic configuration."
+  example-file = "regress0/printer/print_options_auto.smt2"
 
 # Stores then enabled output tags.
 [[option]]

src/options/mkoptions.py

@@ -233,7 +233,7 @@ 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('''  const options::Holder{id_cap}& {id};
-  options::Holder{id_cap}& write{id_capitalized}();''', modules)
+  options::Holder{id_cap}& write_{id}();''', modules)
 
 
 ################################################################################
@@ -259,7 +259,7 @@ def generate_holder_ref_inits(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 concat_format('''  options::Holder{id_cap}& Options::write_{id}()
   {{
     return *d_{id};
   }}
@@ -401,10 +401,10 @@ def generate_set_impl(modules):
         for pred in _set_predicates(module, option):
             res.append('    {}'.format(pred))
         if 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))
+            res.append('    opts.write_{module}().{name} = value;'.format(
+                module=module.id, name=option.name))
+            res.append('    opts.write_{module}().{name}WasSetByUser = true;'.format(
+                module=module.id, name=option.name))
         res.append('    break;')
         res.append('  }')
     res.append('}')

src/options/options_handler.cpp

@@ -152,7 +152,7 @@ void OptionsHandler::setInputLanguage(const std::string& flag, Language lang)
   }
   if (!d_options->printer.outputLanguageWasSetByUser)
   {
-    d_options->writePrinter().outputLanguage = lang;
+    d_options->write_printer().outputLanguage = lang;
     ioutils::setDefaultOutputLanguage(lang);
   }
 }
@@ -173,13 +173,13 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value)
 
 void OptionsHandler::decreaseVerbosity(const std::string& flag, bool value)
 {
-  d_options->writeBase().verbosity -= 1;
+  d_options->write_base().verbosity -= 1;
   setVerbosity(flag, d_options->base.verbosity);
 }
 
 void OptionsHandler::increaseVerbosity(const std::string& flag, bool value)
 {
-  d_options->writeBase().verbosity += 1;
+  d_options->write_base().verbosity += 1;
   setVerbosity(flag, d_options->base.verbosity);
 }
 
@@ -197,9 +197,9 @@ void OptionsHandler::setStats(const std::string& flag, bool value)
 #endif /* CVC5_STATISTICS_ON */
   if (!value)
   {
-    d_options->writeBase().statisticsAll = false;
-    d_options->writeBase().statisticsEveryQuery = false;
-    d_options->writeBase().statisticsInternal = false;
+    d_options->write_base().statisticsAll = false;
+    d_options->write_base().statisticsEveryQuery = false;
+    d_options->write_base().statisticsInternal = false;
   }
 }
 
@@ -217,7 +217,7 @@ void OptionsHandler::setStatsDetail(const std::string& flag, bool value)
 #endif /* CVC5_STATISTICS_ON */
   if (value)
   {
-    d_options->writeBase().statistics = true;
+    d_options->write_base().statistics = true;
   }
 }
 
@@ -233,7 +233,7 @@ void OptionsHandler::enableTraceTag(const std::string& flag,
   {
     if (optarg == "help")
     {
-      d_options->writeDriver().showTraceTags = true;
+      d_options->write_driver().showTraceTags = true;
       showTraceTags("", true);
       return;
     }
@@ -254,13 +254,13 @@ 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->writeBase().outputTagHolder.set(tagid);
+  d_options->write_base().outputTagHolder.set(tagid);
 }
 
 void OptionsHandler::setResourceWeight(const std::string& flag,
                                        const std::string& optarg)
 {
-  d_options->writeBase().resourceWeightHolder.emplace_back(optarg);
+  d_options->write_base().resourceWeightHolder.emplace_back(optarg);
 }
 
 void OptionsHandler::checkBvSatSolver(const std::string& flag,
@@ -312,7 +312,7 @@ void OptionsHandler::checkBvSatSolver(const std::string& flag,
     }
     if (!d_options->bv.bitvectorToBoolWasSetByUser)
     {
-      d_options->writeBv().bitvectorToBool = true;
+      d_options->write_bv().bitvectorToBool = true;
     }
   }
 }

src/smt/abduction_solver.cpp

@@ -70,11 +70,11 @@ bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
 
   Options subOptions;
   subOptions.copyValues(d_env.getOptions());
-  subOptions.writeQuantifiers().sygus = true;
+  subOptions.write_quantifiers().sygus = true;
   // by default, we don't want disjunctive terms (ITE, OR) in abducts
   if (!d_env.getOptions().quantifiers.sygusGrammarUseDisjWasSetByUser)
   {
-    subOptions.writeQuantifiers().sygusGrammarUseDisj = false;
+    subOptions.write_quantifiers().sygusGrammarUseDisj = false;
   }
   SetDefaults::disableChecking(subOptions);
   SubsolverSetupInfo ssi(d_env, subOptions);
@@ -180,7 +180,7 @@ void AbductionSolver::checkAbduct(Node a)
 
   Options subOptions;
   subOptions.copyValues(d_env.getOptions());
-  subOptions.writeSmt().produceAbducts = false;
+  subOptions.write_smt().produceAbducts = false;
   SetDefaults::disableChecking(subOptions);
   SubsolverSetupInfo ssi(d_env, subOptions);
   // two checks: first, consistent with assertions, second, implies negated goal

src/smt/interpolation_solver.cpp

@@ -93,7 +93,7 @@ void InterpolationSolver::checkInterpol(Node interpol,
 
   Options subOptions;
   subOptions.copyValues(d_env.getOptions());
-  subOptions.writeSmt().produceInterpolants = false;
+  subOptions.write_smt().produceInterpolants = false;
   SetDefaults::disableChecking(subOptions);
   SubsolverSetupInfo ssi(d_env, subOptions);
   // two checks: first, axioms imply interpol, second, interpol implies conj.