From 0a6fa189e4e2dc2c47f4050df0aad4a6f3d39b4b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Jun 2013 14:40:05 -0500
Subject: [PATCH] Add support for interval models in bounded integers MBQI (in
 progress).

---
 src/theory/quantifiers/bounded_integers.cpp  |  33 +-
 src/theory/quantifiers/bounded_integers.h    |   8 +-
 src/theory/quantifiers/first_order_model.cpp |  17 +-
 src/theory/quantifiers/first_order_model.h   |   1 +
 src/theory/quantifiers/full_model_check.cpp  | 326 +++++++++++++------
 src/theory/quantifiers/full_model_check.h    |   2 +-
 src/theory/quantifiers/term_database.cpp     |  14 +-
 src/theory/rep_set.cpp                       |  46 ++-
 src/theory/rep_set.h                         |   6 +-
 9 files changed, 312 insertions(+), 141 deletions(-)

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 37bf6436b..d893a9ff2 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -135,7 +135,9 @@ bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
   return false;
 }
 
-void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
+void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,
+                                      std::map< int, std::map< Node, Node > >& bound_lit_map,
+                                      std::map< int, std::map< Node, bool > >& bound_lit_pol_map ) {
   if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
     std::map< Node, Node > msum;
     if (QuantArith::getMonomialSumLit( lit, msum )){
@@ -176,7 +178,10 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
             if( !isBound( f, bv ) ){
               if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {
                 Trace("bound-int-debug") << "The bound is relevant." << std::endl;
-                d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);
+                int loru = n1.getKind()==BOUND_VARIABLE ? 0 : 1;
+                d_bounds[loru][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);
+                bound_lit_map[loru][bv] = lit;
+                bound_lit_pol_map[loru][bv] = pol;
               }
             }
           }
@@ -189,16 +194,18 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
   }
 }
 
-void BoundedIntegers::process( Node f, Node n, bool pol ){
+void BoundedIntegers::process( Node f, Node n, bool pol,
+                               std::map< int, std::map< Node, Node > >& bound_lit_map,
+                               std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){
   if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){
     for( unsigned i=0; i<n.getNumChildren(); i++) {
       bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol;
-      process( f, n[i], newPol );
+      process( f, n[i], newPol, bound_lit_map, bound_lit_pol_map );
     }
   }else if( n.getKind()==NOT ){
-    process( f, n[0], !pol );
+    process( f, n[0], !pol, bound_lit_map, bound_lit_pol_map );
   }else {
-    processLiteral( f, n, pol );
+    processLiteral( f, n, pol, bound_lit_map, bound_lit_pol_map );
   }
 }
 
@@ -232,10 +239,10 @@ void BoundedIntegers::registerQuantifier( Node f ) {
   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;
+      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 );
+      process( f, f[1], true, bound_lit_map, bound_lit_pol_map );
       for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
         Node v = it->first;
         if( !isBound(f,v) ){
@@ -243,6 +250,14 @@ void BoundedIntegers::registerQuantifier( Node f ) {
             d_set[f].push_back(v);
             d_set_nums[f].push_back(numMap[v]);
             success = true;
+            //set Attributes on literals
+            for( unsigned b=0; b<2; b++ ){
+              Assert( bound_lit_map[b].find( v )!=bound_lit_map[b].end() );
+              Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() );
+              BoundIntLitAttribute bila;
+              bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 );
+            }
+            Trace("bound-int") << "Variable " << v << " is bound because of literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
           }
         }
       }
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index f40e2180c..96d2a3d20 100755
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -45,8 +45,12 @@ private:
   std::map< Node, std::map< Node, Node > > d_range;
   std::map< Node, std::map< Node, Node > > d_nground_range;
   void hasFreeVar( Node f, Node n );
