Refactoring of model engine to separate individual implementations of model builder. Begin work on interval models for integers. Other minor cleanup.

14 files changed, 430 insertions, 338 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e402a8969..37bf6436b 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -218,16 +218,22 @@ void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
 void BoundedIntegers::registerQuantifier( Node f ) {

   Trace("bound-int") << "Register quantifier " << f << std::endl;

   bool hasIntType = false;

+  int finiteTypes = 0;

   std::map< Node, int > numMap;

   for( unsigned i=0; i<f[0].getNumChildren(); i++) {

     numMap[f[0][i]] = i;

     if( f[0][i].getType().isInteger() ){

       hasIntType = true;

     }

+    else if( f[0][i].getType().isSort() ){

+      finiteTypes++;

+    }

   }

   if( hasIntType ){

     bool success;

     do{

+      //std::map< int, std::map< Node, Node > > bound_lit_map;

+      //std::map< int, std::map< Node, bool > > bound_lit_pol_map;

       success = false;

       process( f, f[1], true );

       for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){

@@ -248,7 +254,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
       d_range[f][v] = Rewriter::rewrite( r );

       Trace("bound-int") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;

     }

-    if( d_set[f].size()==f[0].getNumChildren() ){

+    if( d_set[f].size()==(f[0].getNumChildren()-finiteTypes) ){

       d_bound_quants.push_back( f );

       for( unsigned i=0; i<d_set[f].size(); i++) {

         Node v = d_set[f][i];

@@ -256,29 +262,6 @@ void BoundedIntegers::registerQuantifier( Node f ) {
         if( quantifiers::TermDb::hasBoundVarAttr(r) ){

           //introduce a new bound

           Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );

-          /*

-          std::vector< Node > bvs;

-          quantifiers::TermDb::getBoundVars(r, bvs);

-          Assert(bvs.size()>0);

-          Node body = NodeManager::currentNM()->mkNode( LEQ, r, new_range );

-          std::vector< Node > children;

-          //get all the other bounds

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

-            Node l = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst(Rational(0)), bvs[j]);

-            Node u = NodeManager::currentNM()->mkNode( LEQ, bvs[j], d_range[f][bvs[j]] );

-            children.push_back(l);

-            children.push_back(u);

-          }

-          Node antec = NodeManager::currentNM()->mkNode( AND, children );

-          body = NodeManager::currentNM()->mkNode( IMPLIES, antec, body );

-

-          Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );

-

-          Node lem = NodeManager::currentNM()->mkNode( FORALL, bvl, body );

-          Trace("bound-int") << "For " << v << ", the quantified formula " << lem << " will be used to minimize the bound." << std::endl;

-          Trace("bound-int-lemma") << " *** bound int: bounding quantified lemma " << lem << std::endl;

-          d_quantEngine->getOutputChannel().lemma( lem );

-          */

           d_nground_range[f][v] = d_range[f][v];

           d_range[f][v] = new_range;

           r = new_range;

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index b775ea1b0..ad433edf5 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -553,6 +553,14 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a
 }
 
 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());
+    }
+    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();
   }
@@ -635,3 +643,11 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   curr = Rewriter::rewrite( curr );
   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
 }
+
+bool FirstOrderModelFmc::isInterval(Node n) {
+  return n.getKind()==APPLY_UF && n.getOperator()==intervalOp;
+}
+
+Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){
+  return NodeManager::currentNM()->mkNode( APPLY_UF, intervalOp, lb, ub );
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index c2d82cc0a..d79171f68 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -134,6 +134,7 @@ private:
   std::map<Node, Def * > d_models;
   std::map<TypeNode, Node > d_model_basis_rep;
   std::map<TypeNode, Node > d_type_star;
+  Node intervalOp;
   Node getUsedRepresentative(Node n, bool strict = false);
   /** get current model value */
   Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
@@ -151,6 +152,8 @@ public:
   bool isModelBasisTerm(Node n);
   Node getModelBasisTerm(TypeNode tn);
   Node getSomeDomainElement(TypeNode tn);
+  bool isInterval(Node n);
+  Node getInterval( Node lb, Node ub );
 };
 
 }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 4411d205e..7f30a045e 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -34,11 +34,21 @@ struct ModelBasisArgSort
 };

 

 

+struct ConstRationalSort

+{

+  std::vector< Node > d_terms;

+  bool operator() (int i, int j) {

+    return (d_terms[i].getConst<Rational>() < d_terms[j].getConst<Rational>() );

+  }

+};

+

+

 bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {

   if (index==(int)c.getNumChildren()) {

     return d_data!=-1;

   }else{

-    Node st = m->getStar(c[index].getType());

+    TypeNode tn = c[index].getType();

+    Node st = m->getStar(tn);

     if(d_child.find(st)!=d_child.end()) {

       if( d_child[st].hasGeneralization(m, c, index+1) ){

         return true;

@@ -49,6 +59,26 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
         return true;

       }

     }

+    //for star: check if all children are defined and have generalizations

+    if( options::fmfFmcCoverSimplify() && c[index]==st ){

+      //check if all children exist and are complete

+      int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);

+      if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){

+        bool complete = true;

+        for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){

+          if( !m->isStar(it->first) ){

+            if( !it->second.hasGeneralization(m, c, index+1) ){

+              complete = false;

+              break;

+            }

+          }

+        }

+        if( complete ){

+          return true;

+        }

+      }

