Remove uf-ss-totality option (#5251)

This option has a number of subtle bugs, it should be reimplemented if/when finite-model-find is refactored. It is not high priority enough to maintain.

This does some additional cleaning of the uf cardinality extension, some methods changed indentation.

Fixes #5239, fixes #4872, fixes #4865.

2 files changed, 231 insertions, 379 deletions

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 73c6b0a21..688a8b645 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -22,15 +22,10 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_model.h"
 
-//#define ONE_SPLIT_REGION
-//#define COMBINE_REGIONS_SMALL_INTO_LARGE
-//#define LAZY_REL_EQC
-
 using namespace std;
 using namespace CVC4::kind;
 using namespace CVC4::context;
 
-
 namespace CVC4 {
 namespace theory {
 namespace uf {
@@ -517,38 +512,21 @@ void SortModel::newEqClass( Node n ){
   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);
-        }
-      }
-      if( options::ufssTotality() ){
-        // Regions map will store whether we need to equate this term
-        // with a constant equivalence class.
-        if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
-          d_regions_map[n] = 0;
-        }else{
-          d_regions_map[n] = -1;
-        }
+      d_regions_map[n] = d_regions_index;
+      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(d_regions[d_regions_index]->getNumReps() == 0);
       }else{
-        d_regions_map[n] = d_regions_index;
-        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(d_regions[d_regions_index]->getNumReps() == 0);
-        }else{
-          d_regions.push_back(new Region(this, d_state.getSatContext()));
-        }
-        d_regions[ d_regions_index ]->addRep( n );
-        d_regions_index = d_regions_index + 1;
+        d_regions.push_back(new Region(this, d_state.getSatContext()));
       }
+      d_regions[d_regions_index]->addRep(n);
+      d_regions_index = d_regions_index + 1;
+
       d_reps = d_reps + 1;
     }
   }
