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

1 files changed, 33 insertions, 46 deletions

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<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.
@@ -228,13 +199,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
    * most once, before solving.
@@ -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)