+    }

+

     return false;

   }

 }

@@ -179,12 +209,12 @@ bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {
   if (d_et.hasGeneralization(m, c)) {

     return false;

   }

-  if( options::fmfFmcCoverSimplify() ){

-    if( d_et.isCovered(m, c, 0) ){

-      Trace("fmc-cover-simplify") << "Entry " << c << " is covered." << std::endl;

-      return false;

-    }

-  }

+  //if( options::fmfFmcCoverSimplify() ){

+  //  if( d_et.isCovered(m, c, 0) ){

+  //    Trace("fmc-cover-simplify") << "Entry " << c << " is covered." << std::endl;

+  //    return false;

+  //  }

+  //}

   int newIndex = (int)d_cond.size();

   if (!d_has_simplified) {

     std::vector<int> compat;

@@ -257,7 +287,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
     }

     if( !last_all_stars ){

       Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl;

-      Trace("fmc-cover-simplify") << "Beforehand: " << std::endl;

+      Trace("fmc-cover-simplify") << "Before: " << std::endl;

       debugPrint("fmc-cover-simplify",Node::null(), mc);

       Trace("fmc-cover-simplify") << std::endl;

       std::vector< Node > cond;

@@ -281,70 +311,11 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
       }

       Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;

       basic_simplify( m );

-      Trace("fmc-cover-simplify") << "Afterhand: " << std::endl;

-      debugPrint("fmc-cover-simplify",Node::null(), mc);

-      Trace("fmc-cover-simplify") << std::endl;

-    }

-  }

-

-

-/*

-  //now do exhaustive covering simplification

-  if( options::fmfFmcCoverSimplify() && !d_cond.empty() ){

-    std::vector< int > indices;

-    std::map< int, std::vector< int > > star_replace;

-    d_et.exhaustiveSimplify( m, d_cond[0], 0, indices, star_replace );

-    if( !indices.empty() ){

-      static bool appSimp = false;

-      if( !appSimp ){

-        appSimp = true;

-        std::cout << "FMC-CS" << std::endl;

-      }

-      Trace("fmc-cover-simplify") << "Beforehand: " << std::endl;

-      debugPrint("fmc-cover-simplify",Node::null(), mc);

-      Trace("fmc-cover-simplify") << std::endl;

-      d_has_simplified = false;

-      Trace("fmc-cover-simplify") << "By exhaustive covering, these indices can be removed : ";

-      for( unsigned i=0; i<indices.size(); i++) {

-        Trace("fmc-cover-simplify") << indices[i] << " ";

-      }

-      Trace("fmc-cover-simplify") << std::endl;

-      std::vector< Node > cond;

-      cond.insert( cond.end(), d_cond.begin(), d_cond.end() );

-      d_cond.clear();

-      std::vector< Node > value;

-      value.insert( value.end(), d_value.begin(), d_value.end() );

-      d_value.clear();

-      d_et.reset();

-      d_has_simplified = false;

-      for (unsigned i=0; i<cond.size(); i++) {

-        if( std::find( indices.begin(), indices.end(), i )==indices.end() ){

-          Node cc = cond[i];

-          if(star_replace.find(i)!=star_replace.end()) {

-            std::vector< Node > nc;

-            nc.push_back( cc.getOperator() );

-            Trace("fmc-cover-simplify") << "Modify entry : " << cc << std::endl;

-            for( unsigned j=0; j< cc.getNumChildren(); j++){

-              if( std::find( star_replace[i].begin(), star_replace[i].end(), j )!=star_replace[i].end() ){

-                nc.push_back( m->getStar(cc[j].getType()) );

-              }else{

-                nc.push_back( cc[j] );

-              }

-            }

-            cc = NodeManager::currentNM()->mkNode( APPLY_UF, nc );

-            Trace("fmc-cover-simplify") << "Got : " << cc << std::endl;

-          }

-          addEntry(m, cc, value[i]);

-        }

-      }

-      Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;

-      basic_simplify( m );

-      Trace("fmc-cover-simplify") << "Afterhand: " << std::endl;

+      Trace("fmc-cover-simplify") << "After: " << std::endl;

       debugPrint("fmc-cover-simplify",Node::null(), mc);

       Trace("fmc-cover-simplify") << std::endl;

     }

   }

-  */

 }

 

 void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {

@@ -371,7 +342,6 @@ QModelBuilder( c, qe ){
 }

 

 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){

-  d_addedLemmas = 0;

   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();

   if( fullModel ){

     //make function values

@@ -455,34 +425,78 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       //reset the model

       fm->d_models[op]->reset();

 

-      std::vector< Node > conds;

-      std::vector< Node > values;

-      std::vector< Node > entry_conds;

       Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;

       for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){

         Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]);

         Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;

       }

       Trace("fmc-model-debug") << std::endl;

-      //initialize the model

+

+

+      std::vector< Node > add_conds;

+      std::vector< Node > add_values;

