Remove `Notice()` in favor of new `verbose()` (#7588)

This PR removes the remaining usages of the Notice() macros and uses verbose() instead.

diff --git a/src/api/__pycache__/parsekinds.cpython-39.pyc b/src/api/__pycache__/parsekinds.cpython-39.pyc
new file mode 100644 (file)
index 0000000..34d010c
Binary files /dev/null and b/src/api/__pycache__/parsekinds.cpython-39.pyc differ

diff --git a/src/base/output.cpp b/src/base/output.cpp
index 2b77a3b2a06c5d523aa607615aa102574aa17d3b..f9946c4a819adfcd2ed47ddf744bbdb55dab091e 100644 (file)
--- a/src/base/output.cpp
+++ b/src/base/output.cpp
@@ -32,7 +32,6 @@ const int Cvc5ostream::s_indentIosIndex = std::ios_base::xalloc();
 DebugC DebugChannel(&std::cout);
 WarningC WarningChannel(&std::cerr);
 MessageC MessageChannel(&std::cout);
-NoticeC NoticeChannel(&null_os);
 TraceC TraceChannel(&std::cout);
 std::ostream DumpOutC::dump_cout(std::cout.rdbuf());  // copy cout stream buffer
 DumpOutC DumpOutChannel(&DumpOutC::dump_cout);

diff --git a/src/base/output.h b/src/base/output.h
index 2783f4bc6c5834ef97fd27899f1bd99ad2b2eb9c..dad354ad480e36dbf1b85439dff171a5a1bfc999 100644 (file)
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -280,23 +280,6 @@ public:
   bool isOn() const { return d_os != &null_os; }
 }; /* class MessageC */
 
