From 0dec323ac1b45ce1ca194e9bb2a335c8def525d2 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 2 Jul 2018 20:08:53 -0500
Subject: [PATCH] Remove miscellaneous dead and unused code from quantifiers
 (#2121)

---
 src/options/options_handler.cpp               |   5 -
 src/options/quantifiers_modes.h               |   2 -
 src/smt/smt_engine.cpp                        |   8 +-
 .../ematching/inst_strategy_e_matching.cpp    |  37 --
 src/theory/quantifiers/equality_query.cpp     |   4 +-
 src/theory/quantifiers/first_order_model.cpp  |  84 +---
 src/theory/quantifiers/first_order_model.h    |  11 -
 .../quantifiers/fmf/full_model_check.cpp      | 395 +++---------------
 src/theory/quantifiers/fmf/full_model_check.h |  11 -
 src/theory/quantifiers/fmf/model_engine.cpp   |   4 +-
 src/theory/quantifiers/theory_quantifiers.cpp |  37 --
 src/theory/quantifiers/theory_quantifiers.h   |   5 -
 src/theory/quantifiers_engine.cpp             |  28 +-
 src/theory/quantifiers_engine.h               |   6 -
 14 files changed, 77 insertions(+), 560 deletions(-)

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 513f9138c..2b1d72802 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -299,9 +299,6 @@ gen-ev \n\
 + Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
   model finding paper based on generalizing evaluations.\n\
 \n\
-fmc-interval \n\
-+ Same as default, but with intervals for models of integer functions.\n\
-\n\
 abs \n\
 + Use abstract MBQI algorithm (uses disjoint sets). \n\
 \n\
@@ -650,8 +647,6 @@ theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode(
     return theory::quantifiers::MBQI_NONE;
   } else if(optarg == "default" || optarg ==  "fmc") {
     return theory::quantifiers::MBQI_FMC;
-  } else if(optarg == "fmc-interval") {
-    return theory::quantifiers::MBQI_FMC_INTERVAL;
   } else if(optarg == "abs") {
     return theory::quantifiers::MBQI_ABS;
   } else if(optarg == "trust") {
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 33c047d23..a949b97be 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -59,8 +59,6 @@ enum MbqiMode {
   MBQI_NONE,
   /** default, mbqi from Section 5.4.2 of AJR thesis */
   MBQI_FMC,
-  /** mbqi with integer intervals */
-  MBQI_FMC_INTERVAL,
   /** abstract mbqi algorithm */
   MBQI_ABS,
   /** mbqi trust (produce no instantiations) */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1705cd0a3..53ea9fd58 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1916,10 +1916,10 @@ void SmtEngine::setDefaults() {
   if( options::fmfBound() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );
-    if( ! options::mbqiMode.wasSetByUser() ||
-        ( options::mbqiMode()!=quantifiers::MBQI_NONE &&
-          options::mbqiMode()!=quantifiers::MBQI_FMC &&
-          options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ) ){
+    if (!options::mbqiMode.wasSetByUser()
+        || (options::mbqiMode() != quantifiers::MBQI_NONE
+            && options::mbqiMode() != quantifiers::MBQI_FMC))
+    {
       //if bounded integers are set, use no MBQI by default
       options::mbqiMode.set( quantifiers::MBQI_NONE );
     }
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 3f2dc7cc6..cfcfcc5a5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -571,43 +571,6 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
   }
 }
 
-/*  TODO?
-bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
-  std::map< Node, bool >::iterator itq = d_quant.find( f );
-  if( itq==d_quant.end() ){
-    //generate triggers
-    Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f );
-    std::vector< Node > vars;
-    std::vector< Node > patTerms;
-    bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms );
-    if( ret ){
-      d_quant[f] = ret;
-      //add all variables to trigger that don't already occur
-      for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-        Node x = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i );
-        if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
-          patTerms.push_back( x );
-        }
-      }
-      Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl;
-      for( unsigned i=0; i<patTerms.size(); i++ ){
-        Trace("local-t-ext") << "  " << patTerms[i] << std::endl;
-      }
-      Trace("local-t-ext") << std::endl;
-      Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, true, Trigger::TR_GET_OLD );
-      d_lte_trigger[f] = tr;
-    }else{
-      Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
-      Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl;
-    }
-    d_quant[f] = ret;
-    return ret;
-  }else{
-    return itq->second;
-  }
-}
-*/
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 1d582f597..ac07e13fb 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -67,7 +67,9 @@ bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
           }
           Trace("term-db-lemma") << "  add split on : " << eq << std::endl;
         }
-        d_qe->addSplit( eq );
+        eq = Rewriter::rewrite(eq);
+        Node split = NodeManager::currentNM()->mkNode(OR, eq, eq.negate());
+        d_qe->addLemma(split);
         return false;
       }else{
         ee->assertEquality( eq, true, eq_exp );
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index e844b4eca..9d83c589f 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -387,16 +387,6 @@ Node FirstOrderModel::getModelBasis(Node q, Node n)
   return gn;
 }
 
