From d8de492163b90974709a16918cb615515a536afc Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 25 Jun 2013 12:18:05 -0500
Subject: Refactoring of model engine to separate individual implementations of
 model builder.  Begin work on interval models for integers.  Other minor
 cleanup.

---
 src/theory/quantifiers/bounded_integers.cpp  |  31 +--
 src/theory/quantifiers/first_order_model.cpp |  16 ++
 src/theory/quantifiers/first_order_model.h   |   3 +
 src/theory/quantifiers/full_model_check.cpp  | 350 +++++++++++++++++----------
 src/theory/quantifiers/full_model_check.h    |  15 +-
 src/theory/quantifiers/model_builder.cpp     | 102 +++++++-
 src/theory/quantifiers/model_builder.h       |  15 +-
 src/theory/quantifiers/model_engine.cpp      | 187 ++++----------
 src/theory/quantifiers/model_engine.h        |  18 +-
 src/theory/quantifiers/options               |   2 +
 src/theory/quantifiers/term_database.h       |   4 +
 src/theory/rep_set.cpp                       |  11 +-
 src/theory/rep_set.h                         |   6 +-
 src/theory/uf/theory_uf_strong_solver.cpp    |   8 +-
 14 files changed, 430 insertions(+), 338 deletions(-)

(limited to 'src/theory')

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
-- 
cgit v1.2.3