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.

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index ff6f0ebc7ec80585f2c28fa8b6673985d27837b6..81f5c45e6ca6bc89665a8198f82f2cdaf5fd9745 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -464,5 +464,7 @@ void TheoryInferenceManager::safePoint(ResourceManager::Resource r)
   d_out.safePoint(r);
 }
 
+void TheoryInferenceManager::setIncomplete() { d_out.setIncomplete(); }
+
 }  // namespace theory
 }  // namespace CVC4

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 496a7f0f1fb78e0576632d22d99ba57f92769119..e63d55366ec58744d33a956c831a35dfdc7d6eed 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -341,6 +341,11 @@ class TheoryInferenceManager
    * Forward to OutputChannel::safePoint() to spend resources.
    */
   void safePoint(ResourceManager::Resource r);
+  /**
+   * Notification from a theory that it realizes it is incomplete at
+   * this context level.
+   */
+  void setIncomplete();
 
  protected:
   /**

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 1f83c94d6bef3e6148d5a5166b3b2a441b79c12e..b35efc23a04decc05fdc91b9bd10c37d026be68c 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -183,7 +183,7 @@ void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
 void Region::setRep( Node n, bool valid ) {
   Assert(hasRep(n) != valid);
   if( valid && d_nodes.find( n )==d_nodes.end() ){
-    d_nodes[n] = new RegionNodeInfo( d_cf->d_thss->getSatContext() );
+    d_nodes[n] = new RegionNodeInfo(d_cf->d_state.getSatContext());
   }
   d_nodes[n]->setValid(valid);
   d_reps_size = d_reps_size + ( valid ? 1 : -1 );
@@ -460,22 +460,22 @@ std::string SortModel::CardinalityDecisionStrategy::identify() const
 }
 
 SortModel::SortModel(Node n,
-                     context::Context* c,
-                     context::UserContext* u,
+                     TheoryState& state,
+                     TheoryInferenceManager& im,
                      CardinalityExtension* thss)
     : d_type(n.getType()),
+      d_state(state),
+      d_im(im),
       d_thss(thss),
-      d_regions_index(c, 0),
-      d_regions_map(c),
-      d_split_score(c),
-      d_disequalities_index(c, 0),
-      d_reps(c, 0),
-      d_conflict(c, false),
-      d_cardinality(c, 1),
-      d_hasCard(c, false),
-      d_maxNegCard(c, 0),
-      d_initialized(u, false),
-      d_lemma_cache(u),
+      d_regions_index(d_state.getSatContext(), 0),
+      d_regions_map(d_state.getSatContext()),
+      d_split_score(d_state.getSatContext()),
+      d_disequalities_index(d_state.getSatContext(), 0),
+      d_reps(d_state.getSatContext(), 0),
+      d_cardinality(d_state.getSatContext(), 1),
+      d_hasCard(d_state.getSatContext(), false),
+      d_maxNegCard(d_state.getSatContext(), 0),
+      d_initialized(d_state.getUserContext(), false),
       d_c_dec_strat(nullptr)
 {
   d_cardinality_term = n;
@@ -486,7 +486,7 @@ SortModel::SortModel(Node n,
     // We are guaranteed that the decision manager is ready since we
     // construct this module during TheoryUF::finishInit.
     d_c_dec_strat.reset(new CardinalityDecisionStrategy(
-        n, c, thss->getTheory()->getValuation()));
+        n, d_state.getSatContext(), thss->getTheory()->getValuation()));
   }
 }
 
@@ -500,7 +500,8 @@ SortModel::~SortModel() {
 }
 
 /** initialize */
