From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 24 Aug 2021 01:09:31 +0000 (-0500)
Subject: Top-level structure for set defaults (#7047)
X-Git-Tag: cvc5-1.0.0~1342
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=198e4a9b622bff260cf6b24f67f31fbff11873f2;p=cvc5.git

Top-level structure for set defaults (#7047)

This breaks setDefaults into three functions that summarize the high-level behavior of setDefaults.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 5532d599c..d158d5010 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -52,6 +52,16 @@ SetDefaults::SetDefaults(bool isInternalSubsolver)
 }
 
 void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
+{
+  // initial changes that are independent of logic, and may impact the logic
+  setDefaultsPre(opts);
+  // now, finalize the logic
+  finalizeLogic(logic, opts);
+  // further changes to options based on the logic
+  setDefaultsPost(logic, opts);
+}
+
+void SetDefaults::setDefaultsPre(Options& opts)
 {
   // implied options
   if (opts.smt.debugCheckModels)
@@ -131,7 +141,10 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
     Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl;
     opts.bv.bitvectorAlgebraicSolver = true;
   }
+}
 
+void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
+{
   if (opts.bv.bitblastMode == options::BitblastMode::EAGER)
   {
     if (opts.smt.produceModels
@@ -390,15 +403,10 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
     opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
   }
 
-  // whether we want to force safe unsat cores, i.e., if we are in the default
-  // ASSUMPTIONS mode, since other ones are experimental
-  bool safeUnsatCores =
-      opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
-
   // Disable options incompatible with incremental solving, unsat cores or
   // output an error if enabled explicitly. It is also currently incompatible
   // with arithmetic, force the option off.
-  if (opts.base.incrementalSolving || safeUnsatCores)
+  if (opts.base.incrementalSolving || safeUnsatCores(opts))
   {
     if (opts.smt.unconstrainedSimp)
     {
@@ -459,7 +467,7 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
 
   // Disable options incompatible with unsat cores or output an error if enabled
   // explicitly
-  if (safeUnsatCores)
+  if (safeUnsatCores(opts))
   {
     if (opts.smt.simplificationMode != options::SimplificationMode::NONE)
     {
@@ -627,12 +635,12 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
     opts.smt.produceModels = true;
   }
 
-  /////////////////////////////////////////////////////////////////////////////
-  // Widen logic
-  /////////////////////////////////////////////////////////////////////////////
+  // widen the logic
   widenLogic(logic, opts);
-  /////////////////////////////////////////////////////////////////////////////
+}
 
+void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
+{
   // Set the options for the theoryOf
   if (!opts.theory.theoryOfModeWasSetByUser)
   {
@@ -652,7 +660,8 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
   if (!opts.uf.ufSymmetryBreakerWasSetByUser)
   {
     bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
-                       && !opts.base.incrementalSolving && !safeUnsatCores;
+                       && !opts.base.incrementalSolving
+                       && !safeUnsatCores(opts);
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
                  << std::endl;
     opts.uf.ufSymmetryBreaker = qf_uf_noinc;
@@ -701,7 +710,7 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
                       && (logic.isTheoryEnabled(THEORY_ARRAYS)
                           && logic.isTheoryEnabled(THEORY_UF)
                           && logic.isTheoryEnabled(THEORY_BV))
-                      && !safeUnsatCores;
+                      && !safeUnsatCores(opts);
     Trace("smt") << "setting repeat simplification to " << repeatSimp
                  << std::endl;
     opts.smt.repeatSimp = repeatSimp;
@@ -1046,6 +1055,13 @@ bool SetDefaults::mustDisableProofs(const Options& opts) const
   return false;
 }
 
+bool SetDefaults::safeUnsatCores(const Options& opts) const
+{
+  // whether we want to force safe unsat cores, i.e., if we are in the default
+  // ASSUMPTIONS mode, since other ones are experimental
+  return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
+}
+
 void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const
 {
   bool needsUf = false;
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index a1bf17a8f..96f8567df 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -46,6 +46,7 @@ class SetDefaults
   void setDefaults(LogicInfo& logic, Options& opts);
 
  private:
+  //------------------------- utility methods
   /**
    * Determine whether we will be solving a SyGuS problem.
    */
@@ -59,12 +60,34 @@ class SetDefaults
    * that answers "unsat" without showing a proof of unsatisfiabilty.
    */
   bool mustDisableProofs(const Options& opts) const;
+  /**
+   * Return true if we are using "safe" unsat cores, which disables all
+   * techniques that may interfere with producing correct unsat cores.
+   */
+  bool safeUnsatCores(const Options& opts) const;
+  //------------------------- options setting, prior finalization of logic
+  /**
+   * Set defaults pre, which sets all options prior to finalizing the logic.
+   * It is required that any options that impact the finalization of logic
+   * (finalizeLogic).
+   */
+  void setDefaultsPre(Options& opts);
+  //------------------------- finalization of the logic
+  /**
+   * Finalize the logic based on the options.
+   */
+  void finalizeLogic(LogicInfo& logic, Options& opts) const;
   /**
    * 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) const;
+  //------------------------- options setting, post finalization of logic
+  /**
+   * Set all default options, after we have finalized the logic.
+   */
+  void setDefaultsPost(const LogicInfo& logic, Options& opts) const;
   /**
    * Set defaults related to quantifiers, called when quantifiers are enabled.
    * This method modifies opt.quantifiers only.