14 files changed, 1654 insertions, 70 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index bda124e96..c94775aec 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -16,6 +16,8 @@
 #include "theory/quantifiers/model_engine.h"
 #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"
 
 #define USE_INDEX_ORDERING
 
@@ -27,8 +29,9 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::quantifiers::fmcheck;
 
-FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ),
-d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){
+FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
+TheoryModel( c, name, true ),
+d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){
 
 }
 
@@ -66,16 +69,23 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
 }
 
 void FirstOrderModel::initialize( bool considerAxioms ) {
-  processInitialize();
+  processInitialize( true );
   //this is called after representatives have been chosen and the equality engine has been built
   //for each quantifier, collect all operators we care about
   for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
     Node f = getAssertedQuantifier( i );
+    processInitializeQuantifier( f );
+    if( d_quant_var_id.find( f )==d_quant_var_id.end() ){
+      for(unsigned i=0; i<f[0].getNumChildren(); i++){
+        d_quant_var_id[f][f[0][i]] = i;
+      }
+    }
     if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){
       //initialize relevant models within bodies of all quantifiers
       initializeModelForTerm( f[1] );
     }
   }
+  processInitialize( false );
 }
 
 void FirstOrderModel::initializeModelForTerm( Node n ){
@@ -85,14 +95,30 @@ void FirstOrderModel::initializeModelForTerm( Node n ){
   }
 }
 
-FirstOrderModelIG::FirstOrderModelIG(context::Context* c, std::string name) : FirstOrderModel(c,name) {
+Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
+  //check if there is even any domain elements at all
+  if (!d_rep_set.hasType(tn)) {
+    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
+    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    d_rep_set.add(mbt);
+  }else if( d_rep_set.d_type_reps[tn].size()==0 ){
+    Message() << "empty reps" << std::endl;
+    exit(0);
+  }
+  return d_rep_set.d_type_reps[tn][0];
+}
+
+FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) :
+FirstOrderModel(qe, c,name) {
 
 }
 
-void FirstOrderModelIG::processInitialize(){
-  //rebuild models
-  d_uf_model_tree.clear();
-  d_uf_model_gen.clear();
+void FirstOrderModelIG::processInitialize( bool ispre ){
+  if( ispre ){
+    //rebuild models
+    d_uf_model_tree.clear();
+    d_uf_model_gen.clear();
+  }
 }
 
 void FirstOrderModelIG::processInitializeModelForTerm( Node n ){
@@ -513,10 +539,8 @@ Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & ar
 
 
 
-
-
 FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(c, name), d_qe(qe){
+FirstOrderModel(qe, c, name){
 
 }
 
@@ -552,19 +576,21 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a
   return d_models[n.getOperator()]->evaluate(this, args);
 }
 
-void FirstOrderModelFmc::processInitialize() {
-  if( options::fmfFmcInterval() && intervalOp.isNull() ){
-    std::vector< TypeNode > types;
-    for(unsigned i=0; i<2; i++){
-      types.push_back(NodeManager::currentNM()->integerType());
+void FirstOrderModelFmc::processInitialize( bool ispre ) {
+  if( ispre ){
+    if( options::fmfFmcInterval() && intervalOp.isNull() ){
+      std::vector< TypeNode > types;
+      for(unsigned i=0; i<2; i++){
+        types.push_back(NodeManager::currentNM()->integerType());
+      }
+      TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() );
+      intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" );
     }
-    TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() );
-    intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" );
-  }
-  for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
-    it->second->reset();
+    for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
+      it->second->reset();
+    }
+    d_model_basis_rep.clear();
   }
-  d_model_basis_rep.clear();
 }
 
 void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
@@ -575,19 +601,6 @@ void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
   }
 }
 
-Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){
-  //check if there is even any domain elements at all
-  if (!d_rep_set.hasType(tn)) {
-    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
-    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
-    d_rep_set.d_type_reps[tn].push_back(mbt);
-  }else if( d_rep_set.d_type_reps[tn].size()==0 ){
-    Message() << "empty reps" << std::endl;
-    exit(0);
-  }
-  return d_rep_set.d_type_reps[tn][0];
-}
-
 
 bool FirstOrderModelFmc::isStar(Node n) {
   return n==getStar(n.getType());
@@ -684,3 +697,163 @@ bool FirstOrderModelFmc::isInRange( Node v, Node i ) {
     return v==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 );
+}
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index b5bdff9ee..ab3a1aa52 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -33,16 +33,21 @@ class FirstOrderModelIG;
 namespace fmcheck {
   class FirstOrderModelFmc;
 }
