diff options
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 47 |
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. |