+      bool needsDefault = true;

       for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){

         Node n = fm->d_uf_terms[op][i];

         if( !n.getAttribute(NoMatchAttribute()) ){

-          addEntry(fm, op, n, n, conds, values, entry_conds);

+          add_conds.push_back( n );

+          add_values.push_back( n );

         }

       }

-      Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);

-      //add default value

-      if( fm->hasTerm( nmb ) ){

-        Trace("fmc-model-debug") << "Add default " << nmb << std::endl;

-        addEntry(fm, op, nmb, nmb, conds, values, entry_conds);

-      }else{

-        Node vmb = getSomeDomainElement(fm, nmb.getType());

-        Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";

-        Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;

-        addEntry(fm, op, nmb, vmb, conds, values, entry_conds);

+      //possibly get default

+      if( needsDefault ){

+        Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);

+        //add default value if necessary

+        if( fm->hasTerm( nmb ) ){

+          Trace("fmc-model-debug") << "Add default " << nmb << std::endl;

+          add_conds.push_back( nmb );

+          add_values.push_back( nmb );

+        }else{

+          Node vmb = getSomeDomainElement(fm, nmb.getType());

+          Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";

+          Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;

+          add_conds.push_back( nmb );

+          add_values.push_back( vmb );

+        }

+      }

+

+      std::vector< Node > conds;

+      std::vector< Node > values;

+      std::vector< Node > entry_conds;

+      //get the entries for the mdoel

+      for( size_t i=0; i<add_conds.size(); i++ ){

+        Node c = add_conds[i];

+        Node v = add_values[i];

+        std::vector< Node > children;

+        std::vector< Node > entry_children;

+        children.push_back(op);

+        entry_children.push_back(op);

+        bool hasNonStar = false;

+        for( unsigned i=0; i<c.getNumChildren(); i++) {

+          Node ri = fm->getUsedRepresentative( c[i]);

+          children.push_back(ri);

+          if (fm->isModelBasisTerm(ri)) {

+            ri = fm->getStar( ri.getType() );

+          }else{

+            hasNonStar = true;

+          }

+          entry_children.push_back(ri);

+        }

+        Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );

+        Node nv = fm->getUsedRepresentative( v);

+        Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );

+        if( std::find(conds.begin(), conds.end(), n )==conds.end() ){

+          Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;

+          conds.push_back(n);

+          values.push_back(nv);

+          entry_conds.push_back(en);

+        }

+        else {

+          Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;

+        }

       }

 

+

       //sort based on # default arguments

       std::vector< int > indices;

       ModelBasisArgSort mbas;

@@ -493,13 +507,32 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       }

       std::sort( indices.begin(), indices.end(), mbas );

 

-

       for (int i=0; i<(int)indices.size(); i++) {

         fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);

       }

       fm->d_models[op]->debugPrint("fmc-model", op, this);

       Trace("fmc-model") << std::endl;

 

+      if( options::fmfFmcInterval() ){

+        Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;

+        fm->d_models[op]->debugPrint("fmc-interval-model", op, this);

+        Trace("fmc-interval-model") << std::endl;

+        std::vector< int > indices;

+        for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){

+          indices.push_back( i );

+        }

+        std::map< int, std::map< int, Node > > changed_vals;

+        makeIntervalModel( fm, op, indices, 0, changed_vals );

+        for( std::map< int, std::map< int, Node > >::iterator it = changed_vals.begin(); it != changed_vals.end(); ++it ){

+          Trace("fmc-interval-model") << "Entry #" << it->first << " changed : ";

+          for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){

+            Trace("fmc-interval-model") << it2->first << " -> " << it2->second << ", ";

+          }

+          Trace("fmc-interval-model") << std::endl;

+        }

+      }

+

+

       Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;

       fm->d_models[op]->simplify( this, fm );

       Trace("fmc-model-simplify") << "After simplification : " << std::endl;

@@ -525,6 +558,11 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
   }

   else if(fm->isStar(n) && dispStar) {

     Trace(tr) << "*";

+  }

+  else if(fm->isInterval(n)) {

+    debugPrint(tr, n[0], dispStar );

+    Trace(tr) << "...";

+    debugPrint(tr, n[1], dispStar );

   }else{

     TypeNode tn = n.getType();

     if( d_rep_ids.find(tn)!=d_rep_ids.end() ){

@@ -534,17 +572,15 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
         Trace(tr) << n;

       }

     }else{

-        Trace(tr) << n;

+      Trace(tr) << n;

     }

   }

 }

 

 

-bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) {

+bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {

   Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;

-  if (!options::fmfModelBasedInst()) {

-    return false;

-  }else{

+  if( optUseModel() ){

     FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();

     if (effort==0) {

       //register the quantifier

@@ -602,8 +638,9 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
             for( unsigned j=0; j<inst.size(); j++) {

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

             }

+            d_triedLemmas++;

             if( d_qe->addInstantiation( f, m ) ){

-              lemmas++;

+              d_addedLemmas++;

             }else{

               //this can happen if evaluation is unknown

               //might try it next effort level

@@ -627,29 +664,27 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
           //get witness for d_star_insts[f][i]

           int j = d_star_insts[f][i];

           if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){

-            int lem = exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j );

-            if( lem==-1 ){

+            if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){

               //something went wrong, resort to exhaustive instantiation

               return false;

-            }else{

-              lemmas += lem;

             }

           }

         }

       }

     }

     return true;

+  }else{

+    return false;

   }

 }

 

