From 8c6752343ee49bed7abb03401c9411345b2dfe04 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 4 Nov 2021 07:44:43 -0700 Subject: [PATCH] Make `Theory::get()` private (#7518) Now that theories have been refactored to use common interfaces, they should not access Theory::get() anymore because facts are consumed by Theory::check(). --- src/theory/arith/theory_arith_private.h | 9 ++- src/theory/theory.cpp | 26 ++++++-- src/theory/theory.h | 79 +++++++++++-------------- 3 files changed, 57 insertions(+), 57 deletions(-) diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index fe941a7fb..918f73a53 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -684,11 +684,10 @@ private: /** Debugging only routine. Prints the model. */ void debugPrintModel(std::ostream& out) const; - inline bool done() const { return d_containing.done(); } - inline TNode get() { return d_containing.get(); } - inline bool isLeaf(TNode x) const { return d_containing.isLeaf(x); } - inline TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); } - inline void debugPrintFacts() const { d_containing.debugPrintFacts(); } + bool done() const { return d_containing.done(); } + bool isLeaf(TNode x) const { return d_containing.isLeaf(x); } + TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); } + void debugPrintFacts() const { d_containing.debugPrintFacts(); } bool outputTrustedLemma(TrustNode lem, InferenceId id); bool outputLemma(TNode lem, InferenceId id); void outputTrustedConflict(TrustNode conf, InferenceId id); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index cfa8f82cf..bec5c7416 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -65,11 +65,6 @@ Theory::Theory(TheoryId id, Valuation valuation, std::string name) : EnvObj(env), - d_id(id), - d_facts(d_env.getContext()), - d_factsHead(d_env.getContext(), 0), - d_sharedTermsIndex(d_env.getContext(), 0), - d_careGraph(nullptr), d_instanceName(name), d_checkTime(statisticsRegistry().registerTimer(getStatsPrefix(id) + name + "checkTime")), @@ -84,7 +79,12 @@ Theory::Theory(TheoryId id, d_inferManager(nullptr), d_quantEngine(nullptr), d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() - : nullptr) + : nullptr), + d_id(id), + d_facts(d_env.getContext()), + d_factsHead(d_env.getContext(), 0), + d_sharedTermsIndex(d_env.getContext(), 0), + d_careGraph(nullptr) { } @@ -683,5 +683,19 @@ bool Theory::expUsingCentralEqualityEngine(TheoryId id) return id != THEORY_ARITH && usesCentralEqualityEngine(id); } +theory::Assertion Theory::get() +{ + Assert(!done()) << "Theory::get() called with assertion queue empty!"; + + // Get the assertion + Assertion fact = d_facts[d_factsHead]; + d_factsHead = d_factsHead + 1; + + Trace("theory") << "Theory::get() => " << fact << " (" + << d_facts.size() - d_factsHead << " left)" << std::endl; + + return fact; +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/theory.h b/src/theory/theory.h index 67c460615..56b27f6f0 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -99,35 +99,6 @@ class Theory : protected EnvObj { friend class ::cvc5::TheoryEngine; - private: - // Disallow default construction, copy, assignment. - Theory() = delete; - Theory(const Theory&) = delete; - Theory& operator=(const Theory&) = delete; - - /** An integer identifying the type of the theory. */ - TheoryId d_id; - - /** - * The assertFact() queue. - * - * These can not be TNodes as some atoms (such as equalities) are sent - * across theories without being stored in a global map. - */ - context::CDList d_facts; - - /** Index into the head of the facts list */ - context::CDO d_factsHead; - - /** Indices for splitting on the shared terms. */ - context::CDO d_sharedTermsIndex; - - /** The care graph the theory will use during combination. */ - CareGraph* d_careGraph; - - /** Pointer to the decision manager. */ - DecisionManager* d_decManager; - protected: /** Name of this theory instance. Along with the TheoryId this should * provide an unique string identifier for each instance of a Theory class. @@ -227,13 +198,6 @@ class Theory : protected EnvObj */ bool proofsEnabled() const; - /** - * Returns the next assertion in the assertFact() queue. - * - * @return the next assertion in the assertFact() queue - */ - inline Assertion get(); - /** * Set separation logic heap. This is called when the location and data * types for separation logic are determined. This should be called at @@ -858,22 +822,45 @@ class Theory : protected EnvObj static bool usesCentralEqualityEngine(TheoryId id); /** Explains/propagates via central equality engine only */ static bool expUsingCentralEqualityEngine(TheoryId id); -}; /* class Theory */ -std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); + private: + // Disallow default construction, copy, assignment. + Theory() = delete; + Theory(const Theory&) = delete; + Theory& operator=(const Theory&) = delete; + /** + * Returns the next assertion in the assertFact() queue. + * + * @return the next assertion in the assertFact() queue + */ + Assertion get(); -inline theory::Assertion Theory::get() { - Assert(!done()) << "Theory::get() called with assertion queue empty!"; + /** An integer identifying the type of the theory. */ + TheoryId d_id; - // Get the assertion - Assertion fact = d_facts[d_factsHead]; - d_factsHead = d_factsHead + 1; + /** + * The assertFact() queue. + * + * These can not be TNodes as some atoms (such as equalities) are sent + * across theories without being stored in a global map. + */ + context::CDList d_facts; - Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; + /** Index into the head of the facts list */ + context::CDO d_factsHead; - return fact; -} + /** Indices for splitting on the shared terms. */ + context::CDO d_sharedTermsIndex; + + /** The care graph the theory will use during combination. */ + CareGraph* d_careGraph; + + /** Pointer to the decision manager. */ + DecisionManager* d_decManager; +}; /* class Theory */ + +std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); inline std::ostream& operator<<(std::ostream& out, const cvc5::theory::Theory& theory) -- 2.30.2