-Node FirstOrderModel::getModelBasisBody(Node q)
-{
-  if (d_model_basis_body.find(q) == d_model_basis_body.end())
-  {
-    Node n = d_qe->getTermUtil()->getInstConstantBody(q);
-    d_model_basis_body[q] = getModelBasis(q, n);
-  }
-  return d_model_basis_body[q];
-}
-
 void FirstOrderModel::computeModelBasisArgAttribute(Node n)
 {
   if (!n.hasAttribute(ModelBasisArgAttribute()))
@@ -471,8 +461,6 @@ void FirstOrderModelIG::resetEvaluate(){
   d_eval_uf_use_default.clear();
   d_eval_uf_model.clear();
   d_eval_term_index_order.clear();
-  d_eval_failed.clear();
-  d_eval_failed_lits.clear();
   d_eval_formulas = 0;
   d_eval_uf_terms = 0;
   d_eval_lits = 0;
@@ -563,12 +551,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
     return 0;
   }else{
     ++d_eval_lits;
-    ////if we know we will fail again, immediately return
-    //if( d_eval_failed.find( n )!=d_eval_failed.end() ){
-    //  if( d_eval_failed[n] ){
-    //    return -1;
-    //  }
-    //}
     //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
     int retVal = 0;
     depIndex = ri->getNumTerms()-1;
@@ -594,11 +576,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
       ++d_eval_lits_unknown;
       Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
       Trace("fmf-eval-amb") << "   value : " << val << std::endl;
-      //std::cout << "Neither true nor false : " << n << std::endl;
-      //std::cout << "  Value : " << val << std::endl;
-      //for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      //  std::cout << "   " << i << " : " << n[i].getType() << std::endl;
-      //}
     }
     return retVal;
   }
@@ -723,13 +700,6 @@ Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector<
   }
 }
 
-void FirstOrderModelIG::clearEvalFailed( int index ){
-  for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
-    d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
-  }
-  d_eval_failed_lits[index].clear();
-}
-
 void FirstOrderModelIG::makeEvalUfModel( Node n ){
   if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){
     makeEvalUfIndexOrder( n );
@@ -856,14 +826,6 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a
 
 void FirstOrderModelFmc::processInitialize( bool ispre ) {
   if( ispre ){
-    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());
-      }
-      TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() );
-      intervalOp = NodeManager::currentNM()->mkSkolem( "interval", typ, "op representing interval" );
-    }
     for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
       it->second->reset();
     }
@@ -895,14 +857,6 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) {
   return it->second;
 }
 
-Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
-  Node st = getStar(tn);
-  if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && tn.isInteger() ){
-    st = getInterval( st, st );
-  }
-  return st;
-}
-
 Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   Trace("fmc-model") << "Get function value for " << op << std::endl;
   TypeNode type = op.getType();
