Remove public option wrappers (#6716)

This PR gets rid of almost all remaining public option wrappers. It does so by
- making base, main and parser options public such that they can directly be used from the driver and the parser
- moving incremental and the resource limiting options to base
- moving dumping options to main

After this PR, the only option wrapper left is becoming obsolete as well after (the follow-up of) #6697.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 668fc938254a84f5bb4bd38f985a7403ae208600..30722298854ca431352c3b13583c7e411c783841 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -55,6 +55,7 @@
 #include "expr/sequence.h"
 #include "expr/type_node.h"
 #include "expr/uninterpreted_constant.h"
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/option_exception.h"
 #include "options/options.h"
@@ -6452,7 +6453,7 @@ Result Solver::checkEntailed(const Term& term) const
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
-                 || d_smtEngine->getOptions().smt.incrementalSolving)
+                 || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERM(term);
@@ -6468,7 +6469,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
-                 || d_smtEngine->getOptions().smt.incrementalSolving)
+                 || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERMS(terms);
@@ -6497,7 +6498,7 @@ Result Solver::checkSat(void) const
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
-                 || d_smtEngine->getOptions().smt.incrementalSolving)
+                 || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   //////// all checks before this line
@@ -6512,7 +6513,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
-                 || d_smtEngine->getOptions().smt.incrementalSolving)
+                 || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort());
@@ -6528,7 +6529,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
-                 || d_smtEngine->getOptions().smt.incrementalSolving)
+                 || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort());
@@ -6863,7 +6864,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
-  CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving)
+  CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot get unsat assumptions unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions)
@@ -7044,7 +7045,7 @@ void Solver::pop(uint32_t nscopes) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving)
+  CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot pop when not solving incrementally (use --incremental)";
   CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels())
       << "Cannot pop beyond first pushed context";
@@ -7176,7 +7177,7 @@ void Solver::push(uint32_t nscopes) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving)
+  CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot push when not solving incrementally (use --incremental)";
   //////// all checks before this line
   for (uint32_t n = 0; n < nscopes; ++n)

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 6bdc1abc9942ca22c08deec4b847d045bde89696..b6ead1b708f103d4ac306233b45aac2c49945f26 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -26,7 +26,8 @@
 #include <vector>
 
 #include "main/main.h"
-#include "options/options_public.h"
+#include "options/base_options.h"
+#include "options/main_options.h"
 #include "smt/command.h"
 #include "smt/smt_engine.h"
 
@@ -65,7 +66,7 @@ CommandExecutor::~CommandExecutor()
 
 void CommandExecutor::printStatistics(std::ostream& out) const
 {
-  if (options::getStatistics(d_options))
+  if (d_options.base.statistics)
   {
     getSmtEngine()->printStatistics(out);
   }
@@ -73,7 +74,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const
 
 void CommandExecutor::printStatisticsSafe(int fd) const
 {
-  if (options::getStatistics(d_options))
+  if (d_options.base.statistics)
   {
     getSmtEngine()->printStatisticsSafe(fd);
   }
@@ -81,7 +82,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const
 
 bool CommandExecutor::doCommand(Command* cmd)
 {
-  if (options::getParseOnly(d_options))
+  if (d_options.base.parseOnly)
   {
     return true;
   }
@@ -100,9 +101,9 @@ bool CommandExecutor::doCommand(Command* cmd)
 
     return status;
   } else {
-    if (options::getVerbosity(d_options) > 2)
+    if (d_options.base.verbosity > 2)
     {
-      *options::getOut(d_options) << "Invoking: " << *cmd << std::endl;
+      *d_options.base.out << "Invoking: " << *cmd << std::endl;
     }
 
     return doCommandSingleton(cmd);
@@ -111,7 +112,7 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  printStatistics(*options::getErr(d_options));
+  printStatistics(*d_options.base.err);
   /* We have to keep options passed via CL on reset. These options are stored
    * in CommandExecutor::d_options (populated and created in the driver), and
    * CommandExecutor::d_options only contains *these* options since the
@@ -124,10 +125,10 @@ void CommandExecutor::reset()
 bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
-  if (options::getVerbosity(d_options) >= -1)
+  if (d_options.base.verbosity >= -1)
   {
     status = solverInvoke(
-        d_solver.get(), d_symman.get(), cmd, options::getOut(d_options));
+        d_solver.get(), d_symman.get(), cmd, d_options.base.out);
   }
   else
   {
@@ -150,9 +151,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_result = res = q->getResult();
   }
 
-  if ((cs != nullptr || q != nullptr) && options::getStatsEveryQuery(d_options))
+  if ((cs != nullptr || q != nullptr) && d_options.base.statisticsEveryQuery)
   {
-    getSmtEngine()->printStatisticsDiff(*options::getErr(d_options));
+    getSmtEngine()->printStatisticsDiff(*d_options.base.err);
   }
 
   bool isResultUnsat = res.isUnsat() || res.isEntailed();
@@ -160,32 +161,32 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   // dump the model/proof/unsat core if option is set
   if (status) {
     std::vector<std::unique_ptr<Command> > getterCommands;
-    if (options::getDumpModels(d_options)
+    if (d_options.driver.dumpModels
         && (res.isSat()
             || (res.isSatUnknown()
                 && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (options::getDumpProofs(d_options) && isResultUnsat)
+    if (d_options.driver.dumpProofs && isResultUnsat)
     {
       getterCommands.emplace_back(new GetProofCommand());
     }
 
-    if (options::getDumpInstantiations(d_options)
+    if (d_options.driver.dumpInstantiations
         && GetInstantiationsCommand::isEnabled(d_solver.get(), res))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if (options::getDumpUnsatCores(d_options) && isResultUnsat)
+    if ((d_options.driver.dumpUnsatCores || d_options.driver.dumpUnsatCoresFull) && isResultUnsat)
     {
       getterCommands.emplace_back(new GetUnsatCoreCommand());
     }
 
     if (!getterCommands.empty()) {
       // set no time limit during dumping if applicable
-      if (options::getForceNoLimitCpuWhileDump(d_options))
+      if (d_options.driver.forceNoLimitCpuWhileDump)
       {
         setNoLimitCPU();
       }
@@ -225,17 +226,17 @@ bool solverInvoke(api::Solver* solver,
 }
 
 void CommandExecutor::flushOutputStreams() {
-  printStatistics(*(options::getErr(d_options)));
+  printStatistics(*d_options.base.err);
 
   // make sure out and err streams are flushed too
 
-  if (options::getOut(d_options) != nullptr)
+  if (d_options.base.out != nullptr)
   {
-    *options::getOut(d_options) << std::flush;
+    *d_options.base.out << std::flush;
   }
-  if (options::getErr(d_options) != nullptr)
+  if (d_options.base.err != nullptr)
   {
-    *options::getErr(d_options) << std::flush;
+    *d_options.base.err << std::flush;
   }
 }
 

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 697501d13361dda776ea563848aa0a0ae4cb0988..ed1825711763e20993986086ecbaa421d54e21a6 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -33,8 +33,9 @@
 #include "main/main.h"
 #include "main/signal_handlers.h"
 #include "main/time_limit.h"
+#include "options/base_options.h"
 #include "options/options.h"
-#include "options/options_public.h"
+#include "options/parser_options.h"
 #include "options/main_options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
@@ -88,9 +89,9 @@ void printUsage(Options& opts, bool full) {
      << endl
      << "cvc5 options:" << endl;
   if(full) {
-    Options::printUsage(ss.str(), *(options::getOut(opts)));
+    Options::printUsage(ss.str(), *opts.base.out);
   } else {
-    Options::printShortUsage(ss.str(), *(options::getOut(opts)));
+    Options::printShortUsage(ss.str(), *opts.base.out);
   }
 }
 
@@ -116,14 +117,14 @@ int runCvc5(int argc, char* argv[], Options& opts)
     printUsage(opts, true);
     exit(1);
   }
-  else if (options::getLanguageHelp(opts))
+  else if (opts.base.languageHelp)
   {
-    Options::printLanguageHelp(*(options::getOut(opts)));
+    Options::printLanguageHelp(*opts.base.out);
     exit(1);
   }
   else if (opts.driver.version)
   {
-    *(options::getOut(opts)) << Configuration::about().c_str() << flush;
+    *opts.base.out << Configuration::about().c_str() << flush;
     exit(0);
   }
 
@@ -131,7 +132,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC5_COMPETITION_MODE
-  *(options::getOut(opts)) << unitbuf;
+  *opts.base.out << unitbuf;
 #endif /* CVC5_COMPETITION_MODE */
 
   // We only accept one input file
@@ -143,7 +144,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 
   // if we're reading from stdin on a TTY, default to interactive mode
-  if (!options::wasSetByUserInteractive(opts))
+  if (!opts.driver.interactiveWasSetByUser)
   {
     opts.driver.interactive = inputFromStdin && isatty(fileno(stdin));
   }
@@ -157,33 +158,32 @@ int runCvc5(int argc, char* argv[], Options& opts)
   }
   const char* filename = filenameStr.c_str();
 
-  if (options::getInputLanguage(opts) == language::input::LANG_AUTO)
+  if (opts.base.inputLanguage == language::input::LANG_AUTO)
   {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      options::setInputLanguage(language::input::LANG_CVC, opts);
+      opts.base.inputLanguage = language::input::LANG_CVC;
     } else {
       size_t len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        options::setInputLanguage(language::input::LANG_SMTLIB_V2_6, opts);
+        opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6;
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        options::setInputLanguage(language::input::LANG_TPTP, opts);
+        opts.base.inputLanguage = language::input::LANG_TPTP;
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        options::setInputLanguage(language::input::LANG_CVC, opts);
+        opts.base.inputLanguage = language::input::LANG_CVC;
       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
         // version 2 sygus is the default
-        options::setInputLanguage(language::input::LANG_SYGUS_V2, opts);
+        opts.base.inputLanguage = language::input::LANG_SYGUS_V2;
       }
     }
   }
 
-  if (options::getOutputLanguage(opts) == language::output::LANG_AUTO)
+  if (opts.base.outputLanguage == language::output::LANG_AUTO)
   {
-    options::setOutputLanguage(
-        language::toOutputLanguage(options::getInputLanguage(opts)), opts);
+    opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage);
   }
 
   // Determine which messages to show based on smtcomp_mode and verbosity
@@ -197,8 +197,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
   }
 
   // important even for muzzled builds (to get result output right)
-  (*(options::getOut(opts)))
-      << language::SetLanguage(options::getOutputLanguage(opts));
+  (*opts.base.out)
+      << language::SetLanguage(opts.base.outputLanguage);
 
   // Create the command executor to execute the parsed commands
   pExecutor = std::make_unique<CommandExecutor>(opts);
@@ -218,7 +218,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
         throw Exception(
             "--tear-down-incremental doesn't work in interactive mode");
       }
-      if (!options::wasSetByUserIncrementalSolving(opts))
+      if (!opts.base.incrementalSolvingWasSetByUser)
       {
         cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
@@ -245,7 +245,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
         try {
           cmd.reset(shell.readCommand());
         } catch(UnsafeInterruptException& e) {
-          (*options::getOut(opts)) << CommandInterrupted();
+          *opts.base.out << CommandInterrupted();
           break;
         }
         if (cmd == nullptr)
@@ -258,7 +258,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
     }
     else if (opts.driver.tearDownIncremental > 0)
     {
-      if (!options::getIncrementalSolving(opts)
+      if (!opts.base.incrementalSolving
           && opts.driver.tearDownIncremental > 1)
       {
         // For tear-down-incremental values greater than 1, need incremental
@@ -266,7 +266,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
         cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
-        // if(options::wasSetByUserIncrementalSolving(opts)) {
+        // if(opts.base.incrementalWasSetByUser) {
         //   throw OptionException(
         //     "--tear-down-incremental incompatible with --incremental");
         // }
@@ -282,13 +282,13 @@ int runCvc5(int argc, char* argv[], Options& opts)
       std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
         parser->setInput(Input::newStreamInput(
-            options::getInputLanguage(opts), cin, filename));
+            opts.base.inputLanguage, cin, filename));
       }
       else
       {
-        parser->setInput(Input::newFileInput(options::getInputLanguage(opts),
+        parser->setInput(Input::newFileInput(opts.base.inputLanguage,
                                              filename,
-                                             options::getMemoryMap(opts)));
+                                             opts.parser.memoryMap));
       }
 
       vector< vector<Command*> > allCommands;
@@ -299,7 +299,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
       while (status)
       {
         if (interrupted) {
-          (*options::getOut(opts)) << CommandInterrupted();
+          *opts.base.out << CommandInterrupted();
           break;
         }
 
@@ -357,7 +357,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
               }
             }
             if (interrupted) continue;
