Add support for interval models in bounded integers MBQI (in progress).

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