Minor refactor CEGQI.

3 files changed, 300 insertions, 256 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 353b6d1c4..f047276b0 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -441,7 +441,7 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef
       }
       Assert( vchildren.empty() );
       if( incomplete ){
-        Trace("ajr-temp") << "Construct incomplete entry." << std::endl;
+        Trace("ambqi-check-debug2") << "Construct incomplete entry." << std::endl;
 
         //if a child is unknown, we must return unknown
         construct_entry( entry, entry_def, val_unk );
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 089fd973e..a034bb8c1 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -43,13 +43,271 @@ CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active
   d_refine_count = 0;
 }
 
-void CegInstantiation::CegConjecture::assign( Node q ) {
+void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
   Assert( d_quant.isNull() );
   Assert( q.getKind()==FORALL );
   d_quant = q;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
   }
+  //construct base instantiation
+  d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) );
+  Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
+  if( qe->getTermDatabase()->isQAttrSygus( q ) ){
+    CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
+    Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
+    //store the inner variables for each disjunct
+    for( unsigned j=0; j<d_base_disj.size(); j++ ){
+      d_inner_vars_disj.push_back( std::vector< Node >() );
+      //if the disjunct is an existential, store it
+      if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){
+        for( unsigned k=0; k<d_base_disj[j][0][0].getNumChildren(); k++ ){
+          d_inner_vars.push_back( d_base_disj[j][0][0][k] );
+          d_inner_vars_disj[j].push_back( d_base_disj[j][0][0][k] );
+        }
+      }
+    }
+    analyzeSygusConjecture();
+    d_syntax_guided = true;
+  }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
+    d_syntax_guided = false;
+  }else{
+    Assert( false );
+  }
+}
+
+
+
+void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
+  Node q = d_quant;
+  // 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
+  if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
+    //try to phrase as single invocation property
+    bool singleInvocation = true;
+    Trace("cegqi-analyze") << "...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-analyze-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-analyze-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-analyze") << "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 );
+        Node pv = NodeManager::currentNM()->mkBoundVar( "F", inv.getType() );
+        d_single_inv_map[prog] = pv;
+        pbvs.push_back( pv );
+        Trace("cegqi-analyze-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 ){
+            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 );
+
+            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-analyze-debug") << "  ..." << arg << " occurs in ";
+              Trace("cegqi-analyze-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-analyze-debug") << "  ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl;
+                Trace("cegqi-analyze-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-analyze") << "  " << prog << " -> " << sinv << std::endl;
+        d_single_inv_app_map[prog] = sinv;
+      }
+      //construct the single invocation version of the property
+      Trace("cegqi-analyze") << "Single invocation formula conjuncts are : " << std::endl;
+      //std::vector< Node > si_conj;
+      Assert( !pbvs.empty() );
+      Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+      Node si;
+      for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
+        Assert( si.isNull() );
+        std::vector< Node > tmp;
+        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-analyze-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 );
+          Trace("cegqi-analyze") << "    " << curr;
+          tmp.push_back( curr.negate() );
+          if( !it->first.isNull() ){
+            Trace("cegqi-analyze-debug") << " under " << it->first;
+          }
+          Trace("cegqi-analyze") << std::endl;
+        }
+        Assert( !tmp.empty() );
+        Node bd = tmp.size()==1 ? tmp[0] : NodeManager::currentNM()->mkNode( OR, tmp );
+        if( !it->first.isNull() ){
+          // apply substitution for skolem variables
+          std::vector< Node > vars;
+          d_single_inv_arg_sk.clear();
+          for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
+            std::stringstream ss;
+            ss << "k_" << it->first[j];
+            Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
+            vars.push_back( it->first[j] );
+            d_single_inv_arg_sk.push_back( v );
+          }
+          bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() );
+          
+          Trace("cegqi-analyze-debug") << "    -> " << bd << std::endl;
+        }
+        si = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+      }
+      Trace("cegqi-analyze-debug") << "...formula is : " << si << std::endl;
+      d_single_inv = si;
+    }else{
+      Trace("cegqi-analyze") << "Property is not single invocation." << std::endl;
+    }
+  }
+}
+  
+bool CegInstantiation::CegConjecture::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 = n.negate();
+    }
+    Trace("cegqi-analyze") << "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-analyze") << "  Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl;
+      for( unsigned j=0; j<it->second.size(); j++ ){
+        Trace("cegqi-analyze") << "    " << it->second[j] << std::endl;
+      }
+    }
+    return success;
+  }
+  return true;
+}
+
+bool CegInstantiation::CegConjecture::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 CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
@@ -64,6 +322,27 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
       Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() );
       Trace("cegqi") << "Add candidate lemma : " << lem << std::endl;
       qe->getOutputChannel().lemma( lem );
