Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing, implement get-qe-disjunct.

11 files changed, 324 insertions, 230 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index f2d5c640d..ead2bc57c 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -212,13 +212,14 @@ void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& term
   }
 }
 
-void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const {
+void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const {
   if( terms.size()==q[0].getNumChildren() ){
-    insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+    //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+    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, vars, terms );
+      it->second.getInstantiations( insts, q, terms, qe );
       terms.pop_back();
     }
   }
@@ -310,14 +311,15 @@ void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& te
   }
 }
 
-void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const{
+void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) 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( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) );
+      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, vars, terms );
+        it->second->getInstantiations( insts, q, terms, qe );
         terms.pop_back();
       }
     }
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index abe31b48d..35353863c 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -101,7 +101,7 @@ public:
   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< TNode >& vars, std::vector< TNode >& terms ) const;
+  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
 public:
   InstMatchTrie(){}
   ~InstMatchTrie(){}
@@ -132,13 +132,9 @@ public:
     std::vector< TNode > terms;
     print( out, q, terms );
   }
-  void getInstantiations( std::vector< Node >& insts, Node q ) {
-    std::vector< TNode > terms;
-    std::vector< TNode > vars;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      vars.push_back( q[0][i] );
-    }
-    getInstantiations( insts, q, vars, terms );
+  void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
+    std::vector< Node > terms;
+    getInstantiations( insts, q, terms, qe );
   }
   void clear() { d_data.clear(); }
 };/* class InstMatchTrie */
@@ -152,7 +148,7 @@ public:
   context::CDO< bool > d_valid;
 private:
   void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
-  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const;
+  void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
 public:
   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
   ~CDInstMatchTrie(){}
@@ -183,13 +179,9 @@ public:
     std::vector< TNode > terms;
     print( out, q, terms );
   }
-  void getInstantiations( std::vector< Node >& insts, Node q ) {
-    std::vector< TNode > terms;
-    std::vector< TNode > vars;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      vars.push_back( q[0][i] );
-    }
-    getInstantiations( insts, q, vars, terms );
+  void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
+    std::vector< Node > terms;
+    getInstantiations( insts, q, terms, qe );
   }
 };/* class CDInstMatchTrie */
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index d5ef2e290..ad400413e 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -34,8 +34,7 @@ using namespace CVC4::theory::arith;
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
 InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
-  : QuantifiersModule( qe )
-  , d_added_cbqi_lemma( qe->getUserContext() ){
+  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), d_added_inst( qe->getUserContext() ) {
 }
 
 InstStrategyCbqi::~InstStrategyCbqi() throw(){}
@@ -98,6 +97,14 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
         }else{
           Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
         }
+        //if doing partial quantifier elimination, do not process this if already processed once
+        if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ){
+          if( d_added_inst.find( q )!=d_added_inst.end() ){
+            d_quantEngine->getModel()->setQuantifierActive( q, false );
+            d_cbqi_set_quant_inactive = true;
+            d_incomplete_check = true;
+          }
+        }
       }
     }
   }
