5 files changed, 352 insertions, 253 deletions

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 3177739ac..facd7bd2e 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -662,7 +662,7 @@ Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices
   Assert( index<d_inst.size() );
   Assert( i<d_inst[index].size() );
   unsigned uindex = indices[index];
-  if( index==d_inst.size()-1 ){
+  if( index==indices.size()-1 ){
     return d_inst[uindex][i];
   }else{
     Node cond = d_lemmas_produced[uindex];
@@ -753,12 +753,29 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
 
     //construct the solution
     Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
+    bool useUnsatCore = false;
+    std::vector< Node > active_lemmas;
+    /*  TODO?
+    //minimize based on unsat core, if possible
+    std::vector< Node > active_lemmas;
+    if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){
+      useUnsatCore = true;
+    } 
+    */
     Assert( d_lemmas_produced.size()==d_inst.size() );
     std::vector< unsigned > indices;
     for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){
-      Assert( sol_index<d_inst[i].size() );
-      indices.push_back( i );
+      bool incl = true;
+      if( useUnsatCore ){
+        incl = std::find( active_lemmas.begin(), active_lemmas.end(), d_lemmas_produced[i] )!=active_lemmas.end();
+      }
+      if( incl ){
+        Assert( sol_index<d_inst[i].size() );
+        indices.push_back( i );
+      }
     }
+    Trace("csi-sol") << "...included " << indices.size() << " / " << d_lemmas_produced.size() << " instantiations." << std::endl;
+    Assert( !indices.empty() );
     //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions)
     // TODO : to minimize solution size, put the largest term last
     sortSiInstanceIndices ssii;
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 8818175db..c419bbc46 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -199,31 +199,90 @@ bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector<
   }
 }
 
-void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const {
+bool InstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio, int index ){
+  if( index==(int)q[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
+    setInstLemma( lem );
+    return true;
+  }else{
+    int i_index = imtio ? imtio->d_order[index] : index;
+    std::map< Node, InstMatchTrie >::iterator it = d_data.find( m[i_index] );
+    if( it!=d_data.end() ){
+      return it->second.recordInstLemma( q, m, lem, imtio, index+1 );
+    }else{
+      return false;
+    }
+  }
+}
+
+void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const {
   if( terms.size()==q[0].getNumChildren() ){
-    out << "  ( ";
-    for( unsigned i=0; i<terms.size(); i++ ){
-      if( i>0 ){ out << ", ";}
-      out << terms[i];
+    bool print;
+    if( useActive ){
+      if( hasInstLemma() ){
+        Node lem = getInstLemma();
+        print = std::find( active.begin(), active.end(), lem )!=active.end();
+      }else{
+        print = false;
+      }
+    }else{
+      print = true;
+    }  
+    if( print ){ 
+      if( firstTime ){
+        out << "Instantiations of " << q << " : " << std::endl;
+        firstTime = false;
+      }
+      out << "  ( ";
+      for( unsigned i=0; i<terms.size(); i++ ){
+        if( i>0 ){ out << ", ";}
+        out << terms[i];
+      }
+      out << " )" << std::endl;
     }
-    out << " )" << std::endl;
   }else{
     for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
       terms.push_back( it->first );
-      it->second.print( out, q, terms );
+      it->second.print( out, q, terms, firstTime, useActive, active );
       terms.pop_back();
     }
   }
 }
 
-void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const {
+void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const {
   if( terms.size()==q[0].getNumChildren() ){
-    //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
-    insts.push_back( qe->getInstantiation( q, terms, true ) );
+    if( useActive ){
+      if( hasInstLemma() ){
+        Node lem = getInstLemma();
+        if( std::find( active.begin(), active.end(), lem )!=active.end() ){
+          insts.push_back( lem );
+        }
+      }
+    }else{
+      insts.push_back( qe->getInstantiation( q, terms, true ) );
+    }
   }else{
     for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
       terms.push_back( it->first );
-      it->second.getInstantiations( insts, q, terms, qe );
+      it->second.getInstantiations( insts, q, terms, qe, useActive, active );
+      terms.pop_back();
+    }
+  }
+}
+
+void InstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
+  if( terms.size()==q[0].getNumChildren() ){
+    if( hasInstLemma() ){
+      Node lem = getInstLemma();
+      if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){
+        quant[lem] = q;
+        tvec[lem].clear();
+        tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() );
+      }
+    }
+  }else{
+    for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
+      terms.push_back( it->first );
+      it->second.getExplanationForInstLemmas( q, terms, lems, quant, tvec );
       terms.pop_back();
     }
   }