-int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {

-  int addedLemmas = 0;

+bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {

   RepSetIterator riter( d_qe, &(fm->d_rep_set) );

   Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";

   debugPrintCond("fmc-exh", c, true);

   Trace("fmc-exh")<< std::endl;

   if( riter.setQuantifier( f ) ){

-    std::vector< RepDomain > dom;

+    //set the domains based on the entry

     for (unsigned i=0; i<c.getNumChildren(); i++) {

       if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {

         TypeNode tn = c[i].getType();

@@ -661,11 +696,11 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Nod
               riter.d_domain[i].clear();

               riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);

             }else{

-              return -1;

+              return false;

             }

           }

         }else{

-          return -1;

+          return false;

         }

       }

     }

@@ -684,22 +719,33 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Nod
       int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);

       Trace("fmc-exh-debug") << ", index = " << ev_index;

       Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];

+      bool successAdd = false;

       if (ev!=d_true) {

         InstMatch m;

         for( int i=0; i<riter.getNumTerms(); i++ ){

           m.set( d_qe, f, i, riter.getTerm( i ) );

         }

         Trace("fmc-exh-debug") << ", add!";

+        d_triedLemmas++;

         //add as instantiation

         if( d_qe->addInstantiation( f, m ) ){

-          addedLemmas++;

+          Trace("fmc-exh-debug")  << " ...success.";

+          d_addedLemmas++;

+          successAdd = true;

         }

       }

       Trace("fmc-exh-debug") << std::endl;

-      riter.increment();

+      int index = riter.increment();

+      Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;

+      if (index>=0 && successAdd && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {

+        Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;

+        riter.increment2( index-1 );

+      }

     }

+    return true;

+  }else{

+    return false;

   }

-  return addedLemmas;

 }

 

 void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {

@@ -1127,40 +1173,76 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const
 }

 

 

+bool FullModelChecker::useSimpleModels() {

+  return options::fmfFullModelCheckSimple();

+}

 

-void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,

-                                   std::vector< Node > & conds,

-                                   std::vector< Node > & values,

-                                   std::vector< Node > & entry_conds ) {

-  std::vector< Node > children;

-  std::vector< Node > entry_children;

-  children.push_back(op);

-  entry_children.push_back(op);

-  bool hasNonStar = false;

-  for( unsigned i=0; i<c.getNumChildren(); i++) {

-    Node ri = fm->getUsedRepresentative( c[i]);

-    children.push_back(ri);

-    if (fm->isModelBasisTerm(ri)) {

-      ri = fm->getStar( ri.getType() );

+void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,

+                                          std::map< int, std::map< int, Node > >& changed_vals ) {

+  if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){

+    makeIntervalModel2( fm, op, indices, 0, changed_vals );

+  }else{

+    TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();

+    if( tn.isInteger() ){

+      makeIntervalModel(fm,op,indices,index+1, changed_vals );

     }else{

-      hasNonStar = true;

+      std::map< Node, std::vector< int > > new_indices;

+      for( unsigned i=0; i<indices.size(); i++ ){

+        Node v = fm->d_models[op]->d_cond[indices[i]][index];

+        new_indices[v].push_back( i );

+      }

+

+      for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){

+        makeIntervalModel( fm, op, it->second, index+1, changed_vals );

+      }

     }

-    entry_children.push_back(ri);

-  }

-  Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );

-  Node nv = fm->getUsedRepresentative( v);

-  Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );

-  if( std::find(conds.begin(), conds.end(), n )==conds.end() ){

-    Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;

-    conds.push_back(n);

-    values.push_back(nv);

-    entry_conds.push_back(en);

-  }

-  else {

-    Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;

   }

 }

 

-bool FullModelChecker::useSimpleModels() {

-  return options::fmfFullModelCheckSimple();

-}

+void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,

+                                          std::map< int, std::map< int, Node > >& changed_vals ) {

+  if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){

+    TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();

+    if( tn.isInteger() ){

+      std::map< Node, std::vector< int > > new_indices;

+      for( unsigned i=0; i<indices.size(); i++ ){

+        Node v = fm->d_models[op]->d_cond[indices[i]][index];

+        new_indices[v].push_back( i );

+      }

+

+      std::vector< Node > values;

+      for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){

+        makeIntervalModel2( fm, op, it->second, index+1, changed_vals );

+        if( !fm->isStar(it->first) ){

+          values.push_back( it->first );

+        }

+      }

+

+      if( tn.isInteger() ){

+        //sort values by size

+        ConstRationalSort crs;

+        std::vector< int > sindices;

+        for( unsigned i=0; i<values.size(); i++ ){

+          sindices.push_back( (int)i );

+          crs.d_terms.push_back( values[i] );

+        }

+        std::sort( sindices.begin(), sindices.end(), crs );

+

+        Node ub = fm->getStar( tn );

+        for( int i=(int)(sindices.size()-1); i>=0; i-- ){

+          Node lb = fm->getStar( tn );

+          if( i>0 ){

+            lb = values[sindices[i]];

+          }

+          Node interval = fm->getInterval( lb, ub );

+          for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){

+            changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;

+          }

+          ub = lb;

+        }

+      }