+    }else if( !d_single_inv.isNull() ){
+      Assert( d_single_inv.getKind()==FORALL );
+      std::vector< Node > vars;
+      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" );
+        vars.push_back( d_single_inv[0][i] );
+        d_single_inv_sk.push_back( k );
+      }
+      Node inst = d_single_inv[1].substitute( vars.begin(), vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+      Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), inst.negate() );
+      Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl;
+      /*  inactive for now (until figure out how to use it)
+      qe->getOutputChannel().lemma( lem );
+      if( Trace.isOn("cegqi-debug") ){
+        lem = Rewriter::rewrite( lem );
+        Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
+      }
+      */
     }
   }
 }
@@ -133,31 +412,8 @@ void CegInstantiation::registerQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==this ){
     if( !d_conj->isAssigned() ){
       Trace("cegqi") << "Register conjecture : " << q << std::endl;
-      d_conj->assign( q );
-      //construct base instantiation
-      d_conj->d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj->d_candidates ) );
-      Trace("cegqi") << "Base instantiation is : " << d_conj->d_base_inst << std::endl;
-      if( getTermDatabase()->isQAttrSygus( q ) ){
-        collectDisjuncts( d_conj->d_base_inst, d_conj->d_base_disj );
-        Trace("cegqi") << "Conjecture has " << d_conj->d_base_disj.size() << " disjuncts." << std::endl;
-        //store the inner variables for each disjunct
-        for( unsigned j=0; j<d_conj->d_base_disj.size(); j++ ){
-          d_conj->d_inner_vars_disj.push_back( std::vector< Node >() );
-          //if the disjunct is an existential, store it
-          if( d_conj->d_base_disj[j].getKind()==NOT && d_conj->d_base_disj[j][0].getKind()==FORALL ){
-            for( unsigned k=0; k<d_conj->d_base_disj[j][0][0].getNumChildren(); k++ ){
-              d_conj->d_inner_vars.push_back( d_conj->d_base_disj[j][0][0][k] );
-              d_conj->d_inner_vars_disj[j].push_back( d_conj->d_base_disj[j][0][0][k] );
-            }
-          }
-        }
-        analyzeSygusConjecture( q );
-        d_conj->d_syntax_guided = true;
-      }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
-        d_conj->d_syntax_guided = false;
-      }else{
-        Assert( false );
-      }
+      d_conj->assign( d_quantEngine, q );
+
       //fairness
       if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){
         std::vector< Node > mc;
@@ -499,220 +755,4 @@ void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) {
   out << n << std::endl;
 }
 
