Remove two obsolete versions of MBQI.

17 files changed, 4 insertions, 2305 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 2acefc577..f88dcb3a9 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -295,8 +295,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/model_builder.cpp \
 	theory/quantifiers/quantifiers_attributes.h \
 	theory/quantifiers/quantifiers_attributes.cpp \
-	theory/quantifiers/inst_gen.h \
-	theory/quantifiers/inst_gen.cpp \
 	theory/quantifiers/quant_util.h \
 	theory/quantifiers/quant_util.cpp \
 	theory/quantifiers/inst_match_generator.h \
@@ -319,8 +317,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/relevant_domain.cpp \
 	theory/quantifiers/symmetry_breaking.h \
 	theory/quantifiers/symmetry_breaking.cpp \
-	theory/quantifiers/qinterval_builder.h \
-	theory/quantifiers/qinterval_builder.cpp \
 	theory/quantifiers/ambqi_builder.h \
 	theory/quantifiers/ambqi_builder.cpp \
 	theory/quantifiers/quant_conflict_find.h \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dc80d65e3..8bf093370 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1305,10 +1305,6 @@ void SmtEngine::setDefaults() {
       options::mbqiMode.set( quantifiers::MBQI_NONE );
     }
   }
-  if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
-    //must do pre-skolemization
-    options::preSkolemQuant.set( true );
-  }
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 1570ba306..d4f32becc 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -17,7 +17,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/full_model_check.h"
-#include "theory/quantifiers/qinterval_builder.h"
 #include "theory/quantifiers/ambqi_builder.h"
 #include "theory/quantifiers/options.h"
 
@@ -754,167 +753,6 @@ bool FirstOrderModelFmc::isInRange( Node v, Node i ) {
 }
 
 
-FirstOrderModelQInt::FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(qe, c, name) {
-
-}
-
-void FirstOrderModelQInt::processInitialize( bool ispre ) {
-  if( !ispre ){
-    Trace("qint-debug") << "Process initialize" << std::endl;
-    for( std::map<Node, QIntDef * >::iterator it = d_models.begin(); it != d_models.end(); ++it ) {
-      Node op = it->first;
-      TypeNode tno = op.getType();
-      Trace("qint-debug") << "  Init " << op << " " << tno << std::endl;
-      for( unsigned i=0; i<tno.getNumChildren(); i++) {
-        //make sure a representative of the type exists
-        if( !d_rep_set.hasType( tno[i] ) ){
-          Node e = getSomeDomainElement( tno[i] );
-          Trace("qint-debug") << "  * Initialize type " << tno[i] << ", add ";
-          Trace("qint-debug") << e << " " << e.getType() << std::endl;
-          //d_rep_set.add( e );
-        }
-      }
-    }
-  }
-}
-
-Node FirstOrderModelQInt::getFunctionValue(Node op, const char* argPrefix ) {
-  Trace("qint-debug") << "Get function value for " << op << std::endl;
-  TypeNode type = op.getType();
-  std::vector< Node > vars;
-  for( size_t i=0; i<type.getNumChildren()-1; i++ ){
-    std::stringstream ss;
-    ss << argPrefix << (i+1);
-    Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] );
-    vars.push_back( b );
-  }
-  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
-  Node curr = d_models[op]->getFunctionValue( this, vars );
-  Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
-  Trace("qint-debug") << "Return " << fv << std::endl;
-  return fv;
-}
-
-Node FirstOrderModelQInt::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
-  Debug("qint-debug") << "get curr uf value " << n << std::endl;
-  return d_models[n]->evaluate( this, args );
-}
-
-void FirstOrderModelQInt::processInitializeModelForTerm(Node n) {
-  Debug("qint-debug") << "process init " << n << " " << n.getKind() << std::endl;
-
-  if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){
-    Node op = n.getKind()==APPLY_UF ? n.getOperator() : n;
-    if( d_models.find(op)==d_models.end()) {
-      Debug("qint-debug") << "init model for " << op << std::endl;
-      d_models[op] = new QIntDef;
-    }
-  }
-}
-
-Node FirstOrderModelQInt::getUsedRepresentative( Node n ) {
-  if( hasTerm( n ) ){
-    if( n.getType().isBoolean() ){
-      return areEqual(n, d_true) ? d_true : d_false;
-    }else{
-      return getRepresentative( n );
-    }
-  }else{
-    Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl;
-    Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() );
-    return d_rep_set.d_type_reps[n.getType()][0];
-  }
-}
-
-void FirstOrderModelQInt::processInitializeQuantifier( Node q )  {
-  if( d_var_order.find( q )==d_var_order.end() ){
-    d_var_order[q] = new QuantVarOrder( q );
-    d_var_order[q]->debugPrint("qint-var-order");
-    Trace("qint-var-order") << std::endl;
-  }
-}
-unsigned FirstOrderModelQInt::getOrderedNumVars( Node q ) {
-  //return q[0].getNumChildren();
-  return d_var_order[q]->getNumVars();
-}
-
-TypeNode FirstOrderModelQInt::getOrderedVarType( Node q, int i ) {
-  //return q[0][i].getType();
-  return d_var_order[q]->getVar( i ).getType();
-}
-
-int FirstOrderModelQInt::getOrderedVarNumToVarNum( Node q, int i ) {
-  return getVariableId( q, d_var_order[q]->getVar( i ) );
-}
-
-bool FirstOrderModelQInt::isLessThan( Node v1, Node v2 ) {
-  Assert( !v1.isNull() );
-  Assert( !v2.isNull() );
-  if( v1.getType().isSort() ){
-    Assert( getRepId( v1 )!=-1 );
-    Assert( getRepId( v2 )!=-1 );
-    int rid1 = d_rep_id[v1];
-    int rid2 = d_rep_id[v2];
-    return rid1<rid2;
-  }else{
-    return false;
-  }
-}
-
-Node FirstOrderModelQInt::getMin( Node v1, Node v2 ) {
-  return isLessThan( v1, v2 ) ? v1 : v2;
-}
-
-Node FirstOrderModelQInt::getMax( Node v1, Node v2 ) {
-  return isLessThan( v1, v2 ) ? v2 : v1;
-}
-
-Node FirstOrderModelQInt::getMaximum( TypeNode tn ) {
-  return d_max[tn];
-}
-
-Node FirstOrderModelQInt::getNext( TypeNode tn, Node v ) {
-  if( v.isNull() ){
-    return d_min[tn];
-  }else{
-    Assert( getRepId( v )!=-1 );
-    int rid = d_rep_id[v];
-    if( rid==(int)(d_rep_set.d_type_reps[tn].size()-1) ){
-      Assert( false );
-      return Node::null();
-    }else{
-      return d_rep_set.d_type_reps[tn][ rid+1 ];
-    }
-  }
-}
-Node FirstOrderModelQInt::getPrev( TypeNode tn, Node v ) {
-  if( v.isNull() ){
-    Assert( false );
-    return Node::null();
-  }else{
-    Assert( getRepId( v )!=-1 );
-    int rid = d_rep_id[v];
-    if( rid==0 ){
-      return Node::null();
-    }else{
-      return d_rep_set.d_type_reps[tn][ rid-1 ];
-    }
-  }
-}
-
-bool FirstOrderModelQInt::doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur ) {
-  Trace("qint-debug2") << "doMeet " << l1 << "..." << u1 << " with " << l2 << "..." << u2 << std::endl;
-  Assert( !u1.isNull() );
-  Assert( !u2.isNull() );
-  lr = l1.isNull() ? l2 : ( l2.isNull() ? l1 : getMax( l1, l2 ) );
-  ur = getMin( u1, u2 );
-  //return lr==ur || lr.isNull() || isLessThan( lr, ur );
-  return lr.isNull() || isLessThan( lr, ur );
-}
-
-
-
 
 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 0b282d5a5..77ccad247 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -191,50 +191,6 @@ public:
 
 }/* CVC4::theory::quantifiers::fmcheck namespace */
 
