summaryrefslogtreecommitdiff
path: root/src/theory/theory.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r--src/theory/theory.cpp4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index e05363bf2..7e2b6df55 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -231,7 +231,7 @@ void Theory::collectTerms(TNode n, set<Node>& termSet) const
}
-void Theory::computeRelevantTerms(set<Node>& termSet) const
+void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
{
// Collect all terms appearing in assertions
context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
@@ -239,6 +239,8 @@ void Theory::computeRelevantTerms(set<Node>& termSet) const
collectTerms(*assert_it, termSet);
}
+ if (!includeShared) return;
+
// Add terms that are shared terms
context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
for (; shared_it != shared_it_end; ++shared_it) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback