From 4669bb1ab2fce322cd8e3e172e57f0aa3006e1d7 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 4 Nov 2021 18:16:12 -0700 Subject: [PATCH] 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. --- src/preprocessing/passes/miplib_trick.cpp | 4 --- src/preprocessing/passes/sep_skolem_emp.cpp | 2 +- src/smt/env.cpp | 5 ++++ src/smt/env.h | 3 ++ src/smt/preprocessor.cpp | 2 +- src/smt/process_assertions.cpp | 2 +- src/smt/proof_post_processor.cpp | 9 +++--- src/smt/proof_post_processor.h | 9 ++---- src/smt/set_defaults.cpp | 2 +- src/smt/solver_engine.cpp | 10 +++---- src/theory/arith/linear_equality.cpp | 17 ----------- src/theory/arith/linear_equality.h | 4 --- src/theory/arith/nl/cad_solver.cpp | 10 ++++--- src/theory/arith/nl/cad_solver.h | 4 +-- src/theory/arith/nl/poly_conversion.cpp | 2 +- src/theory/arith/tableau.h | 4 +-- src/theory/arith/theory_arith.cpp | 4 +-- src/theory/arith/theory_arith_private.cpp | 30 +++++++++---------- src/theory/booleans/circuit_propagator.cpp | 11 +++---- src/theory/booleans/circuit_propagator.h | 5 ++-- .../sygus/ce_guided_single_inv.cpp | 2 +- .../quantifiers/sygus/sygus_reconstruct.cpp | 4 +-- .../quantifiers/sygus/sygus_reconstruct.h | 5 ++-- .../quantifiers/sygus/synth_conjecture.cpp | 2 +- src/theory/uf/equality_engine.cpp | 10 +++---- src/theory/uf/equality_engine.h | 6 ++-- 26 files changed, 75 insertions(+), 93 deletions(-) diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 61be4395b..59f046262 100644 --- 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 dd85bec69..5d3a1112e 100644 --- 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 641360456..55beaed75 100644 --- 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& args, const std::vector& vals, diff --git a/src/smt/env.h b/src/smt/env.h index f94d8efea..fd90386d7 100644 --- 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 1835e61db..41653b6ee 100644 --- 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 468b754cc..013954d49 100644 --- 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 17ea2c09c..56a759866 100644 --- 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 27adc5eed..e81e51588 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -23,6 +23,7 @@ #include #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 ee6aa28cf..195f9e76d 100644 --- 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 264e1ec0b..12a86d569 100644 --- 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 SolverEngine::reduceUnsatCore(const std::vector& 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 ab6339fd5..a0cc5499d 100644 --- 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 5f177835b..e4ca4fa60 100644 --- 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 a3dd77fd1..721308a3d 100644 --- 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& 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& 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 c13b13614..bedffcaa9 100644 --- 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 2b1ef0a2e..7fbe08b9f 100644 --- 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 edec26260..f9c690545 100644 --- 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 583b53d5e..269ca083b 100644 --- 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()); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 7ce45c374..732ed962e 100644 --- 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 9e53e24dd..741d35e9d 100644 --- 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 feef06a90..fa55e2711 100644 --- 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 33cfc09d3..833abdd22 100644 --- 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 3073a472d..e402bfb9e 100644 --- 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 4102db713..de10b76ea 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -22,6 +22,7 @@ #include #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; * 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>& 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 d068438ba..9c5b8a606 100644 --- 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 a62bf876c..4180fb674 100644 --- 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 232f90595..8f7ebda4e 100644 --- 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; -- 2.30.2