-  void process( Node f, Node n, bool pol );
-  void processLiteral( Node f, Node lit, bool pol );
+  void process( Node f, Node n, bool pol,
+                std::map< int, std::map< Node, Node > >& bound_lit_map,
+                std::map< int, std::map< Node, bool > >& bound_lit_pol_map );
+  void processLiteral( Node f, Node lit, bool pol,
+                       std::map< int, std::map< Node, Node > >& bound_lit_map,
+                       std::map< int, std::map< Node, bool > >& bound_lit_pol_map  );
   std::vector< Node > d_bound_quants;
 private:
   class RangeModel {
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index ad433edf5..60d62391b 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -601,6 +601,14 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) {
   return d_type_star[tn];
 }
 
+Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
+  Node st = getStar(tn);
+  if( options::fmfFmcInterval() && tn.isInteger() ){
+    st = getInterval( st, st );
+  }
+  return st;
+}
+
 bool FirstOrderModelFmc::isModelBasisTerm(Node n) {
   return n==getModelBasisTerm(n.getType());
 }
@@ -630,7 +638,14 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       Node cond = d_models[op]->d_cond[i];
       std::vector< Node > children;
       for( unsigned j=0; j<cond.getNumChildren(); j++) {
-        if (!isStar(cond[j])){
+        if (isInterval(cond[j])){
+          if( !isStar(cond[j][0]) ){
+            children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) );
+          }
+          if( !isStar(cond[j][1]) ){
+            children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
+          }
+        }else if (!isStar(cond[j])){
           Node c = getUsedRepresentative( cond[j] );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
         }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index d79171f68..14e9441b4 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -149,6 +149,7 @@ public:
 
   bool isStar(Node n);
   Node getStar(TypeNode tn);
+  Node getStarElement(TypeNode tn);
   bool isModelBasisTerm(Node n);
   Node getModelBasisTerm(TypeNode tn);
   Node getSomeDomainElement(TypeNode tn);
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 7f30a045e..ed5dea679 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -59,22 +59,24 @@ 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( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){
+      //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;
+          if( complete ){
+            return true;
+          }
         }
       }
     }
@@ -88,15 +90,41 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>
     return d_data;
   }else{
     int minIndex = -1;
-    Node st = m->getStar(inst[index].getType());
-    if(d_child.find(st)!=d_child.end()) {
-      minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);
-    }
-    Node cc = inst[index];
-    if( cc!=st && d_child.find( cc )!=d_child.end() ){
-      int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);
-      if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
-        minIndex = gindex;
+    if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){
+      for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
+        if( !m->isInterval( it->first ) ){
+          std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
+          exit( 11 );
+        }
+        //check if it is in the range
+        bool inRange = true;
+        for( unsigned b=0; b<2; b++ ){
+          if( !m->isStar( it->first[b] ) ){
+            if( ( b==0 && it->first[b].getConst<Rational>() > inst[index].getConst<Rational>() ) ||
+                ( b==1 && it->first[b].getConst<Rational>() <= inst[index].getConst<Rational>() ) ){
+              inRange = false;
+              break;
+            }
+          }
+        }
+        if( inRange ){
+          int gindex = it->second.getGeneralizationIndex(m, inst, index+1);
+          if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
+            minIndex = gindex;
+          }
+        }
+      }
+    }else{
+      Node st = m->getStar(inst[index].getType());
+      if(d_child.find(st)!=d_child.end()) {
+        minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);
+      }
+      Node cc = inst[index];
+      if( cc!=st && d_child.find( cc )!=d_child.end() ){
+        int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);
+        if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
+          minIndex = gindex;
+        }
       }
     }
     return minIndex;
@@ -143,39 +171,6 @@ void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & c
   }
 }
 