@@ -947,14 +901,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       std::vector< Node > children;
       for( unsigned j=0; j<cond.getNumChildren(); j++) {
         TypeNode tn = vars[j].getType();
-        if (isInterval(cond[j])){
-          if( !isStar(cond[j][0]) ){
-            children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) );
-          }
-          if( !isStar(cond[j][1]) ){
-            children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
-          }
-        }else if( !isStar(cond[j]) ){
+        if (!isStar(cond[j]))
+        {
           Node c = getRepresentative( cond[j] );
           c = getRepresentative( c );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
@@ -972,34 +920,6 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
 }
 
-bool FirstOrderModelFmc::isInterval(Node n) {
-  return n.getKind()==APPLY_UF && n.getOperator()==intervalOp;
-}
-
-Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){
-  return NodeManager::currentNM()->mkNode( APPLY_UF, intervalOp, lb, ub );
-}
-
-bool FirstOrderModelFmc::isInRange( Node v, Node i ) {
-  if( isStar( i ) ){
-    return true;
-  }else if( isInterval( i ) ){
-    for( unsigned b=0; b<2; b++ ){
-      if( !isStar( i[b] ) ){
-        if( ( b==0 && i[b].getConst<Rational>() > v.getConst<Rational>() ) ||
-            ( b==1 && i[b].getConst<Rational>() <= v.getConst<Rational>() ) ){
-          return false;
-        }
-      }
-    }
-    return true;
-  }else{
-    return v==i;
-  }
-}
-
-
-
 FirstOrderModelAbs::FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name) :
 FirstOrderModel(qe, c, name) {
 
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index cf6ee003d..748bf12da 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -137,8 +137,6 @@ class FirstOrderModel : public TheoryModel
   Node getModelBasisOpTerm(Node op);
   /** get model basis */
   Node getModelBasis(Node q, Node n);
-  /** get model basis body */
-  Node getModelBasisBody(Node q);
   /** get model basis arg */
   unsigned getModelBasisArg(Node n);
   /** get some domain element */
@@ -234,10 +232,6 @@ public:
 private:
   //default evaluate term function
   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
-  //temporary storing which literals have failed
-  void clearEvalFailed( int index );
-  std::map< Node, bool > d_eval_failed;
-  std::map< int, std::vector< Node > > d_eval_failed_lits;
 };/* class FirstOrderModelIG */
 
 
@@ -253,7 +247,6 @@ class FirstOrderModelFmc : public FirstOrderModel
   /** models for UF */
   std::map<Node, Def * > d_models;
   std::map<TypeNode, Node > d_type_star;
-  Node intervalOp;
   /** get current model value */
   void processInitializeModelForTerm(Node n) override;
 
@@ -267,10 +260,6 @@ class FirstOrderModelFmc : public FirstOrderModel
 
   bool isStar(Node n);
   Node getStar(TypeNode tn);
-  Node getStarElement(TypeNode tn);
-  bool isInterval(Node n);
-  Node getInterval( Node lb, Node ub );
-  bool isInRange( Node v, Node i );
 };/* class FirstOrderModelFmc */
 
 }/* CVC4::theory::quantifiers::fmcheck namespace */
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index b4e9aa1e9..481048105 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -40,16 +40,6 @@ struct ModelBasisArgSort
   }
 };
 
-
-struct ConstRationalSort
-{
-  std::vector< Node > d_terms;
-  bool operator() (int i, int j) {
-    return (d_terms[i].getConst<Rational>() < d_terms[j].getConst<Rational>() );
-  }
-};
-
-
 bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
   if (index==(int)c.getNumChildren()) {
     return d_data!=-1;
@@ -100,27 +90,18 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>
     return d_data;
   }else{
     int minIndex = -1;
-    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 ){
-        //check if it is in the range
-        if( m->isInRange(inst[index], it->first )  ){
-          int gindex = it->second.getGeneralizationIndex(m, inst, index+1);
-          if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
-            minIndex = gindex;
-          }
-        }
-      }
-    }else{
-      Node st = m->getStar(inst[index].getType());
-      if(d_child.find(st)!=d_child.end()) {
-        minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);
-      }
-      Node cc = inst[index];
-      if( cc!=st && d_child.find( cc )!=d_child.end() ){
-        int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);
-        if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
-          minIndex = gindex;
-        }
+    Node st = m->getStar(inst[index].getType());
+    if (d_child.find(st) != d_child.end())
+    {
+      minIndex = d_child[st].getGeneralizationIndex(m, inst, index + 1);
+    }
+    Node cc = inst[index];
+    if (cc != st && d_child.find(cc) != d_child.end())
+    {
+      int gindex = d_child[cc].getGeneralizationIndex(m, inst, index + 1);
+      if (minIndex == -1 || (gindex != -1 && gindex < minIndex))
+      {
+        minIndex = gindex;
       }
     }
     return minIndex;
