Standardizing notifications for setting options in set_defaults (#8057)

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 1fd2c3dc5bcb081847b7c04eaa3fc1c06edffbde..c3df86bf3b954ac40f568b34dbc584dbc1b017ec 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -104,8 +104,8 @@ void SetDefaults::setDefaultsPre(Options& opts)
   {
     if (opts.smt.unsatCoresModeWasSetByUser)
     {
-      verbose(1)
-          << "Overriding OFF unsat-core mode since cores were requested.\n";
+      notifyModifyOption(
+          "unsatCoresMode", "assumptions", "enabling unsat cores");
     }
     opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
   }
@@ -120,8 +120,7 @@ void SetDefaults::setDefaultsPre(Options& opts)
   {
     if (opts.smt.unsatCoresModeWasSetByUser)
     {
-      verbose(1) << "Forcing full-proof mode for unsat cores mode since proofs "
-                    "were requested.\n";
+      notifyModifyOption("unsatCoresMode", "full-proof", "enabling proofs");
     }
     // enable unsat cores, because they are available as a consequence of proofs
     opts.smt.unsatCores = true;
@@ -133,8 +132,7 @@ void SetDefaults::setDefaultsPre(Options& opts)
   {
     if (opts.smt.produceProofsWasSetByUser)
     {
-      verbose(1)
-          << "Forcing proof production since new unsat cores were requested.\n";
+      notifyModifyOption("produceProofs", "true", "enabling unsat cores");
     }
     opts.smt.produceProofs = true;
   }
@@ -151,8 +149,8 @@ void SetDefaults::setDefaultsPre(Options& opts)
     {
       opts.smt.unsatCores = false;
       opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
-      verbose(1) << "SolverEngine: turning off produce-proofs due to "
-                 << reasonNoProofs.str() << "." << std::endl;
+      notifyModifyOption(
+          "produceProofs and unsatCores", "false", reasonNoProofs.str());
       opts.smt.produceProofs = false;
       opts.smt.checkProofs = false;
     }
@@ -200,9 +198,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
             "for the combination of bit-vectors with arrays or uinterpreted "
             "functions. Try --bitblast=lazy"));
       }
-      verbose(1)
-          << "SolverEngine: setting bit-blast mode to lazy to support model"
-          << "generation" << std::endl;
+      notifyModifyOption("bitblastMode", "lazy", "model generation");
       opts.bv.bitblastMode = options::BitblastMode::LAZY;
     }
     else if (!opts.base.incrementalSolving)
@@ -259,8 +255,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
       throw OptionException(std::string(
           "Ackermannization currently does not support model generation."));
     }
-    verbose(1) << "SolverEngine: turn off ackermannization to support model"
-               << "generation" << std::endl;
+    notifyModifyOption("ackermann", "false", "model generation");
     opts.smt.ackermann = false;
   }
 
@@ -950,9 +945,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       reason << "unconstrained simplification";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off unconstrained simplification to "
-                  "support incremental solving"
-               << std::endl;
+    notifyModifyOption("unconstrainedSimp", "false", "incremental solving");
     opts.smt.unconstrainedSimp = false;
   }
   if (opts.bv.bitblastMode == options::BitblastMode::EAGER
@@ -969,9 +962,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       reason << "sygus inference";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off sygus inference to support "
-                  "incremental solving"
-               << std::endl;
+    notifyModifyOption("sygusInference", "false", "incremental solving");
     opts.quantifiers.sygusInference = false;
   }
   if (opts.quantifiers.sygusInst)
@@ -981,9 +972,7 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       reason << "sygus inst";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off sygus inst to support "
-                  "incremental solving"
-               << std::endl;
+    notifyModifyOption("sygusInst", "false", "incremental solving");
     opts.quantifiers.sygusInst = false;
   }
   if (opts.smt.solveIntAsBV > 0)
@@ -993,9 +982,12 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
   }
 
   // disable modes not supported by incremental
+  notifyModifyOption("sortInference", "false", "incremental solving");
   opts.smt.sortInference = false;
   opts.uf.ufssFairnessMonotone = false;
+  notifyModifyOption("globalNegate", "false", "incremental solving");
   opts.quantifiers.globalNegate = false;
+  notifyModifyOption("cegqiNestedQE", "false", "incremental solving");
   opts.quantifiers.cegqiNestedQE = false;
   opts.arith.arithMLTrick = false;
 
@@ -1012,9 +1004,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "simplification";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off simplification to support unsat "
-                  "cores"
-               << std::endl;
+    notifyModifyOption("simplificationMode", "none", "unsat cores");
     opts.smt.simplificationMode = options::SimplificationMode::NONE;
   }
 
