Rename UF with cardinality extension (#3241)

11 files changed, 203 insertions, 212 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d6376fb8d..4f56be8a9 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -679,6 +679,8 @@ libcvc4_add_sources(
   theory/type_enumerator.h
   theory/type_set.cpp
   theory/type_set.h
+  theory/uf/cardinality_extension.cpp
+  theory/uf/cardinality_extension.h
   theory/uf/equality_engine.cpp
   theory/uf/equality_engine.h
   theory/uf/equality_engine_types.h
@@ -691,8 +693,6 @@ libcvc4_add_sources(
   theory/uf/theory_uf_model.cpp
   theory/uf/theory_uf_model.h
   theory/uf/theory_uf_rewriter.h
-  theory/uf/theory_uf_strong_solver.cpp
-  theory/uf/theory_uf_strong_solver.h
   theory/uf/theory_uf_type_rules.h
   theory/valuation.cpp
   theory/valuation.h
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 874c57629..e838988c9 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1587,16 +1587,18 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg)
 
 // theory/uf/options_handlers.h
 const std::string OptionsHandler::s_ufssModeHelp = "\
-UF strong solver options currently supported by the --uf-ss option:\n\
+UF with cardinality options currently supported by the --uf-ss option when\n\
+combined with finite model finding:\n\
 \n\
 full \n\
-+ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\
++ Default, use UF with cardinality to find minimal models for uninterpreted\n\
+sorts.\n\
 \n\
 no-minimal \n\
-+ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\
++ Use UF with cardinality to shrink models, but do no enforce minimality.\n\
 \n\
 none \n\
-+ Do not use uf strong solver to shrink model sizes. \n\
++ Do not use UF with cardinality to shrink model sizes. \n\
 \n\
 ";
 
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index e0c34127a..8790e4ec3 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -12,24 +12,6 @@ header = "options/uf_options.h"
   help       = "use UF symmetry breaker (Deharbe et al., CADE 2011)"
 
 [[option]]
-  name       = "ufssRegions"
-  category   = "regular"
-  long       = "uf-ss-regions"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "disable region-based method for discovering cliques and splits in uf strong solver"
-
-[[option]]
-  name       = "ufssEagerSplits"
-  category   = "regular"
-  long       = "uf-ss-eager-split"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "add splits eagerly for uf strong solver"
-
-[[option]]
   name       = "ufssTotality"
   category   = "regular"
   long       = "uf-ss-totality"
@@ -63,7 +45,7 @@ header = "options/uf_options.h"
   type       = "int"
   default    = "-1"
   read_only  = true
-  help       = "tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"
+  help       = "tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"
 
 [[option]]
   name       = "ufssMode"
@@ -74,7 +56,7 @@ header = "options/uf_options.h"
   handler    = "stringToUfssMode"
   includes   = ["options/ufss_mode.h"]
   read_only  = true
-  help       = "mode of operation for uf strong solver."
+  help       = "mode of operation for uf with cardinality solver."
 
 [[option]]
   name       = "ufssFairness"
diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h
index d6a106ecf..452317b8f 100644
--- a/src/options/ufss_mode.h
+++ b/src/options/ufss_mode.h
@@ -23,12 +23,23 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-enum UfssMode{
-  /** default, use uf strong solver to find minimal models for uninterpreted sorts */
+/**
+ * These modes determine the role of UF with cardinality when using finite model
+ * finding (--finite-model-find).
+ */
+enum UfssMode
+{
+  /**
+   * Default, use UF with cardinality to find minimal models for uninterpreted
+   * sorts.
+   */
   UF_SS_FULL,
-  /** use uf strong solver to shrink model sizes, but do no enforce minimality */
+  /**
+   * Use UF with cardinality to shrink model sizes, but do no enforce
+   * minimality.
+   */
   UF_SS_NO_MINIMAL,
-  /** do not use uf strong solver */
+  /** do not use UF with cardinality */
   UF_SS_NONE,
 };
 
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 63f004448..f3eb88a90 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -28,7 +28,6 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_model.h"
-#include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 35d1f82fd..3ab52a63b 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -24,9 +24,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
+#include "theory/uf/cardinality_extension.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
 using namespace CVC4;
@@ -90,9 +90,13 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
     }
 
     Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
-    //let the strong solver verify that the model is minimal
-    //for debugging, this will if there are terms in the model that the strong solver was not notified of
-    uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
+    // Let the cardinality extension verify that the model is minimal.
+    // This will if there are terms in the model that the cardinality extension
+    // was not notified of.
+    uf::CardinalityExtension* ufss =
+        static_cast<uf::TheoryUF*>(
+            d_quantEngine->getTheoryEngine()->theoryOf(THEORY_UF))
+            ->getCardinalityExtension();
     if( !ufss || ufss->debugModel( fm ) ){
       Trace("model-engine-debug") << "Check model..." << std::endl;
       d_incomplete_check = false;
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/cardinality_extension.cpp
index 1bd8bb247..94e5f67c1 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file theory_uf_strong_solver.cpp
+/*! \file cardinality_extension.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
@@ -9,10 +9,10 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Implementation of theory uf strong solver class
+ ** \brief Implementation of theory of UF with cardinality.
  **/
 
-#include "theory/uf/theory_uf_strong_solver.h"
+#include "theory/uf/cardinality_extension.h"
 
 #include "options/uf_options.h"
 #include "theory/uf/theory_uf.h"
@@ -36,7 +36,7 @@ namespace theory {
 namespace uf {
 
 /* These are names are unambigious are we use abbreviations. */
-typedef StrongSolverTheoryUF::SortModel SortModel;
+typedef CardinalityExtension::SortModel SortModel;
 typedef SortModel::Region Region;
 typedef Region::RegionNodeInfo RegionNodeInfo;
 typedef RegionNodeInfo::DiseqList DiseqList;
@@ -228,7 +228,8 @@ struct sortExternalDegree {
 int gmcCount = 0;
 
 bool Region::getMustCombine( int cardinality ){
-  if( options::ufssRegions() && d_total_diseq_external>=unsigned(cardinality) ){
+  if (d_total_diseq_external >= static_cast<unsigned>(cardinality))
+  {
     //The number of external disequalities is greater than or equal to
     //cardinality.  Thus, a clique of size cardinality+1 may exist
     //between nodes in d_regions[i] and other regions Check if this is
@@ -285,8 +286,9 @@ bool Region::check( Theory::Effort level, int cardinality,
       }else{
         return false;
       }
-    }else if( options::ufssRegions() || options::ufssEagerSplits() ||
-              level==Theory::EFFORT_FULL ) {
+    }
+    else if (level==Theory::EFFORT_FULL) 
+    {
       //build test clique, up to size cardinality+1
       if( d_testCliqueSize<=unsigned(cardinality) ){
         std::vector< Node > newClique;
@@ -460,7 +462,7 @@ std::string SortModel::CardinalityDecisionStrategy::identify() const
 SortModel::SortModel(Node n,
                      context::Context* c,
                      context::UserContext* u,
-                     StrongSolverTheoryUF* thss)
+                     CardinalityExtension* thss)
     : d_type(n.getType()),
       d_thss(thss),
       d_regions_index(c, 0),
@@ -528,21 +530,15 @@ void SortModel::newEqClass( Node n ){
           d_regions_map[n] = -1;
         }
       }else{
-        if( !options::ufssRegions() ){
-          // If not using regions, always add new equivalence classes
-          // to region index = 0.
-          d_regions_index = 0;
-        }
         d_regions_map[n] = d_regions_index;
-        Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n
+        Debug("uf-ss") << "CardinalityExtension: New Eq Class " << n
                        << std::endl;
         Debug("uf-ss-debug") << d_regions_index << " "
                              << (int)d_regions.size() << std::endl;
         if( d_regions_index<d_regions.size() ){
           d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
           d_regions[ d_regions_index ]->setValid(true);
-          Assert( !options::ufssRegions() ||
-                  d_regions[ d_regions_index ]->getNumReps()==0 );
+          Assert(d_regions[d_regions_index]->getNumReps()==0);
         }else{
           d_regions.push_back( new Region( this, d_thss->getSatContext() ) );
         }
@@ -563,10 +559,8 @@ void SortModel::merge( Node a, Node b ){
       }
       d_regions_map[b] = -1;
     }else{
-      //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) );
-      //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) );
-      Debug("uf-ss") << "StrongSolverTheoryUF: Merging "
-                     << a << " = " << b << "..." << std::endl;
+      Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b
+                     << "..." << std::endl;
       if( a!=b ){
         Assert( d_regions_map.find( a )!=d_regions_map.end() );
         Assert( d_regions_map.find( b )!=d_regions_map.end() );
@@ -620,8 +614,9 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){
       //do nothing
     }else{
       //if they are not already disequal
-      a = d_thss->getTheory()->d_equalityEngine.getRepresentative( a );
-      b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b );
+      eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine();
+      a = ee->getRepresentative(a);
+      b = ee->getRepresentative(b);
       int ai = d_regions_map[a];
       int bi = d_regions_map[b];
       if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){
@@ -660,8 +655,8 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){
 }
 
 bool SortModel::areDisequal( Node a, Node b ) {
-  Assert( a == d_thss->getTheory()->d_equalityEngine.getRepresentative( a ) );
-  Assert( b == d_thss->getTheory()->d_equalityEngine.getRepresentative( b ) );
+  Assert(a == d_thss->getTheory()->getEqualityEngine()->getRepresentative(a));
+  Assert(b == d_thss->getTheory()->getEqualityEngine()->getRepresentative(b));
   if( d_regions_map.find( a )!=d_regions_map.end() &&
       d_regions_map.find( b )!=d_regions_map.end() ){
     int ai = d_regions_map[a];
@@ -676,14 +671,14 @@ bool SortModel::areDisequal( Node a, Node b ) {
 void SortModel::check( Theory::Effort level, OutputChannel* out ){
   Assert( options::ufssMode()==UF_SS_FULL );
   if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
-    Debug("uf-ss") << "StrongSolverTheoryUF: Check " << level << " " << d_type << std::endl;
+    Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
+                   << std::endl;
     if( level==Theory::EFFORT_FULL ){
       Debug("fmf-full-check") << std::endl;
       Debug("fmf-full-check") << "Full check for SortModel " << d_type << ", status : " << std::endl;
       debugPrint("fmf-full-check");
       Debug("fmf-full-check") << std::endl;
     }
-    //Notice() << "StrongSolverTheoryUF: Check " << level << std::endl;
     if( d_reps<=(unsigned)d_cardinality ){
       Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
       if( level==Theory::EFFORT_FULL ){
@@ -713,7 +708,8 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
       if( !applyTotality( d_cardinality ) ){
         //do splitting on demand
         bool addedLemma = false;
-        if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
+        if (level==Theory::EFFORT_FULL)
+        {
           Trace("uf-ss-debug") << "Add splits?" << std::endl;
           //see if we have any recommended splits from large regions
           for( int i=0; i<(int)d_regions_index; i++ ){
@@ -835,8 +831,9 @@ void SortModel::setSplitScore( Node n, int s ){
 void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
   if( !d_conflict ){
     Trace("uf-ss-assert")
-      << "Assert cardinality "<< d_type << " " << c << " " << val << " level = "
-      << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl;
+        << "Assert cardinality " << d_type << " " << c << " " << val
+        << " level = "
+        << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl;
     Assert( c>0 );
     Node cl = getCardinalityLiteral( c );
     if( val ){
@@ -1205,22 +1202,6 @@ bool SortModel::debugModel( TheoryModel* m ){
     Trace("uf-ss-warn") << "   Max neg cardinality : " << d_maxNegCard << std::endl;
     Trace("uf-ss-warn") << "   # Reps : " << nReps << std::endl;
     if( d_maxNegCard>=nReps ){
-      /*
-      for( unsigned i=0; i<d_fresh_aloc_reps.size(); i++ ){
-        if( add>0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){
-          rs->d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] );
-          add--;
-        }
-      }
-      for( int i=0; i<add; i++ ){
-        std::stringstream ss;
-        ss << "r_" << d_type << "_";
-        Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type,
-      "enumeration to meet negative card constraint" );
-        d_fresh_aloc_reps.push_back( nn );
-        rs->d_type_reps[d_type].push_back( nn );
-      }
-      */
       while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){
         std::stringstream ss;
         ss << "r_" << d_type << "_";
@@ -1316,7 +1297,7 @@ Node SortModel::getCardinalityLiteral(unsigned c)
   return lit;
 }
 
-StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
+CardinalityExtension::CardinalityExtension(context::Context* c,
                                            context::UserContext* u,
                                            OutputChannel& out,
                                            TheoryUF* th)
@@ -1341,38 +1322,46 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
   }
 }
 
-StrongSolverTheoryUF::~StrongSolverTheoryUF() {
+CardinalityExtension::~CardinalityExtension()
+{
   for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
        it != d_rep_model.end(); ++it) {
     delete it->second;
   }
 }
 
-SortInference* StrongSolverTheoryUF::getSortInference() {
+SortInference* CardinalityExtension::getSortInference()
+{
   return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference();
 }
 
 /** get default sat context */
-context::Context* StrongSolverTheoryUF::getSatContext() {
+context::Context* CardinalityExtension::getSatContext()
+{
   return d_th->getSatContext();
 }
 
 /** get default output channel */
-OutputChannel& StrongSolverTheoryUF::getOutputChannel() {
+OutputChannel& CardinalityExtension::getOutputChannel()
+{
   return d_th->getOutputChannel();
 }
 
 /** ensure eqc */
-void StrongSolverTheoryUF::ensureEqc( SortModel* c, Node a ) {
+void CardinalityExtension::ensureEqc(SortModel* c, Node a)
+{
   if( !hasEqc( a ) ){
     d_rel_eqc[a] = true;
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
+    Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
+                          << a.getType() << std::endl;
     c->newEqClass( a );
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
+    Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
+                          << std::endl;
   }
 }
 
-void StrongSolverTheoryUF::ensureEqcRec( Node n ) {
+void CardinalityExtension::ensureEqcRec(Node n)
+{
   if( !hasEqc( n ) ){
     SortModel* c = getSortModel( n );
     if( c ){
@@ -1385,66 +1374,75 @@ void StrongSolverTheoryUF::ensureEqcRec( Node n ) {
 }
 
 /** has eqc */
-bool StrongSolverTheoryUF::hasEqc( Node a ) {
+bool CardinalityExtension::hasEqc(Node a)
+{
   NodeBoolMap::iterator it = d_rel_eqc.find( a );
   return it!=d_rel_eqc.end() && (*it).second;
 }
 
 /** new node */
-void StrongSolverTheoryUF::newEqClass( Node a ){
+void CardinalityExtension::newEqClass(Node a)
+{
   SortModel* c = getSortModel( a );
   if( c ){
 #ifdef LAZY_REL_EQC
     //do nothing
 #else
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
+    Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
+                          << a.getType() << std::endl;
     c->newEqClass( a );
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
+    Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
+                          << std::endl;
 #endif
   }
 }
 
 /** merge */
-void StrongSolverTheoryUF::merge( Node a, Node b ){
+void CardinalityExtension::merge(Node a, Node b)
+{
   //TODO: ensure they are relevant
   SortModel* c = getSortModel( a );
   if( c ){
 #ifdef LAZY_REL_EQC
     ensureEqc( c, a );
     if( hasEqc( b ) ){
-      Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
+      Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b
+                            << " : " << a.getType() << std::endl;
       c->merge( a, b );
-      Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
+      Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
     }else{
       //c->assignEqClass( b, a );
       d_rel_eqc[b] = true;
     }
 #else
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
+    Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b
+                          << " : " << a.getType() << std::endl;
     c->merge( a, b );
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
+    Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
 #endif
   }
 }
 
 /** assert terms are disequal */
-void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
+void CardinalityExtension::assertDisequal(Node a, Node b, Node reason)
+{
   SortModel* c = getSortModel( a );
   if( c ){
 #ifdef LAZY_REL_EQC
     ensureEqc( c, a );
     ensureEqc( c, b );
 #endif
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl;
-    //Assert( d_th->d_equalityEngine.getRepresentative( a )==a );
-    //Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
+    Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a
+                          << " " << b << " : " << a.getType() << std::endl;
     c->assertDisequal( a, b, reason );
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Assert disequal." << std::endl;
+    Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal."
+                          << std::endl;
   }
 }
 
 /** assert a node */
-void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
+void CardinalityExtension::assertNode(Node n, bool isDecision)
+{
   Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
 #ifdef LAZY_REL_EQC
   ensureEqcRec( n );
@@ -1542,30 +1540,33 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
   Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
 }
 
-bool StrongSolverTheoryUF::areDisequal( Node a, Node b ) {
+bool CardinalityExtension::areDisequal(Node a, Node b)
+{
   if( a==b ){
     return false;
-  }else{
-    a = d_th->d_equalityEngine.getRepresentative( a );
-    b = d_th->d_equalityEngine.getRepresentative( b );
-    if( d_th->d_equalityEngine.areDisequal( a, b, false ) ){
-      return true;
-    }else{
-      SortModel* c = getSortModel( a );
-      if( c ){
-        return c->areDisequal( a, b );
-      }else{
-        return false;
-      }
-    }
   }
+  eq::EqualityEngine* ee = d_th->getEqualityEngine();
+  a = ee->getRepresentative(a);
+  b = ee->getRepresentative(b);
+  if (ee->areDisequal(a, b, false))
+  {
+    return true;
+  }
+  SortModel* c = getSortModel(a);
+  if (c)
+  {
+    return c->areDisequal(a, b);
+  }
+  return false;
 }
 
 /** check */
-void StrongSolverTheoryUF::check( Theory::Effort level ){
+void CardinalityExtension::check(Theory::Effort level)
+{
   if( !d_conflict ){
     if( options::ufssMode()==UF_SS_FULL ){
-      Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl;
+      Trace("uf-ss-solver")
+          << "CardinalityExtension: check " << level << std::endl;
       if (level == Theory::EFFORT_FULL)
       {
         if (Debug.isOn("uf-ss-debug"))
@@ -1575,7 +1576,7 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
         if (Trace.isOn("uf-ss-state"))
         {
           Trace("uf-ss-state")
-              << "StrongSolverTheoryUF::check " << level << std::endl;
+              << "CardinalityExtension::check " << level << std::endl;
           for (std::pair<const TypeNode, SortModel*>& rm : d_rep_model)
           {
             Trace("uf-ss-state") << "  " << rm.first << " has cardinality "
@@ -1626,11 +1627,13 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
       // unhandled uf ss mode
       Assert( false );
     }
-    Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl;
+    Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
+                          << std::endl;
   }
 }
 
-void StrongSolverTheoryUF::presolve() {
+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();
@@ -1638,13 +1641,13 @@ void StrongSolverTheoryUF::presolve() {
   }
 }
 
-StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::
+CardinalityExtension::CombinedCardinalityDecisionStrategy::
     CombinedCardinalityDecisionStrategy(context::Context* satContext,
                                         Valuation valuation)
     : DecisionStrategyFmf(satContext, valuation)
 {
 }
-Node StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::mkLiteral(
+Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
     unsigned i)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -1652,12 +1655,13 @@ Node StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::mkLiteral(
 }
 
 std::string
-StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::identify() const
+CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
 {
   return std::string("uf_combined_card");
 }
 
-void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
+void CardinalityExtension::preRegisterTerm(TNode n)
+{
   if( options::ufssMode()==UF_SS_FULL ){
     //initialize combined cardinality
     initializeCombinedCardinality();
@@ -1699,17 +1703,8 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
   }
 }
 
-//void StrongSolverTheoryUF::registerQuantifier( Node f ){
-//  Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
-  //must ensure the quantifier does not quantify over arithmetic
-  //for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
-  //  TypeNode tn = f[0][i].getType();
-  //  preRegisterType( tn, true );
-  //}
-//}
-
-
-SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
+SortModel* CardinalityExtension::getSortModel(Node n)
+{
   TypeNode tn = n.getType();
   std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
   //pre-register the type if not done already
@@ -1725,7 +1720,8 @@ SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
 }
 
 /** get cardinality for sort */
-int StrongSolverTheoryUF::getCardinality( Node n ) {
+int CardinalityExtension::getCardinality(Node n)
+{
   SortModel* c = getSortModel( n );
   if( c ){
     return c->getCardinality();
@@ -1734,7 +1730,8 @@ int StrongSolverTheoryUF::getCardinality( Node n ) {
   }
 }
 
-int StrongSolverTheoryUF::getCardinality( TypeNode tn ) {
+int CardinalityExtension::getCardinality(TypeNode tn)
+{
   std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
   if( it!=d_rep_model.end() && it->second ){
     return it->second->getCardinality();
@@ -1743,20 +1740,8 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) {
 }
 
 //print debug
-void StrongSolverTheoryUF::debugPrint( const char* c ){
-  //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine );
-  //while( !eqc_iter.isFinished() ){
-  //  Debug( c ) << "Eq class [[" << (*eqc_iter) << "]]" << std::endl;
-  //  EqClassIterator< TheoryUF::NotifyClass > eqc_iter2( *eqc_iter, &((TheoryUF*)d_th)->d_equalityEngine );
-  //  Debug( c ) << "   ";
-  //  while( !eqc_iter2.isFinished() ){
-  //    Debug( c ) << "[" << (*eqc_iter2) << "] ";
-  //    eqc_iter2++;
-  //  }
-  //  Debug( c ) << std::endl;
-  //  eqc_iter++;
-  //}
-
+void CardinalityExtension::debugPrint(const char* c)
+{
   for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
     Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl;
     it->second->debugPrint( c );
@@ -1764,7 +1749,8 @@ void StrongSolverTheoryUF::debugPrint( const char* c ){
   }
 }
 
-bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){
+bool CardinalityExtension::debugModel(TheoryModel* m)
+{
   for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
     if( !it->second->debugModel( m ) ){
       return false;
@@ -1774,7 +1760,8 @@ bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){
 }
 
 /** initialize */
-void StrongSolverTheoryUF::initializeCombinedCardinality() {
+void CardinalityExtension::initializeCombinedCardinality()
+{
   if (d_cc_dec_strat.get() != nullptr
       && !d_initializedCombinedCardinality.get())
   {
@@ -1785,7 +1772,8 @@ void StrongSolverTheoryUF::initializeCombinedCardinality() {
 }
 
 /** check */
-void StrongSolverTheoryUF::checkCombinedCardinality() {
+void CardinalityExtension::checkCombinedCardinality()
+{
   Assert( options::ufssMode()==UF_SS_FULL );
   if( options::ufssFairness() ){
     Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
@@ -1865,13 +1853,13 @@ void StrongSolverTheoryUF::checkCombinedCardinality() {
   }
 }
 
-StrongSolverTheoryUF::Statistics::Statistics():
-  d_clique_conflicts("StrongSolverTheoryUF::Clique_Conflicts", 0),
-  d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0),
-  d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0),
-  d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0),
-  d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0),
-  d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1)
+CardinalityExtension::Statistics::Statistics()
+    : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
+      d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
+      d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
+      d_disamb_term_lemmas("CardinalityExtension::Disambiguate_Term_Lemmas", 0),
+      d_totality_lemmas("CardinalityExtension::Totality_Lemmas", 0),
+      d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
 {
   smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
   smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
@@ -1881,7 +1869,8 @@ StrongSolverTheoryUF::Statistics::Statistics():
   smtStatisticsRegistry()->registerStat(&d_max_model_size);
 }
 
-StrongSolverTheoryUF::Statistics::~Statistics(){
+CardinalityExtension::Statistics::~Statistics()
+{
   smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
   smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/cardinality_extension.h
index 5dac994aa..3e3d90be5 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file theory_uf_strong_solver.h
+/*! \file cardinality_extension.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Theory uf strong solver
+ ** \brief Theory of UF with cardinality.
  **/
 
 #include "cvc4_private.h"
@@ -19,49 +19,52 @@
 
 #include "context/cdhashmap.h"
 #include "context/context.h"
-#include "context/context_mm.h"
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
 
 #include "theory/decision_manager.h"
 
 namespace CVC4 {
+
 class SortInference;
-namespace theory {
-namespace uf {
-class TheoryUF;
-} /* namespace CVC4::theory::uf */
-} /* namespace CVC4::theory */
-} /* namespace CVC4 */
 
-namespace CVC4 {
 namespace theory {
 namespace uf {
 
-class StrongSolverTheoryUF{
-protected:
+class TheoryUF;
+
+/**
+ * This module implements a theory solver for UF with cardinality constraints.
+ * For high level details, see Reynolds et al "Finite Model Finding in SMT",
+ * CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability
+ * Modulo Theories".
+ */
+class CardinalityExtension
+{
+ protected:
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
-  typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap;
-public:
+
+ public:
   /**
    * Information for incremental conflict/clique finding for a
    * particular sort.
    */
-  class SortModel {
-  private:
+  class SortModel
+  {
+   private:
     std::map< Node, std::vector< int > > d_totality_lems;
     std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms;
     std::map< Node, int > d_sym_break_index;
-  public:
 
+   public:
     /**
      * A partition of the current equality graph for which cliques
      * can occur internally.
      */
-    class Region {
-    public:
+    class Region
+    {
+     public:
       /** information stored about each node in region */
       class RegionNodeInfo {
       public:
@@ -95,7 +98,7 @@ public:
           context::CDO< int > d_size;
           NodeBoolMap d_disequalities;
         }; /* class DiseqList */
-      public:
+       public:
         /** constructor */
         RegionNodeInfo( context::Context* c )
           : d_internal(c), d_external(c), d_valid(c, true) {
@@ -119,7 +122,7 @@ public:
 
         DiseqList* get(unsigned i) { return d_disequalities[i]; }
 
-      private:
+       private:
         DiseqList d_internal;
         DiseqList d_external;
         context::CDO< bool > d_valid;
@@ -149,7 +152,7 @@ public:
       //whether region is valid
       context::CDO< bool > d_valid;
 
-    public:
+     public:
       //constructor
       Region( SortModel* cf, context::Context* c );
       virtual ~Region();
@@ -209,11 +212,11 @@ public:
       Node frontKey() const { return d_nodes.begin()->first; }
     }; /* class Region */
 
-  private:
+   private:
     /** the type this model is for */
     TypeNode d_type;
-    /** strong solver pointer */
-    StrongSolverTheoryUF* d_thss;
+    /** Pointer to the cardinality extension that owns this. */
+    CardinalityExtension* d_thss;
     /** regions used to d_region_index */
     context::CDO< unsigned > d_regions_index;
     /** vector of regions */
@@ -292,9 +295,11 @@ public:
 
     bool doSendLemma( Node lem );
 
-  public:
-    SortModel( Node n, context::Context* c, context::UserContext* u,
-               StrongSolverTheoryUF* thss );
+   public:
+    SortModel(Node n,
+              context::Context* c,
+              context::UserContext* u,
+              CardinalityExtension* thss);
     virtual ~SortModel();
     /** initialize */
     void initialize( OutputChannel* out );
@@ -359,10 +364,12 @@ public:
     std::unique_ptr<CardinalityDecisionStrategy> d_c_dec_strat;
   }; /** class SortModel */
 
-public:
-  StrongSolverTheoryUF(context::Context* c, context::UserContext* u,
-                       OutputChannel& out, TheoryUF* th);
-  ~StrongSolverTheoryUF();
+ public:
+  CardinalityExtension(context::Context* c,
+                       context::UserContext* u,
+                       OutputChannel& out,
+                       TheoryUF* th);
+  ~CardinalityExtension();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
   /** get sort inference module */
@@ -388,7 +395,7 @@ public:
   /** preregister a term */
   void preRegisterTerm( TNode n );
   /** identify */
-  std::string identify() const { return std::string("StrongSolverTheoryUF"); }
+  std::string identify() const { return std::string("CardinalityExtension"); }
   //print debug
   void debugPrint( const char* c );
   /** debug a model */
@@ -428,7 +435,7 @@ public:
   /** ensure eqc for all subterms of n */
   void ensureEqcRec(Node n);
 
-  /** The output channel for the strong solver. */
+  /** The output channel used by this class. */
   OutputChannel* d_out;
   /** theory uf pointer */
   TheoryUF* d_th;
@@ -469,8 +476,7 @@ public:
   context::CDO<int> d_min_pos_tn_master_card;
   /** relevant eqc */
   NodeBoolMap d_rel_eqc;
-}; /* class StrongSolverTheoryUF */
-
+}; /* class CardinalityExtension */
 
 }/* CVC4::theory namespace::uf */
 }/* CVC4::theory namespace */
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 3e321bf29..32d32b479 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -242,7 +242,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
 
   Debug("equality") << d_name << "::eq::newNode(" << node << ") => " << newId << std::endl;
 
-  // notify e.g. the UF theory strong solver
+  // notify e.g. the theory that owns this equality engine.
   if (d_performNotify) {
     d_notify.eqNotifyNewClass(node);
   }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7ea3f8370..6284ae31e 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -29,9 +29,9 @@
 #include "proof/uf_proof.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
+#include "theory/uf/cardinality_extension.h"
 #include "theory/uf/ho_extension.h"
 #include "theory/uf/theory_uf_rewriter.h"
-#include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
 
@@ -81,7 +81,7 @@ void TheoryUF::finishInit() {
   if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind()
       && options::ufssMode() != UF_SS_NONE)
   {
-    d_thss.reset(new StrongSolverTheoryUF(
+    d_thss.reset(new CardinalityExtension(
         getSatContext(), getUserContext(), *d_out, this));
   }
   if (options::ufHo())
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 248f46900..dd69b2ee2 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -33,13 +33,11 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-class UfTermDb;
-class StrongSolverTheoryUF;
+class CardinalityExtension;
 class HoExtension;
 
 class TheoryUF : public Theory {
 
-  friend class StrongSolverTheoryUF;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 public:
@@ -120,8 +118,8 @@ private:
   /** The notify class */
   NotifyClass d_notify;
 
-  /** The associated theory strong solver (or nullptr if it does not exist) */
-  std::unique_ptr<StrongSolverTheoryUF> d_thss;
+  /** The associated cardinality extension (or nullptr if it does not exist) */
+  std::unique_ptr<CardinalityExtension> d_thss;
   /** the higher-order solver extension (or nullptr if it does not exist) */
   std::unique_ptr<HoExtension> d_ho;
 
@@ -218,8 +216,8 @@ private:
 
   eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; }
 
-  /** get a pointer to the strong solver (uf with cardinality) */
-  StrongSolverTheoryUF* getStrongSolver() const { return d_thss.get(); }
+  /** get a pointer to the uf with cardinality */
+  CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
   /** are we in conflict? */
   bool inConflict() const { return d_conflict; }