@@ -556,107 +534,116 @@ void SortModel::newEqClass( Node n ){
 
 /** merge */
 void SortModel::merge( Node a, Node b ){
-  if (!d_state.isInConflict())
+  if (d_state.isInConflict())
+  {
+    return;
+  }
+  Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b << "..."
+                 << std::endl;
+  if (a != b)
   {
-    if( options::ufssTotality() ){
-      if( d_regions_map[b]==-1 ){
-        d_regions_map[a] = -1;
+    Assert(d_regions_map.find(a) != d_regions_map.end());
+    Assert(d_regions_map.find(b) != d_regions_map.end());
+    int ai = d_regions_map[a];
+    int bi = d_regions_map[b];
+    Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
+    if (ai != bi)
+    {
+      if (d_regions[ai]->getNumReps() == 1)
+      {
+        int ri = combineRegions(bi, ai);
+        d_regions[ri]->setEqual(a, b);
+        checkRegion(ri);
       }
-      d_regions_map[b] = -1;
-    }else{
-      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());
-        int ai = d_regions_map[a];
-        int bi = d_regions_map[b];
-        Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
-        if( ai!=bi ){
-          if( d_regions[ai]->getNumReps()==1  ){
-            int ri = combineRegions( bi, ai );
-            d_regions[ri]->setEqual( a, b );
-            checkRegion( ri );
-          }else if( d_regions[bi]->getNumReps()==1 ){
-            int ri = combineRegions( ai, bi );
-            d_regions[ri]->setEqual( a, b );
-            checkRegion( ri );
-          }else{
-            // Either move a to d_regions[bi], or b to d_regions[ai].
-            RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
-            RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
-            int aex = ( a_region_info->getNumInternalDisequalities() -
-                        getNumDisequalitiesToRegion( a, bi ) );
-            int bex = ( b_region_info->getNumInternalDisequalities() -
-                        getNumDisequalitiesToRegion( b, ai ) );
-            // Based on which would produce the fewest number of
-            // external disequalities.
-            if( aex<bex ){
-              moveNode( a, bi );
-              d_regions[bi]->setEqual( a, b );
-            }else{
-              moveNode( b, ai );
-              d_regions[ai]->setEqual( a, b );
-            }
-            checkRegion( ai );
-            checkRegion( bi );
-          }
+      else if (d_regions[bi]->getNumReps() == 1)
+      {
+        int ri = combineRegions(ai, bi);
+        d_regions[ri]->setEqual(a, b);
+        checkRegion(ri);
+      }
+      else
+      {
+        // Either move a to d_regions[bi], or b to d_regions[ai].
+        RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
+        RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
+        int aex = (a_region_info->getNumInternalDisequalities()
+                   - getNumDisequalitiesToRegion(a, bi));
+        int bex = (b_region_info->getNumInternalDisequalities()
+                   - getNumDisequalitiesToRegion(b, ai));
+        // Based on which would produce the fewest number of
+        // external disequalities.
+        if (aex < bex)
+        {
+          moveNode(a, bi);
+          d_regions[bi]->setEqual(a, b);
         }else{
+          moveNode(b, ai);
           d_regions[ai]->setEqual( a, b );
-          checkRegion( ai );
         }
-        d_regions_map[b] = -1;
+        checkRegion(ai);
+        checkRegion(bi);
       }
-      d_reps = d_reps - 1;
     }
+    else
+    {
+      d_regions[ai]->setEqual(a, b);
+      checkRegion(ai);
+    }
+    d_regions_map[b] = -1;
   }
+  d_reps = d_reps - 1;
 }
 
 /** assert terms are disequal */
 void SortModel::assertDisequal( Node a, Node b, Node reason ){
-  if (!d_state.isInConflict())
+  if (d_state.isInConflict())
   {
-    if( options::ufssTotality() ){
-      //do nothing
-    }else{
-      //if they are not already disequal
-      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 ) ){
-        Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
-        //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL ||
-        //    a!=reason[0][0] || b!=reason[0][1] ){
-        //  Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
-        //}
-        Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." << std::endl;
-        //add to list of disequalities
-        if( d_disequalities_index<d_disequalities.size() ){
-          d_disequalities[d_disequalities_index] = reason;
-        }else{
-          d_disequalities.push_back( reason );
-        }
-        d_disequalities_index = d_disequalities_index + 1;
-        //now, add disequalities to regions
-        Assert(d_regions_map.find(a) != d_regions_map.end());
-        Assert(d_regions_map.find(b) != d_regions_map.end());
-        Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
-        if( ai==bi ){
-          //internal disequality
-          d_regions[ai]->setDisequal( a, b, 1, true );
-          d_regions[ai]->setDisequal( b, a, 1, true );
-          checkRegion( ai, false );  //do not need to check if it needs to combine (no new ext. disequalities)
-        }else{
-          //external disequality
-          d_regions[ai]->setDisequal( a, b, 0, true );
-          d_regions[bi]->setDisequal( b, a, 0, true );
-          checkRegion( ai );
-          checkRegion( bi );
-        }
-      }
-    }
+    return;
+  }
+  // if they are not already disequal
+  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))
+  {
+    // already disequal
+    return;
+  }
+  Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..."
+                 << std::endl;
+  Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..."
+                          << std::endl;
+  // add to list of disequalities
+  if (d_disequalities_index < d_disequalities.size())
+  {
+    d_disequalities[d_disequalities_index] = reason;
+  }
+  else
+  {
+    d_disequalities.push_back(reason);
+  }
+  d_disequalities_index = d_disequalities_index + 1;
+  // now, add disequalities to regions
+  Assert(d_regions_map.find(a) != d_regions_map.end());
+  Assert(d_regions_map.find(b) != d_regions_map.end());
+  Debug("uf-ss") << "   regions: " << ai << " " << bi << std::endl;
+  if (ai == bi)
+  {
+    // internal disequality
+    d_regions[ai]->setDisequal(a, b, 1, true);
+    d_regions[ai]->setDisequal(b, a, 1, true);
+    // do not need to check if it needs to combine (no new ext. disequalities)
+    checkRegion(ai, false);
+  }
+  else
+  {
+    // external disequality
+    d_regions[ai]->setDisequal(a, b, 0, true);
+    d_regions[bi]->setDisequal(b, a, 0, true);
+    checkRegion(ai);
+    checkRegion(bi);
   }
 }
 