-/** The notice output class */
-class NoticeC
-{
-  std::ostream* d_os;
-
-public:
-  explicit NoticeC(std::ostream* os) : d_os(os) {}
-
-  Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
-
-  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
-  std::ostream& getStream() const { return *d_os; }
-  std::ostream* getStreamPointer() const { return d_os; }
-
-  bool isOn() const { return d_os != &null_os; }
-}; /* class NoticeC */
-
 /** The trace output class */
 class TraceC
 {
@@ -387,8 +370,6 @@ extern DebugC DebugChannel CVC5_EXPORT;
 extern WarningC WarningChannel CVC5_EXPORT;
 /** The message output singleton */
 extern MessageC MessageChannel CVC5_EXPORT;
-/** The notice output singleton */
-extern NoticeC NoticeChannel CVC5_EXPORT;
 /** The trace output singleton */
 extern TraceC TraceChannel CVC5_EXPORT;
 /** The dump output singleton */
@@ -403,8 +384,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
 #define CVC5Message \
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::MessageChannel
-#define Notice \
-  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::NoticeChannel
 #define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
 #define DumpOut \
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
@@ -425,8 +404,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
       : ::cvc5::WarningChannel
 #define CVC5Message \
   (!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::MessageChannel
-#define Notice \
-  (!::cvc5::NoticeChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::NoticeChannel
 #ifdef CVC5_TRACING
 #define Trace ::cvc5::TraceChannel
 #else /* CVC5_TRACING */

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 893a77cd94b8f90d326f14f5779db76d4974ff89..e7f0a90b9ba78f422212980819c1b0522c53618f 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -159,7 +159,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&cvc5::null_os);
     TraceChannel.setStream(&cvc5::null_os);
-    NoticeChannel.setStream(&cvc5::null_os);
     MessageChannel.setStream(&cvc5::null_os);
     WarningChannel.setStream(&cvc5::null_os);
   }

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index c178a637cff0b4305fa9268d18f6ba4a8bf0f685..1a0795ddc5b3f0a9a5725065a280996afbdea75a 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -89,7 +89,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver,
 {
   ParserBuilder parserBuilder(solver, sm, true);
   /* Create parser with bogus input. */
-  d_parser = parserBuilder.build();
+  d_parser.reset(parserBuilder.build());
   if (d_solver->getOptionInfo("force-logic").setByUser)
   {
     LogicInfo tmp(d_solver->getOption("force-logic"));
@@ -129,13 +129,16 @@ InteractiveShell::InteractiveShell(api::Solver* solver,
     d_usingEditline = true;
     int err = ::read_history(d_historyFilename.c_str());
     ::stifle_history(s_historyLimit);
-    if(Notice.isOn()) {
+    if (d_solver->getOptionInfo("verbosity").intValue() >= 1)
+    {
       if(err == 0) {
-        Notice() << "Read " << ::history_length << " lines of history from "
-                 << d_historyFilename << std::endl;
+        d_solver->getDriverOptions().err()
+            << "Read " << ::history_length << " lines of history from "
+            << d_historyFilename << std::endl;
       } else {
-        Notice() << "Could not read history from " << d_historyFilename
-                 << ": " << strerror(err) << std::endl;
+        d_solver->getDriverOptions().err()
+            << "Could not read history from " << d_historyFilename << ": "
+            << strerror(err) << std::endl;
       }
     }
   }
@@ -151,15 +154,20 @@ InteractiveShell::InteractiveShell(api::Solver* solver,
 InteractiveShell::~InteractiveShell() {
 #if HAVE_LIBEDITLINE
   int err = ::write_history(d_historyFilename.c_str());
-  if(err == 0) {
-    Notice() << "Wrote " << ::history_length << " lines of history to "
-             << d_historyFilename << std::endl;
-  } else {
-    Notice() << "Could not write history to " << d_historyFilename
-             << ": " << strerror(err) << std::endl;
+  if (d_solver->getOptionInfo("verbosity").intValue() >= 1)
+  {
+    if (err == 0)
+    {
+      d_solver->getDriverOptions().err()
+          << "Wrote " << ::history_length << " lines of history to "
+          << d_historyFilename << std::endl;
+    } else {
+      d_solver->getDriverOptions().err()
+          << "Could not write history to " << d_historyFilename << ": "
+          << strerror(err) << std::endl;
+  }
   }
 #endif /* HAVE_LIBEDITLINE */
-  delete d_parser;
 }
 
 Command* InteractiveShell::readCommand()

diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 6029d6b0e2652011835b5760280804535a548876..401f7a1c97152645aad5c8f26010e3a4f9291c86 100644 (file)
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -17,6 +17,7 @@
 #define CVC5__INTERACTIVE_SHELL_H
 
 #include <iosfwd>
+#include <memory>
 #include <string>
 
 namespace cvc5 {
@@ -55,13 +56,13 @@ class InteractiveShell
   /**
    * Return the internal parser being used.
    */
-  parser::Parser* getParser() { return d_parser; }
+  parser::Parser* getParser() { return d_parser.get(); }
 
  private:
   api::Solver* d_solver;
   std::istream& d_in;
   std::ostream& d_out;
-  parser::Parser* d_parser;
+  std::unique_ptr<parser::Parser> d_parser;
   bool d_quit;
   bool d_usingEditline;
 

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 060b7eeba45a66e201654085db824891efabc7f3..5adce0a4ff9e52ae5881a6073e3568d95d0899b5 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -75,7 +75,6 @@ void OptionsHandler::setErrStream(const std::string& flag, const ManagedErr& me)
   Debug.setStream(me);
   Warning.setStream(me);
   CVC5Message.setStream(me);
-  Notice.setStream(me);
   Trace.setStream(me);
 }
 
@@ -134,15 +133,9 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value)
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&cvc5::null_os);
     TraceChannel.setStream(&cvc5::null_os);
-    NoticeChannel.setStream(&cvc5::null_os);
     MessageChannel.setStream(&cvc5::null_os);
     WarningChannel.setStream(&cvc5::null_os);
   } else {
-    if(value < 1) {
-      NoticeChannel.setStream(&cvc5::null_os);
-    } else {
-      NoticeChannel.setStream(&std::cout);
-    }
     if(value < 0) {
       MessageChannel.setStream(&cvc5::null_os);
       WarningChannel.setStream(&cvc5::null_os);
@@ -269,7 +262,6 @@ void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)
 {
   Debug.getStream() << Command::printsuccess(value);
   Trace.getStream() << Command::printsuccess(value);
-  Notice.getStream() << Command::printsuccess(value);
   CVC5Message.getStream() << Command::printsuccess(value);
   Warning.getStream() << Command::printsuccess(value);
   *d_options->base.out << Command::printsuccess(value);
@@ -352,7 +344,6 @@ void OptionsHandler::setDefaultExprDepth(const std::string& flag, int depth)
 {
   Debug.getStream() << expr::ExprSetDepth(depth);
   Trace.getStream() << expr::ExprSetDepth(depth);
-  Notice.getStream() << expr::ExprSetDepth(depth);
   CVC5Message.getStream() << expr::ExprSetDepth(depth);
   Warning.getStream() << expr::ExprSetDepth(depth);
 }
@@ -361,7 +352,6 @@ void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag)
 {
   Debug.getStream() << expr::ExprDag(dag);
   Trace.getStream() << expr::ExprDag(dag);
-  Notice.getStream() << expr::ExprDag(dag);
   CVC5Message.getStream() << expr::ExprDag(dag);
   Warning.getStream() << expr::ExprDag(dag);
 }

diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 28a09fc9c8f78a840fea304ca69b09c6a3392bc0..c178ccebf9855bbe61c4d660fd55978a86d4f198 100644 (file)
--- a/src/proof/proof_checker.cpp
+++ b/src/proof/proof_checker.cpp
@@ -207,7 +207,7 @@ Node ProofChecker::checkInternal(PfRule id,
   {
     if (useTrustedChecker)
     {
-      Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl;
+      out << "ProofChecker::check: trusting PfRule " << id << std::endl;
       // trusted checker
       return expected;
     }
@@ -275,8 +275,9 @@ void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
   if (it != d_checker.end())
   {
     // checker is already provided
-    Notice() << "ProofChecker::registerChecker: checker already exists for "
-             << id << std::endl;
+    Trace("pfcheck")
+        << "ProofChecker::registerChecker: checker already exists for " << id
+        << std::endl;
     return;
   }
   d_checker[id] = psc;
@@ -293,9 +294,10 @@ void ProofChecker::registerTrustedChecker(PfRule id,
   // overwrites if already there
   if (d_plevel.find(id) != d_plevel.end())
   {
-    Notice() << "ProofChecker::registerTrustedRule: already provided pedantic "
-                "level for "
-             << id << std::endl;
+    Trace("proof-pedantic")
+        << "ProofChecker::registerTrustedRule: already provided pedantic "
+           "level for "
+        << id << std::endl;
   }
   d_plevel[id] = plevel;
 }

diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index 8b4b332a16fc5afed4b8b7f0df2143569f6317e2..72c39c59fc25893ea7328f46e7931932faaf9a48 100644 (file)
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -237,8 +237,9 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
     {
       if (acu.find(a) == acu.end())
       {
-        Notice() << "ProofNodeManager::mkScope: assumption " << a
-                 << " does not match a free assumption in proof" << std::endl;
+        Trace("pnm") << "ProofNodeManager::mkScope: assumption " << a
+                     << " does not match a free assumption in proof"
+                     << std::endl;
       }
     }
   }

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index e193bfb28a1991f1e765e4f6a92d950f4fb7fda9..a681aa4f118a1e80319881f3ef0d368601f201fe 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -30,8 +30,12 @@ namespace prop {
 
 //// DPllMinisatSatSolver
 
-MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
-    : d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry)
+MinisatSatSolver::MinisatSatSolver(Env& env, StatisticsRegistry& registry)
+    : EnvObj(env),
+      d_minisat(NULL),
+      d_context(NULL),
+      d_assumptions(),
+      d_statistics(registry)
 {}
 
 MinisatSatSolver::~MinisatSatSolver()
@@ -108,20 +112,22 @@ void MinisatSatSolver::initialize(context::Context* context,
 {
   d_context = context;
 
-  if (options::decisionMode() != options::DecisionMode::INTERNAL)
+  if (options().decision.decisionMode != options::DecisionMode::INTERNAL)
   {
-    Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)"
-             << " unless using internal decision strategy." << std::endl;
+    verbose(1) << "minisat: Incremental solving is forced on (to avoid "
+                  "variable elimination)"
+               << " unless using internal decision strategy." << std::endl;
   }
 
   // Create the solver
-  d_minisat = new Minisat::SimpSolver(
-      theoryProxy,
-      d_context,
-      userContext,
-      pnm,
-      options::incrementalSolving()
-          || options::decisionMode() != options::DecisionMode::INTERNAL);
+  d_minisat =
+      new Minisat::SimpSolver(theoryProxy,
+                              d_context,
+                              userContext,
+                              pnm,
+                              options().base.incrementalSolving
+                                  || options().decision.decisionMode
+                                         != options::DecisionMode::INTERNAL);
 
   d_statistics.init(d_minisat);
 }
@@ -132,20 +138,21 @@ void MinisatSatSolver::setupOptions() {
   // Copy options from cvc5 options structure into minisat, as appropriate
 
   // Set up the verbosity
-  d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
+  d_minisat->verbosity = (options().base.verbosity > 0) ? 1 : -1;
 
   // Set up the random decision parameters
-  d_minisat->random_var_freq = options::satRandomFreq();
+  d_minisat->random_var_freq = options().prop.satRandomFreq;
   // If 0, we use whatever we like (here, the Minisat default seed)
-  if(options::satRandomSeed() != 0) {
-    d_minisat->random_seed = double(options::satRandomSeed());
+  if (options().prop.satRandomSeed != 0)
+  {
+    d_minisat->random_seed = double(options().prop.satRandomSeed);
   }
 
   // Give access to all possible options in the sat solver
-  d_minisat->var_decay = options::satVarDecay();
-  d_minisat->clause_decay = options::satClauseDecay();
-  d_minisat->restart_first = options::satRestartFirst();
-  d_minisat->restart_inc = options::satRestartInc();
+  d_minisat->var_decay = options().prop.satVarDecay;
+  d_minisat->clause_decay = options().prop.satClauseDecay;
+  d_minisat->restart_first = options().prop.satRestartFirst;
+  d_minisat->restart_inc = options().prop.satRestartInc;
 }
 
 ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
@@ -159,7 +166,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   }
   d_minisat->addClause(minisat_clause, removable, clause_id);
   // FIXME: to be deleted when we kill old proof code for unsat cores
-  Assert(!options::unsatCores() || options::produceProofs()
+  Assert(!options().smt.unsatCores || options().smt.produceProofs
          || clause_id != ClauseIdError);
   return clause_id;
 }

diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 984cc6479f15e35b3a6300b204fc2affb4d2bb71..ef2cca6f0645bfe8178ff82326d227ca14f028b2 100644 (file)
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -17,8 +17,9 @@
 
 #pragma once
 
-#include "prop/sat_solver.h"
 #include "prop/minisat/simp/SimpSolver.h"
+#include "prop/sat_solver.h"
+#include "smt/env_obj.h"
 #include "util/statistics_registry.h"
 
 namespace cvc5 {
@@ -32,10 +33,10 @@ void toSatClause(const typename Solver::TClause& minisat_cl,
 
 namespace prop {
 
-class MinisatSatSolver : public CDCLTSatSolverInterface
+class MinisatSatSolver : public CDCLTSatSolverInterface, protected EnvObj
 {
  public:
-  MinisatSatSolver(StatisticsRegistry& registry);
+  MinisatSatSolver(Env& env, StatisticsRegistry& registry);
   ~MinisatSatSolver() override;
 
   static SatVariable     toSatVariable(Minisat::Var var);

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 0e911a49544fc16e444884dab2e6a24ba203accf..eeca414e2b5d042ab0db9c6990fbb2e4b9e66301 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -99,7 +99,8 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env)
     d_decisionEngine.reset(new decision::DecisionEngineEmpty(env));
   }
 
-  d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());
+  d_satSolver =
+      SatSolverFactory::createCDCLTMinisat(d_env, smtStatisticsRegistry());
 
   // CNF stream and theory proxy required pointers to each other, make the
   // theory proxy first

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 7852fc4e740b6289ab8f0ff244a1d3dc33a1b8ed..dfd660ace616a11bf3d8f78ded522e9c0ed2edcf 100644 (file)
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -24,9 +24,9 @@ namespace cvc5 {
 namespace prop {
 
 MinisatSatSolver* SatSolverFactory::createCDCLTMinisat(
-    StatisticsRegistry& registry)
+    Env& env, StatisticsRegistry& registry)
 {
-  return new MinisatSatSolver(registry);
+  return new MinisatSatSolver(env, registry);
 }
 
 SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry,

diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index c997a1ab8f53c3137957dde6423de5d77a130b68..fce8e31e280a8fbc676ff16f73e5970deb3e69c0 100644 (file)
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -32,7 +32,8 @@ namespace prop {
 class SatSolverFactory
 {
  public:
-  static MinisatSatSolver* createCDCLTMinisat(StatisticsRegistry& registry);
+  static MinisatSatSolver* createCDCLTMinisat(Env& env,
+                                              StatisticsRegistry& registry);
 
   static SatSolver* createCryptoMinisat(StatisticsRegistry& registry,
                                         const std::string& name = "");

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index d7f654fc6fae78cfb71f30780dceb83f839c5fd6..7d546eae73afb79332a52b219d5d4efa498a151d 100644 (file)
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -36,10 +36,10 @@ void CheckModels::checkModel(TheoryModel* m,
                              const context::CDList<Node>& al,
                              bool hardFailure)
 {
-  // Throughout, we use Notice() to give diagnostic output.
+  // Throughout, we use verbose(1) to give diagnostic output.
   //
   // If this function is running, the user gave --check-model (or equivalent),
-  // and if Notice() is on, the user gave --verbose (or equivalent).
+  // and if verbose(1) is on, the user gave --verbose (or equivalent).
 
   // check-model is not guaranteed to succeed if approximate values were used.
   // Thus, we intentionally abort here.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 195f9e76d9c12b6066e59c8c8ade95d0d4a19dfb..895e41c964176df74fbd0a35de17de5f1dc32886 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -46,8 +46,8 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-SetDefaults::SetDefaults(bool isInternalSubsolver)
-    : d_isInternalSubsolver(isInternalSubsolver)
+SetDefaults::SetDefaults(Env& env, bool isInternalSubsolver)
+    : EnvObj(env), d_isInternalSubsolver(isInternalSubsolver)
 {
 }
 
@@ -100,7 +100,7 @@ void SetDefaults::setDefaultsPre(Options& opts)
   {
     if (opts.smt.unsatCoresModeWasSetByUser)
     {
-      Notice()
+      verbose(1)
           << "Overriding OFF unsat-core mode since cores were requested.\n";
     }
     opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
@@ -116,8 +116,8 @@ void SetDefaults::setDefaultsPre(Options& opts)
   {
     if (opts.smt.unsatCoresModeWasSetByUser)
     {
-      Notice() << "Forcing full-proof mode for unsat cores mode since proofs "
-                  "were requested.\n";
+      verbose(1) << "Forcing full-proof mode for unsat cores mode since proofs "
+                    "were requested.\n";
     }
     // enable unsat cores, because they are available as a consequence of proofs
     opts.smt.unsatCores = true;
@@ -129,7 +129,7 @@ void SetDefaults::setDefaultsPre(Options& opts)
   {
     if (opts.smt.produceProofsWasSetByUser)
     {
-      Notice()
+      verbose(1)
           << "Forcing proof production since new unsat cores were requested.\n";
     }
     opts.smt.produceProofs = true;
@@ -158,8 +158,8 @@ void SetDefaults::setDefaultsPre(Options& opts)
     {
       opts.smt.unsatCores = false;
       opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
-      Notice() << "SolverEngine: turning off produce-proofs due to "
-               << reasonNoProofs.str() << "." << std::endl;
+      verbose(1) << "SolverEngine: turning off produce-proofs due to "
+                 << reasonNoProofs.str() << "." << std::endl;
       opts.smt.produceProofs = false;
       opts.smt.checkProofs = false;
     }
@@ -207,7 +207,7 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
             "for the combination of bit-vectors with arrays or uinterpreted "
             "functions. Try --bitblast=lazy"));
       }
-      Notice()
+      verbose(1)
           << "SolverEngine: setting bit-blast mode to lazy to support model"
           << "generation" << std::endl;
       opts.bv.bitblastMode = options::BitblastMode::LAZY;
@@ -266,8 +266,8 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
       throw OptionException(std::string(
           "Ackermannization currently does not support model generation."));
     }
-    Notice() << "SolverEngine: turn off ackermannization to support model"
-             << "generation" << std::endl;
+    verbose(1) << "SolverEngine: turn off ackermannization to support model"
+               << "generation" << std::endl;
     opts.smt.ackermann = false;
   }
 
@@ -377,8 +377,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
        || opts.smt.produceProofs)
       && !opts.smt.produceAssertions)
   {
-    Notice() << "SolverEngine: turning on produce-assertions to support "
-             << "option requiring assertions." << std::endl;
+    verbose(1) << "SolverEngine: turning on produce-assertions to support "
+               << "option requiring assertions." << std::endl;
     opts.smt.produceAssertions = true;
   }
 
@@ -465,7 +465,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
             "bool-to-bv != off not supported with CBQI BV for quantified "
             "logics");
       }
-      Notice()
+      verbose(1)
           << "SolverEngine: turning off bool-to-bitvector to support CBQI BV"
           << std::endl;
       opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
@@ -477,7 +477,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck
           || usesSygus(opts)))
   {
-    Notice() << "SolverEngine: turning on produce-models" << std::endl;
+    verbose(1) << "SolverEngine: turning on produce-models" << std::endl;
     opts.smt.produceModels = true;
   }
   
@@ -582,8 +582,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       throw OptionException(
           "bool-to-bv=all not supported for non-bitvector logics.");
     }
-    Notice() << "SolverEngine: turning off bool-to-bv for non-bv logic: "
-             << logic.getLogicString() << std::endl;
+    verbose(1) << "SolverEngine: turning off bool-to-bv for non-bv logic: "
+               << logic.getLogicString() << std::endl;
     opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
   }
 
@@ -759,8 +759,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
         ss << "Cannot use " << sOptNoModel << " with model generation.";
         throw OptionException(ss.str());
       }
-      Notice() << "SolverEngine: turning off produce-models to support "
-               << sOptNoModel << std::endl;
+      verbose(1) << "SolverEngine: turning off produce-models to support "
+                 << sOptNoModel << std::endl;
       opts.smt.produceModels = false;
     }
     if (opts.smt.produceAssignments)
@@ -772,8 +772,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
            << " with model generation (produce-assignments).";
         throw OptionException(ss.str());
       }
-      Notice() << "SolverEngine: turning off produce-assignments to support "
-               << sOptNoModel << std::endl;
+      verbose(1) << "SolverEngine: turning off produce-assignments to support "
+                 << sOptNoModel << std::endl;
       opts.smt.produceAssignments = false;
     }
     if (opts.smt.checkModels)
@@ -785,8 +785,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
            << " with model generation (check-models).";
         throw OptionException(ss.str());
       }
-      Notice() << "SolverEngine: turning off check-models to support "
-               << sOptNoModel << std::endl;
+      verbose(1) << "SolverEngine: turning off check-models to support "
+                 << sOptNoModel << std::endl;
       opts.smt.checkModels = false;
     }
   }
@@ -840,8 +840,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     }
     else
     {
-      Notice() << "Cannot use --nl-cad without configuring with --poly."
-               << std::endl;
+      verbose(1) << "Cannot use --nl-cad without configuring with --poly."
+                 << std::endl;
       opts.arith.nlCad = false;
       opts.arith.nlExt = options::NlExtMode::FULL;
     }
@@ -903,7 +903,7 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
   // options that are automatically set to support proofs
   if (opts.bv.bvAssertInput)
   {
-    Notice()
+    verbose(1)
         << "Disabling bv-assert-input since it is incompatible with proofs."
         << std::endl;
     opts.bv.bvAssertInput = false;
@@ -913,8 +913,8 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
   if (opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
       && !opts.bv.bvSolverWasSetByUser)
   {
-    Notice() << "Forcing internal bit-vector solver due to proof production."
-             << std::endl;
+    verbose(1) << "Forcing internal bit-vector solver due to proof production."
+               << std::endl;
     opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
   }
   return false;
@@ -963,9 +963,9 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       reason << "unconstrained simplification";
       return true;
     }
-    Notice() << "SolverEngine: turning off unconstrained simplification to "
-                "support incremental solving"
-             << std::endl;
+    verbose(1) << "SolverEngine: turning off unconstrained simplification to "
+                  "support incremental solving"
+               << std::endl;
     opts.smt.unconstrainedSimp = false;
   }
   if (opts.bv.bitblastMode == options::BitblastMode::EAGER
@@ -982,9 +982,9 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       reason << "sygus inference";
       return true;
     }
-    Notice() << "SolverEngine: turning off sygus inference to support "
-                "incremental solving"
-             << std::endl;
+    verbose(1) << "SolverEngine: turning off sygus inference to support "
+                  "incremental solving"
+               << std::endl;
     opts.quantifiers.sygusInference = false;
   }
   if (opts.quantifiers.sygusInst)
