diff options
Diffstat (limited to 'src/theory/theory.h')
| -rw-r--r-- | src/theory/theory.h | 39 |
1 files changed, 26 insertions, 13 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 4feeac394..78c6e34cb 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -183,13 +183,7 @@ class Theory { */ context::CDList<TNode> d_sharedTerms; - /** - * Helper function for computeRelevantTerms - */ - void collectTerms(TNode n, - std::set<Kind>& irrKinds, - std::set<Node>& termSet) const; - + //---------------------------------- collect model info /** * Scans the current set of assertions and shared terms top-down * until a theory-leaf is reached, and adds all terms found to @@ -203,11 +197,30 @@ class Theory { * includeShared: Whether to include shared terms in termSet. Notice that * shared terms are not influenced by irrKinds. */ - void computeRelevantTerms(std::set<Node>& termSet, - std::set<Kind>& irrKinds, - bool includeShared = true) const; - /** same as above, but with empty irrKinds */ - void computeRelevantTerms(std::set<Node>& termSet, bool includeShared = true) const; + void computeRelevantTermsInternal(std::set<Node>& termSet, + std::set<Kind>& irrKinds, + bool includeShared = true) const; + /** + * Helper function for computeRelevantTerms + */ + void collectTerms(TNode n, + std::set<Kind>& irrKinds, + std::set<Node>& termSet) const; + /** + * Same as above, but with empty irrKinds. This version can be overridden + * by the theory, e.g. by restricting or extending the set of terms returned + * by computeRelevantTermsInternal, which is called by default with no + * irrKinds. + */ + virtual void computeRelevantTerms(std::set<Node>& termSet, + bool includeShared = true); + /** + * Collect model values, after equality information is added to the model. + * The argument termSet is the set of relevant terms returned by + * computeRelevantTerms. + */ + virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet); + //---------------------------------- end collect model info /** * Construct a Theory. @@ -619,7 +632,7 @@ class Theory { * This method returns true if and only if the equality engine of m is * consistent as a result of this call. */ - virtual bool collectModelInfo(TheoryModel* m) { return true; } + virtual bool collectModelInfo(TheoryModel* m); /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } /** |