Decouple counter-example guided quantifier instantiation from Sygus.

8 files changed, 666 insertions, 477 deletions

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 3ddd5e157..0fef2aa42 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -31,395 +31,17 @@ using namespace CVC4::theory::quantifiers;
 using namespace std;
 
 namespace CVC4 {
-
-CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){
-  d_sol = NULL;
-  d_c_inst_match_trie = NULL;
-}
-
-Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
-  if( !d_single_inv.isNull() ) {
-    Assert( d_single_inv.getKind()==FORALL );
-    d_single_inv_var.clear();
-    d_single_inv_sk.clear();
-    for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
-      std::stringstream ss;
-      ss << "k_" << d_single_inv[0][i];
-      Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
-      d_single_inv_var.push_back( d_single_inv[0][i] );
-      d_single_inv_sk.push_back( k );
-      d_single_inv_sk_index[k] = i;
-    }
-    Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
-    inst = TermDb::simpleNegate( inst );
-    Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
-    return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
-  }else{
-    return Node::null();
-  }
-}
-
-void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
-  //initialize data
-  d_sol = new CegConjectureSingleInvSol( qe );
-  d_qe = qe;
-  d_quant = q;
-  if( options::incrementalSolving() ){
-    d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() );
-  }
-  //process
-  Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl;
-  // conj -> conj*
-  std::map< Node, std::vector< Node > > children;
-  // conj X prog -> inv*
-  std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke;
-  std::vector< Node > progs;
-  std::map< Node, std::map< Node, bool > > contains;
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    progs.push_back( q[0][i] );
-  }
-  //collect information about conjunctions
-  bool singleInvocation = false;
-  if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
-    singleInvocation = true;
-    //try to phrase as single invocation property
-    Trace("cegqi-si") << "...success." << std::endl;
-    std::map< Node, std::vector< Node > > invocations;
-    std::map< Node, std::map< int, std::vector< Node > > > single_invoke_args;
-    std::map< Node, std::map< int, std::map< Node, std::vector< Node > > > > single_invoke_args_from;
-    for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
-      for( unsigned j=0; j<it->second.size(); j++ ){
-        Node conj = it->second[j];
-        Trace("cegqi-si-debug") << "Process child " << conj << " from " << it->first << std::endl;
-        std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( conj );
-        if( itp!=prog_invoke.end() ){
-          for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
-            if( it2->second.size()>1 ){
-              singleInvocation = false;
-              break;
-            }else if( it2->second.size()==1 ){
-              Node prog = it2->first;
-              Node inv = it2->second[0];
-              Assert( inv[0]==prog );
-              invocations[prog].push_back( inv );
-              for( unsigned k=1; k<inv.getNumChildren(); k++ ){
-                Node arg = inv[k];
-                Trace("cegqi-si-debug") << "process : " << arg << " occurs in position " << k-1 << " in invocation " << inv << " of " << prog << " in " << conj << std::endl;
-                single_invoke_args_from[prog][k-1][arg].push_back( conj );
-                if( std::find( single_invoke_args[prog][k-1].begin(), single_invoke_args[prog][k-1].end(), arg )==single_invoke_args[prog][k-1].end() ){
-                  single_invoke_args[prog][k-1].push_back( arg );
-                }
-              }
-            }
-          }
-        }
-      }
-    }
-    if( singleInvocation ){
-      Trace("cegqi-si") << "Property is single invocation with : " << std::endl;
-      std::vector< Node > pbvs;
-      std::vector< Node > new_vars;
-      std::map< Node, std::vector< Node > > new_assumptions;
-      for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){
-        Assert( !it->second.empty() );
-        Node prog = it->first;
-        Node inv = it->second[0];
-        std::vector< Node > invc;
-        invc.push_back( inv.getOperator() );
-        invc.push_back( prog );
-        std::stringstream ss;
-        ss << "F_" << prog;
-        Node pv = NodeManager::currentNM()->mkBoundVar( ss.str(), inv.getType() );
-        d_single_inv_map[prog] = pv;
-        d_single_inv_map_to_prog[pv] = prog;
-        pbvs.push_back( pv );
-        Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl;
-        for( unsigned k=1; k<inv.getNumChildren(); k++ ){
-          Assert( !single_invoke_args[prog][k-1].empty() );
-          if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){
-            invc.push_back( single_invoke_args[prog][k-1][0] );
-          }else{
-            //introduce fresh variable, assign all
-            Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" );
-            new_vars.push_back( v );
-            invc.push_back( v );
-            d_single_inv_arg_sk.push_back( v );
-
-            for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){
-              Node arg = single_invoke_args[prog][k-1][i];
-              Node asum = NodeManager::currentNM()->mkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate();
-              Trace("cegqi-si-debug") << "  ..." << arg << " occurs in ";
-              Trace("cegqi-si-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl;
-              for( unsigned j=0; j<single_invoke_args_from[prog][k-1][arg].size(); j++ ){
-                Node conj = single_invoke_args_from[prog][k-1][arg][j];
-                Trace("cegqi-si-debug") << "  ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl;
-                Trace("cegqi-si-debug") << "  ...add assumption " << asum << " to " << conj << std::endl;
-                if( std::find( new_assumptions[conj].begin(), new_assumptions[conj].end(), asum )==new_assumptions[conj].end() ){
-                  new_assumptions[conj].push_back( asum );
-                }
-              }
-            }
-          }
-        }
-        Node sinv = NodeManager::currentNM()->mkNode( APPLY_UF, invc );
-        Trace("cegqi-si") << "  " << prog << " -> " << sinv << std::endl;
-        d_single_inv_app_map[prog] = sinv;
-      }
-      //construct the single invocation version of the property
-      Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
-      //std::vector< Node > si_conj;
-      Assert( !pbvs.empty() );
-      Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
-      for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
-        //should hold since we prevent miniscoping
-        Assert( d_single_inv.isNull() );
-        std::vector< Node > conjuncts;
-        for( unsigned i=0; i<it->second.size(); i++ ){
-          Node c = it->second[i];
-          std::vector< Node > disj;
-          //insert new assumptions
-          disj.insert( disj.end(), new_assumptions[c].begin(), new_assumptions[c].end() );
-          //get replaced version
-          Node cr;
-          std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c );
-          if( itp!=prog_invoke.end() ){
-            std::vector< Node > terms;
-            std::vector< Node > subs;
-            for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
-              if( !it2->second.empty() ){
-                Node prog = it2->first;
-                Node inv = it2->second[0];
-                Assert( it2->second.size()==1 );
-                terms.push_back( inv );
-                subs.push_back( d_single_inv_map[prog] );
-                Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl;
-              }
-            }
-            cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
-          }else{
-            cr = c;
-          }
-          if( cr.getKind()==OR ){
-            for( unsigned j=0; j<cr.getNumChildren(); j++ ){
-              disj.push_back( cr[j] );
-            }
-          }else{
-            disj.push_back( cr );
-          }
-          Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
-          curr = TermDb::simpleNegate( curr );
-          Trace("cegqi-si") << "    " << curr;
-          conjuncts.push_back( curr );
-          if( !it->first.isNull() ){
-            Trace("cegqi-si-debug") << " under " << it->first;
-          }
-          Trace("cegqi-si") << std::endl;
-        }
-        Assert( !conjuncts.empty() );
-        //make the skolems for the existential
-        if( !it->first.isNull() ){
-          std::vector< Node > vars;
-          std::vector< Node > sks;
-          for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
-            std::stringstream ss;
-            ss << "a_" << it->first[j];
-            Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
-            vars.push_back( it->first[j] );
-            sks.push_back( v );
-          }
-          //substitute conjunctions
-          for( unsigned i=0; i<conjuncts.size(); i++ ){
-            conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
-          }
-          d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() );
-          //substitute single invocation applications
-          for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
-            Node n = itam->second;
-            d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
-          }
-        }
-        //ensure that this is a ground property
-        for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
-          Node n = itam->second;
-          //check if all variables are arguments of this
-          std::vector< Node > n_args;
-          for( unsigned i=1; i<n.getNumChildren(); i++ ){
-            n_args.push_back( n[i] );
-          }
-          for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){
-            if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){
-              Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl;
-              //try to do variable elimination on d_single_inv_arg_sk[i]
-              if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){
-                Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl;
-                d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 );
-                i--;
-              }else{
-                singleInvocation = false;
-                //exit( 57 );
-              }
-              break;
-            }
-          }
-        }
-
-        if( singleInvocation ){
-          Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
-          d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
-          Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
-          if( options::eMatching.wasSetByUser() ){
-            Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
-            std::vector< Node > patTerms;
-            std::vector< Node > exclude;
-            inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
-            if( !patTerms.empty() ){
-              Trace("cegqi-si-em") << "Triggers : " << std::endl;
-              for( unsigned i=0; i<patTerms.size(); i++ ){
-                Trace("cegqi-si-em") << "   " << patTerms[i] << std::endl;
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-  if( !singleInvocation ){
-    Trace("cegqi-si") << "Property is not single invocation." << std::endl;
-    if( options::cegqiSingleInvAbort() ){
-      Message() << "Property is not single invocation." << std::endl;
-      exit( 0 );
-    }
-  }
-}
-
-bool CegConjectureSingleInv::doVariableElimination( Node v, std::vector< Node >& conjuncts ) {
-  //all conjuncts containing v must contain a literal v != s for some s
-  // if so, do DER on all such conjuncts
-  TNode s;
-  for( unsigned i=0; i<conjuncts.size(); i++ ){
-    int status = 0;
-    if( getVariableEliminationTerm( true, true, v, conjuncts[i], s, status ) ){
-      Trace("cegqi-si-debug") << "Substitute " << s << " for " << v << " in " << conjuncts[i] << std::endl;
-      Assert( !s.isNull() );
-      conjuncts[i] = conjuncts[i].substitute( v, s );
-    }else{
-      if( status==1 ){
-        Trace("cegqi-si-debug") << "Conjunct " << conjuncts[i] << " contains " << v << " but not in disequality." << std::endl;
-        return false;
-      }else{
-        Trace("cegqi-si-debug") << "Conjunct does not contain " << v << "." << std::endl;
-      }
-    }
-  }
-  return true;
-}
-
-bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, Node v, Node n, TNode& s, int& status ) {
-  if( hasPol ){
-    if( n.getKind()==NOT ){
-      return getVariableEliminationTerm( !pol, true, v, n[0], s, status );
-    }else if( pol && n.getKind()==EQUAL ){
-      for( unsigned r=0; r<2; r++ ){
-        if( n[r]==v ){
-          status = 1;
-          Node ss = n[r==0 ? 1 : 0];
-          if( s.isNull() ){
-            s = ss;
-          }
-          return ss==s;
-        }
-      }
-      //did not match, now see if it contains v
-    }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( getVariableEliminationTerm( pol, true, v, n[i], s, status ) ){
-          return true;
-        }
-      }
-      return false;
-    }
-  }
-  if( n==v ){
-    status = 1;
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      getVariableEliminationTerm( pol, false, v, n[i], s, status );
-    }
-  }
-  return false;
-}
-
-bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
-                                                            std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
-                                                            std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
-  if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){
-        return false;
-      }
-    }
-  }else if( pol && n.getKind()==NOT && n[0].getKind()==FORALL ){
-    if( !p.isNull() ){
-      //do not allow nested quantifiers
-      return false;
-    }
-    analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false );
-  }else{
-    if( pol ){
-      n = TermDb::simpleNegate( n );
-    }
-    Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl;
-    children[p].push_back( n );
-    for( unsigned i=0; i<progs.size(); i++ ){
-      prog_invoke[n][progs[i]].clear();
-    }
-    bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] );
-    for( unsigned i=0; i<progs.size(); i++ ){
-      std::map< Node, std::vector< Node > >::iterator it = prog_invoke[n].find( progs[i] );
-      Trace("cegqi-si") << "  Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl;
-      for( unsigned j=0; j<it->second.size(); j++ ){
-        Trace("cegqi-si") << "    " << it->second[j] << std::endl;
-      }
-    }
-    return success;
-  }
-  return true;
-}
-
-bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ) {
-  if( n.getNumChildren()>0 ){
-    if( n.getKind()==FORALL ){
-      //do not allow nested quantifiers
-      return false;
-    }
-    //look at first argument in evaluator
-    Node p = n[0];
-    std::map< Node, std::vector< Node > >::iterator it = prog_invoke.find( p );
-    if( it!=prog_invoke.end() ){
-      if( std::find( it->second.begin(), it->second.end(), n )==it->second.end() ){
-        it->second.push_back( n );
-      }
-    }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !analyzeSygusTerm( n[i], prog_invoke, contains ) ){
-        return false;
-      }
-    }
-  }else{
-    //record this conjunct contains n
-    contains[n] = true;
-  }
-  return true;
-}
-
-
-
-void CegConjectureSingleInv::computeProgVars( Node n ){
+  
+CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){
+  
+}  
+  
+void CegInstantiator::computeProgVars( Node n ){
   if( d_prog_var.find( n )==d_prog_var.end() ){
     d_prog_var[n].clear();
-    if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
+    if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){
       d_prog_var[n][n] = true;
-    }else if( n.getKind()==SKOLEM && std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )==d_single_inv_arg_sk.end() ){
+    }else if( !d_out->isEligibleForInstantiation( n ) ){
       d_inelig[n] = true;
       return;
     }