+class FirstOrderModelQInt;
 
 class FirstOrderModel : public TheoryModel
 {
-private:
+protected:
+  /** quant engine */
+  QuantifiersEngine * d_qe;
   /** whether an axiom is asserted */
   context::CDO< bool > d_axiom_asserted;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
   /** is model set */
   context::CDO< bool > d_isModelSet;
+  /** get variable id */
+  std::map< Node, std::map< Node, int > > d_quant_var_id;
   /** get current model value */
   virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
 public: //for Theory Quantifiers:
@@ -57,20 +62,28 @@ public: //for Theory Quantifiers:
   /** initialize model for term */
   void initializeModelForTerm( Node n );
   virtual void processInitializeModelForTerm( Node n ) = 0;
+  virtual void processInitializeQuantifier( Node q ) {}
 public:
-  FirstOrderModel( context::Context* c, std::string name );
+  FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
   virtual ~FirstOrderModel(){}
   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
+  virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
   // initialize the model
   void initialize( bool considerAxioms = true );
-  virtual void processInitialize() = 0;
+  virtual void processInitialize( bool ispre ) = 0;
   /** mark model set */
   void markModelSet() { d_isModelSet = true; }
   /** is model set */
   bool isModelSet() { return d_isModelSet; }
   /** get current model value */
   Node getCurrentModelValue( Node n, bool partial = false );
+  /** get variable id */
+  int getVariableId(Node f, Node n) {
+    return d_quant_var_id.find( f )!=d_quant_var_id.end() ? d_quant_var_id[f][n] : -1;
+  }
+  /** get some domain element */
+  Node getSomeDomainElement(TypeNode tn);
 };/* class FirstOrderModel */
 
 
@@ -93,10 +106,10 @@ private:
   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 //the following functions are for evaluating quantifier bodies
 public:
-  FirstOrderModelIG(context::Context* c, std::string name);
+  FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
   FirstOrderModelIG * asFirstOrderModelIG() { return this; }
   // initialize the model
-  void processInitialize();
+  void processInitialize( bool ispre );
   //for initialize model
   void processInitializeModelForTerm( Node n );
   /** reset evaluation */
@@ -128,8 +141,6 @@ class FirstOrderModelFmc : public FirstOrderModel
 {
   friend class FullModelChecker;
 private:
-  /** quant engine */
-  QuantifiersEngine * d_qe;
   /** models for UF */
   std::map<Node, Def * > d_models;
   std::map<TypeNode, Node > d_model_basis_rep;
@@ -143,8 +154,7 @@ public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
   FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
   // initialize the model
-  void processInitialize();
-
+  void processInitialize( bool ispre );
   Node getFunctionValue(Node op, const char* argPrefix );
 
   bool isStar(Node n);
@@ -152,7 +162,6 @@ public:
   Node getStarElement(TypeNode tn);
   bool isModelBasisTerm(Node n);
   Node getModelBasisTerm(TypeNode tn);
-  Node getSomeDomainElement(TypeNode tn);
   bool isInterval(Node n);
   Node getInterval( Node lb, Node ub );
   bool isInRange( Node v, Node i );
@@ -161,6 +170,50 @@ public:
 }
 
 
+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 );
+};
+
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 2f32ec5e6..174e26a5a 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -588,7 +588,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
         std::vector< TypeNode > types;
         for(unsigned i=0; i<f[0].getNumChildren(); i++){
           types.push_back(f[0][i].getType());
-          d_quant_var_id[f][f[0][i]] = i;
         }
         TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
         Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
@@ -599,7 +598,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
         initializeType( fmfmc, f[0][i].getType() );
       }
 
