From 6bae871954c48993009ed91d4b907c136017ed38 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 15 Jun 2021 22:30:19 +0200 Subject: 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. --- src/api/cpp/cvc5.cpp | 17 ++--- src/main/command_executor.cpp | 43 +++++------ src/main/driver_unified.cpp | 72 +++++++++---------- src/main/interactive_shell.cpp | 17 ++--- src/main/main.cpp | 16 ++--- src/main/time_limit.cpp | 4 +- src/options/CMakeLists.txt | 1 - src/options/base_options.toml | 59 +++++++++++++++ src/options/main_options.toml | 48 +++++++++++++ src/options/options_handler.cpp | 3 +- src/options/options_public.cpp | 108 ---------------------------- src/options/options_public.h | 36 ---------- src/options/parser_options.toml | 1 + src/options/resource_manager_options.toml | 51 ------------- src/options/smt_options.toml | 57 --------------- src/parser/parser.cpp | 4 +- src/parser/parser_builder.cpp | 17 ++--- src/parser/smt2/smt2.cpp | 3 +- src/preprocessing/passes/ackermann.cpp | 2 +- src/preprocessing/passes/int_to_bv.cpp | 1 + src/preprocessing/passes/ite_simp.cpp | 1 + src/preprocessing/passes/miplib_trick.cpp | 2 +- src/prop/minisat/core/Solver.cc | 1 + src/smt/command.cpp | 1 + src/smt/preprocessor.cpp | 1 + src/smt/set_defaults.cpp | 2 +- src/smt/smt_engine.cpp | 7 +- src/smt/smt_engine_state.cpp | 1 + src/smt/sygus_solver.cpp | 1 + src/theory/arith/arith_ite_utils.cpp | 1 + src/theory/arith/theory_arith_private.cpp | 2 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 1 + src/theory/bv/bv_eager_solver.cpp | 1 + src/theory/quantifiers/instantiate.cpp | 1 + src/theory/quantifiers/term_registry.cpp | 1 + src/util/resource_manager.cpp | 36 +++++----- 36 files changed, 245 insertions(+), 375 deletions(-) delete mode 100644 src/options/resource_manager_options.toml (limited to 'src') 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& 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& 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 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 #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 > 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(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(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 > 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(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 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 #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" @@ -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" 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 -#include -#include -#include - -#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" 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 @@ -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 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 #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 +#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(); } -- cgit v1.2.3 From 4ca14e808d788ef9570dda1188645783c6a11e70 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 15 Jun 2021 15:44:52 -0700 Subject: pow2: adding a kind, inference rules, and some implementations in the pow2 solver (#6736) This PR is the sequel of #6676 . It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations. --- src/CMakeLists.txt | 1 + src/api/cpp/cvc5_kind.h | 16 ++++++++ src/theory/arith/kinds | 2 + src/theory/arith/nl/pow2_solver.cpp | 73 +++++++++++++++++++++++++++++++++++++ src/theory/inference_id.cpp | 4 ++ src/theory/inference_id.h | 5 +++ 6 files changed, 101 insertions(+) create mode 100644 src/theory/arith/nl/pow2_solver.cpp (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index bec3a8345..2419e1e41 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -441,6 +441,7 @@ libcvc5_add_sources( theory/arith/nl/nonlinear_extension.h theory/arith/nl/poly_conversion.cpp theory/arith/nl/poly_conversion.h + theory/arith/nl/pow2_solver.cpp theory/arith/nl/pow2_solver.h theory/arith/nl/stats.cpp theory/arith/nl/stats.h diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 2ec190360..2c5d2873e 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -412,6 +412,22 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(const Op& op, const std::vector& children) const` */ IAND, + /** + * Operator for raising 2 to a non-negative integer power + * + * Create with: + * - `Solver::mkOp(Kind kind) const` + * + + * Parameters: + * - 1: Op of kind IAND + * - 2: Integer term + * + * Create with: + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector& children) const` + */ + POW2, #if 0 /* Synonym for MULT. */ NONLINEAR_MULT, diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 396befb35..0c93db90f 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -26,6 +26,7 @@ operator INTS_MODULUS_TOTAL 2 "integer modulus with interpreted division by 0 (i operator ABS 1 "absolute value" parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term" operator POW 2 "arithmetic power" +operator POW2 1 "arithmetic power of 2" operator EXPONENTIAL 1 "exponential" operator SINE 1 "sine" @@ -148,6 +149,7 @@ typerule ARCTANGENT "SimpleTypeRule" typerule ARCCOSECANT "SimpleTypeRule" typerule ARCSECANT "SimpleTypeRule" typerule ARCCOTANGENT "SimpleTypeRule" +typerule POW2 "SimpleTypeRule" typerule SQRT "SimpleTypeRule" diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp new file mode 100644 index 000000000..534895c7f --- /dev/null +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -0,0 +1,73 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Makai Mann, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of pow2 solver. + */ + +#include "theory/arith/nl/pow2_solver.h" + +#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_state.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace arith { +namespace nl { + +Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model) + : d_im(im), d_model(model), d_initRefine(state.getUserContext()) +{ + NodeManager* nm = NodeManager::currentNM(); + d_false = nm->mkConst(false); + d_true = nm->mkConst(true); + d_zero = nm->mkConst(Rational(0)); + d_one = nm->mkConst(Rational(1)); + d_two = nm->mkConst(Rational(2)); +} + +Pow2Solver::~Pow2Solver() {} + +void Pow2Solver::initLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts) +{ + d_pow2s.clear(); + Trace("pow2-mv") << "POW2 terms : " << std::endl; + for (const Node& a : xts) + { + Kind ak = a.getKind(); + if (ak != POW2) + { + // don't care about other terms + continue; + } + d_pow2s.push_back(a); + } + Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl; +} + +void Pow2Solver::checkInitialRefine() {} + +void Pow2Solver::checkFullRefine() {} + +Node Pow2Solver::valueBasedLemma(Node i) { return Node(); } + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index fe4ed4c22..778c842a6 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -75,6 +75,10 @@ const char* toString(InferenceId i) return "ARITH_NL_IAND_SUM_REFINE"; case InferenceId::ARITH_NL_IAND_BITWISE_REFINE: return "ARITH_NL_IAND_BITWISE_REFINE"; + case InferenceId::ARITH_NL_POW2_INIT_REFINE: + return "ARITH_NL_POW2_INIT_REFINE"; + case InferenceId::ARITH_NL_POW2_VALUE_REFINE: + return "ARITH_NL_POW2_VALUE_REFINE"; case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT"; case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: return "ARITH_NL_CAD_EXCLUDED_INTERVAL"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 169992f41..6a87776d6 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -126,6 +126,11 @@ enum class InferenceId ARITH_NL_IAND_SUM_REFINE, // bitwise refinements (IAndSolver::checkFullRefine) ARITH_NL_IAND_BITWISE_REFINE, + //-------------------- nonlinear pow2 solver + // initial refinements (Pow2Solver::checkInitialRefine) + ARITH_NL_POW2_INIT_REFINE, + // value refinements (Pow2Solver::checkFullRefine) + ARITH_NL_POW2_VALUE_REFINE, //-------------------- nonlinear cad solver // conflict / infeasible subset obtained from cad ARITH_NL_CAD_CONFLICT, -- cgit v1.2.3 From c299e8661f24d3a6acb736e9e5df1b1920488ac3 Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Tue, 15 Jun 2021 16:20:20 -0700 Subject: [Optimization] Use Result in OptimizationResult (#6740) OptimizationResult now contains: - cvc5::Result - optimal value for objective - whether the objective is unbounded This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API. Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)... --- src/omt/bitvector_optimizer.cpp | 128 +++++++++++------------- src/omt/integer_optimizer.cpp | 13 ++- src/smt/optimization_solver.cpp | 91 +++++++++-------- src/smt/optimization_solver.h | 121 +++++++++++----------- test/unit/theory/theory_bv_opt_white.cpp | 20 ++-- test/unit/theory/theory_int_opt_white.cpp | 16 +-- test/unit/theory/theory_opt_multigoal_white.cpp | 49 ++++----- 7 files changed, 214 insertions(+), 224 deletions(-) (limited to 'src') diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index bce6c9b6d..01cb6da42 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -53,15 +53,13 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); - } - + // the last result that is SAT + Result lastSatResult = intermediateSatResult; // value equals to upperBound value = optChecker->getValue(target); @@ -104,39 +102,35 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, nm->mkNode(LTOperator, target, nm->mkConst(pivot)))); } intermediateSatResult = optChecker->checkSat(); - if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::SAT) + switch (intermediateSatResult.isSat()) { - value = optChecker->getValue(target); - upperBound = value.getConst(); - } - else if (intermediateSatResult.isSat() == Result::UNSAT) - { - if (lowerBound == pivot) - { - // lowerBound == pivot ==> upperbound = lowerbound + 1 - // and lowerbound <= target < upperbound is UNSAT - // return the upperbound + case Result::SAT_UNKNOWN: optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); - } - else - { - lowerBound = pivot; - } - } - else - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); + case Result::SAT: + lastSatResult = intermediateSatResult; + value = optChecker->getValue(target); + upperBound = value.getConst(); + break; + case Result::UNSAT: + if (lowerBound == pivot) + { + // lowerBound == pivot ==> upperbound = lowerbound + 1 + // and lowerbound <= target < upperbound is UNSAT + // return the upperbound + optChecker->pop(); + return OptimizationResult(lastSatResult, value); + } + else + { + lowerBound = pivot; + } + break; + default: Unreachable(); } optChecker->pop(); } - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, @@ -148,15 +142,13 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); - } - + // the last result that is SAT + Result lastSatResult = intermediateSatResult; // value equals to upperBound value = optChecker->getValue(target); @@ -196,39 +188,35 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, nm->mkNode(GTOperator, target, nm->mkConst(pivot)), nm->mkNode(LEOperator, target, nm->mkConst(upperBound)))); intermediateSatResult = optChecker->checkSat(); - if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::SAT) + switch (intermediateSatResult.isSat()) { - value = optChecker->getValue(target); - lowerBound = value.getConst(); - } - else if (intermediateSatResult.isSat() == Result::UNSAT) - { - if (lowerBound == pivot) - { - // upperbound = lowerbound + 1 - // and lowerbound < target <= upperbound is UNSAT - // return the lowerbound + case Result::SAT_UNKNOWN: optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); - } - else - { - upperBound = pivot; - } - } - else - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); + case Result::SAT: + lastSatResult = intermediateSatResult; + value = optChecker->getValue(target); + lowerBound = value.getConst(); + break; + case Result::UNSAT: + if (lowerBound == pivot) + { + // upperbound = lowerbound + 1 + // and lowerbound < target <= upperbound is UNSAT + // return the lowerbound + optChecker->pop(); + return OptimizationResult(lastSatResult, value); + } + else + { + upperBound = pivot; + } + break; + default: Unreachable(); } optChecker->pop(); } - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } } // namespace cvc5::omt diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index 045268337..379b0cd43 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -33,13 +33,10 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); + return OptimizationResult(intermediateSatResult, value); } // node storing target > old_value (used in optimization loop) Node increment; @@ -56,12 +53,14 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, // then assert optimization_target > current_model_value incrementalOperator = kind::GT; } + Result lastSatResult = intermediateSatResult; // Workhorse of linear search: // This loop will keep incrmenting/decrementing the objective until unsat // When unsat is hit, // the optimized value is the model value just before the unsat call while (intermediateSatResult.isSat() == Result::SAT) { + lastSatResult = intermediateSatResult; value = optChecker->getValue(target); Assert(!value.isNull()); increment = nm->mkNode(incrementalOperator, target, value); @@ -69,7 +68,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, intermediateSatResult = optChecker->checkSat(); } optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker, diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index e85ea82ef..a46452004 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -32,12 +32,11 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent) : d_parent(parent), d_optChecker(), d_objectives(parent->getUserContext()), - d_results(), - d_objectiveCombination(LEXICOGRAPHIC) + d_results() { } -OptimizationResult::ResultType OptimizationSolver::checkOpt() +Result OptimizationSolver::checkOpt(ObjectiveCombination combination) { // if the results of the previous call have different size than the // objectives, then we should clear the pareto optimization context @@ -48,7 +47,7 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt() { d_results.emplace_back(); } - switch (d_objectiveCombination) + switch (combination) { case BOX: return optimizeBox(); break; case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break; @@ -76,16 +75,9 @@ void OptimizationSolver::addObjective(TNode target, std::vector OptimizationSolver::getValues() { - Assert(d_objectives.size() == d_results.size()); return d_results; } -void OptimizationSolver::setObjectiveCombination( - ObjectiveCombination combination) -{ - d_objectiveCombination = combination; -} - std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) { @@ -106,13 +98,12 @@ std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( return optChecker; } -OptimizationResult::ResultType OptimizationSolver::optimizeBox() +Result OptimizationSolver::optimizeBox() { // resets the optChecker d_optChecker = createOptCheckerWithTimeout(d_parent); OptimizationResult partialResult; - OptimizationResult::ResultType aggregatedResultType = - OptimizationResult::OPTIMAL; + Result aggregatedResult(Result::Sat::SAT); std::unique_ptr optimizer; for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { @@ -134,18 +125,19 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox() } // match the optimization result type, and aggregate the results of // subproblems - switch (partialResult.getType()) + switch (partialResult.getResult().isSat()) { - case OptimizationResult::OPTIMAL: break; - case OptimizationResult::UNBOUNDED: break; - case OptimizationResult::UNSAT: - if (aggregatedResultType == OptimizationResult::OPTIMAL) + case Result::SAT: break; + case Result::UNSAT: + // the assertions are unsatisfiable + for (size_t j = 0; j < numObj; ++j) { - aggregatedResultType = OptimizationResult::UNSAT; + d_results[j] = partialResult; } - break; - case OptimizationResult::UNKNOWN: - aggregatedResultType = OptimizationResult::UNKNOWN; + d_optChecker.reset(); + return partialResult.getResult(); + case Result::SAT_UNKNOWN: + aggregatedResult = partialResult.getResult(); break; default: Unreachable(); } @@ -154,15 +146,20 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox() } // kill optChecker after optimization ends d_optChecker.reset(); - return aggregatedResultType; + return aggregatedResult; } -OptimizationResult::ResultType -OptimizationSolver::optimizeLexicographicIterative() +Result OptimizationSolver::optimizeLexicographicIterative() { // resets the optChecker d_optChecker = createOptCheckerWithTimeout(d_parent); - OptimizationResult partialResult; + // partialResult defaults to SAT if no objective is present + // NOTE: the parenthesis around Result(Result::SAT) is required, + // otherwise the compiler will report "parameter declarator cannot be + // qualified". For more details: + // https://stackoverflow.com/questions/44045257/c-compiler-error-c2751-what-exactly-causes-it + // https://en.wikipedia.org/wiki/Most_vexing_parse + OptimizationResult partialResult((Result(Result::SAT)), TNode()); std::unique_ptr optimizer; for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { @@ -186,26 +183,33 @@ OptimizationSolver::optimizeLexicographicIterative() d_results[i] = partialResult; // checks the optimization result of the current objective - switch (partialResult.getType()) + switch (partialResult.getResult().isSat()) { - case OptimizationResult::OPTIMAL: + case Result::SAT: // assert target[i] == value[i] and proceed d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode( kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue())); break; - case OptimizationResult::UNBOUNDED: return OptimizationResult::UNBOUNDED; - case OptimizationResult::UNSAT: return OptimizationResult::UNSAT; - case OptimizationResult::UNKNOWN: return OptimizationResult::UNKNOWN; + case Result::UNSAT: + d_optChecker.reset(); + return partialResult.getResult(); + case Result::SAT_UNKNOWN: + d_optChecker.reset(); + return partialResult.getResult(); default: Unreachable(); } + + // if the result for the current objective is unbounded + // then just stop + if (partialResult.isUnbounded()) break; } // kill optChecker in case pareto misuses it d_optChecker.reset(); - // now all objectives are OPTIMAL, just return OPTIMAL as overall result - return OptimizationResult::OPTIMAL; + // now all objectives are optimal, just return SAT as the overall result + return partialResult.getResult(); } -OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() +Result OptimizationSolver::optimizeParetoNaiveGIA() { // initial call to Pareto optimizer, create the checker if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent); @@ -216,8 +220,8 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() switch (satResult.isSat()) { - case Result::Sat::UNSAT: return OptimizationResult::UNSAT; - case Result::Sat::SAT_UNKNOWN: return OptimizationResult::UNKNOWN; + case Result::Sat::UNSAT: return satResult; + case Result::Sat::SAT_UNKNOWN: return satResult; case Result::Sat::SAT: { // if satisfied, use d_results to store the initial results @@ -226,14 +230,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { d_results[i] = OptimizationResult( - OptimizationResult::OPTIMAL, - d_optChecker->getValue(d_objectives[i].getTarget())); + satResult, d_optChecker->getValue(d_objectives[i].getTarget())); } break; } default: Unreachable(); } + Result lastSatResult = satResult; + // a vector storing assertions saying that no objective is worse std::vector noWorseObj; // a vector storing assertions saying that there is at least one objective @@ -278,15 +283,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() case Result::Sat::SAT_UNKNOWN: // if result is UNKNOWN, abort the current session and return UNKNOWN d_optChecker.reset(); - return OptimizationResult::UNKNOWN; + return satResult; case Result::Sat::SAT: { + lastSatResult = satResult; // if result is SAT, update d_results to the more optimal values for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { d_results[i] = OptimizationResult( - OptimizationResult::OPTIMAL, - d_optChecker->getValue(d_objectives[i].getTarget())); + satResult, d_optChecker->getValue(d_objectives[i].getTarget())); } break; } @@ -302,7 +307,7 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() // for the next run. d_optChecker->assertFormula(nm->mkOr(someObjBetter)); - return OptimizationResult::OPTIMAL; + return lastSatResult; } } // namespace smt diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 6d138deb2..d13168780 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -33,63 +33,75 @@ namespace smt { /** * The optimization result of an optimization objective * containing: - * - whether it's optimal or not - * - if so, the optimal value, otherwise the value might be empty node or - * something suboptimal + * - the optimization result: SAT/UNSAT/UNKNOWN + * - the optimal value if SAT and bounded + * (optimal value reached and it's not infinity), + * or an empty node if SAT and unbounded + * (optimal value is +inf for maximum or -inf for minimum), + * otherwise the value might be empty node + * or something suboptimal + * - whether the objective is unbounded */ class OptimizationResult { public: - /** - * Enum indicating whether the checkOpt result - * is optimal or not. - **/ - enum ResultType - { - // whether the value is optimal is UNKNOWN - UNKNOWN, - // the original set of assertions has result UNSAT - UNSAT, - // the value is optimal - OPTIMAL, - // the goal is unbounded, - // if objective is maximize, it's +infinity - // if objective is minimize, it's -infinity - UNBOUNDED, - }; - /** * Constructor * @param type the optimization outcome * @param value the optimized value + * @param unbounded whether the objective is unbounded **/ - OptimizationResult(ResultType type, TNode value) - : d_type(type), d_value(value) + OptimizationResult(Result result, TNode value, bool unbounded = false) + : d_result(result), d_value(value), d_unbounded(unbounded) + { + } + OptimizationResult() + : d_result(Result::Sat::SAT_UNKNOWN, + Result::UnknownExplanation::NO_STATUS), + d_value(), + d_unbounded(false) { } - OptimizationResult() : d_type(UNKNOWN), d_value() {} ~OptimizationResult() = default; /** * Returns an enum indicating whether - * the result is optimal or not. - * @return an enum showing whether the result is optimal, unbounded, - * unsat or unknown. + * the result is SAT or not. + * @return whether the result is SAT, UNSAT or SAT_UNKNOWN **/ - ResultType getType() const { return d_type; } + Result getResult() const { return d_result; } + /** * Returns the optimal value. * @return Node containing the optimal value, - * if getType() is not OPTIMAL, it might return an empty node or a node - * containing non-optimal value + * if result is unbounded, this will be an empty node, + * if getResult() is UNSAT, it will return an empty node, + * if getResult() is SAT_UNKNOWN, it will return something suboptimal + * or an empty node, depending on how the solver runs. **/ Node getValue() const { return d_value; } + /** + * Checks whether the objective is unbouned + * @return whether the objective is unbounded + * if the objective is unbounded (this function returns true), + * then the optimal value is: + * +inf, if it's maximize; + * -inf, if it's minimize + **/ + bool isUnbounded() const { return d_unbounded; } + private: - /** the indicating whether the result is optimal or something else **/ - ResultType d_type; - /** if the result is optimal, this is storing the optimal value **/ + /** indicating whether the result is SAT, UNSAT or UNKNOWN **/ + Result d_result; + /** if the result is bounded, this is storing the value **/ Node d_value; + /** whether the objective is unbounded + * If this is true, then: + * if objective is maximize, it's +infinity; + * if objective is minimize, it's -infinity + **/ + bool d_unbounded; }; /** @@ -199,10 +211,10 @@ class OptimizationSolver /** * Run the optimization loop for the added objective * For multiple objective combination, it defaults to lexicographic, - * and combination could be set by calling - * setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO) + * possible combinations: BOX, LEXICOGRAPHIC, PARETO + * @param combination BOX / LEXICOGRAPHIC / PARETO */ - OptimizationResult::ResultType checkOpt(); + Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC); /** * Add an optimization objective. @@ -223,11 +235,6 @@ class OptimizationSolver **/ std::vector getValues(); - /** - * Sets the objective combination - **/ - void setObjectiveCombination(ObjectiveCombination combination); - private: /** * Initialize an SMT subsolver for offline optimization purpose @@ -244,26 +251,26 @@ class OptimizationSolver /** * Optimize multiple goals in Box order - * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED; - * UNSAT if at least one objective is UNSAT and no objective is UNKNOWN; - * UNKNOWN if any of the objective is UNKNOWN. + * @return SAT if all of the objectives are optimal or unbounded; + * UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN; + * SAT_UNKNOWN if any of the objective is SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeBox(); + Result optimizeBox(); /** * Optimize multiple goals in Lexicographic order, * using iterative implementation - * @return OPTIMAL if all objectives are OPTIMAL and bounded; - * UNBOUNDED if one of the objectives is UNBOUNDED + * @return SAT if the objectives are optimal, + * if one of the objectives is unbounded, + * the optimization will stop at that objective; + * UNSAT if any of the objectives is UNSAT * and optimization will stop at that objective; - * UNSAT if one of the objectives is UNSAT - * and optimization will stop at that objective; - * UNKNOWN if one of the objectives is UNKNOWN + * SAT_UNKNOWN if any of the objectives is UNKNOWN * and optimization will stop at that objective; * If the optimization is stopped at an objective, - * all objectives following that objective will be UNKNOWN. + * all objectives following that objective will be SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeLexicographicIterative(); + Result optimizeLexicographicIterative(); /** * Optimize multiple goals in Pareto order @@ -277,11 +284,12 @@ class OptimizationSolver * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm. * Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009. * - * @return if it finds a new Pareto optimal result it will return OPTIMAL; + * @return if it finds a new Pareto optimal result it will return SAT; * if it exhausts the results in the Pareto front it will return UNSAT; - * if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN. + * if the underlying SMT solver returns SAT_UNKNOWN, + * it will return SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeParetoNaiveGIA(); + Result optimizeParetoNaiveGIA(); /** A pointer to the parent SMT engine **/ SmtEngine* d_parent; @@ -294,9 +302,6 @@ class OptimizationSolver /** The results of the optimizations from the last checkOpt call **/ std::vector d_results; - - /** The current objective combination method **/ - ObjectiveCombination d_objectiveCombination; }; } // namespace smt diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index c23ce79dd..5cd29878e 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -57,9 +57,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, (uint32_t)0x3FFFFFA1)); @@ -78,9 +78,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); BitVector val = d_optslv->getValues()[0].getValue().getConst(); std::cout << "opt value is: " << val << std::endl; @@ -105,9 +105,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); BitVector val = d_optslv->getValues()[0].getValue().getConst(); std::cout << "opt value is: " << val << std::endl; @@ -130,9 +130,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the maxmum x = ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), @@ -154,9 +154,9 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the maximum x = 18 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index cf0434ddc..583f908e7 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -62,9 +62,9 @@ TEST_F(TestTheoryWhiteIntOpt, max) // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // We expect max_cost == 99 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), @@ -93,9 +93,9 @@ TEST_F(TestTheoryWhiteIntOpt, min) // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // We expect max_cost == 99 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), @@ -125,10 +125,10 @@ TEST_F(TestTheoryWhiteIntOpt, result) d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); // This should return OPT_UNSAT since 0 > x > 100 is impossible. - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); // We expect our check to have returned UNSAT - ASSERT_EQ(r, OptimizationResult::UNSAT); + ASSERT_EQ(r.isSat(), Result::UNSAT); d_smtEngine->resetAssertions(); } @@ -157,9 +157,9 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index 73c6d9e7e..9a091fb3b 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -54,11 +54,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) // y <= x d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - // Box optimization OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::BOX); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // maximize y with `signed` comparison over bit-vectors. @@ -66,9 +63,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + // Box optimization + Result r = optSolver.checkOpt(OptimizationSolver::BOX); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector results = optSolver.getValues(); @@ -100,8 +98,6 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // maximize y with `signed` comparison over bit-vectors. @@ -109,9 +105,9 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector results = optSolver.getValues(); @@ -180,18 +176,17 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) (maximize b) */ OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::PARETO); optSolver.addObjective(a, OptimizationObjective::MAXIMIZE); optSolver.addObjective(b, OptimizationObjective::MAXIMIZE); - OptimizationResult::ResultType r; + Result r; // all possible result pairs std::set> possibleResults = { {1, 3}, {2, 2}, {3, 1}}; - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector results = optSolver.getValues(); std::pair res = { results[0].getValue().getConst().toInteger().toUnsignedInt(), @@ -205,8 +200,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); res = { results[0].getValue().getConst().toInteger().toUnsignedInt(), @@ -220,8 +215,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); res = { results[0].getValue().getConst().toInteger().toUnsignedInt(), @@ -235,8 +230,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::UNSAT); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::UNSAT); ASSERT_EQ(possibleResults.size(), 0); } @@ -254,11 +249,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // y <= x d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - // Lexico optimization OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); @@ -270,9 +262,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + // Lexico optimization + Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector results = optSolver.getValues(); @@ -290,16 +283,16 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) d_smtEngine->pop(); // now we only have one objective: (minimize x) - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); ASSERT_EQ(results.size(), 1); ASSERT_EQ(results[0].getValue().getConst(), BitVector(32u, 18u)); // resetting the assertions also resets the optimization objectives d_smtEngine->resetAssertions(); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); ASSERT_EQ(results.size(), 0); } -- cgit v1.2.3 From 6ae5647e754925a5c963d2b92c7255d7e0de6b03 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 16 Jun 2021 10:46:01 +0200 Subject: Properly consider aliases in option handlers (#6683) This PR makes sure that option handlers have access to both the canonical option name and the option name that was actually used. It also updates the options README and gets rid of the base_handlers.h of which only a fraction was used. --- src/options/CMakeLists.txt | 1 - src/options/README | 127 ----------------------- src/options/README.md | 211 +++++++++++++++++++++++++++++++++++++++ src/options/base_handlers.h | 87 ---------------- src/options/mkoptions.py | 51 +++++----- src/options/options_handler.cpp | 117 +++++++++++++++------- src/options/options_handler.h | 144 +++++++++++++++++--------- src/options/options_template.cpp | 91 ++++++++--------- src/options/prop_options.toml | 8 +- 9 files changed, 468 insertions(+), 369 deletions(-) delete mode 100644 src/options/README create mode 100644 src/options/README.md delete mode 100644 src/options/base_handlers.h (limited to 'src') diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 26ced1a24..cc7b621a8 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -17,7 +17,6 @@ check_python_module("toml") libcvc5_add_sources( - base_handlers.h decision_weight.h didyoumean.cpp didyoumean.h diff --git a/src/options/README b/src/options/README deleted file mode 100644 index 868690b85..000000000 --- a/src/options/README +++ /dev/null @@ -1,127 +0,0 @@ -Modules -======= - - Each options module starts with the following required attributes: - - id ... (string) ID of the module (e.g., "ARITH") - name ... (string) name of the module (e.g., "Arithmetic Theory") - header ... (string) name of the options header to generated (e.g., "options/arith_options.h") - - A module defines 0 or more options. - - In general, each attribute/value pair is required to be in one line. - Comments start with # and are not allowed in attribute/value lines. - - -Options -======= - - Options can be defined with the [[option]] tag, the required attributes for - an option are: - - category ... (string) common | expert | regular | undocumented - type ... (string) C++ type of the option value - - Optional attributes are: - - name ... (string) option name that is used to access via - options::() - smt_name ... (string) alternative name to access option via - set-option/get-option commands - short ... (string) short option name consisting of one character - (no '-' prefix required) - long ... (string) long option name (required if short is specified, - no '--' prefix required). - long option names may have a suffix '=XXX' where - 'XXX' can be used to indicate the type of the - option value, e.g., '=MODE', '=LANG', '=N', ... - default ... (string) default value of type 'type' - handler ... (string) handler for parsing option values before setting - option - predicates ... (list) functions that check whether given option value is - valid - includes ... (list) header files required by handler/predicates - alternate ... (bool) true (default): add --no- alternative option - false: omit --no- alternative option - help ... (string) documentation (required if category is not - undocumented) - - Note that if an option defines a long option name with type 'bool', - mkoptions.py automatically generates a --no- option to set the option - to false. - This behaviour can be explicitely disabled for options with attribute - alternate = false. - More information on how to use handler and predicates can be found - at the end of the README. - - - Example: - - [[option]] - name = "outputLanguage" - smt_name = "output-language" - category = "common" - short = "" - long = "output-lang=LANG" - type = "OutputLanguage" - default = "language::output::LANG_AUTO" - handler = "stringToOutputLanguage" - predicates = [] - includes = ["options/language.h"] - help = "force output language (default is \"auto\"; see --output-lang help)" - - -Further information (the old option package) -============================================ - - The options/ package supports a wide range of operations for responding to - an option being set. Roughly the three major concepts are: - - - handler to parse an option before setting its value. - - predicates to reject bad values for the option. - - More details on each class of custom handlers. - - - handler = "" - - Handlers provide support for parsing custom option types. - The signature for a handler call is: - - T custom-option-handler(std::string option, std::string optarg, - OptionsHandler* handler); - - where T is the type of the option. The suggested implementation is to - implement custom-handler as a dispatch into a function on handler with the - signature: - - T OptionsHandler::custom-option-handler(std::string option, - std::string optarg); - - The handlers are run before predicates. - Having multiple handlers is considered bad practice and is unsupported. - Handlers may have arbitrary side effects, but should call no code - inaccessible to liboptions. For side effects that are not required in order - to parse the option, using :predicate is recommended. Memory - management done by a handler needs to either be encapsulated by the type - and the destructor for the type or should *always* be owned by handler. - More elaborate memory management schemes are not currently supported. - - - predicates = [...] - - Predicates provide support for checking whether or not the value of an - option is acceptable. Predicates are run after handlers. - The signature for a predicate call is: - - void custom-predicate(std::string option, T value, - OptionsHandler* handler); - - where T is the type of the option. The suggested implementation is to - implement custom-predicate as a dispatch into a function on handler with - the signature: - - void OptionsHandler::custom-predicate(std::string option, T value); - - The predicates are run after handlers. Multiple - predicates may be defined for the same option, but the order they are run - is not guaranteed. Predicates may have arbitrary side effects, but should - call no code inaccessible to liboptions. diff --git a/src/options/README.md b/src/options/README.md new file mode 100644 index 000000000..df5686abc --- /dev/null +++ b/src/options/README.md @@ -0,0 +1,211 @@ +Specifying Modules +================== + +Every options module, that is a group of options that belong together in some +way, is declared in its own file in `options/{module name}_options.toml`. Each +options module starts with the following required attributes: + +* `id` (string): ID of the module (e.g., `"arith"`) +* `name` (string): name of the module (e.g., `"Arithmetic Theory"`) + +Additional, a module can optionally be defined to be public. A public module +includes `cvc5_public.h` instead of `cvc5_private.h` can thus be included from +"external" code like the parser or the main driver. + +* `public` (bool): make option module public + +A module defines 0 or more options. + +In general, each attribute/value pair is required to be in one line. Comments +start with # and are not allowed in attribute/value lines. + +After parsing, a module is extended to have the following attributes: + +* `id`: lower-case version of the parsed `id` +* `id_cap`: upper-case version of `id` (used for the `Holder{id_cap}` class) +* `filename`: base filename for generated files (`"{id}_options"`) +* `header`: generated header name (`"options/{filename}.h"`) + + +Specifying Options +================== + +Options can be defined within a module file with the `[[option]]` tag, the +required attributes for an option are: + +* `category` (string): one of `common`, `expert`, `regular`, or `undocumented` +* `type` (string): the C++ type of the option value + +Optional attributes are: + +* `name` (string): the option name used to access the option internally + (`d_option.{module.id}.{name}`) +* `long` (string): long option name (without `--` prefix). Long option names may + have a suffix `=XXX` where `XXX` can be used to indicate the type of the + option value, e.g., `=MODE`, `=LANG`, `=N`, ... +* `short` (string): short option name consisting of one character (no `-` prefix + required), can be given if `long` is specified +* `alias` (list): alternative names that can be used instead of `long` +* `default` (string): default value, needs to be a valid C++ expression of type + `type` +* `alternate` (bool, default `true`): if `true`, adds `--no-{long}` alternative + option +* `mode` (list): used to define options whose type shall be an auto-generated + enum, more details below +* `handler` (string): alternate parsing routine for option types not covered by + the default parsers, more details below +* `predicates` (list): custom validation function to check whether an option + value is valid, more details below +* `includes` (list): additional header files required by handler or predicate + functions +* `help` (string): documentation string (required, unless the `category` is + `undocumented`) +* `help_mode` (string): documentation for the mode enum (required if `mode` is + given) + + +Handler functions +----------------- + +Custom handler functions are used to turn the option value from a `std::string` +into the type specified by `type`. Standard handler functions are provided for +basic types (`std::string`, `bool`, integer types and floating point types) as +well as enums specified by `mode`. A custom handler function needs to be member +function of `options::OptionsHandler` with signature `{type} {handler}(const +std::string& option, const std::string& flag, const std::string& optionvalue)`, +or alternatively `void {handler}(const std::string& option, const std::string& +flag)` if the `type` is `void`. The two parameters `option` and `flag` hold the +canonical and the actually used option names, respectively, and they may differ +if an alternative name (from `alias`) was used. While `option` should be used to +identify an option (e.g. by comparing against `*__name`), `flag` should be +usually used in user messages. + + +Predicate functions +------------------- + +Predicate functions are used to check whether an option value is valid after it +has been parsed by a (standard or custom) handler function. Like a handler +function, a predicate function needs to be a member function of +`options::OptionsHandler` with signature `void {predicate}(const std::string& +option, const std::string& flag, {type} value)`. If the check fails, the +predicate should raise an `OptionException`. + + +Mode options +------------ + +An option can be defined to hold one of a given set of values we call modes. +Doing so automatically defines an `enum class` for the set of modes and makes +the option accept one of the values from the enum. The enum class will be called +`{type}` and methods `operator<<` and `stringTo{enum}` are automatically +generated. A mode is defined by specifying `[[option.mode.{NAME}]]` after the +main `[[option]]` section with the following attributes: + +* `name` (string): the string value that corresponds to the enum value +* `help` (string): documentation about this mode + +Example: + + [[option]] + name = "bitblastMode" + category = "regular" + long = "bitblast=MODE" + type = "BitblastMode" + default = "LAZY" + help = "choose bitblasting mode, see --bitblast=help" + help_mode = "Bit-blasting modes." + [[option.mode.LAZY]] + name = "lazy" + help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver." + [[option.mode.EAGER]] + name = "eager" + help = "Bitblast eagerly to bit-vector SAT solver." + +The option can now be set with `--bitblast=lazy`, `(set-option :bitblast +eager)`, or `options::set("bitblast", "eager")`. + + +Generated code +============== + +The entire options setup heavily relies on generating a lot of code from the +information retrieved from the `*_options.toml` files. After code generation, +files related to options live either in `src/options/` (if not changed) or in +`build/src/options/` (if automatically generated). After all code has been +generated, the entire options setup consists of the following components: + +* `options.h`: core `Options` class +* `options_api.h`: utility methods used by the API (`parse()`, `set()`, `get()`, + ...) +* `options_public.h`: utility methods used to access options from outside of + libcvc5 +* `{module}_options.h`: specifics for one single options module + + +`Options` class +--------------- + +The `Options` class is the central entry point for regular usage of options. It +holds a `std::unique_ptr` to an "option holder" for every option module, that +can be accessed using references `{module}` (either as `const&` or `&`). These +holders hold the actual option data for the specific module. + +The holder types are forward declared and can thus only be accessed if one also +includes the appropriate `{module}_options.h`, which contains the proper +declaration for the holder class. + + +Option modules +-------------- + +Every option module declares an "option holder" class, which is a simple struct +that has two members for every option (that is not declared as `type = void`): +the actual option value as `{option.type} {option.name}` and a Boolean flag +`bool {option.name}__setByUser` that indicates whether the option value was +explicitly set by the user. If any of the options of a module is a mode option, +the option module also defines an enum class that corresponds to the mode, +including `operator<<()` and `stringTo{mode type}`. + +For convenience, the option modules also provide methods `void +{module.id}::setDefault{option.name}(Options& opts, {option.type} value)`. Each +such method sets the option value to the given value, if the option was not yet +set by the user, i.e., the `__setByUser` flag is false. Additionally, every +option module exports the `long` option name as `static constexpr const char* +{module.id}::{option.name}__name`. + + +Full Example +============ + + [[option]] + category = "regular" + name = "decisionMode" + long = "decision=MODE" + alias = ["decision-mode"] + type = "DecisionMode" + default = "INTERNAL" + predicates = ["setDecisionModeStopOnly"] + help = "choose decision mode, see --decision=help" + help_mode = "Decision modes." + [[option.mode.INTERNAL]] + name = "internal" + help = "Use the internal decision heuristics of the SAT solver." + [[option.mode.JUSTIFICATION]] + name = "justification" + help = "An ATGP-inspired justification heuristic." + [[option.mode.RELEVANCY]] + name = "justification-stoponly" + help = "Use the justification heuristic only to stop early, not for decisions." + +This defines a new option that is accessible via +`d_options.{module.id}.decisionMode` and stores an automatically generated mode +`DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and +`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also +with `--decision-mode=justification`, and similarly from an SMT-LIB input with +`(set-option :decision internal)` and `(set-option :decision-mode +justification)`. The command-line help for this option looks as follows: + + --output-lang=LANG | --output-language=LANG + force output language (default is "auto"; see + --output-lang help) diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h deleted file mode 100644 index 86112a907..000000000 --- a/src/options/base_handlers.h +++ /dev/null @@ -1,87 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include "cvc5_private.h" - -#ifndef CVC5__BASE_HANDLERS_H -#define CVC5__BASE_HANDLERS_H - -#include -#include -#include - -#include "options/option_exception.h" - -namespace cvc5 { -namespace options { - -template