+    }else{

+      makeIntervalModel2( fm, op, indices, index+1, changed_vals );

+    }

+  }

+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 3d9a82b9e..45110b2b7 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -40,9 +40,6 @@ public:
   void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );

 

   bool isCovered(FirstOrderModelFmc * m, Node c, int index);

-

-  //void exhaustiveSimplify( FirstOrderModelFmc * m, Node c, int index, std::vector< int >& indices,

-  //                         std::map< int, std::vector< int > >& star_replace );

   void collectIndices(Node c, int index, std::vector< int >& indices );

   bool isComplete(FirstOrderModelFmc * m, Node c, int index);

 };

@@ -95,12 +92,12 @@ protected:
   std::map<Node, std::map< Node, int > > d_quant_var_id;

   std::map<Node, std::vector< int > > d_star_insts;

   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);

-  int exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);

+  bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);

 protected:

-  void addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,

-                 std::vector< Node > & conds,

-                 std::vector< Node > & values,

-                 std::vector< Node > & entry_conds );

+  void makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,

+                          std::map< int, std::map< int, Node > >& changed_vals );

+  void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,

+                          std::map< int, std::map< int, Node > >& changed_vals );

 private:

   void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );

 

@@ -138,7 +135,7 @@ public:
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);

   void debugPrint(const char * tr, Node n, bool dispStar = false);

 

-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );

+  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );

 

   Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );

 

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index fbf3ce59c..b1851cfa4 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -36,7 +36,6 @@ using namespace CVC4::theory::quantifiers;
 QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) :
 TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){
   d_considerAxioms = true;
-  d_addedLemmas = 0;
 }
 
 bool QModelBuilder::isQuantifierActive( Node f ) {
@@ -128,7 +127,6 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
     debugModel( fm );
   }else{
     d_curr_model = fm;
-    d_addedLemmas = 0;
     d_didInstGen = false;
     //reset the internal information
     reset( fm );
@@ -340,15 +338,23 @@ bool QModelBuilderIG::optOneQuantPerRoundInstGen(){
 }
 
 QModelBuilderIG::Statistics::Statistics():
-  d_num_quants_init("QModelBuilder::Number_Quantifiers", 0),
-  d_num_partial_quants_init("QModelBuilder::Number_Partial_Quantifiers", 0),
-  d_init_inst_gen_lemmas("QModelBuilder::Initialize_Inst_Gen_Lemmas", 0 ),
-  d_inst_gen_lemmas("QModelBuilder::Inst_Gen_Lemmas", 0 )
+  d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
+  d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
+  d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
+  d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
+  d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
+  d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
+  d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
+  d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
 {
   StatisticsRegistry::registerStat(&d_num_quants_init);
   StatisticsRegistry::registerStat(&d_num_partial_quants_init);
   StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas);
   StatisticsRegistry::registerStat(&d_inst_gen_lemmas);
+  StatisticsRegistry::registerStat(&d_eval_formulas);
+  StatisticsRegistry::registerStat(&d_eval_uf_terms);
+  StatisticsRegistry::registerStat(&d_eval_lits);
+  StatisticsRegistry::registerStat(&d_eval_lits_unknown);
 }
 
 QModelBuilderIG::Statistics::~Statistics(){
@@ -356,6 +362,10 @@ QModelBuilderIG::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_num_partial_quants_init);
   StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas);
   StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas);
+  StatisticsRegistry::unregisterStat(&d_eval_formulas);
+  StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
+  StatisticsRegistry::unregisterStat(&d_eval_lits);
+  StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
 }
 
 bool QModelBuilderIG::isQuantifierActive( Node f ){
@@ -371,6 +381,86 @@ 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();
+      Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+      fmig->resetEvaluate();
+      Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+      while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+        d_triedLemmas++;
+        for( int i=0; i<(int)riter.d_index.size(); i++ ){
+          Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
+        }
+        int eval = 0;
+        int depIndex;
+        //see if instantiation is already true in current model
+        Debug("fmf-model-eval") << "Evaluating ";
+        riter.debugPrintSmall("fmf-model-eval");
+        Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+        //if evaluate(...)==1, then the instantiation is already true in the model
+        //  depIndex is the index of the least significant variable that this evaluation relies upon
+        depIndex = riter.getNumTerms()-1;
+        eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
+        if( eval==1 ){
+          Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
+        }else{
+          Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+        }
+        if( eval==1 ){
+          //instantiation is already true -> skip
+          riter.increment2( depIndex );
+        }else{
+          //instantiation was not shown to be true, construct the match
+          InstMatch m;
+          for( int i=0; i<riter.getNumTerms(); i++ ){
+            m.set( d_qe, f, riter.d_index_order[i], riter.getTerm( i ) );
+          }
+          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+          //add as instantiation
+          if( d_qe->addInstantiation( f, m ) ){
+            d_addedLemmas++;
+            //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+            if( eval==-1 ){
+              riter.increment2( depIndex );
+            }else{
+              riter.increment();
+            }
+          }else{
+            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+            riter.increment();
+          }
+        }
+      }
+      //print debugging information
+      if( fmig ){
+        d_statistics.d_eval_formulas += fmig->d_eval_formulas;
+        d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
+        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") << "   Inst Tried: " << d_triedLemmas << std::endl;
+      Trace("inst-fmf-ei") << "   Inst Added: " << d_addedLemmas << std::endl;
+      if( d_addedLemmas>1000 ){
+        Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+        Trace("model-engine-warn") << "   Inst Tried: " << d_triedLemmas << std::endl;
+        Trace("model-engine-warn") << "   Inst Added: " << d_addedLemmas << std::endl;
+        Trace("model-engine-warn") << std::endl;
+      }
+    }
+     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+    d_incomplete_check = riter.d_incomplete;
+    return true;
+  }else{
+    return false;
+  }
+}
+
 
 
 void QModelBuilderDefault::reset( FirstOrderModel* fm ){
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 708688c60..0d7c146ba 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -39,13 +39,16 @@ public:
   // is quantifier active?
   virtual bool isQuantifierActive( Node f );
   //do exhaustive instantiation
-  virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) { return false; }
+  virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
   //whether to construct model
   virtual bool optUseModel();