@@ -436,19 +58,19 @@ void CegConjectureSingleInv::computeProgVars( Node n ){
   }
 }
 
-bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, 
-                                               std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
-                                               unsigned i, std::vector< Node >& lems, unsigned effort ){
-  if( i==d_single_inv_sk.size() ){
-    return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0, lems );
+bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, 
+                                        std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
+                                        unsigned i, unsigned effort ){
+  if( i==d_vars.size() ){
+    return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0 );
   }else{
     eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
     std::map< int, std::map< Node, std::map< Node, bool > > > subs_proc;
-    Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
-    Node pv = d_single_inv_sk[i];
+    //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
+    Node pv = d_vars[i];
     TypeNode pvtn = pv.getType();
     
-    if( (i+1)<d_single_inv_arg_sk.size() || effort!=2 ){
+    if( (i+1)<d_vars.size() || effort!=2 ){
       //[1] easy case : pv is in the equivalence class as another term not containing pv
       if( ee->hasTerm( pv ) ){
         Node pvr = ee->getRepresentative( pv );
@@ -478,7 +100,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v
               if( proc ){
                 //try the substitution
                 subs_proc[0][ns][pv_coeff] = true;
-                if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){
+                if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){
                   return true;
                 }
               }
@@ -558,7 +180,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v
                           }
                           if( subs_proc[0][veq[1]].find( veq_c )==subs_proc[0][veq[1]].end() ){
                             subs_proc[0][veq[1]][veq_c] = true;
-                            if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){
+                            if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){
                               return true;
                             }
                           }
@@ -670,7 +292,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v
                         }
                         if( subs_proc[uires][uval].find( veq_c )==subs_proc[uires][uval].end() ){
                           subs_proc[uires][uval][veq_c] = true;
-                          if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){
+                          if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){
                             return true;
                           }
                         }
