diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-17 12:52:53 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-17 12:52:53 -0500 |
commit | 0783307a81f3f27194d7c08e1e8f32123432b9b8 (patch) | |
tree | 080b4b48b245aa2f055033708b6788a92610ce55 /src/smt/set_defaults.h | |
parent | 1f9f73a863401da3bc06fc82bb06f0afe947cce9 (diff) | |
parent | e8f18dd65c829c3c12158d57e1fc7d2c9dcdcfd4 (diff) |
Merge branch 'master' into rmMaybermMaybe
Diffstat (limited to 'src/smt/set_defaults.h')
-rw-r--r-- | src/smt/set_defaults.h | 48 |
1 files changed, 36 insertions, 12 deletions
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 6e77b488c..99db64b4a 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -16,25 +16,49 @@ #ifndef CVC5__SMT__SET_DEFAULTS_H #define CVC5__SMT__SET_DEFAULTS_H +#include "options/options.h" #include "theory/logic_info.h" 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, 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 |