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