-
-class QIntDef;
-class QuantVarOrder;
-class FirstOrderModelQInt : public FirstOrderModel
-{
-  friend class QIntervalBuilder;
-private:
-  /** uf op to some representation */
-  std::map<Node, QIntDef * > d_models;
-  /** representatives to ids */
-  std::map< Node, int > d_rep_id;
-  std::map< TypeNode, Node > d_min;
-  std::map< TypeNode, Node > d_max;
-  /** quantifiers to information regarding variable ordering */
-  std::map<Node, QuantVarOrder * > d_var_order;
-  /** get current model value */
-  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
-  void processInitializeModelForTerm(Node n);
-public:
-  FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name);
-  FirstOrderModelQInt * asFirstOrderModelQInt() { return this; }
-  void processInitialize( bool ispre );
-  Node getFunctionValue(Node op, const char* argPrefix );
-
-  Node getUsedRepresentative( Node n );
-  int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; }
-  bool isLessThan( Node v1, Node v2 );
-  Node getMin( Node v1, Node v2 );
-  Node getMax( Node v1, Node v2 );
-  Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); }
-  Node getMaximum( TypeNode tn );
-  bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); }
-  bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); }
-  Node getNext( TypeNode tn, Node v );
-  Node getPrev( TypeNode tn, Node v );
-  bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur );
-  QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; }
-
-  void processInitializeQuantifier( Node q ) ;
-  unsigned getOrderedNumVars( Node q );
-  TypeNode getOrderedVarType( Node q, int i );
-  int getOrderedVarNumToVarNum( Node q, int i );
-};/* class FirstOrderModelQInt */
-
 class AbsDef;
 
 class FirstOrderModelAbs : public FirstOrderModel
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
deleted file mode 100644
index 33fcaa27a..000000000
--- a/src/theory/quantifiers/inst_gen.cpp
+++ /dev/null
@@ -1,300 +0,0 @@
-/*********************                                                        */
-/*! \file inst_gen.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of inst gen classes
- **/
-
-#include "theory/quantifiers/inst_gen.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/model_builder.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database.h"
-
-//#define CHILD_USE_CONSIDER
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-
-
-InstGenProcess::InstGenProcess( Node n ) : d_node( n ){
-  Assert( TermDb::hasInstConstAttr(n) );
-  int count = 0;
-  for( size_t i=0; i<n.getNumChildren(); i++ ){
-    if( n[i].getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr(n[i]) ){
-      d_children.push_back( InstGenProcess( n[i] ) );
-      d_children_index.push_back( i );
-      d_children_map[ i ] = count;
-      count++;
-    }
-    if( n[i].getKind()==INST_CONSTANT ){
-      d_var_num[i] = n[i].getAttribute(InstVarNumAttribute());
-    }
-  }
-}
-
-void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){
-  if( !qe->existsInstantiation( f, m, true ) ){
-    //make sure no duplicates are produced
-    if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){
-      d_match_values.push_back( val );
-      d_matches.push_back( InstMatch( &m ) );
-      ((QModelBuilderIG*)qe->getModelBuilder())->d_instGenMatches++;
-    }
-  }
-}
-
-void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){
-  Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;
-  //whether we are doing a product or sum or matches
-  bool doProduct = true;
-  //get the model
-  FirstOrderModel* fm = qe->getModel();
-
-  //calculate terms we will consider
-  std::vector< Node > considerTerms;
-  std::vector< std::vector< Node > > newConsiderVal;
-  std::vector< bool > newUseConsider;
-  std::map< Node, InstMatch > considerTermsMatch[2];
-  std::map< Node, bool > considerTermsSuccess[2];
-  newConsiderVal.resize( d_children.size() );
-  newUseConsider.resize( d_children.size(), useConsider );
-  if( d_node.getKind()==APPLY_UF ){
-    Node op = d_node.getOperator();
-    if( useConsider ){
-#ifndef CHILD_USE_CONSIDER
-      for( size_t i=0; i<newUseConsider.size(); i++ ){
-        newUseConsider[i] = false;
-      }
-#endif
-      for( size_t i=0; i<considerVal.size(); i++ ){
-        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ),
-                                 qe->getEqualityQuery()->getEngine() );
-        while( !eqc.isFinished() ){
-          Node en = (*eqc);
-          if( en.getKind()==APPLY_UF && en.getOperator()==op ){
-              considerTerms.push_back( en );
-          }
-          ++eqc;
-        }
-      }
-    }else{
-      considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() );
-    }
-    //for each term we consider, calculate a current match
-    for( size_t i=0; i<considerTerms.size(); i++ ){
-      Node n = considerTerms[i];
-      bool isSelected = ((QModelBuilderIG*)qe->getModelBuilder())->isTermSelected( n );
-      bool hadSuccess CVC4_UNUSED = false;
-      for( int t=(isSelected ? 0 : 1); t<2; t++ ){
-        if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
-          considerTermsMatch[t][n] = InstMatch( f );
-          considerTermsSuccess[t][n] = true;
-          for( size_t j=0; j<d_node.getNumChildren(); j++ ){
-            if( d_children_map.find( j )==d_children_map.end() ){
-              if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
-                if( d_node[j].getKind()==INST_CONSTANT ){
-                  if( !considerTermsMatch[t][n].set( qe, d_var_num[j], n[j] ) ){
-                    Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";
-                    Trace("inst-gen-cm") << considerTermsMatch[t][n].get( d_var_num[j] ) << std::endl;
-                    considerTermsSuccess[t][n] = false;
-                    break;
-                  }
-                }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){
-                  Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;
-                  considerTermsSuccess[t][n] = false;
-                  break;
-                }
-              }
-            }
-          }
-          //if successful, store it
-          if( considerTermsSuccess[t][n] ){
-#ifdef CHILD_USE_CONSIDER
-            if( !hadSuccess ){
-              hadSuccess = true;
-              for( size_t k=0; k<d_children.size(); k++ ){
-                if( newUseConsider[k] ){
-                  int childIndex = d_children_index[k];
-                  //determine if we are restricted or not
-                  if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){
-                    Node r = qe->getModel()->getRepresentative( n[childIndex] );
-                    if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){
-                      newConsiderVal[k].push_back( r );
-                      //check if we now need to consider the entire domain
-                      TypeNode tn = r.getType();
-                      if( qe->getModel()->d_rep_set.hasType( tn ) ){
-                        if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){
-                          newConsiderVal[k].clear();
-                          newUseConsider[k] = false;
-                        }
-                      }
-                    }
-                  }else{
-                    //matching against selected term, will need to consider all values
-                    newConsiderVal[k].clear();
-                    newUseConsider[k] = false;
-                  }
-                }
-              }
-            }
-#endif
-          }
-        }
-      }
-    }
-  }else{
-    //the interpretted case
-    if( d_node.getType().isBoolean() ){
-      if( useConsider ){
-        //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; }
-        Assert( considerVal.size()==1 );
-        bool reqPol = considerVal[0]==fm->d_true;
-        Node ncv = considerVal[0];
-        if( d_node.getKind()==NOT ){
-          ncv = reqPol ? fm->d_false : fm->d_true;
-        }
-        if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){
-          for( size_t i=0; i<newConsiderVal.size(); i++ ){
-            newConsiderVal[i].push_back( ncv );
-          }
-          //instead we will do a sum
-          if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol )  ){
-            doProduct = false;
-          }
-        }else{
-          //do not use consider
-          for( size_t i=0; i<newUseConsider.size(); i++ ){
-            newUseConsider[i] = false;
-          }
-        }
-      }
-    }
-  }
-
-  //calculate all matches for children
-  for( int i=0; i<(int)d_children.size(); i++ ){
-    d_children[i].calculateMatches( qe, f, newConsiderVal[i], newUseConsider[i] );
-    if( doProduct && d_children[i].getNumMatches()==0 ){
-      return;
-    }
-  }
-  if( d_node.getKind()==APPLY_UF ){
-    //if this is an uninterpreted function
-    Node op = d_node.getOperator();
-    //process all values
-    for( size_t i=0; i<considerTerms.size(); i++ ){
-      Node n = considerTerms[i];
-      bool isSelected = ((QModelBuilderIG*)qe->getModelBuilder())->isTermSelected( n );
-      for( int t=(isSelected ? 0 : 1); t<2; t++ ){
-        //do not consider ground case if it is already congruent to another ground term
-        if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
-          Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;
-          if( considerTermsSuccess[t][n] ){
-            //try to find unifier for d_node = n
-            calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 );
-          }
-        }
-      }
-    }
-  }else{
-    //if this is an interpreted function
-    if( doProduct ){
-      //combining children matches
-      InstMatch curr( f );
-      std::vector< Node > terms;
-      calculateMatchesInterpreted( qe, f, curr, terms, 0 );
-    }else{
-      //summing children matches
-      Assert( considerVal.size()==1 );
-      for( int i=0; i<(int)d_children.size(); i++ ){
-        for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){
-          InstMatch m( f );
-          if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){
-            addMatchValue( qe, f, considerVal[0], m );
-          }
-        }
-      }
-    }
-  }
-  Trace("inst-gen-cm") << "done calculate matches" << std::endl;
-  //can clear information used for finding duplicates
-  d_inst_trie.clear();
-}
-
-bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){
-  //FIXME: is this correct? (query may not be accurate)
-  return m.merge( q, d_matches[i] );
-}
-
-void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){
-  if( childIndex==(int)d_children.size() ){
-    Node val = qe->getModel()->getRepresentative( n );  //FIXME: is this correct?
-    Trace("inst-gen-cm") << "  - u-match : " << val << std::endl;
-    Trace("inst-gen-cm") << "            : " << curr << std::endl;
-    addMatchValue( qe, f, val, curr );
-  }else{
-    Trace("inst-gen-cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl;
-    bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) );
-    for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){
-      //FIXME: is this correct?
-      if( sel || qe->getEqualityQuery()->areEqual( d_children[ childIndex ].getMatchValue( i ), n[d_children_index[childIndex]] ) ){
-        InstMatch next( &curr );
-        if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){
-          calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected );
-        }else{
-          Trace("inst-gen-cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl;
-          Trace("inst-gen-cm") << childIndex << " match " << i << " not equal subs." << std::endl;
-        }
-      }else{
-        Trace("inst-gen-cm") << childIndex << " match " << i << " not equal value." << std::endl;
-      }
-    }
-  }
-}
-
-void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ){
-  FirstOrderModel* fm = qe->getModel();
-  if( argIndex==(int)d_node.getNumChildren() ){
-    Node val;
-    if( d_node.getNumChildren()==0 ){
-      val = d_node;
-    }else if( d_node.getKind()==EQUAL ){
-      val = qe->getEqualityQuery()->areEqual( terms[0], terms[1] ) ? fm->d_true : fm->d_false;
-    }else{
-      val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms );
-      val = Rewriter::rewrite( val );
-    }
-    Trace("inst-gen-cm") << "  - i-match : " << d_node << std::endl;
-    Trace("inst-gen-cm") << "            : " << val << std::endl;
-    Trace("inst-gen-cm") << "            : " << curr << std::endl;
-    addMatchValue( qe, f, val, curr );
-  }else{
-    if( d_children_map.find( argIndex )==d_children_map.end() ){
-      terms.push_back( fm->getRepresentative( d_node[argIndex] ) );
-      calculateMatchesInterpreted( qe, f, curr, terms, argIndex+1 );
-      terms.pop_back();
-    }else{
-      for( int i=0; i<(int)d_children[ d_children_map[argIndex] ].getNumMatches(); i++ ){
-        InstMatch next( &curr );
-        if( d_children[ d_children_map[argIndex] ].getMatch( qe->getEqualityQuery(), i, next ) ){
-          terms.push_back( d_children[ d_children_map[argIndex] ].getMatchValue( i ) );
-          calculateMatchesInterpreted( qe, f, next, terms, argIndex+1 );
-          terms.pop_back();
-        }
-      }
-    }
-  }
-}
diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h
deleted file mode 100644
index 6567994f2..000000000
--- a/src/theory/quantifiers/inst_gen.h
+++ /dev/null
@@ -1,60 +0,0 @@
-/*********************                                                        */
-/*! \file inst_gen.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Inst Gen classes
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_GEN_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_GEN_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/inst_match.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class InstGenProcess
-{
-private:
-  //the node we are processing
-  Node d_node;
-  std::map< int, int > d_var_num;
-  //the sub children for this node
-  std::vector< InstGenProcess > d_children;
-  std::vector< int > d_children_index;
-  std::map< int, int > d_children_map;
-  //the matches we have produced
-  std::vector< InstMatch > d_matches;
-  std::vector< Node > d_match_values;
-  //add match value
-  std::map< Node, inst::InstMatchTrie > d_inst_trie;
-  void addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m );
-private:
-  void calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected );
-  void calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex );
-public:
-  InstGenProcess( Node n );
-  virtual ~InstGenProcess(){}
-
-  void calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider );
-  int getNumMatches() { return d_matches.size(); }
-  bool getMatch( EqualityQuery* q, int i, InstMatch& m );
-  Node getMatchValue( int i ) { return d_match_values[i]; }
-};/* class InstGenProcess */
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__INST_GEN_H */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index f6392a0b2..53f55e70b 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -22,7 +22,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/model_builder.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/inst_gen.h"
 #include "theory/quantifiers/trigger.h"
 #include "theory/quantifiers/options.h"
 
@@ -754,389 +753,3 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
 }
 
 