@@ -301,8 +360,7 @@ bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vecto
       return false;
     }
   }else{
-    Node n = m[index];
-    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] );
     if( it!=d_data.end() ){
       return it->second->removeInstMatch( qe, q, m, index+1 );
     }else{
@@ -311,34 +369,99 @@ bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vecto
   }
 }
 
-void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{
+bool CDInstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index ) {
+  if( index==(int)q[0].getNumChildren() ){
+    if( d_valid.get() ){
+      setInstLemma( lem );
+      return true;
+    }else{
+      return false;
+    }
+  }else{
+    std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] );
+    if( it!=d_data.end() ){
+      return it->second->recordInstLemma( q, m, lem, index+1 );
+    }else{
+      return false;
+    }
+  }
+}
+
+void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
   if( d_valid.get() ){
     if( terms.size()==q[0].getNumChildren() ){
-      out << "  ( ";
-      for( unsigned i=0; i<terms.size(); i++ ){
-        if( i>0 ) out << ", ";
-        out << terms[i];
+      bool print;    
+      if( useActive ){
+        if( hasInstLemma() ){
+          Node lem = getInstLemma();
+          print = std::find( active.begin(), active.end(), lem )!=active.end();
+        }else{
+          print = false;
+        }
+      }else{
+        print = true;
+      }  
+      if( print ){ 
+        if( firstTime ){
+          out << "Instantiations of " << q << " : " << std::endl;
+          firstTime = false;
+        }
+        out << "  ( ";
+        for( unsigned i=0; i<terms.size(); i++ ){
+          if( i>0 ) out << ", ";
+          out << terms[i];
+        }
+        out << " )" << std::endl;
       }
-      out << " )" << std::endl;
     }else{
       for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
         terms.push_back( it->first );
-        it->second->print( out, q, terms );
+        it->second->print( out, q, terms, firstTime, useActive, active );
         terms.pop_back();
       }
     }
   }
 }
 
-void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const{
+void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const{
   if( d_valid.get() ){
     if( terms.size()==q[0].getNumChildren() ){
-      //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
-      insts.push_back( qe->getInstantiation( q, terms, true ) );
+      if( useActive ){
+        if( hasInstLemma() ){
+          Node lem;
+          if( std::find( active.begin(), active.end(), lem )!=active.end() ){
+            insts.push_back( lem );
+          }
+        }
+      }else{
+        insts.push_back( qe->getInstantiation( q, terms, true ) );
+      }
+    }else{
+      for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
+        terms.push_back( it->first );
+        it->second->getInstantiations( insts, q, terms, qe, useActive, active );
+        terms.pop_back();
+      }
+    }
+  }
+}
+
+
+void CDInstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
+  if( d_valid.get() ){
+    if( terms.size()==q[0].getNumChildren() ){
+      if( hasInstLemma() ){
+        Node lem;
+        if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){
+          quant[lem] = q;
+          tvec[lem].clear();
+          tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() );
+        }
+      }
     }else{
       for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
         terms.push_back( it->first );
-        it->second->getInstantiations( insts, q, terms, qe );
+        it->second->getExplanationForInstLemmas( q, terms, lems, quant, tvec );
         terms.pop_back();
       }
     }
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index ad287c1a3..68446922f 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -96,12 +96,19 @@ public:
   public:
     std::vector< int > d_order;
   };/* class InstMatchTrie ImtIndexOrder */
-
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
 private:
-  void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
-  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
+  void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
+  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
+  void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const;
+private:
+  void setInstLemma( Node n ){ 
+    d_data.clear();
+    d_data[n].clear(); 
+  }
+  bool hasInstLemma() const { return !d_data.empty(); }
+  Node getInstLemma() const { return d_data.begin()->first; }
 public:
   InstMatchTrie(){}
   ~InstMatchTrie(){}
@@ -129,14 +136,19 @@ public:
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
                      ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
   bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
-  void print( std::ostream& out, Node q ) const{
+  bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio = NULL, int index = 0 );
+  void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
     std::vector< TNode > terms;
-    print( out, q, terms );
+    print( out, q, terms, firstTime, useActive, active );
   }
-  void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
+  void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
     std::vector< Node > terms;
-    getInstantiations( insts, q, terms, qe );
+    getInstantiations( insts, q, terms, qe, useActive, active );
   }
+  void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
+    std::vector< Node > terms;
+    getExplanationForInstLemmas( q, terms, lems, quant, tvec );
+  }  
   void clear() { d_data.clear(); }
 };/* class InstMatchTrie */
 
@@ -147,9 +159,17 @@ private:
   std::map< Node, CDInstMatchTrie* > d_data;
   /** is valid */
   context::CDO< bool > d_valid;
-
-  void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
-  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
+private:
+  void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const;
+  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const;
+  void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const;
+private:
+  void setInstLemma( Node n ){ 
+    d_data.clear();
+    d_data[n] = NULL; 
+  }
+  bool hasInstLemma() const { return !d_data.empty(); }
+  Node getInstLemma() const { return d_data.begin()->first; }
 public:
   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
   ~CDInstMatchTrie();
@@ -177,14 +197,19 @@ public:
   bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
                      int index = 0, bool onlyExist = false );
   bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
-  void print( std::ostream& out, Node q ) const{
+  bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index = 0 );
+  void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{
     std::vector< TNode > terms;
-    print( out, q, terms );
+    print( out, q, terms, firstTime, useActive, active );
   }
-  void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
+  void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) {
     std::vector< Node > terms;
-    getInstantiations( insts, q, terms, qe );
+    getInstantiations( insts, q, terms, qe, useActive, active );
   }
+  void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const {
+    std::vector< Node > terms;
+    getExplanationForInstLemmas( q, terms, lems, quant, tvec );
+  }  
 };/* class CDInstMatchTrie */
 
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2d56f2cdf..7e896d358 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -85,48 +85,6 @@ bool QuantifiersRewriter::isCube( Node n ){
   }
 }
 
-int QuantifiersRewriter::getPurifyId( Node n ){
-  if( !TermDb::hasBoundVarAttr( n ) ){
-    return 0;
-  }else if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){
-    return 1;
-  }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE ){
-    return 0;
-  }else{
-    return -1;
-  }
-}
-
-int QuantifiersRewriter::getPurifyIdLit2( Node n, std::map< Node, int >& visited ) {
-  std::map< Node, int >::iterator it = visited.find( n );
-  if( visited.find( n )==visited.end() ){
-    int ret = 0;
-    if( TermDb::hasBoundVarAttr( n ) ){
-      ret = getPurifyId( n );
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        int cid = getPurifyIdLit2( n[i], visited );
-        if( cid!=0 ){
-          if( ret==0 ){
-            ret = cid;
-          }else if( cid!=ret ){
-            ret = -2;
-            break;
-          }
-        }
-      }
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return it->second;
-  }
-}
-
-int QuantifiersRewriter::getPurifyIdLit( Node n ) {
-  std::map< Node, int > visited;
-  return getPurifyIdLit2( n, visited );
-}
-
 void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
   if( n.getKind()==OR ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
@@ -884,29 +842,53 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
   return body;
 }
 
-bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) {
+bool QuantifiersRewriter::isVariableElim( Node v, Node s ) {
   if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
     return false;
   }else{
-    if( !var_parent.empty() ){
-      std::map< Node, std::vector< int > >::iterator it = var_parent.find( v );
-      if( it!=var_parent.end() ){
-        Assert( !it->second.empty() );
-        int id = getPurifyId( s );
-        return it->second.size()==1 && it->second[0]==id;
+    return true;
+  }
+}
+
+void QuantifiersRewriter::isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, 
+                                               std::map< Node, bool >& elig_vars  ) {
+  int vindex = hasPol ? ( pol ? 1 : -1 ) : 0;
+  if( visited[n].find( vindex )==visited[n].end() ){
+    visited[n][vindex] = true;
+    if( elig_vars.find( n )!=elig_vars.end() ){
+      //variable contained in a place apart from bounds, no longer eligible for elimination
+      elig_vars.erase( n );
+      Trace("var-elim-ineq-debug") << "...found occurrence of " << n << ", mark ineligible" << std::endl;
+    }else{
+      if( hasPol ){
+        std::map< Node, int >::iterator itx = exclude.find( n );
+        if( itx!=exclude.end() && itx->second==vindex ){
+          //already processed this literal
+          return;
+        }
+      }
+      for( unsigned j=0; j<n.getNumChildren(); j++ ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( n, j, hasPol, pol, newHasPol, newPol );
+        isVariableBoundElig( n[j], exclude, visited, newHasPol, newPol, elig_vars );
+        if( elig_vars.empty() ){
+          break;
+        }
       }
     }
-    return true;
+  }else{
+    //already visited
   }
 }
 
 bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vector< Node >& args, std::vector< Node >& vars, std::vector< Node >& subs,
-                                                  std::map< Node, std::vector< int > >& var_parent ) {
-  if( lit.getKind()==EQUAL && pol ){
+                                                  std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds ) {
+  if( lit.getKind()==EQUAL && pol && options::varElimQuant() ){
     for( unsigned i=0; i<2; i++ ){
       std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] );
       if( ita!=args.end() ){
-        if( isVariableElim( lit[i], lit[1-i], var_parent ) ){
+        if( isVariableElim( lit[i], lit[1-i] ) ){
           Trace("var-elim-quant") << "Variable eliminate based on equality : " << lit[i] << " -> " << lit[1-i] << std::endl;
           vars.push_back( lit[i] );
           subs.push_back( lit[1-i] );
@@ -915,28 +897,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
         }
       }
     }
-    //for arithmetic, solve the equality
-    if( lit[0].getType().isReal() ){
-      std::map< Node, Node > msum;
-      if( QuantArith::getMonomialSumLit( lit, msum ) ){
-        for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
-          std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first );
-          if( ita!=args.end() ){
-            Node veq_c;
-            Node val;
-            int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL );
-            if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){
-              Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl;
-              vars.push_back( itm->first );
-              subs.push_back( val );
-              args.erase( ita );
-              return true;
-            }
-          }
-        }
-      }
-    }
-  }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE ){
+  }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ){
     Trace("var-elim-dt") << "Expand datatype variable based on : " << lit << std::endl;
     std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[0] );
     if( ita!=args.end() ){
@@ -960,7 +921,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
       args.insert( args.end(), newVars.begin(), newVars.end() );
       return true;
     }
-  }else if( lit.getKind()==BOUND_VARIABLE ){
+  }else if( lit.getKind()==BOUND_VARIABLE && options::varElimQuant() ){
     std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
     if( ita!=args.end() ){
       Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl;
@@ -970,24 +931,69 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
       return true;
     }
   }
+  if( ( lit.getKind()==EQUAL && lit[0].getType().isReal() && pol ) || ( ( lit.getKind()==GEQ || lit.getKind()==GT ) && options::varIneqElimQuant() ) ){
+    //for arithmetic, solve the (in)equality
+    std::map< Node, Node > msum;
+    if( QuantArith::getMonomialSumLit( lit, msum ) ){
+      for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
+        if( !itm->first.isNull() ){
+          std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first );
+          if( ita!=args.end() ){
+            if( lit.getKind()==EQUAL ){
+              Assert( pol );
+              Node veq_c;
+              Node val;
+              int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL );
+              if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val ) ){
+                Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl;
+                vars.push_back( itm->first );
+                subs.push_back( val );
+                args.erase( ita );
+                return true;
+              }
+            }else{
+              Assert( lit.getKind()==GEQ || lit.getKind()==GT );
+              //store that this literal is upper/lower bound for itm->first
+              Node veq_c;
+              Node val;
+              int ires = QuantArith::isolate( itm->first, msum, veq_c, val, lit.getKind() );
+              if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val ) ){
+                bool is_upper = pol!=( ires==1 );
+                Trace("var-elim-ineq-debug") << lit << " is a " << ( is_upper ? "upper" : "lower" ) << " bound for " << itm->first << std::endl;
+                Trace("var-elim-ineq-debug") << "  pol/ires = " << pol << " " << ires << std::endl;
+                num_bounds[itm->first][is_upper][lit] = pol;
+              }
+            }
+          }else{
+            //compute variables in itm->first, these are not eligible for elimination
+            std::vector< Node > bvs;
+            TermDb::getBoundVars( itm->first, bvs );
+            for( unsigned j=0; j<bvs.size(); j++ ){
+              num_bounds[bvs[j]][true].clear();
+              num_bounds[bvs[j]][false].clear();
+            }
+          }
+        }
+      }
+    }
+  }
+  
   return false;
 }
 
-Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ){
+Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ){
   Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
+  std::map< Node, std::map< bool, std::map< Node, bool > > > num_bounds;
   QuantPhaseReq qpr( body );
   std::vector< Node > vars;
   std::vector< Node > subs;
   for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
-    //Notice() << "   " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
-    if( ( it->first.getKind()==EQUAL && it->second && options::varElimQuant() ) ||
-        ( it->first.getKind()==APPLY_TESTER && it->second && it->first[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ) ||
-        ( it->first.getKind()==BOUND_VARIABLE && options::varElimQuant() ) ){
-      if( computeVariableElimLit( it->first, it->second, args, vars, subs, var_parent ) ){
-        break;
-      }
+    Trace("var-elim-quant-debug") << "   phase req : " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
+    if( computeVariableElimLit( it->first, it->second, args, vars, subs, num_bounds ) ){
+      break;
     }
   }
+  
   if( !vars.empty() ){
     Trace("var-elim-quant-debug") << "VE " << vars.size() << "/" << args.size() << std::endl;
     //remake with eliminated nodes
@@ -997,21 +1003,65 @@ Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >
       qa.d_ipl = qa.d_ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
     }
     Trace("var-elim-quant") << "Return " << body << std::endl;
+  }else{
+    //collect all variables that have only upper/lower bounds
+    std::map< Node, bool > elig_vars;
+    for( std::map< Node, std::map< bool, std::map< Node, bool > > >::iterator it = num_bounds.begin(); it != num_bounds.end(); ++it ){
+      if( it->second.find( true )==it->second.end() ){
+        Trace("var-elim-ineq-debug") << "Variable " << it->first << " has only lower bounds." << std::endl;
+        elig_vars[it->first] = false;
+      }else if( it->second.find( false )==it->second.end() ){
+        Trace("var-elim-ineq-debug") << "Variable " << it->first << " has only upper bounds." << std::endl;
+        elig_vars[it->first] = true;
+      }
+    }
+    if( !elig_vars.empty() ){
+      std::vector< Node > inactive_vars;
+      std::map< Node, std::map< int, bool > > visited;
+      std::map< Node, int > exclude;
+      for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+        if( it->first.getKind()==GEQ || it->first.getKind()==GT ){
+          exclude[ it->first ] = it->second ? -1 : 1;
+          Trace("var-elim-ineq-debug") << "...exclude " << it->first << " at polarity " << exclude[ it->first ] << std::endl;
+        }
+      }
+      //traverse the body, invalidate variables if they occur in places other than the bounds they occur in
+      isVariableBoundElig( body, exclude, visited, true, true, elig_vars );
+      
+      if( !elig_vars.empty() ){
+        if( !qa.d_ipl.isNull() ){
+          isVariableBoundElig( qa.d_ipl, exclude, visited, false, true, elig_vars );
+        }
+        for( std::map< Node, bool >::iterator itev = elig_vars.begin(); itev != elig_vars.end(); ++itev ){
+          Node v = itev->first;
+          Trace("var-elim-ineq-debug") << v << " is eligible for elimination." << std::endl;
+          //do substitution corresponding to infinite projection, all literals involving unbounded variable go to true/false
+          std::vector< Node > terms;
+          std::vector< Node > subs;
+          for( std::map< Node, bool >::iterator itb = num_bounds[v][elig_vars[v]].begin(); itb != num_bounds[v][elig_vars[v]].end(); ++itb ){
+            Trace("var-elim-ineq-debug") << "  subs : " << itb->first << " -> " << itb->second << std::endl;
+            terms.push_back( itb->first );
+            subs.push_back( NodeManager::currentNM()->mkConst( itb->second ) );
+          }
+          body = body.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+          Trace("var-elim-ineq-debug") << "Return " << body << std::endl;
+          //eliminate from args
+          std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), v );
+          Assert( ita!=args.end() );
+          args.erase( ita );
+        }
+      } 
+    }
   }
   return body;
 }
 
 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ){
-  //the parent id's for each variable, if using purifyQuant
-  std::map< Node, std::vector< int > > var_parent;
-  if( options::purifyQuant() ){
-    body = computePurify( body, args, var_parent );
-  }
   if( options::varElimQuant() || options::dtVarExpandQuant() ){
     Node prev;
     do{
       prev = body;
-      body = computeVarElimination2( body, args, qa, var_parent );
+      body = computeVarElimination2( body, args, qa );
     }while( prev!=body && !args.empty() );
   }
   return body;
@@ -1358,9 +1408,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-    return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std;
-  }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
-    return options::purifyQuant() && is_std;
+    return ( options::varElimQuant() || options::dtVarExpandQuant() ) && is_std;
   }else{
     return false;
   }