@@ -994,9 +994,9 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
       reason << "sygus inst";
       return true;
     }
-    Notice() << "SolverEngine: turning off sygus inst to support "
-                "incremental solving"
-             << std::endl;
+    verbose(1) << "SolverEngine: turning off sygus inst to support "
+                  "incremental solving"
+               << std::endl;
     opts.quantifiers.sygusInst = false;
   }
   if (opts.smt.solveIntAsBV > 0)
@@ -1025,9 +1025,9 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "simplification";
       return true;
     }
-    Notice() << "SolverEngine: turning off simplification to support unsat "
-                "cores"
-             << std::endl;
+    verbose(1) << "SolverEngine: turning off simplification to support unsat "
+                  "cores"
+               << std::endl;
     opts.smt.simplificationMode = options::SimplificationMode::NONE;
   }
 
@@ -1038,8 +1038,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "learned rewrites";
       return true;
     }
-    Notice() << "SolverEngine: turning off learned rewrites to support "
-                "unsat cores\n";
+    verbose(1) << "SolverEngine: turning off learned rewrites to support "
+                  "unsat cores\n";
     opts.smt.learnedRewrite = false;
   }
 
@@ -1050,8 +1050,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "pseudoboolean rewrites";
       return true;
     }
-    Notice() << "SolverEngine: turning off pseudoboolean rewrites to support "
-                "unsat cores\n";
+    verbose(1) << "SolverEngine: turning off pseudoboolean rewrites to support "
+                  "unsat cores\n";
     opts.arith.pbRewrites = false;
   }
 
