(new theory) Update TheoryUF to new interface (#4944)

This updates TheoryUF to use the 4 check callbacks instead of implementing check, and uses the official TheoryState object instead of its context::CDO<bool> d_conflict field.

It also makes a minor change to collectModelValues for const and to preNotifyFact to include an isInternal flag.

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;
 }