@@ -201,20 +208,25 @@ bool InstStrategyCbqi::doCbqi( Node q ){
   std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
   if( it==d_do_cbqi.end() ){
     bool ret = false;
-    //if has an instantiation pattern, don't do it
-    if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
-      ret = false;
+    if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
+      ret = true;
     }else{
-      if( options::cbqiAll() ){
-        ret = true;
+      //if has an instantiation pattern, don't do it
+      if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
+        ret = false;
       }else{
-        //if quantifier has a non-arithmetic variable, then do not use cbqi
-        //if quantifier has an APPLY_UF term, then do not use cbqi
-        Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
-        std::map< Node, bool > visited;
-        ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+        if( options::cbqiAll() ){
+          ret = true;
+        }else{
+          //if quantifier has a non-arithmetic variable, then do not use cbqi
+          //if quantifier has an APPLY_UF term, then do not use cbqi
+          Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+          std::map< Node, bool > visited;
+          ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+        }
       }
     }
+    Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl;
     d_do_cbqi[q] = ret;
     return ret;
   }else{
@@ -623,7 +635,12 @@ bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) {
   Assert( !d_curr_quant.isNull() );
   //check if we need virtual term substitution (if used delta or infinity)
   bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
-  return d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts );
+  if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
+    d_added_inst.insert( d_curr_quant );
+    return true;
+  }else{
+    return false;
+  }
 }
 
 bool InstStrategyCegqi::addLemma( Node lem ) {
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 5511af209..8de844eb8 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -39,6 +39,8 @@ protected:
   bool d_incomplete_check;
   /** whether we have added cbqi lemma */
   NodeSet d_added_cbqi_lemma;
+  /** whether we have instantiated quantified formulas */
+  NodeSet d_added_inst;
   /** whether to do cbqi for this quantified formula */
   std::map< Node, bool > d_do_cbqi;
   /** register ce lemma */
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 8c6b30124..040eadc9f 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -24,7 +24,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value ){
+void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){
   Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
   if( attr=="axiom" ){
     Trace("quant-attr-debug") << "Set axiom " << n << std::endl;
@@ -58,5 +58,13 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, s
     Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl;
     RrPriorityAttribute rrpa;
     n.setAttribute( rrpa, lvl );
+  }else if( attr=="quant-elim" ){
+    Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
+    QuantElimAttribute qea;
+    n.setAttribute( qea, true );
+  }else if( attr=="quant-elim-partial" ){
+    Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl;
+    QuantElimPartialAttribute qepa;
+    n.setAttribute( qepa, true );
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index bad58eef8..55461e5c1 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -36,7 +36,7 @@ struct QuantifiersAttributes
     *   This function will apply a custom set of attributes to all top-level universal
     *   quantifiers contained in n
     */
-  static void setUserAttribute( const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value );
+  static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value );
 };
 
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 881210d78..3c155c421 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -229,36 +229,27 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
 
 RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
-  if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){
-    RewriteStatus status = REWRITE_DONE;
-    Node ret = in;
-    //get the arguments
-    std::vector< Node > args;
-    for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
-      args.push_back( in[0][i] );
-    }
-    //get the instantiation pattern list
-    Node ipl;
+  RewriteStatus status = REWRITE_DONE;
+  Node ret = in;
+  //get the body
+  if( in.getKind()==EXISTS ){
+    std::vector< Node > children;
+    children.push_back( in[0] );
+    children.push_back( in[1].negate() );
     if( in.getNumChildren()==3 ){
-      ipl = in[2];
-    }
-    //get the body
-    if( in.getKind()==EXISTS ){
-      std::vector< Node > children;
-      children.push_back( in[0] );
-      children.push_back( in[1].negate() );
-      if( in.getNumChildren()==3 ){
-        children.push_back( in[2] );
-      }
-      ret = NodeManager::currentNM()->mkNode( FORALL, children );
-      ret = ret.negate();
-      status = REWRITE_AGAIN_FULL;
-    }else{
+      children.push_back( in[2] );
+    }
+    ret = NodeManager::currentNM()->mkNode( FORALL, children );
+    ret = ret.negate();
+    status = REWRITE_AGAIN_FULL;
+  }else if( in.getKind()==FORALL ){
+    //compute attributes
+    QAttributes qa;
+    TermDb::computeQuantAttributes( in, qa );
+    if( !qa.isRewriteRule() ){
       for( int op=0; op<COMPUTE_LAST; op++ ){
-        //TODO : compute isNested (necessary?)
-        bool isNested = false;
-        if( doOperation( in, isNested, op ) ){
-          ret = computeOperation( in, isNested, op );
+        if( doOperation( in, op, qa ) ){
+          ret = computeOperation( in, op, qa );
           if( ret!=in ){
             status = REWRITE_AGAIN_FULL;
             break;
@@ -266,15 +257,14 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
         }
       }
     }
-    //print if changed
-    if( in!=ret ){
-      Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
-      Trace("quantifiers-rewrite") << " to " << std::endl;
-      Trace("quantifiers-rewrite") << ret << std::endl;
-    }
-    return RewriteResponse( status, ret );
   }
-  return RewriteResponse(REWRITE_DONE, in);
+  //print if changed
+  if( in!=ret ){
+    Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
+    Trace("quantifiers-rewrite") << " to " << std::endl;
+    Trace("quantifiers-rewrite") << ret << std::endl;
+  }
+  return RewriteResponse( status, ret );
 }
 
 Node QuantifiersRewriter::computeElimSymbols( Node body ) {
@@ -564,12 +554,13 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v
   }
 }
 
-Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q ){
+Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ){
   std::map< Node, bool > curr_cond;
   std::map< Node, Node > cache;
   std::map< Node, Node > icache;
-  Node h = TermDb::getFunDefHead( q );
-  if( !h.isNull() ){
+  if( qa.isFunDef() ){
+    Node h = TermDb::getFunDefHead( q );
+    Assert( !h.isNull() );
     // if it is a function definition, rewrite the body independently
     Node fbody = TermDb::getFunDefBody( q );
     Assert( !body.isNull() );
@@ -782,7 +773,7 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){
   return false;
 }
 
-Node QuantifiersRewriter::computeCondSplit( Node body, Node ipl ){
+Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
   if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){
     Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
     std::map< Node, Node > pcons;
@@ -799,7 +790,8 @@ Node QuantifiersRewriter::computeCondSplit( Node body, Node ipl ){
     }
   }
   if( options::condVarSplitQuant() ){
-    if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() && !TermDb::isFunDefAnnotation( ipl ) ) ){
+    if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){
+      Assert( !qa.isFunDef() );
       Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl;
       bool do_split = false;
       unsigned index_max = body.getKind()==ITE ? 0 : 1;
@@ -956,7 +948,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
   return false;
 }
 
-Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ){
+Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ){
   Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
   QuantPhaseReq qpr( body );
   std::vector< Node > vars;
@@ -976,15 +968,15 @@ Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >
     //remake with eliminated nodes
     body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
     body = Rewriter::rewrite( body );
-    if( !ipl.isNull() ){
-      ipl = ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+    if( !qa.d_ipl.isNull() ){
+      qa.d_ipl = qa.d_ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
     }
     Trace("var-elim-quant") << "Return " << body << std::endl;
   }
   return body;
 }
 
-Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
+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() ){
@@ -994,7 +986,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
     Node prev;
     do{
       prev = body;
-      body = computeVarElimination2( body, args, ipl, var_parent );
+      body = computeVarElimination2( body, args, qa, var_parent );
     }while( prev!=body && !args.empty() );
   }
   return body;
@@ -1289,13 +1281,13 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node
   return f;
 }
 
-Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
+Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){
   std::vector< Node > activeArgs;
   //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables
-  if( options::ceGuidedInst() && TermDb::isSygusConjectureAnnotation( ipl ) ){
+  if( options::ceGuidedInst() && qa.d_sygus ){
     activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
   }else{
-    computeArgVec2( args, activeArgs, body, ipl );
+    computeArgVec2( args, activeArgs, body, qa.d_ipl );
   }
   if( activeArgs.empty() ){
     return body;
@@ -1303,14 +1295,14 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node i
     std::vector< Node > children;
     children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) );
     children.push_back( body );
-    if( !ipl.isNull() ){
-      children.push_back( ipl );
+    if( !qa.d_ipl.isNull() ){
+      children.push_back( qa.d_ipl );
     }
     return NodeManager::currentNM()->mkNode( kind::FORALL, children );
   }
 }
 
-Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ){
+Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ){
   if( body.getKind()==FORALL ){
     //combine arguments
     std::vector< Node > newArgs;
@@ -1318,26 +1310,26 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
       newArgs.push_back( body[0][i] );
     }
     newArgs.insert( newArgs.end(), args.begin(), args.end() );
-    return mkForAll( newArgs, body[ 1 ], ipl );
+    return mkForAll( newArgs, body[ 1 ], qa );
   }else{
     if( body.getKind()==NOT ){
       //push not downwards
       if( body[0].getKind()==NOT ){
-        return computeMiniscoping( f, args, body[0][0], ipl );
+        return computeMiniscoping( f, args, body[0][0], qa );
       }else if( body[0].getKind()==AND ){
         if( options::miniscopeQuantFreeVar() ){
           NodeBuilder<> t(kind::OR);
           for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
             t <<  ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() );
           }
-          return computeMiniscoping( f, args, t.constructNode(), ipl );
+          return computeMiniscoping( f, args, t.constructNode(), qa );
         }
       }else if( body[0].getKind()==OR ){
         if( options::miniscopeQuant() ){
           NodeBuilder<> t(kind::AND);
           for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
             Node trm = body[0][i].negate();
-            t << computeMiniscoping( f, args, trm, ipl );
+            t << computeMiniscoping( f, args, trm, qa );
           }
           return t.constructNode();
         }
