diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/smt/options_manager.cpp | 48 | ||||
| -rw-r--r-- | src/smt/options_manager.h | 72 | ||||
| -rw-r--r-- | src/smt/set_defaults.cpp | 488 | ||||
| -rw-r--r-- | src/smt/set_defaults.h | 47 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 14 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 6 |
7 files changed, 290 insertions, 387 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 698c38cae..bc7103f0d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -311,8 +311,6 @@ libcvc5_add_sources( smt/node_command.h smt/optimization_solver.cpp smt/optimization_solver.h - smt/options_manager.cpp - smt/options_manager.h smt/output_manager.cpp smt/output_manager.h smt/quant_elim_solver.cpp diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp deleted file mode 100644 index 9ffb396d1..000000000 --- a/src/smt/options_manager.cpp +++ /dev/null @@ -1,48 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Module for managing options of an SmtEngine. - */ - -#include "smt/options_manager.h" - -#include "base/output.h" -#include "expr/expr_iomanip.h" -#include "options/base_options.h" -#include "options/expr_options.h" -#include "options/smt_options.h" -#include "smt/command.h" -#include "smt/dump.h" -#include "smt/set_defaults.h" -#include "util/resource_manager.h" - -namespace cvc5 { -namespace smt { - -OptionsManager::OptionsManager(Options* opts) : d_options(opts) -{ -} - -OptionsManager::~OptionsManager() {} - -void OptionsManager::notifySetOption(const std::string& key) -{ -} - -void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver) -{ - // ensure that our heuristics are properly set up - setDefaults(logic, *d_options, isInternalSubsolver); -} - -} // namespace smt -} // namespace cvc5 diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h deleted file mode 100644 index e7c9d61cb..000000000 --- a/src/smt/options_manager.h +++ /dev/null @@ -1,72 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Tim King, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Module for managing options of an SmtEngine. - */ - -#ifndef CVC5__SMT__OPTIONS_MANAGER_H -#define CVC5__SMT__OPTIONS_MANAGER_H - -#include "options/options_listener.h" - -namespace cvc5 { - -class LogicInfo; -class Options; -class ResourceManager; -class SmtEngine; - -namespace smt { - -/** - * This class is intended to be used by SmtEngine, and is responsible for: - * (1) Implementing core options including timeouts and output preferences, - * (2) Setting default values for options based on a logic. - * - * Notice that the constructor of this class retroactively sets all - * necessary options that have already been set in the options object it is - * given. This is to ensure that the command line arguments, which modified - * on an options object in the driver, immediately take effect upon creation of - * this class. - */ -class OptionsManager : public OptionsListener -{ - public: - OptionsManager(Options* opts); - ~OptionsManager(); - /** - * Called when a set option call is made on the options object associated - * with this class. This handles all options that should be taken into account - * immediately instead of e.g. at SmtEngine::finishInit time. This primarily - * includes options related to parsing and output. - * - * This function call is made after the option has been updated. This means - * that the value of the option can be queried in the options object that - * this class is listening to. - */ - void notifySetOption(const std::string& key) override; - /** - * Finish init, which is called at the beginning of SmtEngine::finishInit, - * just before solving begins. This initializes the options pertaining to - * time limits, and sets the default options. - */ - void finishInit(LogicInfo& logic, bool isInternalSubsolver); - - private: - /** Reference to the options object */ - Options* d_options; -}; - -} // namespace smt -} // namespace cvc5 - -#endif /* CVC5__SMT__OPTIONS_MANAGER_H */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index c916ac962..6fd2a3f68 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -46,7 +46,12 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) +SetDefaults::SetDefaults(bool isInternalSubsolver) + : d_isInternalSubsolver(isInternalSubsolver) +{ +} + +void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) { // implied options if (opts.smt.debugCheckModels) @@ -333,7 +338,7 @@ void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) } // sygus inference may require datatypes - if (!isInternalSubsolver) + if (!d_isInternalSubsolver) { if (opts.smt.produceAbducts || opts.smt.produceInterpols != options::ProduceInterpols::NONE @@ -659,95 +664,9 @@ void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) } ///////////////////////////////////////////////////////////////////////////// - // Theory widening - // - // Some theories imply the use of other theories to handle certain operators, - // e.g. UF to handle partial functions. + // Widen logic ///////////////////////////////////////////////////////////////////////////// - bool needsUf = false; - // strings require LIA, UF; widen the logic - if (logic.isTheoryEnabled(THEORY_STRINGS)) - { - LogicInfo log(logic.getUnlockedCopy()); - // Strings requires arith for length constraints, and also UF - needsUf = true; - if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) - { - Notice() - << "Enabling linear integer arithmetic because strings are enabled" - << std::endl; - log.enableTheory(THEORY_ARITH); - log.enableIntegers(); - log.arithOnlyLinear(); - } - else if (!logic.areIntegersUsed()) - { - Notice() << "Enabling integer arithmetic because strings are enabled" - << std::endl; - log.enableIntegers(); - } - logic = log; - logic.lock(); - } - if (opts.bv.bvAbstraction) - { - // bv abstraction may require UF - Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; - needsUf = true; - } - else if (opts.quantifiers.preSkolemQuantNested - && opts.quantifiers.preSkolemQuantNestedWasSetByUser) - { - // 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. - Notice() << "Enabling UF because preSkolemQuantNested requires it." - << std::endl; - needsUf = true; - } - if (needsUf - // Arrays, datatypes and sets permit Boolean terms and thus require UF - || logic.isTheoryEnabled(THEORY_ARRAYS) - || logic.isTheoryEnabled(THEORY_DATATYPES) - || logic.isTheoryEnabled(THEORY_SETS) - || logic.isTheoryEnabled(THEORY_BAGS) - // Non-linear arithmetic requires UF to deal with division/mod because - // their expansion introduces UFs for the division/mod-by-zero case. - // If we are eliminating non-linear arithmetic via solve-int-as-bv, - // then this is not required, since non-linear arithmetic will be - // eliminated altogether (or otherwise fail at preprocessing). - || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && opts.smt.solveIntAsBV == 0) - // FP requires UF since there are multiple operators that are partially - // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more - // details). - || logic.isTheoryEnabled(THEORY_FP)) - { - if (!logic.isTheoryEnabled(THEORY_UF)) - { - LogicInfo log(logic.getUnlockedCopy()); - if (!needsUf) - { - Notice() << "Enabling UF because " << logic << " requires it." - << std::endl; - } - log.enableTheory(THEORY_UF); - logic = log; - logic.lock(); - } - } - if (opts.arith.arithMLTrick) - { - if (!logic.areIntegersUsed()) - { - // enable integers - LogicInfo log(logic.getUnlockedCopy()); - Notice() << "Enabling integers because arithMLTrick requires it." - << std::endl; - log.enableIntegers(); - logic = log; - logic.lock(); - } - } + widenLogic(logic, opts); ///////////////////////////////////////////////////////////////////////////// // Set the options for the theoryOf @@ -1124,154 +1043,7 @@ void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) // if we are attempting to rewrite everything to SyGuS, use sygus() if (usesSygus) { - if (!opts.quantifiers.sygus) - { - Trace("smt") << "turning on sygus" << std::endl; - } - opts.quantifiers.sygus = true; - // must use Ferrante/Rackoff for real arithmetic - if (!opts.quantifiers.cegqiMidpointWasSetByUser) - { - opts.quantifiers.cegqiMidpoint = true; - } - // must disable cegqi-bv since it may introduce witness terms, which - // cannot appear in synthesis solutions - if (!opts.quantifiers.cegqiBvWasSetByUser) - { - opts.quantifiers.cegqiBv = false; - } - if (opts.quantifiers.sygusRepairConst) - { - if (!opts.quantifiers.cegqiWasSetByUser) - { - opts.quantifiers.cegqi = true; - } - } - if (opts.quantifiers.sygusInference) - { - // optimization: apply preskolemization, makes it succeed more often - if (!opts.quantifiers.preSkolemQuantWasSetByUser) - { - opts.quantifiers.preSkolemQuant = true; - } - if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) - { - opts.quantifiers.preSkolemQuantNested = true; - } - } - // counterexample-guided instantiation for sygus - if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) - { - opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE; - } - if (!opts.quantifiers.quantConflictFindWasSetByUser) - { - opts.quantifiers.quantConflictFind = false; - } - if (!opts.quantifiers.instNoEntailWasSetByUser) - { - opts.quantifiers.instNoEntail = false; - } - if (!opts.quantifiers.cegqiFullEffortWasSetByUser) - { - // should use full effort cbqi for single invocation and repair const - opts.quantifiers.cegqiFullEffort = true; - } - if (opts.quantifiers.sygusRew) - { - opts.quantifiers.sygusRewSynth = true; - opts.quantifiers.sygusRewVerify = true; - } - if (opts.quantifiers.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. - opts.quantifiers.sygusRewSynth = true; - // we should not use the extended rewriter, since we are interested - // in rewrites that are not in the main rewriter - if (!opts.quantifiers.sygusExtRewWasSetByUser) - { - opts.quantifiers.sygusExtRew = false; - } - } - // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm - // is one that is specialized for returning a single solution. Non-basic - // sygus algorithms currently include the PBE solver, UNIF+PI, static - // template inference for invariant synthesis, and single invocation - // techniques. - bool reqBasicSygus = false; - if (opts.smt.produceAbducts) - { - // if doing abduction, we should filter strong solutions - if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) - { - opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG; - } - // we must use basic sygus algorithms, since e.g. we require checking - // a sygus side condition for consistency with axioms. - reqBasicSygus = true; - } - if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify - || opts.quantifiers.sygusQueryGen) - { - // rewrite rule synthesis implies that sygus stream must be true - opts.quantifiers.sygusStream = true; - } - if (opts.quantifiers.sygusStream || opts.base.incrementalSolving) - { - // Streaming and incremental mode are incompatible with techniques that - // focus the search towards finding a single solution. - reqBasicSygus = true; - } - // Now, disable options for non-basic sygus algorithms, if necessary. - if (reqBasicSygus) - { - if (!opts.quantifiers.sygusUnifPbeWasSetByUser) - { - opts.quantifiers.sygusUnifPbe = false; - } - if (opts.quantifiers.sygusUnifPiWasSetByUser) - { - opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE; - } - if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) - { - opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE; - } - if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) - { - opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE; - } - } - if (!opts.datatypes.dtRewriteErrorSelWasSetByUser) - { - opts.datatypes.dtRewriteErrorSel = true; - } - // do not miniscope - if (!opts.quantifiers.miniscopeQuantWasSetByUser) - { - opts.quantifiers.miniscopeQuant = false; - } - if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser) - { - opts.quantifiers.miniscopeQuantFreeVar = false; - } - if (!opts.quantifiers.quantSplitWasSetByUser) - { - opts.quantifiers.quantSplit = false; - } - // do not do macros - if (!opts.quantifiers.macrosQuantWasSetByUser) - { - opts.quantifiers.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 (!opts.arith.nlExtTangentPlanesWasSetByUser) - { - opts.arith.nlExtTangentPlanes = true; - } + setDefaultsSygus(opts); } // counterexample-guided instantiation for non-sygus // enable if any possible quantifiers with arithmetic, datatypes or bitvectors @@ -1581,5 +1353,245 @@ void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) #endif } +void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) +{ + bool needsUf = false; + // strings require LIA, UF; widen the logic + if (logic.isTheoryEnabled(THEORY_STRINGS)) + { + LogicInfo log(logic.getUnlockedCopy()); + // Strings requires arith for length constraints, and also UF + needsUf = true; + if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) + { + Notice() + << "Enabling linear integer arithmetic because strings are enabled" + << std::endl; + log.enableTheory(THEORY_ARITH); + log.enableIntegers(); + log.arithOnlyLinear(); + } + else if (!logic.areIntegersUsed()) + { + Notice() << "Enabling integer arithmetic because strings are enabled" + << std::endl; + log.enableIntegers(); + } + logic = log; + logic.lock(); + } + if (opts.bv.bvAbstraction) + { + // bv abstraction may require UF + Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; + needsUf = true; + } + else if (opts.quantifiers.preSkolemQuantNested + && opts.quantifiers.preSkolemQuantNestedWasSetByUser) + { + // 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. + Notice() << "Enabling UF because preSkolemQuantNested requires it." + << std::endl; + needsUf = true; + } + if (needsUf + // Arrays, datatypes and sets permit Boolean terms and thus require UF + || logic.isTheoryEnabled(THEORY_ARRAYS) + || logic.isTheoryEnabled(THEORY_DATATYPES) + || logic.isTheoryEnabled(THEORY_SETS) + || logic.isTheoryEnabled(THEORY_BAGS) + // Non-linear arithmetic requires UF to deal with division/mod because + // their expansion introduces UFs for the division/mod-by-zero case. + // If we are eliminating non-linear arithmetic via solve-int-as-bv, + // then this is not required, since non-linear arithmetic will be + // eliminated altogether (or otherwise fail at preprocessing). + || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() + && opts.smt.solveIntAsBV == 0) + // FP requires UF since there are multiple operators that are partially + // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more + // details). + || logic.isTheoryEnabled(THEORY_FP)) + { + if (!logic.isTheoryEnabled(THEORY_UF)) + { + LogicInfo log(logic.getUnlockedCopy()); + if (!needsUf) + { + Notice() << "Enabling UF because " << logic << " requires it." + << std::endl; + } + log.enableTheory(THEORY_UF); + logic = log; + logic.lock(); + } + } + if (opts.arith.arithMLTrick) + { + if (!logic.areIntegersUsed()) + { + // enable integers + LogicInfo log(logic.getUnlockedCopy()); + Notice() << "Enabling integers because arithMLTrick requires it." + << std::endl; + log.enableIntegers(); + logic = log; + logic.lock(); + } + } +} + +void SetDefaults::setDefaultsSygus(Options& opts) +{ + if (!opts.quantifiers.sygus) + { + Trace("smt") << "turning on sygus" << std::endl; + } + opts.quantifiers.sygus = true; + // must use Ferrante/Rackoff for real arithmetic + if (!opts.quantifiers.cegqiMidpointWasSetByUser) + { + opts.quantifiers.cegqiMidpoint = true; + } + // must disable cegqi-bv since it may introduce witness terms, which + // cannot appear in synthesis solutions + if (!opts.quantifiers.cegqiBvWasSetByUser) + { + opts.quantifiers.cegqiBv = false; + } + if (opts.quantifiers.sygusRepairConst) + { + if (!opts.quantifiers.cegqiWasSetByUser) + { + opts.quantifiers.cegqi = true; + } + } + if (opts.quantifiers.sygusInference) + { + // optimization: apply preskolemization, makes it succeed more often + if (!opts.quantifiers.preSkolemQuantWasSetByUser) + { + opts.quantifiers.preSkolemQuant = true; + } + if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) + { + opts.quantifiers.preSkolemQuantNested = true; + } + } + // counterexample-guided instantiation for sygus + if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) + { + opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE; + } + if (!opts.quantifiers.quantConflictFindWasSetByUser) + { + opts.quantifiers.quantConflictFind = false; + } + if (!opts.quantifiers.instNoEntailWasSetByUser) + { + opts.quantifiers.instNoEntail = false; + } + if (!opts.quantifiers.cegqiFullEffortWasSetByUser) + { + // should use full effort cbqi for single invocation and repair const + opts.quantifiers.cegqiFullEffort = true; + } + if (opts.quantifiers.sygusRew) + { + opts.quantifiers.sygusRewSynth = true; + opts.quantifiers.sygusRewVerify = true; + } + if (opts.quantifiers.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. + opts.quantifiers.sygusRewSynth = true; + // we should not use the extended rewriter, since we are interested + // in rewrites that are not in the main rewriter + if (!opts.quantifiers.sygusExtRewWasSetByUser) + { + opts.quantifiers.sygusExtRew = false; + } + } + // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm + // is one that is specialized for returning a single solution. Non-basic + // sygus algorithms currently include the PBE solver, UNIF+PI, static + // template inference for invariant synthesis, and single invocation + // techniques. + bool reqBasicSygus = false; + if (opts.smt.produceAbducts) + { + // if doing abduction, we should filter strong solutions + if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) + { + opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG; + } + // we must use basic sygus algorithms, since e.g. we require checking + // a sygus side condition for consistency with axioms. + reqBasicSygus = true; + } + if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify + || opts.quantifiers.sygusQueryGen) + { + // rewrite rule synthesis implies that sygus stream must be true + opts.quantifiers.sygusStream = true; + } + if (opts.quantifiers.sygusStream || opts.base.incrementalSolving) + { + // Streaming and incremental mode are incompatible with techniques that + // focus the search towards finding a single solution. + reqBasicSygus = true; + } + // Now, disable options for non-basic sygus algorithms, if necessary. + if (reqBasicSygus) + { + if (!opts.quantifiers.sygusUnifPbeWasSetByUser) + { + opts.quantifiers.sygusUnifPbe = false; + } + if (opts.quantifiers.sygusUnifPiWasSetByUser) + { + opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE; + } + if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) + { + opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE; + } + if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) + { + opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE; + } + } + if (!opts.datatypes.dtRewriteErrorSelWasSetByUser) + { + opts.datatypes.dtRewriteErrorSel = true; + } + // do not miniscope + if (!opts.quantifiers.miniscopeQuantWasSetByUser) + { + opts.quantifiers.miniscopeQuant = false; + } + if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser) + { + opts.quantifiers.miniscopeQuantFreeVar = false; + } + if (!opts.quantifiers.quantSplitWasSetByUser) + { + opts.quantifiers.quantSplit = false; + } + // do not do macros + if (!opts.quantifiers.macrosQuantWasSetByUser) + { + opts.quantifiers.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 (!opts.arith.nlExtTangentPlanesWasSetByUser) + { + opts.arith.nlExtTangentPlanes = true; + } +} + } // namespace smt } // namespace cvc5 diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 22e271c72..99db64b4a 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -23,19 +23,42 @@ namespace cvc5 { namespace smt { /** - * The purpose of this method is to set the default options and update the logic - * info for an SMT engine. - * - * @param logic A reference to the logic of SmtEngine, which can be - * updated by this method based on the current options and the logic itself. - * @param isInternalSubsolver Whether we are setting the options for an - * internal subsolver (see SmtEngine::isInternalSubsolver). - * - * NOTE: we currently modify the current options in scope. This method - * can be further refactored to modify an options object provided as an - * explicit argument. + * Class responsible for setting default options, which includes managing + * implied options and dependencies between the options and the logic. */ -void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver); +class SetDefaults +{ + public: + /** + * @param isInternalSubsolver Whether we are setting the options for an + * internal subsolver (see SmtEngine::isInternalSubsolver). + */ + SetDefaults(bool isInternalSubsolver); + /** + * The purpose of this method is to set the default options and update the + * logic info for an SMT engine. + * + * @param logic A reference to the logic of SmtEngine, which can be + * updated by this method based on the current options and the logic itself. + * @param opts The options to modify, typically the main options of the + * SmtEngine in scope. + */ + void setDefaults(LogicInfo& logic, Options& opts); + + private: + /** + * Widen logic to theories that are required, since some theories imply the + * use of other theories to handle certain operators, e.g. UF to handle + * partial functions. + */ + void widenLogic(LogicInfo& logic, Options& opts); + /** + * Set defaults related to SyGuS, called when SyGuS is enabled. + */ + void setDefaultsSygus(Options& opts); + /** Are we an internal subsolver? */ + bool d_isInternalSubsolver; +}; } // namespace smt } // namespace cvc5 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5f3920929..3e4c1efa7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -49,10 +49,10 @@ #include "smt/model_blocker.h" #include "smt/model_core_builder.h" #include "smt/node_command.h" -#include "smt/options_manager.h" #include "smt/preprocessor.h" #include "smt/proof_manager.h" #include "smt/quant_elim_solver.h" +#include "smt/set_defaults.h" #include "smt/smt_engine_scope.h" #include "smt/smt_engine_state.h" #include "smt/smt_engine_stats.h" @@ -103,7 +103,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) d_isInternalSubsolver(false), d_stats(nullptr), d_outMgr(this), - d_optm(nullptr), d_pp(nullptr), d_scope(nullptr) { @@ -120,8 +119,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // On the other hand, this hack breaks use cases where multiple SmtEngine // objects are created by the user. d_scope.reset(new SmtScope(this)); - // set the options manager - d_optm.reset(new smt::OptionsManager(&getOptions())); // listen to node manager events getNodeManager()->subscribeEvents(d_snmListener.get()); // listen to resource out @@ -195,10 +192,10 @@ void SmtEngine::finishInit() // set the random seed Random::getRandom().setSeed(d_env->getOptions().driver.seed); - // Call finish init on the options manager. This inializes the resource - // manager based on the options, and sets up the best default options - // based on our heuristics. - d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver); + // Call finish init on the set defaults module. This inializes the logic + // and the best default options based on our heuristics. + SetDefaults sdefaults(d_isInternalSubsolver); + sdefaults.setDefaults(d_env->d_logic, getOptions()); ProofNodeManager* pnm = nullptr; if (d_env->getOptions().smt.produceProofs) @@ -324,7 +321,6 @@ SmtEngine::~SmtEngine() getNodeManager()->unsubscribeEvents(d_snmListener.get()); d_snmListener.reset(nullptr); d_routListener.reset(nullptr); - d_optm.reset(nullptr); d_pp.reset(nullptr); // destroy the state d_state.reset(nullptr); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d00fa0c76..f42d791e2 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1112,12 +1112,6 @@ class CVC5_EXPORT SmtEngine /** the output manager for commands */ mutable OutputManager d_outMgr; /** - * The options manager, which is responsible for implementing core options - * such as those related to time outs and printing. It is also responsible - * for set default options based on the logic. - */ - std::unique_ptr<smt::OptionsManager> d_optm; - /** * The preprocessor. */ std::unique_ptr<smt::Preprocessor> d_pp; |