@@ -1062,8 +1062,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "sort inference";
       return true;
     }
-    Notice() << "SolverEngine: turning off sort inference to support unsat "
-                "cores\n";
+    verbose(1) << "SolverEngine: turning off sort inference to support unsat "
+                  "cores\n";
     opts.smt.sortInference = false;
   }
 
@@ -1074,8 +1074,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "pre-skolemization";
       return true;
     }
-    Notice() << "SolverEngine: turning off pre-skolemization to support "
-                "unsat cores\n";
+    verbose(1) << "SolverEngine: turning off pre-skolemization to support "
+                  "unsat cores\n";
     opts.quantifiers.preSkolemQuant = false;
   }
 
@@ -1086,8 +1086,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "bv-to-bool";
       return true;
     }
-    Notice() << "SolverEngine: turning off bitvector-to-bool to support "
-                "unsat cores\n";
+    verbose(1) << "SolverEngine: turning off bitvector-to-bool to support "
+                  "unsat cores\n";
     opts.bv.bitvectorToBool = false;
   }
 
@@ -1098,7 +1098,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "bool-to-bv != off";
       return true;
     }
-    Notice() << "SolverEngine: turning off bool-to-bv to support unsat cores\n";
+    verbose(1)
+        << "SolverEngine: turning off bool-to-bv to support unsat cores\n";
     opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
   }
 
@@ -1109,7 +1110,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "bv-intro-pow2";
       return true;
     }