@@ -673,116 +660,134 @@ bool SortModel::areDisequal( Node a, Node b ) {
   }
 }
 
-/** check */
 void SortModel::check(Theory::Effort level)
 {
   Assert(options::ufssMode() == options::UfssMode::FULL);
-  if (level >= Theory::EFFORT_STANDARD && d_hasCard && !d_state.isInConflict())
+  if (!d_hasCard && d_state.isInConflict())
   {
-    Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
-                   << std::endl;
+    // not necessary to check
+    return;
+  }
+  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;
+  }
+  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 ){
-      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;
+      Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type "
+                         << d_type << ", <= " << d_cardinality << 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 ){
-        Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
-        //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl;
-        //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl;
-        //Notice() << cardinality << " ";
+    return;
+  }
+  // first check if we can generate a clique conflict
+  // do a check within each region
+  for (size_t i = 0; i < d_regions_index; i++)
+  {
+    if (d_regions[i]->valid())
+    {
+      std::vector<Node> clique;
+      if (d_regions[i]->check(level, d_cardinality, clique))
+      {
+        // add clique lemma
+        addCliqueLemma(clique);
+        return;
       }
-      return;
-    }else{
-      //first check if we can generate a clique conflict
-      if( !options::ufssTotality() ){
-        //do a check within each region
-        for( int i=0; i<(int)d_regions_index; i++ ){
-          if( d_regions[i]->valid() ){
-            std::vector< Node > clique;
-            if( d_regions[i]->check( level, d_cardinality, clique ) ){
-              //add clique lemma
-              addCliqueLemma(clique);
-              return;
-            }else{
-              Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
-            }
-          }
+      else
+      {
+        Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
+      }
+    }
+  }
+  // do splitting on demand
+  bool addedLemma = false;
+  if (level == Theory::EFFORT_FULL)
+  {
+    Trace("uf-ss-debug") << "Add splits?" << std::endl;
+    // see if we have any recommended splits from large regions
+    for (size_t i = 0; i < d_regions_index; i++)
+    {
+      if (d_regions[i]->valid() && d_regions[i]->getNumReps() > d_cardinality)
+      {
+        int sp = addSplit(d_regions[i]);
+        if (sp == 1)
+        {
+          addedLemma = true;
+        }
+        else if (sp == -1)
+        {
+          check(level);
+          return;
         }
       }
-      if( !applyTotality( d_cardinality ) ){
-        //do splitting on demand
-        bool addedLemma = false;
-        if (level==Theory::EFFORT_FULL)
+    }
+  }
+  // If no added lemmas, force continuation via combination of regions.
+  if (level != Theory::EFFORT_FULL || addedLemma)
+  {
+    return;
+  }
+  // check at full effort
+  Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
+  Trace("uf-ss-si") << "Must combine region" << std::endl;
+  bool recheck = false;
+  SortInference* si = d_thss->getSortInference();
+  if (si != nullptr)
+  {
+    // If sort inference is enabled, search for regions with same sort.
+    std::map<int, int> sortsFound;
+    for (size_t i = 0; i < d_regions_index; i++)
+    {
+      if (d_regions[i]->valid())
+      {
+        Node op = d_regions[i]->frontKey();
+        int sort_id = si->getSortId(op);
+        if (sortsFound.find(sort_id) != sortsFound.end())
         {
-          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++ ){
-            if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){
-              int sp = addSplit(d_regions[i]);
-              if( sp==1 ){
-                addedLemma = true;
-#ifdef ONE_SPLIT_REGION
-                break;
-#endif
-              }else if( sp==-1 ){
-                check(level);
-                return;
-              }
-            }
-          }
+          Debug("fmf-full-check") << "Combined regions " << i << " "
+                                  << sortsFound[sort_id] << std::endl;
+          combineRegions(sortsFound[sort_id], i);
+          recheck = true;
+          break;
         }
-        //If no added lemmas, force continuation via combination of regions.
-        if( level==Theory::EFFORT_FULL ){
-          if( !addedLemma ){
-            Trace("uf-ss-debug") << "No splits added. " << d_cardinality
-                                 << std::endl;
-            Trace("uf-ss-si")  << "Must combine region" << std::endl;
-            bool recheck = false;
-            SortInference* si = d_thss->getSortInference();
-            if (si != nullptr)
-            {
-              //If sort inference is enabled, search for regions with same sort.
-              std::map< int, int > sortsFound;
-              for( int i=0; i<(int)d_regions_index; i++ ){
-                if( d_regions[i]->valid() ){
-                  Node op = d_regions[i]->frontKey();
-                  int sort_id = si->getSortId(op);
-                  if( sortsFound.find( sort_id )!=sortsFound.end() ){
-                    Debug("fmf-full-check") << "Combined regions " << i << " " << sortsFound[sort_id] << std::endl;
-                    combineRegions( sortsFound[sort_id], i );
-                    recheck = true;
-                    break;
-                  }else{
-                    sortsFound[sort_id] = i;
-                  }
-                }
-              }
-            }
-            if( !recheck ) {
-              //naive strategy, force region combination involving the first valid region
-              for( int i=0; i<(int)d_regions_index; i++ ){
-                if( d_regions[i]->valid() ){
-                  int fcr = forceCombineRegion( i, false );
-                  Debug("fmf-full-check") << "Combined regions " << i << " " << fcr << std::endl;
-                  Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
-                  recheck = true;
-                  break;
-                }
-              }
-            }
-            if( recheck ){
-              Trace("uf-ss-debug") << "Must recheck." << std::endl;
-              check(level);
-            }
-          }
+        else
+        {
+          sortsFound[sort_id] = i;
         }
       }
     }
   }
+  if (!recheck)
+  {
+    // naive strategy, force region combination involving the first
+    // valid region
+    for (size_t i = 0; i < d_regions_index; i++)
+    {
+      if (d_regions[i]->valid())
+      {
+        int fcr = forceCombineRegion(i, false);
+        Debug("fmf-full-check")
+            << "Combined regions " << i << " " << fcr << std::endl;
+        Trace("uf-ss-debug")
+            << "Combined regions " << i << " " << fcr << std::endl;
+        recheck = true;
+        break;
+      }
+    }
+  }
+  if (recheck)
+  {
+    Trace("uf-ss-debug") << "Must recheck." << std::endl;
+    check(level);
+  }
 }
 
 void SortModel::presolve() {
@@ -960,11 +965,6 @@ int SortModel::forceCombineRegion( int ri, bool useDensity ){
 
 
 int SortModel::combineRegions( int ai, int bi ){
-#ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
-  if( d_regions[ai]->getNumReps()<d_regions[bi]->getNumReps() ){
-    return combineRegions( bi, ai );
-  }
-#endif
   Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl;
   Assert(isValid(ai) && isValid(bi));
   Region* region_bi = d_regions[bi];
@@ -1078,71 +1078,6 @@ void SortModel::addCliqueLemma(std::vector<Node>& clique)
   }
 }
 
-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();
-      d_totality_lems[n].push_back( cardinality );
-      Node cardLit = d_cardinality_literal[ cardinality ];
-      int sort_id = 0;
-      SortInference* si = d_thss->getSortInference();
-      if (si != nullptr)
-      {
-        sort_id = si->getSortId(n);
-      }
-      Trace("uf-ss-totality") << "Add totality lemma for " << n << " " << cardinality << ", sort id is " << sort_id << std::endl;
-      int use_cardinality = cardinality;
-      if( options::ufssTotalitySymBreak() ){
-        if( d_sym_break_index.find(n)!=d_sym_break_index.end() ){
-          use_cardinality = d_sym_break_index[n];
-        }else if( (int)d_sym_break_terms[n.getType()][sort_id].size()<cardinality-1 ){
-          use_cardinality = d_sym_break_terms[n.getType()][sort_id].size() + 1;
-          d_sym_break_terms[n.getType()][sort_id].push_back( n );
-          d_sym_break_index[n] = use_cardinality;
-          Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n << ", index = " << use_cardinality << std::endl;
-          if( d_sym_break_terms[n.getType()][sort_id].size()>1 ){
-            //enforce canonicity
-            for( int i=2; i<use_cardinality; i++ ){
-              //can only be assigned to domain constant d if someone has been assigned domain constant d-1
-              Node eq = n.eqNode( getTotalityLemmaTerm( cardinality, i ) );
-              std::vector< Node > eqs;
-              for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){
-                eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) );
-              }
-              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_im.lemma(lem, LemmaProperty::NONE, false);
-            }
-          }
-        }
-      }
-
-      std::vector< Node > eqs;
-      for( int i=0; i<use_cardinality; i++ ){
-        eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) );
-      }
-      Node ax = eqs.size() == 1 ? eqs[0] : nm->mkNode(OR, eqs);
-      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_im.lemma(lem, LemmaProperty::NONE, false);
-      ++( d_thss->d_statistics.d_totality_lemmas );
-    }
-  }
-}
-
-/** apply totality */
-bool SortModel::applyTotality( int cardinality ){
-  return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
-}
-
-/** get totality lemma terms */
-Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){
-  return d_totality_terms[0][i];
-}
-
 void SortModel::simpleCheckCardinality() {
   if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()<d_maxNegCard.get() ){
     Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
@@ -1249,10 +1184,10 @@ int SortModel::getNumRegions(){
   return count;
 }
 
-Node SortModel::getCardinalityLiteral(unsigned c)
+Node SortModel::getCardinalityLiteral(size_t c)
 {
   Assert(c > 0);
-  std::map<int, Node>::iterator itcl = d_cardinality_literal.find(c);
+  std::map<size_t, Node>::iterator itcl = d_cardinality_literal.find(c);
   if (itcl != d_cardinality_literal.end())
   {
     return itcl->second;
@@ -1261,49 +1196,7 @@ Node SortModel::getCardinalityLiteral(unsigned c)
   Node lit = d_c_dec_strat->getLiteral(c - 1);
   d_cardinality_literal[c] = lit;
 
-  // Since we are reasoning about cardinality c, we invoke a totality axiom
-  if (!applyTotality(c))
-  {
-    // return if we are not using totality axioms
-    return lit;
-  }
-
-  NodeManager* nm = NodeManager::currentNM();
-  Node var;
-  if (c == 1 && !options::ufssTotalitySymBreak())
-  {
-    // get arbitrary ground term
-    var = d_cardinality_term;
-  }
-  else
-  {
-    std::stringstream ss;
-    ss << "_c_" << c;
-    var = nm->mkSkolem(ss.str(), d_type, "is a cardinality lemma term");
-  }
-  if ((c - 1) < d_totality_terms[0].size())
-  {
-    d_totality_terms[0][c - 1] = var;
-  }
-  else
-  {
-    d_totality_terms[0].push_back(var);
-  }
-  // must be distinct from all other cardinality terms
-  for (unsigned i = 1, size = d_totality_terms[0].size(); i < size; i++)
-  {
-    Node lem = var.eqNode(d_totality_terms[0][i - 1]).notNode();
-    Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem
-                         << std::endl;
-    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);
-  }
+  // return the literal
   return lit;
 }
 
@@ -1391,15 +1284,11 @@ void CardinalityExtension::newEqClass(Node a)
 {
   SortModel* c = getSortModel( a );
   if( c ){
-#ifdef LAZY_REL_EQC
-    //do nothing
-#else
     Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
                           << a.getType() << std::endl;
     c->newEqClass( a );
     Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
                           << std::endl;
-#endif
   }
 }
 
@@ -1409,23 +1298,10 @@ 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") << "CardinalityExtension: Merge " << a << " " << b
-                            << " : " << a.getType() << std::endl;
-      c->merge( a, b );
-      Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
-    }else{
-      //c->assignEqClass( b, a );
-      d_rel_eqc[b] = true;
-    }
-#else
     Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b
                           << " : " << a.getType() << std::endl;
     c->merge( a, b );
     Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
