Make use of options in setDefaults more consistent (#4729)

The plan is to make setDefaults (the method to update the default options based on our internal heuristics) modify an explicit copy of options.

This is the first step, which eliminates the dependence of this method on SmtEngine.

This PR is furthermore required to eliminate options listeners.

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index ce747b62d8b4e7af111c8ce199d13316de4c2060..a6c967dc96a849cb6298b3507ecde136e38f4b9b 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -425,7 +425,6 @@ header = "options/arith_options.h"
   long       = "pb-rewrites"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "apply pseudo boolean rewrites"
 
 [[option]]

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 517d864d3eb722da839953c65573dfa171eff051..f7ec33f754c83ed82876785d4e462b873e5a4db4 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -249,7 +249,6 @@ header = "options/bv_options.h"
   long       = "bv-intro-pow2"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "introduce bitvector powers of two as a preprocessing pass"
 
 [[option]]

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 80183b71fb3b76391f860d42f49d7b655ecfd897..e4847716a49299953b712f8bf44b2ab88b9d88a1 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -395,7 +395,6 @@ header = "options/smt_options.h"
   long       = "incremental"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "enable incremental solving"
 
 [[option]]

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 11751079eec2a4e38101e295f5efaa46b6d78d2d..8f6ab6c18ce9f7098a6298f6d2edf4686f518954 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -43,7 +43,7 @@ using namespace CVC4::theory;
 namespace CVC4 {
 namespace smt {
 
-void setDefaults(SmtEngine& smte, LogicInfo& logic)
+void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 {
   // implied options
   if (options::debugCheckModels())
@@ -121,7 +121,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       }
       Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
                << "generation" << std::endl;
-      smte.setOption("bitblastMode", SExpr("lazy"));
+      options::bitblastMode.set(options::BitblastMode::LAZY);
     }
     else if (!options::incrementalSolving())
     {
@@ -289,7 +289,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   }
 
   // sygus inference may require datatypes
-  if (!smte.isInternalSubsolver())
+  if (!isInternalSubsolver)
   {
     if (options::produceAbducts()
         || options::produceInterpols() != options::ProduceInterpols::NONE
@@ -325,7 +325,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   {
     Notice() << "SmtEngine: turning on produce-assertions to support "
              << "option requiring assertions." << std::endl;
-    smte.setOption("produce-assertions", SExpr("true"));
+    options::produceAssertions.set(true);
   }
 
   // Disable options incompatible with incremental solving, unsat cores, and
@@ -381,7 +381,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     }
   }
 
-
   if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
     /**
@@ -420,7 +419,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
                   "unsat cores/proofs"
                << std::endl;
-      smte.setOption("pb-rewrites", false);
+      options::pbRewrites.set(false);
     }
 
     if (options::sortInference())
@@ -473,7 +472,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       Notice() << "SmtEngine: turning off bool-to-bv to support unsat "
                   "cores/proofs"
                << std::endl;
-      smte.setOption("boolToBitvector", SExpr("off"));
+      options::boolToBitvector.set(options::BoolToBVMode::OFF);
     }
 
     if (options::bvIntroducePow2())
@@ -486,7 +485,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
                   "unsat-cores/proofs"
                << std::endl;
-      smte.setOption("bv-intro-pow2", false);
+      options::bvIntroducePow2.set(false);
     }
 
     if (options::repeatSimp())
@@ -499,7 +498,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       Notice() << "SmtEngine: turning off repeat-simp to support unsat "
                   "cores/proofs"
                << std::endl;
-      smte.setOption("repeat-simp", false);
+      options::repeatSimp.set(false);
     }
 
     if (options::globalNegate())
@@ -512,7 +511,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       Notice() << "SmtEngine: turning off global-negate to support unsat "
                   "cores/proofs"
                << std::endl;
-      smte.setOption("global-negate", false);
+      options::globalNegate.set(false);
     }
 
     if (options::bitvectorAig())
@@ -551,7 +550,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       }
       Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
                << std::endl;
-      smte.setOption("boolToBitvector", SExpr("off"));
+      options::boolToBitvector.set(options::BoolToBVMode::OFF);
     }
   }
 
@@ -561,7 +560,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
           || is_sygus))
   {
     Notice() << "SmtEngine: turning on produce-models" << std::endl;
-    smte.setOption("produce-models", SExpr("true"));
+    options::produceModels.set(true);
   }
 
   /////////////////////////////////////////////////////////////////////////////
@@ -704,7 +703,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     }
     Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
              << logic.getLogicString() << std::endl;
-    smte.setOption("boolToBitvector", SExpr("off"));
+    options::boolToBitvector.set(options::BoolToBVMode::OFF);
   }
 
   if (!options::bvEagerExplanations.wasSetByUser()
@@ -1333,7 +1332,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
           << "SmtEngine: turning off incremental solving mode (not yet "
              "supported with --proof, try --tear-down-incremental instead)"
           << std::endl;
-      smte.setOption("incremental", SExpr("false"));
+      options::incrementalSolving.set(false);
     }
     if (logic > LogicInfo("QF_AUFBVLRA"))
     {
@@ -1433,7 +1432,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       }
       Notice() << "SmtEngine: turning off produce-models to support "
                << sOptNoModel << std::endl;
-      smte.setOption("produce-models", SExpr("false"));
+      options::produceModels.set(false);
     }
     if (options::produceAssignments())
     {
@@ -1446,7 +1445,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       }
       Notice() << "SmtEngine: turning off produce-assignments to support "
                << sOptNoModel << std::endl;
-      smte.setOption("produce-assignments", SExpr("false"));
+      options::produceAssignments.set(false);
     }
     if (options::checkModels())
     {
@@ -1459,7 +1458,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       }
       Notice() << "SmtEngine: turning off check-models to support "
                << sOptNoModel << std::endl;
-      smte.setOption("check-models", SExpr("false"));
+      options::checkModels.set(false);
     }
   }
 

diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index f3ec21c9beac2d09de5b850caf3ddeaab2726bc4..606921b7c2c8bc603e75b98d6a87075db9f1b820 100644 (file)
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -15,7 +15,6 @@
 #ifndef CVC4__SMT__SET_DEFAULTS_H
 #define CVC4__SMT__SET_DEFAULTS_H
 
-#include "smt/smt_engine.h"
 #include "theory/logic_info.h"
 
 namespace CVC4 {
@@ -23,18 +22,18 @@ namespace smt {
 
 /**
  * The purpose of this method is to set the default options and update the logic
- * info for SMT engine smte.
+ * info for an SMT engine.
  *
- * The argument logic is a reference to the logic of SmtEngine, which can be
+ * @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.
- *
- * Note that currently, options are associated with the ExprManager. Thus, this
- * call updates the options associated with the current ExprManager.
- * If this designed is updated in the future so that SmtEngine has its own
- * copy of options, this method should be updated accordingly so that it
- * is responsible for updating this copy.
+ * @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.
  */
-void setDefaults(SmtEngine& smte, LogicInfo& logic);
+void setDefaults(LogicInfo& logic, bool isInternalSubsolver);
 
 }  // namespace smt
 }  // namespace CVC4

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0d8189aa4423a33f55e8afdefcb8f1cb4576cf5b..12e0f443e133905fe7f123fb1218bf6f4e1ec17f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -742,7 +742,7 @@ void SmtEngine::finishInit()
   Random::getRandom().setSeed(options::seed());
 
   // ensure that our heuristics are properly set up
-  setDefaults(*this, d_logic);
+  setDefaults(d_logic, d_isInternalSubsolver);
   
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
   // We have mutual dependency here, so we add the prop engine to the theory