-    Notice()
+    verbose(1)
         << "SolverEngine: turning off bv-intro-pow2 to support unsat cores";
     opts.bv.bvIntroducePow2 = false;
   }
@@ -1121,7 +1122,7 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "repeat-simp";
       return true;
     }
-    Notice()
+    verbose(1)
         << "SolverEngine: turning off repeat-simp to support unsat cores\n";
     opts.smt.repeatSimp = false;
   }
@@ -1133,8 +1134,8 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "global-negate";
       return true;
     }
-    Notice() << "SolverEngine: turning off global-negate to support unsat "
-                "cores\n";
+    verbose(1) << "SolverEngine: turning off global-negate to support unsat "
+                  "cores\n";
     opts.quantifiers.globalNegate = false;
   }
 
@@ -1150,9 +1151,9 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
       reason << "unconstrained simplification";
       return true;
     }
-    Notice() << "SolverEngine: turning off unconstrained simplification to "
-                "support unsat cores"
-             << std::endl;
+    verbose(1) << "SolverEngine: turning off unconstrained simplification to "
+                  "support unsat cores"
+               << std::endl;
     opts.smt.unconstrainedSimp = false;
   }
   return false;
@@ -1197,7 +1198,7 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const
     needsUf = true;
     if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic())
     {
-      Notice()
+      verbose(1)
           << "Enabling linear integer arithmetic because strings are enabled"
           << std::endl;
       log.enableTheory(THEORY_ARITH);
@@ -1206,8 +1207,8 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const
     }
     else if (!logic.areIntegersUsed())
     {
-      Notice() << "Enabling integer arithmetic because strings are enabled"
-               << std::endl;
+      verbose(1) << "Enabling integer arithmetic because strings are enabled"
+                 << std::endl;
       log.enableIntegers();
     }
     logic = log;
