Use state and inference manager in UF CardinalityExtension (#5036)

Previously, the cardinality extension of UF maintained its own (SAT-context-dependent) conflict flag, made custom calls to output channel, and maintained its own cache of lemmas. This standardizes the CardinalityExtension so that it uses state and inference manager of UF, which means that UF and the cardinality extension are fully syncronized concerning whether we are in a conflicting state at all times (d_state.isInConflict). It further cleans up some of the interfaces in CardinalityExtension. This required adding a forwarding method for setIncomplete in inference manager.

1 files changed, 2 insertions, 8 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index a58834891..0a48d4c71 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -90,8 +90,7 @@ void TheoryUF::finishInit() {
   if (options::finiteModelFind()
       && options::ufssMode() != options::UfssMode::NONE)
   {
-    d_thss.reset(new CardinalityExtension(
-        getSatContext(), getUserContext(), *d_out, this));
+    d_thss.reset(new CardinalityExtension(d_state, d_im, this));
   }
   // The kinds we are treating as function application in congruence
   d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
@@ -136,10 +135,6 @@ void TheoryUF::postCheck(Effort level)
   if (d_thss != nullptr)
   {
     d_thss->check(level);
-    if (d_thss->isConflict())
-    {
-      d_state.notifyInConflict();
-    }
   }
   // check with the higher-order extension
   if (!d_state.isInConflict() && fullEffort(level))
@@ -159,9 +154,8 @@ bool TheoryUF::preNotifyFact(
     bool isDecision =
         d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
     d_thss->assertNode(fact, isDecision);
-    if (d_thss->isConflict())
+    if (d_state.isInConflict())
     {
-      d_state.notifyInConflict();
       return true;
     }
   }