-
-bool EntryTrie::isCovered(FirstOrderModelFmc * m, Node c, int index) {
-  if (index==(int)c.getNumChildren()) {
-    return false;
-  }else{
-    TypeNode tn = c[index].getType();
-    Node st = m->getStar(tn);
-    if( 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.isComplete(m, c, index+1) ){
-              complete = false;
-              break;
-            }
-          }
-        }
-        if( complete ){
-          return true;
-        }
-      }
-    }
-    if( d_child.find(c[index])!=d_child.end() ){
-      return d_child[c[index]].isCovered(m, c, index+1);
-    }else{
-      return false;
-    }
-  }
-}
-
 void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) {
   if (index==(int)c.getNumChildren()) {
     if( d_data!=-1 ){
@@ -209,12 +204,6 @@ 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;
-  //  }
-  //}
   int newIndex = (int)d_cond.size();
   if (!d_has_simplified) {
     std::vector<int> compat;
@@ -247,6 +236,7 @@ Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
   if (gindex!=-1) {
     return d_value[gindex];
   }else{
+    Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl;
     return Node::null();
   }
 }
@@ -280,7 +270,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
     bool last_all_stars = true;
     Node cc = d_cond[d_cond.size()-1];
     for( unsigned i=0; i<cc.getNumChildren(); i++ ){
-      if( !m->isStar(cc[i]) ){
+      if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){
         last_all_stars = false;
         break;
       }
@@ -475,10 +465,12 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         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;
+          if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){
+            if (fm->isModelBasisTerm(ri) ) {
+              ri = fm->getStar( ri.getType() );
+            }else{
+              hasNonStar = true;
+            }
           }
           entry_children.push_back(ri);
         }
@@ -510,8 +502,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       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;
@@ -523,21 +514,45 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         }
         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 << ", ";
+
+        std::vector< Node > conds;
+        std::vector< Node > values;
+        for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){
+          if( changed_vals.find(i)==changed_vals.end() ){
+            conds.push_back( fm->d_models[op]->d_cond[i] );
+          }else{
+            std::vector< Node > children;
+            children.push_back( op );
+            for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){
+              if( changed_vals[i].find(j)==changed_vals[i].end() ){
+                children.push_back( fm->d_models[op]->d_cond[i][j] );
+              }else{
+                children.push_back( changed_vals[i][j] );
+              }
+            }
+            Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+            conds.push_back( nc );
+            Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";
+            debugPrintCond("fmc-interval-model", nc, true );
+            Trace("fmc-interval-model") << std::endl;
           }
-          Trace("fmc-interval-model") << std::endl;
+          values.push_back( fm->d_models[op]->d_value[i] );
+        }
+        fm->d_models[op]->reset();
+        for( unsigned i=0; i<conds.size(); i++ ){
+          fm->d_models[op]->addEntry(fm, conds[i], values[i] );
         }
       }
 
+      Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
+      fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
+      Trace("fmc-model-simplify") << 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;
-      fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
-      Trace("fmc-model-simplify") << std::endl;
+
+      fm->d_models[op]->debugPrint("fmc-model", op, this);
+      Trace("fmc-model") << std::endl;
     }
   }
 }
@@ -600,7 +615,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
       Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
       d_quant_models[f].debugPrint("fmc", Node::null(), this);
       Trace("fmc") << std::endl;
-      //consider all entries going to false
+
+      //consider all entries going to non-true
       for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
         if( d_quant_models[f].d_value[i]!=d_true) {
           Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
@@ -610,6 +626,21 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
             if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
               hasStar = true;
               inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+            }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){
+              hasStar = true;
+              //if interval, find a sample point
+              if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){
+                if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){
+                  inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType()));
+                }else{
+                  Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],
+                                                              NodeManager::currentNM()->mkConst( Rational(1) ) );
+                  nn = Rewriter::rewrite( nn );
+                  inst.push_back( nn );
+                }
+              }else{
+                inst.push_back(d_quant_models[f].d_cond[i][j][0]);
+              }
             }else{
               inst.push_back(d_quant_models[f].d_cond[i][j]);
             }