-void SortModel::initialize( OutputChannel* out ){
+void SortModel::initialize()
+{
   if (d_c_dec_strat.get() != nullptr && !d_initialized)
   {
     d_initialized = true;
@@ -513,14 +514,15 @@ void SortModel::initialize( OutputChannel* out ){
 
 /** new node */
 void SortModel::newEqClass( Node n ){
-  if( !d_conflict ){
+  if (!d_state.isInConflict())
+  {
     if( d_regions_map.find( n )==d_regions_map.end() ){
       // Must generate totality axioms for every cardinality we have
       // allocated thus far.
       for( std::map< int, Node >::iterator it = d_cardinality_literal.begin();
            it != d_cardinality_literal.end(); ++it ){
         if( applyTotality( it->first ) ){
-          addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() );
+          addTotalityAxiom(n, it->first);
         }
       }
       if( options::ufssTotality() ){
@@ -542,7 +544,7 @@ void SortModel::newEqClass( Node n ){
           d_regions[ d_regions_index ]->setValid(true);
           Assert(d_regions[d_regions_index]->getNumReps() == 0);
         }else{
-          d_regions.push_back( new Region( this, d_thss->getSatContext() ) );
+          d_regions.push_back(new Region(this, d_state.getSatContext()));
         }
         d_regions[ d_regions_index ]->addRep( n );
         d_regions_index = d_regions_index + 1;
@@ -554,7 +556,8 @@ void SortModel::newEqClass( Node n ){
 
 /** merge */
 void SortModel::merge( Node a, Node b ){
-  if( !d_conflict ){
+  if (!d_state.isInConflict())
+  {
     if( options::ufssTotality() ){
       if( d_regions_map[b]==-1 ){
         d_regions_map[a] = -1;
@@ -611,7 +614,8 @@ void SortModel::merge( Node a, Node b ){
 
 /** assert terms are disequal */
 void SortModel::assertDisequal( Node a, Node b, Node reason ){
-  if( !d_conflict ){
+  if (!d_state.isInConflict())
+  {
     if( options::ufssTotality() ){
       //do nothing
     }else{
@@ -670,9 +674,11 @@ bool SortModel::areDisequal( Node a, Node b ) {
 }
 
 /** check */
-void SortModel::check( Theory::Effort level, OutputChannel* out ){
+void SortModel::check(Theory::Effort level)
+{
   Assert(options::ufssMode() == options::UfssMode::FULL);
-  if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
+  if (level >= Theory::EFFORT_STANDARD && d_hasCard && !d_state.isInConflict())
+  {
     Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
                    << std::endl;
     if( level==Theory::EFFORT_FULL ){
@@ -699,7 +705,7 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
             std::vector< Node > clique;
             if( d_regions[i]->check( level, d_cardinality, clique ) ){
               //add clique lemma
-              addCliqueLemma( clique, out );
+              addCliqueLemma(clique);
               return;
             }else{
               Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
@@ -716,15 +722,14 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
           //see if we have any recommended splits from large regions
           for( int i=0; i<(int)d_regions_index; i++ ){
             if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){
-
-              int sp = addSplit( d_regions[i], out );
+              int sp = addSplit(d_regions[i]);
               if( sp==1 ){
                 addedLemma = true;
 #ifdef ONE_SPLIT_REGION
                 break;
 #endif
               }else if( sp==-1 ){
-                check( level, out );
+                check(level);
                 return;
               }
             }
@@ -771,7 +776,7 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
             }
             if( recheck ){
               Trace("uf-ss-debug") << "Must recheck." << std::endl;
-              check( level, out );
+              check(level);
             }
           }
         }
@@ -784,10 +789,6 @@ void SortModel::presolve() {
   d_initialized = false;
 }
 
-void SortModel::propagate( Theory::Effort level, OutputChannel* out ){
-
-}
-
 int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
   int ni = d_regions_map[n];
   int counter = 0;
@@ -832,8 +833,10 @@ void SortModel::setSplitScore( Node n, int s ){
   }
 }
 
-void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
-  if( !d_conflict ){
+void SortModel::assertCardinality(int c, bool val)
+{
+  if (!d_state.isInConflict())
+  {
     Trace("uf-ss-assert")
         << "Assert cardinality " << d_type << " " << c << " " << val
         << " level = "
@@ -847,7 +850,8 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
       if( !prevHasCard || c<d_cardinality ){
         d_cardinality = c;
         simpleCheckCardinality();
-        if( d_thss->d_conflict.get() ){
+        if (d_state.isInConflict())
+        {
           return;
         }
       }
@@ -856,7 +860,8 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
         for( int i=0; i<(int)d_regions_index; i++ ){
           if( d_regions[i]->valid() ){
             checkRegion( i );
-            if( d_conflict ){
+            if (d_state.isInConflict())
+            {
               return;
             }
           }
@@ -905,7 +910,7 @@ void SortModel::checkRegion( int ri, bool checkCombine ){
     std::vector< Node > clique;
     if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
       //explain clique
-      addCliqueLemma( clique, &d_thss->getOutputChannel() );
+      addCliqueLemma(clique);
     }
   }
 }
@@ -984,7 +989,8 @@ void SortModel::moveNode( Node n, int ri ){
   d_regions_map[n] = ri;
 }
 
-int SortModel::addSplit( Region* r, OutputChannel* out ){
+int SortModel::addSplit(Region* r)
+{
   Node s;
   if( r->hasSplits() ){
     //take the first split you find
@@ -1032,10 +1038,12 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
     //Notice() << "*** Split on " << s << std::endl;
     //split on the equality s
     Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
-    if( doSendLemma( lem ) ){
+    // send lemma, with caching
+    if (d_im.lemma(lem))
+    {
       Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
       //tell the sat solver to explore the equals branch first
-      out->requirePhase( ss, true );
+      d_im.requirePhase(ss, true);
       ++( d_thss->d_statistics.d_split_lemmas );
     }
     return 1;
@@ -1044,8 +1052,8 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
   }
 }
 
-
-void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
+void SortModel::addCliqueLemma(std::vector<Node>& clique)
+{
   Assert(d_hasCard);
   Assert(d_cardinality > 0);
   while( clique.size()>size_t(d_cardinality+1) ){
@@ -1062,14 +1070,16 @@ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out
   }
   eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
   Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
-  if (doSendLemma(lem))
+  // send lemma, with caching
+  if (d_im.lemma(lem))
   {
     Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
     ++(d_thss->d_statistics.d_clique_lemmas);
   }
 }
 
-void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
+void SortModel::addTotalityAxiom(Node n, int cardinality)
+{
   if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
     if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){
       NodeManager* nm = NodeManager::currentNM();
@@ -1103,7 +1113,7 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
               Node ax = eqs.size()==1 ? eqs[0] : NodeManager::currentNM()->mkNode( OR, eqs );
               Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax );
               Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl;
-              d_thss->getOutputChannel().lemma( lem );
+              d_im.lemma(lem, LemmaProperty::NONE, false);
             }
           }
         }
@@ -1117,7 +1127,7 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
       Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax );
       Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl;
       //send as lemma to the output channel
-      d_thss->getOutputChannel().lemma( lem );
+      d_im.lemma(lem, LemmaProperty::NONE, false);
       ++( d_thss->d_statistics.d_totality_lemmas );
     }
   }
@@ -1138,18 +1148,7 @@ void SortModel::simpleCheckCardinality() {
     Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
                                                       getCardinalityLiteral( d_maxNegCard.get() ).negate() );
     Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
-    d_thss->getOutputChannel().conflict( lem );
-    d_thss->d_conflict.set( true );
-  }
-}
-
-bool SortModel::doSendLemma( Node lem ) {
-  if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){
-    d_lemma_cache[lem] = true;
-    d_thss->getOutputChannel().lemma( lem );
-    return true;
-  }else{
-    return false;
+    d_im.conflict(lem);
   }
 }
 
@@ -1230,7 +1229,7 @@ bool SortModel::debugModel( TheoryModel* m ){
         Node cl = getCardinalityLiteral( d_maxNegCard );
         Node lem = NodeManager::currentNM()->mkNode( OR, cl, NodeManager::currentNM()->mkNode( AND, force_cl ) );
         Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
-        d_thss->getOutputChannel().lemma( lem );
+        d_im.lemma(lem, LemmaProperty::NONE, false);
         return false;
       }
     }
@@ -1294,40 +1293,39 @@ Node SortModel::getCardinalityLiteral(unsigned c)
     Node lem = var.eqNode(d_totality_terms[0][i - 1]).notNode();
     Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem
                          << std::endl;
-    d_thss->getOutputChannel().lemma(lem);
+    d_im.lemma(lem, LemmaProperty::NONE, false);
   }
   // must send totality axioms for each existing term
   for (NodeIntMap::iterator it = d_regions_map.begin();
        it != d_regions_map.end();
        ++it)
   {
-    addTotalityAxiom((*it).first, c, &d_thss->getOutputChannel());
+    addTotalityAxiom((*it).first, c);
   }
   return lit;
 }
 
-CardinalityExtension::CardinalityExtension(context::Context* c,
-                                           context::UserContext* u,
-                                           OutputChannel& out,
+CardinalityExtension::CardinalityExtension(TheoryState& state,
+                                           TheoryInferenceManager& im,
                                            TheoryUF* th)
-    : d_out(&out),
+    : d_state(state),
+      d_im(im),
       d_th(th),
-      d_conflict(c, false),
       d_rep_model(),
-      d_min_pos_com_card(c, -1),
+      d_min_pos_com_card(state.getSatContext(), -1),
       d_cc_dec_strat(nullptr),
-      d_initializedCombinedCardinality(u, false),
-      d_card_assertions_eqv_lemma(u),
-      d_min_pos_tn_master_card(c, -1),
-      d_rel_eqc(c)
+      d_initializedCombinedCardinality(state.getUserContext(), false),
+      d_card_assertions_eqv_lemma(state.getUserContext()),
+      d_min_pos_tn_master_card(state.getSatContext(), -1),
+      d_rel_eqc(state.getSatContext())
 {
   if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness())
   {
     // Register the strategy with the decision manager of the theory.
     // We are guaranteed that the decision manager is ready since we
     // construct this module during TheoryUF::finishInit.
-    d_cc_dec_strat.reset(
-        new CombinedCardinalityDecisionStrategy(c, th->getValuation()));
+    d_cc_dec_strat.reset(new CombinedCardinalityDecisionStrategy(
+        state.getSatContext(), th->getValuation()));
   }
 }
 
@@ -1353,18 +1351,6 @@ SortInference* CardinalityExtension::getSortInference()
   return nullptr;
 }
 
-/** get default sat context */
-context::Context* CardinalityExtension::getSatContext()
-{
-  return d_th->getSatContext();
-}
-
-/** get default output channel */
-OutputChannel& CardinalityExtension::getOutputChannel()
-{
-  return d_th->getOutputChannel();
-}
-
 /** ensure eqc */
 void CardinalityExtension::ensureEqc(SortModel* c, Node a)
 {
@@ -1514,7 +1500,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
           }
         }
         Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
-        d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
+        d_rep_model[tn]->assertCardinality(nCard, polarity);
         //check if combined cardinality is violated
         checkCombinedCardinality();
       }else{
@@ -1523,7 +1509,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
           Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
           eqv_lit = lit.eqNode( eqv_lit );
           Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
-          getOutputChannel().lemma( eqv_lit );
+          d_im.lemma(eqv_lit, LemmaProperty::NONE, false);
           d_card_assertions_eqv_lemma[lit] = true;
         }
       }
@@ -1557,7 +1543,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
     if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
       // cardinality constraint from user input, set incomplete   
       Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
-      d_out->setIncomplete();
+      d_im.setIncomplete();
     }
   }
   Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
@@ -1586,7 +1572,8 @@ bool CardinalityExtension::areDisequal(Node a, Node b)
 /** check */
 void CardinalityExtension::check(Theory::Effort level)
 {
-  if( !d_conflict ){
+  if (!d_state.isInConflict())
+  {
     if (options::ufssMode() == options::UfssMode::FULL)
     {
       Trace("uf-ss-solver")
@@ -1609,9 +1596,9 @@ void CardinalityExtension::check(Theory::Effort level)
         }
       }
       for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-        it->second->check( level, d_out );
-        if( it->second->isConflict() ){
-          d_conflict = true;
+        it->second->check(level);
+        if (d_state.isInConflict())
+        {
           break;
         }
       }
@@ -1636,8 +1623,8 @@ void CardinalityExtension::check(Theory::Effort level)
                     Node eq = Rewriter::rewrite( a.eqNode( b ) );
                     Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
                     Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
-                    d_out->lemma( lem );
-                    d_out->requirePhase( eq, true );
+                    d_im.lemma(lem, LemmaProperty::NONE, false);
+                    d_im.requirePhase(eq, true);
                     type_proc[tn] = true;
                     break;
                   }
@@ -1665,7 +1652,7 @@ void CardinalityExtension::presolve()
   d_initializedCombinedCardinality = false;
   for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
     it->second->presolve();
-    it->second->initialize( d_out );
+    it->second->initialize();
   }
 }
 
@@ -1703,31 +1690,16 @@ void CardinalityExtension::preRegisterTerm(TNode n)
       SortModel* rm = NULL;
       if( tn.isSort() ){
         Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
-        rm  = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
-        //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
-      }else{
-        /*
-        if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
-          Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
-          Debug("uf-ss-na") << " (" << f << ")";
-          Debug("uf-ss-na") << std::endl;
-          Unimplemented() << "Cannot perform finite model finding on arithmetic quantifier";
-        }else if( tn.isDatatype() ){
-          Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
-          Debug("uf-ss-na") << " (" << f << ")";
-          Debug("uf-ss-na") << std::endl;
-          Unimplemented() << "Cannot perform finite model finding on datatype quantifier";
-        }
-        */
+        rm = new SortModel(n, d_state, d_im, this);
       }
       if( rm ){
-        rm->initialize( d_out );
+        rm->initialize();
         d_rep_model[tn] = rm;
         //d_rep_model_init[tn] = true;
       }
     }else{
       //ensure sort model is initialized
-      it->second->initialize( d_out );
+      it->second->initialize();
     }
   }
 }
@@ -1838,8 +1810,7 @@ void CardinalityExtension::checkCombinedCardinality()
                              << " : " << cf << std::endl;
         Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
                                 << " : " << cf << std::endl;
-        getOutputChannel().conflict( cf );
-        d_conflict.set( true );
+        d_im.conflict(cf);
         return;
       }
     }
@@ -1876,8 +1847,7 @@ void CardinalityExtension::checkCombinedCardinality()
                            << std::endl;
       Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
                               << std::endl;
-      getOutputChannel().conflict( cf );
-      d_conflict.set( true );
+      d_im.conflict(cf);
     }
   }
 }

diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index e1ca46bfbfc3dbd7bd195c0ff91510863665b390..4c2707c17a38805ce6c06cb8dd1c52960c7aa8a0 100644 (file)
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -215,6 +215,10 @@ class CardinalityExtension
    private:
     /** the type this model is for */
     TypeNode d_type;
+    /** Reference to the state object */
+    TheoryState& d_state;
+    /** Reference to the inference manager */
+    TheoryInferenceManager& d_im;
     /** Pointer to the cardinality extension that owns this. */
     CardinalityExtension* d_thss;
     /** regions used to d_region_index */
@@ -251,20 +255,18 @@ class CardinalityExtension
     /** move node n to region ri */
     void moveNode( Node n, int ri );
     /** allocate cardinality */
-    void allocateCardinality( OutputChannel* out );
+    void allocateCardinality();
     /**
      * Add splits. Returns
      *   0 = no split,
      *  -1 = entailed disequality added, or
      *   1 = split added.
      */
-    int addSplit( Region* r, OutputChannel* out );
+    int addSplit(Region* r);
     /** add clique lemma */
-    void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out );
+    void addCliqueLemma(std::vector<Node>& clique);
     /** add totality axiom */
-    void addTotalityAxiom( Node n, int cardinality, OutputChannel* out );
-    /** Are we in conflict */
-    context::CDO<bool> d_conflict;
+    void addTotalityAxiom(Node n, int cardinality);
     /** cardinality */
     context::CDO< int > d_cardinality;
     /** cardinality lemma term */
@@ -283,8 +285,6 @@ class CardinalityExtension
     std::vector< Node > d_fresh_aloc_reps;
     /** whether we are initialized */
     context::CDO< bool > d_initialized;
-    /** cache for lemmas */
-    NodeBoolMap d_lemma_cache;
 
     /** apply totality */
     bool applyTotality( int cardinality );
@@ -293,16 +293,14 @@ class CardinalityExtension
     /** simple check cardinality */
     void simpleCheckCardinality();
 
-    bool doSendLemma( Node lem );
-
    public:
     SortModel(Node n,
-              context::Context* c,
-              context::UserContext* u,
+              TheoryState& state,
+              TheoryInferenceManager& im,
               CardinalityExtension* thss);
     virtual ~SortModel();
     /** initialize */
-    void initialize( OutputChannel* out );
+    void initialize();
     /** new node */
     void newEqClass( Node n );
     /** merge */
@@ -312,15 +310,11 @@ class CardinalityExtension
     /** are disequal */
     bool areDisequal( Node a, Node b );
     /** check */
-    void check( Theory::Effort level, OutputChannel* out );
+    void check(Theory::Effort level);
     /** presolve */
     void presolve();
-    /** propagate */
-    void propagate( Theory::Effort level, OutputChannel* out );
     /** assert cardinality */
