diff options
Diffstat (limited to 'src/theory/theory.cpp')
| -rw-r--r-- | src/theory/theory.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index f65a7c45c..50a5c4493 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -425,7 +425,7 @@ void Theory::computeRelevantTerms(std::set<Node>& termSet, bool includeShared) computeRelevantTermsInternal(termSet, irrKinds, includeShared); } -bool Theory::collectModelValues(TheoryModel* m, std::set<Node>& termSet) +bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { return true; } @@ -538,7 +538,7 @@ void Theory::check(Effort level) bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; // call the pre-notify method - if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered)) + if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false)) { // handled in theory-specific way that doesn't involve equality engine continue; @@ -566,7 +566,8 @@ bool Theory::preCheck(Effort level) { return false; } void Theory::postCheck(Effort level) {} -bool Theory::preNotifyFact(TNode atom, bool polarity, TNode fact, bool isPrereg) +bool Theory::preNotifyFact( + TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal) { return false; } |