-  /** number of lemmas generated while building model */
-  int d_addedLemmas;
   //consider axioms
   bool d_considerAxioms;
+  /** number of lemmas generated while building model */
+  //is the exhaustive instantiation incomplete?
+  bool d_incomplete_check;
+  int d_addedLemmas;
+  int d_triedLemmas;
   /** exist instantiation ? */
   virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
   //debug model
@@ -133,6 +136,10 @@ public:
     IntStat d_num_partial_quants_init;
     IntStat d_init_inst_gen_lemmas;
     IntStat d_inst_gen_lemmas;
+    IntStat d_eval_formulas;
+    IntStat d_eval_uf_terms;
+    IntStat d_eval_lits;
+    IntStat d_eval_lits_unknown;
     Statistics();
     ~Statistics();
   };
@@ -147,6 +154,8 @@ public:
   bool didInstGen() { return d_didInstGen; }
   // is quantifier active?
   bool isQuantifierActive( Node f );
+  //do exhaustive instantiation
+  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
 
   //temporary stats
   int d_numQuantSat;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 0f756dcc0..c0fe23b94 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -22,8 +22,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 
-#define EVAL_FAIL_SKIP_MULTIPLE
-
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -67,6 +65,7 @@ void ModelEngine::check( Theory::Effort e ){
         //initialize the model
         Trace("model-engine-debug") << "Build model..." << std::endl;
         d_builder->d_considerAxioms = effort>=1;
+        d_builder->d_addedLemmas = 0;
         d_builder->buildModel( fm, false );
         addedLemmas += (int)d_builder->d_addedLemmas;
         //if builder has lemmas, add and return
@@ -127,28 +126,12 @@ void ModelEngine::assertNode( Node f ){
 
 }
 
-bool ModelEngine::optOneInstPerQuantRound(){
-  return options::fmfOneInstPerRound();
-}
-
-bool ModelEngine::optUseRelevantDomain(){
-  return options::fmfRelevantDomain();
-}
-
 bool ModelEngine::optOneQuantPerRound(){
   return options::fmfOneQuantPerRound();
 }
 
-bool ModelEngine::optExhInstEvalSkipMultiple(){
-#ifdef EVAL_FAIL_SKIP_MULTIPLE
-  return true;
-#else
-  return false;
-#endif
-}
 
 int ModelEngine::checkModel(){
-  int addedLemmas = 0;
   FirstOrderModel* fm = d_quantEngine->getModel();
   //for debugging
   if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
@@ -168,39 +151,41 @@ int ModelEngine::checkModel(){
       }
     }
   }
-  //compute the relevant domain if necessary
-  //if( optUseRelevantDomain() ){
-  //}
+  //relevant domain?
+
   d_triedLemmas = 0;
-  d_testLemmas = 0;
-  d_relevantLemmas = 0;
+  d_addedLemmas = 0;
   d_totalLemmas = 0;