@@ -167,35 +148,6 @@ void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & c
   }
 }
 
-void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) {
-  if (index==(int)c.getNumChildren()) {
-    if( d_data!=-1 ){
-      indices.push_back( d_data );
-    }
-  }else{
-    for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
-      it->second.collectIndices(c, index+1, indices );
-    }
-  }
-}
-
-bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) {
-  if( d_complete==-1 ){
-    d_complete = 1;
-    if (index<(int)c.getNumChildren()) {
-      Node st = m->getStar(c[index].getType());
-      if(d_child.find(st)!=d_child.end()) {
-        if (!d_child[st].isComplete(m, c, index+1)) {
-          d_complete = 0;
-        }
-      }else{
-        d_complete = 0;
-      }
-    }
-  }
-  return d_complete==1;
-}
-
 bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {
   if (d_et.hasGeneralization(m, c)) {
     Trace("fmc-debug") << "Already has generalization, skip." << std::endl;
@@ -269,7 +221,8 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
     bool last_all_stars = true;
     Node cc = d_cond[d_cond.size()-1];
     for( unsigned i=0; i<cc.getNumChildren(); i++ ){
-      if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){
+      if (!m->isStar(cc[i]))
+      {
         last_all_stars = false;
         break;
       }
@@ -291,7 +244,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
       std::vector< Node > nc;
       nc.push_back( cc.getOperator() );
       for( unsigned j=0; j< cc.getNumChildren(); j++){
-        nc.push_back(m->getStarElement(cc[j].getType()));
+        nc.push_back(m->getStar(cc[j].getType()));
       }
       cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );
       //re-add the entries
@@ -476,13 +429,14 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
         Node ri = fm->getRepresentative( c[i] );
         children.push_back(ri);
         bool isStar = false;
-        if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
-          if (fm->isModelBasisTerm(ri) ) {
-            ri = fm->getStar( ri.getType() );
-            isStar = true;
-          }else{
-            hasNonStar = true;
-          }
+        if (fm->isModelBasisTerm(ri))
+        {
+          ri = fm->getStar(ri.getType());
+          isStar = true;
+        }
+        else
+        {
+          hasNonStar = true;
         }
         if( !isStar && !ri.isConst() ){
           Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
@@ -525,11 +479,6 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
       fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
     }
 
-
-    if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
-      convertIntervalModel( fm, op );
-    }
-
     Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
     fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
     Trace("fmc-model-simplify") << std::endl;
@@ -612,11 +561,8 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
   else if(fm->isStar(n) && dispStar) {
     Trace(tr) << "*";
   }
-  else if(fm->isInterval(n)) {
-    debugPrint(tr, n[0], dispStar );
-    Trace(tr) << "...";
-    debugPrint(tr, n[1], dispStar );
-  }else{
+  else
+  {
     TypeNode tn = n.getType();
     if( tn.isSort() && d_rep_ids.find(tn)!=d_rep_ids.end() ){
       if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {
@@ -671,21 +617,6 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
               if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
                 hasStar = true;
                 inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
-              }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){
-                hasStar = true;
-                //if interval, find a sample point
-                if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){
-                  if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){
-                    inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType()));
-                  }else{
-                    Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],
-                                                                NodeManager::currentNM()->mkConst( Rational(1) ) );
-                    nn = Rewriter::rewrite( nn );
-                    inst.push_back( nn );
-                  }
-                }else{
-                  inst.push_back(d_quant_models[f].d_cond[i][j][0]);
-                }
               }else{
                 inst.push_back(d_quant_models[f].d_cond[i][j]);
               }
@@ -816,15 +747,7 @@ class RepBoundFmcEntry : public QRepBoundExt
   virtual RepSetIterator::RsiEnumType setBound(
       Node owner, unsigned i, std::vector<Node>& elements) override
   {
-    if (d_fm->isInterval(d_entry[i]))
-    {
-      // explicitly add the interval?
-    }
-    else if (d_fm->isStar(d_entry[i]))
-    {
-      // must add the full range
-    }
-    else
+    if (!d_fm->isStar(d_entry[i]))
     {
       // only need to consider the single point
       elements.push_back(d_entry[i]);
@@ -1144,7 +1067,8 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
       int j = fm->getVariableId(f, v);
       Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
-      if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) {
+      if (!fm->isStar(cond[j + 1]))
+      {
         v = cond[j+1];
       }else{
         bind_var = true;
@@ -1153,41 +1077,30 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     if (bind_var) {
       Trace("fmc-uf-process") << "bind variable..." << std::endl;
       int j = fm->getVariableId(f, v);
-      if( fm->isStar(cond[j+1]) ){
-        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
-          cond[j+1] = it->first;
-          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
-        }
-        cond[j+1] = fm->getStar(v.getType());
-      }else{
-        Node orig = cond[j+1];
-        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
-          Node nw = doIntervalMeet( fm, it->first, orig );
-          if( !nw.isNull() ){
-            cond[j+1] = nw;
-            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
-          }
-        }
-        cond[j+1] = orig;
+      Assert(fm->isStar(cond[j + 1]));
+      for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin();
+           it != curr.d_child.end();
+           ++it)
+      {
+        cond[j + 1] = it->first;
+        doUninterpretedCompose2(
+            fm, f, entries, index + 1, cond, val, it->second);
       }
+      cond[j + 1] = fm->getStar(v.getType());
     }else{
       if( !v.isNull() ){
-        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);
-            }
-          }
-        }else{
-          if (curr.d_child.find(v)!=curr.d_child.end()) {
-            Trace("fmc-uf-process") << "follow value..." << std::endl;
-            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
-          }
-          Node st = fm->getStarElement(v.getType());
-          if (curr.d_child.find(st)!=curr.d_child.end()) {
-            Trace("fmc-uf-process") << "follow star..." << std::endl;
-            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);
-          }
+        if (curr.d_child.find(v) != curr.d_child.end())
+        {
+          Trace("fmc-uf-process") << "follow value..." << std::endl;
+          doUninterpretedCompose2(
+              fm, f, entries, index + 1, cond, val, curr.d_child[v]);
+        }
+        Node st = fm->getStar(v.getType());
+        if (curr.d_child.find(st) != curr.d_child.end())
+        {
+          Trace("fmc-uf-process") << "follow star..." << std::endl;
+          doUninterpretedCompose2(
+              fm, f, entries, index + 1, cond, val, curr.d_child[st]);
         }
       }
     }
@@ -1240,15 +1153,9 @@ 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::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){
-      Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );
-      if( iv.isNull() ){
-        return 0;
-      }
-    }else{
-      if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {
-        return 0;
-      }
+    if (cond[i] != c[i - 1] && !fm->isStar(cond[i]) && !fm->isStar(c[i - 1]))
+    {
+      return 0;
     }
   }
   return 1;