@@ -690,7 +312,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v
       Node mv = d_qe->getModel()->getValue( pv );
       Node pv_coeff_m;
       Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl;
-      return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, lems, 1 );
+      return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 );
     }else{
       return false;
     }
@@ -698,9 +320,9 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v
 }
 
 
-bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, 
-                                                  std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
-                                                  unsigned i, std::vector< Node >& lems, unsigned effort ) {         
+bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, 
+                                           std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
+                                           unsigned i, unsigned effort ) {         
   //must ensure variables have been computed for n
   computeProgVars( n );
   //substitute into previous substitutions, when applicable
@@ -763,7 +385,7 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff
       Trace("cegqi-si-inst-debug") << pv_coeff << "*";
     }
     Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl;
-    success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, lems, effort );
+    success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, effort );
     if( !success ){
       subs.pop_back();
       vars.pop_back();
@@ -791,11 +413,10 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff
   }
 }
 
-bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, 
-                                                    std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
-                                                    unsigned j, std::vector< Node >& lems ) {
+bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, 
+                                             std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ) {
   if( j==has_coeff.size() ){
-    return addInstantiation( subs, vars, subs_typ, lems );
+    return addInstantiation( subs, vars, subs_typ );
   }else{
     Assert( std::find( vars.begin(), vars.end(), has_coeff[j] )!=vars.end() );
     unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin();
@@ -836,7 +457,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s
             }
           }
           Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl;
