Initial refactoring of set defaults (#7021)

This commit starts to carve out better control flow structure in setDefaults.

It makes setDefaults contained in a class, and moves a few blocks of code to their own functions.

This class also makes options manager obsolete, it is deleted in this PR.

There should be no behavior change in this PR.

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;