@@ -1259,63 +1166,17 @@ 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::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){
-        Node iv = doIntervalMeet( fm, cond[i], c[i-1] );
-        if( !iv.isNull() ){
-          cond[i] = iv;
-        }else{
-          return false;
-        }
-      }else{
-        if( fm->isStar(cond[i]) ){
-          cond[i] = c[i-1];
-        }else if( !fm->isStar(c[i-1]) ){
-          return false;
-        }
-      }
-    }
-  }
-  return true;
-}
-
-Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {
-  Trace("fmc-debug2") << "Interval meet : " << i1 << " " << i2 << " " << mk << std::endl;
-  if( fm->isStar( i1 ) ){
-    return i2;
-  }else if( fm->isStar( i2 ) ){
-    return i1;
-  }else if( !fm->isInterval( i1 ) && fm->isInterval( i2 ) ){
-    return doIntervalMeet( fm, i2, i1, mk );
-  }else if( !fm->isInterval( i2 ) ){
-    if( fm->isInterval( i1 ) ){
-      if( fm->isInRange( i2, i1 ) ){
-        return i2;
+      if (fm->isStar(cond[i]))
+      {
+        cond[i] = c[i - 1];
       }
-    }else if( i1==i2 ){
-      return i1;
-    }
-    return Node::null();
-  }else{
-    Node b[2];
-    for( unsigned j=0; j<2; j++ ){
-      Node b1 = i1[j];
-      Node b2 = i2[j];
-      if( fm->isStar( b1 ) ){
-        b[j] = b2;
-      }else if( fm->isStar( b2 ) ){
-        b[j] = b1;
-      }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){
-        b[j] = j==0 ? b2 : b1;
-      }else{
-        b[j] = j==0 ? b1 : b2;
+      else if (!fm->isStar(c[i - 1]))
+      {
+        return false;
       }
     }
-    if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){
-      return mk ? fm->getInterval( b[0], b[1] ) : i1;
-    }else{
-      return Node::null();
-    }
   }
+  return true;
 }
 
 Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
@@ -1329,11 +1190,11 @@ 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::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL) << std::endl;
+  Trace("fmc-debug") << "Make default vec" << std::endl;
   //get function symbol for f
   cond.push_back(d_quant_cond[f]);
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {
-    Node ts = fm->getStarElement( f[0][i].getType() );
+    Node ts = fm->getStar(f[0][i].getType());
     Assert( ts.getType()==f[0][i].getType() );
     cond.push_back(ts);
   }
@@ -1346,21 +1207,6 @@ void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {
   }
 }
 
-Node FullModelChecker::mkArrayCond( Node a ) {
-  if( d_array_term_cond.find(a)==d_array_term_cond.end() ){
-    if( d_array_cond.find(a.getType())==d_array_cond.end() ){
-      TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() );
-      Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" );
-      d_array_cond[a.getType()] = op;
-    }
-    std::vector< Node > cond;
-    cond.push_back(d_array_cond[a.getType()]);
-    cond.push_back(a);
-    d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond );
-  }
-  return d_array_term_cond[a];
-}
-
 Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
   if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
     if (!vals[0].isNull() && !vals[1].isNull()) {
@@ -1423,122 +1269,3 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const
 bool FullModelChecker::useSimpleModels() {
   return options::fmfFmcSimple();
 }
-
-void FullModelChecker::convertIntervalModel( FirstOrderModelFmc * fm, Node op ){
-  Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;
-  fm->d_models[op]->debugPrint("fmc-interval-model", op, this);
-  Trace("fmc-interval-model") << std::endl;
-  std::vector< int > indices;
-  for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){
-    indices.push_back( i );
-  }
-  std::map< int, std::map< int, Node > > changed_vals;
-  makeIntervalModel( fm, op, indices, 0, changed_vals );
-
-  std::vector< Node > conds;
-  std::vector< Node > values;
-  for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){
-    if( changed_vals.find(i)==changed_vals.end() ){
-      conds.push_back( fm->d_models[op]->d_cond[i] );
-    }else{
-      std::vector< Node > children;
-      children.push_back( op );
-      for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){
-        if( changed_vals[i].find(j)==changed_vals[i].end() ){
-          children.push_back( fm->d_models[op]->d_cond[i][j] );
-        }else{
-          children.push_back( changed_vals[i][j] );
-        }
-      }
-      Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children );
-      conds.push_back( nc );
-      Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";
-      debugPrintCond("fmc-interval-model", nc, true );
-      Trace("fmc-interval-model") << std::endl;
-    }
-    values.push_back( fm->d_models[op]->d_value[i] );
-  }
-  fm->d_models[op]->reset();
-  for( unsigned i=0; i<conds.size(); i++ ){
-    fm->d_models[op]->addEntry(fm, conds[i], values[i] );
-  }
-}
-
-void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
-                                          std::map< int, std::map< int, Node > >& changed_vals ) {
-  if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){
-    makeIntervalModel2( fm, op, indices, 0, changed_vals );
-  }else{
-    TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();
-    if( tn.isInteger() ){
-      makeIntervalModel(fm,op,indices,index+1, changed_vals );
-    }else{
-      std::map< Node, std::vector< int > > new_indices;
-      for( unsigned i=0; i<indices.size(); i++ ){
-        Node v = fm->d_models[op]->d_cond[indices[i]][index];
-        new_indices[v].push_back( indices[i] );
-      }
-
-      for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){
-        makeIntervalModel( fm, op, it->second, index+1, changed_vals );
-      }
-    }
-  }
-}
-
-void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
-                                          std::map< int, std::map< int, Node > >& changed_vals ) {
-  Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : ";
-  for( unsigned i=0; i<indices.size(); i++ ){
-    Debug("fmc-interval-model-debug") << indices[i] << " ";
-  }
-  Debug("fmc-interval-model-debug") << std::endl;
-
-  if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){
-    TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();
-    if( tn.isInteger() ){
-      std::map< Node, std::vector< int > > new_indices;
-      for( unsigned i=0; i<indices.size(); i++ ){
-        Node v = fm->d_models[op]->d_cond[indices[i]][index];
-        new_indices[v].push_back( indices[i] );
-        if( !v.isConst() ){
-          Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl;
-          Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl;
-        }
-      }
-
-      std::vector< Node > values;
-      for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){
-        makeIntervalModel2( fm, op, it->second, index+1, changed_vals );
-        values.push_back( it->first );
-      }
-
-      if( tn.isInteger() ){
-        //sort values by size
-        ConstRationalSort crs;
-        std::vector< int > sindices;
-        for( unsigned i=0; i<values.size(); i++ ){
-          sindices.push_back( (int)i );
-          crs.d_terms.push_back( values[i] );
-        }
-        std::sort( sindices.begin(), sindices.end(), crs );
-
-        Node ub = fm->getStar( tn );
-        for( int i=(int)(sindices.size()-1); i>=0; i-- ){
-          Node lb = fm->getStar( tn );
-          if( i>0 ){
-            lb = values[sindices[i]];
-          }
-          Node interval = fm->getInterval( lb, ub );
-          for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){
-            Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl;
-            changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;
-          }
-          ub = lb;
-        }
-      }
-    }else{
-      makeIntervalModel2( fm, op, indices, index+1, changed_vals );
-    }
-  }
-}
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index c28910700..f0f9a1798 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -42,9 +42,6 @@ public:
   bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );
   int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );
   void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
-
-  void collectIndices(Node c, int index, std::vector< int >& indices );
-  bool isComplete(FirstOrderModelFmc * m, Node c, int index);
 };/* class EntryTrie */
 
 
@@ -114,12 +111,6 @@ protected:
   //--------------------end for preinitialization
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
   bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
-protected:
-  void makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
-                          std::map< int, std::map< int, Node > >& changed_vals );
-  void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
-                          std::map< int, std::map< int, Node > >& changed_vals );
-  void convertIntervalModel( FirstOrderModelFmc * fm, Node op );
 private:
   void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
 
@@ -140,13 +131,11 @@ private:
                              std::vector< Def > & dc, int index,
                              std::vector< Node > & cond, std::vector<Node> & val );
   int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
-  Node doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk = true );
   bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
   Node mkCond( std::vector< Node > & cond );
   Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
   void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );
   void mkCondVec( Node n, std::vector< Node > & cond );
-  Node mkArrayCond( Node a );
   Node evaluateInterpreted( Node n, std::vector< Node > & vals );
   Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 public:
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index b3d9af953..f05246ddb 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -218,7 +218,9 @@ int ModelEngine::checkModel(){
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   // FMC uses two sub-effort levels
-  int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
+  int e_max = options::mbqiMode() == MBQI_FMC
+                  ? 2
+                  : (options::mbqiMode() == MBQI_TRUST ? 0 : 1);
   for( int e=0; e<e_max; e++) {
     d_incomplete_quants.clear();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 8cf8a7042..842671a5e 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -57,22 +57,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
 TheoryQuantifiers::~TheoryQuantifiers() {
 }
 
-void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-
-}
-
-void TheoryQuantifiers::addSharedTerm(TNode t) {
-  Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): "
-                     << t << endl;
-}
-
-
-void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
-  Debug("quantifiers-other") << "TheoryQuantifiers::notifyEq(): "
-                     << lhs << " = " << rhs << endl;
-
-}
-
 void TheoryQuantifiers::finishInit()
 {
   // quantifiers are not evaluated in getModelValue
@@ -119,27 +103,6 @@ void TheoryQuantifiers::ppNotifyAssertions(
   }
 }
 