-          if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){
+          if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){
             return true;
           }
             //equalities are both upper and lower bounds
@@ -850,7 +471,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s
                   NodeManager::currentNM()->mkConst( Rational( 0 ) ),
                   NodeManager::currentNM()->mkConst( Rational( 1 ) ) )
               );
-              if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){
+              if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){
                 return true;
               }
             }
@@ -862,7 +483,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s
       subs[index] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst<Rational>() ), subs[index] );
       subs[index] = Rewriter::rewrite( subs[index] );
       Trace("cegqi-si-inst-debug") << "...success, reals : " << subs[index] << std::endl;
-      if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){
+      if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){
         return true;
       }
     }else{
@@ -874,7 +495,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s
   }
 }
 
-bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ, std::vector< Node >& lems ) {
+bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ) {
   // do delta rationals
   std::map< int, Node > prev;
   for( unsigned i=0; i<subs.size(); i++ ){
@@ -888,46 +509,19 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v
       subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta );
     }
   }
-  std::stringstream siss;
-  siss << "  * single invocation: " << std::endl;
-  for( unsigned j=0; j<vars.size(); j++ ){
-    Node v = d_single_inv_map_to_prog[d_single_inv[0][j]];
-    siss << "    * " << v;
-    siss << " (" << vars[j] << ")";
-    siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl;
-  }
   //check if we have already added this instantiation
-  bool alreadyExists;
-  if( options::incrementalSolving() ){
-    alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() );
-  }else{
-    alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs );
-  }
-  Trace("cegqi-si-inst-debug") << siss.str();
-  Trace("cegqi-si-inst-debug") << "  * success = " << !alreadyExists << std::endl;
-  if( alreadyExists ){
+  bool success = d_out->addInstantiation( subs, subs_typ );
+  if( !success ){
     //revert the substitution
     for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){
       subs[it->first] = it->second;
     }
-    return false;
-  }else{
-    Trace("cegqi-engine") << siss.str() << std::endl;
-    Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
-    lem = Rewriter::rewrite( lem );
-    Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
-    if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){
-      lems.push_back( lem );
-      d_lemmas_produced.push_back( lem );
-      d_inst.push_back( std::vector< Node >() );
-      d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() );
-    }
-    return true;
   }
+  return success;
 }
 
 
-Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, 
+Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, 
                                                 std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) {
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   Assert( n==Rewriter::rewrite( n ) );
@@ -1009,20 +603,467 @@ Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& sub
   }
 }
 