@@ -1025,8 +1015,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "learned rewrites";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off learned rewrites to support "
-                  "unsat cores\n";
+    notifyModifyOption("learnedRewrite", "false", "unsat cores");
     opts.smt.learnedRewrite = false;
   }
 
@@ -1037,8 +1026,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "pseudoboolean rewrites";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off pseudoboolean rewrites to support "
-                  "unsat cores\n";
+    notifyModifyOption("pbRewrites", "false", "unsat cores");
     opts.arith.pbRewrites = false;
   }
 
@@ -1049,8 +1037,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "sort inference";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off sort inference to support unsat "
-                  "cores\n";
+    notifyModifyOption("sortInference", "false", "unsat cores");
     opts.smt.sortInference = false;
   }
 
@@ -1061,8 +1048,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "pre-skolemization";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off pre-skolemization to support "
-                  "unsat cores\n";
+    notifyModifyOption("preSkolemQuant", "false", "unsat cores");
     opts.quantifiers.preSkolemQuant = false;
   }
 
@@ -1073,8 +1059,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "bv-to-bool";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off bitvector-to-bool to support "
-                  "unsat cores\n";
+    notifyModifyOption("bitvectorToBool", "false", "unsat cores");
     opts.bv.bitvectorToBool = false;
   }
 
@@ -1085,8 +1070,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "bool-to-bv != off";
       return true;
     }
-    verbose(1)
-        << "SolverEngine: turning off bool-to-bv to support unsat cores\n";
+    notifyModifyOption("boolToBitvector", "off", "unsat cores");
     opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
   }
 
@@ -1097,8 +1081,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "bv-intro-pow2";
       return true;
     }
-    verbose(1)
-        << "SolverEngine: turning off bv-intro-pow2 to support unsat cores";
+    notifyModifyOption("bvIntroducePow2", "false", "unsat cores");
     opts.bv.bvIntroducePow2 = false;
   }
 
@@ -1109,8 +1092,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "repeat-simp";
       return true;
     }
-    verbose(1)
-        << "SolverEngine: turning off repeat-simp to support unsat cores\n";
+    notifyModifyOption("repeatSimp", "false", "unsat cores");
     opts.smt.repeatSimp = false;
   }
 
@@ -1121,8 +1103,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "global-negate";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off global-negate to support unsat "
-                  "cores\n";
+    notifyModifyOption("globalNegate", "false", "unsat cores");
     opts.quantifiers.globalNegate = false;
   }
 
@@ -1138,9 +1119,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "unconstrained simplification";
       return true;
     }
-    verbose(1) << "SolverEngine: turning off unconstrained simplification to "
-                  "support unsat cores"
-               << std::endl;
+    notifyModifyOption("unconstrainedSimp", "false", "unsat cores");
     opts.smt.unconstrainedSimp = false;
   }
   return false;
@@ -1268,8 +1247,8 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     // Allows to answer sat more often by default.
     if (!opts.quantifiers.fmfBoundWasSetByUser)
     {
+      notifyModifyOption("fmfBound", "true", "arrays-exp");
       opts.quantifiers.fmfBound = true;
-      Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl;
     }
   }
   if (logic.hasCardinalityConstraints())
@@ -1516,9 +1495,9 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
 {
   if (!opts.quantifiers.sygus)
   {
-    Trace("smt") << "turning on sygus" << std::endl;
+    notifyModifyOption("sygus", "true", "");
+    opts.quantifiers.sygus = true;
   }
-  opts.quantifiers.sygus = true;
   // must use Ferrante/Rackoff for real arithmetic
   if (!opts.quantifiers.cegqiMidpointWasSetByUser)
   {
@@ -1728,5 +1707,17 @@ void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic,
                << std::endl;
 }
 
+void SetDefaults::notifyModifyOption(const std::string& x,
+                                     const std::string& val,
+                                     const std::string& reason) const
+{
+  verbose(1) << "SetDefaults: setting " << x << " to " << val;
+  if (!reason.empty())
+  {
+    verbose(1) << " due to " << reason;
+  }
+  verbose(1) << std::endl;
+}
+
 }  // namespace smt
 }  // namespace cvc5

diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 24b39e205b43c24f4e27cb90c0ef8f171566f3f2..238e03b05884906c0b7c46955070cbba3c455a80 100644 (file)
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -135,6 +135,10 @@ class SetDefaults : protected EnvObj
    * Set default decision mode
    */
   void setDefaultDecisionMode(const LogicInfo& logic, Options& opts) const;
+  /** Notify that we are modifying option x to val due to reason. */
+  void notifyModifyOption(const std::string& x,
+                          const std::string& val,
+                          const std::string& reason) const;
   /** Are we an internal subsolver? */
   bool d_isInternalSubsolver;
 };