-    void assertCardinality( OutputChannel* out, int c, bool val );
-    /** is in conflict */
-    bool isConflict() { return d_conflict; }
+    void assertCardinality(int c, bool val);
     /** get cardinality */
     int getCardinality() { return d_cardinality; }
     /** has cardinality */
@@ -365,19 +359,14 @@ class CardinalityExtension
   }; /** class SortModel */
 
  public:
-  CardinalityExtension(context::Context* c,
-                       context::UserContext* u,
-                       OutputChannel& out,
+  CardinalityExtension(TheoryState& state,
+                       TheoryInferenceManager& im,
                        TheoryUF* th);
   ~CardinalityExtension();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
   /** get sort inference module */
   SortInference* getSortInference();
-  /** get default sat context */
-  context::Context* getSatContext();
-  /** get default output channel */
-  OutputChannel& getOutputChannel();
   /** new node */
   void newEqClass( Node n );
   /** merge */
@@ -400,8 +389,6 @@ class CardinalityExtension
   void debugPrint( const char* c );
   /** debug a model */
   bool debugModel( TheoryModel* m );
-  /** get is in conflict */
-  bool isConflict() { return d_conflict; }
   /** get cardinality for node */
   int getCardinality( Node n );
   /** get cardinality for type */
@@ -435,12 +422,12 @@ class CardinalityExtension
   /** ensure eqc for all subterms of n */
   void ensureEqcRec(Node n);
 
-  /** The output channel used by this class. */
-  OutputChannel* d_out;
+  /** Reference to the state object */
+  TheoryState& d_state;
+  /** Reference to the inference manager */
+  TheoryInferenceManager& d_im;
   /** theory uf pointer */
   TheoryUF* d_th;
-  /** Are we in conflict */
-  context::CDO<bool> d_conflict;
   /** rep model structure, one for each type */
   std::map<TypeNode, SortModel*> d_rep_model;
 

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index a58834891cd5de2b5bcc2b48b8b5928ee5885b5d..0a48d4c719ac01e2efc2f3c1f2a9a973e86dfe16 100644 (file)
--- 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;
     }
   }