-void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
+void CegInstantiator::check() {
+  for( unsigned r=0; r<2; r++ ){
+    std::vector< Node > subs;
+    std::vector< Node > vars;
+    std::vector< Node > coeff;
+    std::vector< Node > has_coeff;
+    std::vector< int > subs_typ;
+    //try to add an instantiation
+    if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){
+      return;
+    }
+  }
+  Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+}
+  
+  
+bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
+  return d_out->addInstantiation( subs, subs_typ );
+}
+  
+bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) {
+  return d_out->isEligibleForInstantiation( n );
+}  
+  
+  
+  
+CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){
+  d_sol = NULL;
+  d_c_inst_match_trie = NULL;
+  d_cinst = NULL;
+}
+
+Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
   if( !d_single_inv.isNull() ) {
-    for( unsigned r=0; r<2; r++ ){
-      std::vector< Node > subs;
-      std::vector< Node > vars;
-      std::vector< Node > coeff;
-      std::vector< Node > has_coeff;
-      std::vector< int > subs_typ;
-      //try to add an instantiation
-      if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, lems, r==0 ? 0 : 2 ) ){
-        return;
+    Assert( d_single_inv.getKind()==FORALL );
+    d_single_inv_var.clear();
+    d_single_inv_sk.clear();
+    for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+      std::stringstream ss;
+      ss << "k_" << d_single_inv[0][i];
+      Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
+      d_single_inv_var.push_back( d_single_inv[0][i] );
+      d_single_inv_sk.push_back( k );
+      d_single_inv_sk_index[k] = i;
+    }
+    Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    inst = TermDb::simpleNegate( inst );
+    Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
+    
+    //initialize the instantiator for this
+    CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
+    d_cinst = new CegInstantiator( d_qe, cosi );
+    d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    
+    return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
+  }else{
+    return Node::null();
+  }
+}
+
+void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
+  //initialize data
+  d_sol = new CegConjectureSingleInvSol( qe );
+  d_qe = qe;
+  d_quant = q;
+  if( options::incrementalSolving() ){
+    d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() );
+  }
+  //process
+  Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl;
+  // conj -> conj*
+  std::map< Node, std::vector< Node > > children;
+  // conj X prog -> inv*
+  std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke;
+  std::vector< Node > progs;
+  std::map< Node, std::map< Node, bool > > contains;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    progs.push_back( q[0][i] );
+  }
+  //collect information about conjunctions
+  bool singleInvocation = false;
+  if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
+    singleInvocation = true;
+    //try to phrase as single invocation property
+    Trace("cegqi-si") << "...success." << std::endl;
+    std::map< Node, std::vector< Node > > invocations;
+    std::map< Node, std::map< int, std::vector< Node > > > single_invoke_args;
+    std::map< Node, std::map< int, std::map< Node, std::vector< Node > > > > single_invoke_args_from;
+    for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
+      for( unsigned j=0; j<it->second.size(); j++ ){
+        Node conj = it->second[j];
+        Trace("cegqi-si-debug") << "Process child " << conj << " from " << it->first << std::endl;
+        std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( conj );
+        if( itp!=prog_invoke.end() ){
+          for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
+            if( it2->second.size()>1 ){
+              singleInvocation = false;
+              break;
+            }else if( it2->second.size()==1 ){
+              Node prog = it2->first;
+              Node inv = it2->second[0];
+              Assert( inv[0]==prog );
+              invocations[prog].push_back( inv );
+              for( unsigned k=1; k<inv.getNumChildren(); k++ ){
+                Node arg = inv[k];
+                Trace("cegqi-si-debug") << "process : " << arg << " occurs in position " << k-1 << " in invocation " << inv << " of " << prog << " in " << conj << std::endl;
+                single_invoke_args_from[prog][k-1][arg].push_back( conj );
+                if( std::find( single_invoke_args[prog][k-1].begin(), single_invoke_args[prog][k-1].end(), arg )==single_invoke_args[prog][k-1].end() ){
+                  single_invoke_args[prog][k-1].push_back( arg );
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+    if( singleInvocation ){
+      Trace("cegqi-si") << "Property is single invocation with : " << std::endl;
+      std::vector< Node > pbvs;
+      std::vector< Node > new_vars;
+      std::map< Node, std::vector< Node > > new_assumptions;
+      for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){
+        Assert( !it->second.empty() );
+        Node prog = it->first;
+        Node inv = it->second[0];
+        std::vector< Node > invc;
+        invc.push_back( inv.getOperator() );
+        invc.push_back( prog );
+        std::stringstream ss;
+        ss << "F_" << prog;
+        Node pv = NodeManager::currentNM()->mkBoundVar( ss.str(), inv.getType() );
+        d_single_inv_map[prog] = pv;
+        d_single_inv_map_to_prog[pv] = prog;
+        pbvs.push_back( pv );
+        Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl;
+        for( unsigned k=1; k<inv.getNumChildren(); k++ ){
+          Assert( !single_invoke_args[prog][k-1].empty() );
+          if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){
+            invc.push_back( single_invoke_args[prog][k-1][0] );
+          }else{
+            //introduce fresh variable, assign all
+            Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" );
+            new_vars.push_back( v );
+            invc.push_back( v );
+            d_single_inv_arg_sk.push_back( v );
+
+            for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){
+              Node arg = single_invoke_args[prog][k-1][i];
+              Node asum = NodeManager::currentNM()->mkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate();
+              Trace("cegqi-si-debug") << "  ..." << arg << " occurs in ";
+              Trace("cegqi-si-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl;
+              for( unsigned j=0; j<single_invoke_args_from[prog][k-1][arg].size(); j++ ){
+                Node conj = single_invoke_args_from[prog][k-1][arg][j];
+                Trace("cegqi-si-debug") << "  ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl;
+                Trace("cegqi-si-debug") << "  ...add assumption " << asum << " to " << conj << std::endl;
+                if( std::find( new_assumptions[conj].begin(), new_assumptions[conj].end(), asum )==new_assumptions[conj].end() ){
+                  new_assumptions[conj].push_back( asum );
+                }
+              }
+            }
+          }
+        }
+        Node sinv = NodeManager::currentNM()->mkNode( APPLY_UF, invc );
+        Trace("cegqi-si") << "  " << prog << " -> " << sinv << std::endl;
+        d_single_inv_app_map[prog] = sinv;
+      }
+      //construct the single invocation version of the property
+      Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
+      //std::vector< Node > si_conj;
+      Assert( !pbvs.empty() );
+      Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+      for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
+        //should hold since we prevent miniscoping
+        Assert( d_single_inv.isNull() );
+        std::vector< Node > conjuncts;
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          Node c = it->second[i];
+          std::vector< Node > disj;
+          //insert new assumptions
+          disj.insert( disj.end(), new_assumptions[c].begin(), new_assumptions[c].end() );
+          //get replaced version
+          Node cr;
+          std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c );
+          if( itp!=prog_invoke.end() ){
+            std::vector< Node > terms;
+            std::vector< Node > subs;
+            for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
+              if( !it2->second.empty() ){
+                Node prog = it2->first;
+                Node inv = it2->second[0];
+                Assert( it2->second.size()==1 );
+                terms.push_back( inv );
+                subs.push_back( d_single_inv_map[prog] );
+                Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl;
+              }
+            }
+            cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+          }else{
+            cr = c;
+          }
+          if( cr.getKind()==OR ){
+            for( unsigned j=0; j<cr.getNumChildren(); j++ ){
+              disj.push_back( cr[j] );
+            }
+          }else{
+            disj.push_back( cr );
+          }
+          Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
+          curr = TermDb::simpleNegate( curr );
+          Trace("cegqi-si") << "    " << curr;
+          conjuncts.push_back( curr );
+          if( !it->first.isNull() ){
+            Trace("cegqi-si-debug") << " under " << it->first;
+          }
+          Trace("cegqi-si") << std::endl;
+        }
+        Assert( !conjuncts.empty() );
+        //make the skolems for the existential
+        if( !it->first.isNull() ){
+          std::vector< Node > vars;
+          std::vector< Node > sks;
+          for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
+            std::stringstream ss;
+            ss << "a_" << it->first[j];
+            Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
+            vars.push_back( it->first[j] );
+            sks.push_back( v );
+          }
+          //substitute conjunctions
+          for( unsigned i=0; i<conjuncts.size(); i++ ){
+            conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+          }
+          d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() );
+          //substitute single invocation applications
+          for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
+            Node n = itam->second;
+            d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+          }
+        }
+        //ensure that this is a ground property
+        for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
+          Node n = itam->second;
+          //check if all variables are arguments of this
+          std::vector< Node > n_args;
+          for( unsigned i=1; i<n.getNumChildren(); i++ ){
+            n_args.push_back( n[i] );
+          }
+          for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){
+            if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){
+              Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl;
+              //try to do variable elimination on d_single_inv_arg_sk[i]
+              if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){
+                Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl;
+                d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 );
+                i--;
+              }else{
+                singleInvocation = false;
+                //exit( 57 );
+              }
+              break;
+            }
+          }
+        }
+
+        if( singleInvocation ){
+          Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
+          d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+          Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
+          if( options::eMatching.wasSetByUser() ){
+            Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
+            std::vector< Node > patTerms;
+            std::vector< Node > exclude;
+            inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
+            if( !patTerms.empty() ){
+              Trace("cegqi-si-em") << "Triggers : " << std::endl;
+              for( unsigned i=0; i<patTerms.size(); i++ ){
+                Trace("cegqi-si-em") << "   " << patTerms[i] << std::endl;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  if( !singleInvocation ){
+    Trace("cegqi-si") << "Property is not single invocation." << std::endl;
+    if( options::cegqiSingleInvAbort() ){
+      Message() << "Property is not single invocation." << std::endl;
+      exit( 0 );
+    }
+  }
+}
+
+bool CegConjectureSingleInv::doVariableElimination( Node v, std::vector< Node >& conjuncts ) {
+  //all conjuncts containing v must contain a literal v != s for some s
+  // if so, do DER on all such conjuncts
+  TNode s;
+  for( unsigned i=0; i<conjuncts.size(); i++ ){
+    int status = 0;
+    if( getVariableEliminationTerm( true, true, v, conjuncts[i], s, status ) ){
+      Trace("cegqi-si-debug") << "Substitute " << s << " for " << v << " in " << conjuncts[i] << std::endl;
+      Assert( !s.isNull() );
+      conjuncts[i] = conjuncts[i].substitute( v, s );
+    }else{
+      if( status==1 ){
+        Trace("cegqi-si-debug") << "Conjunct " << conjuncts[i] << " contains " << v << " but not in disequality." << std::endl;
+        return false;
+      }else{
+        Trace("cegqi-si-debug") << "Conjunct does not contain " << v << "." << std::endl;
+      }
+    }
+  }
+  return true;
+}
+
+bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, Node v, Node n, TNode& s, int& status ) {
+  if( hasPol ){
+    if( n.getKind()==NOT ){
+      return getVariableEliminationTerm( !pol, true, v, n[0], s, status );
+    }else if( pol && n.getKind()==EQUAL ){
+      for( unsigned r=0; r<2; r++ ){
+        if( n[r]==v ){
+          status = 1;
+          Node ss = n[r==0 ? 1 : 0];
+          if( s.isNull() ){
+            s = ss;
+          }
+          return ss==s;
+        }
+      }
+      //did not match, now see if it contains v
+    }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( getVariableEliminationTerm( pol, true, v, n[i], s, status ) ){
+          return true;
+        }
+      }
+      return false;
+    }
+  }
+  if( n==v ){
+    status = 1;
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      getVariableEliminationTerm( pol, false, v, n[i], s, status );
+    }
+  }
+  return false;
+}
+
+bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
+                                                            std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
+                                                            std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
+  if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){
+        return false;
+      }
+    }
+  }else if( pol && n.getKind()==NOT && n[0].getKind()==FORALL ){
+    if( !p.isNull() ){
+      //do not allow nested quantifiers
+      return false;
+    }
+    analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false );
+  }else{
+    if( pol ){
+      n = TermDb::simpleNegate( n );
+    }
+    Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl;
+    children[p].push_back( n );
+    for( unsigned i=0; i<progs.size(); i++ ){
+      prog_invoke[n][progs[i]].clear();
+    }
+    bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] );
+    for( unsigned i=0; i<progs.size(); i++ ){
+      std::map< Node, std::vector< Node > >::iterator it = prog_invoke[n].find( progs[i] );
+      Trace("cegqi-si") << "  Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl;
+      for( unsigned j=0; j<it->second.size(); j++ ){
+        Trace("cegqi-si") << "    " << it->second[j] << std::endl;
+      }
+    }
+    return success;
+  }
+  return true;
+}
+
+bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ) {
+  if( n.getNumChildren()>0 ){
+    if( n.getKind()==FORALL ){
+      //do not allow nested quantifiers
+      return false;
+    }
+    //look at first argument in evaluator
+    Node p = n[0];
+    std::map< Node, std::vector< Node > >::iterator it = prog_invoke.find( p );
+    if( it!=prog_invoke.end() ){
+      if( std::find( it->second.begin(), it->second.end(), n )==it->second.end() ){
+        it->second.push_back( n );
+      }
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !analyzeSygusTerm( n[i], prog_invoke, contains ) ){
+        return false;
       }
     }
-    Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+  }else{
+    //record this conjunct contains n
+    contains[n] = true;
+  }
+  return true;
+}
+
+bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ){
+  std::stringstream siss;
+  if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
+    siss << "  * single invocation: " << std::endl;
+    for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
+      Node v = d_single_inv_map_to_prog[d_single_inv[0][j]];
+      siss << "    * " << v;
+      siss << " (" << d_single_inv_sk[j] << ")";
+      siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl;
+    }
+  }
+  bool alreadyExists;
+  if( options::incrementalSolving() ){
+    alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() );
+  }else{
+    alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs );
+  }
+  Trace("cegqi-si-inst-debug") << siss.str();
+  Trace("cegqi-si-inst-debug") << "  * success = " << !alreadyExists << std::endl;
+  if( alreadyExists ){
+    return false;
+  }else{
+    Trace("cegqi-engine") << siss.str() << std::endl;
+    Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
+    lem = Rewriter::rewrite( lem );
+    Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
+    if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){
+      d_curr_lemmas.push_back( lem );
+      d_lemmas_produced.push_back( lem );
+      d_inst.push_back( std::vector< Node >() );
+      d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() );
+    }
+    return true;
+  }
+}
+
+bool CegConjectureSingleInv::isEligibleForInstantiation( Node n ) {
+  return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end();
+}
+
+void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
+  if( !d_single_inv.isNull() ) {
+    Assert( d_cinst!=NULL );
+    d_curr_lemmas.clear();
+    //call check for instantiator
+    d_cinst->check();
+    //add lemmas
+    lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 3bc870d78..9e65b0c24 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -28,12 +28,68 @@ namespace quantifiers {
 
 class CegConjecture;
 
+class CegqiOutput
+{
+public:
+  virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0;
+  virtual bool isEligibleForInstantiation( Node n ) = 0;
+};
+
+class CegInstantiator
+{
+private:
+  QuantifiersEngine * d_qe;
+  CegqiOutput * d_out;
+  //program variable contains cache
+  std::map< Node, std::map< Node, bool > > d_prog_var;
+  std::map< Node, bool > d_inelig;
+private:
+  Node d_n_delta;
+  //for adding instantiations during check
+  void computeProgVars( Node n );
+  // effort=0 : do not use model value, 1: use model value, 2: one must use model value
+  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, 
+                         std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
+                         unsigned i, unsigned effort );
+  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, 
+                            std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
+                            unsigned i, unsigned effort );
+  bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, 
+                              std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
+                              unsigned j );
+  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ );
+  Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, 
+                          std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); 
+public:
+  CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out );
+  //the CE variables
+  std::vector< Node > d_vars;
+  void check();
+};
+
+
+class CegConjectureSingleInv;
+
+class CegqiOutputSingleInv : public CegqiOutput
+{
+public:
+  CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
+  CegConjectureSingleInv * d_out;
+  bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
+  bool isEligibleForInstantiation( Node n );
+};
+
+
+
 class CegConjectureSingleInv
 {
+  friend class CegqiOutputSingleInv;
 private:
   QuantifiersEngine * d_qe;
   CegConjecture * d_parent;
   CegConjectureSingleInvSol * d_sol;
+  //the instantiator
+  CegInstantiator * d_cinst;
   //for recognizing when conjecture is single invocation
   bool analyzeSygusConjunct( Node n, Node p, std::map< Node, std::vector< Node > >& children,
                             std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
@@ -67,26 +123,12 @@ private:
   Node d_orig_solution;
   Node d_solution;
   Node d_sygus_solution;
-  //program variable contains cache
-  std::map< Node, std::map< Node, bool > > d_prog_var;
-  std::map< Node, bool > d_inelig;
 private:
-  Node d_n_delta;
-  //for adding instantiations during check
-  void computeProgVars( Node n );
-  // effort=0 : do not use model value, 1: use model value, 2: one must use model value
-  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, 
-                         std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
-                         unsigned i, std::vector< Node >& lems, unsigned effort );
-  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, 
-                            std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
-                            unsigned i, std::vector< Node >& lems, unsigned effort );
-  bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, 
-                              std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
-                              unsigned j, std::vector< Node >& lems );
-  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ, std::vector< Node >& lems );
-  Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, 
-                          std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); 
+  std::vector< Node > d_curr_lemmas;
+  //add instantiation
+  bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
+  //is eligible for instantiation
+  bool isEligibleForInstantiation( Node n );
 public:
   CegConjectureSingleInv( CegConjecture * p );
   // original conjecture
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index c205a280e..fe992b619 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -346,3 +346,67 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
   Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
   return mkRationalNode(qmodel);
 }
