Standardization of Theory (#5181)

This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.

1 files changed, 13 insertions, 34 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index bc6c995a7..6f6c863df 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -179,15 +179,6 @@ class Theory {
    */
   context::CDList<TNode> d_sharedTerms;
 
-  //---------------------------------- private collect model info
-  /**
-   * Helper function for computeRelevantTerms
-   */
-  void collectTerms(TNode n,
-                    const std::set<Kind>& irrKinds,
-                    std::set<Node>& termSet) const;
-  //---------------------------------- end private collect model info
-
   /**
    * Construct a Theory.
    *
@@ -492,6 +483,16 @@ class Theory {
   DecisionManager* getDecisionManager() { return d_decManager; }
 
   /**
+   * @return The theory state associated with this theory.
+   */
+  TheoryState* getTheoryState() { return d_theoryState; }
+
+  /**
+   * @return The theory inference manager associated with this theory.
+   */
+  TheoryInferenceManager* getInferenceManager() { return d_inferManager; }
+
+  /**
    * Expand definitions in the term node. This returns a term that is
    * equivalent to node. It wraps this term in a TrustNode of kind
    * TrustNodeKind::REWRITE. If node is unchanged by this method, the
@@ -600,11 +601,8 @@ class Theory {
    *
    * Theories that use this check method must use an official theory
    * state object (d_theoryState).
-   *
-   * TODO (project #39): this method should be non-virtual, once all theories
-   * conform to the new standard
    */
-  virtual void check(Effort level = EFFORT_FULL);
+  void check(Effort level = EFFORT_FULL);
   /**
    * Pre-check, called before the fact queue of the theory is processed.
    * If this method returns false, then the theory will process its fact
@@ -662,28 +660,9 @@ class Theory {
    * then calls computeModelValues.
    *
    * TODO (project #39): this method should be non-virtual, once all theories
-   * conform to the new standard
-   */
-  virtual bool collectModelInfo(TheoryModel* m);
-  /**
-   * Scans the current set of assertions and shared terms top-down
-   * until a theory-leaf is reached, and adds all terms found to
-   * termSet.  This is used by collectModelInfo to delimit the set of
-   * terms that should be used when constructing a model.
-   *
-   * @param irrKinds The kinds of terms that appear in assertions that should *not*
-   * be included in termSet. Note that the kinds EQUAL and NOT are always
-   * treated as irrelevant kinds.
-   *
-   * @param includeShared Whether to include shared terms in termSet. Notice that
-   * shared terms are not influenced by irrKinds.
-   *
-   * TODO (project #39): this method will be deleted. The version in
-   * model manager will be used.
+   * conform to the new standard, delete, move to model manager distributed.
    */
-  void computeAssertedTerms(std::set<Node>& termSet,
-                            const std::set<Kind>& irrKinds,
-                            bool includeShared = true) const;
+  virtual bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet);
   /**
    * Compute terms that are not necessarily part of the assertions or
    * shared terms that should be considered relevant, add them to termSet.