update from the master

1 files changed, 318 insertions, 272 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index afe8cd598..5aae4d640 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file quantifiers_rewriter.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of QuantifiersRewriter class
  **/
@@ -229,52 +229,48 @@ 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;
+  int rew_op = -1;
+  //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;
+      children.push_back( in[2] );
+    }
+    ret = NodeManager::currentNM()->mkNode( FORALL, children );
+    ret = ret.negate();
+    status = REWRITE_AGAIN_FULL;
+  }else if( in.getKind()==FORALL ){
+    if( in[1].isConst() ){
+      return RewriteResponse( status, in[1] );
     }else{
-      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( ret!=in ){
-            status = REWRITE_AGAIN_FULL;
-            break;
+      //compute attributes
+      QAttributes qa;
+      TermDb::computeQuantAttributes( in, qa );
+      if( !qa.isRewriteRule() ){
+        for( int op=0; op<COMPUTE_LAST; op++ ){
+          if( doOperation( in, op, qa ) ){
+            ret = computeOperation( in, op, qa );
+            if( ret!=in ){
+              rew_op = op;
+              status = REWRITE_AGAIN_FULL;
+              break;
+            }
           }
         }
       }
     }
-    //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 (op=" << rew_op << ") " << in << std::endl;
+    Trace("quantifiers-rewrite") << " to " << std::endl;
+    Trace("quantifiers-rewrite") << ret << std::endl;
+  }
+  return RewriteResponse( status, ret );
 }
 
 Node QuantifiersRewriter::computeElimSymbols( Node body ) {
@@ -315,6 +311,10 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) {
       }
       childrenChanged = childrenChanged || c!=body[i];
     }
+    //if( body.getKind()==ITE && isLiteral( body[0] ) ){
+    //  ret = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ), 
+    //                                               NodeManager::currentNM()->mkNode( OR, body[0], body[2] ) );
+    //}
     if( childrenChanged ){
       return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children );
     }else{
@@ -330,7 +330,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
     }else if( isLiteral( body[0] ) ){
       return body;
     }else{
-      std::vector< Node > children;
+      std::vector< Node > children; 
       Kind k = body[0].getKind();
 
       if( body[0].getKind()==OR || body[0].getKind()==AND ){
@@ -564,12 +564,23 @@ 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 ){
+void removeEntailedCond( std::map< Node, bool >& currCond, std::vector< Node >& new_cond, std::map< Node, Node >& cache ) {
+  if( !new_cond.empty() ){
+    for( unsigned j=0; j<new_cond.size(); j++ ){
+      currCond.erase( new_cond[j] );
+    }
+    new_cond.clear();
+    cache.clear();
+  }
+}
+
+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() );
@@ -591,96 +602,119 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
     ret = iti->second;
     Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl;
   }else{
-    bool firstTimeCD = true;
+    //only do context dependent processing up to depth 8
+    bool doCD = nCurrCond<8;
     bool changed = false;
     std::vector< Node > children;
-    for( size_t i=0; i<body.getNumChildren(); i++ ){
-      std::vector< Node > new_cond;
+    //set entailed conditions based on OR/AND
+    std::map< int, std::vector< Node > > new_cond_children;
+    if( doCD && ( body.getKind()==OR || body.getKind()==AND ) ){
+      nCurrCond = nCurrCond + 1;
       bool conflict = false;
-      //only do context dependent processing up to depth 8
-      if( nCurrCond<8 ){
-        if( firstTimeCD ){
-          firstTimeCD = false;
-          nCurrCond = nCurrCond + 1;
-        }
-        if( Trace.isOn("quantifiers-rewrite-term-debug") ){
-          //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
-          if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){
-            Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl;
+      bool use_pol = body.getKind()==AND;
+      for( unsigned j=0; j<body.getNumChildren(); j++ ){
+        setEntailedCond( body[j], use_pol, currCond, new_cond_children[j], conflict );
+      }
+      if( conflict ){
+        Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl;
+        ret = NodeManager::currentNM()->mkConst( !use_pol );
+      }
+    }
+    if( ret.isNull() ){
+      for( size_t i=0; i<body.getNumChildren(); i++ ){
+      
+        //set/update entailed conditions
+        std::vector< Node > new_cond;
+        bool conflict = false;
+        if( doCD ){
+          if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+            if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){
+              Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl;
+            }
           }
-        }
-        if( body.getKind()==ITE && i>0 ){
-          setEntailedCond( children[0], i==1, currCond, new_cond, conflict );
-          //should not conflict (entailment check failed) 
-          Assert( !conflict );
-        }
-        //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){
-        //  bool use_pol = !pol;
-        if( body.getKind()==OR || body.getKind()==AND ){
-          bool use_pol = body.getKind()==AND;
-          for( unsigned j=0; j<body.getNumChildren(); j++ ){
-            if( j<i ){
-              setEntailedCond( children[j], use_pol, currCond, new_cond, conflict );
-            }else if( j>i ){
-              setEntailedCond( body[j], use_pol, currCond, new_cond, conflict );
+          if( body.getKind()==ITE && i>0 ){
+            if( i==1 ){
+              nCurrCond = nCurrCond + 1;
             }
+            setEntailedCond( children[0], i==1, currCond, new_cond, conflict );
+            //should not conflict (entailment check failed) 
+            Assert( !conflict );
           }
-          if( conflict ){
-            Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl;
-            ret = NodeManager::currentNM()->mkConst( !use_pol );
+          if( body.getKind()==OR || body.getKind()==AND ){
+            bool use_pol = body.getKind()==AND;
+            //remove the current condition
+            removeEntailedCond( currCond, new_cond_children[i], cache );
+            if( i>0 ){
+              //add the previous condition
+              setEntailedCond( children[i-1], use_pol, currCond, new_cond_children[i-1], conflict );
+            }
+            if( conflict ){
+              Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl;
+              ret = NodeManager::currentNM()->mkConst( !use_pol );
+            }
           }
-        }
-        if( !new_cond.empty() ){
-          cache.clear();
-        }
-        if( Trace.isOn("quantifiers-rewrite-term-debug") ){
-          //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
-          if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){      
-            Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl;
+          if( !new_cond.empty() ){
+            cache.clear();
+          }
+          if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+            if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){      
+              Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl;
+            }
           }
         }
-      }
-      if( !conflict ){
-        bool newHasPol;
-        bool newPol;
-        QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-        Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-        if( body.getKind()==ITE && i==0 ){
-          int res = getEntailedCond( nn, currCond );
-          Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl;
-          if( res==1 ){
-            ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-          }else if( res==-1 ){
-            ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+        
+        //do the recursive call on children
+        if( !conflict ){
+          bool newHasPol;
+          bool newPol;
+          QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+          Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+          if( body.getKind()==ITE && i==0 ){
+            int res = getEntailedCond( nn, currCond );
+            Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl;
+            if( res==1 ){
+              ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+            }else if( res==-1 ){
+              ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+            }
           }
+          children.push_back( nn );
+          changed = changed || nn!=body[i];
+        }
+        
+        //clean up entailed conditions
+        removeEntailedCond( currCond, new_cond, cache );
+        
+        if( !ret.isNull() ){
+          break;
         }
-        children.push_back( nn );
-        changed = changed || nn!=body[i];
       }
-      if( !new_cond.empty() ){
-        for( unsigned j=0; j<new_cond.size(); j++ ){
-          currCond.erase( new_cond[j] );
+      
+      //make return value
+      if( ret.isNull() ){
+        if( changed ){
+          if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+            children.insert( children.begin(), body.getOperator() );
+          }
+          ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+        }else{
+          ret = body;
         }
-        cache.clear();
-      }
-      if( !ret.isNull() ){
-        break;
       }
     }
-    if( ret.isNull() ){
-      if( changed ){
-        if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.insert( children.begin(), body.getOperator() );
-        }
-        ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
-      }else{
-        ret = body;
+    
+    //clean up entailed conditions
+    if( body.getKind()==OR || body.getKind()==AND ){
+      for( unsigned j=0; j<body.getNumChildren(); j++ ){
+        removeEntailedCond( currCond, new_cond_children[j], cache );
       }
     }
+    
     Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl;
     cache[body] = ret;
   }
 
+  //do context-independent rewriting
   iti = icache.find( ret );
   if( iti!=icache.end() ){
     return iti->second;
@@ -710,46 +744,60 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
           }
         }
       }
-    }else if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){
-      Node num = ret[0];
-      Node den = ret[1];
-      if(den.isConst()) {
-        const Rational& rat = den.getConst<Rational>();
-        Assert(!num.isConst());
-        if(rat != 0) {
-          Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-          new_vars.push_back( intVar );
-          Node cond;
-          if(rat > 0) {
-            cond = NodeManager::currentNM()->mkNode(kind::AND,
-                     NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num),
-                     NodeManager::currentNM()->mkNode(kind::LT, num,
-                       NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(1))))));
-          } else {
-            cond = NodeManager::currentNM()->mkNode(kind::AND,
-                     NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num),
-                     NodeManager::currentNM()->mkNode(kind::LT, num,
-                       NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(-1))))));
-          }
-          new_conds.push_back( cond.negate() );
-          if( ret.getKind()==INTS_DIVISION_TOTAL ){
-            ret = intVar;
-          }else{
-            ret = NodeManager::currentNM()->mkNode(kind::MINUS, num, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar));
+    /* ITE lifting
+    if( ret.getKind()==ITE ){
+      TypeNode ite_t = ret[1].getType();
+      if( !ite_t.isBoolean() ){
+        ite_t = TypeNode::leastCommonTypeNode( ite_t, ret[2].getType() );
+        Node ite_v = NodeManager::currentNM()->mkBoundVar(ite_t);
+        new_vars.push_back( ite_v );
+        Node cond = NodeManager::currentNM()->mkNode(kind::ITE, ret[0], ite_v.eqNode( ret[1] ), ite_v.eqNode( ret[2] ) );
+        new_conds.push_back( cond.negate() );
+        ret = ite_v;
+      }
+      */
+    }else if( options::elimExtArithQuant() ){
+      if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){
+        Node num = ret[0];
+        Node den = ret[1];
+        if(den.isConst()) {
+          const Rational& rat = den.getConst<Rational>();
+          Assert(!num.isConst());
+          if(rat != 0) {
+            Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+            new_vars.push_back( intVar );
+            Node cond;
+            if(rat > 0) {
+              cond = NodeManager::currentNM()->mkNode(kind::AND,
+                       NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num),
+                       NodeManager::currentNM()->mkNode(kind::LT, num,
+                         NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(1))))));
+            } else {
+              cond = NodeManager::currentNM()->mkNode(kind::AND,
+                       NodeManager::currentNM()->mkNode(kind::LEQ, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar), num),
+                       NodeManager::currentNM()->mkNode(kind::LT, num,
+                         NodeManager::currentNM()->mkNode(kind::MULT, den, NodeManager::currentNM()->mkNode(kind::PLUS, intVar, NodeManager::currentNM()->mkConst(Rational(-1))))));
+            }
+            new_conds.push_back( cond.negate() );
+            if( ret.getKind()==INTS_DIVISION_TOTAL ){
+              ret = intVar;
+            }else{
+              ret = NodeManager::currentNM()->mkNode(kind::MINUS, num, NodeManager::currentNM()->mkNode(kind::MULT, den, intVar));
+            }
           }
         }
-      }
-    }else if( ret.getKind()==TO_INTEGER || ret.getKind()==IS_INTEGER ){
-      Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-      new_vars.push_back( intVar );
-      new_conds.push_back(NodeManager::currentNM()->mkNode(kind::AND,
-                            NodeManager::currentNM()->mkNode(kind::LT,
-                              NodeManager::currentNM()->mkNode(kind::MINUS, ret[0], NodeManager::currentNM()->mkConst(Rational(1))), intVar),
-                            NodeManager::currentNM()->mkNode(kind::LEQ, intVar, ret[0])).negate());
-      if( ret.getKind()==TO_INTEGER ){
-        ret = intVar;
-      }else{
-        ret = ret[0].eqNode( intVar );
+      }else if( ret.getKind()==TO_INTEGER || ret.getKind()==IS_INTEGER ){
+        Node intVar = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+        new_vars.push_back( intVar );
+        new_conds.push_back(NodeManager::currentNM()->mkNode(kind::AND,
+                              NodeManager::currentNM()->mkNode(kind::LT,
+                                NodeManager::currentNM()->mkNode(kind::MINUS, ret[0], NodeManager::currentNM()->mkConst(Rational(1))), intVar),
+                              NodeManager::currentNM()->mkNode(kind::LEQ, intVar, ret[0])).negate());
+        if( ret.getKind()==TO_INTEGER ){
+          ret = intVar;
+        }else{
+          ret = ret[0].eqNode( intVar );
+        }
       }
     }
     icache[prev] = ret;
