Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.

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];
 }