Eliminate `Warning` macro in favor of `EnvObj::warning` (#7575)

This PR eliminates almost all usages of the Warning macro, replacing it mostly by calling EnvObj::warning.

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 61be4395ba70bc64250eccc665e3de0e98b010dc..59f0462625eb0c01afb6755fa28bc223c3c69ce6 100644 (file)
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -586,10 +586,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           Node newAssertion = var.eqNode(rewrite(sum));
           if (top_level_substs.hasSubstitution(newAssertion[0]))
           {
-            // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
-            // Warning() << "REPLACE         " << newAssertion[1] << endl;
-            // Warning() << "ORIG            " <<
-            // top_level_substs.getSubstitution(newAssertion[0]) << endl;
             Assert(top_level_substs.getSubstitution(newAssertion[0])
                    == newAssertion[1]);
           }

diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index dd85bec69041d1d71de34e3f5c4f676835a16d8d..5d3a1112e2fb293a8d4105fe5f22f1971fc5ceb1 100644 (file)
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -111,7 +111,7 @@ PreprocessingPassResult SepSkolemEmp::applyInternal(
   TypeNode locType, dataType;
   if (!d_preprocContext->getTheoryEngine()->getSepHeapTypes(locType, dataType))
   {
-    Warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
+    warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
                  "heap types during preprocessing"
               << std::endl;
     return PreprocessingPassResult::NO_CONFLICT;

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 641360456e805b8159cb1762acd6a09cce6dffa7..55beaed75ea38eae927a87c382a3005c65d219d1 100644 (file)
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -177,6 +177,11 @@ std::ostream& Env::verbose(int64_t level) const
   return cvc5::null_os;
 }
 
+std::ostream& Env::warning() const
+{
+  return verbose(0);
+}
+
 Node Env::evaluate(TNode n,
                    const std::vector<Node>& args,
                    const std::vector<Node>& vals,

diff --git a/src/smt/env.h b/src/smt/env.h
index f94d8efeac00dd49a134d08d7bbdc24a8c0a70c6..fd90386d7f66dab041f607c2647de6c254a701c4 100644 (file)
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -181,6 +181,9 @@ class Env
    */
   std::ostream& verbose(int64_t level) const;
 
+  /** Convenience wrapper for verbose(0). */
+  std::ostream& warning() const;
+
   /* Rewrite helpers--------------------------------------------------------- */
   /**
    * Evaluate node n under the substitution args -> vals. For details, see

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 1835e61db9b53e735b6c55ea13e96ccd276c829f..41653b6ee6bd102b8817431e6d376b6e024b43b6 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -39,7 +39,7 @@ Preprocessor::Preprocessor(Env& env,
                            SolverEngineStatistics& stats)
     : EnvObj(env),
       d_absValues(abs),
-      d_propagator(true, true),
+      d_propagator(env, true, true),
       d_assertionsProcessed(env.getUserContext(), false),
       d_exDefs(env),
       d_processor(env, stats),

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 468b754cc5ab24c723f6bd21c9f97c1e1a2c69d0..013954d493f85f8baecb0fa4055047fe339af7a6 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -447,7 +447,7 @@ void ProcessAssertions::dumpAssertions(const std::string& key, Assertions& as)
   // as definitions.
   if (!options().smt.produceAssertions)
   {
-    Warning()
+    warning()
         << "Assertions not available for dumping (use --produce-assertions)."
         << std::endl;
     return;

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 17ea2c09c021f3624331ea71109583ec22932ea5..56a7598662e83904210ed46e49a8cbe5ccb9f13e 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -40,7 +40,7 @@ ProofPostprocessCallback::ProofPostprocessCallback(Env& env,
                                                    ProofGenerator* pppg,
                                                    rewriter::RewriteDb* rdb,
                                                    bool updateScopedAssumptions)
-    : d_env(env),
+    : EnvObj(env),
       d_pnm(env.getProofNodeManager()),
       d_pppg(pppg),
       d_wfpm(env),
@@ -959,7 +959,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     // substitution.
     if (pfn == nullptr)
     {
-      Warning() << "resort to TRUST_SUBS" << std::endl
+      warning() << "resort to TRUST_SUBS" << std::endl
                 << eq << std::endl
                 << eqq << std::endl
                 << "from " << children << " applied to " << t << std::endl;
@@ -1233,10 +1233,11 @@ ProofPostproccess::ProofPostproccess(Env& env,
                                      ProofGenerator* pppg,
                                      rewriter::RewriteDb* rdb,
                                      bool updateScopedAssumptions)
-    : d_cb(env, pppg, rdb, updateScopedAssumptions),
+    : EnvObj(env),
+      d_cb(env, pppg, rdb, updateScopedAssumptions),
       // the update merges subproofs
       d_updater(
-          env.getProofNodeManager(), d_cb, env.getOptions().proof.proofPpMerge),
+          env.getProofNodeManager(), d_cb, options().proof.proofPpMerge),
       d_finalCb(env.getProofNodeManager()),
       d_finalizer(env.getProofNodeManager(), d_finalCb)
 {

diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index 27adc5eed7b79e63592e0e72c64f454e7e7ca285..e81e515889fa4c71f7a26ed285b5d9713755d8c3 100644 (file)
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -23,6 +23,7 @@
 #include <unordered_set>
 
 #include "proof/proof_node_updater.h"
+#include "smt/env_obj.h"
 #include "smt/proof_final_callback.h"
 #include "smt/witness_form.h"
 #include "theory/inference_id.h"
@@ -30,8 +31,6 @@
 
 namespace cvc5 {
 
-class Env;
-
 namespace rewriter {
 class RewriteDb;
 }
@@ -42,7 +41,7 @@ namespace smt {
  * A callback class used by SolverEngine for post-processing proof nodes by
  * connecting proofs of preprocessing, and expanding macro PfRule applications.
  */
-class ProofPostprocessCallback : public ProofNodeUpdaterCallback
+class ProofPostprocessCallback : public ProofNodeUpdaterCallback, protected EnvObj
 {
  public:
   ProofPostprocessCallback(Env& env,
@@ -77,8 +76,6 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
  private:
   /** Common constants */
   Node d_true;
-  /** Reference to the env */
-  Env& d_env;
   /** Pointer to the proof node manager */
   ProofNodeManager* d_pnm;
   /** The preprocessing proof generator */
@@ -248,7 +245,7 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
  * (1) Connect proofs of preprocessing,
  * (2) Expand macro PfRule applications.
  */
-class ProofPostproccess
+class ProofPostproccess : protected EnvObj
 {
  public:
   /**

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index ee6aa28cfb30e265330c39e54edbbd8f7f13e675..195f9e76d9c12b6066e59c8c8ade95d0d4a19dfb 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -722,7 +722,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     {
       if (opts.theory.relevanceFilterWasSetByUser)
       {
-        Warning() << "SolverEngine: turning on relevance filtering to support "
+        Trace("smt") << "SolverEngine: turning on relevance filtering to support "
                      "--nl-ext-rlv="
                   << opts.arith.nlRlvMode << std::endl;
       }

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 264e1ec0bd6d2fb11ca3206dbe1e97bfc7c7d1e5..12a86d5692aae923b95727b14f5707e6937e894e 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -284,7 +284,7 @@ SolverEngine::~SolverEngine()
   }
   catch (Exception& e)
   {
-    Warning() << "cvc5 threw an exception during cleanup." << endl << e << endl;
+    d_env->warning() << "cvc5 threw an exception during cleanup." << std::endl << e << std::endl;
   }
 }
 
@@ -358,7 +358,7 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value)
   {
     if (value != "2" && value != "2.6")
     {
-      Warning() << "SMT-LIB version " << value
+      d_env->warning() << "SMT-LIB version " << value
                 << " unsupported, defaulting to language (and semantics of) "
                    "SMT-LIB 2.6\n";
     }
@@ -1341,7 +1341,7 @@ std::vector<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& core)
     }
     else if (r.asSatisfiabilityResult().isUnknown())
     {
-      Warning()
+      d_env->warning()
           << "SolverEngine::reduceUnsatCore(): could not reduce unsat core "
              "due to "
              "unknown result.";
@@ -1415,7 +1415,7 @@ void SolverEngine::checkUnsatCore()
                     << std::endl;
   if (r.asSatisfiabilityResult().isUnknown())
   {
-    Warning() << "SolverEngine::checkUnsatCore(): could not check core result "
+    d_env->warning() << "SolverEngine::checkUnsatCore(): could not check core result "
                  "unknown."
               << std::endl;
   }
@@ -1618,7 +1618,7 @@ Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
   const LogicInfo& logic = getLogicInfo();
   if (!logic.isPure(THEORY_ARITH) && strict)
   {
-    Warning() << "Unexpected logic for quantifier elimination " << logic
+    d_env->warning() << "Unexpected logic for quantifier elimination " << logic
               << endl;
   }
   return d_quantElimSolver->getQuantifierElimination(

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index ab6339fd50456db6de431d5094ac04bd2e42c881..a0cc5499de7b53dfa9af3779e0f14d112cf8182a 100644 (file)
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -403,23 +403,6 @@ void LinearEqualityModule::debugCheckTableau(){
     Assert(sum == shouldBe);
   }
 }
-bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){
-  bool result = true;
-  for(ArithVar var = 0, end = d_tableau.getNumColumns(); var != end; ++var){
-    //  for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
-    //ArithVar var = d_arithvarNodeMap.asArithVar(*i);
-    if(!d_variables.assignmentIsConsistent(var)){
-      d_variables.printModel(var);
-      Warning() << s << ":" << "Assignment is not consistent for " << var ;
-      if(d_tableau.isBasic(var)){
-        Warning() << " (basic)";
-      }
-      Warning() << endl;
-      result = false;
-    }
-  }
-  return result;
-}
 
 DeltaRational LinearEqualityModule::computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const {
   DeltaRational sum(0,0);

diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 5f177835b47196dace310a9837f9f8ef0028951c..e4ca4fa600a9310383529301d81a6d8d31530e21 100644 (file)
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -653,10 +653,6 @@ public:
   /** Debugging information for a pivot. */
   void debugPivot(ArithVar x_i, ArithVar x_j);
 
-  /** Checks the tableau + partial model for consistency. */
-  bool debugEntireLinEqIsConsistent(const std::string& s);
-
-
   ArithVar minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const;
 
   /**

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index a3dd77fd12add26d029ee647a17fdd3c4aee4718..721308a3d34e9556aa58e305d822255248b7a12b 100644 (file)
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -16,6 +16,7 @@
 #include "theory/arith/nl/cad_solver.h"
 
 #include "expr/skolem_manager.h"
+#include "smt/env.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/nl_model.h"
@@ -29,6 +30,7 @@ namespace nl {
 
 CadSolver::CadSolver(Env& env, InferenceManager& im, NlModel& model)
     :
+      EnvObj(env),
 #ifdef CVC5_POLY_IMP
       d_CAC(env),
 #endif
@@ -72,7 +74,7 @@ void CadSolver::initLastCall(const std::vector<Node>& assertions)
   d_CAC.computeVariableOrdering();
   d_CAC.retrieveInitialAssignment(d_model, d_ranVariable);
 #else
-  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
+  warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."
             << std::endl;
 #endif
@@ -104,7 +106,7 @@ void CadSolver::checkFull()
     d_im.addPendingLemma(lem, InferenceId::ARITH_NL_CAD_CONFLICT, proof);
   }
 #else
-  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
+  warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."
             << std::endl;
 #endif
@@ -154,7 +156,7 @@ void CadSolver::checkPartial()
     }
   }
 #else
-  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
+  warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."
             << std::endl;
 #endif
@@ -199,7 +201,7 @@ bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
   assertions.clear();
   return true;
 #else
-  Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
+  warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."
             << std::endl;
   return false;

diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index c13b13614e48198de9e6bae1ba2e57d2aea53522..bedffcaa9566e7943482a18b2c55600ed5de95e4 100644 (file)
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -20,7 +20,7 @@
 
 #include "context/context.h"
 #include "expr/node.h"
-#include "smt/env.h"
+#include "smt/env_obj.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/cad/proof_checker.h"
 
@@ -41,7 +41,7 @@ class NlModel;
  * A solver for nonlinear arithmetic that implements the CAD-based method
  * described in https://arxiv.org/pdf/2003.05633.pdf.
  */
-class CadSolver
+class CadSolver: protected EnvObj
 {
  public:
   CadSolver(Env& env, InferenceManager& im, NlModel& model);

diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index 2b1ef0a2e80f7f006945a3d3bef8f36c29cb0f9f..7fbe08b9f6e08c9fb7acccf6d221fbb614eaed92 100644 (file)
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -133,7 +133,7 @@ poly::UPolynomial as_poly_upolynomial_impl(const cvc5::Node& n,
       return res;
     }
     default:
-      Warning() << "Unhandled node " << n << " with kind " << n.getKind()
+      Assert(false) << "Unhandled node " << n << " with kind " << n.getKind()
                 << std::endl;
   }
   return poly::UPolynomial();

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index edec262605ddc5d222d3932682e61d187e4c4ba5..f9c6905459e3561850b2099ca9be7ea60ad46321 100644 (file)
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -65,9 +65,9 @@ public:
 
   void debugPrintIsBasic(ArithVar v) const {
     if(isBasic(v)){
-      Warning() << v << " is basic." << std::endl;
+      Debug("model") << v << " is basic." << std::endl;
     }else{
-      Warning() << v << " is non-basic." << std::endl;
+      Debug("model") << v << " is non-basic." << std::endl;
     }
   }
 

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 583b53d5e14da341ae7a7d934d8cf78981081b9a..269ca083b454a45389aa6e3d8022040b44c53724 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -386,9 +386,9 @@ bool TheoryArith::sanityCheckIntegerModel()
       Trace("arith-check") << p.first << " -> " << p.second << std::endl;
       if (p.first.getType().isInteger() && !p.second.getType().isInteger())
       {
-        Warning() << "TheoryArithPrivate generated a bad model value for "
+        warning() << "TheoryArithPrivate generated a bad model value for "
                      "integer variable "
-                  << p.first << " : " << p.second;
+                  << p.first << " : " << p.second << std::endl;
         // must branch and bound
         TrustNode lem =
             d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 7ce45c374b39d3d4030cef5b050bc3c97da2963f..732ed962ef27f8cfb9c514b3a5a09dc915e644d1 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3964,19 +3964,19 @@ bool TheoryArithPrivate::entireStateIsConsistent(const string& s){
     //ArithVar var = d_partialModel.asArithVar(*i);
     if(!d_partialModel.assignmentIsConsistent(var)){
       d_partialModel.printModel(var);
-      Warning() << s << ":" << "Assignment is not consistent for " << var << d_partialModel.asNode(var);
+      warning() << s << ":" << "Assignment is not consistent for " << var << d_partialModel.asNode(var);
       if(d_tableau.isBasic(var)){
-        Warning() << " (basic)";
+        warning() << " (basic)";
       }
-      Warning() << endl;
+      warning() << std::endl;
       result = false;
     }else if(d_partialModel.isInteger(var) && !d_partialModel.integralAssignment(var)){
       d_partialModel.printModel(var);
-      Warning() << s << ":" << "Assignment is not integer for integer variable " << var << d_partialModel.asNode(var);
+      warning() << s << ":" << "Assignment is not integer for integer variable " << var << d_partialModel.asNode(var);
       if(d_tableau.isBasic(var)){
-        Warning() << " (basic)";
+        warning() << " (basic)";
       }
-      Warning() << endl;
+      warning() << std::endl;
       result = false;
     }
   }
@@ -3991,19 +3991,19 @@ bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){
       if(!d_errorSet.inError(var)){
 
         d_partialModel.printModel(var);
-        Warning() << "Unenqueued var is not consistent for " << var <<  d_partialModel.asNode(var);
+        warning() << "Unenqueued var is not consistent for " << var <<  d_partialModel.asNode(var);
         if(d_tableau.isBasic(var)){
-          Warning() << " (basic)";
+          warning() << " (basic)";
         }
-        Warning() << endl;
+        warning() << std::endl;
         result = false;
       } else if(Debug.isOn("arith::consistency::initial")){
         d_partialModel.printModel(var);
-        Warning() << "Initial var is not consistent for " << var <<  d_partialModel.asNode(var);
+        warning() << "Initial var is not consistent for " << var <<  d_partialModel.asNode(var);
         if(d_tableau.isBasic(var)){
-          Warning() << " (basic)";
+          warning() << " (basic)";
         }
-        Warning() << endl;
+        warning() << std::endl;
       }
      }
   }
@@ -4119,10 +4119,10 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
                            << endl;
 
       if(bestImplied->negationHasProof()){
-        Warning() << "the negation of " <<  bestImplied << " : " << endl
-                  << "has proof " << bestImplied->getNegation() << endl
+        warning() << "the negation of " <<  bestImplied << " : " << std::endl
+                  << "has proof " << bestImplied->getNegation() << std::endl
                   << bestImplied->getNegation()->externalExplainByAssertions()
-                  << endl;
+                  << std::endl;
       }
 
       if(!assertedToTheTheory && canBePropagated && !hasProof ){

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 9e53e24dd3f988fbd9ba06d6d3fd60a2ba3abf6c..741d35e9d89d081a11ccaf1cc0b59ac612606d57 100644 (file)
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -34,8 +34,9 @@ namespace cvc5 {
 namespace theory {
 namespace booleans {
 
-CircuitPropagator::CircuitPropagator(bool enableForward, bool enableBackward)
-    : d_context(),
+CircuitPropagator::CircuitPropagator(Env& env, bool enableForward, bool enableBackward)
+    : EnvObj(env),
+      d_context(),
       d_propagationQueue(),
       d_propagationQueueClearer(&d_context, d_propagationQueue),
       d_conflict(&d_context, TrustNode()),
@@ -118,7 +119,7 @@ void CircuitPropagator::assignAndEnqueue(TNode n,
   {
     if (proof == nullptr)
     {
-      Warning() << "CircuitPropagator: Proof is missing for " << n << std::endl;
+      warning() << "CircuitPropagator: Proof is missing for " << n << std::endl;
       Assert(false);
     }
     else
@@ -127,7 +128,7 @@ void CircuitPropagator::assignAndEnqueue(TNode n,
       Node expected = value ? Node(n) : n.negate();
       if (proof->getResult() != expected)
       {
-        Warning() << "CircuitPropagator: Incorrect proof: " << expected
+        warning() << "CircuitPropagator: Incorrect proof: " << expected
                   << " vs. " << proof->getResult() << std::endl
                   << *proof << std::endl;
       }
@@ -741,7 +742,7 @@ TrustNode CircuitPropagator::propagate()
         }
         else
         {
-          Warning() << "CircuitPropagator: Proof is missing for " << lit
+          warning() << "CircuitPropagator: Proof is missing for " << lit
                     << std::endl;
           TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
           d_learnedLiterals.push_back(tlit);

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index feef06a90a3124dc22069beb93cb0b6fa72e5a3e..fa55e2711f7aae010783a4dff6e18926af3d6f37 100644 (file)
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -29,6 +29,7 @@
 #include "expr/node.h"
 #include "proof/lazy_proof_chain.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -45,7 +46,7 @@ namespace booleans {
  * the same fact is not output twice, so that the same edge in the
  * circuit isn't propagated twice, etc.
  */
-class CircuitPropagator
+class CircuitPropagator : protected EnvObj
 {
  public:
   /**
@@ -66,7 +67,7 @@ class CircuitPropagator
   /**
    * Construct a new CircuitPropagator.
    */
-  CircuitPropagator(bool enableForward = true, bool enableBackward = true);
+  CircuitPropagator(Env& env, bool enableForward = true, bool enableBackward = true);
 
   /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
   bool getAssignment(TNode n) const

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 33cfc09d37f10774c68f564693e175fc47592079..833abdd222701e327f8934c1f9c8f816e566d624 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -239,7 +239,7 @@ bool CegSingleInv::solve()
   Result::Sat res = r.asSatisfiabilityResult().isSat();
   if (res != Result::UNSAT)
   {
-    Warning() << "Warning : the single invocation solver determined the SyGuS "
+    warning() << "Warning : the single invocation solver determined the SyGuS "
                  "conjecture"
               << (res == Result::SAT ? " is" : " may be") << " infeasible"
               << std::endl;

diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index 3073a472d3eb13b71e7478248074a4b50cfa4d92..e402bfb9e3a5df09ba3131bd4070735c7e2cafd2 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
@@ -29,7 +29,7 @@ namespace quantifiers {
 SygusReconstruct::SygusReconstruct(Env& env,
                                    TermDbSygus* tds,
                                    SygusStatistics& s)
-    : d_env(env), d_tds(tds), d_stats(s)
+    : EnvObj(env), d_tds(tds), d_stats(s)
 {
 }
 
@@ -190,7 +190,7 @@ Node SygusReconstruct::reconstructSolution(Node sol,
 
   // we ran out of elements, return null
   reconstructed = -1;
-  Warning() << CommandFailure(
+  warning() << CommandFailure(
       "Cannot get synth function: reconstruction to syntax failed.");
   return Node::null();
 }

diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h
index 4102db713d9c892fc57666a7081251d84ed9dd35..de10b76ea225e1863d90708c3ff5b904e7464992 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.h
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h
@@ -22,6 +22,7 @@
 #include <vector>
 
 #include "expr/match_trie.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/sygus/rcons_obligation.h"
 #include "theory/quantifiers/sygus/rcons_type_info.h"
 
@@ -138,7 +139,7 @@ using NodePairMap = std::unordered_map<Node, Node>;
  *           push(Stack, k'')
  * }
  */
-class SygusReconstruct : public expr::NotifyMatch
+class SygusReconstruct : public expr::NotifyMatch, protected EnvObj
 {
  public:
   /**
@@ -298,8 +299,6 @@ class SygusReconstruct : public expr::NotifyMatch
   void printPool(
       const std::unordered_map<TypeNode, std::vector<Node>>& pool) const;
 
-  /** Reference to the env */
-  Env& d_env;
   /** pointer to the sygus term database */
   TermDbSygus* d_tds;
   /** reference to the statistics of parent */

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index d068438bae2c9f0598f1ff8900c4bd675542a9c0..9c5b8a6061cf6be8d005c0b5faccce9390116a0a 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -285,7 +285,7 @@ bool SynthConjecture::needsCheck()
     if (!value)
     {
       Trace("sygus-engine-debug") << "Conjecture is infeasible." << std::endl;
-      Warning() << "Warning : the SyGuS conjecture may be infeasible"
+      warning() << "Warning : the SyGuS conjecture may be infeasible"
                 << std::endl;
       return false;
     }

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index a62bf876c65cdd140dab9304a3230776d0f44fe4..4180fb674746a48e093fcdb5e24ec34686826886 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -106,8 +106,8 @@ EqualityEngine::EqualityEngine(Env& env,
                                bool constantsAreTriggers,
                                bool anyTermTriggers)
     : ContextNotifyObj(c),
+      EnvObj(env),
       d_masterEqualityEngine(0),
-      d_env(env),
       d_context(c),
       d_done(c, false),
       d_notify(&s_notifyNone),
@@ -137,9 +137,9 @@ EqualityEngine::EqualityEngine(Env& env,
                                bool constantsAreTriggers,
                                bool anyTermTriggers)
     : ContextNotifyObj(c),
+      EnvObj(env),
       d_masterEqualityEngine(nullptr),
       d_proofEqualityEngine(nullptr),
-      d_env(env),
       d_context(c),
       d_done(c, false),
       d_notify(&s_notifyNone),
@@ -1392,9 +1392,9 @@ void EqualityEngine::getExplanation(
                   || (d_done && isConstant(t1Id) && isConstant(t2Id));
 
   if (!canExplain) {
-    Warning() << "Can't explain equality:" << std::endl;
-    Warning() << d_nodes[t1Id] << " with find " << d_nodes[getEqualityNode(t1Id).getFind()] << std::endl;
-    Warning() << d_nodes[t2Id] << " with find " << d_nodes[getEqualityNode(t2Id).getFind()] << std::endl;
+    warning() << "Can't explain equality:" << std::endl;
+    warning() << d_nodes[t1Id] << " with find " << d_nodes[getEqualityNode(t1Id).getFind()] << std::endl;
+    warning() << d_nodes[t2Id] << " with find " << d_nodes[getEqualityNode(t2Id).getFind()] << std::endl;
   }
   Assert(canExplain);
 #endif

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 232f9059512f608a729c9fc5276b6cfe327e4167..8f7ebda4e610e988c940a5f4f4b49e0577b909e6 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -30,6 +30,7 @@
 #include "context/cdo.h"
 #include "expr/kind_map.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/theory_id.h"
 #include "theory/uf/equality_engine_iterator.h"
 #include "theory/uf/equality_engine_notify.h"
@@ -52,7 +53,7 @@ class ProofEqEngine;
  * Class for keeping an incremental congruence closure over a set of terms. It provides
  * notifications via an EqualityEngineNotify object.
  */
-class EqualityEngine : public context::ContextNotifyObj {
+class EqualityEngine : public context::ContextNotifyObj, protected EnvObj {
 
   friend class EqClassesIterator;
   friend class EqClassIterator;
@@ -130,9 +131,6 @@ class EqualityEngine : public context::ContextNotifyObj {
   };/* struct EqualityEngine::statistics */
 
  private:
-  /** The environment we are using */
-  Env& d_env;
-
   /** The context we are using */
   context::Context* d_context;