Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.

12 files changed, 62 insertions, 216 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 539622877..014d3c603 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1142,16 +1142,9 @@ void SmtEngine::setLogicInternal() throw() {
       options::instWhenMode.set( INST_WHEN_LAST_CALL );
     }
   }
-  if ( ! options::fmfInstGen.wasSetByUser()) {
-    //if full model checking is on, disable inst-gen techniques
-    if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
-      options::fmfInstGen.set( false );
-    }else{
-      options::fmfInstGen.set( true );
-    }
-  }
   if ( options::fmfBoundInt() ){
-    if( options::mbqiMode()!=quantifiers::MBQI_NONE ){
+    if( options::mbqiMode()!=quantifiers::MBQI_NONE &&
+        options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){
       //if bounded integers are set, must use full model check for MBQI
       options::mbqiMode.set( quantifiers::MBQI_FMC );
     }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index c94775aec..797ca8f70 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -169,7 +169,7 @@ void FirstOrderModelIG::resetEvaluate(){
 //   each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
 int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
   ++d_eval_formulas;
-  //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
+  Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl;
   //Notice() << "Eval " << n << std::endl;
   if( n.getKind()==NOT ){
     int val = evaluate( n[0], depIndex, ri );
@@ -447,7 +447,7 @@ void FirstOrderModelIG::makeEvalUfModel( Node n ){
       d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );
       d_uf_model_gen[op].makeModel( this, d_eval_uf_model[n] );
       //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
-      //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
+      //d_eval_uf_model[n].debugPrint( std::cout, d_qe->getModel(), 2 );
     }
   }
 }
@@ -578,7 +578,7 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a
 
 void FirstOrderModelFmc::processInitialize( bool ispre ) {
   if( ispre ){
-    if( options::fmfFmcInterval() && intervalOp.isNull() ){
+    if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && intervalOp.isNull() ){
       std::vector< TypeNode > types;
       for(unsigned i=0; i<2; i++){
         types.push_back(NodeManager::currentNM()->integerType());
@@ -616,7 +616,7 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) {
 
 Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
   Node st = getStar(tn);
-  if( options::fmfFmcInterval() && tn.isInteger() ){
+  if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && tn.isInteger() ){
     st = getInterval( st, st );
   }
   return st;
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 174e26a5a..c7d7b7415 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -60,9 +60,9 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
         return true;
       }
     }
-    if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){
+    if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){
       //for star: check if all children are defined and have generalizations
-      if( options::fmfFmcCoverSimplify() && c[index]==st ){
+      if( c[index]==st ){     ///options::fmfFmcCoverSimplify()
         //check if all children exist and are complete
         int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);
         if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){
@@ -92,7 +92,7 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>
     return d_data;
   }else{
     int minIndex = -1;
-    if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){
+    if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){
       for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
         //if( !m->isInterval( it->first ) ){
         //  std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
@@ -327,7 +327,7 @@ QModelBuilder( c, qe ){
 bool FullModelChecker::optBuildAtFullModel() {
   //need to build after full model has taken effect if we are constructing interval models
   //  this is because we need to have a constant in all integer equivalence classes
-  return options::fmfFmcInterval();
+  return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL;
 }
 
 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
@@ -443,7 +443,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
             Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;
           }
           children.push_back(ri);
-          if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){
+          if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
             if (fm->isModelBasisTerm(ri) ) {
               ri = fm->getStar( ri.getType() );
             }else{
@@ -485,7 +485,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       }
 
 
-      if( options::fmfFmcInterval() ){
+      if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
         convertIntervalModel( fm, op );
       }
 
@@ -1103,7 +1103,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
       }
     }else{
       if( !v.isNull() ){
-        if( options::fmfFmcInterval() && v.getType().isInteger() ){
+        if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && v.getType().isInteger() ){
           for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
             if( fm->isInRange( v, it->first ) ){
               doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
@@ -1165,7 +1165,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c
   Trace("fmc-debug3") << "isCompat " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
-    if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+    if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){
       Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );
       if( iv.isNull() ){
         return 0;
@@ -1184,7 +1184,7 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( cond[i]!=c[i-1] ) {
-      if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+      if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){
         Node iv = doIntervalMeet( fm, cond[i], c[i-1] );
         if( !iv.isNull() ){
           cond[i] = iv;
@@ -1254,7 +1254,7 @@ Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
 }
 
 void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {
-  Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl;
+  Trace("fmc-debug") << "Make default vec, intervals = " << (options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL) << std::endl;
   //get function symbol for f
   cond.push_back(d_quant_cond[f]);
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 468c78978..cb63ccd45 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -273,17 +273,15 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
       ++(d_statistics.d_num_quants_init);
     }
     //try to add it
-    if( optInstGen() ){
-      Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
-      //add model basis instantiation
-      if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
-        d_quant_basis_match_added[f] = true;
-        return 1;
-      }else{
-        //shouldn't happen usually, but will occur if x != y is a required literal for f.
-        //Notice() << "No model basis for " << f << std::endl;
-        d_quant_basis_match_added[f] = false;
-      }
+    Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
+    //add model basis instantiation
+    if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
+      d_quant_basis_match_added[f] = true;
+      return 1;
+    }else{
+      //shouldn't happen usually, but will occur if x != y is a required literal for f.
+      //Notice() << "No model basis for " << f << std::endl;
+      d_quant_basis_match_added[f] = false;
     }
   }
   return 0;
@@ -418,6 +416,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         //if evaluate(...)==1, then the instantiation is already true in the model
         //  depIndex is the index of the least significant variable that this evaluation relies upon
         depIndex = riter.getNumTerms()-1;
+        Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermDatabase()->getInstConstantBody( f ) << std::endl;
         eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
         if( eval==1 ){
           Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 5006a8a61..f314584cd 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -37,7 +37,7 @@ ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ){
 
   Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
-  if( options::mbqiMode()==MBQI_FMC || options::fmfBoundInt() ){
+  if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){
     Trace("model-engine-debug") << "...make fmc builder." << std::endl;
     d_builder = new fmcheck::FullModelChecker( c, qe );
   }else if( options::mbqiMode()==MBQI_INTERVAL ){
@@ -212,7 +212,7 @@ int ModelEngine::checkModel(){
   }
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
-  int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1;
+  int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : 1;
   for( int e=0; e<e_max; e++) {
     if (d_addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -230,6 +230,8 @@ int ModelEngine::checkModel(){
           if( optOneQuantPerRound() && d_addedLemmas>0 ){
             break;
           }
+        }else{
+          Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
         }
       }
     }
@@ -248,11 +250,12 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   d_builder->d_addedLemmas = 0;
   d_builder->d_incomplete_check = false;
   if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
+    Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
     d_triedLemmas += d_builder->d_triedLemmas;
     d_addedLemmas += d_builder->d_addedLemmas;
     d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
   }else{
-    Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
+    Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
       Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 7c4cb3651..d5c755ad2 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -65,7 +65,7 @@ typedef enum {
   /** mbqi from Section 5.4.2 of AJR thesis */
   MBQI_FMC,
   /** mbqi with integer intervals */
-  //MBQI_FMC_INTERVAL,
+  MBQI_FMC_INTERVAL,
   /** mbqi with interval abstraction of uninterpreted sorts */
   MBQI_INTERVAL,
 } MbqiMode;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index f485b981c..190c7ddc9 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -76,9 +76,8 @@ option eagerInstQuant --eager-inst-quant bool :default false
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose literal matching mode
 
-option cbqi --enable-cbqi/--disable-cbqi bool :default false
- turns on counterexample-based quantifier instantiation [off by default]
-/turns off counterexample-based quantifier instantiation
+option cbqi --enable-cbqi bool :default false
+ turns on counterexample-based quantifier instantiation
 
 option recurseCbqi --cbqi-recurse bool :default false
  turns on recursive counterexample-based quantifier instantiation
@@ -97,30 +96,23 @@ option finiteModelFind --finite-model-find bool :default false
 
 option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose mode for model-based quantifier instantiation
+option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
+ only add one instantiation per quantifier per round for mbqi
+option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
+ only add instantiations for one quantifier per round for mbqi 
 
-option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
- disable simple models in full model check for finite model finding
-option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true
- disable covering simplification of fmc models
-option fmfFmcInterval --fmf-fmc-interval bool :default false
- construct interval models for fmc models
-
-option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
- only add one instantiation per quantifier per round for fmf
-option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false
- only add instantiations for one quantifier per round for fmf 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
 option fmfRelevantDomain --fmf-relevant-domain bool :default false
  use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
-option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
- enable Inst-Gen instantiation techniques for finite model finding (default)
-/disable Inst-Gen instantiation techniques for finite model finding
+option fmfInstGen /--disable-fmf-inst-gen bool :default true
+ disable Inst-Gen instantiation techniques for finite model finding
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
  only perform Inst-Gen instantiation techniques on one quantifier per round
 option fmfFreshDistConst --fmf-fresh-dc bool :default false
  use fresh distinguished representative when applying Inst-Gen techniques
-
+option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
+ disable simple models in full model check for finite model finding
 option fmfBoundInt --fmf-bound-int bool :default false
  finite model finding on bounded integer quantification
 
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index a119bcaf6..4929fa60b 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -87,9 +87,12 @@ instgen \n\
 + Use instantiation algorithm that mimics Inst-Gen calculus. \n\
 \n\
 fmc \n\
-+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
   Modulo Theories.\n\
 \n\
+fmc-interval \n\
++ Same as fmc, but with intervals for models of integer functions.\n\
+\n\
 interval \n\
 + Use algorithm that abstracts domain elements as intervals. \n\
 \n\
@@ -166,6 +169,8 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi
     return MBQI_INST_GEN;
   } else if(optarg ==  "fmc") {
     return MBQI_FMC;
+  } else if(optarg ==  "fmc-interval") {
+    return MBQI_FMC_INTERVAL;
   } else if(optarg ==  "interval") {
     return MBQI_INTERVAL;
   } else if(optarg ==  "help") {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0388a2979..5def2a832 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -51,7 +51,8 @@ d_lemmas_produced_c(u){
 
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
   //the model object
-  if( options::mbqiMode()==quantifiers::MBQI_FMC || options::fmfBoundInt() ){
+  if( options::mbqiMode()==quantifiers::MBQI_FMC ||
+      options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){
     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
   }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
     d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" );
diff --git a/src/theory/uf/options b/src/theory/uf/options
index cfa6e6c04..26f87da79 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -15,20 +15,14 @@ option ufssRegions /--disable-uf-ss-regions bool :default true
  disable region-based method for discovering cliques and splits in uf strong solver
 option ufssEagerSplits --uf-ss-eager-split bool :default false
  add splits eagerly for uf strong solver
-option ufssColoringSat --uf-ss-coloring-sat bool :default false
- use coloring-based SAT heuristic for uf strong solver
 option ufssTotality --uf-ss-totality bool :default false
  always use totality axioms for enforcing cardinality constraints
 option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
  apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
-option ufssTotalityLazy --uf-ss-totality-lazy bool :default false
- apply totality axioms lazily
 option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false
  apply symmetry breaking for totality axioms
 option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
  tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
-option ufssSmartSplits --uf-ss-smart-split bool :default false
- use smart splitting heuristic for uf strong solver
 option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
  use explained clique lemmas for uf strong solver
 option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index a4cefe269..54a3075a1 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -428,12 +428,10 @@ void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){
 void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){
   if( !d_conflict ){
     if( d_regions_map.find( n )==d_regions_map.end() ){
-      if( !options::ufssTotalityLazy() ){
-        //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() );
-          }
+      //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() );
         }
       }
       if( options::ufssTotality() ){
@@ -449,9 +447,6 @@ void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){
           d_regions_index = 0;
         }
         d_regions_map[n] = d_regions_index;
-        if( options::ufssSmartSplits() ){
-          setSplitScore( n, 0 );
-        }
         Debug("uf-ss") << "StrongSolverTheoryUF: 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() ){
@@ -634,18 +629,7 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel
           }
         }
       }
-      if( applyTotality( d_cardinality ) ){
-        //add totality axioms for all nodes that have not yet been equated to cardinality terms
-        if( options::ufssTotalityLazy() ){    //this should always be true
-          if( level==Theory::EFFORT_FULL ){
-            for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
-              if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){
-                addTotalityAxiom( (*it).first, d_cardinality, &d_thss->getOutputChannel() );
-              }
-            }
-          }
-        }
-      }else{
+      if( !applyTotality( d_cardinality ) ){
         //do splitting on demand
         bool addedLemma = false;
         if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
@@ -1073,7 +1057,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     //out->propagateAsDecision( lem[0] );
     d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality );
 
-    if( applyTotality( d_aloc_cardinality ) && !options::ufssTotalityLazy() ){
+    if( applyTotality( d_aloc_cardinality ) ){
       //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, d_aloc_cardinality, &d_thss->getOutputChannel() );
@@ -1085,27 +1069,11 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
 int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
   Node s;
   if( r->hasSplits() ){
-    if( !options::ufssSmartSplits() ){
-      //take the first split you find
-      for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
-        if( (*it).second ){
-          s = (*it).first;
-          break;
-        }
-      }
-    }else{
-      int maxScore = -1;
-      std::vector< Node > splits;
-      for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
-        if( (*it).second ){
-          int score1 = d_split_score[ (*it).first[0] ];
-          int score2 = d_split_score[ (*it).first[1] ];
-          int score = score1<score2 ? score1 : score2;
-          if( score>maxScore ){
-            maxScore = -1;
-            s = (*it).first;
-          }
-        }
+    //take the first split you find
+    for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
+      if( (*it).second ){
+        s = (*it).first;
+        break;
       }
     }
     Assert( s!=Node::null() );
@@ -1474,11 +1442,6 @@ Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) {
 StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
 d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c )
 {
-  if( options::ufssColoringSat() ){
-    d_term_amb = new TermDisambiguator( th->getQuantifiersEngine(), c );
-  }else{
-    d_term_amb = NULL;
-  }
   if( options::ufssDiseqPropagation() ){
     d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this );
   }else{
@@ -1628,13 +1591,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
     if( level==Theory::EFFORT_FULL ){
       debugPrint( "uf-ss-debug" );
     }
-    if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
-      int lemmas =  d_term_amb->disambiguateTerms( d_out );
-      d_statistics.d_disamb_term_lemmas += lemmas;
-      if( lemmas>=0 ){
-        return;
-      }
-    }
     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() ){
@@ -1646,11 +1602,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){
     if( !d_conflict && options::ufssSymBreak() ){
       d_sym_break->check( level );
     }
-    //disambiguate terms if necessary
-    //if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
-    //  Assert( d_term_amb!=NULL );
-    //  d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out );
-    //}
     Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl;
   }
 }
@@ -1918,76 +1869,6 @@ StrongSolverTheoryUF::Statistics::~Statistics(){
 }
 
 
-int TermDisambiguator::disambiguateTerms( OutputChannel* out ){
-  Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl;
-  int lemmaAdded = 0;
-  //otherwise, determine ambiguous pairs of ground terms for relevant sorts
-  quantifiers::TermDb* db = d_qe->getTermDatabase();
-  for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
-    Debug("uf-ss-disamb") << "Check " << it->first << std::endl;
-    if( it->second.size()>1 ){
-      if(involvesRelevantType( it->second[0] ) ){
-        for( int i=0; i<(int)it->second.size(); i++ ){
-          for( int j=(i+1); j<(int)it->second.size(); j++ ){
-            Kind knd = it->second[i].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
-            Node eq = NodeManager::currentNM()->mkNode( knd, it->second[i], it->second[j] );
-            eq = Rewriter::rewrite(eq);
-            //determine if they are ambiguous
-            if( d_term_amb.find( eq )==d_term_amb.end() ){
-              Debug("uf-ss-disamb") << "Check disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
-              d_term_amb[ eq ] = true;
-              //if they are equal
-              if( d_qe->getEqualityQuery()->areEqual( it->second[i], it->second[j] ) ){
-                d_term_amb[ eq ] = false;
-              }else{
-                //if an argument is disequal, then they are not ambiguous
-                for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
-                  if( d_qe->getEqualityQuery()->areDisequal( it->second[i][k], it->second[j][k] ) ){
-                    d_term_amb[ eq ] = false;
-                    break;
-                  }
-                }
-              }
-              if( d_term_amb[ eq ] ){
-                Debug("uf-ss-disamb") << "Disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
-                //must add lemma
-                std::vector< Node > children;
-                children.push_back( eq );
-                for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
-                  Kind knd2 = it->second[i][k].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
-                  Node eqc = NodeManager::currentNM()->mkNode( knd2, it->second[i][k], it->second[j][k] );
-                  children.push_back( eqc.notNode() );
-                }
-                Assert( children.size()>1 );
-                Node lem = NodeManager::currentNM()->mkNode( OR, children );
-                Trace( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
-                //Notice() << "*** Disambiguate lemma : " << lem << std::endl;
-                out->lemma( lem );
-                d_term_amb[ eq ] = false;
-                lemmaAdded++;
-                return lemmaAdded;
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-  Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl;
-  return lemmaAdded;
-}
-
-bool TermDisambiguator::involvesRelevantType( Node n ){
-  if( n.getKind()==APPLY_UF ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n[i].getType().isSort() ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
 DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss) :
   d_qe(qe), d_ufss(ufss){
   d_true = NodeManager::currentNM()->mkConst( true );
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 4f41ebf2e..3ed1ea985 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -37,7 +37,6 @@ class SubsortSymmetryBreaker;
 namespace uf {
 
 class TheoryUF;
-class TermDisambiguator;
 class DisequalityPropagator;
 
 class StrongSolverTheoryUF{
@@ -320,8 +319,6 @@ private:
   /** check */
   void checkCombinedCardinality();
 private:
-  /** term disambiguator */
-  TermDisambiguator* d_term_amb;
   /** disequality propagator */
   DisequalityPropagator* d_deq_prop;
   /** symmetry breaking techniques */
@@ -331,8 +328,6 @@ public:
   ~StrongSolverTheoryUF() {}
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
-  /** term disambiguator */
-  TermDisambiguator* getTermDisambiguator() { return d_term_amb; }
   /** disequality propagator */
   DisequalityPropagator* getDisequalityPropagator() { return d_deq_prop; }
   /** symmetry breaker */
@@ -401,23 +396,6 @@ public:
   Statistics d_statistics;
 };/* class StrongSolverTheoryUF */
 
-
-class TermDisambiguator
-{
-private:
-  /** quantifiers engine */
-  QuantifiersEngine* d_qe;
-  /** whether two terms are ambiguous (indexed by equalities) */
-  context::CDHashMap<Node, bool, NodeHashFunction> d_term_amb;
-  /** involves relevant type */
-  static bool involvesRelevantType( Node n );
-public:
-  TermDisambiguator( QuantifiersEngine* qe, context::Context* c ) : d_qe( qe ), d_term_amb( c ){}
-  ~TermDisambiguator(){}
-  /** check ambiguous terms */
-  int disambiguateTerms( OutputChannel* out );
-};
-
 class DisequalityPropagator
 {
 private: