From c32f952b1e496a5bd05552f676d51b5af3e49ed0 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 26 Apr 2021 21:43:15 +0200 Subject: [PATCH] First part of options refactoring (#6428) This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular - it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser()) - it removes options::optionName.set() (we still have Options::set()) - it removes options::optionName.getName() in favor of options::optionName.name - it removes the specializations of Options::assign() and Options::assignBool() from the headers - it eliminates runHandlerAndPredicates() and runBoolPredicates() The removed methods are only used in few places with are changed to using Options::current().X() instead. In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine. --- src/options/bv_options.toml | 1 + src/options/mkoptions.py | 159 ++---- src/options/module_template.cpp | 2 + src/options/open_ostream.cpp | 1 + src/options/options.h | 51 +- src/options/options_handler.cpp | 64 +-- src/options/options_public_functions.cpp | 2 +- src/options/options_template.cpp | 9 +- src/printer/printer.cpp | 40 +- src/prop/minisat/simp/SimpSolver.cc | 2 +- src/smt/env.h | 6 + src/smt/managed_ostreams.cpp | 4 +- src/smt/options_manager.cpp | 28 +- src/smt/set_defaults.cpp | 499 +++++++++--------- src/smt/smt_engine.cpp | 105 ++-- src/smt/update_ostream.h | 2 +- src/theory/arith/theory_arith_private.cpp | 124 +---- src/theory/quantifiers/expr_miner.cpp | 2 +- .../quantifiers/sygus/sygus_repair_const.cpp | 2 +- 19 files changed, 461 insertions(+), 642 deletions(-) diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index acb010a2e..18f190ff1 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -51,6 +51,7 @@ header = "options/bv_options.h" category = "expert" long = "bv-aig-simp=COMMAND" type = "std::string" + default = "\"balance;drw\"" predicates = ["abcEnabledBuild"] help = "abc command to run AIG simplifications (implies --bitblast-aig, default is \"balance;drw\")" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 9c66c6b61..fa2a39b04 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -81,63 +81,35 @@ g_getopt_long_start = 256 TPL_HOLDER_MACRO_NAME = 'CVC5_OPTIONS__{id}__FOR_OPTION_HOLDER' -TPL_RUN_HANDLER = \ -"""template <> options::{name}__option_t::type runHandlerAndPredicates( - options::{name}__option_t, - std::string option, - std::string optionarg, - options::OptionsHandler* handler) -{{ - options::{name}__option_t::type retval = {handler}; - {predicates} - return retval; -}}""" - -TPL_DECL_ASSIGN = \ +TPL_IMPL_ASSIGN = \ """template <> void Options::assign( options::{name}__option_t, std::string option, - std::string value);""" - -TPL_IMPL_ASSIGN = TPL_DECL_ASSIGN[:-1] + \ -""" + std::string optionarg) {{ - d_holder->{name} = - runHandlerAndPredicates(options::{name}, option, value, d_handler); + auto parsedval = {handler}; + {predicates} + d_holder->{name} = parsedval; d_holder->{name}__setByUser__ = true; Trace("options") << "user assigned option {name}" << std::endl; }}""" - -TPL_RUN_HANDLER_BOOL = \ -"""template <> void runBoolPredicates( - options::{name}__option_t, - std::string option, - bool b, - options::OptionsHandler* handler) -{{ - {predicates} -}}""" - -TPL_DECL_ASSIGN_BOOL = \ +TPL_IMPL_ASSIGN_BOOL = \ """template <> void Options::assignBool( options::{name}__option_t, std::string option, - bool value);""" - -TPL_IMPL_ASSIGN_BOOL = TPL_DECL_ASSIGN_BOOL[:-1] + \ -""" + bool value) {{ - runBoolPredicates(options::{name}, option, value, d_handler); + {predicates} d_holder->{name} = value; d_holder->{name}__setByUser__ = true; Trace("options") << "user assigned option {name}" << std::endl; }}""" TPL_CALL_ASSIGN_BOOL = \ - ' options->assignBool(options::{name}, {option}, {value});' + ' assignBool(options::{name}, {option}, {value});' -TPL_CALL_ASSIGN = ' options->assign(options::{name}, {option}, optionarg);' +TPL_CALL_ASSIGN = ' assign(options::{name}, {option}, optionarg);' TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));' @@ -157,9 +129,7 @@ TPL_OPTION_STRUCT_RW = \ {{ typedef {type} type; type operator()() const; - bool wasSetByUser() const; - void set(const type& v); - const char* getName() const; + static constexpr const char* name = "{long_name}"; }} thread_local {name};""" TPL_OPTION_STRUCT_RO = \ @@ -167,20 +137,18 @@ TPL_OPTION_STRUCT_RO = \ {{ typedef {type} type; type operator()() const; - bool wasSetByUser() const; - const char* getName() const; + static constexpr const char* name = "{long_name}"; }} thread_local {name};""" TPL_DECL_SET = \ -"""template <> void Options::set( - options::{name}__option_t, - const options::{name}__option_t::type& x);""" +"""template <> options::{name}__option_t::type& Options::ref( + options::{name}__option_t);""" TPL_IMPL_SET = TPL_DECL_SET[:-1] + \ """ {{ - d_holder->{name} = x; + return d_holder->{name}; }}""" @@ -206,32 +174,12 @@ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \ # Option specific methods -TPL_IMPL_OPTION_SET = \ -"""inline void {name}__option_t::set(const {name}__option_t::type& v) -{{ - Options::current()->set(*this, v); -}}""" - TPL_IMPL_OP_PAR = \ """inline {name}__option_t::type {name}__option_t::operator()() const {{ - return (*Options::current())[*this]; -}}""" - -TPL_IMPL_OPTION_WAS_SET_BY_USER = \ -"""inline bool {name}__option_t::wasSetByUser() const -{{ - return Options::current()->wasSetByUser(*this); -}}""" - -TPL_IMPL_GET_NAME = \ -"""inline const char* {name}__option_t::getName() const -{{ - return "{long_name}"; + return Options::current()[*this]; }}""" - - # Mode templates TPL_DECL_MODE_ENUM = \ """ @@ -242,16 +190,14 @@ enum class {type} TPL_DECL_MODE_FUNC = \ """ -std::ostream& -operator<<(std::ostream& os, {type} mode);""" +std::ostream& operator<<(std::ostream& os, {type} mode);""" TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \ """ {{ - os << "{type}::"; switch(mode) {{{cases} default: - Unreachable(); + Unreachable(); }} return os; }} @@ -260,13 +206,11 @@ TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \ TPL_IMPL_MODE_CASE = \ """ case {type}::{enum}: - os << "{enum}"; - break;""" + return os << "{type}::{enum}";""" TPL_DECL_MODE_HANDLER = \ """ -{type} -stringTo{type}(const std::string& option, const std::string& optarg);""" +{type} stringTo{type}(const std::string& optarg);""" TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \ """ @@ -274,14 +218,11 @@ TPL_IMPL_MODE_HANDLER = TPL_DECL_MODE_HANDLER[:-1] + \ {cases} else if (optarg == "help") {{ - puts({help}); - exit(1); - }} - else - {{ - throw OptionException(std::string("unknown option for --{long}: `") + - optarg + "'. Try --{long}=help."); + std::cerr << {help}; + std::exit(1); }} + throw OptionException(std::string("unknown option for --{long}: `") + + optarg + "'. Try --{long}=help."); }} """ @@ -513,7 +454,11 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # Generate module declaration tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW - decls.append(tpl_decl.format(name=option.name, type=option.type)) + if option.long: + long_name = option.long.split('=')[0] + else: + long_name = "" + decls.append(tpl_decl.format(name=option.name, type=option.type, long_name = long_name)) # Generate module specialization if not option.read_only: @@ -521,11 +466,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): specs.append(TPL_DECL_OP_BRACKET.format(name=option.name)) specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name)) - if option.type == 'bool': - specs.append(TPL_DECL_ASSIGN_BOOL.format(name=option.name)) - else: - specs.append(TPL_DECL_ASSIGN.format(name=option.name)) - if option.long and option.type not in ['bool', 'void'] and \ '=' not in option.long: die("module '{}': option '{}' with type '{}' needs an argument " \ @@ -539,15 +479,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): # Generate module inlines inls.append(TPL_IMPL_OP_PAR.format(name=option.name)) - inls.append(TPL_IMPL_OPTION_WAS_SET_BY_USER.format(name=option.name)) - if not option.read_only: - inls.append(TPL_IMPL_OPTION_SET.format(name=option.name)) - if option.long: - long_name = option.long.split('=')[0] - else: - long_name = "" - inls.append(TPL_IMPL_GET_NAME.format( - name=option.name, long_name=long_name)) ### Generate code for {module.name}_options.cpp @@ -704,12 +635,12 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): handler = None if option.handler: if option.type == 'void': - handler = 'handler->{}(option)'.format(option.handler) + handler = 'd_handler->{}(option)'.format(option.handler) else: handler = \ - 'handler->{}(option, optionarg)'.format(option.handler) + 'd_handler->{}(option, optionarg)'.format(option.handler) elif option.mode: - handler = 'stringTo{}(option, optionarg)'.format(option.type) + handler = 'stringTo{}(optionarg)'.format(option.type) elif option.type != 'bool': handler = \ 'handleOption<{}>(option, optionarg)'.format(option.type) @@ -719,12 +650,12 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): if option.predicates: if option.type == 'bool': predicates = \ - ['handler->{}(option, b);'.format(x) \ + ['d_handler->{}(option, value);'.format(x) \ for x in option.predicates] else: assert option.type != 'void' predicates = \ - ['handler->{}(option, retval);'.format(x) \ + ['d_handler->{}(option, parsedval);'.format(x) \ for x in option.predicates] # Generate options_handler and getopt_long @@ -867,24 +798,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): options_getoptions.append(s) - # Define runBoolPredicates/runHandlerAndPredicates - tpl = None - if option.type == 'bool': - if predicates: - assert handler is None - tpl = TPL_RUN_HANDLER_BOOL - elif option.short or option.long: - assert option.type != 'void' - assert handler - tpl = TPL_RUN_HANDLER - if tpl: - custom_handlers.append( - tpl.format( - name=option.name, - handler=handler, - predicates='\n'.join(predicates) - )) - # Define handler assign/assignBool tpl = None if option.type == 'bool': @@ -893,7 +806,9 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): tpl = TPL_IMPL_ASSIGN if tpl: custom_handlers.append(tpl.format( - name=option.name + name=option.name, + handler=handler, + predicates='\n'.join(predicates) )) # Default option values diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index 3b928dba0..0de77e8a6 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -19,6 +19,8 @@ #include "options/options_holder.h" #include "base/check.h" +#include + // clang-format off namespace cvc5 { diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp index 3b13c42e2..9ebea6da0 100644 --- a/src/options/open_ostream.cpp +++ b/src/options/open_ostream.cpp @@ -20,6 +20,7 @@ #include +#include #include #include #include diff --git a/src/options/options.h b/src/options/options.h index 67707c990..b249c90ed 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -18,8 +18,7 @@ #ifndef CVC5__OPTIONS__OPTIONS_H #define CVC5__OPTIONS__OPTIONS_H -#include -#include +#include #include #include @@ -77,9 +76,6 @@ class CVC5_EXPORT Options static std::string formatThreadOptionException(const std::string& option); - static const size_t s_maxoptlen = 128; - static const unsigned s_preemptAdditional = 6; - public: class OptionsScope { @@ -102,8 +98,8 @@ public: } /** Get the current Options in effect */ - static inline Options* current() { - return s_current; + static inline Options& current() { + return *s_current; } Options(OptionsListener* ol = nullptr); @@ -117,15 +113,39 @@ public: void copyValues(const Options& options); /** - * Set the value of the given option. Use of this default - * implementation causes a compile-time error; write-able - * options specialize this template with a real implementation. + * Set the value of the given option. Uses `ref()`, which causes a + * compile-time error if the given option is read-only. + */ + template + void set(T t, const typename T::type& val) { + ref(t) = val; + } + + /** + * Set the default value of the given option. Is equivalent to calling `set()` + * if `wasSetByUser()` returns false. Uses `ref()`, which causes a compile-time + * error if the given option is read-only. + */ + template + void setDefault(T t, const typename T::type& val) + { + if (!wasSetByUser(t)) + { + ref(t) = val; + } + } + + /** + * Get a non-const reference to the value of the given option. Causes a + * compile-time error if the given option is read-only. Writeable options + * specialize this template with a real implementation. */ template - void set(T, const typename T::type&) { - // Flag a compile-time error. Write-able options specialize - // this template to provide an implementation. - T::you_are_trying_to_assign_to_a_read_only_option; + typename T::type& ref(T) { + // Flag a compile-time error. + T::you_are_trying_to_get_nonconst_access_to_a_read_only_option; + // Ensure the compiler does not complain about the return value. + return *static_cast(nullptr); } /** @@ -297,8 +317,7 @@ public: * * Preconditions: options, extender and nonoptions are non-null. */ - static void parseOptionsRecursive(Options* options, - int argc, + void parseOptionsRecursive(int argc, char* argv[], std::vector* nonoptions); }; /* class Options */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 0e2315aa0..dd555ab56 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -159,14 +159,11 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) || m == SatSolverMode::KISSAT)) { if (options::bitblastMode() == options::BitblastMode::LAZY - && options::bitblastMode.wasSetByUser()) + && Options::current().wasSetByUser(options::bitblastMode)) { throwLazyBBUnsupported(m); } - if (!options::bitvectorToBool.wasSetByUser()) - { - options::bitvectorToBool.set(true); - } + Options::current().setDefault(options::bitvectorToBool, true); } } @@ -174,23 +171,10 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) { if (m == options::BitblastMode::LAZY) { - if (!options::bitvectorPropagate.wasSetByUser()) - { - options::bitvectorPropagate.set(true); - } - if (!options::bitvectorEqualitySolver.wasSetByUser()) - { - options::bitvectorEqualitySolver.set(true); - } - - if (!options::bitvectorInequalitySolver.wasSetByUser()) - { - options::bitvectorInequalitySolver.set(true); - } - if (!options::bitvectorAlgebraicSolver.wasSetByUser()) - { - options::bitvectorAlgebraicSolver.set(true); - } + Options::current().setDefault(options::bitvectorPropagate, true); + Options::current().setDefault(options::bitvectorEqualitySolver, true); + Options::current().setDefault(options::bitvectorInequalitySolver, true); + Options::current().setDefault(options::bitvectorAlgebraicSolver, true); if (options::bvSatSolver() != options::SatSolverMode::MINISAT) { throwLazyBBUnsupported(options::bvSatSolver()); @@ -198,27 +182,21 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) } else if (m == BitblastMode::EAGER) { - if (!options::bitvectorToBool.wasSetByUser()) - { - options::bitvectorToBool.set(true); - } + Options::current().setDefault(options::bitvectorToBool, true); } } void OptionsHandler::setBitblastAig(std::string option, bool arg) { if(arg) { - if(options::bitblastMode.wasSetByUser()) { + if(Options::current().wasSetByUser(options::bitblastMode)) { if (options::bitblastMode() != options::BitblastMode::EAGER) { throw OptionException("bitblast-aig must be used with eager bitblaster"); } } else { - options::BitblastMode mode = stringToBitblastMode("", "eager"); - options::bitblastMode.set(mode); - } - if(!options::bitvectorAigSimplifications.wasSetByUser()) { - options::bitvectorAigSimplifications.set("balance;drw"); + options::BitblastMode mode = stringToBitblastMode("eager"); + Options::current().set(options::bitblastMode, mode); } } } @@ -253,13 +231,13 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, // decision/options_handlers.h void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m) { - options::decisionStopOnly.set(m == DecisionMode::RELEVANCY); + Options::current().set(options::decisionStopOnly, m == DecisionMode::RELEVANCY); } void OptionsHandler::setProduceAssertions(std::string option, bool value) { - options::produceAssertions.set(value); - options::interactiveMode.set(value); + Options::current().set(options::produceAssertions, value); + Options::current().set(options::interactiveMode, value); } void OptionsHandler::setStats(const std::string& option, bool value) @@ -278,22 +256,22 @@ void OptionsHandler::setStats(const std::string& option, bool value) std::string opt = option.substr(2); if (value) { - if (opt == options::statisticsAll.getName()) + if (opt == options::statisticsAll.name) { d_options->d_holder->statistics = true; } - else if (opt == options::statisticsEveryQuery.getName()) + else if (opt == options::statisticsEveryQuery.name) { d_options->d_holder->statistics = true; } - else if (opt == options::statisticsExpert.getName()) + else if (opt == options::statisticsExpert.name) { d_options->d_holder->statistics = true; } } else { - if (opt == options::statistics.getName()) + if (opt == options::statistics.name) { d_options->d_holder->statisticsAll = false; d_options->d_holder->statisticsEveryQuery = false; @@ -508,7 +486,7 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) { if(optarg == "help") { - options::languageHelp.set(true); + Options::current().set(options::languageHelp, true); return language::output::LANG_AUTO; } @@ -526,7 +504,7 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option, std::string optarg) { if(optarg == "help") { - options::languageHelp.set(true); + Options::current().set(options::languageHelp, true); return language::input::LANG_AUTO; } @@ -571,12 +549,12 @@ void OptionsHandler::setVerbosity(std::string option, int value) } void OptionsHandler::increaseVerbosity(std::string option) { - options::verbosity.set(options::verbosity() + 1); + Options::current().set(options::verbosity, options::verbosity() + 1); setVerbosity(option, options::verbosity()); } void OptionsHandler::decreaseVerbosity(std::string option) { - options::verbosity.set(options::verbosity() - 1); + Options::current().set(options::verbosity, options::verbosity() - 1); setVerbosity(option, options::verbosity()); } diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index f70c1ce3b..6ad537240 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -179,7 +179,7 @@ std::string Options::getBinaryName() const{ } std::ostream* Options::currentGetOut() { - return current()->getOut(); + return current().getOut(); } diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index f24f83b2b..4493f6094 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -408,7 +408,7 @@ std::vector Options::parseOptions(Options* options, options->d_holder->binary_name = std::string(progName); std::vector nonoptions; - parseOptionsRecursive(options, argc, argv, &nonoptions); + options->parseOptionsRecursive(argc, argv, &nonoptions); if(Debug.isOn("options")){ for(std::vector::const_iterator i = nonoptions.begin(), iend = nonoptions.end(); i != iend; ++i){ @@ -419,8 +419,7 @@ std::vector Options::parseOptions(Options* options, return nonoptions; } -void Options::parseOptionsRecursive(Options* options, - int argc, +void Options::parseOptionsRecursive(int argc, char* argv[], std::vector* nonoptions) { @@ -434,9 +433,6 @@ void Options::parseOptionsRecursive(Options* options, } } - // Having this synonym simplifies the generation code in mkoptions. - options::OptionsHandler* handler = options->d_handler; - // Reset getopt(), in the case of multiple calls to parseOptions(). // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. optind = 0; @@ -597,7 +593,6 @@ void Options::setOptionInternal(const std::string& key, const std::string& optionarg) { options::OptionsHandler* handler = d_handler; - Options* options = this; ${setoption_handlers}$ throw UnrecognizedOptionException(key); } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 19d14eb09..927fd1d13 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -127,25 +127,31 @@ void Printer::toStream(std::ostream& out, const SkolemList& sks) const Printer* Printer::getPrinter(OutputLanguage lang) { - if(lang == language::output::LANG_AUTO) { - // Infer the language to use for output. - // - // Options can be null in certain circumstances (e.g., when printing - // the singleton "null" expr. So we guard against segfault - if(not Options::isCurrentNull()) { - if(options::outputLanguage.wasSetByUser()) { - lang = options::outputLanguage(); + if (lang == language::output::LANG_AUTO) + { + // Infer the language to use for output. + // + // Options can be null in certain circumstances (e.g., when printing + // the singleton "null" expr. So we guard against segfault + if (not Options::isCurrentNull()) + { + if (Options::current().wasSetByUser(options::outputLanguage)) + { + lang = options::outputLanguage(); + } + if (lang == language::output::LANG_AUTO + && Options::current().wasSetByUser(options::inputLanguage)) + { + lang = language::toOutputLanguage(options::inputLanguage()); + } + } + if (lang == language::output::LANG_AUTO) + { + lang = language::output::LANG_SMTLIB_V2_6; // default } - if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) { - lang = language::toOutputLanguage(options::inputLanguage()); - } - } - if (lang == language::output::LANG_AUTO) - { - lang = language::output::LANG_SMTLIB_V2_6; // default - } } - if(d_printers[lang] == NULL) { + if (d_printers[lang] == nullptr) + { d_printers[lang] = makePrinter(lang); } return d_printers[lang].get(); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index e8179c5fe..74cbadfc2 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -76,7 +76,7 @@ SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy, n_touched(0) { if(options::minisatUseElim() && - options::minisatUseElim.wasSetByUser() && + Options::current().wasSetByUser(options::minisatUseElim) && enableIncremental) { WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl; } diff --git a/src/smt/env.h b/src/smt/env.h index 209b6f3e7..12e0983cb 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -87,6 +87,12 @@ class Env /** Get a pointer to the underlying dump manager. */ smt::DumpManager* getDumpManager(); + template + const auto& getOption(Opt opt) const + { + return d_options[opt]; + } + /** Get the options object (const version only) owned by this Env. */ const Options& getOptions() const; diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index 31bcc5f2f..b2f02b34d 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -90,7 +90,7 @@ ManagedRegularOutputChannel::~ManagedRegularOutputChannel() { // to null_os. Consult RegularOutputChannelListener for the list of // channels. if(options::err() == getManagedOstream()){ - options::err.set(&null_os); + Options::current().set(options::err, &null_os); } } @@ -114,7 +114,7 @@ ManagedDiagnosticOutputChannel::~ManagedDiagnosticOutputChannel() { // to null_os. Consult DiagnosticOutputChannelListener for the list of // channels. if(options::err() == getManagedOstream()){ - options::err.set(&null_os); + Options::current().set(options::err, &null_os); } if(Debug.getStreamPointer() == getManagedOstream()) { diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index c84854992..05bad2727 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -33,31 +33,31 @@ OptionsManager::OptionsManager(Options* opts) : d_options(opts) // set options that must take effect immediately if (opts->wasSetByUser(options::defaultExprDepth)) { - notifySetOption(options::defaultExprDepth.getName()); + notifySetOption(options::defaultExprDepth.name); } if (opts->wasSetByUser(options::defaultDagThresh)) { - notifySetOption(options::defaultDagThresh.getName()); + notifySetOption(options::defaultDagThresh.name); } if (opts->wasSetByUser(options::dumpModeString)) { - notifySetOption(options::dumpModeString.getName()); + notifySetOption(options::dumpModeString.name); } if (opts->wasSetByUser(options::printSuccess)) { - notifySetOption(options::printSuccess.getName()); + notifySetOption(options::printSuccess.name); } if (opts->wasSetByUser(options::diagnosticChannelName)) { - notifySetOption(options::diagnosticChannelName.getName()); + notifySetOption(options::diagnosticChannelName.name); } if (opts->wasSetByUser(options::regularChannelName)) { - notifySetOption(options::regularChannelName.getName()); + notifySetOption(options::regularChannelName.name); } if (opts->wasSetByUser(options::dumpToFileName)) { - notifySetOption(options::dumpToFileName.getName()); + notifySetOption(options::dumpToFileName.name); } // set this as a listener to be notified of options changes from now on opts->setListener(this); @@ -69,7 +69,7 @@ void OptionsManager::notifySetOption(const std::string& key) { Trace("smt") << "SmtEnginePrivate::notifySetOption(" << key << ")" << std::endl; - if (key == options::defaultExprDepth.getName()) + if (key == options::defaultExprDepth.name) { int depth = (*d_options)[options::defaultExprDepth]; Debug.getStream() << expr::ExprSetDepth(depth); @@ -80,7 +80,7 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << expr::ExprSetDepth(depth); // intentionally exclude Dump stream from this list } - else if (key == options::defaultDagThresh.getName()) + else if (key == options::defaultDagThresh.name) { int dag = (*d_options)[options::defaultDagThresh]; Debug.getStream() << expr::ExprDag(dag); @@ -91,12 +91,12 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << expr::ExprDag(dag); Dump.getStream() << expr::ExprDag(dag); } - else if (key == options::dumpModeString.getName()) + else if (key == options::dumpModeString.name) { const std::string& value = (*d_options)[options::dumpModeString]; Dump.setDumpFromString(value); } - else if (key == options::printSuccess.getName()) + else if (key == options::printSuccess.name) { bool value = (*d_options)[options::printSuccess]; Debug.getStream() << Command::printsuccess(value); @@ -107,15 +107,15 @@ void OptionsManager::notifySetOption(const std::string& key) Warning.getStream() << Command::printsuccess(value); *options::out() << Command::printsuccess(value); } - else if (key == options::regularChannelName.getName()) + else if (key == options::regularChannelName.name) { d_managedRegularChannel.set(options::regularChannelName()); } - else if (key == options::diagnosticChannelName.getName()) + else if (key == options::diagnosticChannelName.name) { d_managedDiagnosticChannel.set(options::diagnosticChannelName()); } - else if (key == options::dumpToFileName.getName()) + else if (key == options::dumpToFileName.name) { d_managedDumpChannel.set(options::dumpToFileName()); } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 047dbfea6..ed5d986be 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -49,84 +49,85 @@ namespace smt { void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { + Options& opts = Options::current(); // implied options if (options::debugCheckModels()) { - options::checkModels.set(true); + opts.set(options::checkModels, true); } if (options::checkModels() || options::dumpModels()) { - options::produceModels.set(true); + opts.set(options::produceModels, true); } if (options::checkModels()) { - options::produceAssignments.set(true); + opts.set(options::produceAssignments, true); } // unsat cores and proofs shenanigans if (options::dumpUnsatCoresFull()) { - options::dumpUnsatCores.set(true); + opts.set(options::dumpUnsatCores, true); } if (options::checkUnsatCores() || options::dumpUnsatCores() || options::unsatAssumptions() || options::unsatCoresMode() != options::UnsatCoresMode::OFF) { - options::unsatCores.set(true); + opts.set(options::unsatCores, true); } if (options::unsatCores() && options::unsatCoresMode() == options::UnsatCoresMode::OFF) { - if (options::unsatCoresMode.wasSetByUser()) + if (opts.wasSetByUser(options::unsatCoresMode)) { Notice() << "Overriding OFF unsat-core mode since cores were requested..\n"; } - options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF); + opts.set(options::unsatCoresMode, options::UnsatCoresMode::OLD_PROOF); } if (options::checkProofs() || options::dumpProofs()) { - options::produceProofs.set(true); + opts.set(options::produceProofs, true); } if (options::produceProofs() && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) { - if (options::unsatCoresMode.wasSetByUser()) + if (opts.wasSetByUser(options::unsatCoresMode)) { Notice() << "Forcing full-proof mode for unsat cores mode since proofs " "were requested.\n"; } // enable unsat cores, because they are available as a consequence of proofs - options::unsatCores.set(true); - options::unsatCoresMode.set(options::UnsatCoresMode::FULL_PROOF); + opts.set(options::unsatCores, true); + opts.set(options::unsatCoresMode, options::UnsatCoresMode::FULL_PROOF); } // set proofs on if not yet set if (options::unsatCores() && !options::produceProofs() && options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF) { - if (options::produceProofs.wasSetByUser()) + if (opts.wasSetByUser(options::produceProofs)) { Notice() << "Forcing proof production since new unsat cores were requested.\n"; } - options::produceProofs.set(true); + opts.set(options::produceProofs, true); } // if unsat cores are disabled, then unsat cores mode should be OFF Assert(options::unsatCores() == (options::unsatCoresMode() != options::UnsatCoresMode::OFF)); - if (options::bitvectorAigSimplifications.wasSetByUser()) + if (opts.wasSetByUser(options::bitvectorAigSimplifications)) { Notice() << "SmtEngine: setting bitvectorAig" << std::endl; - options::bitvectorAig.set(true); + opts.set(options::bitvectorAig, true); } - if (options::bitvectorAlgebraicBudget.wasSetByUser()) + if (opts.wasSetByUser(options::bitvectorAlgebraicBudget)) { Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl; - options::bitvectorAlgebraicSolver.set(true); + opts.set(options::bitvectorAlgebraicSolver, true); } bool isSygus = language::isInputLangSygus(options::inputLanguage()); @@ -138,8 +139,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && (logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_UF))) { - if (options::bitblastMode.wasSetByUser() - || options::produceModels.wasSetByUser()) + if (opts.wasSetByUser(options::bitblastMode) + || opts.wasSetByUser(options::produceModels)) { throw OptionException(std::string( "Eager bit-blasting currently does not support model generation " @@ -148,11 +149,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } Notice() << "SmtEngine: setting bit-blast mode to lazy to support model" << "generation" << std::endl; - options::bitblastMode.set(options::BitblastMode::LAZY); + opts.set(options::bitblastMode, options::BitblastMode::LAZY); } else if (!options::incrementalSolving()) { - options::ackermann.set(true); + opts.set(options::ackermann, true); } if (options::incrementalSolving() && !logic.isPure(THEORY_BV)) @@ -164,7 +165,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Force lazy solver since we don't handle EAGER_ATOMS in the // BVSolver::BITBLAST solver. - options::bvSolver.set(options::BVSolver::LAZY); + opts.set(options::bvSolver, options::BVSolver::LAZY); } /* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers @@ -172,14 +173,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::bvSolver() == options::BVSolver::SIMPLE || options::bvSolver() == options::BVSolver::BITBLAST) { - options::bvLazyReduceExtf.set(false); - options::bvLazyRewriteExtf.set(false); + opts.set(options::bvLazyReduceExtf, false); + opts.set(options::bvLazyRewriteExtf, false); } /* Disable bit-level propagation by default for the BITBLAST solver. */ if (options::bvSolver() == options::BVSolver::BITBLAST) { - options::bitvectorPropagate.set(false); + opts.set(options::bitvectorPropagate, false); } if (options::solveIntAsBV() > 0) @@ -232,14 +233,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && (logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_UF))) { - if (options::produceModels.wasSetByUser()) + if (opts.wasSetByUser(options::produceModels)) { throw OptionException(std::string( "Ackermannization currently does not support model generation.")); } Notice() << "SmtEngine: turn off ackermannization to support model" << "generation" << std::endl; - options::ackermann.set(false); + opts.set(options::ackermann, false); } if (options::ackermann()) @@ -275,9 +276,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // this by default. if (options::doITESimp()) { - if (!options::earlyIteRemoval.wasSetByUser()) + if (!opts.wasSetByUser(options::earlyIteRemoval)) { - options::earlyIteRemoval.set(true); + opts.set(options::earlyIteRemoval, true); } } @@ -288,7 +289,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { // If the user explicitly set a logic that includes strings, but is not // the generic "ALL" logic, then enable stringsExp. - options::stringExp.set(true); + opts.set(options::stringExp, true); } if (options::stringExp() || !options::stringLazyPreproc()) { @@ -302,9 +303,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << std::endl; } // We require bounded quantifier handling. - if (!options::fmfBound.wasSetByUser()) + if (!opts.wasSetByUser(options::fmfBound)) { - options::fmfBound.set(true); + opts.set(options::fmfBound, true); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } // Note we allow E-matching by default to support combinations of sequences @@ -325,9 +326,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) { // no fine-graininess - if (!options::proofGranularityMode.wasSetByUser()) + if (!opts.wasSetByUser(options::proofGranularityMode)) { - options::proofGranularityMode.set(options::ProofGranularityMode::OFF); + opts.set(options::proofGranularityMode, options::ProofGranularityMode::OFF); } } @@ -340,9 +341,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic.lock(); } // Allows to answer sat more often by default. - if (!options::fmfBound.wasSetByUser()) + if (!opts.wasSetByUser(options::fmfBound)) { - options::fmfBound.set(true); + opts.set(options::fmfBound, true); Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; } } @@ -383,24 +384,24 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // if we requiring disabling proofs, disable them now if (disableProofs && options::produceProofs()) { - options::unsatCores.set(false); - options::unsatCoresMode.set(options::UnsatCoresMode::OFF); + opts.set(options::unsatCores, false); + opts.set(options::unsatCoresMode, options::UnsatCoresMode::OFF); if (options::produceProofs()) { Notice() << "SmtEngine: turning off produce-proofs." << std::endl; } - options::produceProofs.set(false); - options::checkProofs.set(false); - options::proofEagerChecking.set(false); + opts.set(options::produceProofs, false); + opts.set(options::checkProofs, false); + opts.set(options::proofEagerChecking, false); } // sygus core connective requires unsat cores if (options::sygusCoreConnective()) { - options::unsatCores.set(true); + opts.set(options::unsatCores, true); if (options::unsatCoresMode() == options::UnsatCoresMode::OFF) { - options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF); + opts.set(options::unsatCoresMode, options::UnsatCoresMode::OLD_PROOF); } } @@ -414,7 +415,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { Notice() << "SmtEngine: turning on produce-assertions to support " << "option requiring assertions." << std::endl; - options::produceAssertions.set(true); + opts.set(options::produceAssertions, true); } // whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF @@ -429,7 +430,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::unconstrainedSimp()) { - if (options::unconstrainedSimp.wasSetByUser()) + if (opts.wasSetByUser(options::unconstrainedSimp)) { throw OptionException( "unconstrained simplification not supported with old unsat " @@ -438,13 +439,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Notice() << "SmtEngine: turning off unconstrained simplification to " "support old unsat cores/incremental solving" << std::endl; - options::unconstrainedSimp.set(false); + opts.set(options::unconstrainedSimp, false); } } else { // Turn on unconstrained simplification for QF_AUFBV - if (!options::unconstrainedSimp.wasSetByUser()) + if (!opts.wasSetByUser(options::unconstrainedSimp)) { bool uncSimp = !logic.isQuantified() && !options::produceModels() && !options::produceAssignments() @@ -454,7 +455,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && !logic.isTheoryEnabled(THEORY_ARITH); Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; - options::unconstrainedSimp.set(uncSimp); + opts.set(options::unconstrainedSimp, uncSimp); } } @@ -462,7 +463,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::sygusInference()) { - if (options::sygusInference.wasSetByUser()) + if (opts.wasSetByUser(options::sygusInference)) { throw OptionException( "sygus inference not supported with incremental solving"); @@ -470,7 +471,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Notice() << "SmtEngine: turning off sygus inference to support " "incremental solving" << std::endl; - options::sygusInference.set(false); + opts.set(options::sygusInference, false); } } @@ -482,7 +483,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) * Therefore, we enable bv-to-bool, which runs before * the translation to integers. */ - options::bitvectorToBool.set(true); + opts.set(options::bitvectorToBool, true); } // Disable options incompatible with unsat cores or output an error if enabled @@ -491,7 +492,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::simplificationMode() != options::SimplificationMode::NONE) { - if (options::simplificationMode.wasSetByUser()) + if (opts.wasSetByUser(options::simplificationMode)) { throw OptionException( "simplification not supported with old unsat cores"); @@ -499,101 +500,101 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Notice() << "SmtEngine: turning off simplification to support unsat " "cores" << std::endl; - options::simplificationMode.set(options::SimplificationMode::NONE); + opts.set(options::simplificationMode, options::SimplificationMode::NONE); } if (options::pbRewrites()) { - if (options::pbRewrites.wasSetByUser()) + if (opts.wasSetByUser(options::pbRewrites)) { throw OptionException( "pseudoboolean rewrites not supported with old unsat cores"); } Notice() << "SmtEngine: turning off pseudoboolean rewrites to support " "old unsat cores\n"; - options::pbRewrites.set(false); + opts.set(options::pbRewrites, false); } if (options::sortInference()) { - if (options::sortInference.wasSetByUser()) + if (opts.wasSetByUser(options::sortInference)) { throw OptionException( "sort inference not supported with old unsat cores"); } Notice() << "SmtEngine: turning off sort inference to support old unsat " "cores\n"; - options::sortInference.set(false); + opts.set(options::sortInference, false); } if (options::preSkolemQuant()) { - if (options::preSkolemQuant.wasSetByUser()) + if (opts.wasSetByUser(options::preSkolemQuant)) { throw OptionException( "pre-skolemization not supported with old unsat cores"); } Notice() << "SmtEngine: turning off pre-skolemization to support old " "unsat cores\n"; - options::preSkolemQuant.set(false); + opts.set(options::preSkolemQuant, false); } if (options::bitvectorToBool()) { - if (options::bitvectorToBool.wasSetByUser()) + if (opts.wasSetByUser(options::bitvectorToBool)) { throw OptionException("bv-to-bool not supported with old unsat cores"); } Notice() << "SmtEngine: turning off bitvector-to-bool to support old " "unsat cores\n"; - options::bitvectorToBool.set(false); + opts.set(options::bitvectorToBool, false); } if (options::boolToBitvector() != options::BoolToBVMode::OFF) { - if (options::boolToBitvector.wasSetByUser()) + if (opts.wasSetByUser(options::boolToBitvector)) { throw OptionException( "bool-to-bv != off not supported with old unsat cores"); } Notice() << "SmtEngine: turning off bool-to-bv to support old unsat cores\n"; - options::boolToBitvector.set(options::BoolToBVMode::OFF); + opts.set(options::boolToBitvector, options::BoolToBVMode::OFF); } if (options::bvIntroducePow2()) { - if (options::bvIntroducePow2.wasSetByUser()) + if (opts.wasSetByUser(options::bvIntroducePow2)) { throw OptionException( "bv-intro-pow2 not supported with old unsat cores"); } Notice() << "SmtEngine: turning off bv-intro-pow2 to support old unsat cores"; - options::bvIntroducePow2.set(false); + opts.set(options::bvIntroducePow2, false); } if (options::repeatSimp()) { - if (options::repeatSimp.wasSetByUser()) + if (opts.wasSetByUser(options::repeatSimp)) { throw OptionException("repeat-simp not supported with old unsat cores"); } Notice() << "SmtEngine: turning off repeat-simp to support old unsat cores\n"; - options::repeatSimp.set(false); + opts.set(options::repeatSimp, false); } if (options::globalNegate()) { - if (options::globalNegate.wasSetByUser()) + if (opts.wasSetByUser(options::globalNegate)) { throw OptionException( "global-negate not supported with old unsat cores"); } Notice() << "SmtEngine: turning off global-negate to support old unsat " "cores\n"; - options::globalNegate.set(false); + opts.set(options::globalNegate, false); } if (options::bitvectorAig()) @@ -609,16 +610,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) else { // by default, nonclausal simplification is off for QF_SAT - if (!options::simplificationMode.wasSetByUser()) + if (!opts.wasSetByUser(options::simplificationMode)) { bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified(); Trace("smt") << "setting simplification mode to <" << logic.getLogicString() << "> " << (!qf_sat) << std::endl; // simplification=none works better for SMT LIB benchmarks with - // quantifiers, not others options::simplificationMode.set(qf_sat || + // quantifiers, not others opts.set(options::simplificationMode, qf_sat || // quantifiers ? options::SimplificationMode::NONE : // options::SimplificationMode::BATCH); - options::simplificationMode.set(qf_sat + opts.set(options::simplificationMode, qf_sat ? options::SimplificationMode::NONE : options::SimplificationMode::BATCH); } @@ -628,7 +629,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::boolToBitvector() != options::BoolToBVMode::OFF) { - if (options::boolToBitvector.wasSetByUser()) + if (opts.wasSetByUser(options::boolToBitvector)) { throw OptionException( "bool-to-bv != off not supported with CBQI BV for quantified " @@ -636,7 +637,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" << std::endl; - options::boolToBitvector.set(options::BoolToBVMode::OFF); + opts.set(options::boolToBitvector, options::BoolToBVMode::OFF); } } @@ -646,7 +647,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || usesSygus)) { Notice() << "SmtEngine: turning on produce-models" << std::endl; - options::produceModels.set(true); + opts.set(options::produceModels, true); } ///////////////////////////////////////////////////////////////////////////// @@ -687,7 +688,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) needsUf = true; } else if (options::preSkolemQuantNested() - && options::preSkolemQuantNested.wasSetByUser()) + && opts.wasSetByUser(options::preSkolemQuantNested)) { // if pre-skolem nested is explictly set, then we require UF. If it is // not explicitly set, it is disabled below if UF is not present. @@ -742,7 +743,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) ///////////////////////////////////////////////////////////////////////////// // Set the options for the theoryOf - if (!options::theoryOfMode.wasSetByUser()) + if (!opts.wasSetByUser(options::theoryOfMode)) { if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV) && !logic.isTheoryEnabled(THEORY_STRINGS) @@ -752,18 +753,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && !logic.isQuantified())) { Trace("smt") << "setting theoryof-mode to term-based" << std::endl; - options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED); + opts.set(options::theoryOfMode, options::TheoryOfMode::THEORY_OF_TERM_BASED); } } // by default, symmetry breaker is on only for non-incremental QF_UF - if (!options::ufSymmetryBreaker.wasSetByUser()) + if (!opts.wasSetByUser(options::ufSymmetryBreaker)) { bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified() && !options::incrementalSolving() && !safeUnsatCores; Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << std::endl; - options::ufSymmetryBreaker.set(qf_uf_noinc); + opts.set(options::ufSymmetryBreaker, qf_uf_noinc); } // If in arrays, set the UF handler to arrays @@ -779,7 +780,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Theory::setUninterpretedSortOwner(THEORY_UF); } - if (!options::simplifyWithCareEnabled.wasSetByUser()) + if (!opts.wasSetByUser(options::simplifyWithCareEnabled)) { bool qf_aufbv = !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS) @@ -788,10 +789,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) bool withCare = qf_aufbv; Trace("smt") << "setting ite simplify with care to " << withCare << std::endl; - options::simplifyWithCareEnabled.set(withCare); + opts.set(options::simplifyWithCareEnabled, withCare); } // Turn off array eager index splitting for QF_AUFLIA - if (!options::arraysEagerIndexSplitting.wasSetByUser()) + if (!opts.wasSetByUser(options::arraysEagerIndexSplitting)) { if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS) && logic.isTheoryEnabled(THEORY_UF) @@ -799,11 +800,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { Trace("smt") << "setting array eager index splitting to false" << std::endl; - options::arraysEagerIndexSplitting.set(false); + opts.set(options::arraysEagerIndexSplitting, false); } } // Turn on multiple-pass non-clausal simplification for QF_AUFBV - if (!options::repeatSimp.wasSetByUser()) + if (!opts.wasSetByUser(options::repeatSimp)) { bool repeatSimp = !logic.isQuantified() && (logic.isTheoryEnabled(THEORY_ARRAYS) @@ -812,40 +813,40 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) && !safeUnsatCores; Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; - options::repeatSimp.set(repeatSimp); + opts.set(options::repeatSimp, repeatSimp); } if (options::boolToBitvector() == options::BoolToBVMode::ALL && !logic.isTheoryEnabled(THEORY_BV)) { - if (options::boolToBitvector.wasSetByUser()) + if (opts.wasSetByUser(options::boolToBitvector)) { throw OptionException( "bool-to-bv=all not supported for non-bitvector logics."); } Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: " << logic.getLogicString() << std::endl; - options::boolToBitvector.set(options::BoolToBVMode::OFF); + opts.set(options::boolToBitvector, options::BoolToBVMode::OFF); } - if (!options::bvEagerExplanations.wasSetByUser() + if (!opts.wasSetByUser(options::bvEagerExplanations) && logic.isTheoryEnabled(THEORY_ARRAYS) && logic.isTheoryEnabled(THEORY_BV)) { Trace("smt") << "enabling eager bit-vector explanations " << std::endl; - options::bvEagerExplanations.set(true); + opts.set(options::bvEagerExplanations, true); } // Turn on arith rewrite equalities only for pure arithmetic - if (!options::arithRewriteEq.wasSetByUser()) + if (!opts.wasSetByUser(options::arithRewriteEq)) { bool arithRewriteEq = logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified(); Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl; - options::arithRewriteEq.set(arithRewriteEq); + opts.set(options::arithRewriteEq, arithRewriteEq); } - if (!options::arithHeuristicPivots.wasSetByUser()) + if (!opts.wasSetByUser(options::arithHeuristicPivots)) { int16_t heuristicPivots = 5; if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) @@ -861,9 +862,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots << std::endl; - options::arithHeuristicPivots.set(heuristicPivots); + opts.set(options::arithHeuristicPivots, heuristicPivots); } - if (!options::arithPivotThreshold.wasSetByUser()) + if (!opts.wasSetByUser(options::arithPivotThreshold)) { uint16_t pivotThreshold = 2; if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) @@ -875,9 +876,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold << std::endl; - options::arithPivotThreshold.set(pivotThreshold); + opts.set(options::arithPivotThreshold, pivotThreshold); } - if (!options::arithStandardCheckVarOrderPivots.wasSetByUser()) + if (!opts.wasSetByUser(options::arithStandardCheckVarOrderPivots)) { int16_t varOrderPivots = -1; if (logic.isPure(THEORY_ARITH) && !logic.isQuantified()) @@ -886,20 +887,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } Trace("smt") << "setting arithStandardCheckVarOrderPivots " << varOrderPivots << std::endl; - options::arithStandardCheckVarOrderPivots.set(varOrderPivots); + opts.set(options::arithStandardCheckVarOrderPivots, varOrderPivots); } if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed()) { - if (!options::nlExtTangentPlanesInterleave.wasSetByUser()) + if (!opts.wasSetByUser(options::nlExtTangentPlanesInterleave)) { Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << std::endl; - options::nlExtTangentPlanesInterleave.set(true); + opts.set(options::nlExtTangentPlanesInterleave, true); } } // Set decision mode based on logic (if not set by user) - if (!options::decisionMode.wasSetByUser()) + if (!opts.wasSetByUser(options::decisionMode)) { options::DecisionMode decMode = // anything that uses sygus uses internal @@ -954,50 +955,50 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) : false); Trace("smt") << "setting decision mode to " << decMode << std::endl; - options::decisionMode.set(decMode); - options::decisionStopOnly.set(stoponly); + opts.set(options::decisionMode, decMode); + opts.set(options::decisionStopOnly, stoponly); } if (options::incrementalSolving()) { // disable modes not supported by incremental - options::sortInference.set(false); - options::ufssFairnessMonotone.set(false); - options::globalNegate.set(false); - options::bvAbstraction.set(false); - options::arithMLTrick.set(false); + opts.set(options::sortInference, false); + opts.set(options::ufssFairnessMonotone, false); + opts.set(options::globalNegate, false); + opts.set(options::bvAbstraction, false); + opts.set(options::arithMLTrick, false); } if (logic.hasCardinalityConstraints()) { // must have finite model finding on - options::finiteModelFind.set(true); + opts.set(options::finiteModelFind, true); } if (options::instMaxLevel() != -1) { Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << std::endl; - options::cegqi.set(false); + opts.set(options::cegqi, false); } - if ((options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy()) - || (options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt())) + if ((opts.wasSetByUser(options::fmfBoundLazy) && options::fmfBoundLazy()) + || (opts.wasSetByUser(options::fmfBoundInt) && options::fmfBoundInt())) { - options::fmfBound.set(true); + opts.set(options::fmfBound, true); } // now have determined whether fmfBoundInt is on/off // apply fmfBoundInt options if (options::fmfBound()) { - if (!options::mbqiMode.wasSetByUser() + if (!opts.wasSetByUser(options::mbqiMode) || (options::mbqiMode() != options::MbqiMode::NONE && options::mbqiMode() != options::MbqiMode::FMC)) { // if bounded integers are set, use no MBQI by default - options::mbqiMode.set(options::MbqiMode::NONE); + opts.set(options::mbqiMode, options::MbqiMode::NONE); } - if (!options::prenexQuant.wasSetByUser()) + if (!opts.wasSetByUser(options::prenexQuant)) { - options::prenexQuant.set(options::PrenexQuantMode::NONE); + opts.set(options::prenexQuant, options::PrenexQuantMode::NONE); } } if (options::ufHo()) @@ -1006,37 +1007,37 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // cannot be used if (options::mbqiMode() != options::MbqiMode::NONE) { - options::mbqiMode.set(options::MbqiMode::NONE); + opts.set(options::mbqiMode, options::MbqiMode::NONE); } - if (!options::hoElimStoreAx.wasSetByUser()) + if (!opts.wasSetByUser(options::hoElimStoreAx)) { // by default, use store axioms only if --ho-elim is set - options::hoElimStoreAx.set(options::hoElim()); + opts.set(options::hoElimStoreAx, options::hoElim()); } if (!options::assignFunctionValues()) { // must assign function values - options::assignFunctionValues.set(true); + opts.set(options::assignFunctionValues, true); } // Cannot use macros, since lambda lifting and macro elimination are inverse // operations. if (options::macrosQuant()) { - options::macrosQuant.set(false); + opts.set(options::macrosQuant, false); } } if (options::fmfFunWellDefinedRelevant()) { - if (!options::fmfFunWellDefined.wasSetByUser()) + if (!opts.wasSetByUser(options::fmfFunWellDefined)) { - options::fmfFunWellDefined.set(true); + opts.set(options::fmfFunWellDefined, true); } } if (options::fmfFunWellDefined()) { - if (!options::finiteModelFind.wasSetByUser()) + if (!opts.wasSetByUser(options::finiteModelFind)) { - options::finiteModelFind.set(true); + opts.set(options::finiteModelFind, true); } } @@ -1045,20 +1046,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::finiteModelFind()) { // apply conservative quantifiers splitting - if (!options::quantDynamicSplit.wasSetByUser()) + if (!opts.wasSetByUser(options::quantDynamicSplit)) { - options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT); + opts.set(options::quantDynamicSplit, options::QuantDSplitMode::DEFAULT); } - if (!options::eMatching.wasSetByUser()) + if (!opts.wasSetByUser(options::eMatching)) { - options::eMatching.set(options::fmfInstEngine()); + opts.set(options::eMatching, options::fmfInstEngine()); } - if (!options::instWhenMode.wasSetByUser()) + if (!opts.wasSetByUser(options::instWhenMode)) { // instantiate only on last call if (options::eMatching()) { - options::instWhenMode.set(options::InstWhenMode::LAST_CALL); + opts.set(options::instWhenMode, options::InstWhenMode::LAST_CALL); } } } @@ -1071,71 +1072,71 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { Trace("smt") << "turning on sygus" << std::endl; } - options::sygus.set(true); + opts.set(options::sygus, true); // must use Ferrante/Rackoff for real arithmetic - if (!options::cegqiMidpoint.wasSetByUser()) + if (!opts.wasSetByUser(options::cegqiMidpoint)) { - options::cegqiMidpoint.set(true); + opts.set(options::cegqiMidpoint, true); } // must disable cegqi-bv since it may introduce witness terms, which // cannot appear in synthesis solutions - if (!options::cegqiBv.wasSetByUser()) + if (!opts.wasSetByUser(options::cegqiBv)) { - options::cegqiBv.set(false); + opts.set(options::cegqiBv, false); } if (options::sygusRepairConst()) { - if (!options::cegqi.wasSetByUser()) + if (!opts.wasSetByUser(options::cegqi)) { - options::cegqi.set(true); + opts.set(options::cegqi, true); } } if (options::sygusInference()) { // optimization: apply preskolemization, makes it succeed more often - if (!options::preSkolemQuant.wasSetByUser()) + if (!opts.wasSetByUser(options::preSkolemQuant)) { - options::preSkolemQuant.set(true); + opts.set(options::preSkolemQuant, true); } - if (!options::preSkolemQuantNested.wasSetByUser()) + if (!opts.wasSetByUser(options::preSkolemQuantNested)) { - options::preSkolemQuantNested.set(true); + opts.set(options::preSkolemQuantNested, true); } } // counterexample-guided instantiation for sygus - if (!options::cegqiSingleInvMode.wasSetByUser()) + if (!opts.wasSetByUser(options::cegqiSingleInvMode)) { - options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::USE); + opts.set(options::cegqiSingleInvMode, options::CegqiSingleInvMode::USE); } - if (!options::quantConflictFind.wasSetByUser()) + if (!opts.wasSetByUser(options::quantConflictFind)) { - options::quantConflictFind.set(false); + opts.set(options::quantConflictFind, false); } - if (!options::instNoEntail.wasSetByUser()) + if (!opts.wasSetByUser(options::instNoEntail)) { - options::instNoEntail.set(false); + opts.set(options::instNoEntail, false); } - if (!options::cegqiFullEffort.wasSetByUser()) + if (!opts.wasSetByUser(options::cegqiFullEffort)) { // should use full effort cbqi for single invocation and repair const - options::cegqiFullEffort.set(true); + opts.set(options::cegqiFullEffort, true); } if (options::sygusRew()) { - options::sygusRewSynth.set(true); - options::sygusRewVerify.set(true); + opts.set(options::sygusRewSynth, true); + opts.set(options::sygusRewVerify, true); } if (options::sygusRewSynthInput()) { // If we are using synthesis rewrite rules from input, we use // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for // details on this technique. - options::sygusRewSynth.set(true); + opts.set(options::sygusRewSynth, true); // we should not use the extended rewriter, since we are interested // in rewrites that are not in the main rewriter - if (!options::sygusExtRew.wasSetByUser()) + if (!opts.wasSetByUser(options::sygusExtRew)) { - options::sygusExtRew.set(false); + opts.set(options::sygusExtRew, false); } } // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm @@ -1147,9 +1148,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::produceAbducts()) { // if doing abduction, we should filter strong solutions - if (!options::sygusFilterSolMode.wasSetByUser()) + if (!opts.wasSetByUser(options::sygusFilterSolMode)) { - options::sygusFilterSolMode.set(options::SygusFilterSolMode::STRONG); + opts.set(options::sygusFilterSolMode, options::SygusFilterSolMode::STRONG); } // we must use basic sygus algorithms, since e.g. we require checking // a sygus side condition for consistency with axioms. @@ -1159,7 +1160,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || options::sygusQueryGen()) { // rewrite rule synthesis implies that sygus stream must be true - options::sygusStream.set(true); + opts.set(options::sygusStream, true); } if (options::sygusStream() || options::incrementalSolving()) { @@ -1170,50 +1171,50 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Now, disable options for non-basic sygus algorithms, if necessary. if (reqBasicSygus) { - if (!options::sygusUnifPbe.wasSetByUser()) + if (!opts.wasSetByUser(options::sygusUnifPbe)) { - options::sygusUnifPbe.set(false); + opts.set(options::sygusUnifPbe, false); } - if (options::sygusUnifPi.wasSetByUser()) + if (opts.wasSetByUser(options::sygusUnifPi)) { - options::sygusUnifPi.set(options::SygusUnifPiMode::NONE); + opts.set(options::sygusUnifPi, options::SygusUnifPiMode::NONE); } - if (!options::sygusInvTemplMode.wasSetByUser()) + if (!opts.wasSetByUser(options::sygusInvTemplMode)) { - options::sygusInvTemplMode.set(options::SygusInvTemplMode::NONE); + opts.set(options::sygusInvTemplMode, options::SygusInvTemplMode::NONE); } - if (!options::cegqiSingleInvMode.wasSetByUser()) + if (!opts.wasSetByUser(options::cegqiSingleInvMode)) { - options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::NONE); + opts.set(options::cegqiSingleInvMode, options::CegqiSingleInvMode::NONE); } } - if (!options::dtRewriteErrorSel.wasSetByUser()) + if (!opts.wasSetByUser(options::dtRewriteErrorSel)) { - options::dtRewriteErrorSel.set(true); + opts.set(options::dtRewriteErrorSel, true); } // do not miniscope - if (!options::miniscopeQuant.wasSetByUser()) + if (!opts.wasSetByUser(options::miniscopeQuant)) { - options::miniscopeQuant.set(false); + opts.set(options::miniscopeQuant, false); } - if (!options::miniscopeQuantFreeVar.wasSetByUser()) + if (!opts.wasSetByUser(options::miniscopeQuantFreeVar)) { - options::miniscopeQuantFreeVar.set(false); + opts.set(options::miniscopeQuantFreeVar, false); } - if (!options::quantSplit.wasSetByUser()) + if (!opts.wasSetByUser(options::quantSplit)) { - options::quantSplit.set(false); + opts.set(options::quantSplit, false); } // do not do macros - if (!options::macrosQuant.wasSetByUser()) + if (!opts.wasSetByUser(options::macrosQuant)) { - options::macrosQuant.set(false); + opts.set(options::macrosQuant, false); } // use tangent planes by default, since we want to put effort into // the verification step for sygus queries with non-linear arithmetic - if (!options::nlExtTangentPlanes.wasSetByUser()) + if (!opts.wasSetByUser(options::nlExtTangentPlanes)) { - options::nlExtTangentPlanes.set(true); + opts.set(options::nlExtTangentPlanes, true); } } // counterexample-guided instantiation for non-sygus @@ -1225,16 +1226,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || logic.isTheoryEnabled(THEORY_FP))) || options::cegqiAll()) { - if (!options::cegqi.wasSetByUser()) + if (!opts.wasSetByUser(options::cegqi)) { - options::cegqi.set(true); + opts.set(options::cegqi, true); } // check whether we should apply full cbqi if (logic.isPure(THEORY_BV)) { - if (!options::cegqiFullEffort.wasSetByUser()) + if (!opts.wasSetByUser(options::cegqiFullEffort)) { - options::cegqiFullEffort.set(true); + opts.set(options::cegqiFullEffort, true); } } } @@ -1243,129 +1244,129 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::incrementalSolving()) { // cannot do nested quantifier elimination in incremental mode - options::cegqiNestedQE.set(false); + opts.set(options::cegqiNestedQE, false); } if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV)) { - if (!options::quantConflictFind.wasSetByUser()) + if (!opts.wasSetByUser(options::quantConflictFind)) { - options::quantConflictFind.set(false); + opts.set(options::quantConflictFind, false); } - if (!options::instNoEntail.wasSetByUser()) + if (!opts.wasSetByUser(options::instNoEntail)) { - options::instNoEntail.set(false); + opts.set(options::instNoEntail, false); } - if (!options::instWhenMode.wasSetByUser() && options::cegqiModel()) + if (!opts.wasSetByUser(options::instWhenMode) && options::cegqiModel()) { // only instantiation should happen at last call when model is avaiable - options::instWhenMode.set(options::InstWhenMode::LAST_CALL); + opts.set(options::instWhenMode, options::InstWhenMode::LAST_CALL); } } else { // only supported in pure arithmetic or pure BV - options::cegqiNestedQE.set(false); + opts.set(options::cegqiNestedQE, false); } if (options::globalNegate()) { - if (!options::prenexQuant.wasSetByUser()) + if (!opts.wasSetByUser(options::prenexQuant)) { - options::prenexQuant.set(options::PrenexQuantMode::NONE); + opts.set(options::prenexQuant, options::PrenexQuantMode::NONE); } } } // implied options... if (options::strictTriggers()) { - if (!options::userPatternsQuant.wasSetByUser()) + if (!opts.wasSetByUser(options::userPatternsQuant)) { - options::userPatternsQuant.set(options::UserPatMode::TRUST); + opts.set(options::userPatternsQuant, options::UserPatMode::TRUST); } } - if (options::qcfMode.wasSetByUser() || options::qcfTConstraint()) + if (opts.wasSetByUser(options::qcfMode) || options::qcfTConstraint()) { - options::quantConflictFind.set(true); + opts.set(options::quantConflictFind, true); } if (options::cegqiNestedQE()) { - options::prenexQuantUser.set(true); - if (!options::preSkolemQuant.wasSetByUser()) + opts.set(options::prenexQuantUser, true); + if (!opts.wasSetByUser(options::preSkolemQuant)) { - options::preSkolemQuant.set(true); + opts.set(options::preSkolemQuant, true); } } // for induction techniques if (options::quantInduction()) { - if (!options::dtStcInduction.wasSetByUser()) + if (!opts.wasSetByUser(options::dtStcInduction)) { - options::dtStcInduction.set(true); + opts.set(options::dtStcInduction, true); } - if (!options::intWfInduction.wasSetByUser()) + if (!opts.wasSetByUser(options::intWfInduction)) { - options::intWfInduction.set(true); + opts.set(options::intWfInduction, true); } } if (options::dtStcInduction()) { // try to remove ITEs from quantified formulas - if (!options::iteDtTesterSplitQuant.wasSetByUser()) + if (!opts.wasSetByUser(options::iteDtTesterSplitQuant)) { - options::iteDtTesterSplitQuant.set(true); + opts.set(options::iteDtTesterSplitQuant, true); } - if (!options::iteLiftQuant.wasSetByUser()) + if (!opts.wasSetByUser(options::iteLiftQuant)) { - options::iteLiftQuant.set(options::IteLiftQuantMode::ALL); + opts.set(options::iteLiftQuant, options::IteLiftQuantMode::ALL); } } if (options::intWfInduction()) { - if (!options::purifyTriggers.wasSetByUser()) + if (!opts.wasSetByUser(options::purifyTriggers)) { - options::purifyTriggers.set(true); + opts.set(options::purifyTriggers, true); } } if (options::conjectureNoFilter()) { - if (!options::conjectureFilterActiveTerms.wasSetByUser()) + if (!opts.wasSetByUser(options::conjectureFilterActiveTerms)) { - options::conjectureFilterActiveTerms.set(false); + opts.set(options::conjectureFilterActiveTerms, false); } - if (!options::conjectureFilterCanonical.wasSetByUser()) + if (!opts.wasSetByUser(options::conjectureFilterCanonical)) { - options::conjectureFilterCanonical.set(false); + opts.set(options::conjectureFilterCanonical, false); } - if (!options::conjectureFilterModel.wasSetByUser()) + if (!opts.wasSetByUser(options::conjectureFilterModel)) { - options::conjectureFilterModel.set(false); + opts.set(options::conjectureFilterModel, false); } } - if (options::conjectureGenPerRound.wasSetByUser()) + if (opts.wasSetByUser(options::conjectureGenPerRound)) { if (options::conjectureGenPerRound() > 0) { - options::conjectureGen.set(true); + opts.set(options::conjectureGen, true); } else { - options::conjectureGen.set(false); + opts.set(options::conjectureGen, false); } } // can't pre-skolemize nested quantifiers without UF theory if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant()) { - if (!options::preSkolemQuantNested.wasSetByUser()) + if (!opts.wasSetByUser(options::preSkolemQuantNested)) { - options::preSkolemQuantNested.set(false); + opts.set(options::preSkolemQuantNested, false); } } if (!logic.isTheoryEnabled(THEORY_DATATYPES)) { - options::quantDynamicSplit.set(options::QuantDSplitMode::NONE); + opts.set(options::quantDynamicSplit, options::QuantDSplitMode::NONE); } // until bugs 371,431 are fixed - if (!options::minisatUseElim.wasSetByUser()) + if (!opts.wasSetByUser(options::minisatUseElim)) { // cannot use minisat elimination for logics where a theory solver // introduces new literals into the search. This includes quantifiers @@ -1378,7 +1379,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || options::checkModels() || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) { - options::minisatUseElim.set(false); + opts.set(options::minisatUseElim, false); } } @@ -1387,14 +1388,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (!options::relevanceFilter()) { - if (options::relevanceFilter.wasSetByUser()) + if (opts.wasSetByUser(options::relevanceFilter)) { Warning() << "SmtEngine: turning on relevance filtering to support " "--nl-ext-rlv=" << options::nlRlvMode() << std::endl; } // must use relevance filtering techniques - options::relevanceFilter.set(true); + opts.set(options::relevanceFilter, true); } } @@ -1402,14 +1403,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::produceModels() || options::produceAssignments() || options::checkModels()) { - options::arraysOptimizeLinear.set(false); + opts.set(options::arraysOptimizeLinear, false); } if (!options::bitvectorEqualitySolver()) { if (options::bvLazyRewriteExtf()) { - if (options::bvLazyRewriteExtf.wasSetByUser()) + if (opts.wasSetByUser(options::bvLazyRewriteExtf)) { throw OptionException( "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set"); @@ -1418,21 +1419,21 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Trace("smt") << "disabling bvLazyRewriteExtf since equality solver is disabled" << std::endl; - options::bvLazyRewriteExtf.set(false); + opts.set(options::bvLazyRewriteExtf, false); } - if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser()) + if (options::stringFMF() && !opts.wasSetByUser(options::stringProcessLoopMode)) { Trace("smt") << "settting stringProcessLoopMode to 'simple' since " "--strings-fmf enabled" << std::endl; - options::stringProcessLoopMode.set(options::ProcessLoopMode::SIMPLE); + opts.set(options::stringProcessLoopMode, options::ProcessLoopMode::SIMPLE); } // !!! All options that require disabling models go here bool disableModels = false; std::string sOptNoModel; - if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) + if (opts.wasSetByUser(options::unconstrainedSimp) && options::unconstrainedSimp()) { disableModels = true; sOptNoModel = "unconstrained-simp"; @@ -1456,7 +1457,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { if (options::produceModels()) { - if (options::produceModels.wasSetByUser()) + if (opts.wasSetByUser(options::produceModels)) { std::stringstream ss; ss << "Cannot use " << sOptNoModel << " with model generation."; @@ -1464,11 +1465,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } Notice() << "SmtEngine: turning off produce-models to support " << sOptNoModel << std::endl; - options::produceModels.set(false); + opts.set(options::produceModels, false); } if (options::produceAssignments()) { - if (options::produceAssignments.wasSetByUser()) + if (opts.wasSetByUser(options::produceAssignments)) { std::stringstream ss; ss << "Cannot use " << sOptNoModel @@ -1477,11 +1478,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } Notice() << "SmtEngine: turning off produce-assignments to support " << sOptNoModel << std::endl; - options::produceAssignments.set(false); + opts.set(options::produceAssignments, false); } if (options::checkModels()) { - if (options::checkModels.wasSetByUser()) + if (opts.wasSetByUser(options::checkModels)) { std::stringstream ss; ss << "Cannot use " << sOptNoModel @@ -1490,7 +1491,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } Notice() << "SmtEngine: turning off check-models to support " << sOptNoModel << std::endl; - options::checkModels.set(false); + opts.set(options::checkModels, false); } } @@ -1508,16 +1509,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (logic == LogicInfo("QF_UFNRA")) { #ifdef CVC5_USE_POLY - if (!options::nlCad() && !options::nlCad.wasSetByUser()) + if (!options::nlCad() && !opts.wasSetByUser(options::nlCad)) { - options::nlCad.set(true); - if (!options::nlExt.wasSetByUser()) + opts.set(options::nlCad, true); + if (!opts.wasSetByUser(options::nlExt)) { - options::nlExt.set(false); + opts.set(options::nlExt, false); } - if (!options::nlRlvMode.wasSetByUser()) + if (!opts.wasSetByUser(options::nlRlvMode)) { - options::nlRlvMode.set(options::NlRlvMode::INTERLEAVE); + opts.set(options::nlRlvMode, options::NlRlvMode::INTERLEAVE); } } #endif @@ -1525,18 +1526,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) #ifndef CVC5_USE_POLY if (options::nlCad()) { - if (options::nlCad.wasSetByUser()) + if (opts.wasSetByUser(options::nlCad)) { std::stringstream ss; - ss << "Cannot use " << options::nlCad.getName() << " without configuring with --poly."; + ss << "Cannot use " << options::nlCad.name << " without configuring with --poly."; throw OptionException(ss.str()); } else { - Notice() << "Cannot use --" << options::nlCad.getName() + Notice() << "Cannot use --" << options::nlCad.name << " without configuring with --poly." << std::endl; - options::nlCad.set(false); - options::nlExt.set(true); + opts.set(options::nlCad, false); + opts.set(options::nlExt, true); } } #endif diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 09b3d64ab..24a3e409e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -147,7 +147,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // d_proofManager must be created before Options has been finished // being parsed from the input file. Because of this, we cannot trust - // that options::unsatCores() is set correctly yet. + // that d_env->getOption(options::unsatCores) is set correctly yet. d_proofManager.reset(new ProofManager(getUserContext())); d_definedFunctions = new (true) DefinedFunctionMap(getUserContext()); @@ -205,7 +205,7 @@ void SmtEngine::finishInit() } // set the random seed - Random::getRandom().setSeed(options::seed()); + Random::getRandom().setSeed(d_env->getOption(options::seed)); // Call finish init on the options manager. This inializes the resource // manager based on the options, and sets up the best default options @@ -213,7 +213,7 @@ void SmtEngine::finishInit() d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver); ProofNodeManager* pnm = nullptr; - if (options::produceProofs()) + if (d_env->getOption(options::produceProofs)) { // ensure bound variable uses canonical bound variables getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); @@ -274,11 +274,12 @@ void SmtEngine::finishInit() getDumpManager()->finishInit(); // subsolvers - if (options::produceAbducts()) + if (d_env->getOption(options::produceAbducts)) { d_abductSolver.reset(new AbductionSolver(this)); } - if (options::produceInterpols() != options::ProduceInterpols::NONE) + if (d_env->getOption(options::produceInterpols) + != options::ProduceInterpols::NONE) { d_interpolSolver.reset(new InterpolationSolver(this)); } @@ -322,7 +323,8 @@ SmtEngine::~SmtEngine() // d_proofManager is always created when proofs are enabled at configure // time. Because of this, this code should not be wrapped in PROOF() which - // additionally checks flags such as options::produceProofs(). + // additionally checks flags such as + // d_env->getOption(options::produceProofs). // // Note: the proof manager must be destroyed before the theory engine. // Because the destruction of the proofs depends on contexts owned be the @@ -465,7 +467,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) { d_state->setFilename(value); } - else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser()) + else if (key == "smt-lib-version" && !Options::current().wasSetByUser(options::inputLanguage)) { language::input::Language ilang = language::input::LANG_SMTLIB_V2_6; @@ -475,15 +477,15 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) << " unsupported, defaulting to language (and semantics of) " "SMT-LIB 2.6\n"; } - options::inputLanguage.set(ilang); + Options::current().set(options::inputLanguage, ilang); // also update the output language - if (!options::outputLanguage.wasSetByUser()) + if (!Options::current().wasSetByUser(options::outputLanguage)) { language::output::Language olang = language::toOutputLanguage(ilang); - if (options::outputLanguage() != olang) + if (d_env->getOption(options::outputLanguage) != olang) { - options::outputLanguage.set(olang); - *options::out() << language::SetLanguage(olang); + Options::current().set(options::outputLanguage, olang); + *d_env->getOption(options::out) << language::SetLanguage(olang); } } } @@ -571,7 +573,7 @@ std::string SmtEngine::getInfo(const std::string& key) const } Assert(key == "all-options"); // get the options, like all-statistics - return toSExpr(Options::current()->getOptions()); + return toSExpr(Options::current().getOptions()); } void SmtEngine::debugCheckFormals(const std::vector& formals, Node func) @@ -595,7 +597,8 @@ void SmtEngine::debugCheckFunctionBody(Node formula, const std::vector& formals, Node func) { - TypeNode formulaType = formula.getType(options::typeChecking()); + TypeNode formulaType = + formula.getType(d_env->getOption(options::typeChecking)); TypeNode funcType = func.getType(); // We distinguish here between definitions of constants and functions, // because the type checking for them is subtly different. Perhaps we @@ -777,7 +780,7 @@ Result SmtEngine::quickCheck() { Model* SmtEngine::getAvailableModel(const char* c) const { - if (!options::assignFunctionValues()) + if (!d_env->getOption(options::assignFunctionValues)) { std::stringstream ss; ss << "Cannot " << c << " when --assign-function-values is false."; @@ -794,7 +797,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - if (!options::produceModels()) + if (!d_env->getOption(options::produceModels)) { std::stringstream ss; ss << "Cannot " << c << " when produce-models options is off."; @@ -938,19 +941,22 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, << "(" << assumptions << ") => " << r << endl; // Check that SAT results generate a model correctly. - if(options::checkModels()) { + if (d_env->getOption(options::checkModels)) + { if (r.asSatisfiabilityResult().isSat() == Result::SAT) { checkModel(); } } // Check that UNSAT results generate a proof correctly. - if (options::checkProofs() || options::proofEagerChecking()) + if (d_env->getOption(options::checkProofs) + || d_env->getOption(options::proofEagerChecking)) { if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - if ((options::checkProofs() || options::proofEagerChecking()) - && !options::produceProofs()) + if ((d_env->getOption(options::checkProofs) + || d_env->getOption(options::proofEagerChecking)) + && !d_env->getOption(options::produceProofs)) { throw ModalException( "Cannot check-proofs because proofs were disabled."); @@ -959,7 +965,7 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, } } // Check that UNSAT results generate an unsat core correctly. - if (options::checkUnsatCores()) + if (d_env->getOption(options::checkUnsatCores)) { if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { @@ -988,7 +994,7 @@ std::vector SmtEngine::getUnsatAssumptions(void) { Trace("smt") << "SMT getUnsatAssumptions()" << endl; SmtScope smts(this); - if (!options::unsatAssumptions()) + if (!d_env->getOption(options::unsatAssumptions)) { throw ModalException( "Cannot get unsat assumptions when produce-unsat-assumptions option " @@ -1201,7 +1207,9 @@ Node SmtEngine::getValue(const Node& ex) const Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); - if(options::abstractValues() && resultNode.getType().isArray()) { + if (d_env->getOption(options::abstractValues) + && resultNode.getType().isArray()) + { resultNode = d_absValues->mkAbstractValue(resultNode); Trace("smt") << "--- abstract value >> " << resultNode << endl; } @@ -1240,13 +1248,15 @@ Model* SmtEngine::getModel() { Assert(te != nullptr); te->setEagerModelBuilding(); - if (options::modelCoresMode() != options::ModelCoresMode::NONE) + if (d_env->getOption(options::modelCoresMode) + != options::ModelCoresMode::NONE) { // If we enabled model cores, we compute a model core for m based on our // (expanded) assertions using the model core builder utility std::vector eassertsProc = getExpandedAssertions(); - ModelCoreBuilder::setModelCore( - eassertsProc, m->getTheoryModel(), options::modelCoresMode()); + ModelCoreBuilder::setModelCore(eassertsProc, + m->getTheoryModel(), + d_env->getOption(options::modelCoresMode)); } // set the information on the SMT-level model Assert(m != nullptr); @@ -1269,7 +1279,8 @@ Result SmtEngine::blockModel() Model* m = getAvailableModel("block model"); - if (options::blockModelsMode() == options::BlockModelsMode::NONE) + if (d_env->getOption(options::blockModelsMode) + == options::BlockModelsMode::NONE) { std::stringstream ss; ss << "Cannot block model when block-models is set to none."; @@ -1278,8 +1289,10 @@ Result SmtEngine::blockModel() // get expanded assertions std::vector eassertsProc = getExpandedAssertions(); - Node eblocker = ModelBlocker::getModelBlocker( - eassertsProc, m->getTheoryModel(), options::blockModelsMode()); + Node eblocker = + ModelBlocker::getModelBlocker(eassertsProc, + m->getTheoryModel(), + d_env->getOption(options::blockModelsMode)); return assertFormula(eblocker); } @@ -1375,17 +1388,17 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; } void SmtEngine::checkProof() { - Assert(options::produceProofs()); + Assert(d_env->getOption(options::produceProofs)); // internal check the proof PropEngine* pe = getPropEngine(); Assert(pe != nullptr); - if (options::proofEagerChecking()) + if (d_env->getOption(options::proofEagerChecking)) { pe->checkProof(d_asserts->getAssertionList()); } Assert(pe->getProof() != nullptr); std::shared_ptr pePfn = pe->getProof(); - if (options::checkProofs()) + if (d_env->getOption(options::checkProofs)) { d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions); } @@ -1398,7 +1411,7 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry() UnsatCore SmtEngine::getUnsatCoreInternal() { - if (!options::unsatCores()) + if (!d_env->getOption(options::unsatCores)) { throw ModalException( "Cannot get an unsat core when produce-unsat-cores[-new] or " @@ -1438,7 +1451,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() } void SmtEngine::checkUnsatCore() { - Assert(options::unsatCores()) + Assert(d_env->getOption(options::unsatCores)) << "cannot check unsat core if unsat cores are turned off"; Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; @@ -1538,7 +1551,7 @@ std::string SmtEngine::getProof() { getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut()); } - if (!options::produceProofs()) + if (!d_env->getOption(options::produceProofs)) { throw ModalException("Cannot get a proof when proof option is off."); } @@ -1561,7 +1574,7 @@ std::string SmtEngine::getProof() void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); finishInit(); - if (options::instFormatMode() == options::InstFormatMode::SZS) + if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS) { out << "% SZS output start Proof for " << d_state->getFilename() << std::endl; @@ -1570,9 +1583,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) { // First, extract and print the skolemizations bool printed = false; - bool reqNames = !options::printInstFull(); + bool reqNames = !d_env->getOption(options::printInstFull); // only print when in list mode - if (options::printInstMode() == options::PrintInstMode::LIST) + if (d_env->getOption(options::printInstMode) == options::PrintInstMode::LIST) { std::map> sks; qe->getSkolemTermVectors(sks); @@ -1607,14 +1620,15 @@ void SmtEngine::printInstantiations( std::ostream& out ) { continue; } // must have a name - if (options::printInstMode() == options::PrintInstMode::NUM) + if (d_env->getOption(options::printInstMode) == options::PrintInstMode::NUM) { out << "(num-instantiations " << name << " " << i.second.size() << ")" << std::endl; } else { - Assert(options::printInstMode() == options::PrintInstMode::LIST); + Assert(d_env->getOption(options::printInstMode) + == options::PrintInstMode::LIST); InstantiationList ilist(name, i.second); out << ilist; } @@ -1625,7 +1639,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { { out << "No instantiations" << std::endl; } - if (options::instFormatMode() == options::InstFormatMode::SZS) + if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS) { out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; } @@ -1636,9 +1650,9 @@ void SmtEngine::getInstantiationTermVectors( { SmtScope smts(this); finishInit(); - if (options::produceProofs() - && (!options::unsatCores() - || options::unsatCoresMode() == options::UnsatCoresMode::FULL_PROOF) + if (d_env->getOption(options::produceProofs) + && (!d_env->getOption(options::unsatCores) + || d_env->getOption(options::unsatCoresMode) == options::UnsatCoresMode::FULL_PROOF) && getSmtMode() == SmtMode::UNSAT) { // minimize instantiations based on proof manager @@ -1745,7 +1759,8 @@ std::vector SmtEngine::getAssertions() getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut()); } Trace("smt") << "SMT getAssertions()" << endl; - if(!options::produceAssertions()) { + if (!d_env->getOption(options::produceAssertions)) + { const char* msg = "Cannot query the current assertion list when not in produce-assertions mode."; throw ModalException(msg); diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index d81a507f8..cc660ba70 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -72,7 +72,7 @@ public: class OptionsErrOstreamUpdate : public OstreamUpdate { public: std::ostream& get() override { return *(options::err()); } - void set(std::ostream* setTo) override { return options::err.set(setTo); } + void set(std::ostream* setTo) override { return Options::current().set(options::err, setTo); } }; /* class OptionsErrOstreamUpdate */ class DumpOstreamUpdate : public OstreamUpdate { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 4687922a0..ce8e2393b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2906,10 +2906,10 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu if(d_qflraStatus != Result::UNSAT){ static const int32_t pass2Limit = 20; int16_t oldCap = options::arithStandardCheckVarOrderPivots(); - options::arithStandardCheckVarOrderPivots.set(pass2Limit); + Options::current().set(options::arithStandardCheckVarOrderPivots, pass2Limit); SimplexDecisionProcedure& simplex = selectSimplex(false); d_qflraStatus = simplex.findModel(false); - options::arithStandardCheckVarOrderPivots.set(oldCap); + Options::current().set(options::arithStandardCheckVarOrderPivots, oldCap); } if(Debug.isOn("arith::importSolution")){ @@ -3048,126 +3048,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ return emmittedConflictOrSplit; } -// LinUnknown, /* Unknown error */ -// LinFeasible, /* Relaxation is feasible */ -// LinInfeasible, /* Relaxation is infeasible/all integer branches closed */ -// LinExhausted -// // Fancy final tries the following strategy -// // At final check, try the preferred simplex solver with a pivot cap -// // If that failed, swap the the other simplex solver -// // If that failed, check if there are integer variables to cut -// // If that failed, do a simplex without a pivot limit - -// int16_t oldCap = options::arithStandardCheckVarOrderPivots(); - -// static const int32_t pass2Limit = 10; -// static const int32_t relaxationLimit = 10000; -// static const int32_t mipLimit = 200000; - -// //cout << "start" << endl; -// d_qflraStatus = simplex.findModel(false); -// //cout << "end" << endl; -// if(d_qflraStatus == Result::SAT_UNKNOWN || -// (d_qflraStatus == Result::SAT && !hasIntegerModel() && !d_likelyIntegerInfeasible)){ - -// ApproximateSimplex* approxSolver = ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel, *(getTreeLog()), *(getApproxStats())); -// approxSolver->setPivotLimit(relaxationLimit); - -// if(!d_guessedCoeffSet){ -// d_guessedCoeffs = approxSolver->heuristicOptCoeffs(); -// d_guessedCoeffSet = true; -// } -// if(!d_guessedCoeffs.empty()){ -// approxSolver->setOptCoeffs(d_guessedCoeffs); -// } - -// MipResult mipRes; -// ApproximateSimplex::Solution relaxSolution, mipSolution; -// LinResult relaxRes = approxSolver->solveRelaxation(); -// switch(relaxRes){ -// case LinFeasible: -// { -// relaxSolution = approxSolver->extractRelaxation(); - -// /* If the approximate solver known to be integer infeasible -// * only redo*/ -// int maxDepth = -// d_likelyIntegerInfeasible ? 1 : options::arithMaxBranchDepth(); - -// if(d_likelyIntegerInfeasible){ -// d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution); -// }else{ -// approxSolver->setPivotLimit(mipLimit); -// mipRes = approxSolver->solveMIP(false); -// if(mipRes == ApproximateSimplex::ApproxUnsat){ -// mipRes = approxSolver->solveMIP(true); -// } -// d_errorSet.reduceToSignals(); -// //CVC5Message() << "here" << endl; -// if(mipRes == ApproximateSimplex::ApproxSat){ -// mipSolution = approxSolver->extractMIP(); -// d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution); -// }else{ -// if(mipRes == ApproximateSimplex::ApproxUnsat){ -// d_likelyIntegerInfeasible = true; -// } -// vector lemmas = approxSolver->getValidCuts(); -// for(size_t i = 0; i < lemmas.size(); ++i){ -// d_approxCuts.pushback(lemmas[i]); -// } -// d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution); -// } -// } -// options::arithStandardCheckVarOrderPivots.set(pass2Limit); -// if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = -// simplex.findModel(false); } -// //CVC5Message() << "done" << endl; -// } -// break; -// case ApproximateSimplex::ApproxUnsat: -// { -// ApproximateSimplex::Solution sol = -// approxSolver->extractRelaxation(); - -// d_qflraStatus = d_attemptSolSimplex.attempt(sol); -// options::arithStandardCheckVarOrderPivots.set(pass2Limit); - -// if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); } -// } -// break; -// default: -// break; -// } -// delete approxSolver; -// } -// } - -// if(!useFancyFinal){ -// d_qflraStatus = simplex.findModel(noPivotLimit); -// }else{ - -// if(d_qflraStatus == Result::SAT_UNKNOWN){ -// //CVC5Message() << "got sat unknown" << endl; -// vector toCut = cutAllBounded(); -// if(toCut.size() > 0){ -// //branchVector(toCut); -// emmittedConflictOrSplit = true; -// }else{ -// //CVC5Message() << "splitting" << endl; - -// d_qflraStatus = simplex.findModel(noPivotLimit); -// } -// } -// options::arithStandardCheckVarOrderPivots.set(oldCap); -// } - -// // TODO Save zeroes with no conflicts -// d_linEq.stopTrackingBoundCounts(); -// d_partialModel.startQueueingBoundCounts(); - -// return emmittedConflictOrSplit; -// } - bool TheoryArithPrivate::hasFreshArithLiteral(Node n) const{ switch(n.getKind()){ case kind::LEQ: diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 0d62481f9..582d67b31 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, Node query) { Assert (!query.isNull()); - if (options::sygusExprMinerCheckTimeout.wasSetByUser()) + if (Options::current().wasSetByUser(options::sygusExprMinerCheckTimeout)) { initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout()); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 232b9f736..62f362e2b 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -234,7 +234,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, std::unique_ptr repcChecker; // initialize the subsolver using the standard method initializeSubsolver(repcChecker, - options::sygusRepairConstTimeout.wasSetByUser(), + Options::current().wasSetByUser(options::sygusRepairConstTimeout), options::sygusRepairConstTimeout()); // renable options disabled by sygus repcChecker->setOption("miniscope-quant", "true"); -- 2.30.2