@@ -1218,8 +1219,8 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const
   {
     // 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;
+    verbose(1) << "Enabling UF because preSkolemQuantNested requires it."
+               << std::endl;
     needsUf = true;
   }
   if (needsUf
@@ -1245,8 +1246,8 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const
       LogicInfo log(logic.getUnlockedCopy());
       if (!needsUf)
       {
-        Notice() << "Enabling UF because " << logic << " requires it."
-                 << std::endl;
+        verbose(1) << "Enabling UF because " << logic << " requires it."
+                   << std::endl;
       }
       log.enableTheory(THEORY_UF);
       logic = log;
@@ -1259,8 +1260,8 @@ void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const
     {
       // enable integers
       LogicInfo log(logic.getUnlockedCopy());
-      Notice() << "Enabling integers because arithMLTrick requires it."
-               << std::endl;
+      verbose(1) << "Enabling integers because arithMLTrick requires it."
+                 << std::endl;
       log.enableIntegers();
       logic = log;
       logic.lock();
@@ -1288,8 +1289,8 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
 
   if (opts.quantifiers.instMaxLevel != -1)
   {
-    Notice() << "SolverEngine: turning off cbqi to support instMaxLevel"
-             << std::endl;
+    verbose(1) << "SolverEngine: turning off cbqi to support instMaxLevel"
+               << std::endl;
     opts.quantifiers.cegqi = false;
   }
 

diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 31e2c3e4151a2bcb4151d5ea5f1a86e6c684beed..24b39e205b43c24f4e27cb90c0ef8f171566f3f2 100644 (file)
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -17,6 +17,7 @@
 #define CVC5__SMT__SET_DEFAULTS_H
 
 #include "options/options.h"
+#include "smt/env_obj.h"
 #include "theory/logic_info.h"
 
 namespace cvc5 {
@@ -26,14 +27,14 @@ namespace smt {
  * Class responsible for setting default options, which includes managing
  * implied options and dependencies between the options and the logic.
  */
-class SetDefaults
+class SetDefaults : protected EnvObj
 {
  public:
   /**
    * @param isInternalSubsolver Whether we are setting the options for an
    * internal subsolver (see SolverEngine::isInternalSubsolver).
    */
-  SetDefaults(bool isInternalSubsolver);
+  SetDefaults(Env& env, bool isInternalSubsolver);
   /**
    * The purpose of this method is to set the default options and update the
    * logic info for an SMT engine.

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 12a86d5692aae923b95727b14f5707e6937e894e..6dc40ac8b2ed709dd2c9bacc6216a49eeb0a743c 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -179,7 +179,7 @@ void SolverEngine::finishInit()
 
   // 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);
+  SetDefaults sdefaults(*d_env, d_isInternalSubsolver);
   sdefaults.setDefaults(d_env->d_logic, getOptions());
 
   if (d_env->getOptions().smt.produceProofs)

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index fc68ddfc44a31fa0685393ead13601e356019402..dd4093e30ee73ca02d87a245eaef588be651a5fa 100644 (file)
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -133,7 +133,8 @@ Node SkolemCache::mkTypedSkolemCached(
       break;
     default:
     {
-      Notice() << "Don't know how to handle Skolem ID " << id << std::endl;
+      Trace("skolem-cache")
+          << "Don't know how to handle Skolem ID " << id << std::endl;
       Node v = nm->mkBoundVar(tn);
       Node cond = nm->mkConst(true);
       sk = sm->mkSkolem(v, cond, c, "string skolem");

diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp
index 4d6bade9528e299acf0f0f9e81a77e6e3754a975..719b76cab89e98bdd96d32d3d0117d5890232402 100644 (file)
--- a/test/unit/theory/theory_arith_cad_white.cpp
+++ b/test/unit/theory/theory_arith_cad_white.cpp
@@ -349,7 +349,7 @@ void test_delta(const std::vector<Node>& a)
     std::cout << "Collected MIS: " << mis << std::endl;
     Assert(!mis.empty()) << "Infeasible subset can not be empty";
     Node lem = NodeManager::currentNM()->mkAnd(mis).negate();
-    Notice() << "UNSAT with MIS: " << lem << std::endl;
+    std::cout << "UNSAT with MIS: " << lem << std::endl;
   }
 }
 

diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index e1d8032277d951b5f9823223d54fd0edbdb31a58..72067c496c77510770128a01ef58ce3bf1ec14dd 100644 (file)
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -30,13 +30,11 @@ class TestUtilBlackOutput : public TestInternal
     TestInternal::SetUp();
     DebugChannel.setStream(&d_debugStream);
     TraceChannel.setStream(&d_traceStream);
-    NoticeChannel.setStream(&d_noticeStream);
     MessageChannel.setStream(&d_messageStream);
     WarningChannel.setStream(&d_warningStream);
 
     d_debugStream.str("");
     d_traceStream.str("");
-    d_noticeStream.str("");
     d_messageStream.str("");
     d_warningStream.str("");
   }
@@ -52,7 +50,6 @@ class TestUtilBlackOutput : public TestInternal
   }
   std::stringstream d_debugStream;
   std::stringstream d_traceStream;
-  std::stringstream d_noticeStream;
   std::stringstream d_messageStream;
   std::stringstream d_warningStream;
 };
@@ -68,7 +65,6 @@ TEST_F(TestUtilBlackOutput, output)
 
   CVC5Message() << "a message";
   Warning() << "bad warning!";
-  Notice() << "note";
 
   Trace.on("foo");
   Trace("foo") << "tracing1";
@@ -82,7 +78,6 @@ TEST_F(TestUtilBlackOutput, output)
   ASSERT_EQ(d_debugStream.str(), "");
   ASSERT_EQ(d_messageStream.str(), "");
   ASSERT_EQ(d_warningStream.str(), "");
-  ASSERT_EQ(d_noticeStream.str(), "");
   ASSERT_EQ(d_traceStream.str(), "");
 
 #else /* CVC5_MUZZLE */
@@ -95,7 +90,6 @@ TEST_F(TestUtilBlackOutput, output)
 
   ASSERT_EQ(d_messageStream.str(), "a message");
   ASSERT_EQ(d_warningStream.str(), "bad warning!");
-  ASSERT_EQ(d_noticeStream.str(), "note");
 
 #ifdef CVC5_TRACING
   ASSERT_EQ(d_traceStream.str(), "tracing1tracing3");
@@ -131,7 +125,6 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   ASSERT_FALSE(Trace.isOn("foo"));
   ASSERT_FALSE(Warning.isOn());
   ASSERT_FALSE(CVC5Message.isOn());
-  ASSERT_FALSE(Notice.isOn());
 
   cout << "debug" << std::endl;
   Debug("foo") << failure() << std::endl;
@@ -141,8 +134,6 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   Warning() << failure() << std::endl;
   cout << "message" << std::endl;
   CVC5Message() << failure() << std::endl;
-  cout << "notice" << std::endl;
-  Notice() << failure() << std::endl;
 #endif
 }
 
@@ -176,10 +167,6 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_messageStream.str(), std::string());
   d_messageStream.str("");
 
-  Notice() << "baz foo";
-  ASSERT_EQ(d_noticeStream.str(), std::string());
-  d_noticeStream.str("");
-
 #else /* CVC5_MUZZLE */
 
   Debug.off("yo");
@@ -216,10 +203,6 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_messageStream.str(), std::string("baz foo"));
   d_messageStream.str("");
 
-  Notice() << "baz foo";
-  ASSERT_EQ(d_noticeStream.str(), std::string("baz foo"));
-  d_noticeStream.str("");
-
 #endif /* CVC5_MUZZLE */
 }
 }  // namespace test