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().

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index fe941a7fb49c520fd92645dd90d1762c901aeb34..918f73a534d43a7c21d7464271c462c49abbc94a 100644 (file)
--- 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 cfa8f82cfdbca6527c6f5f0c3042212cf676b9b6..bec5c7416d403295ec162f07fdd89ba47e5e6848 100644 (file)
--- 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 67c460615be216ef10a2660e331814f0aa59f9b8..56b27f6f02605605c8c626f71f7001b7f9b37166 100644 (file)
--- 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<Assertion> d_facts;
-
-  /** Index into the head of the facts list */
-  context::CDO<unsigned> d_factsHead;
-
-  /** Indices for splitting on the shared terms. */
-  context::CDO<unsigned> 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<Assertion> 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<unsigned> d_factsHead;
 
-  return fact;
-}
+  /** Indices for splitting on the shared terms. */
+  context::CDO<unsigned> 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)