+
+
+
+bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
+  return d_out->addInstantiation( subs, subs_typ );
+}
+
+bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) {
+  return d_out->isEligibleForInstantiation( n );
+}
+
+
+InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) {
+  d_out = new CegqiOutputInstStrategy( this );
+}
+
+void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
+  
+}
+
+int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
+  if( e<2 ){
+    return STATUS_UNFINISHED;
+  }else if( e==2 ){
+    CegInstantiator * cinst;
+    std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
+    if( it==d_cinst.end() ){
+      cinst = new CegInstantiator( d_quantEngine, d_out );
+      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+        cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
+      }
+      d_cinst[f] = cinst;
+    }else{
+      cinst = it->second;
+    }
+    d_curr_quant = f;
+    cinst->check();
+    d_curr_quant = Node::null();
+    
+    return STATUS_UNKNOWN;
+  }
+}
+
+bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
+  Assert( !d_curr_quant.isNull() );
+  return d_quantEngine->addInstantiation( d_curr_quant, subs, false );
+}
+
+bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
+  return true;
+} 
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 72ab5d247..e139d0b6f 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -22,6 +22,7 @@
 #include "theory/arith/arithvar.h"
 
 #include "util/statistics_registry.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
 
 namespace CVC4 {
 namespace theory {
@@ -80,6 +81,37 @@ public:
 };
 
 
+//generalized counterexample guided quantifier instantiation
+
+class InstStrategyCegqi;
+
+class CegqiOutputInstStrategy : public CegqiOutput
+{
+public:
+  CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
+  InstStrategyCegqi * d_out;
+  bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
+  bool isEligibleForInstantiation( Node n );
+};
+
+class InstStrategyCegqi : public InstStrategy {
+private:
+  CegqiOutputInstStrategy * d_out;
+  std::map< Node, CegInstantiator * > d_cinst;
+  Node d_curr_quant;
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e );
+public:
+  InstStrategyCegqi( QuantifiersEngine * qe );
+  ~InstStrategyCegqi(){}
+  
+  bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
+  bool isEligibleForInstantiation( Node n );  
+  /** identify */
+  std::string identify() const { return std::string("Cegqi"); }
+};
+
 }
 }
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 52139a0b8..9c3035c85 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,7 +31,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ), d_setIncomplete( setIncomplete ){
 
 }
 