-            (*options::getOut(opts)) << CommandSuccess();
+            *opts.base.out << CommandSuccess();
             needReset = 0;
           }
           else
@@ -436,7 +436,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
     }
     else
     {
-      if (!options::wasSetByUserIncrementalSolving(opts))
+      if (!opts.base.incrementalSolvingWasSetByUser)
       {
         cmd.reset(new SetOptionCommand("incremental", "false"));
         cmd->setMuted(true);
@@ -449,20 +449,20 @@ int runCvc5(int argc, char* argv[], Options& opts)
       std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
         parser->setInput(Input::newStreamInput(
-            options::getInputLanguage(opts), cin, filename));
+            opts.base.inputLanguage, cin, filename));
       }
       else
       {
-        parser->setInput(Input::newFileInput(options::getInputLanguage(opts),
+        parser->setInput(Input::newFileInput(opts.base.inputLanguage,
                                              filename,
-                                             options::getMemoryMap(opts)));
+                                             opts.parser.memoryMap));
       }
 
       bool interrupted = false;
       while (status)
       {
         if (interrupted) {
-          (*options::getOut(opts)) << CommandInterrupted();
+          *opts.base.out << CommandInterrupted();
           pExecutor->reset();
           break;
         }
@@ -496,9 +496,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
     }
 
 #ifdef CVC5_COMPETITION_MODE
-    if (cvc5::options::getOut(opts) != nullptr)
+    if (opts.base.out != nullptr)
     {
-      *cvc5::options::getOut(opts) << std::flush;
+      *opts.base.out << std::flush;
     }
     // exit, don't return (don't want destructors to run)
     // _exit() from unistd.h doesn't run global destructors
@@ -510,7 +510,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
     pExecutor->flushOutputStreams();
 
 #ifdef CVC5_DEBUG
-    if (opts.driver.earlyExit && options::wasSetByUserEarlyExit(opts))
+    if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser)
     {
       _exit(returnValue);
     }

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 048c101f08e5ffd78e4821f9c2cc694f3e5ec398..964b88ea0fcd366e0ad05c65ec09bd120e3587d8 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -40,10 +40,11 @@
 #include "base/check.h"
 #include "base/output.h"
 #include "expr/symbol_manager.h"
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
 #include "options/options.h"
-#include "options/options_public.h"
+#include "options/parser_options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -89,16 +90,16 @@ static set<string> s_declarations;
 
 InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
     : d_options(solver->getOptions()),
-      d_in(*options::getIn(d_options)),
-      d_out(*options::getOut(d_options)),
+      d_in(*d_options.base.in),
+      d_out(*d_options.base.out),
       d_quit(false)
 {
   ParserBuilder parserBuilder(solver, sm, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.build();
-  if (options::wasSetByUserForceLogicString(d_options))
+  if (d_options.parser.forceLogicStringWasSetByUser)
   {
-    LogicInfo tmp(options::getForceLogicString(d_options));
+    LogicInfo tmp(d_options.parser.forceLogicString);
     d_parser->forceLogic(tmp.getLogicString());
   }
 
@@ -113,7 +114,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
     ::using_history();
 
     OutputLanguage lang =
-        toOutputLanguage(options::getInputLanguage(d_options));
+        toOutputLanguage(d_options.base.inputLanguage);
     switch(lang) {
       case output::LANG_CVC:
         d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
@@ -314,7 +315,7 @@ restart:
   }
 
   d_parser->setInput(Input::newStringInput(
-      options::getInputLanguage(d_options), input, INPUT_FILENAME));
+      d_options.base.inputLanguage, input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */
@@ -365,7 +366,7 @@ restart:
   }
   catch (ParserException& pe)
   {
-    if (language::isOutputLang_smt2(options::getOutputLanguage(d_options)))
+    if (language::isOutputLang_smt2(d_options.base.outputLanguage))
     {
       d_out << "(error \"" << pe << "\")" << endl;
     }

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 2b25e6c9339f23c20a5ec7a36149668b0b659ee7..a00e29b04643f20638bdfb8b545fb31cdd094af8 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -26,10 +26,10 @@
 #include "base/output.h"
 #include "main/command_executor.h"
 #include "main/interactive_shell.h"
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/options.h"
-#include "options/options_public.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
@@ -53,25 +53,25 @@ int main(int argc, char* argv[]) {
     return runCvc5(argc, argv, opts);
   } catch(OptionException& e) {
 #ifdef CVC5_COMPETITION_MODE
-    *options::getOut(opts) << "unknown" << endl;
+    *opts.base.out << "unknown" << endl;
 #endif
     cerr << "(error \"" << e << "\")" << endl
          << endl
          << "Please use --help to get help on command-line options." << endl;
   } catch(Exception& e) {
 #ifdef CVC5_COMPETITION_MODE
-    *options::getOut(opts) << "unknown" << endl;
+    *opts.base.out << "unknown" << endl;
 #endif
-    if (language::isOutputLang_smt2(options::getOutputLanguage(opts)))
+    if (language::isOutputLang_smt2(opts.base.outputLanguage))
     {
-      *options::getOut(opts) << "(error \"" << e << "\")" << endl;
+      *opts.base.out << "(error \"" << e << "\")" << endl;
     } else {
-      *options::getErr(opts) << "(error \"" << e << "\")" << endl;
+      *opts.base.err << "(error \"" << e << "\")" << endl;
     }
-    if (options::getStatistics(opts) && pExecutor != nullptr)
+    if (opts.base.statistics && pExecutor != nullptr)
     {
       totalTime.reset();
-      pExecutor->printStatistics(*options::getErr(opts));
+      pExecutor->printStatistics(*opts.base.err);
     }
   }
   exit(1);

diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index c0fc6846aa82431ef1447fd24c3b3f7b4711f68c..28a0087bb996f4ff078b2d30b34ef5577e527aeb 100644 (file)
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -56,7 +56,7 @@
 #include <cstring>
 
 #include "base/exception.h"
-#include "options/options_public.h"
+#include "options/base_options.h"
 #include "signal_handlers.h"
 
 namespace cvc5 {
@@ -80,7 +80,7 @@ TimeLimit::~TimeLimit()
 
 TimeLimit install_time_limit(const Options& opts)
 {
-  unsigned long ms = options::getCumulativeTimeLimit(opts);
+  uint64_t ms = opts.base.cumulativeMillisecondLimit;
   // Skip if no time limit shall be set.
   if (ms == 0) {
     return TimeLimit();

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 978c328887291005bdf18944d3009876f382b10a..26ced1a24bcb0b7af5a000331d675760aeec7299 100644 (file)
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -55,7 +55,6 @@ set(options_toml_files
   proof_options.toml
   prop_options.toml
   quantifiers_options.toml
-  resource_manager_options.toml
   sep_options.toml
   sets_options.toml
   smt_options.toml

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index f9d1c1a187e4c36a35ba2e80f74cd33bc086daa3..64d373509acb7eb88518dcae4347a31beb3a14b4 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -1,5 +1,6 @@
 id     = "BASE"
 name   = "Base"
+public = true
 
 [[option]]
   name       = "in"
@@ -75,6 +76,15 @@ name   = "Base"
   handler    = "decreaseVerbosity"
   help       = "decrease verbosity (may be repeated)"
 
+[[option]]
+  name       = "incrementalSolving"
+  category   = "common"
+  short      = "i"
+  long       = "incremental"
+  type       = "bool"
+  default    = "true"
+  help       = "enable incremental solving"
+
 [[option]]
   name       = "statistics"
   long       = "stats"
@@ -144,3 +154,52 @@ name   = "Base"
   long       = "print-success"
   type       = "bool"
   help       = "print the \"success\" output required of SMT-LIBv2"
+
+[[option]]
+  name       = "cumulativeMillisecondLimit"
+  category   = "common"
+  long       = "tlimit=MS"
+  type       = "uint64_t"
+  help       = "set time limit in milliseconds of wall clock time"
+
+[[option]]
+  name       = "perCallMillisecondLimit"
+  category   = "common"
+  long       = "tlimit-per=MS"
+  type       = "uint64_t"
+  help       = "set time limit per query in milliseconds"
+
+[[option]]
+  name       = "cumulativeResourceLimit"
+  category   = "common"
+  long       = "rlimit=N"
+  type       = "uint64_t"
+  help       = "set resource limit"
+
+[[option]]
+  name       = "perCallResourceLimit"
+  alias      = ["reproducible-resource-limit"]
+  category   = "common"
+  long       = "rlimit-per=N"
+  type       = "uint64_t"
+  help       = "set resource limit per query"
+
+# --rweight is used to override the default of one particular resource weight.
+# It can be given multiple times to override multiple weights. When options are
+# parsed, the resource manager might now be created yet, and it is not clear
+# how an option handler would access it in a reasonable way. The option handler
+# thus merely puts the data in another option that holds a vector of strings.
+# This other option "resourceWeightHolder" has the sole purpose of storing
+# this data in a way so that the resource manager can access it in its
+# constructor.
+[[option]]
+  category   = "expert"
+  long       = "rweight=VAL=N"
+  type       = "std::string"
+  handler    = "setResourceWeight"
+  help       = "set a single resource weight"
+
+[[option]]
+  name       = "resourceWeightHolder"
+  category   = "undocumented"
+  type       = "std::vector<std::string>"

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 0f5dfdcd71ce85f31ca043e3b658c8cd673d7710..fdaebbd6dde4805cb0534467639c3402fd4dce44 100644 (file)
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -95,3 +95,51 @@ public = true
   type       = "int"
   default    = "0"
   help       = "implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries"
+
+[[option]]
+  name       = "dumpModels"
+  category   = "regular"
+  long       = "dump-models"
+  type       = "bool"
+  default    = "false"
+  help       = "output models after every SAT/INVALID/UNKNOWN response"
+
+[[option]]
+  name       = "dumpProofs"
+  category   = "regular"
+  long       = "dump-proofs"
+  type       = "bool"
+  default    = "false"
+  help       = "output proofs after every UNSAT/VALID response"
+
+[[option]]
+  name       = "dumpInstantiations"
+  category   = "regular"
+  long       = "dump-instantiations"
+  type       = "bool"
+  default    = "false"
+  help       = "output instantiations of quantified formulas after every UNSAT/VALID response"
+
+[[option]]
+  name       = "dumpUnsatCores"
+  category   = "regular"
+  long       = "dump-unsat-cores"
+  type       = "bool"
+  default    = "false"
+  help       = "output unsat cores after every UNSAT/VALID response"
+
+[[option]]
+  name       = "dumpUnsatCoresFull"
+  category   = "regular"
+  long       = "dump-unsat-cores-full"
+  type       = "bool"
+  default    = "false"
+  help       = "dump the full unsat core, including unlabeled assertions"
+
+[[option]]
+  name       = "forceNoLimitCpuWhileDump"
+  category   = "regular"
+  long       = "force-no-limit-cpu-while-dump"
+  type       = "bool"
+  default    = "false"
+  help       = "Force no CPU limit when dumping models and proofs"

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index c1c843802bb6818ab28b1238f5fb0e06e1d59f75..1ac5ec56db93f10d1a61a6db31a6f9a2f69f13e8 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -33,7 +33,6 @@
 #include "options/didyoumean.h"
 #include "options/language.h"
 #include "options/option_exception.h"
-#include "options/resource_manager_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 
@@ -83,7 +82,7 @@ unsigned long OptionsHandler::limitHandler(std::string option,
 
 void OptionsHandler::setResourceWeight(std::string option, std::string optarg)
 {
-  d_options->resman.resourceWeightHolder.emplace_back(optarg);
+  d_options->base.resourceWeightHolder.emplace_back(optarg);
 }
 
 // theory/quantifiers/options_handlers.h

diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
index 35e891f5ab5eafb4acc6f46174ed3830e65dd9b4..5520583123c65da47012920603b5ec7f66b6dcb2 100644 (file)
--- a/src/options/options_public.cpp
+++ b/src/options/options_public.cpp
@@ -17,118 +17,10 @@
 
 #include "options_public.h"
 
-#include <fstream>
-#include <ostream>
-#include <string>
-#include <vector>
-
-#include "base/listener.h"
-#include "base/modal_exception.h"
-#include "options/base_options.h"
-#include "options/language.h"
-#include "options/main_options.h"
-#include "options/option_exception.h"
-#include "options/options.h"
-#include "options/parser_options.h"
-#include "options/printer_modes.h"
-#include "options/printer_options.h"
-#include "options/resource_manager_options.h"
-#include "options/smt_options.h"
 #include "options/uf_options.h"
 
 namespace cvc5::options {
 
-InputLanguage getInputLanguage(const Options& opts)
-{
-  return opts.base.inputLanguage;
-}
-InstFormatMode getInstFormatMode(const Options& opts)
-{
-  return opts.printer.instFormatMode;
-}
-OutputLanguage getOutputLanguage(const Options& opts)
-{
-  return opts.base.outputLanguage;
-}
 bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
-bool getDumpInstantiations(const Options& opts)
-{
-  return opts.smt.dumpInstantiations;
-}
-bool getDumpModels(const Options& opts) { return opts.smt.dumpModels; }
-bool getDumpProofs(const Options& opts) { return opts.smt.dumpProofs; }
-bool getDumpUnsatCores(const Options& opts)
-{
-  return opts.smt.dumpUnsatCores || opts.smt.dumpUnsatCoresFull;
-}
-bool getFilesystemAccess(const Options& opts)
-{
-  return opts.parser.filesystemAccess;
-}
-bool getForceNoLimitCpuWhileDump(const Options& opts)
-{
-  return opts.smt.forceNoLimitCpuWhileDump;
-}
-bool getIncrementalSolving(const Options& opts)
-{
-  return opts.smt.incrementalSolving;
-}
-bool getLanguageHelp(const Options& opts) { return opts.base.languageHelp; }
-bool getMemoryMap(const Options& opts) { return opts.parser.memoryMap; }
-bool getParseOnly(const Options& opts) { return opts.base.parseOnly; }
-bool getProduceModels(const Options& opts) { return opts.smt.produceModels; }
-bool getSemanticChecks(const Options& opts)
-{
-  return opts.parser.semanticChecks;
-}
-bool getStatistics(const Options& opts) { return opts.base.statistics; }
-bool getStatsEveryQuery(const Options& opts)
-{
-  return opts.base.statisticsEveryQuery;
-}
-bool getStrictParsing(const Options& opts)
-{
-  return opts.parser.strictParsing;
-}
-uint64_t getCumulativeTimeLimit(const Options& opts)
-{
-  return opts.resman.cumulativeMillisecondLimit;
-}
-const std::string& getForceLogicString(const Options& opts)
-{
-  return opts.parser.forceLogicString;
-}
-int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; }
-
-std::istream* getIn(const Options& opts) { return opts.base.in; }
-std::ostream* getErr(const Options& opts) { return opts.base.err; }
-std::ostream* getOut(const Options& opts) { return opts.base.out; }
-
-void setInputLanguage(InputLanguage val, Options& opts)
-{
-  opts.base.inputLanguage = val;
-}
-void setOut(std::ostream* val, Options& opts) { opts.base.out = val; }
-void setOutputLanguage(OutputLanguage val, Options& opts)
-{
-  opts.base.outputLanguage = val;
-}
-
-bool wasSetByUserEarlyExit(const Options& opts)
-{
-  return opts.driver.earlyExitWasSetByUser;
-}
-bool wasSetByUserForceLogicString(const Options& opts)
-{
-  return opts.parser.forceLogicStringWasSetByUser;
-}
-bool wasSetByUserIncrementalSolving(const Options& opts)
-{
-  return opts.smt.incrementalSolvingWasSetByUser;
-}
-bool wasSetByUserInteractive(const Options& opts)
-{
-  return opts.driver.interactiveWasSetByUser;
-}
 
 }  // namespace cvc5::options

diff --git a/src/options/options_public.h b/src/options/options_public.h
index 1d2f9edba8ee1a04d880c99b28a84c2d3d6c7e06..60929c96c3b2ee9204b41d2d27f23e8dbcb344d0 100644 (file)
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -23,47 +23,11 @@
 #ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H
 #define CVC5__OPTIONS__OPTIONS_PUBLIC_H
 
-#include "options/language.h"
 #include "options/options.h"
-#include "options/printer_modes.h"
 
 namespace cvc5::options {
 
-InputLanguage getInputLanguage(const Options& opts) CVC5_EXPORT;
-InstFormatMode getInstFormatMode(const Options& opts) CVC5_EXPORT;
-OutputLanguage getOutputLanguage(const Options& opts) CVC5_EXPORT;
 bool getUfHo(const Options& opts) CVC5_EXPORT;
-bool getDumpInstantiations(const Options& opts) CVC5_EXPORT;
-bool getDumpModels(const Options& opts) CVC5_EXPORT;
-bool getDumpProofs(const Options& opts) CVC5_EXPORT;
-bool getDumpUnsatCores(const Options& opts) CVC5_EXPORT;
-bool getFilesystemAccess(const Options& opts) CVC5_EXPORT;
-bool getForceNoLimitCpuWhileDump(const Options& opts) CVC5_EXPORT;
-bool getIncrementalSolving(const Options& opts) CVC5_EXPORT;
-bool getLanguageHelp(const Options& opts) CVC5_EXPORT;
-bool getMemoryMap(const Options& opts) CVC5_EXPORT;
-bool getParseOnly(const Options& opts) CVC5_EXPORT;
-bool getProduceModels(const Options& opts) CVC5_EXPORT;
-bool getSemanticChecks(const Options& opts) CVC5_EXPORT;
-bool getStatistics(const Options& opts) CVC5_EXPORT;
-bool getStatsEveryQuery(const Options& opts) CVC5_EXPORT;
-bool getStrictParsing(const Options& opts) CVC5_EXPORT;
-uint64_t getCumulativeTimeLimit(const Options& opts) CVC5_EXPORT;
-const std::string& getForceLogicString(const Options& opts) CVC5_EXPORT;
-int32_t getVerbosity(const Options& opts) CVC5_EXPORT;
-
-std::istream* getIn(const Options& opts) CVC5_EXPORT;
-std::ostream* getErr(const Options& opts) CVC5_EXPORT;
-std::ostream* getOut(const Options& opts) CVC5_EXPORT;
-
-void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT;
-void setOut(std::ostream* val, Options& opts) CVC5_EXPORT;
-void setOutputLanguage(OutputLanguage val, Options& opts) CVC5_EXPORT;
-
-bool wasSetByUserEarlyExit(const Options& opts) CVC5_EXPORT;
-bool wasSetByUserForceLogicString(const Options& opts) CVC5_EXPORT;
-bool wasSetByUserIncrementalSolving(const Options& opts) CVC5_EXPORT;
-bool wasSetByUserInteractive(const Options& opts) CVC5_EXPORT;
 
 }  // namespace cvc5::options
 

diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml
index 6fc683368a42a8a78fc19986ef8dcf0dd007793e..f19b903a626b65e93abeaa8840e16ef924d8312b 100644 (file)
--- a/src/options/parser_options.toml
+++ b/src/options/parser_options.toml
@@ -1,5 +1,6 @@
 id     = "PARSER"
 name   = "Parser"
+public = true
 
 [[option]]
   name       = "strictParsing"

diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml
deleted file mode 100644 (file)
index 6d5c4d4..0000000
--- a/src/options/resource_manager_options.toml
+++ /dev/null
@@ -1,51 +0,0 @@
-id     = "RESMAN"
-name   = "Resource Manager"
-
-[[option]]
-  name       = "cumulativeMillisecondLimit"
-  category   = "common"
-  long       = "tlimit=MS"
-  type       = "uint64_t"
-  help       = "set time limit in milliseconds of wall clock time"
-
-[[option]]
-  name       = "perCallMillisecondLimit"
-  category   = "common"
-  long       = "tlimit-per=MS"
-  type       = "uint64_t"
-  help       = "set time limit per query in milliseconds"
-
-[[option]]
-  name       = "cumulativeResourceLimit"
-  category   = "common"
-  long       = "rlimit=N"
-  type       = "uint64_t"
-  help       = "set resource limit"
-
-[[option]]
-  name       = "perCallResourceLimit"
-  alias      = ["reproducible-resource-limit"]
-  category   = "common"
-  long       = "rlimit-per=N"
-  type       = "uint64_t"
-  help       = "set resource limit per query"
-
-# --rweight is used to override the default of one particular resource weight.
-# It can be given multiple times to override multiple weights. When options are
-# parsed, the resource manager might now be created yet, and it is not clear
-# how an option handler would access it in a reasonable way. The option handler
-# thus merely puts the data in another option that holds a vector of strings.
-# This other option "resourceWeightHolder" has the sole purpose of storing
-# this data in a way so that the resource manager can access it in its
-# constructor.
-[[option]]
-  category   = "expert"
-  long       = "rweight=VAL=N"
-  type       = "std::string"
-  handler    = "setResourceWeight"
-  help       = "set a single resource weight"
-
-[[option]]
-  name       = "resourceWeightHolder"
-  category   = "undocumented"
-  type       = "std::vector<std::string>"

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index d1354f7777a6094167d786314c24708bfbe329e4..4d08aa67204822587ccfc08d81a7ec3855b469cf 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -78,14 +78,6 @@ name   = "SMT Layer"
   type       = "bool"
   help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions"
 
-[[option]]
-  name       = "dumpModels"
-  category   = "regular"
-  long       = "dump-models"
-  type       = "bool"
-  default    = "false"
-  help       = "output models after every SAT/INVALID/UNKNOWN response"
-
 [[option]]
   name       = "modelCoresMode"
   category   = "regular"
@@ -130,14 +122,6 @@ name   = "SMT Layer"
   default    = "false"
   help       = "produce proofs, support check-proofs and get-proof"
 
-[[option]]
-  name       = "dumpProofs"
-  category   = "regular"
-  long       = "dump-proofs"
-  type       = "bool"
-  default    = "false"
-  help       = "output proofs after every UNSAT/VALID response"
-
 [[option]]
   name       = "checkProofs"
   category   = "regular"
@@ -145,14 +129,6 @@ name   = "SMT Layer"
   type       = "bool"
   help       = "after UNSAT/VALID, check the generated proof (with proof)"
 
-[[option]]
-  name       = "dumpInstantiations"
-  category   = "regular"
-  long       = "dump-instantiations"
-  type       = "bool"
-  default    = "false"
-  help       = "output instantiations of quantified formulas after every UNSAT/VALID response"
-
 [[option]]
   name       = "sygusOut"
   category   = "regular"
@@ -217,22 +193,6 @@ name   = "SMT Layer"
   type       = "bool"
   help       = "after UNSAT/VALID, produce and check an unsat core (expensive)"
 
-[[option]]
-  name       = "dumpUnsatCores"
-  category   = "regular"
-  long       = "dump-unsat-cores"
-  type       = "bool"
-  default    = "false"
-  help       = "output unsat cores after every UNSAT/VALID response"
-
-[[option]]
-  name       = "dumpUnsatCoresFull"
-  category   = "regular"
-  long       = "dump-unsat-cores-full"
-  type       = "bool"
-  default    = "false"
-  help       = "dump the full unsat core, including unlabeled assertions"
-
 [[option]]
   name       = "unsatAssumptions"
   category   = "regular"
@@ -359,15 +319,6 @@ name   = "SMT Layer"
   default    = "false"
   help       = "calculate sort inference of input problem, convert the input based on monotonic sorts"
 
-[[option]]
-  name       = "incrementalSolving"
-  category   = "common"
-  short      = "i"
-  long       = "incremental"
-  type       = "bool"
-  default    = "true"
-  help       = "enable incremental solving"
-
 [[option]]
   name       = "abstractValues"
   category   = "regular"
@@ -421,14 +372,6 @@ name   = "SMT Layer"
   type       = "std::string"
   help       = "set the diagnostic output channel of the solver"
 
-[[option]]
-  name       = "forceNoLimitCpuWhileDump"
-  category   = "regular"
-  long       = "force-no-limit-cpu-while-dump"
-  type       = "bool"
-  default    = "false"
-  help       = "Force no CPU limit when dumping models and proofs"
-
 [[option]]
   name       = "foreignTheoryRewrite"
   category   = "regular"

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index d96e94d4375ff4f56cdbb582dbdcc315d312e6c7..eab982013413f075f66caf9e8d8e674230bb88d4 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -26,8 +26,8 @@
 #include "base/check.h"
 #include "base/output.h"
 #include "expr/kind.h"
+#include "options/base_options.h"
 #include "options/options.h"
-#include "options/options_public.h"
 #include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "smt/command.h"
@@ -900,7 +900,7 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s)
 api::Term Parser::mkStringConstant(const std::string& s)
 {
   if (language::isInputLang_smt2_6(
-          options::getInputLanguage(d_solver->getOptions())))
+          d_solver->getOptions().base.inputLanguage))
   {
     return d_solver->mkString(s, true);
   }

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 1f25e00dd17c8be0edd9690c7ed661aff405472a..816803ccc0ea8924ee278b086585ff1810e352da 100644 (file)
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -21,8 +21,9 @@
 #include "api/cpp/cvc5.h"
 #include "base/check.h"
 #include "cvc/cvc.h"
+#include "options/base_options.h"
 #include "options/options.h"
-#include "options/options_public.h"
+#include "options/parser_options.h"
 #include "parser/antlr_input.h"
 #include "parser/input.h"
 #include "parser/parser.h"
@@ -120,14 +121,14 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
 ParserBuilder& ParserBuilder::withOptions(const Options& opts)
 {
   ParserBuilder& retval = *this;
-  retval = retval.withInputLanguage(options::getInputLanguage(opts))
-               .withChecks(options::getSemanticChecks(opts))
-               .withStrictMode(options::getStrictParsing(opts))
-               .withParseOnly(options::getParseOnly(opts))
-               .withIncludeFile(options::getFilesystemAccess(opts));
-  if (options::wasSetByUserForceLogicString(opts))
+  retval = retval.withInputLanguage(opts.base.inputLanguage)
+               .withChecks(opts.parser.semanticChecks)
+               .withStrictMode(opts.parser.strictParsing)
+               .withParseOnly(opts.base.parseOnly)
+               .withIncludeFile(opts.parser.filesystemAccess);
+  if (opts.parser.forceLogicStringWasSetByUser)
   {
-    LogicInfo tmp(options::getForceLogicString(opts));
+    LogicInfo tmp(opts.parser.forceLogicString);
     retval = retval.withForcedLogic(tmp.getLogicString());
   }
   return retval;

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 56aebdcf76ec0dc2ddd7a61cb4e85223dcc48e7e..282b72974c4230352875ad5f6e3d999f559e3889 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -17,6 +17,7 @@
 #include <algorithm>
 
 #include "base/check.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "options/options_public.h"
 #include "parser/antlr_input.h"
@@ -846,7 +847,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name)
 
 InputLanguage Smt2::getLanguage() const
 {
-  return options::getInputLanguage(d_solver->getOptions());
+  return d_solver->getOptions().base.inputLanguage;
 }
 
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 89029b5eba087371942ef9050cb00f42bc271df4..eb6410291b10cc5f738e5f6c3f81f46e37031847 100644 (file)
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -29,8 +29,8 @@
 #include "base/check.h"
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
+#include "options/base_options.h"
 #include "options/options.h"
-#include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 15a16888dff7e27c4055b8b3d5d7dfbb16686a19..df9d44e39b334f2c8c03bfacf34a76e34b3c0b2e 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -26,6 +26,7 @@
 #include "expr/node.h"
 #include "expr/node_traversal.h"
 #include "expr/skolem_manager.h"
+#include "options/base_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 5bfb2a79f5dc880cc0fee59e338678f8e0a8bb26..d1dd389aed78c730d2bc41bae481f7ae631a00c2 100644 (file)
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -17,6 +17,7 @@
 
 #include <vector>
 
+#include "options/base_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 79fcc402883feeb4e824523511978b801fad0a68..a5720e7584b62e5f76003ca40504ef9899af90b0 100644 (file)
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -22,7 +22,7 @@
 #include "expr/node_self_iterator.h"
 #include "expr/skolem_manager.h"
 #include "options/arith_options.h"
-#include "options/smt_options.h"
+#include "options/base_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index fd86d3a42e214e64426fbaf05f698dde522c91a9..6f99a47f052835c786680ef1cb23e4a32d3b4c3d 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "base/check.h"
 #include "base/output.h"
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/prop_options.h"
 #include "options/smt_options.h"

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index d672b79a6a0bc544a73d3c997e194d2c4fe9ca13..5f0da7a0c4e132c70ab05410c3c82bb280227efd 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -31,6 +31,7 @@
 #include "expr/symbol_manager.h"
 #include "expr/type_node.h"
 #include "options/options.h"
+#include "options/main_options.h"
 #include "options/printer_options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 7406b922efa280fe11a23586db3323443c327157..3c0a4ac5b4eccd1cf4054597c84fe22850d1a943 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -15,6 +15,7 @@
 
 #include "smt/preprocessor.h"
 
+#include "options/base_options.h"
 #include "options/expr_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/preprocessing_pass_context.h"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index cd05b84c408e63bc61eac93f798f4b1b6398537f..e119ce4d4ce29b17b524d7909d9cce5fc39c25d6 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -66,7 +66,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // unsat cores and proofs shenanigans
   if (options::dumpUnsatCoresFull())
   {
-    opts.smt.dumpUnsatCores = true;
+    opts.driver.dumpUnsatCores = true;
   }
   if (options::checkUnsatCores() || options::dumpUnsatCores()
       || options::unsatAssumptions()

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bd48fe0eacdcb76613fbb8d9b153ab69deb81cd7..9056e7c94158e193539adaad5bf8a4ce3f7fbbfa 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -29,7 +29,6 @@
 #include "options/option_exception.h"
 #include "options/printer_options.h"
 #include "options/proof_options.h"
-#include "options/resource_manager_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
@@ -1811,16 +1810,16 @@ void SmtEngine::setResourceLimit(uint64_t units, bool cumulative)
 {
   if (cumulative)
   {
-    d_env->d_options.resman.cumulativeResourceLimit = units;
+    d_env->d_options.base.cumulativeResourceLimit = units;
   }
   else
   {
-    d_env->d_options.resman.perCallResourceLimit = units;
+    d_env->d_options.base.perCallResourceLimit = units;
   }
 }
 void SmtEngine::setTimeLimit(uint64_t millis)
 {
-  d_env->d_options.resman.perCallMillisecondLimit = millis;
+  d_env->d_options.base.perCallMillisecondLimit = millis;
 }
 
 unsigned long SmtEngine::getResourceUsage() const

diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 4afa15a3bc6b36a15a82351fc87ef91e3b732f79..cb0a9412339d8d14aca5ea3d4978beac34098cee 100644 (file)
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -16,6 +16,7 @@
 #include "smt/smt_engine_state.h"
 
 #include "base/modal_exception.h"
+#include "options/base_options.h"
 #include "options/option_exception.h"
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 8fa610cdaaf8d464fb2bea5cebab302042f3ab78..98278ef9e20e41ea5411930a52765587b28cdd32 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -20,6 +20,7 @@
 #include "base/modal_exception.h"
 #include "expr/dtype.h"
 #include "expr/skolem_manager.h"
+#include "options/base_options.h"
 #include "options/option_exception.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 99b95719fdd2ac4a66f718487cc1f2a829b06597..3dff64113dfa9215f4ae0d371d6f4c82f44703d6 100644 (file)
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -22,6 +22,7 @@
 
 #include "base/output.h"
 #include "expr/skolem_manager.h"
+#include "options/base_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/util/ite_utilities.h"
 #include "theory/arith/arith_utilities.h"

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a675c1bf411e0bd5895aee117ba08fb946058c36..97b29b6b3cfff2be41d0bf59273d45b702177339 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -35,7 +35,7 @@
 #include "expr/node_builder.h"
 #include "expr/skolem_manager.h"
 #include "options/arith_options.h"
-#include "options/smt_options.h"  // for incrementalSolving()
+#include "options/base_options.h"
 #include "preprocessing/util/ite_utilities.h"
 #include "proof/proof_generator.h"
 #include "proof/proof_node_manager.h"

diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 9871f2a9290d67db3b1276c659a3aa3623e4a019..55ed6c41d46b6ef74f00c98764d28f84a8edcb74 100644 (file)
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -16,6 +16,7 @@
 #include "theory/bv/bitblast/eager_bitblaster.h"
 
 #include "cvc5_private.h"
+#include "options/base_options.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "prop/cnf_stream.h"

diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 2d0ae1931b638cd7af5c3702169e0dd698ea825a..b0082b992575671bd3000bdc19c7ff31ba8ffddb 100644 (file)
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/bv/bv_eager_solver.h"
 
+#include "options/base_options.h"
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "theory/bv/bitblast/aig_bitblaster.h"

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 71f4028ec6456f19ac7db83b0e5cd98cb1a463aa..0f82d83012d3f20ebbc87cf6c001ff912b7b1c09 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/instantiate.h"
 
 #include "expr/node_algorithm.h"
+#include "options/base_options.h"
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"

diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 5b7bd15527a15a89ab99f6a7c9cfaba0bdebdd47..31e5240df29df751565f880b9c1150fbdfbcc3e9 100644 (file)
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/term_registry.h"
 
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "theory/quantifiers/first_order_model.h"

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index f0cc78789b9442c3c68fd53d2f3e03504a2dbb76..c4a94dfa2a91e01f7a7a9d30f7bf3e85b26fe99e 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -22,9 +22,9 @@
 #include "base/check.h"
 #include "base/listener.h"
 #include "base/output.h"
+#include "options/base_options.h"
 #include "options/option_exception.h"
 #include "options/options.h"
-#include "options/resource_manager_options.h"
 #include "util/statistics_registry.h"
 
 using namespace std;
@@ -164,7 +164,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats,
 
   d_infidWeights.fill(1);
   d_resourceWeights.fill(1);
-  for (const auto& opt : d_options.resman.resourceWeightHolder)
+  for (const auto& opt : d_options.base.resourceWeightHolder)
   {
     std::string name;
     uint64_t weight;
@@ -189,9 +189,9 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }
 
 uint64_t ResourceManager::getResourceRemaining() const
 {
-  if (d_options.resman.cumulativeResourceLimit <= d_cumulativeResourceUsed)
+  if (d_options.base.cumulativeResourceLimit <= d_cumulativeResourceUsed)
     return 0;
-  return d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed;
+  return d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed;
 }
 
 void ResourceManager::spendResource(uint64_t amount)
@@ -237,21 +237,21 @@ void ResourceManager::spendResource(theory::InferenceId iid)
 
 void ResourceManager::beginCall()
 {
-  d_perCallTimer.set(d_options.resman.perCallMillisecondLimit);
+  d_perCallTimer.set(d_options.base.perCallMillisecondLimit);
   d_thisCallResourceUsed = 0;
 
-  if (d_options.resman.cumulativeResourceLimit > 0)
+  if (d_options.base.cumulativeResourceLimit > 0)
   {
     // Compute remaining cumulative resource budget
     d_thisCallResourceBudget =
-        d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed;
+        d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed;
   }
-  if (d_options.resman.perCallResourceLimit > 0)
+  if (d_options.base.perCallResourceLimit > 0)
   {
     // Check if per-call resource budget is even smaller
-    if (d_options.resman.perCallResourceLimit < d_thisCallResourceBudget)
+    if (d_options.base.perCallResourceLimit < d_thisCallResourceBudget)
     {
-      d_thisCallResourceBudget = d_options.resman.perCallResourceLimit;
+      d_thisCallResourceBudget = d_options.base.perCallResourceLimit;
     }
   }
 }
@@ -265,25 +265,25 @@ void ResourceManager::endCall()
 
 bool ResourceManager::limitOn() const
 {
-  return (d_options.resman.cumulativeResourceLimit > 0)
-         || (d_options.resman.perCallMillisecondLimit > 0)
-         || (d_options.resman.perCallResourceLimit > 0);
+  return (d_options.base.cumulativeResourceLimit > 0)
+         || (d_options.base.perCallMillisecondLimit > 0)
+         || (d_options.base.perCallResourceLimit > 0);
 }
 
 bool ResourceManager::outOfResources() const
 {
-  if (d_options.resman.perCallResourceLimit > 0)
+  if (d_options.base.perCallResourceLimit > 0)
   {
     // Check if per-call resources are exhausted
-    if (d_thisCallResourceUsed >= d_options.resman.perCallResourceLimit)
+    if (d_thisCallResourceUsed >= d_options.base.perCallResourceLimit)
     {
       return true;
     }
   }
-  if (d_options.resman.cumulativeResourceLimit > 0)
+  if (d_options.base.cumulativeResourceLimit > 0)
   {
     // Check if cumulative resources are exhausted
-    if (d_cumulativeResourceUsed >= d_options.resman.cumulativeResourceLimit)
+    if (d_cumulativeResourceUsed >= d_options.base.cumulativeResourceLimit)
     {
       return true;
     }
@@ -293,7 +293,7 @@ bool ResourceManager::outOfResources() const
 
 bool ResourceManager::outOfTime() const
 {
-  if (d_options.resman.perCallMillisecondLimit == 0) return false;
+  if (d_options.base.perCallMillisecondLimit == 0) return false;
   return d_perCallTimer.expired();
 }
 

diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 9794888b2e861e425c0b7161a1044db72322b475..ee58b7ad48a01ed858ce59f479d143e77dd9b42a 100644 (file)
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -18,6 +18,7 @@
 #include <sstream>
 
 #include "api/cpp/cvc5.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "options/options_public.h"
 #include "options/set_language.h"
@@ -35,8 +36,8 @@ void testGetInfo(api::Solver* solver, const char* s);
 int main()
 {
   Options opts;
-  options::setInputLanguage(language::input::LANG_SMTLIB_V2, opts);
-  options::setOutputLanguage(language::output::LANG_SMTLIB_V2, opts);
+  opts.base.inputLanguage = language::input::LANG_SMTLIB_V2;
+  opts.base.outputLanguage = language::output::LANG_SMTLIB_V2;
 
   cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);