-
-
-//////////////////////  Inst-Gen style Model Builder ///////////
-
-void QModelBuilderInstGen::reset( FirstOrderModel* fm ){
-  //for new inst gen
-  d_quant_selection_formula.clear();
-  d_term_selected.clear();
-
-  //d_sub_quant_inst_trie.clear();//*
-}
-
-int QModelBuilderInstGen::initializeQuantifier( Node f, Node fp ){
-  int addedLemmas = QModelBuilderIG::initializeQuantifier( f, fp );
-  for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
-    addedLemmas += initializeQuantifier( d_sub_quants[f][i], fp );
-  }
-  return addedLemmas;
-}
-
-void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
-  //Node fp = getParentQuantifier( f );//*
-  //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) );
-  //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//*
-  Trace("sel-form-debug") << "* Analyze " << f << std::endl;
-  //determine selection formula, set terms in selection formula as being selected
-  Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ),
-                                d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 );
-  //if( !s.isNull() ){
-  //  s = Rewriter::rewrite( s );
-  //}
-  Trace("sel-form-debug") << "Selection formula " << f << std::endl;
-  Trace("sel-form-debug") << "                  " << s << std::endl;
-  if( !s.isNull() ){
-    d_quant_selection_formula[f] = s;
-    Node gs = d_qe->getTermDatabase()->getModelBasis( f, s );
-    setSelectedTerms( gs );
-    //quick check if it is constant sat
-    if( hasConstantDefinition( s ) ){
-      d_quant_sat[f] = true;
-    }
-  }else{
-    Trace("sel-form-null") << "*** No selection formula for " << f << std::endl;
-  }
-  //analyze sub quantifiers
-  if( d_quant_sat.find( f )==d_quant_sat.end() ){
-    for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
-      analyzeQuantifier( fm, d_sub_quants[f][i] );
-    }
-  }
-}
-
-
-int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
-  int addedLemmas = 0;
-  if( d_quant_sat.find( f )==d_quant_sat.end() ){
-    Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f];
-    if( fp!=f ) Trace("inst-gen") << "   ";
-    Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
-    if( fp!=f ) Trace("inst-gen") << "   ";
-    Trace("inst-gen") << "Sel Form :      " << d_quant_selection_formula[f] << std::endl;
-    //we wish to add all known exceptions to our selection formula for f. this will help to refine our current model.
-    if( !d_quant_selection_formula[f].isNull() ){
-      //first, try on sub quantifiers
-      bool subQuantSat = true;
-      for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
-        addedLemmas += doInstGen( fm, d_sub_quants[f][i] );
-        if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
-          subQuantSat = false;
-        }
-      }
-      if( addedLemmas>0 || !subQuantSat ){
-        Trace("inst-gen") << " -> children added lemmas or non-satisfied" << std::endl;
-        return addedLemmas;
-      }else{
-        Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl;
-        //get all possible values of selection formula
-        InstGenProcess igp( d_quant_selection_formula[f] );
-        std::vector< Node > considered;
-        considered.push_back( fm->d_false );
-        igp.calculateMatches( d_qe, f, considered, true );
-        //igp.calculateMatches( d_qe, f);
-        Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl;
-        for( int i=0; i<igp.getNumMatches(); i++ ){
-          //if the match is not already true in the model
-          if( igp.getMatchValue( i )!=fm->d_true ){
-            InstMatch m( f );
-            igp.getMatch( d_qe->getEqualityQuery(), i, m );
-            //Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl;
-            //we only consider matches that are non-empty
-            //  matches that are empty should trigger other instances that are non-empty
-            if( !m.empty() ){
-              Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl;
-              //translate to be in terms match in terms of fp
-              InstMatch mp(f);
-              getParentQuantifierMatch( mp, fp, m, f );
-              //if this is a partial instantion
-              if( !m.isComplete() ){
-                //need to make it internal here
-                //Trace("mkInternal") << "Make internal representative " << mp << std::endl;
-                //mp.makeInternalRepresentative( d_qe );
-                //Trace("mkInternal") << "Got " << mp << std::endl;
-                //if the instantiation does not yet exist
-                if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){
-                  //also add it to children
-                  d_child_sub_quant_inst_trie[f].addInstMatch( d_qe, f, m );
-                  //get the partial instantiation pf
-                  Node pf = d_qe->getInstantiation( fp, mp );
-                  Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl;
-                  Trace("inst-gen-pi") << "                         " << pf << std::endl;
-                  d_sub_quants[ f ].push_back( pf );
-                  d_sub_quant_inst[ pf ] = InstMatch( &mp );
-                  d_sub_quant_parent[ pf ] = fp;
-                  //now make mp a complete match
-                  mp.add( d_quant_basis_match[ fp ] );
-                  d_quant_basis_match[ pf ] = InstMatch( &mp );
-                  ++(d_statistics.d_num_quants_init);
-                  ++(d_statistics.d_num_partial_quants_init);
-                  addedLemmas += initializeQuantifier( pf, fp );
-                  Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl;
-                  subQuantSat = false;
-                }
-              }else{
-                if( d_qe->addInstantiation( fp, mp ) ){
-                  addedLemmas++;
-                }
-              }
-            }
-          }
-        }
-        if( addedLemmas==0 ){
-          //all sub quantifiers must be satisfied as well
-          if( subQuantSat ){
-            d_quant_sat[ f ] = true;
-          }
-        }
-        if( fp!=f ) Trace("inst-gen") << "   ";
-        Trace("inst-gen") << "  -> added lemmas = " << addedLemmas << std::endl;
-        if( d_quant_sat.find( f )!=d_quant_sat.end() ){
-          if( fp!=f ) Trace("inst-gen") << "   ";
-          Trace("inst-gen") << "  -> *** it is satisfied" << std::endl;
-        }
-      }
-    }
-  }
-  return addedLemmas;
-}
-
-Node mkAndSelectionFormula( std::vector< Node >& children ){
-  std::vector< Node > ch;
-  for( size_t i=0; i<children.size(); i++ ){
-    if( children[i].getKind()==AND ){
-      for( size_t j=0; j<children[i].getNumChildren(); j++ ){
-        ch.push_back( children[i][j] );
-      }
-    }else{
-      ch.push_back( children[i] );
-    }
-  }
-  return NodeManager::currentNM()->mkNode( AND, ch );
-}
-Node mkAndSelectionFormula( Node n1, Node n2 ){
-  std::vector< Node > children;
-  children.push_back( n1 );
-  children.push_back( n2 );
-  return mkAndSelectionFormula( children );
-}
-
-//if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context,
-//   and NULL otherwise
-Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){
-  Trace("sel-form-debug") << "Looking for selection formula " << n << " " << polarity << std::endl;
-  Node ret;
-  if( n.getKind()==NOT ){
-    ret = getSelectionFormula( fn[0], n[0], !polarity, useOption );
-  }else if( n.getKind()==OR || n.getKind()==AND ){
-    //whether we only need to find one or all
-    bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity );
-    std::vector< Node > children;
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      Node fnc = fn[i];
-      Node nc = n[i];
-      Node nn = getSelectionFormula( fnc, nc, polarity, useOption );
-      if( nn.isNull() && !favorPol ){
-        //cannot make selection formula
-        children.clear();
-        break;
-      }
-      if( !nn.isNull() ){
-        //if( favorPol ){   //temporary
-        //  return nn;      //
-        //}                 //
-        if( std::find( children.begin(), children.end(), nn )==children.end() ){
-          children.push_back( nn );
-        }
-      }
-    }
-    if( !children.empty() ){
-      if( favorPol ){
-        //filter which formulas we wish to keep, make disjunction
-        Node min_lit;
-        int min_score = -1;
-        for( size_t i=0; i<children.size(); i++ ){
-          //if it is constant apply uf application, return it for sure
-          if( hasConstantDefinition( children[i] ) ){
-            min_lit = children[i];
-            break;
-          }else{
-            int score = getSelectionFormulaScore( children[i] );
-            if( min_score<0 || score<min_score ){
-              min_score = score;
-              min_lit = children[i];
-            }
-          }
-        }
-        //currently just return the best single literal
-        ret = min_lit;
-      }else{
-        //selection formula must be conjunction of children
-        ret = mkAndSelectionFormula( children );
-      }
-    }else{
-      ret = Node::null();
-    }
-  }else if( n.getKind()==ITE ){
-    Node nn;
-    Node nc[2];
-    //get selection formula for the
-    for( int i=0; i<2; i++ ){
-      nn = getSelectionFormula( fn[0], n[0], i==0, useOption );
-      nc[i] = getSelectionFormula( fn[i+1], n[i+1], polarity, useOption );
-      if( !nn.isNull() && !nc[i].isNull() ){
-        ret = mkAndSelectionFormula( nn, nc[i] );
-        break;
-      }
-    }
-    if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){
-      ret = mkAndSelectionFormula( nc[0], nc[1] );
-    }
-  }else if( n.getKind()==IFF ){
-    bool opPol = !polarity;
-    for( int p=0; p<2; p++ ){
-      Node nn[2];
-      for( int i=0; i<2; i++ ){
-        bool pol = i==0 ? p==0 : ( opPol ? p!=0 : p==0 );
-        nn[i] = getSelectionFormula( fn[i], n[i], pol, useOption );
-        if( nn[i].isNull() ){
-          break;
-        }
-      }
-      if( !nn[0].isNull() && !nn[1].isNull() ){
-        ret = mkAndSelectionFormula( nn[0], nn[1] );
-      }
-    }
-  }else{
-    //literal case
-    //first, check if it is a usable selection literal
-    if( isUsableSelectionLiteral( n, useOption ) ){
-      bool value;
-      if( d_qe->getValuation().hasSatValue( n, value ) ){
-        if( value==polarity ){
-          ret = fn;
-          if( !polarity ){
-            ret = ret.negate();
-          }
-        }else{
-          Trace("sel-form-debug") << "  (wrong polarity)" << std::endl;
-        }
-      }else{
-        Trace("sel-form-debug") << "  (does not have sat value)" << std::endl;
-      }
-    }else{
-      Trace("sel-form-debug") << "  (is not usable literal)" << std::endl;
-    }
-  }
-  Trace("sel-form-debug") << "   return " << ret << std::endl;
-  return ret;
-}
-
-int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){
-  if( fn.getType().isBoolean() ){
-    if( fn.getKind()==APPLY_UF ){
-      Node op = fn.getOperator();
-      //return total number of terms
-      return d_qe->getTermDatabase()->d_op_nonred_count[op];
-    }else{
-      int score = 0;
-      for( size_t i=0; i<fn.getNumChildren(); i++ ){
-        score += getSelectionFormulaScore( fn[i] );
-      }
-      return score;
-    }
-  }else{
-    return 0;
-  }
-}
-
-void QModelBuilderInstGen::setSelectedTerms( Node s ){
-
-  //if it is apply uf and has model basis arguments, then mark term as being "selected"
-  if( s.getKind()==APPLY_UF ){
-    Assert( s.hasAttribute(ModelBasisArgAttribute()) );
-    if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl;
-    if( s.getAttribute(ModelBasisArgAttribute())!=0 ){
-      d_term_selected[ s ] = true;
-      Trace("sel-form-term") << "  " << s << " is a selected term." << std::endl;
-    }
-  }
-  for( int i=0; i<(int)s.getNumChildren(); i++ ){
-    setSelectedTerms( s[i] );
-  }
-}
-
-bool QModelBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){
-  if( n.getKind()==FORALL ){
-    return false;
-  }else if( n.getKind()!=APPLY_UF ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      //if it is a variable, then return false
-      if( n[i].getAttribute(ModelBasisAttribute()) ){
-        return false;
-      }
-    }
-  }
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
-    if( !isUsableSelectionLiteral( n[i], useOption ) ){
-      return false;
-    }
-  }
-  return true;
-}
-
-void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){
-  if( f!=fp ){
-    //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl;
-    //std::cout << "     " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl;
-    int counter = 0;
-    for( size_t i=0; i<fp[0].getNumChildren(); i++ ){
-      if( (int)counter< (int)f[0].getNumChildren() ){
-        if( fp[0][i]==f[0][counter] ){
-          Node n = m.get( counter );
-          if( !n.isNull() ){
-            mp.set( d_qe, i, n );
-          }
-          counter++;
-        }
-      }
-    }
-    mp.add( d_sub_quant_inst[f] );
-  }else{
-    mp.add( m );
-  }
-}
-
-void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
-  FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
-  bool setDefaultVal = true;
-  Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
-  //set the values in the model
-  for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
-    Node n = fmig->d_uf_terms[op][i];
-    if( isTermActive( n ) ){
-      Node v = fmig->getRepresentative( n );
-      fmig->d_uf_model_gen[op].setValue( fm, n, v );
-    }
-    //also possible set as default
-    if( d_term_selected.find( n )!=d_term_selected.end() || n==defaultTerm ){
-      Node v = fmig->getRepresentative( n );
-      fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
-      if( n==defaultTerm ){
-        setDefaultVal = false;
-      }
-    }
-  }
-  //set the overall default value if not set already  (is this necessary??)
-  if( setDefaultVal ){
-    Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
-    fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
-  }
-  fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] );
-  d_uf_model_constructed[op] = true;
-}
-
-bool QModelBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
-  return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true );
-}
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 3e4471fa4..7679cf93f 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -199,58 +199,6 @@ public:
   bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); }
 };
 
-class QModelBuilderInstGen : public QModelBuilderIG
-{
-private:    ///information for (new) InstGen
-  //map from quantifiers to their selection formulas
-  std::map< Node, Node > d_quant_selection_formula;
-  //map of terms that are selected
-  std::map< Node, bool > d_term_selected;
-  //a collection of (complete) InstMatch structures produced for each root quantifier
-  std::map< Node, inst::InstMatchTrie > d_sub_quant_inst_trie;
-  //for each quantifier, a collection of InstMatch structures, representing the children
-  std::map< Node, inst::InstMatchTrie > d_child_sub_quant_inst_trie;
-  //children quantifiers for each quantifier, each is an instance
-  std::map< Node, std::vector< Node > > d_sub_quants;
-  //instances of each partial instantiation with respect to the root
-  std::map< Node, InstMatch > d_sub_quant_inst;
-  //*root* parent of each partial instantiation
-  std::map< Node, Node > d_sub_quant_parent;
-protected:
-  //reset
-  void reset( FirstOrderModel* fm );
-  //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f
-  int initializeQuantifier( Node f, Node fp );
-  //analyze quantifier
-  void analyzeQuantifier( FirstOrderModel* fm, Node f );
-  //do InstGen techniques for quantifier, return number of lemmas produced
-  int doInstGen( FirstOrderModel* fm, Node f );
-  //theory-specific build models
-  void constructModelUf( FirstOrderModel* fm, Node op );
-private:
-  //get selection formula for quantifier body
-  Node getSelectionFormula( Node fn, Node n, bool polarity, int useOption );
-  //get a heuristic score for a selection formula
-  int getSelectionFormulaScore( Node fn );
-  //set selected terms in term
-  void setSelectedTerms( Node s );
-  //is usable selection literal
-  bool isUsableSelectionLiteral( Node n, int useOption );
-  //get parent quantifier match
-  void getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f );
-  //get parent quantifier
-  Node getParentQuantifier( Node f ) { return d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; }
-public:
-  QModelBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
-  ~QModelBuilderInstGen(){}
-  // is term selected
-  bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); }
-  /** exist instantiation ? */
-  bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
-  //has inst gen
-  bool hasInstGen( Node f ) { return !d_quant_selection_formula[f].isNull(); }
-};
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 6ec347031..591034ffc 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -22,7 +22,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/full_model_check.h"
-#include "theory/quantifiers/qinterval_builder.h"
 #include "theory/quantifiers/ambqi_builder.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp
index 9e4cab9fa..ebc1088a8 100644
--- a/src/theory/quantifiers/modes.cpp
+++ b/src/theory/quantifiers/modes.cpp
@@ -85,15 +85,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode)
   case theory::quantifiers::MBQI_NONE:
     out << "MBQI_NONE";
     break;
-  case theory::quantifiers::MBQI_INST_GEN:
-    out << "MBQI_INST_GEN";
-    break;
   case theory::quantifiers::MBQI_FMC:
     out << "MBQI_FMC";
     break;