@@ -41,6 +41,7 @@ InstantiationEngine::~InstantiationEngine() {
   delete d_i_lte;
   delete d_i_fs;
   delete d_i_splx;
+  delete d_i_cegqi;
 }
 
 void InstantiationEngine::finishInit(){
@@ -72,8 +73,14 @@ void InstantiationEngine::finishInit(){
 
   //counterexample-based quantifier instantiation
   if( options::cbqi() ){
-    d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
-    d_instStrategies.push_back( d_i_splx );
+    if( !options::cbqi2() || options::cbqi.wasSetByUser() ){
+      d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
+      d_instStrategies.push_back( d_i_splx );
+    }
+    if( options::cbqi2() ){
+      d_i_cegqi = new InstStrategyCegqi( d_quantEngine );
+      d_instStrategies.push_back( d_i_cegqi );
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index c69136933..8a733ac1d 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -29,6 +29,7 @@ class InstStrategyAutoGenTriggers;
 class InstStrategyLocalTheoryExt;
 class InstStrategyFreeVariable;
 class InstStrategySimplex;
+class InstStrategyCegqi;
 
 /** instantiation strategy class */
 class InstStrategy {
@@ -68,6 +69,8 @@ private:
   InstStrategyFreeVariable * d_i_fs;
   /** simplex (cbqi) */
   InstStrategySimplex * d_i_splx;
+  /** generic cegqi */
+  InstStrategyCegqi * d_i_cegqi;
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** whether the instantiation engine should set incomplete if it cannot answer SAT */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index a7440639b..62790432d 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -220,8 +220,10 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
   generalize based on content in global search space narrowing
   
 # older implementation
-option cbqi --enable-cbqi bool :read-write :default false
+option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
+option cbqi2 --cbqi2 bool :read-write :default false
+ turns on new implementation of counterexample-based quantifier instantiation
 option recurseCbqi --cbqi-recurse bool :default false
  turns on recursive counterexample-based quantifier instantiation
  
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a475a8912..888cdbce0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -899,11 +899,9 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
     // doing literal-based matching (consider polarity of literals)
     for( int i=0; i<(int)nodes.size(); i++ ){
       Node prev = nodes[i];
-      bool nodeChanged = false;
       if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
         bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
         nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
-        nodeChanged = true;
       }
       //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
       //  Node req = qe->getPhaseReqEquality( f, trNodes[i] );