@@ -683,13 +714,24 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
   Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
   debugPrintCond("fmc-exh", c, true);
   Trace("fmc-exh")<< std::endl;
+  //set the bounds on the iterator based on intervals
+  for( unsigned i=0; i<c.getNumChildren(); i++ ){
+    if( fm->isInterval(c[i]) ){
+      for( unsigned b=0; b<2; b++ ){
+        if( !fm->isStar(c[i][b]) ){
+          riter.d_bounds[b][i] = c[i][b];
+        }
+      }
+    }
+  }
+  //initialize
   if( riter.setQuantifier( f ) ){
     //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();
         if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
-          if( fm->isStar(c[i]) ){
+          if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){
             //add the full range
           }else{
             if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
@@ -704,8 +746,10 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         }
       }
     }
+    int addedLemmas = 0;
     //now do full iteration
     while( !riter.isFinished() ){
+      d_triedLemmas++;
       Trace("fmc-exh-debug") << "Inst : ";
       std::vector< Node > inst;
       for( int i=0; i<riter.getNumTerms(); i++ ){
@@ -719,29 +763,27 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       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 ) ){
           Trace("fmc-exh-debug")  << " ...success.";
-          d_addedLemmas++;
-          successAdd = true;
+          addedLemmas++;
         }
       }
       Trace("fmc-exh-debug") << std::endl;
       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) {
+      if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && 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 );
       }
     }
+    d_addedLemmas += addedLemmas;
     return true;
   }else{
     return false;
@@ -750,9 +792,12 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
 
 void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {
   Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
-  if( n.getKind() == kind::BOUND_VARIABLE ){
+  //first check if it is a bounding literal
+  if( n.hasAttribute(BoundIntLitAttribute()) ){
+    Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;
+    d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );
+  }else if( n.getKind() == kind::BOUND_VARIABLE ){
     d.addEntry(fm, mkCondDefault(fm, f), n);
-    Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;
   }
   else if( n.getKind() == kind::NOT ){
     //just do directly
@@ -792,10 +837,12 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
   }
   else if( n.getNumChildren()==0 ){
     Node r = n;
-    if( !fm->hasTerm(n) ){
-      r = getSomeDomainElement(fm, n.getType() );
+    if( !n.isConst() ){
+      if( !fm->hasTerm(n) ){
+        r = getSomeDomainElement(fm, n.getType() );
+      }
+      r = fm->getUsedRepresentative( r );
     }
-    r = fm->getUsedRepresentative( r);
     d.addEntry(fm, mkCondDefault(fm, f), r);
   }
   else{
@@ -983,7 +1030,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
       int j = getVariableId(f, v);
       Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
-      if (!fm->isStar(cond[j+1])) {
+      if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) {
         v = cond[j+1];
       }else{
         bind_var = true;
@@ -992,18 +1039,30 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     if (bind_var) {
       Trace("fmc-uf-process") << "bind variable..." << std::endl;
       int j = getVariableId(f, v);
-      for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
-        cond[j+1] = it->first;
-        doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+      if( fm->isStar(cond[j+1]) ){
+        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+          cond[j+1] = it->first;
+          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+        }
+        cond[j+1] = fm->getStar(v.getType());
+      }else{
+        Node orig = cond[j+1];
+        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+          Node nw = doIntervalMeet( fm, it->first, orig );
+          if( !nw.isNull() ){
+            cond[j+1] = nw;
+            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+          }
+        }
+        cond[j+1] = orig;
       }
-      cond[j+1] = fm->getStar(v.getType());
     }else{
       if( !v.isNull() ){
         if (curr.d_child.find(v)!=curr.d_child.end()) {
           Trace("fmc-uf-process") << "follow value..." << std::endl;
           doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
         }
-        Node st = fm->getStar(v.getType());
+        Node st = fm->getStarElement(v.getType());
         if (curr.d_child.find(st)!=curr.d_child.end()) {
           Trace("fmc-uf-process") << "follow star..." << std::endl;
           doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);
@@ -1050,29 +1109,73 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, De
 }
 
 int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
+  Trace("fmc-debug2") << "isCompat " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
-    if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {
-      return 0;
+    if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+      Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );
+      if( iv.isNull() ){
+        return 0;
+      }
+    }else{
+      if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {
+        return 0;
+      }
     }
   }
   return 1;
 }
 
 bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
+  Trace("fmc-debug2") << "doMeet " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( cond[i]!=c[i-1] ) {
-      if( fm->isStar(cond[i]) ){
-        cond[i] = c[i-1];
-      }else if( !fm->isStar(c[i-1]) ){
-        return false;
+      if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+        Node iv = doIntervalMeet( fm, cond[i], c[i-1] );
+        if( !iv.isNull() ){
+          cond[i] = iv;
+        }else{
+          return false;
+        }
+      }else{
+        if( fm->isStar(cond[i]) ){
+          cond[i] = c[i-1];
+        }else if( !fm->isStar(c[i-1]) ){
+          return false;
+        }
       }
     }
   }
   return true;
 }
 
+Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {
+  if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){
+    std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;
+    exit( 0 );
+  }
+  Node b[2];
+  for( unsigned j=0; j<2; j++ ){
+    Node b1 = i1[j];
+    Node b2 = i2[j];
+    if( fm->isStar( b1 ) ){
+      b[j] = b2;
+    }else if( fm->isStar( b2 ) ){
+      b[j] = b1;
+    }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){
+      b[j] = j==0 ? b2 : b1;
+    }else{
+      b[j] = j==0 ? b1 : b2;
+    }
+  }
+  if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){
+    return mk ? fm->getInterval( b[0], b[1] ) : i1;
+  }else{
+    return Node::null();
+  }
+}
+
 Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
   return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
 }
@@ -1087,7 +1190,7 @@ void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::v
   //get function symbol for f
   cond.push_back(d_quant_cond[f]);
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {
-    Node ts = fm->getStar( f[0][i].getType() );
+    Node ts = fm->getStarElement( f[0][i].getType() );
     cond.push_back(ts);
   }
 }
@@ -1189,7 +1292,7 @@ void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std:
       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 );
+        new_indices[v].push_back( indices[i] );
       }
 
       for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){
@@ -1201,21 +1304,29 @@ void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std:
 
 void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
                                           std::map< int, std::map< int, Node > >& changed_vals ) {
+  Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : ";
+  for( unsigned i=0; i<indices.size(); i++ ){
+    Debug("fmc-interval-model-debug") << indices[i] << " ";
+  }
+  Debug("fmc-interval-model-debug") << std::endl;
+
   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 );
+        new_indices[v].push_back( indices[i] );
+        if( !v.isConst() ){
+          Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl;
+          Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl;
+        }
       }
 
       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 );
-        }
+        values.push_back( it->first );
       }
 
       if( tn.isInteger() ){
@@ -1236,6 +1347,7 @@ void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std
           }
           Node interval = fm->getInterval( lb, ub );
           for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){
+            Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl;
             changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;
           }
           ub = lb;
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 45110b2b7..2cb2198ef 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -39,7 +39,6 @@ public:
   int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );
   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 collectIndices(Node c, int index, std::vector< int >& indices );
   bool isComplete(FirstOrderModelFmc * m, Node c, int index);
 };
@@ -118,6 +117,7 @@ private:
                              std::vector< Def > & dc, int index,
                              std::vector< Node > & cond, std::vector<Node> & val );
   int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
+  Node doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk = true );
   bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
   Node mkCond( std::vector< Node > & cond );
   Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index dc00b5f95..e1a953e1b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -195,11 +195,15 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
     Node mbt;
     if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