-#endif
   }
 }
 
@@ -1434,10 +1310,6 @@ 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") << "CardinalityExtension: Assert disequal " << a
                           << " " << b << " : " << a.getType() << std::endl;
     c->assertDisequal( a, b, reason );
@@ -1450,9 +1322,6 @@ void CardinalityExtension::assertDisequal(Node a, Node b, Node reason)
 void CardinalityExtension::assertNode(Node n, bool isDecision)
 {
   Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
-#ifdef LAZY_REL_EQC
-  ensureEqcRec( n );
-#endif
   bool polarity = n.getKind() != kind::NOT;
   TNode lit = polarity ? n : n[0];
   if (options::ufssMode() == options::UfssMode::FULL)
@@ -1860,15 +1729,11 @@ 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);
   smtStatisticsRegistry()->registerStat(&d_split_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_totality_lemmas);
   smtStatisticsRegistry()->registerStat(&d_max_model_size);
 }
 
@@ -1877,8 +1742,6 @@ CardinalityExtension::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
   smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
 }
 
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index db27c98cd..cbef690b1 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -222,7 +222,7 @@ class CardinalityExtension
     /** Pointer to the cardinality extension that owns this. */
     CardinalityExtension* d_thss;
     /** regions used to d_region_index */
-    context::CDO< unsigned > d_regions_index;
+    context::CDO<size_t> d_regions_index;
     /** vector of regions */
     std::vector< Region* > d_regions;
     /** map from Nodes to index of d_regions they exist in, -1 means invalid */