@@ -782,7 +830,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 +847,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;
@@ -932,8 +981,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
       newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
       std::vector< Node > newVars;
       for( unsigned j=0; j<c.getNumArgs(); j++ ){
-        TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
-        tn = tn[1];
+        TypeNode tn = TypeNode::fromType( c[j].getRangeType() );
         Node v = NodeManager::currentNM()->mkBoundVar( tn );
         newChildren.push_back( v );
         newVars.push_back( v );
@@ -957,7 +1005,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;
@@ -977,15 +1025,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() ){
@@ -995,7 +1043,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;
@@ -1290,13 +1338,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;
@@ -1304,14 +1352,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;
@@ -1319,26 +1367,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();
         }
@@ -1348,7 +1396,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;
@@ -1376,7 +1424,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;
         }
       }
@@ -1385,7 +1433,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 );
   //}
 }
 
@@ -1491,101 +1539,96 @@ 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 q, int computeOption, QAttributes& qa ){
+  bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST;
+  bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger;
   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();
+    return true;
   }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_strict_trigger;
   }else if( computeOption==COMPUTE_PRENEX ){
-    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
+    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std;
   }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 ){
-    return options::purifyQuant();
+    return options::purifyQuant() && is_std;
   }else{
     return false;
   }
 }
 
 //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() && args.size()==f[0].getNumChildren() ){
+        children.push_back( qa.d_ipl );
       }
+      return NodeManager::currentNM()->mkNode(kind::FORALL, children );
     }
-  }else{
-    return f;
   }
 }
 
@@ -1754,31 +1797,29 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     //check if it contains a quantifier as a subterm
     //if so, we will write this node
     if( containsQuantifiers( n ) ){
-      if( n.getType().isBoolean() ){
-        if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
-          if( options::preSkolemQuantAgg() ){
-            Node nn;
-            //must remove structure
-            if( n.getKind()==kind::ITE ){
-              nn = NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
-            }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
-              nn = NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
-            }else if( n.getKind()==kind::IMPLIES ){
-              nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
-            }
-            return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
-          }
-        }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
-          vector< Node > children;
-          for( int i=0; i<(int)n.getNumChildren(); i++ ){
-            children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
+      if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){
+        if( options::preSkolemQuantAgg() ){
+          Node nn;
+          //must remove structure
+          if( n.getKind()==kind::ITE ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+          }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+          }else if( n.getKind()==kind::IMPLIES ){
+            nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
           }
-          return NodeManager::currentNM()->mkNode( n.getKind(), children );
+          return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
         }
+      }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
+        vector< Node > children;
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
+        }
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
       }
     }
   }
@@ -1786,15 +1827,20 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
 }
 
 Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
+  Node prev = n;
   if( options::preSkolemQuant() ){
     if( !isInst || !options::preSkolemQuantNested() ){
-      //apply pre-skolemization to existential quantifiers
       Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
+      //apply pre-skolemization to existential quantifiers
       std::vector< TypeNode > fvTypes;
       std::vector< TNode > fvs;
-      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs );
+      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
     }
   }
+  if( n!=prev ){       
+    Trace("quantifiers-preprocess") << "Preprocess " << prev<< std::endl;
+    Trace("quantifiers-preprocess") << "..returned " << n << std::endl;
+  }
   return n;
 }
 
@@ -1886,7 +1932,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;