-Node TheoryQuantifiers::getValue(TNode n) {
-  //NodeManager* nodeManager = NodeManager::currentNM();
-  switch(n.getKind()) {
-  case FORALL:
-  case EXISTS:
-    bool value;
-    if( d_valuation.hasSatValue( n, value ) ){
-      return NodeManager::currentNM()->mkConst(value);
-    }else{
-      return NodeManager::currentNM()->mkConst(false);  //FIX_THIS?
-    }
-    break;
-  default:
-    Unhandled(n.getKind());
-  }
-}
-
-void TheoryQuantifiers::computeCareGraph() {
-  //do nothing
-}
-
 bool TheoryQuantifiers::collectModelInfo(TheoryModel* m)
 {
   for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 2eb3f70be..074e288c6 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -39,9 +39,6 @@ class TheoryQuantifiers : public Theory {
                     const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
-  void addSharedTerm(TNode t) override;
-  void notifyEq(TNode lhs, TNode rhs);
   /** finish initialization */
   void finishInit() override;
   void preRegisterTerm(TNode n) override;
@@ -49,7 +46,6 @@ class TheoryQuantifiers : public Theory {
   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
   void check(Effort e) override;
   Node getNextDecisionRequest(unsigned& priority) override;
-  Node getValue(TNode n);
   bool collectModelInfo(TheoryModel* m) override;
   void shutdown() override {}
   std::string identify() const override
@@ -64,7 +60,6 @@ class TheoryQuantifiers : public Theory {
  private:
   void assertUniversal( Node n );
   void assertExistential( Node n );
-  void computeCareGraph() override;
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3d966726b..73d2de401 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -247,8 +247,10 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   // if we require specialized ways of building the model
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
-    if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
-        options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){
+    if (options::mbqiMode() == quantifiers::MBQI_FMC
+        || options::mbqiMode() == quantifiers::MBQI_TRUST
+        || options::fmfBound())
+    {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
       d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
@@ -873,11 +875,6 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   addTermToDatabase(d_term_util->getInstConstantBody(f), true);
 }
 
-void QuantifiersEngine::propagate( Theory::Effort level ){
-  CodeTimer codeTimer(d_statistics.d_time);
-
-}
-
 Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
   unsigned min_priority = 0;
   Node dec;  
@@ -989,23 +986,6 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
   d_phase_req_waiting[lit] = req;
 }
 
-bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
-  n = Rewriter::rewrite( n );
-  Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
-  if( addLemma( lem ) ){
-    Debug("inst") << "*** Add split " << n<< std::endl;
-    return true;
-  }
-  return false;
-}
-
-bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
-  //Assert( !areEqual( n1, n2 ) );
-  //Assert( !areDisequal( n1, n2 ) );
-  Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
-  return addSplit( fm );
-}
-
 bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) {
   if( d_qepr ){
     Assert( !options::incrementalSolving() );
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 56fe06257..674954023 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -289,8 +289,6 @@ public:
   void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
   void assertQuantifier( Node q, bool pol );
-  /** propagate */
-  void propagate( Theory::Effort level );
   /** get next decision request */
   Node getNextDecisionRequest( unsigned& priority );
 private:
@@ -314,10 +312,6 @@ public:
   bool removeLemma( Node lem );
   /** add require phase */
   void addRequirePhase( Node lit, bool req );
-  /** split on node n */
-  bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
-  /** add split equality */
-  bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
   /** add EPR axiom */
   bool addEPRAxiom( TypeNode tn );
   /** mark relevant quantified formula, this will indicate it should be checked before the others */
-- 
2.30.2