@@ -265,31 +265,22 @@ class CardinalityExtension
     int addSplit(Region* r);
     /** add clique lemma */
     void addCliqueLemma(std::vector<Node>& clique);
-    /** add totality axiom */
-    void addTotalityAxiom(Node n, int cardinality);
     /** cardinality */
-    context::CDO< int > d_cardinality;
+    context::CDO<size_t> d_cardinality;
     /** cardinality lemma term */
     Node d_cardinality_term;
-    /** cardinality totality terms */
-    std::map< int, std::vector< Node > > d_totality_terms;
     /** cardinality literals */
-    std::map< int, Node > d_cardinality_literal;
+    std::map<size_t, Node> d_cardinality_literal;
     /** whether a positive cardinality constraint has been asserted */
     context::CDO< bool > d_hasCard;
     /** clique lemmas that have been asserted */
     std::map< int, std::vector< std::vector< Node > > > d_cliques;
     /** maximum negatively asserted cardinality */
-    context::CDO< int > d_maxNegCard;
+    context::CDO<size_t> d_maxNegCard;
     /** list of fresh representatives allocated */
     std::vector< Node > d_fresh_aloc_reps;
     /** whether we are initialized */
     context::CDO< bool > d_initialized;
-
-    /** apply totality */
-    bool applyTotality( int cardinality );
-    /** get totality lemma terms */
-    Node getTotalityLemmaTerm( int cardinality, int i );
     /** simple check cardinality */
     void simpleCheckCardinality();
 
@@ -322,7 +313,7 @@ class CardinalityExtension
     /** get cardinality term */
     Node getCardinalityTerm() { return d_cardinality_term; }
     /** get cardinality literal */
-    Node getCardinalityLiteral(unsigned c);
+    Node getCardinalityLiteral(size_t c);
     /** get maximum negative cardinality */
     int getMaximumNegativeCardinality() { return d_maxNegCard.get(); }
     //print debug
@@ -406,8 +397,6 @@ class CardinalityExtension
     IntStat d_clique_conflicts;
     IntStat d_clique_lemmas;
     IntStat d_split_lemmas;
-    IntStat d_disamb_term_lemmas;
-    IntStat d_totality_lemmas;
     IntStat d_max_model_size;
     Statistics();
     ~Statistics();