1 files changed, 22 insertions, 19 deletions

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 0bf2ed2ea..cb42f09d5 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -67,12 +67,12 @@ void TheorySets::finishInit()
   d_valuation.setUnevaluatedKind(WITNESS);
 
   // functions we are doing congruence over
-  d_equalityEngine->addFunctionKind(kind::SINGLETON);
-  d_equalityEngine->addFunctionKind(kind::UNION);
-  d_equalityEngine->addFunctionKind(kind::INTERSECTION);
-  d_equalityEngine->addFunctionKind(kind::SETMINUS);
-  d_equalityEngine->addFunctionKind(kind::MEMBER);
-  d_equalityEngine->addFunctionKind(kind::SUBSET);
+  d_equalityEngine->addFunctionKind(SINGLETON);
+  d_equalityEngine->addFunctionKind(UNION);
+  d_equalityEngine->addFunctionKind(INTERSECTION);
+  d_equalityEngine->addFunctionKind(SETMINUS);
+  d_equalityEngine->addFunctionKind(MEMBER);
+  d_equalityEngine->addFunctionKind(SUBSET);
   // relation operators
   d_equalityEngine->addFunctionKind(PRODUCT);
   d_equalityEngine->addFunctionKind(JOIN);
@@ -88,14 +88,20 @@ void TheorySets::finishInit()
   d_internal->finishInit();
 }
 
-void TheorySets::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); }
+void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
 
-void TheorySets::check(Effort e) {
-  if (done() && e < Theory::EFFORT_FULL) {
-    return;
-  }
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-  d_internal->check(e);
+bool TheorySets::preNotifyFact(
+    TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
+{
+  return d_internal->preNotifyFact(atom, polarity, fact);
+}
+
+void TheorySets::notifyFact(TNode atom,
+                            bool polarity,
+                            TNode fact,
+                            bool isInternal)
+{
+  d_internal->notifyFact(atom, polarity, fact);
 }
 
 bool TheorySets::collectModelValues(TheoryModel* m,
@@ -114,15 +120,12 @@ TrustNode TheorySets::explain(TNode node)
   return TrustNode::mkTrustPropExp(node, exp, nullptr);
 }
 
-EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) {
-  return d_internal->getEqualityStatus(a, b);
-}
-
 Node TheorySets::getModelValue(TNode node) {
   return Node::null();
 }
 
-void TheorySets::preRegisterTerm(TNode node) {
+void TheorySets::preRegisterTerm(TNode node)
+{
   d_internal->preRegisterTerm(node);
 }
 
@@ -158,7 +161,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubsti
   Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
 
   // this is based off of Theory::ppAssert
-  if (in.getKind() == kind::EQUAL)
+  if (in.getKind() == EQUAL)
   {
     if (in[0].isVar() && isLegalElimination(in[0], in[1]))
     {