diff options
37 files changed, 248 insertions, 377 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 668fc9382..307222988 100644 --- 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 6bdc1abc9..b6ead1b70 100644 --- 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 697501d13..ed1825711 100644 --- 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 048c101f0..964b88ea0 100644 --- 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 2b25e6c93..a00e29b04 100644 --- 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 c0fc6846a..28a0087bb 100644 --- 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 978c32888..26ced1a24 100644 --- 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 f9d1c1a18..64d373509 100644 --- 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" @@ -76,6 +77,15 @@ name = "Base" 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" category = "common" @@ -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 0f5dfdcd7..fdaebbd6d 100644 --- 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 c1c843802..1ac5ec56d 100644 --- 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 35e891f5a..552058312 100644 --- 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 1d2f9edba..60929c96c 100644 --- 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 6fc683368..f19b903a6 100644 --- 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 index 6d5c4d4cf..000000000 --- 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 d1354f777..4d08aa672 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -79,14 +79,6 @@ name = "SMT Layer" 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" long = "model-cores=MODE" @@ -131,14 +123,6 @@ name = "SMT Layer" 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" long = "check-proofs" @@ -146,14 +130,6 @@ name = "SMT Layer" 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" long = "sygus-out=MODE" @@ -218,22 +194,6 @@ name = "SMT Layer" 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" long = "produce-unsat-assumptions" @@ -360,15 +320,6 @@ name = "SMT Layer" 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" long = "abstract-values" @@ -422,14 +373,6 @@ name = "SMT Layer" 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" long = "foreign-theory-rewrite" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index d96e94d43..eab982013 100644 --- 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 1f25e00dd..816803ccc 100644 --- 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 56aebdcf7..282b72974 100644 --- 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 89029b5eb..eb6410291 100644 --- 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 15a16888d..df9d44e39 100644 --- 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 5bfb2a79f..d1dd389ae 100644 --- 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 79fcc4028..a5720e758 100644 --- 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 fd86d3a42..6f99a47f0 100644 --- 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 d672b79a6..5f0da7a0c 100644 --- 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 7406b922e..3c0a4ac5b 100644 --- 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 cd05b84c4..e119ce4d4 100644 --- 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 bd48fe0ea..9056e7c94 100644 --- 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 4afa15a3b..cb0a94123 100644 --- 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 8fa610cda..98278ef9e 100644 --- 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 99b95719f..3dff64113 100644 --- 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 a675c1bf4..97b29b6b3 100644 --- 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 9871f2a92..55ed6c41d 100644 --- 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 2d0ae1931..b0082b992 100644 --- 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 71f4028ec..0f82d8301 100644 --- 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 5b7bd1552..31e5240df 100644 --- 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 f0cc78789..c4a94dfa2 100644 --- 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 9794888b2..ee58b7ad4 100644 --- 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); |