@@ -1394,14 +1442,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
     n = computePrenex( n, args, true );
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     n = computeVarElimination( n, args, qa );
-  }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
-    std::vector< Node > conj;
-    computePurifyExpand( n, conj, args, qa );
-    if( !conj.empty() ){
-      return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
-    }else{
-      return f;
-    }
   }
   Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
   if( f[1]==n && args.size()==f[0].getNumChildren() ){
@@ -1633,104 +1673,3 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   return n;
 }
 
-Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
-                                          std::map< Node, std::vector< int > >& var_parent, int parentId ){
-  std::map< Node, Node >::iterator it = visited.find( body );
-  if( it!=visited.end() ){
-    return it->second;
-  }else{
-    Node ret = body;
-    if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::hasBoundVarAttr( ret ) ){
-      std::vector< Node > children;
-      bool childrenChanged = false;
-      int id = getPurifyId( body );
-      for( unsigned i=0; i<body.getNumChildren(); i++ ){
-        Node bi;
-        if( body.getKind()==EQUAL && i==1 ){
-          int cid = getPurifyId( children[0] );
-          bi = computePurify2( body[i], args, visited, var_to_term, var_parent, cid );
-          if( children[0].getKind()==BOUND_VARIABLE ){
-            cid = getPurifyId( bi );
-            if( cid!=0 && std::find( var_parent[children[0]].begin(), var_parent[children[0]].end(), cid )==var_parent[children[0]].end() ){
-              var_parent[children[0]].push_back( id );
-            }
-          }
-        }else{
-          bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id );
-        }
-        childrenChanged = childrenChanged || bi!=body[i];
-        children.push_back( bi );
-        if( id!=0 && bi.getKind()==BOUND_VARIABLE ){
-          if( std::find( var_parent[bi].begin(), var_parent[bi].end(), id )==var_parent[bi].end() ){
-            var_parent[bi].push_back( id );
-          }
-        }
-      }
-      if( childrenChanged ){
-        if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.insert( children.begin(), body.getOperator() );
-        }
-        ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
-      }
-      if( parentId!=0 && parentId!=id ){
-        Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() );
-        var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) );
-        ret = v;
-        args.push_back( v );
-      }
-    }
-    visited[body] = ret;
-    return ret;
-  }
-}
-
-Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) {
-  std::map< Node, Node > visited;
-  std::map< Node, Node > var_to_term;
-  Node pbody = computePurify2( body, args, visited, var_to_term, var_parent, 0 );
-  if( pbody==body ){
-    return body;
-  }else{
-    Trace("quantifiers-rewrite-purify") << "Purify : " << body << std::endl;
-    Trace("quantifiers-rewrite-purify") << "   Got : " << pbody << std::endl;
-    for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){
-      Trace("quantifiers-rewrite-purify") << "         " << it->first << " : " << it->second << std::endl;
-    }
-    Trace("quantifiers-rewrite-purify") << "Variable parents : " << std::endl;
-    for( std::map< Node, std::vector< int > >::iterator it = var_parent.begin(); it != var_parent.end(); ++it ){
-      Trace("quantifiers-rewrite-purify") << "  " << it->first << " -> ";
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        Trace("quantifiers-rewrite-purify") << it->second[i] << " ";
-      }
-      Trace("quantifiers-rewrite-purify") << std::endl;
-    }
-    Trace("quantifiers-rewrite-purify") << std::endl;
-    std::vector< Node > disj;
-    for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){
-      disj.push_back( it->second.negate() );
-    }
-    Node res;
-    if( disj.empty() ){
-      res = pbody;
-    }else{
-      disj.push_back( pbody );
-      res = NodeManager::currentNM()->mkNode( OR, disj );
-    }
-    Trace("quantifiers-rewrite-purify") << "Constructed : " << res << std::endl << std::endl;
-    return res;
-  }
-}
-
-void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ) {
-  if( body.getKind()==OR ){
-    Trace("quantifiers-rewrite-purify-exp") << "Purify expansion : " << body << std::endl;
-    std::map< int, std::vector< Node > > disj;
-    std::map< int, std::vector< Node > > fvs;
-    for( unsigned i=0; i<body.getNumChildren(); i++ ){
-      int pid CVC4_UNUSED = getPurifyIdLit( body[i] );
-    }
-    //mark as an attribute
-    //Node attr = NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, body );
-  }
-}
-
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 776517109..60dc8ab10 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -35,8 +35,6 @@ public:
   static bool isClause( Node n );
   static bool isLiteral( Node n );
   static bool isCube( Node n );
-  static int getPurifyId( Node n );
-  static int getPurifyIdLit( Node n );
 private:
   static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
@@ -49,12 +47,12 @@ private:
                                     std::vector< Node >& new_vars, std::vector< Node >& new_conds );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
   static bool isConditionalVariableElim( Node n, int pol=0 );
-  static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent );
+  static bool isVariableElim( Node v, Node s );
+  static void isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, 
+                                   std::map< Node, bool >& elig_vars );
   static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
-                                      std::map< Node, std::vector< int > >& var_parent );
-  static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
-                              std::map< Node, std::vector< int > >& var_parent, int parentId );
-  static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent );
+                                      std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds );
+  static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa );
 private:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
@@ -65,8 +63,6 @@ private:
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
-  static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent );
-  static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa );
 private:
   enum{
     COMPUTE_ELIM_SYMBOLS = 0,
@@ -76,7 +72,6 @@ private:
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
     COMPUTE_COND_SPLIT,
-    COMPUTE_PURIFY_EXPAND,
     //COMPUTE_FLATTEN_ARGS_UF,
     //COMPUTE_CNF,
     COMPUTE_LAST