-  case theory::quantifiers::MBQI_INTERVAL:
-    out << "MBQI_INTERVAL";
-    break;
   case theory::quantifiers::MBQI_ABS:
     out << "MBQI_ABS";
     break;
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index acc883f2a..80dbb783e 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -62,14 +62,10 @@ typedef enum {
   MBQI_GEN_EVAL,
   /** no mbqi */
   MBQI_NONE,
-  /** implementation that mimics inst-gen */
-  MBQI_INST_GEN,
   /** default, mbqi from Section 5.4.2 of AJR thesis */
   MBQI_FMC,
   /** mbqi with integer intervals */
   MBQI_FMC_INTERVAL,
-  /** mbqi with interval abstraction of uninterpreted sorts */
-  MBQI_INTERVAL,
   /** abstract mbqi algorithm */
   MBQI_ABS,
   /** mbqi trust (produce no instantiations) */
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index c2afbbd3e..f01e563df 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -264,14 +264,10 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi
     return MBQI_GEN_EVAL;
   } else if(optarg == "none") {
     return MBQI_NONE;
-  } else if(optarg == "instgen") {
-    return MBQI_INST_GEN;
   } else if(optarg == "default" || optarg ==  "fmc") {
     return MBQI_FMC;
   } else if(optarg == "fmc-interval") {
     return MBQI_FMC_INTERVAL;
-  } else if(optarg == "interval") {
-    return MBQI_INTERVAL;
   } else if(optarg == "abs") {
     return MBQI_ABS;
   } else if(optarg == "trust") {
diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp
deleted file mode 100644
index 5dd6316b3..000000000
--- a/src/theory/quantifiers/qinterval_builder.cpp
+++ /dev/null
@@ -1,1111 +0,0 @@
-/*********************                                                        */
-/*! \file qinterval_builder.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of qinterval builder
- **/
-
-
-#include "theory/quantifiers/qinterval_builder.h"
-#include "theory/quantifiers/term_database.h"
-
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-//lower bound is exclusive
-//upper bound is inclusive
-
-struct QIntSort
-{
-  FirstOrderModelQInt * m;
-  bool operator() (Node i, Node j) {
-    return m->isLessThan( i, j );
-  }
-};
-
-void QIntDef::init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ) {
-  for( unsigned i=0; i<m->getOrderedNumVars( q ); i++ ){
-    l.push_back( Node::null() );
-    u.push_back( m->getMaximum( m->getOrderedVarType( q, i ) ) );
-  }
-}
-
-void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u )
-{
-  Trace(c) << "( ";
-  for( unsigned i=0; i<l.size(); i++ ){
-    if( i>0 ) Trace(c) << ", ";
-    //Trace(c) << l[i] << "..." << u[i];
-    int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;
-    int uindex = m->getRepId( u[i] );
-    Trace(c) << lindex << "..." << uindex;
-  }
-  Trace(c) << " )";
-}
-
-
-int QIntDef::getEvIndex( FirstOrderModelQInt * m, Node n, bool exc ) {
-  if( n.isNull() ){
-    Assert( exc );
-    return 0;
-  }else{
-    int min = 0;
-    int max = (int)(d_def_order.size()-1);
-    while( min!=max ){
-      int index = (min+max)/2;
-      Assert( index>=0 && index<(int)d_def_order.size() );
-      if( n==d_def_order[index] ){
-        max = index;
-        min = index;
-      }else if( m->isLessThan( n, d_def_order[index] ) ){
-        max = index;
-      }else{
-        min = index+1;
-      }
-    }
-    if( n==d_def_order[min] && exc ){
-      min++;
-    }
-    Assert( min>=0 && min<(int)d_def_order.size() );
-    if( ( min!=0 && !m->isLessThan( d_def_order[min-1], n ) && ( !exc || d_def_order[min-1]!=n ) ) ||
-        ( ( exc || d_def_order[min]!=n ) && !m->isLessThan( n, d_def_order[min] ) ) ){
-      Debug("qint-error") << "ERR size : " << d_def_order.size() << ", exc : " << exc << std::endl;
-      for( unsigned i=0; i<d_def_order.size(); i++ ){
-        Debug("qint-error") << "ERR ch #" << i << " : " << d_def_order[i];
-        Debug("qint-error") << " " << m->getRepId( d_def_order[i] ) << std::endl;
-      }
-      Debug("qint-error") << " : " << n << " " << min << " " << m->getRepId( n ) << std::endl;
-    }
-
-    Assert( min==0 || m->isLessThan( d_def_order[min-1], n ) || ( exc && d_def_order[min-1]==n ) );
-    Assert( ( !exc && n==d_def_order[min] ) || m->isLessThan( n, d_def_order[min] ) );
-    return min;
-  }
-}
-
-void QIntDef::addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
-                        Node v, unsigned depth ) {
-  if( depth==0 ){
-    Trace("qint-compose-debug") << "Add entry ";
-    debugPrint( "qint-compose-debug", m, q, l, u );
-    Trace("qint-compose-debug") << " -> " << v << "..." << std::endl;
-  }
-  //Assert( false );
-  if( depth==u.size() ){
-    Assert( d_def_order.empty() );
-    Assert( v.isNull() || v.isConst() || ( v.getType().isSort() && m->getRepId( v )!=-1 ) );
-    d_def_order.push_back( v );
-  }else{
-    /*
-    if( !d_def_order.empty() &&
-        ( l[depth].isNull() || m->isLessThan( l[depth], d_def_order[d_def_order.size()-1] ) ) ){
-      int startEvIndex = getEvIndex( m, l[depth], true );
-      int endEvIndex;
-      if( m->isLessThan( u[depth], d_def_order[d_def_order.size()-1] ) ){
-        endEvIndex = getEvIndex( m, u[depth] );
-      }else{
-        endEvIndex = d_def_order.size()-1;
-      }
-      Trace("qint-compose-debug2") << this << " adding for bounds " << l[depth] << "..." << u[depth] << std::endl;
-      for( int i=startEvIndex; i<=endEvIndex; i++ ){
-        Trace("qint-compose-debug2") << this << " add entry " << d_def_order[i] << std::endl;
-        d_def[d_def_order[i]].addEntry( m, q, l, u, v, depth+1 );
-      }
-    }
-    if( !d_def_order.empty() &&
-         d_def.find(u[depth])==d_def.end() &&
-         !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
-      Trace("qint-compose-debug2") << "Bad : depth : " << depth << std::endl;
-    }
-    Assert( d_def_order.empty() ||
-            d_def.find(u[depth])!=d_def.end() ||
-            m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) );
-
-    if( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
-      Trace("qint-compose-debug2") << this << " add entry new : " << u[depth] << std::endl;
-      d_def_order.push_back( u[depth] );
-      d_def[u[depth]].addEntry( m, q, l, u, v, depth+1 );
-    }
-    */
-    //%%%%%%
-    bool success = true;
-    int nnum = m->getVarOrder( q )->getNextNum( depth );
-    Node pl;
-    Node pu;
-    if( nnum!=-1 ){
-      Trace("qint-compose-debug2") << "...adding entry #" << depth << " is #" << nnum << std::endl;
-      //Assert( l[nnum].isNull() || l[nnum]==l[depth] || m->isLessThan( l[nnum], l[depth] ) );
-      //Assert( u[nnum]==u[depth] || m->isLessThan( u[depth], u[nnum] ) );
-      pl = l[nnum];
-      pu = u[nnum];
-      if( !m->doMeet( l[nnum], u[nnum], l[depth], u[depth], l[nnum], u[nnum] ) ){
-        success = false;
-      }
-    }
-    //%%%%%%
-    if( success ){
-      Node r = u[depth];
-      if( d_def.find( r )!=d_def.end() ){
-        d_def[r].addEntry( m, q, l, u, v, depth+1 );
-      }else{
-        if( !d_def_order.empty() &&
-            !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
-          Trace("qint-compose-debug2") << "Bad : depth : " << depth << " ";
-          Trace("qint-compose-debug2") << d_def_order[d_def_order.size()-1] << " " << u[depth] << std::endl;
-        }
-        Assert( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], r ) );
-        d_def_order.push_back( r );
-        d_def[r].addEntry( m, q, l, u, v, depth+1 );
-      }
-    }
-    if( nnum!=-1 ){
-      l[nnum] = pl;
-      u[nnum] = pu;
-    }
-  }
-}
-
-Node QIntDef::simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
-                          unsigned depth ) {
-  if( d_def.empty() ){
-    if( d_def_order.size()!=0 ){
-      Debug("qint-error") << "Simplify, size = " << d_def_order.size() << std::endl;
-    }
-    Assert( d_def_order.size()==1 );
-    return d_def_order[0];
-  }else{
-    Assert( !d_def_order.empty() );
-    std::vector< Node > newDefs;
-    Node curr;
-    for( unsigned i=0; i<d_def_order.size(); i++ ){
-      Node n = d_def[d_def_order[i]].simplify_r( m, q, il, iu, depth+1 );
-      if( i>0 ){
-        if( n==curr && !n.isNull() ){
-          d_def.erase( d_def_order[i-1] );
-        }else{
-          newDefs.push_back( d_def_order[i-1] );
-        }
-      }
-      curr = n;
-    }
-    newDefs.push_back( d_def_order[d_def_order.size()-1] );
-    d_def_order.clear();
-    d_def_order.insert( d_def_order.end(), newDefs.begin(), newDefs.end() );
-    return d_def_order.size()==1 ? curr : Node::null();
-  }
-}
-
-Node QIntDef::simplify( FirstOrderModelQInt * m, Node q ) {
-  std::vector< Node > l;
-  std::vector< Node > u;
-  if( !q.isNull() ){
-    //init_vec( m, q, l, u );
-  }
-  return simplify_r( m, q, l, u, 0 );
-}
-
-bool QIntDef::isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
-                         unsigned depth ) {
-  if( d_def_order.empty() ){
-    return false;
-  }else if( d_def.empty() ){
-    return true;
-  }else{
-    //get the current maximum
-    Node mx;
-    if( !q.isNull() ){
-      int pnum = m->getVarOrder( q )->getPrevNum( depth );
-      if( pnum!=-1 ){
-        mx = u[pnum];
-      }
-    }
-    if( mx.isNull() ){
-      mx = m->getMaximum( d_def_order[d_def_order.size()-1].getType() );
-    }
-    //if not current maximum
-    if( d_def_order[d_def_order.size()-1]!=mx ){
-      return false;
-    }else{
-      Node pu = u[depth];
-      for( unsigned i=0; i<d_def_order.size(); i++ ){
-        u[depth] = d_def_order[i];
-        if( !d_def[d_def_order[i]].isTotal_r( m, q, l, u, depth+1 ) ){
-          return false;
-        }
-      }
-      u[depth] = pu;
-      return true;
-    }
-  }
-}
-
-bool QIntDef::isTotal( FirstOrderModelQInt * m, Node q ) {
-  std::vector< Node > l;
-  std::vector< Node > u;
-  if( !q.isNull() ){
-    init_vec( m, q, l, u );
-  }
-  return isTotal_r( m, q, l, u, 0 );
-}
-
-void QIntDef::construct_compose_r( FirstOrderModelQInt * m, Node q,
-                                    std::vector< Node >& l, std::vector< Node >& u,
-                                    Node n, QIntDef * f,
-                                    std::vector< Node >& args,
-                                    std::map< unsigned, QIntDef >& children,
-                                    std::map< unsigned, Node >& bchildren,
-                                    QIntVarNumIndex& vindex, unsigned depth ) {
-  //check for short circuit
-  if( !f ){
-    if( !args.empty() ){
-      if( ( n.getKind()==OR && args[args.size()-1]==m->d_true ) ||
-          ( n.getKind()==AND && args[args.size()-1]==m->d_false ) ){
-        addEntry( m, q, l, u, args[args.size()-1] );
-        return;
-      }
-    }
-  }
-
-  for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << "  "; }
-  Trace("qint-compose") << (f ? "U" : "I" ) << "C( ";
-  for( unsigned i=0; i<l.size(); i++ ){
-    if( i>0 ) Trace("qint-compose") << ", ";
-    //Trace("qint-compose") << l[i] << "..." << u[i];
-    int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;
-    int uindex = m->getRepId( u[i] );
-    Trace( "qint-compose" ) << lindex << "..." << uindex;
-  }
-  Trace("qint-compose") << " )...";
-
-  //finished?
-  if( ( f && f->d_def.empty() ) || args.size()==n.getNumChildren() ){
-    if( f ){
-      Assert( f->d_def_order.size()==1 );
-      Trace("qint-compose") << "UVALUE(" << f->d_def_order[0] << ")" << std::endl;
-      addEntry( m, q, l, u, f->d_def_order[0] );
-    }else{
-      Node nn;
-      bool nnSet = false;
-      for( unsigned i=0; i<args.size(); i++ ){
-        if( args[i].isNull() ){
-          nnSet = true;
-          break;
-        }
-      }
-      if( !nnSet ){
-        if( n.getKind()==EQUAL ){
-          nn = NodeManager::currentNM()->mkConst( args[0]==args[1] );
-        }else{
-          //apply the operator to args
-          nn = NodeManager::currentNM()->mkNode( n.getKind(), args );
-          nn = Rewriter::rewrite( nn );
-        }
-      }
-      Trace("qint-compose") << "IVALUE(" << nn << ")" << std::endl;
-      addEntry( m, q, l, u, nn );
-      Trace("qint-compose-debug2") << "...added entry." << std::endl;
-    }
-  }else{
-    //if a non-simple child
-    if( children.find( depth )!=children.end() ){
-      //***************************
-      Trace("qint-compose") << "compound child, recurse" << std::endl;
-      std::vector< int > currIndex;
-      std::vector< int > endIndex;
-      std::vector< Node > prevL;
-      std::vector< Node > prevU;
-      std::vector< QIntDef * > visited;
-      do{
-        Assert( currIndex.size()==visited.size() );
-
-        //populate the vectors
-        while( visited.size()<m->getOrderedNumVars( q ) ){
-          unsigned i = visited.size();
-          QIntDef * qq = visited.empty() ? &children[depth] : visited[i-1]->getChild( currIndex[i-1] );
-          visited.push_back( qq );
-          Node qq_mx = qq->getMaximum();
-          Trace("qint-compose-debug2") << "...Get ev indices " << i << " " << l[i] << " " << u[i] << std::endl;
-          currIndex.push_back( qq->getEvIndex( m, l[i], true ) );
-          Trace("qint-compose-debug2") << "...Done get curr index " << currIndex[currIndex.size()-1] << std::endl;
-          if( m->isLessThan( qq_mx, u[i] ) ){
-            endIndex.push_back( qq->getNumChildren()-1 );
-          }else{
-            endIndex.push_back( qq->getEvIndex( m, u[i] ) );
-          }
-          Trace("qint-compose-debug2") << "...Done get end index " << endIndex[endIndex.size()-1] << std::endl;
-          prevL.push_back( l[i] );
-          prevU.push_back( u[i] );
-          if( !m->doMeet( prevL[i], prevU[i],
-                          qq->getLower( currIndex[i] ), qq->getUpper( currIndex[i] ), l[i], u[i] ) ){
-            Assert( false );
-          }
-        }
-        for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << "  "; }
-        for( unsigned i=0; i<currIndex.size(); i++ ){
-          Trace("qint-compose") << "[" << currIndex[i] << "/" << endIndex[i] << "]";
-        }
-        Trace("qint-compose") << std::endl;
-        //consider the current
-        int activeIndex = visited.size()-1;
-        QIntDef * qa = visited.empty() ? &children[depth] : visited[activeIndex]->getChild( currIndex[activeIndex] );
-        if( f ){
-          int fIndex = f->getEvIndex( m, qa->getValue() );
-          construct_compose_r( m, q, l, u, n, f->getChild( fIndex ), args, children, bchildren, vindex, depth+1 );
-        }else{
-          args.push_back( qa->getValue() );
-          construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );
-          args.pop_back();
-        }
-
-        //increment the index (if possible)
-        while( activeIndex>=0 && currIndex[activeIndex]==endIndex[activeIndex] ){
-          currIndex.pop_back();
-          endIndex.pop_back();
-          l[activeIndex] = prevL[activeIndex];
-          u[activeIndex] = prevU[activeIndex];
-          prevL.pop_back();
-          prevU.pop_back();
-          visited.pop_back();
-          activeIndex--;
-        }
-        if( activeIndex>=0 ){
-          for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << "  "; }
-          Trace("qint-compose-debug") << "Increment at " << activeIndex << std::endl;
-          currIndex[activeIndex]++;
-          if( !m->doMeet( prevL[activeIndex], prevU[activeIndex],
-                          visited[activeIndex]->getLower( currIndex[activeIndex] ),
-                          visited[activeIndex]->getUpper( currIndex[activeIndex] ),
-                          l[activeIndex], u[activeIndex] ) ){
-            Assert( false );
-          }
-        }
-      }while( !visited.empty() );
-      //***************************
-    }else{
-      Assert( bchildren.find( depth )!=bchildren.end() );
-      Node v = bchildren[depth];
-      if( f ){
-        if( v.getKind()==BOUND_VARIABLE ){
-          int vn = vindex.d_var_num[depth];
-          Trace("qint-compose") << "variable #" << vn << ", recurse" << std::endl;
-          //int vn = m->getOrderedVarOccurId( q, n, depth );
-          Trace("qint-compose-debug") << "-process " << v << ", which is var #" << vn << std::endl;
-          Node lprev = l[vn];
-          Node uprev = u[vn];
-          //restrict to last variable in order
-          int pnum = m->getVarOrder( q )->getPrevNum( vn );
-          if( pnum!=-1 ){
-            Trace("qint-compose-debug") << "-restrict to var #" << pnum << " " << l[pnum] << " " << u[pnum] << std::endl;
-            l[vn] = l[pnum];
-            u[vn] = u[pnum];
-          }
-          int startIndex = f->getEvIndex( m, l[vn], true );
-          int endIndex = f->getEvIndex( m, u[vn] );
-          Trace("qint-compose-debug") << "--will process " << startIndex << " " << endIndex << std::endl;
-          for( int i=startIndex; i<=endIndex; i++ ){
-            if( m->doMeet( lprev, uprev, f->getLower( i ), f->getUpper( i ), l[vn], u[vn] ) ){
-              construct_compose_r( m, q, l, u, n, f->getChild( i ), args, children, bchildren, vindex, depth+1 );
-            }else{
-              Assert( false );
-            }
-          }
-          l[vn] = lprev;
-          u[vn] = uprev;
-        }else{
-          Trace("qint-compose") << "value, recurse" << std::endl;
-          //simple
-          int ei = f->getEvIndex( m, v );
-          construct_compose_r( m, q, l, u, n, f->getChild( ei ), args, children, bchildren, vindex, depth+1 );
-        }
-      }else{
-        Trace("qint-compose") << "value, recurse" << std::endl;
-        args.push_back( v );
-        construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );
-        args.pop_back();
-      }
-    }
-  }
-}
-
-
-void QIntDef::construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v ) {
-  if( depth==m->getOrderedNumVars( q ) ){
-    Assert( !v.isNull() );
-    d_def_order.push_back( v );
-  }else{
-    TypeNode tn = m->getOrderedVarType( q, depth );
-    //int vnum = m->getVarOrder( q )->getVar( depth )==
-    if( depth==vn ){
-      for( unsigned i=0; i<m->d_rep_set.d_type_reps[tn].size(); i++ ){
-        Node vv = m->d_rep_set.d_type_reps[tn][i];
-        d_def_order.push_back( vv );
-        d_def[vv].construct_enum_r( m, q, vn, depth+1, vv );
-      }
-    }else if( m->getVarOrder( q )->getVar( depth )==m->getVarOrder( q )->getVar( vn ) && depth>vn ){
-      d_def_order.push_back( v );
-      d_def[v].construct_enum_r( m, q, vn, depth+1, v );
-    }else{
-      Node mx = m->getMaximum( tn );
-      d_def_order.push_back( mx );
-      d_def[mx].construct_enum_r( m, q, vn, depth+1, v );
-    }
-  }
-}
-
-bool QIntDef::construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn ) {
-  TypeNode tn = m->getOrderedVarType( q, vn );
-  if( tn.isSort() ){
-    construct_enum_r( m, q, vn, 0, Node::null() );
-    return true;
-  }else{
-    return false;
-  }
-}
-
-bool QIntDef::construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
-                                 std::map< unsigned, QIntDef >& children,
-                                 std::map< unsigned, Node >& bchildren, int varChCount,
-                                 QIntVarNumIndex& vindex ) {
- Trace("qint-compose") << "Do " << (f ? "uninterpreted" : "interpreted");
- Trace("qint-compose") << " compose, var count = " << varChCount << "..." << std::endl;
-  std::vector< Node > l;
-  std::vector< Node > u;
-  init_vec( m, q, l, u );
-  if( varChCount==0 || f ){
-    //standard (no variable child) interpreted compose, or uninterpreted compose
-    std::vector< Node > args;
-    construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, 0 );
-  }else{
-    //special cases
-    bool success = false;
-    int varIndex = ( bchildren.find( 0 )!=bchildren.end() && bchildren[0].getKind()==BOUND_VARIABLE ) ? 0 : 1;
-    if( varChCount>1 ){
-      if( n.getKind()==EQUAL ){
-        //make it an enumeration
-        unsigned vn = vindex.d_var_num[0];
-        if( children[0].construct_enum( m, q, vn ) ){
-          bchildren.erase( 0 );
-          varIndex = 1;
-          success = true;
-        }
-      }
-    }else{
-      success = n.getKind()==EQUAL;
-    }
-    if( success ){
-      int oIndex = varIndex==0 ? 1 : 0;
-      Node v = bchildren[varIndex];
-      unsigned vn = vindex.d_var_num[varIndex];
-      if( children.find( oIndex )==children.end() ){
-        Assert( bchildren.find( oIndex )!=bchildren.end() );
-        Node at = bchildren[oIndex];
-        Trace("qint-icompose") << "Basic child, " << at << " with var " << v << std::endl;
-        Node prev = m->getPrev( bchildren[oIndex].getType(), bchildren[oIndex] );
-        Node above = u[vn];
-        if( !prev.isNull() ){
-          u[vn] = prev;
-          addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );
-        }
-        l[vn] = prev;
-        u[vn] = at;
-        addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( true ) );
-        if( at!=above ){
-          l[vn] = at;
-          u[vn] = above;
-          addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );
-        }
-      }else{
-        QIntDef * qid = &children[oIndex];
-        qid->debugPrint("qint-icompose", m, q );
-        Trace("qint-icompose") << " against variable..." << v << ", which is var #" << vn << std::endl;
-
-        TypeNode tn = v.getType();
-        QIntDefIter qdi( m, q, qid );
-        while( !qdi.isFinished() ){
-          std::vector< Node > us;
-          qdi.getUppers( us );
-          std::vector< Node > ls;
-          qdi.getLowers( ls );
-          qdi.debugPrint( "qint-icompose" );
-
-          Node n_below = ls[vn];
-          Node n_prev = m->getPrev( tn, qdi.getValue() );
-          Node n_at = qdi.getValue();
-          Node n_above = us[vn];
-          Trace("qint-icompose") << n_below << " < " << n_prev << " < " << n_at << " < " << n_above << std::endl;
-          if( n.getKind()==EQUAL ){
-            bool atLtAbove = m->isLessThan( n_at, n_above );
-            Node currL = n_below;
-            if( n_at==n_above || atLtAbove ){
-              //add for value (at-1)
-              if( !n_prev.isNull() && ( n_below.isNull() || m->isLessThan( n_below, n_prev ) ) ){
-                ls[vn] = currL;
-                us[vn] = n_prev;
-                currL = n_prev;
-                Trace("qint-icompose") << "-add entry(-) at " << ls[vn] << "..." << us[vn] << std::endl;
-                addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( false ) );
-              }
-              //add for value (at)
-              if( ( n_below.isNull() || m->isLessThan( n_below, n_at ) ) && atLtAbove ){
-                ls[vn] = currL;
-                us[vn] = n_at;
-                currL = n_at;
-                Trace("qint-icompose") << "-add entry(=) at " << ls[vn] << "..." << us[vn] << std::endl;
-                addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( true ) );
-              }
-            }
-            ls[vn] = currL;
-            us[vn] = n_above;
-            Trace("qint-icompose") << "-add entry(+) at " << ls[vn] << "..." << us[vn] << std::endl;
-            addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( n_at==n_above ) );
-          }else{
-            return false;
-          }
-          qdi.increment();
-
-          Trace("qint-icompose-debug") << "Now : " << std::endl;
-          debugPrint("qint-icompose-debug", m, q );
-          Trace("qint-icompose-debug") << std::endl;
-        }
-      }
-
-      Trace("qint-icompose") << "Result : " << std::endl;
-      debugPrint("qint-icompose", m, q );
-      Trace("qint-icompose") << std::endl;
-
-    }else{
-      return false;
-    }
-  }
-  Trace("qint-compose") << "Done i-compose" << std::endl;
-  return true;
-}
-
-
-void QIntDef::construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth ) {
-  d_def.clear();
-  d_def_order.clear();
-  Assert( !fapps.empty() );
-  if( depth==fapps[0].getNumChildren() ){
-    //get representative in model for this term
-    Assert( fapps.size()>=1 );
-    Node r = m->getUsedRepresentative( fapps[0] );
-    d_def_order.push_back( r );
-  }else{
-    std::map< Node, std::vector< Node > > fapp_child;
-    //partition based on evaluations of fapps[1][depth]....fapps[n][depth]
-    for( unsigned i=0; i<fapps.size(); i++ ){
-      Node r = m->getUsedRepresentative( fapps[i][depth] );
-      fapp_child[r].push_back( fapps[i] );
-    }
-    //sort by QIntSort
-    for( std::map< Node, std::vector< Node > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
-      d_def_order.push_back( it->first );
-    }
-    QIntSort qis;
-    qis.m = m;
-    std::sort( d_def_order.begin(), d_def_order.end(), qis );
-    //construct children
-    for( unsigned i=0; i<d_def_order.size(); i++ ){
-      Node n = d_def_order[i];
-      if( i==d_def_order.size()-1 ){
-        d_def_order[i] = m->getMaximum( d_def_order[i].getType() );
-      }
-      Debug("qint-model-debug2") << "Construct for " << n << ", terms = " << fapp_child[n].size() << std::endl;
-      d_def[d_def_order[i]].construct( m, fapp_child[n], depth+1 );
-    }
-  }
-}
-
-Node QIntDef::getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth ) {
-  if( d_def.empty() ){
-    Assert( d_def_order.size()==1 );
-    //must convert to actual domain constant
-    if( d_def_order[0].getType().isSort() ){
-      return m->d_rep_set.d_type_reps[ d_def_order[0].getType() ][ m->getRepId( d_def_order[0] ) ];
-    }else{
-      return m->getUsedRepresentative( d_def_order[0] );
-    }
-  }else{
-    TypeNode tn = vars[depth].getType();
-    Node curr;
-    int rep_id = m->d_rep_set.getNumRepresentatives( tn );
-    for( int i=(int)(d_def_order.size()-1); i>=0; i-- ){
-      int curr_rep_id = i==0 ? 0 : m->getRepId( d_def_order[i-1] )+1;
-      Node ccurr = d_def[d_def_order[i]].getFunctionValue( m, vars, depth+1 );
-      if( curr.isNull() ){
-        curr = ccurr;
-      }else{
-        std::vector< Node > c;
-        Assert( curr_rep_id<rep_id );
-        for( int j=curr_rep_id; j<rep_id; j++ ){
-          c.push_back( vars[depth].eqNode( m->d_rep_set.d_type_reps[tn][j] ) );
-        }
-        Node cond = c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( OR, c );
-        curr = NodeManager::currentNM()->mkNode( ITE, cond, ccurr, curr );
-      }
-      rep_id = curr_rep_id;
-    }
-    return curr;
-  }
-}
-
-Node QIntDef::evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth ) {
-  if( depth==reps.size() ){
-    Assert( d_def_order.size()==1 );
-    return d_def_order[0];
-  }else{
-    if( d_def.find( reps[depth] )!=d_def.end() ){
-      return d_def[reps[depth]].evaluate_r( m, reps, depth+1 );
-    }else{
-      int ei = getEvIndex( m, reps[depth] );
-      return d_def[d_def_order[ei]].evaluate_r( m, reps, depth+1 );
-    }
-  }
-}
-Node QIntDef::evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth ) {
-  if( depth==n.getNumChildren() ){
-    Assert( d_def_order.size()==1 );
-    return d_def_order[0];
-  }else{
-    Node r = m->getUsedRepresentative( n[depth] );
-    if( d_def.find( r )!=d_def.end() ){
-      return d_def[r].evaluate_n_r( m, n, depth+1 );
-    }else{
-      int ei = getEvIndex( m, r );
-      return d_def[d_def_order[ei]].evaluate_n_r( m, n, depth+1 );
-    }
-  }
-}
-
-
-
-QIntDef * QIntDef::getChild( unsigned i ) {
-  Assert( i<d_def_order.size() );
-  Assert( d_def.find( d_def_order[i] )!=d_def.end() );
-  return &d_def[ d_def_order[i] ];
-}
-
-void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t ) {
-  /*
-  for( unsigned i=0; i<d_def_order.size(); i++ ){
-    for( int j=0; j<t; j++ ) { Trace(c) << " "; }
-    //Trace(c) << this << " ";
-    Trace(c) << d_def_order[i] << " : " << std::endl;
-    if( d_def.find( d_def_order[i] )!=d_def.end() ){
-      d_def[d_def_order[i]].debugPrint( c, m, t+1 );
-    }
-  }
-  */
-  //if( t==0 ){
-  QIntDefIter qdi( m, q, this );
-  while( !qdi.isFinished() ){
-    qdi.debugPrint( c, t );
-    qdi.increment();
-  }
-  //}
-}
-
-
-QIntDefIter::QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid ) : d_fm( m ), d_q( q ){
-  resetIndex( qid );
-}
-
-void QIntDefIter::debugPrint( const char * c, int t ) {
-  //Trace( c ) << getSize() << " " << d_index_visited.size() << " ";
-  for( int j=0; j<t; j++ ) { Trace(c) << " "; }
-  std::vector< Node > l;
-  std::vector< Node > u;
-  getLowers( l );
-  getUppers( u );
-  QIntDef::debugPrint( c, d_fm, d_q, l, u );
-  Trace( c ) << " -> " << getValue() << std::endl;
-}
-
-void QIntDefIter::resetIndex( QIntDef * qid ){
-  //std::cout << "check : " << qid << " " << qid->d_def_order.size() << " " << qid->d_def.size() << std::endl;
-  if( !qid->d_def.empty() ){
-    //std::cout << "add to visited " <<  qid << std::endl;
-    d_index.push_back( 0 );
-    d_index_visited.push_back( qid );
-    resetIndex( qid->getChild( 0 ) );
-  }
-}
-
-bool QIntDefIter::increment( int index ) {
-  if( !isFinished() ){
-    index = index==-1 ? (int)(d_index.size()-1) : index;
-    while( (int)(d_index.size()-1)>index ){
-      //std::cout << "remove from visit 1 " << std::endl;
-      d_index.pop_back();
-      d_index_visited.pop_back();
-    }
-    while( index>=0 && d_index[index]>=(int)(d_index_visited[index]->d_def_order.size()-1) ){
-      //std::cout << "remove from visit " << d_index_visited[ d_index_visited.size()-1 ] << std::endl;
-      d_index.pop_back();
-      d_index_visited.pop_back();
-      index--;
-    }
-    if( index>=0 ){
-      //std::cout << "increment at index = " << index << std::endl;
-      d_index[index]++;
-      resetIndex( d_index_visited[index]->getChild( d_index[index] ) );
-      return true;
-    }else{
-      d_index.clear();
-      return false;
-    }
-  }else{
-    return false;
-  }
-}
-
-Node QIntDefIter::getLower( int index ) {
-  if( d_index[index]==0 && !d_q.isNull() ){
-    int pnum = d_fm->getVarOrder( d_q )->getPrevNum( index );
-    if( pnum!=-1 ){
-      return getLower( pnum );
-    }
-  }
-  return d_index_visited[index]->getLower( d_index[index] );
-}
-
-Node QIntDefIter::getUpper( int index ) {
-  return d_index_visited[index]->getUpper( d_index[index] );
-}
-
-void QIntDefIter::getLowers( std::vector< Node >& reps ) {
-  for( unsigned i=0; i<getSize(); i++ ){
-    bool added = false;
-    if( d_index[i]==0 && !d_q.isNull() ){
-      int pnum = d_fm->getVarOrder( d_q )->getPrevNum( i );
-      if( pnum!=-1 ){
-        added = true;
-        reps.push_back( reps[pnum] );
-      }
-    }
-    if( !added ){
-      reps.push_back( getLower( i ) );
-    }
-  }
-}
-
-void QIntDefIter::getUppers( std::vector< Node >& reps ) {
-  for( unsigned i=0; i<getSize(); i++ ){
-    reps.push_back( getUpper( i ) );
-  }
-}
-
-Node QIntDefIter::getValue() {
-  return d_index_visited[ d_index_visited.size()-1 ]->getChild( d_index[d_index.size()-1] )->getValue();
-}
-
-
-//------------------------variable ordering----------------------------
-
-QuantVarOrder::QuantVarOrder( Node q ) : d_q( q ) {
-  d_var_count = 0;
-  initialize( q[1], 0, d_var_occur );
-}
-
-int QuantVarOrder::initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex ) {
-  if( n.getKind()!=FORALL ){
-    //std::vector< Node > vars;
-    //std::vector< int > args;
-    int procVarOn = n.getKind()==APPLY_UF ? 0 : 1;
-    for( int r=0; r<=procVarOn; r++ ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( n[i].getKind()==BOUND_VARIABLE && r==procVarOn ){
-          int occ_index = -1;
-          for( unsigned j=0; j<d_var_to_num[n[i]].size(); j++ ){
-            if( d_var_to_num[n[i]][j]>=minVarIndex ){
-              occ_index = d_var_to_num[n[i]][j];
-            }
-          }
-          if( occ_index==-1 ){
-            //need to assign new
-            d_num_to_var[d_var_count] = n[i];
-            if( !d_var_to_num[n[i]].empty() ){
-              int v = d_var_to_num[n[i]][ d_var_to_num[n[i]].size()-1 ];
-              d_num_to_prev_num[ d_var_count ] = v;
-              d_num_to_next_num[ v ] = d_var_count;
-            }
-            d_var_num_index[ d_var_count ] = d_var_to_num[n[i]].size();
-            d_var_to_num[n[i]].push_back( d_var_count );
-            occ_index = d_var_count;
-            d_var_count++;
-          }
-          vindex.d_var_num[i] = occ_index;
-          minVarIndex = occ_index;
-        }else if( r==0 ){
-          minVarIndex = initialize( n[i], minVarIndex, vindex.d_var_index[i] );
-        }
-      }
-    }
-  }
-  return minVarIndex;
-}
-
-bool QuantVarOrder::getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
-                                      std::vector< Node >& inst ) {
-  Debug("qint-var-order-debug2") << "Get for " << d_q << " " << l.size() << " " << u.size() << std::endl;
-  for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
-    Debug("qint-var-order-debug2") << "Get for " << d_q[0][i] << " " << d_var_to_num[d_q[0][i]].size() << std::endl;
-    Node ll = Node::null();
-    Node uu = m->getMaximum( d_q[0][i].getType() );
-    for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
-      Debug("qint-var-order-debug2") << "Go " << j << std::endl;
-      Node cl = ll;
-      Node cu = uu;
-      int index = d_var_to_num[d_q[0][i]][j];
-      Debug("qint-var-order-debug2") << "Do meet for " << index << "..." << std::endl;
-      Debug("qint-var-order-debug2") << l[index] << " " << u[index] << " " << cl << " " << cu << std::endl;
-      if( !m->doMeet( l[index], u[index], cl, cu, ll, uu ) ){
-        Debug("qint-var-order-debug2") << "FAILED" << std::endl;
-        return false;
-      }
-      Debug("qint-var-order-debug2") << "Result : " << ll << " " << uu << std::endl;
-    }
-    Debug("qint-var-order-debug2") << "Got " << uu << std::endl;
-    inst.push_back( uu );
-  }
-  return true;
-}
-
-void QuantVarOrder::debugPrint( const char * c ) {
-  Trace( c ) << "Variable order for " << d_q << " is : " << std::endl;
-  debugPrint( c, d_q[1], d_var_occur );
-  Trace( c ) << std::endl;
-  for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
-    Trace( c ) << d_q[0][i] << " : ";
-    for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
-      Trace( c ) << d_var_to_num[d_q[0][i]][j] << " ";
-    }
-    Trace( c ) << std::endl;
-  }
-}
-
-void QuantVarOrder::debugPrint( const char * c, Node n, QIntVarNumIndex& vindex ) {
-  if( n.getKind()==FORALL ){
-    Trace(c) << "NESTED_QUANT";
-  }else{
-    Trace(c) << n.getKind() << "(";
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( i>0 ) Trace( c ) << ",";
-      Trace( c ) << " ";
-      if( n[i].getKind()==BOUND_VARIABLE ){
-        Trace(c) << "VAR[" << vindex.d_var_num[i] << "]";
-      }else{
-        debugPrint( c, n[i], vindex.d_var_index[i] );
-      }
-      if( i==n.getNumChildren()-1 ) Trace( c ) << " ";
-    }
-    Trace(c) << ")";
-  }
-}
-
-QIntervalBuilder::QIntervalBuilder( context::Context* c, QuantifiersEngine* qe ) :
-QModelBuilder( c, qe ){
-  d_true = NodeManager::currentNM()->mkConst( true );
-}
-
-
-//------------------------model construction----------------------------
-
-void QIntervalBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
-  Trace("fmf-qint-debug") << "process build model " << fullModel << std::endl;
-  FirstOrderModel* f = (FirstOrderModel*)m;
-  FirstOrderModelQInt* fm = f->asFirstOrderModelQInt();
-  if( fullModel ){
-    Trace("qint-model") << "Construct model representation..." << std::endl;
-    //make function values
-    for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-      if( it->first.getType().getNumChildren()>1 ){
-        Trace("qint-model") << "Construct for " << it->first << "..." << std::endl;
-        m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
-      }
-    }
-    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
-    //mark that the model has been set
-    fm->markModelSet();
-    //debug the model
-    debugModel( fm );
-  }else{
-    fm->initialize();
-    //process representatives
-    fm->d_rep_id.clear();
-    fm->d_max.clear();
-    fm->d_min.clear();
-    Trace("qint-model") << std::endl << "Making representatives..." << std::endl;
-    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-         it != fm->d_rep_set.d_type_reps.end(); ++it ){
-      if( it->first.isSort() ){
-        if( it->second.empty() ){
-          std::cout << "Empty rep for " << it->first << std::endl;
-          exit(0);
-        }
-        Trace("qint-model") << "Representatives for " << it->first << " : " << std::endl;
-        for( unsigned i=0; i<it->second.size(); i++ ){
-          Trace("qint-model") << i << " : " << it->second[i] << std::endl;
-          fm->d_rep_id[it->second[i]] = i;
-        }
-        fm->d_min[it->first] = it->second[0];
-        fm->d_max[it->first] = it->second[it->second.size()-1];
-      }else{
-        //TODO: enumerate?
-      }
-    }
-    Trace("qint-model") << std::endl << "Making function definitions..." << std::endl;
-    //construct the models for functions
-    for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-      Node f = it->first;
-      Trace("qint-model-debug") << "Building Model for " << f << std::endl;
-      //reset the model
-      //get all (non-redundant) f-applications
-      std::vector< Node > fapps;
-      Trace("qint-model-debug") << "Initial terms: " << std::endl;
-      for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
-        Node n = fm->d_uf_terms[f][i];
-        if( !n.getAttribute(NoMatchAttribute()) ){
-          Trace("qint-model-debug") << "  " << n << std::endl;
-          fapps.push_back( n );
-        }
-      }
-      if( fapps.empty() ){
-        //choose arbitrary value
-        Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
-        Trace("qint-model-debug") << "Initial terms empty, add " << mbt << std::endl;
-        fapps.push_back( mbt );
-      }
-      //construct the interval model
-      it->second->construct( fm, fapps );
-      Trace("qint-model-debug") << "Definition for " << f << " : " << std::endl;
-      it->second->debugPrint("qint-model-debug", fm, Node::null() );
-
-      it->second->simplify( fm, Node::null() );
-      Trace("qint-model") << "(Simplified) definition for " << f << " : " << std::endl;
-      it->second->debugPrint("qint-model", fm, Node::null() );
-
-      if( Debug.isOn("qint-model-debug") ){
-        for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
-          Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
-          Debug("qint-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
-          Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
-        }
-      }
-    }
-  }
-}
-
-
-//--------------------model checking---------------------------------------
-
-//do exhaustive instantiation
-bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
-  Trace("qint-check") << "exhaustive instantiation " << q << " " << effort << std::endl;
-  if (effort==0) {
-
-    FirstOrderModelQInt * fmqint = fm->asFirstOrderModelQInt();
-    QIntDef qid;
-    doCheck( fmqint, q, qid, q[1], fmqint->d_var_order[q]->d_var_occur );
-    //now process entries
-    Trace("qint-inst") << "Interpretation for " << q << " is : " << std::endl;
-    qid.debugPrint( "qint-inst", fmqint, q );
-    Trace("qint-inst") << std::endl;
-    Debug("qint-check-debug2") << "Make iterator..." << std::endl;
-    QIntDefIter qdi( fmqint, q, &qid );
-    while( !qdi.isFinished() ){
-      if( qdi.getValue()!=d_true ){
-        Debug("qint-check-debug2") << "Set up vectors..." << std::endl;
-        std::vector< Node > l;
-        std::vector< Node > u;
-        std::vector< Node > inst;
-        qdi.getLowers( l );
-        qdi.getUppers( u );
-        Debug("qint-check-debug2") << "Get instantiation..." << std::endl;
-        if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){
-          Trace("qint-inst") << "** Instantiate with ";
-          //just add the instance
-          for( unsigned j=0; j<inst.size(); j++) {
-            Trace("qint-inst") << inst[j] << " ";
-          }
-          Trace("qint-inst") << std::endl;
-          d_triedLemmas++;
-          if( d_qe->addInstantiation( q, inst ) ){
-            Trace("qint-inst") << "   ...added instantiation." << std::endl;
-            d_addedLemmas++;
-          }else{
-            Trace("qint-inst") << "   ...duplicate instantiation" << std::endl;
-            //verify that instantiation is witness for current entry
-            if( Debug.isOn("qint-check-debug2") ){
-              Debug("qint-check-debug2") << "Check if : ";
-              std::vector< Node > exp_inst;
-              for( unsigned i=0; i<fmqint->getOrderedNumVars( q ); i++ ){
-                int index = fmqint->getOrderedVarNumToVarNum( q, i );
-                exp_inst.push_back( inst[ index ] );
-                Debug("qint-check-debug2") << inst[index] << " ";
-              }
-              Debug("qint-check-debug2") << " evaluates to " << qdi.getValue() << std::endl;
-              Assert( qid.evaluate( fmqint, exp_inst )==qdi.getValue() );
-            }
-          }
-        }else{
-          Trace("qint-inst") << "** Spurious instantiation." << std::endl;
-        }
-      }
-      qdi.increment();
-    }
-  }
-  return true;
-}
-
-bool QIntervalBuilder::doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
-                                QIntVarNumIndex& vindex ) {
-  Assert( n.getKind()!=FORALL );
-  std::map< unsigned, QIntDef > children;
-  std::map< unsigned, Node > bchildren;
-  int varChCount = 0;
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    if( n[i].getKind()==FORALL ){
-      bchildren[i] = Node::null();
-    }else if( n[i].getKind() == BOUND_VARIABLE ){
-      varChCount++;
-      bchildren[i] = n[i];
-    }else if( m->hasTerm( n[i] ) ){
-      bchildren[i] = m->getUsedRepresentative( n[i] );
-    }else{
-      if( !doCheck( m, q, children[i], n[i], vindex.d_var_index[i] ) ){
-        bchildren[i] = Node::null();
-      }
-    }
-  }
-  Trace("qint-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;
-  if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){
-    Node op = n.getKind() == APPLY_UF ? n.getOperator() : n;
-    //uninterpreted compose
-    qid.construct_compose( m, q, n, m->d_models[op], children, bchildren, varChCount, vindex );
-  }else if( !qid.construct_compose( m, q, n, NULL, children, bchildren, varChCount, vindex ) ){
-    Trace("qint-check-debug") << "** Cannot produce definition for " << n << std::endl;
-    return false;
-  }
-  Trace("qint-check-debug2") << "Definition for " << n << " is : " << std::endl;
-  qid.debugPrint("qint-check-debug2", m, q);
-  qid.simplify( m, q );
-  Trace("qint-check-debug") << "(Simplified) Definition for " << n << " is : " << std::endl;
-  qid.debugPrint("qint-check-debug", m, q);
-  Trace("qint-check-debug") << std::endl;
-  Assert( qid.isTotal( m, q ) );
-  return true;
-}
diff --git a/src/theory/quantifiers/qinterval_builder.h b/src/theory/quantifiers/qinterval_builder.h
deleted file mode 100644
index 7515f13c6..000000000
--- a/src/theory/quantifiers/qinterval_builder.h
+++ /dev/null
@@ -1,155 +0,0 @@
-/*********************                                                        */
-/*! \file qinterval_builder.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief qinterval model class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef QINTERVAL_BUILDER
-#define QINTERVAL_BUILDER
-
-#include "theory/quantifiers/model_builder.h"
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class FirstOrderModelQInt;
-
-class QIntVarNumIndex
-{
-public:
-  std::map< int, int > d_var_num;
-  std::map< int, QIntVarNumIndex > d_var_index;
-};
-
-class QIntDef
-{
-private:
-  Node evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth );
-  Node evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth );
-  void construct_compose_r( FirstOrderModelQInt * m, Node q,
-                            std::vector< Node >& l, std::vector< Node >& u, Node n, QIntDef * f,
-                            std::vector< Node >& args,
-                            std::map< unsigned, QIntDef >& children,
-                            std::map< unsigned, Node >& bchildren,
-                            QIntVarNumIndex& vindex,
-                            unsigned depth );
-
-  void construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v );
-  int getEvIndex( FirstOrderModelQInt * m, Node n, bool exc = false );
-  void addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
-                 Node v, unsigned depth = 0 );
-  Node simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
-                   unsigned depth );
-  bool isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
-                  unsigned depth );
-public:
-  QIntDef(){}
-  std::map< Node, QIntDef > d_def;
-  std::vector< Node > d_def_order;
-
-  void construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth = 0 );
-  bool construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
-                          std::map< unsigned, QIntDef >& children,
-                          std::map< unsigned, Node >& bchildren, int varChCount,
-                          QIntVarNumIndex& vindex );
-  bool construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn );
-
-  Node evaluate( FirstOrderModelQInt * m, std::vector< Node >& reps ) { return evaluate_r( m, reps, 0 ); }
-  Node evaluate_n( FirstOrderModelQInt * m, Node n ) { return evaluate_n_r( m, n, 0 ); }
-
-  void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t = 0 );
-  QIntDef * getChild( unsigned i );
-  Node getValue() { return d_def_order[0]; }
-  Node getLower( unsigned i ) { return i==0 ? Node::null() : d_def_order[i-1]; }
-  Node getUpper( unsigned i ) { return d_def_order[i]; }
-  Node getMaximum() { return d_def_order.empty() ? Node::null() : getUpper( d_def_order.size()-1 ); }
-  int getNumChildren() { return d_def_order.size(); }
-  bool isTotal( FirstOrderModelQInt * m, Node q );
-
-  Node simplify( FirstOrderModelQInt * m, Node q );
-  Node getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth = 0 );
-
-  static void init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
-  static void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
-};
-
-class QIntDefIter {
-private:
-  FirstOrderModelQInt * d_fm;
-  Node d_q;
-  void resetIndex( QIntDef * qid );
-public:
-  QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid );
-  void debugPrint( const char * c, int t = 0 );
-  std::vector< QIntDef * > d_index_visited;
-  std::vector< int > d_index;
-  bool isFinished() { return d_index.empty(); }
-  bool increment( int index = -1 );
-  unsigned getSize() { return d_index.size(); }
-  Node getLower( int index );
-  Node getUpper( int index );
-  void getLowers( std::vector< Node >& reps );
-  void getUppers( std::vector< Node >& reps );
-  Node getValue();
-};
-
-
-class QuantVarOrder
-{
-private:
-  int initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex );
-  int d_var_count;
-  Node d_q;
-  void debugPrint( const char * c, Node n, QIntVarNumIndex& vindex );
-public:
-  QuantVarOrder( Node q );
-  std::map< int, Node > d_num_to_var;
-  std::map< int, int > d_num_to_prev_num;
-  std::map< int, int > d_num_to_next_num;
-  std::map< Node, std::vector< int > > d_var_to_num;
-  std::map< int, int > d_var_num_index;
-  //std::map< Node, std::map< int, int > > d_var_occur;
-  //int getVarNum( Node n, int arg ) { return d_var_occur[n][arg]; }
-  unsigned getNumVars() { return d_var_count; }
-  Node getVar( int i ) { return d_num_to_var[i]; }
-  int getPrevNum( int i ) { return d_num_to_prev_num.find( i )!=d_num_to_prev_num.end() ? d_num_to_prev_num[i] : -1; }
-  int getNextNum( int i ) { return d_num_to_next_num.find( i )!=d_num_to_next_num.end() ? d_num_to_next_num[i] : -1; }
-  int getVarNumIndex( int i ) { return d_var_num_index[i]; }
-  bool getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
-                         std::vector< Node >& inst );
-  void debugPrint( const char * c );
-  QIntVarNumIndex d_var_occur;
-};
-
-class QIntervalBuilder : public QModelBuilder
-{
-private:
-  Node d_true;
-  bool doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
-                QIntVarNumIndex& vindex );
-public:
-  QIntervalBuilder( context::Context* c, QuantifiersEngine* qe );
-  //process build model
-  void processBuildModel(TheoryModel* m, bool fullModel);
-  //do exhaustive instantiation
-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
-};
-
-
-}
-}
-}
-
-#endif
\ No newline at end of file
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b21494f77..9a4961e2c 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -416,7 +416,7 @@ void TermDb::reset( Theory::Effort effort ){
     }
   }
   Trace("term-db-stats") << "TermDb: Reset" << std::endl;
-  Trace("term-db-stats") << "Congruent/Non-Congruent/Non-Relevant = ";
+  Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
   Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
   if( Debug.isOn("term-db") ){
     Debug("term-db") << "functions : " << std::endl;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index eabba85bf..c10992435 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -34,7 +34,6 @@
 #include "theory/uf/options.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/quantifiers/full_model_check.h"
-#include "theory/quantifiers/qinterval_builder.h"
 #include "theory/quantifiers/ambqi_builder.h"
 
 using namespace std;
@@ -91,8 +90,6 @@ d_lemmas_produced_c(u){
       options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ||
       options::mbqiMode()==quantifiers::MBQI_TRUST ){
     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
-  }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
-    d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" );
   }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
     d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
   }else{
@@ -163,15 +160,9 @@ d_lemmas_produced_c(u){
         options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
       d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
-    }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
-      Trace("quant-engine-debug") << "...make interval builder." << std::endl;
-      d_builder = new quantifiers::QIntervalBuilder( c, this );
     }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
       Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
       d_builder = new quantifiers::AbsMbqiBuilder( c, this );
-    }else if( options::mbqiMode()==quantifiers::MBQI_INST_GEN ){
-      Trace("quant-engine-debug") << "...make inst-gen builder." << std::endl;
-      d_builder = new quantifiers::QModelBuilderInstGen( c, this );
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
       d_builder = new quantifiers::QModelBuilderDefault( c, this );
@@ -676,6 +667,7 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
   return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
 }
 
+/*
 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
   if( options::incrementalSolving() ){
     if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
@@ -696,6 +688,7 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
   }
   return false;
 }
+*/
 
 bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
   if( doCache ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f56cd0d19..199fe79b9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -256,7 +256,7 @@ public:
   /** do substitution */
   Node getSubstitute( Node n, std::vector< Node >& terms );
   /** exist instantiation ? */
-  bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
+  //bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
   /** add lemma lem */
   bool addLemma( Node lem, bool doCache = true );
   /** add require phase */