-      std::stringstream ss;
-      ss << Expr::setlanguage(options::outputLanguage());
-      ss << "e_" << tn;
-      mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
-      Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
+      if( tn.isInteger() || tn.isReal() ){
+        mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+      }else{
+        std::stringstream ss;
+        ss << Expr::setlanguage(options::outputLanguage());
+        ss << "e_" << tn;
+        mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
+        Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
+      }
     }else{
       mbt = d_type_map[ tn ][ 0 ];
     }
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 180c4bbcf..b44cc6779 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -139,7 +139,6 @@ bool RepSetIterator::initialize(){
     //store default domain
     d_domain.push_back( RepDomain() );
     TypeNode tn = d_types[i];
-    bool isSet = false;
     if( tn.isSort() ){
       if( !d_rep_set->hasType( tn ) ){
         Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );
@@ -147,31 +146,36 @@ bool RepSetIterator::initialize(){
         d_rep_set->add( var );
       }
     }else if( tn.isInteger() ){
+      bool inc = false;
       //check if it is bound
       if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
         if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){
           Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl;
           d_enum_type.push_back( ENUM_RANGE );
-          isSet = true;
         }else{
-          Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl;
-          d_incomplete = true;
+          inc = true;
         }
       }else{
-        Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl;
-        d_incomplete = true;
+        inc = true;
       }
-    }else if( tn.isReal() ){
-      Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl;
-      d_incomplete = true;
-    //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
-    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){
+      if( inc ){
+        //check if it is otherwise bound
+        if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){
+          Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded." << std::endl;
+          d_enum_type.push_back( ENUM_RANGE );
+        }else{
+          Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl;
+          d_incomplete = true;
+        }
+      }
+    //enumerate if the sort is reasonably small, the upper bound of 1000 is chosen arbitrarily for now
+    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){
       d_rep_set->complete( tn );
     }else{
-      Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
+      Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
       d_incomplete = true;
     }
-    if( !isSet ){
+    if( d_enum_type.size()<=i ){
       d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
       if( d_rep_set->hasType( tn ) ){
         for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
@@ -182,7 +186,7 @@ bool RepSetIterator::initialize(){
       }
     }
   }
-  //must set a variable index order
+  //must set a variable index order based on bounded integers
   if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) {
     Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
     std::vector< int > varOrder;
@@ -211,6 +215,7 @@ bool RepSetIterator::initialize(){
     Trace("bound-int-rsi") << std::endl;
     setIndexOrder(indexOrder);
   }
+  //now reset the indices
   for (unsigned i=0; i<d_index.size(); i++) {
     if (!resetIndex(i, true)){
       break;
@@ -255,6 +260,19 @@ bool RepSetIterator::resetIndex( int i, bool initial ) {
         return false;
       }else{
         Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl;
+        for( unsigned b=0; b<2; b++ ){
+          if( d_bounds[b].find(ii)!=d_bounds[b].end() ){
+            Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl;
+            if( b==0 && d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>() ){
+              l = d_bounds[b][ii];
+            }else if( b==1 && d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>() ){
+              u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii],
+                                                    NodeManager::currentNM()->mkConst( Rational(1) ) );
+              u = Rewriter::rewrite( u );
+            }
+          }
+        }
+
         Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
         Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
         d_domain[ii].clear();
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 672f33b54..a619915ee 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -71,6 +71,8 @@ private:
   Node d_owner;
   //reset index
   bool resetIndex( int i, bool initial = false );
+  /** set index order */
+  void setIndexOrder( std::vector< int >& indexOrder );
 public:
   RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
   ~RepSetIterator(){}
@@ -104,9 +106,9 @@ public:
   //  for example, if d_index_order = { 2, 0, 1 }
   //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
   std::map< int, int > d_var_order;
+  //intervals
+  std::map< int, Node > d_bounds[2];
 public:
-  /** set index order */
-  void setIndexOrder( std::vector< int >& indexOrder );
   /** increment the iterator at index=counter */
   int increment2( int counter );
   /** increment the iterator */
-- 
2.30.2