+  //for statistics
+  for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+    Node f = fm->getAssertedQuantifier( i );
+    int totalInst = 1;
+    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+      TypeNode tn = f[0][i].getType();
+      if( fm->d_rep_set.hasType( tn ) ){
+        totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+      }
+    }
+    d_totalLemmas += totalInst;
+  }
+
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1;
   for( int e=0; e<e_max; e++) {
-    if (addedLemmas==0) {
+    if (d_addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node f = fm->getAssertedQuantifier( i );
-        //keep track of total instantiations for statistics
-        int totalInst = 1;
-        for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-          TypeNode tn = f[0][i].getType();
-          if( fm->d_rep_set.hasType( tn ) ){
-            totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
-          }
-        }
-        d_totalLemmas += totalInst;
         //determine if we should check this quantifier
         if( d_builder->isQuantifierActive( f ) ){
-          addedLemmas += exhaustiveInstantiate( f, e );
+          exhaustiveInstantiate( f, e );
           if( Trace.isOn("model-engine-warn") ){
-            if( addedLemmas>10000 ){
+            if( d_addedLemmas>10000 ){
               Debug("fmf-exit") << std::endl;
               debugPrint("fmf-exit");
               exit( 0 );
             }
           }
-          if( optOneQuantPerRound() && addedLemmas>0 ){
+          if( optOneQuantPerRound() && d_addedLemmas>0 ){
             break;
           }
         }
@@ -210,17 +195,23 @@ int ModelEngine::checkModel(){
   //print debug information
   if( Trace.isOn("model-engine") ){
     Trace("model-engine") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
-    Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
-    Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+    Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
+    Trace("model-engine") << d_totalLemmas << std::endl;
   }
-  d_statistics.d_exh_inst_lemmas += addedLemmas;
-  return addedLemmas;
+  d_statistics.d_exh_inst_lemmas += d_addedLemmas;
+  return d_addedLemmas;
 }
 
-int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
-  int addedLemmas = 0;
+void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   //first check if the builder can do the exhaustive instantiation
-  if( !d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort, addedLemmas ) ){
+  d_builder->d_triedLemmas = 0;
+  d_builder->d_addedLemmas = 0;
+  d_builder->d_incomplete_check = false;
+  if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
+    d_triedLemmas += d_builder->d_triedLemmas;
+    d_addedLemmas += d_builder->d_addedLemmas;
+    d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
+  }else{
     Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
@@ -230,97 +221,31 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      FirstOrderModelIG * fmig = NULL;
-      if( !options::fmfFullModelCheck() ){
-        fmig = (FirstOrderModelIG*)d_quantEngine->getModel();
-        Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
-        fmig->resetEvaluate();
-      }
       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
-      int tests = 0;
       int triedLemmas = 0;
-      while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
-        for( int i=0; i<(int)riter.d_index.size(); i++ ){
-          Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
-        }
-        d_testLemmas++;
-        int eval = 0;
-        int depIndex;
-        if( d_builder->optUseModel() && fmig ){
-          //see if instantiation is already true in current model
-          Debug("fmf-model-eval") << "Evaluating ";
-          riter.debugPrintSmall("fmf-model-eval");
-          Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
-          tests++;
-          //if evaluate(...)==1, then the instantiation is already true in the model
-          //  depIndex is the index of the least significant variable that this evaluation relies upon
-          depIndex = riter.getNumTerms()-1;
-          eval = fmig->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
-          if( eval==1 ){
-            Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
-          }else{
-            Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
-          }
+      int addedLemmas = 0;
+      while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+        //instantiation was not shown to be true, construct the match
+        InstMatch m;
+        for( int i=0; i<riter.getNumTerms(); i++ ){
+          m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
         }
-        if( eval==1 ){
-          //instantiation is already true -> skip
-          riter.increment2( depIndex );
+        Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+        triedLemmas++;
+        //add as instantiation
+        if( d_quantEngine->addInstantiation( f, m ) ){
+          addedLemmas++;
         }else{
-          //instantiation was not shown to be true, construct the match
-          InstMatch m;
-          for( int i=0; i<riter.getNumTerms(); i++ ){
-            m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
-          }
-          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
-          triedLemmas++;
-          d_triedLemmas++;
-          //add as instantiation
-          if( d_quantEngine->addInstantiation( f, m ) ){
-            addedLemmas++;
-            //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
-            if( eval==-1 && optExhInstEvalSkipMultiple() ){
-              riter.increment2( depIndex );
-            }else{
-              riter.increment();
-            }
-          }else{
-            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
-            riter.increment();
-          }
+          Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
         }
+        riter.increment();
       }
-      //print debugging information
-      if( fmig ){
-        d_statistics.d_eval_formulas += fmig->d_eval_formulas;
-        d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
-        d_statistics.d_eval_lits += fmig->d_eval_lits;
-        d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
-      }
-      int relevantInst = 1;
-      for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-        relevantInst = relevantInst * (int)riter.d_domain[i].size();
-      }
-      d_relevantLemmas += relevantInst;
-      Trace("inst-fmf-ei") << "Finished: " << std::endl;
-      //Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
-      Trace("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
-      Trace("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
-      Trace("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
-      Trace("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
-      if( addedLemmas>1000 ){
-        Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
-        //Trace("model-engine-warn") << "   Inst Total: " << totalInst << std::endl;
-        Trace("model-engine-warn") << "   Inst Relevant: " << relevantInst << std::endl;
-        Trace("model-engine-warn") << "   Inst Tried: " << triedLemmas << std::endl;
-        Trace("model-engine-warn") << "   Inst Added: " << addedLemmas << std::endl;
-        Trace("model-engine-warn") << "   # Tests: " << tests << std::endl;
-        Trace("model-engine-warn") << std::endl;
-      }
+      d_addedLemmas += addedLemmas;
+      d_triedLemmas += triedLemmas;
     }
-     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+    //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
     d_incomplete_check = d_incomplete_check || riter.d_incomplete;
   }
-  return addedLemmas;
 }
 
 void ModelEngine::debugPrint( const char* c ){
@@ -340,26 +265,14 @@ void ModelEngine::debugPrint( const char* c ){
 
 ModelEngine::Statistics::Statistics():
   d_inst_rounds("ModelEngine::Inst_Rounds", 0),
-  d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
-  d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
-  d_eval_lits("ModelEngine::Eval_Lits", 0 ),
-  d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ),
   d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 )
 {
   StatisticsRegistry::registerStat(&d_inst_rounds);
-  StatisticsRegistry::registerStat(&d_eval_formulas);
-  StatisticsRegistry::registerStat(&d_eval_uf_terms);
-  StatisticsRegistry::registerStat(&d_eval_lits);
-  StatisticsRegistry::registerStat(&d_eval_lits_unknown);
   StatisticsRegistry::registerStat(&d_exh_inst_lemmas);
 }
 
 ModelEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_inst_rounds);
-  StatisticsRegistry::unregisterStat(&d_eval_formulas);
-  StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
-  StatisticsRegistry::unregisterStat(&d_eval_lits);
-  StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
   StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
 }
 
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 0f0ab4fe7..20c677e9c 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -33,25 +33,21 @@ private:
   /** builder class */
   QModelBuilder* d_builder;
 private:    //analysis of current model:
-  //is the exhaustive instantiation incomplete?
-  bool d_incomplete_check;
 private:
   //options
-  bool optOneInstPerQuantRound();
-  bool optUseRelevantDomain();
   bool optOneQuantPerRound();
-  bool optExhInstEvalSkipMultiple();
 private:
   //check model
   int checkModel();
-  //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
-  int exhaustiveInstantiate( Node f, int effort = 0 );
+  //exhaustively instantiate quantifier (possibly using mbqi)
+  void exhaustiveInstantiate( Node f, int effort = 0 );
 private:
   //temporary statistics
+  //is the exhaustive instantiation incomplete?
+  bool d_incomplete_check;
+  int d_addedLemmas;
   int d_triedLemmas;
-  int d_testLemmas;
   int d_totalLemmas;
-  int d_relevantLemmas;
 public:
   ModelEngine( context::Context* c, QuantifiersEngine* qe );
   ~ModelEngine(){}
@@ -68,10 +64,6 @@ public:
   class Statistics {
   public:
     IntStat d_inst_rounds;
-    IntStat d_eval_formulas;
-    IntStat d_eval_uf_terms;
-    IntStat d_eval_lits;
-    IntStat d_eval_lits_unknown;
     IntStat d_exh_inst_lemmas;
     Statistics();
     ~Statistics();
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 0f9d0f295..1e6f04162 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -99,6 +99,8 @@ option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
 option fmfFmcCoverSimplify --fmf-fmc-cover-simplify bool :default false
  apply covering simplification technique to fmc models
+option fmfFmcInterval --fmf-fmc-interval bool :default false
+ construct interval models for fmc models
 
 option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
  only add one instantiation per quantifier per round for fmf
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index fb5964554..1688479f3 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -68,6 +68,10 @@ typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarCompute
 struct QRewriteRuleAttributeId {};
 typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
 
+//for bounded integers
+struct BoundIntLitAttributeId {};
+typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
+
 
 class QuantifiersEngine;
 
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index f2cb22b85..180c4bbcf 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -276,7 +276,7 @@ bool RepSetIterator::resetIndex( int i, bool initial ) {
   return true;
 }
 
-void RepSetIterator::increment2( int counter ){
+int RepSetIterator::increment2( int counter ){
   Assert( !isFinished() );
 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
   counter = (int)d_index.size()-1;
@@ -305,14 +305,17 @@ void RepSetIterator::increment2( int counter ){
     }
     if( emptyDomain ){
       Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl;
-      increment();
+      return increment();
     }
   }
+  return counter;
 }
 
-void RepSetIterator::increment(){
+int RepSetIterator::increment(){
   if( !isFinished() ){
-    increment2( (int)d_index.size()-1 );
+    return increment2( (int)d_index.size()-1 );
+  }else{
+    return -1;
   }
 }
 
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index e703ee467..672f33b54 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -107,12 +107,10 @@ public:
 public:
   /** set index order */
   void setIndexOrder( std::vector< int >& indexOrder );
-  /** set domain */
-  //void setDomain( std::vector< RepDomain >& domain );
   /** increment the iterator at index=counter */
-  void increment2( int counter );
+  int increment2( int counter );
   /** increment the iterator */
-  void increment();
+  int increment();
   /** is the iterator finished? */
   bool isFinished();
   /** get the i_th term we are considering */
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index baa40463f..71a342f76 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1001,14 +1001,14 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     if( applyTotality( d_aloc_cardinality ) ){
       //must generate new cardinality lemma term
       Node var;
-      //if( d_aloc_cardinality==1 ){
+      if( d_aloc_cardinality==1 && !options::ufssTotalitySymBreak() ){
         //get arbitrary ground term
-        //var = d_cardinality_term;
-      //}else{
+        var = d_cardinality_term;
+      }else{
         std::stringstream ss;
         ss << "_c_" << d_aloc_cardinality;
         var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
-      //}
+      }
       d_totality_terms[0].push_back( var );
       Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl;
       //must be distinct from all other cardinality terms