-      if( !options::fmfModelBasedInst() ){
+      if( options::mbqiMode()==MBQI_NONE ){
         //just exhaustive instantiate
         Node c = mkCondDefault( fmfmc, f );
         d_quant_models[f].addEntry( fmfmc, c, d_false );
@@ -958,8 +957,8 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
   }else{
     TypeNode tn = eq[0].getType();
     if( tn.isSort() ){
-      int j = getVariableId(f, eq[0]);
-      int k = getVariableId(f, eq[1]);
+      int j = fm->getVariableId(f, eq[0]);
+      int k = fm->getVariableId(f, eq[1]);
       if( !fm->d_rep_set.hasType( tn ) ){
         getSomeDomainElement( fm, tn );  //to verify the type is initialized
       }
@@ -977,7 +976,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
 }
 
 void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {
-  int j = getVariableId(f, v);
+  int j = fm->getVariableId(f, v);
   for (unsigned i=0; i<dc.d_cond.size(); i++) {
     Node val = dc.d_value[i];
     if( val.isNull() ){
@@ -1074,7 +1073,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     Trace("fmc-uf-process") << "Process " << v << std::endl;
     bool bind_var = false;
     if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
-      int j = getVariableId(f, v);
+      int j = fm->getVariableId(f, v);
       Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
       if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) {
         v = cond[j+1];
@@ -1084,7 +1083,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     }
     if (bind_var) {
       Trace("fmc-uf-process") << "bind variable..." << std::endl;
-      int j = getVariableId(f, v);
+      int j = fm->getVariableId(f, v);
       if( fm->isStar(cond[j+1]) ){
         for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
           cond[j+1] = it->first;
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 606392831..db5abb01e 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -92,7 +92,6 @@ protected:
   std::map<Node, Node > d_quant_cond;
   std::map< TypeNode, Node > d_array_cond;
   std::map< Node, Node > d_array_term_cond;
-  std::map<Node, std::map< Node, int > > d_quant_var_id;
   std::map<Node, std::vector< int > > d_star_insts;
   void initializeType( FirstOrderModelFmc * fm, TypeNode tn );
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
@@ -138,7 +137,6 @@ public:
 
   bool optBuildAtFullModel();
 
-  int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index ea6f2d775..468c78978 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -44,7 +44,7 @@ bool QModelBuilder::isQuantifierActive( Node f ) {
 
 
 bool QModelBuilder::optUseModel() {
-  return options::fmfModelBasedInst() || options::fmfBoundInt();
+  return options::mbqiMode()!=MBQI_NONE || options::fmfBoundInt();
 }
 
 void QModelBuilder::debugModel( FirstOrderModel* fm ){
@@ -124,6 +124,7 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::
 void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelIG* fm = f->asFirstOrderModelIG();
+  Trace("model-engine-debug") << "Process build model, fullModel = " << fullModel << " " << optUseModel() << std::endl;
   if( fullModel ){
     Assert( d_curr_model==fm );
     //update models
@@ -145,7 +146,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
     reset( fm );
     //only construct first order model if optUseModel() is true
     if( optUseModel() ){
-      Trace("model-engine-debug") << "Initializing quantifiers..." << std::endl;
+      Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
       //check if any quantifiers are un-initialized
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node f = fm->getAssertedQuantifier( i );
@@ -397,7 +398,6 @@ bool QModelBuilderIG::isTermActive( Node n ){
 //do exhaustive instantiation
 bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   if( optUseModel() ){
-
     RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
       FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
@@ -456,7 +456,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         d_statistics.d_eval_lits += fmig->d_eval_lits;
         d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
       }
-      Trace("inst-fmf-ei") << "Finished: " << std::endl;
+      Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
       Trace("inst-fmf-ei") << "   Inst Tried: " << d_triedLemmas << std::endl;
       Trace("inst-fmf-ei") << "   Inst Added: " << d_addedLemmas << std::endl;
       if( d_addedLemmas>1000 ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 99f5e8df6..5006a8a61 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -21,6 +21,8 @@
 #include "theory/quantifiers/first_order_model.h"
 #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"
 
 using namespace std;
 using namespace CVC4;
@@ -34,11 +36,18 @@ using namespace CVC4::theory::inst;
 ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ){
 
-  if( options::fmfFullModelCheck() || options::fmfBoundInt() ){
+  Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
+  if( options::mbqiMode()==MBQI_FMC || options::fmfBoundInt() ){
+    Trace("model-engine-debug") << "...make fmc builder." << std::endl;
     d_builder = new fmcheck::FullModelChecker( c, qe );
-  }else if( options::fmfNewInstGen() ){
+  }else if( options::mbqiMode()==MBQI_INTERVAL ){
+    Trace("model-engine-debug") << "...make interval builder." << std::endl;
+    d_builder = new QIntervalBuilder( c, qe );
+  }else if( options::mbqiMode()==MBQI_INST_GEN ){
+    Trace("model-engine-debug") << "...make inst-gen builder." << std::endl;
     d_builder = new QModelBuilderInstGen( c, qe );
   }else{
+    Trace("model-engine-debug") << "...make default model builder." << std::endl;
     d_builder = new QModelBuilderDefault( c, qe );
   }
 
@@ -203,7 +212,7 @@ int ModelEngine::checkModel(){
   }
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
-  int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1;
+  int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1;
   for( int e=0; e<e_max; e++) {
     if (d_addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 0c3c74b5f..fcbba7aee 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -20,7 +20,6 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/model_builder.h"
 #include "theory/theory_model.h"
-#include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp
index 7da3b150f..10185914e 100644
--- a/src/theory/quantifiers/modes.cpp
+++ b/src/theory/quantifiers/modes.cpp
@@ -77,5 +77,28 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
+  switch(mode) {
+  case theory::quantifiers::MBQI_DEFAULT:
+    out << "MBQI_DEFAULT";
+    break;
+  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;
+  default:
+    out << "MbqiMode!UNKNOWN";
+  }
+  return out;
+}
+
 }/* CVC4 namespace */
 
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index edf9c78fe..7c4cb3651 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -55,6 +55,22 @@ typedef enum {
   AXIOM_INST_MODE_PRIORITY,
 } AxiomInstMode;
 
+typedef enum {
+  /** default, mbqi from CADE 24 paper */
+  MBQI_DEFAULT,
+  /** no mbqi */
+  MBQI_NONE,
+  /** implementation that mimics inst-gen */
+  MBQI_INST_GEN,
+  /** 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,
+} MbqiMode;
+
+
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 1eb98e7b7..f485b981c 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -95,11 +95,9 @@ option internalReps /--disable-quant-internal-reps bool :default true
 option finiteModelFind --finite-model-find bool :default false
  use finite model finding heuristic for quantifier instantiation
 
-option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
- disable model-based quantifier instantiation for finite model finding
+option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
+ choose mode for model-based quantifier instantiation
 
-option fmfFullModelCheck --fmf-fmc bool :default false :read-write
- enable full model check for finite model finding
 option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
 option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true
@@ -115,8 +113,6 @@ option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
 option fmfRelevantDomain --fmf-relevant-domain bool :default false
  use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
-option fmfNewInstGen --fmf-new-inst-gen bool :default false
- use new inst gen technique for answering sat without exhaustive instantiation
 option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
  enable Inst-Gen instantiation techniques for finite model finding (default)
 /disable Inst-Gen instantiation techniques for finite model finding
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 410578af0..a119bcaf6 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -73,6 +73,28 @@ priority \n\
 \n\
 ";
 
+static const std::string mbqiModeHelp = "\
+Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
+\n\
+default \n\
++ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+  model finding paper.\n\
+\n\
+none \n\
++ Disable model-based quantifier instantiation.\n\
+\n\
+instgen \n\
++ Use instantiation algorithm that mimics Inst-Gen calculus. \n\
+\n\
+fmc \n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\
+  Modulo Theories.\n\
+\n\
+interval \n\
++ Use algorithm that abstracts domain elements as intervals. \n\
+\n\
+";
+
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
     return INST_WHEN_PRE_FULL;
@@ -135,6 +157,30 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar
   }
 }
 
+inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "default") {
+    return MBQI_DEFAULT;
+  } else if(optarg ==  "none") {
+    return MBQI_NONE;
+  } else if(optarg ==  "instgen") {
+    return MBQI_INST_GEN;
+  } else if(optarg ==  "fmc") {
+    return MBQI_FMC;
+  } else if(optarg ==  "interval") {
+    return MBQI_INTERVAL;
+  } else if(optarg ==  "help") {
+    puts(mbqiModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --mbqi: `") +
+                          optarg + "'.  Try --mbqi help.");
+  }
+}
+
+inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) throw(OptionException) {
+
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp
new file mode 100755
index 000000000..ce85cecc0
--- /dev/null
+++ b/src/theory/quantifiers/qinterval_builder.cpp
@@ -0,0 +1,1111 @@
+/*********************                                                        */

+/*! \file qinterval_builder.cpp

+ ** \verbatim

+ ** Original author: Andrew Reynolds

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2013  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"

+

+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( d_considerAxioms );

+    //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

+          InstMatch m;

+          for( unsigned j=0; j<inst.size(); j++) {

+            m.set( d_qe, q, j, inst[j] );

+            Trace("qint-inst") << inst[j] << " ";

+          }

+          Trace("qint-inst") << std::endl;

+          d_triedLemmas++;

+          if( d_qe->addInstantiation( q, m ) ){

+            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
new file mode 100755
index 000000000..8f48776cc
--- /dev/null
+++ b/src/theory/quantifiers/qinterval_builder.h
@@ -0,0 +1,155 @@
+/*********************                                                        */

+/*! \file qinterval_builder.h

+ ** \verbatim

+ ** Original author: Andrew Reynolds

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2013  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 e18a4e0dc..6b1368be1 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -146,6 +146,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
              if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
                NoMatchAttribute nma;
                n.setAttribute(nma,true);
+               Debug("term-db-cong") << n << " is redundant." << std::endl;
                congruentCount++;
              }else{
                nonCongruentCount++;
@@ -173,6 +174,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
              if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
                NoMatchAttribute nma;
                en.setAttribute(nma,true);
+               Debug("term-db-cong") << en << " is redundant." << std::endl;
                congruentCount++;
              }else{
                nonCongruentCount++;
@@ -222,10 +224,14 @@ Node TermDb::getModelBasisOpTerm( Node op ){
     TypeNode t = op.getType();
     std::vector< Node > children;
     children.push_back( op );
-    for( size_t i=0; i<t.getNumChildren()-1; i++ ){
+    for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){
       children.push_back( getModelBasisTerm( t[i] ) );
     }
-    d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+    if( children.size()==1 ){
+      d_model_basis_op_term[op] = op;
+    }else{
+      d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+    }
   }
   return d_model_basis_op_term[op];
 }