@@ -1347,7 +1339,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
         //break apart
         NodeBuilder<> t(kind::AND);
         for( unsigned i=0; i<body.getNumChildren(); i++ ){
-          t << computeMiniscoping( f, args, body[i], ipl );
+          t << computeMiniscoping( f, args, body[i], qa );
         }
         Node retVal = t;
         return retVal;
@@ -1375,7 +1367,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
           return body_split;
         }else if( body_split.getNumChildren()>0 ){
           newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
-          body_split << mkForAll( args, newBody, ipl );
+          body_split << mkForAll( args, newBody, qa );
           return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
         }
       }
@@ -1384,7 +1376,7 @@ Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args,
   //if( body==f[1] ){
   //  return f;
   //}else{
-  return mkForAll( args, body, ipl );
+  return mkForAll( args, body, qa );
   //}
 }
 
@@ -1490,27 +1482,29 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
       return n;
     }
   }
-  return mkForAll( args, body, Node::null() );
+  QAttributes qa;
+  return mkForAll( args, body, qa );
 }
 
-bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
+bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& qa ){
+  bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef();
   if( computeOption==COMPUTE_ELIM_SYMBOLS ){
     return true;
   }else if( computeOption==COMPUTE_MINISCOPING ){
-    return true;
+    return is_std;
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
-    return options::aggressiveMiniscopeQuant();
+    return options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_NNF ){
     return options::nnfQuant();
   }else if( computeOption==COMPUTE_PROCESS_TERMS ){
     return true;
     //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
   }else if( computeOption==COMPUTE_COND_SPLIT ){
-    return options::iteDtTesterSplitQuant() || options::condVarSplitQuant();
+    return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && is_std;
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-    return options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant();
+    return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std;
   //}else if( computeOption==COMPUTE_CNF ){
   //  return options::cnfQuant();
   }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
@@ -1521,70 +1515,62 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
 }
 
 //general method for computing various rewrites
-Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOption ){
-  if( f.getKind()==FORALL ){
-    Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << ", nested = " << isNested << std::endl;
-    std::vector< Node > args;
-    for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-      args.push_back( f[0][i] );
-    }
-    Node n = f[1];
-    Node ipl;
-    if( f.getNumChildren()==3 ){
-      ipl = f[2];
-    }
-    if( computeOption==COMPUTE_ELIM_SYMBOLS ){
-      n = computeElimSymbols( n );
-    }else if( computeOption==COMPUTE_MINISCOPING ){
-      //return directly
-      return computeMiniscoping( f, args, n, ipl );
-    }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
-      return computeAggressiveMiniscoping( args, n );
-    }else if( computeOption==COMPUTE_NNF ){
-      n = computeNNF( n );
-    }else if( computeOption==COMPUTE_PROCESS_TERMS ){
-      std::vector< Node > new_conds;
-      n = computeProcessTerms( n, args, new_conds, f );
-      if( !new_conds.empty() ){
-        new_conds.push_back( n );
-        n = NodeManager::currentNM()->mkNode( OR, new_conds );
-      }
-    }else if( computeOption==COMPUTE_COND_SPLIT ){
-      n = computeCondSplit( n, ipl );
-    }else if( computeOption==COMPUTE_PRENEX ){
-      n = computePrenex( n, args, true );
-    }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-      n = computeVarElimination( n, args, ipl );
-    //}else if( computeOption==COMPUTE_CNF ){
-      //n = computeCNF( n, args, defs, false );
-      //ipl = Node::null();
-    }else if( computeOption==COMPUTE_PURIFY_EXPAND ){
-      std::vector< Node > conj;
-      computePurifyExpand( n, conj, args, ipl );
-      if( !conj.empty() ){
-        return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
-      }else{
-        return f;
-      }
+Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){
+  Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl;
+  std::vector< Node > args;
+  for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+    args.push_back( f[0][i] );
+  }
+  Node n = f[1];
+  if( computeOption==COMPUTE_ELIM_SYMBOLS ){
+    n = computeElimSymbols( n );
+  }else if( computeOption==COMPUTE_MINISCOPING ){
+    //return directly
+    return computeMiniscoping( f, args, n, qa );
+  }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
+    return computeAggressiveMiniscoping( args, n );
+  }else if( computeOption==COMPUTE_NNF ){
+    n = computeNNF( n );
+  }else if( computeOption==COMPUTE_PROCESS_TERMS ){
+    std::vector< Node > new_conds;
+    n = computeProcessTerms( n, args, new_conds, f, qa );
+    if( !new_conds.empty() ){
+      new_conds.push_back( n );
+      n = NodeManager::currentNM()->mkNode( OR, new_conds );
     }
-    Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
-    if( f[1]==n && args.size()==f[0].getNumChildren() ){
+  }else if( computeOption==COMPUTE_COND_SPLIT ){
+    n = computeCondSplit( n, qa );
+  }else if( computeOption==COMPUTE_PRENEX ){
+    n = computePrenex( n, args, true );
+  }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
+    n = computeVarElimination( n, args, qa );
+  //}else if( computeOption==COMPUTE_CNF ){
+    //n = computeCNF( n, args, defs, false );
+    //ipl = Node::null();
+  }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() ){
+    return f;
+  }else{
+    if( args.empty() ){
+      return n;
     }else{
-      if( args.empty() ){
-        return n;
-      }else{
-        std::vector< Node > children;
-        children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
-        children.push_back( n );
-        if( !ipl.isNull() ){
-          children.push_back( ipl );
-        }
-        return NodeManager::currentNM()->mkNode(kind::FORALL, children );
+      std::vector< Node > children;
+      children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
+      children.push_back( n );
+      if( !qa.d_ipl.isNull() ){
+        children.push_back( qa.d_ipl );
       }
+      return NodeManager::currentNM()->mkNode(kind::FORALL, children );
     }
-  }else{
-    return f;
   }
 }
 
@@ -1885,7 +1871,7 @@ Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, s
   }
 }
 
-void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, Node ipl ) {
+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;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 47997f9a7..dbb28827c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -26,6 +26,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class QAttributes;
+
 class QuantifiersRewriter {
 private:
   static int getPurifyIdLit2( Node n, std::map< Node, int >& visited );
@@ -37,7 +39,7 @@ public:
   static int getPurifyIdLit( Node n );
 private:
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
-  static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
+  static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
   static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited );
   static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
   static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
@@ -52,21 +54,21 @@ private:
                                       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, Node& ipl, std::map< Node, std::vector< int > >& var_parent );
+  static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent );
 private:
   static Node computeElimSymbols( Node body );
-  static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
+  static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   static Node computeNNF( Node body );
   //cache is dependent upon currCond, icache is not, new_conds are negated conditions
-  static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q );
-  static Node computeCondSplit( Node body, Node ipl );
+  static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
+  static Node computeCondSplit( Node body, QAttributes& qa );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
   static Node computeSplit( Node f, std::vector< Node >& args, Node body );
-  static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
+  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, Node ipl );
+  static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa );
 private:
   enum{
     COMPUTE_ELIM_SYMBOLS = 0,
@@ -82,7 +84,7 @@ private:
     //COMPUTE_CNF,
     COMPUTE_LAST
   };
-  static Node computeOperation( Node f, bool isNested, int computeOption );
+  static Node computeOperation( Node f, int computeOption, QAttributes& qa );
 public:
   static RewriteResponse preRewrite(TNode in);
   static RewriteResponse postRewrite(TNode in);
@@ -90,7 +92,7 @@ public:
   static inline void shutdown() {}
 private:
   /** options */
-  static bool doOperation( Node f, bool isNested, int computeOption );
+  static bool doOperation( Node f, int computeOption, QAttributes& qa );
 private:
   static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 public:
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a679ccfa8..284cae2e0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1787,69 +1787,107 @@ bool TermDb::isSygusConjectureAnnotation( Node ipl ){
   return false;
 }
 
+bool TermDb::isQuantElimAnnotation( Node ipl ) {
+  if( !ipl.isNull() ){
+    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+      if( ipl[i].getKind()==INST_ATTRIBUTE ){
+        Node avar = ipl[i][0];
+        if( avar.getAttribute(QuantElimAttribute()) ){
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
+
 void TermDb::computeAttributes( Node q ) {
+  computeQuantAttributes( q, d_qattr[q] );
+  if( !d_qattr[q].d_rr.isNull() ){
+    if( d_quantEngine->getRewriteEngine()==NULL ){
+      Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl;
+    }
+    //set rewrite engine as owner
+    d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+  }
+  if( d_qattr[q].isFunDef() ){
+    Node f = d_qattr[q].d_fundef_f;
+    if( d_fun_defs.find( f )!=d_fun_defs.end() ){
+      Message() << "Cannot define function " << f << " more than once." << std::endl;
+      exit( 1 );
+    }
+    d_fun_defs[f] = true;
+    d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
+  }
+  if( d_qattr[q].d_sygus ){
+    if( d_quantEngine->getCegInstantiation()==NULL ){
+      Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
+    }
+    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+  }
+  if( d_qattr[q].d_synthesis ){
+    if( d_quantEngine->getCegInstantiation()==NULL ){
+      Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
+    }
+    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+  }
+}
+
+void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){
   Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
   if( q.getNumChildren()==3 ){
+    qa.d_ipl = q[2];
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
       if( q[2][i].getKind()==INST_ATTRIBUTE ){
         Node avar = q[2][i][0];
         if( avar.getAttribute(AxiomAttribute()) ){
           Trace("quant-attr") << "Attribute : axiom : " << q << std::endl;
-          d_qattr_axiom[q] = true;
+          qa.d_axiom = true;
         }
         if( avar.getAttribute(ConjectureAttribute()) ){
           Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
-          d_qattr_conjecture[q] = true;
+          qa.d_conjecture = true;
         }
         if( avar.getAttribute(FunDefAttribute()) ){
           Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
-          d_qattr_fundef[q] = true;
           //get operator directly from pattern
-          Node f = q[2][i][0].getOperator();
-          if( d_fun_defs.find( f )!=d_fun_defs.end() ){
-            Message() << "Cannot define function " << f << " more than once." << std::endl;
-            exit( 0 );
-          }
-          d_fun_defs[f] = true;
-          d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
+          qa.d_fundef_f = q[2][i][0].getOperator();
         }
         if( avar.getAttribute(SygusAttribute()) ){
           //not necessarily nested existential
           //Assert( q[1].getKind()==NOT );
           //Assert( q[1][0].getKind()==FORALL );
-
           Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
-          d_qattr_sygus[q] = true;
-          if( d_quantEngine->getCegInstantiation()==NULL ){
-            Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
-          }
-          d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+          qa.d_sygus = true;
         }
         if( avar.getAttribute(SynthesisAttribute()) ){
           Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
-          d_qattr_synthesis[q] = true;
-          if( d_quantEngine->getCegInstantiation()==NULL ){
-            Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
-          }
-          d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+          qa.d_synthesis = true;
         }
         if( avar.hasAttribute(QuantInstLevelAttribute()) ){
-          d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute());
-          Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl;
+          qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
+          Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
         }
         if( avar.hasAttribute(RrPriorityAttribute()) ){
-          d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute());
-          Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl;
+          qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute());
+          Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl;
         }
+        if( avar.getAttribute(QuantElimAttribute()) ){
+          Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
+          qa.d_quant_elim = true;
+          //don't set owner, should happen naturally
+        } 
+        if( avar.getAttribute(QuantElimPartialAttribute()) ){
+          Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
+          qa.d_quant_elim = true;
+          qa.d_quant_elim_partial = true;
+          //don't set owner, should happen naturally
+        } 
         if( avar.getKind()==REWRITE_RULE ){
           Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
           Assert( i==0 );
-          if( d_quantEngine->getRewriteEngine()==NULL ){
-            Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl;
-          }
-          //set rewrite engine as owner
-          d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+          qa.d_rr = avar;
         }
       }
     }
@@ -1857,69 +1895,85 @@ void TermDb::computeAttributes( Node q ) {
 }
 
 bool TermDb::isQAttrConjecture( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_conjecture.find( q );
-  if( it==d_qattr_conjecture.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.d_conjecture;
   }
 }
 
 bool TermDb::isQAttrAxiom( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_axiom.find( q );
-  if( it==d_qattr_axiom.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.d_axiom;
   }
 }
 
 bool TermDb::isQAttrFunDef( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_fundef.find( q );
-  if( it==d_qattr_fundef.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.isFunDef();
   }
 }
 
 bool TermDb::isQAttrSygus( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_sygus.find( q );
-  if( it==d_qattr_sygus.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.d_sygus;
   }
 }
 
 bool TermDb::isQAttrSynthesis( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_synthesis.find( q );
-  if( it==d_qattr_synthesis.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.d_synthesis;
   }
 }
 
 int TermDb::getQAttrQuantInstLevel( Node q ) {
-  std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q );
-  if( it==d_qattr_qinstLevel.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return -1;
   }else{
-    return it->second;
+    return it->second.d_qinstLevel;
   }
 }
 
 int TermDb::getQAttrRewriteRulePriority( Node q ) {
-  std::map< Node, int >::iterator it = d_qattr_rr_priority.find( q );
-  if( it==d_qattr_rr_priority.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return -1;
   }else{
-    return it->second;
+    return it->second.d_rr_priority;
   }
 }
 
+bool TermDb::isQAttrQuantElim( Node q ) {
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
+    return false;
+  }else{
+    return it->second.d_quant_elim;
+  }
+}
 
+bool TermDb::isQAttrQuantElimPartial( Node q ) {
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
+    return false;
+  }else{
+    return it->second.d_quant_elim_partial;
+  }
+}
 
 TermDbSygus::TermDbSygus(){
   d_true = NodeManager::currentNM()->mkConst( true );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 0c4e94517..3fa0fbd29 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -99,6 +99,14 @@ typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
 struct AbsTypeFunDefAttributeId {};
 typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
 
+/** Attribute true for quantifiers that we are doing quantifier elimination on */
+struct QuantElimAttributeId {};
+typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;
+
+/** Attribute true for quantifiers that we are doing partial quantifier elimination on */
+struct QuantElimPartialAttributeId {};
+typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
+
 class QuantifiersEngine;
 
 namespace inst{
@@ -119,6 +127,26 @@ public:
 };/* class TermArgTrie */
 
 
+class QAttributes{
+public:
+  QAttributes() : d_conjecture(false), d_axiom(false), d_sygus(false),
+                  d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
+  ~QAttributes(){}
+  Node d_rr;
+  bool d_conjecture;
+  bool d_axiom;
+  Node d_fundef_f;
+  bool d_sygus;
+  bool d_synthesis;
+  int d_rr_priority;
+  int d_qinstLevel;
+  bool d_quant_elim;
+  bool d_quant_elim_partial;
+  Node d_ipl;
+  bool isRewriteRule() { return !d_rr.isNull(); }
+  bool isFunDef() { return !d_fundef_f.isNull(); }
+};
+
 namespace fmcheck {
   class FullModelChecker;
 }
@@ -440,15 +468,11 @@ public: //general queries concerning quantified formulas wrt modules
   static Node getFunDefHead( Node q );
   /** get fun def body */
   static Node getFunDefBody( Node q );
+  /** is quant elim annotation */
+  static bool isQuantElimAnnotation( Node ipl );
 //attributes
 private:
-  std::map< Node, bool > d_qattr_conjecture;
-  std::map< Node, bool > d_qattr_axiom;
-  std::map< Node, bool > d_qattr_fundef;
-  std::map< Node, bool > d_qattr_sygus;
-  std::map< Node, bool > d_qattr_synthesis;
-  std::map< Node, int > d_qattr_rr_priority;
-  std::map< Node, int > d_qattr_qinstLevel;
+  std::map< Node, QAttributes > d_qattr;
   //record attributes
   void computeAttributes( Node q );
 public:
@@ -466,7 +490,12 @@ public:
   int getQAttrQuantInstLevel( Node q );
   /** get rewrite rule priority */
   int getQAttrRewriteRulePriority( Node q );
-
+  /** is quant elim */
+  bool isQAttrQuantElim( Node q );
+  /** is quant elim partial */
+  bool isQAttrQuantElimPartial( Node q );
+  /** compute quantifier attributes */
+  static void computeQuantAttributes( Node q, QAttributes& qa );
 };/* class TermDb */
 
 class TermDbSygus {
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 86fc057ea..e3992f1a7 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -47,6 +47,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   out.handleUserAttribute( "synthesis", this );
   out.handleUserAttribute( "quant-inst-max-level", this );
   out.handleUserAttribute( "rr-priority", this );
+  out.handleUserAttribute( "quant-elim", this );
+  out.handleUserAttribute( "quant-elim-partial", this );
 }
 
 TheoryQuantifiers::~TheoryQuantifiers() {