-void CegInstantiation::analyzeSygusConjecture( Node q ) {
-  // 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
-  if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
-    //try to phrase as single invocation property
-    bool singleInvocation = true;
-    Trace("cegqi-analyze") << "...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-analyze-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-analyze-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-analyze") << "Property is single invocation with : " << std::endl;
-      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 );
-        d_single_inv_map[q][prog] = NodeManager::currentNM()->mkSkolem( "F", inv.getType(), "single invocation function variable" );
-        Trace("cegqi-analyze-debug2") << "Make variable " << d_single_inv_map[q][prog] << " 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 ){
-            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 );
-
-            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-analyze-debug") << "  ..." << arg << " occurs in ";
-              Trace("cegqi-analyze-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-analyze-debug") << "  ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl;
-                Trace("cegqi-analyze-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-analyze") << "  " << prog << " -> " << sinv << std::endl;
-        d_single_inv_app_map[q][prog] = sinv;
-      }
-      //construct the single invocation version of the property
-      Trace("cegqi-analyze") << "Single invocation formula conjuncts are : " << std::endl;
-      std::vector< Node > si_conj;
-      for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
-        std::vector< Node > tmp;
-        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[q][prog] );
-                Trace("cegqi-analyze-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[q][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 );
-          Trace("cegqi-analyze") << "    " << curr;
-          if( it->first.isNull() ){
-            si_conj.push_back( curr.negate() );
-          }else{
-            tmp.push_back( curr );
-            Trace("cegqi-analyze-debug") << " under " << it->first;
-          }
-          Trace("cegqi-analyze") << std::endl;
-        }
-        if( !it->first.isNull() ){
-          Assert( !tmp.empty() );
-          Node bd = tmp.size()==1 ? tmp[0] : NodeManager::currentNM()->mkNode( AND, tmp );
-          Node curr = NodeManager::currentNM()->mkNode( FORALL, it->first, bd ).negate();
-          si_conj.push_back( curr );
-          Trace("cegqi-analyze-debug") << "    -> " << curr << std::endl;
-        }
-      }
-      Node si = si_conj.size()==1 ? si_conj[0] : NodeManager::currentNM()->mkNode( OR, si_conj );
-      Trace("cegqi-analyze-debug") << "...formula is : " << si << std::endl;
-      d_single_inv[q] = si;
-    }else{
-      Trace("cegqi-analyze") << "Property is not single invocation." << std::endl;
-    }
-  }
-}
-  
-bool CegInstantiation::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 = n.negate();
-    }
-    Trace("cegqi-analyze") << "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-analyze") << "  Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl;
-      for( unsigned j=0; j<it->second.size(); j++ ){
-        Trace("cegqi-analyze") << "    " << it->second[j] << std::endl;
-      }
-    }
-    return success;
-  }
-  return true;
-}
-
-bool CegInstantiation::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;
-}
-
 }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 8b3d56a2a..ad94b51a5 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -67,11 +67,27 @@ private:
     /** refine count */
     unsigned d_refine_count;
     /** assign */
-    void assign( Node q );
+    void assign( QuantifiersEngine * qe, Node q );
     /** is assigned */
     bool isAssigned() { return !d_quant.isNull(); }
     /** current extential quantifeirs whose couterexamples we must refine */
     std::vector< std::vector< Node > > d_ce_sk;
+  private: //for single invocation
+    void analyzeSygusConjecture();
+    bool analyzeSygusConjunct( Node n, Node p, 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 );
+    bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains );
+  public:
+    Node d_single_inv;
+    //map from programs to variables in single invocation property
+    std::map< Node, Node > d_single_inv_map;
+    //map from programs to evaluator term representing the above variable
+    std::map< Node, Node > d_single_inv_app_map;
+    //list of skolems for each argument of programs
+    std::vector< Node > d_single_inv_arg_sk;
+    //list of skolems for each program
+    std::vector< Node > d_single_inv_sk;
   public:  //for fairness
     /** the cardinality literals */
     std::map< int, Node > d_lits;
@@ -107,18 +123,6 @@ private:
   /** get model term */
   Node getModelTerm( Node n );
 private:
-  std::map< Node, Node > d_single_inv;
-  //map from programs to variables in single invocation property
-  std::map< Node, std::map< Node, Node > > d_single_inv_map;
-  //map from programs to evaluator term representing the above variable
-  std::map< Node, std::map< Node, Node > > d_single_inv_app_map;
-private:
-  void analyzeSygusConjecture( Node q );
-  bool analyzeSygusConjunct( Node n, Node p, 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 );
-  bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains );
-private:
   /** print sygus term */
   void printSygusTerm( std::ostream& out, Node n );
 public: