From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 2 Feb 2015 16:42:31 +0000 (+0100)
Subject: Single invocation module for counterexample guided quantifier instantiation --cegqi... 
X-Git-Tag: cvc5-1.0.0~6409
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8deb9d980d7b0e281a0190539b756896a487c451;p=cvc5.git

Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring.  Do not apply exhaustive tester inference for sygus datatypes.
---

diff --git a/src/Makefile.am b/src/Makefile.am
index 184ef5d56..4ae3c16f8 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -327,6 +327,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/conjecture_generator.cpp \
 	theory/quantifiers/ce_guided_instantiation.h \
 	theory/quantifiers/ce_guided_instantiation.cpp \
+	theory/quantifiers/ce_guided_single_inv.h \
+	theory/quantifiers/ce_guided_single_inv.cpp \
 	theory/quantifiers/local_theory_ext.h \
 	theory/quantifiers/local_theory_ext.cpp \
 	theory/quantifiers/fun_def_process.h \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0be445f57..3aec77a45 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1346,6 +1346,9 @@ void SmtEngine::setDefaults() {
   }
   
   //apply counterexample guided instantiation options
+  if( options::cegqiSingleInv() ){
+    options::ceGuidedInst.set( true );
+  }
   if( options::ceGuidedInst() ){
     if( !options::quantConflictFind.wasSetByUser() ){
       options::quantConflictFind.set( false );
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 5e42ac302..4946e25f9 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -52,7 +52,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
       Assert( pdt.isSygus() );
       csIndex = Datatype::cindexOf(selectorExpr);
       sIndex = Datatype::indexOf(selectorExpr);
-      TypeNode tnnp = n[0].getType();
+      tnnp = n[0].getType();
       //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt
       registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex );
 
@@ -88,17 +88,33 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
           //check if we can strengthen the first argument
           if( !arg1.isNull() ){
             const Datatype& dt1 = ((DatatypeType)(tn1).toType()).getDatatype();
+            Kind k = d_util->getArgKind( tnnp, csIndex );
+            //size comparison for arguments (if necessary)
+            Node sz_leq;
+            if( tn1==tnn && d_util->isComm( k ) ){
+              sz_leq = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkNode( DT_SIZE, n ), NodeManager::currentNM()->mkNode( DT_SIZE, arg1 ) );
+            }
             std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i );
             if( it!=d_sygus_pc_arg_pos[tnn][csIndex].end() ){
               Assert( !it->second.empty() );
               std::vector< Node > lem_c;
               for( unsigned j=0; j<it->second.size(); j++ ){
-                lem_c.push_back( DatatypesRewriter::mkTester( arg1, it->second[j], dt1 ) );
+                Node tt = DatatypesRewriter::mkTester( arg1, it->second[j], dt1 );
+                //if commutative operator, and children have same constructor type, then first arg is larger than second arg
+                if( it->second[j]==(int)i && !sz_leq.isNull() ){
+                  tt = NodeManager::currentNM()->mkNode( AND, tt, sz_leq );
+                }
+                lem_c.push_back( tt );
               }
               Node argStr = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( OR, lem_c );
               Trace("sygus-str") << "...strengthen corresponding first argument of " << test << " : " << argStr << std::endl;
               test_c.push_back( argStr );
               narrow = true;
+            }else{
+              if( !sz_leq.isNull() ){
+                test_c.push_back( NodeManager::currentNM()->mkNode( OR, DatatypesRewriter::mkTester( arg1, i, dt1 ).negate(), sz_leq ) );
+                narrow = true;
+              }
             }
           }
           //other constraints on arguments
@@ -282,6 +298,18 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
               Node g = d_util->mkGeneric( pdt, csIndex, var_count, pre );
               addSplit = !isGenericRedundant( tnnp, g );
             }
+            /*
+            else{
+              Trace("sygus-nf-temp") << "Check " << dt[i].getName() << " as argument " << sIndex << " under " << parentKind << std::endl;
+              std::map< int, Node > prec;
+              std::map< TypeNode, int > var_count;
+              Node gc = d_util->mkGeneric( dt, i, var_count, prec );
+              std::map< int, Node > pre;
+              pre[sIndex] = gc;
+              Node g = d_util->mkGeneric( pdt, csIndex, var_count, pre );
+              bool tmp = !isGenericRedundant( tnnp, g, false );
+            }
+            */
           }
         }
         d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit );
@@ -394,7 +422,6 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
     }
     Kind nk = UNDEFINED_KIND;
     Kind reqk = UNDEFINED_KIND;  //required kind for all children
-    std::map< int, Kind > reqk_arg; //TODO
     if( parent==NOT ){
       if( k==AND ) {
         nk = OR;reqk = NOT;
@@ -436,52 +463,51 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
       int pcr = d_util->getKindArg( tnp, nk );
       if( pcr!=-1 ){
         Assert( pcr<(int)pdt.getNumConstructors() );
-        //must have same number of arguments
-        if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){
-          bool success = true;
-          std::map< int, TypeNode > childTypes;
-          for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
-            TypeNode tna = getArgType( pdt[pcr], i );
-            Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) );
-            if( reqk!=UNDEFINED_KIND ){
-              //child must have a NOT
-              int nindex = d_util->getKindArg( tna, reqk );
-              if( nindex!=-1 ){
-                const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype();
-                childTypes[i] = getArgType( adt[nindex], 0 );
-              }else{
-                Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl;
-                success = false;
-                break;
-              }
-            }else{
-              childTypes[i] = tna;
-            }
-          }
-          if( success ){
-            //children types of reduced operator must match types of original
+        if( reqk!=UNDEFINED_KIND ){
+          //must have same number of arguments
+          if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){
+            bool success = true;
+            std::map< int, TypeNode > childTypes;
             for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
-              if( getArgType( dt[c], i )!=childTypes[i] ){
-                Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl;
-                success = false;
-                break;
+              TypeNode tna = getArgType( pdt[pcr], i );
+              Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) );
+              if( reqk!=UNDEFINED_KIND ){
+                //child must have a NOT
+                int nindex = d_util->getKindArg( tna, reqk );
+                if( nindex!=-1 ){
+                  const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype();
+                  if( getArgType( dt[c], i )!=getArgType( adt[nindex], 0 ) ){
+                    Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl;
+                    success = false;
+                    break;
+                  }
+                }else{
+                  Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl;
+                  success = false;
+                  break;
+                }
+              }else{
+                childTypes[i] = tna;
               }
             }
-            if( !success ){
-              //check based on commutativity TODO
-            }
             if( success ){
               Trace("sygus-split-debug") << "...success" << std::endl;
               return false;
             }
+          }else{
+            Trace("sygus-split-debug") << "...#arg mismatch." << std::endl;
           }
         }else{
-          Trace("sygus-split-debug") << "...#arg mismatch." << std::endl;
+          return !isTypeMatch( pdt[pcr], dt[c] );
         }
       }else{
         Trace("sygus-split-debug") << "...operator not available." << std::endl;
       }
     }
+  }
+  if( parent==MINUS || parent==BITVECTOR_SUB ){
+    
+    
   }
   return true;
 }
@@ -575,25 +601,37 @@ bool SygusSplit::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConst
   }
 }
 
-bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) {
+bool SygusSplit::isGenericRedundant( TypeNode tn, Node g, bool active ) {
   //everything added to this cache should be mutually exclusive cases
   std::map< Node, bool >::iterator it = d_gen_redundant[tn].find( g );
   if( it==d_gen_redundant[tn].end() ){
     Trace("sygus-gnf") << "Register generic for " << tn << " : " << g << std::endl;
     Node gr = d_util->getNormalized( tn, g, false );
     Trace("sygus-gnf-debug") << "Generic " << g << " rewrites to " << gr << std::endl;
-    std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr );
-    bool red = true;
-    if( itg==d_gen_terms[tn].end() ){
-      red = false;
-      d_gen_terms[tn][gr] = g;
-      Trace("sygus-gnf-debug") << "...not redundant." << std::endl;
+    if( active ){
+      std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr );
+      bool red = true;
+      if( itg==d_gen_terms[tn].end() ){
+        red = false;
+        d_gen_terms[tn][gr] = g;
+        d_gen_terms_inactive[tn][gr] = g;
+        Trace("sygus-gnf-debug") << "...not redundant." << std::endl;
+      }else{
+        Trace("sygus-gnf-debug") << "...redundant." << std::endl;
+        Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl;
+      }
+      d_gen_redundant[tn][g] = red;
+      return red;
     }else{
-      Trace("sygus-gnf-debug") << "...redundant." << std::endl;
-      Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl;
+      std::map< Node, Node >::iterator itg = d_gen_terms_inactive[tn].find( gr );
+      if( itg==d_gen_terms_inactive[tn].end() ){
+        Trace("sygus-nf-temp") << "..." << g << " rewrites to " << gr << std::endl;
+        d_gen_terms_inactive[tn][gr] = g;
+      }else{
+        Trace("sygus-nf-temp") << "* Note " << g << " and " << itg->second << " both rewrite to " << gr << std::endl;
+      }
+      return false;
     }
-    d_gen_redundant[tn][g] = red;
-    return red;
   }else{
     return it->second;
   }
@@ -1064,10 +1102,10 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
     }else{
       Trace("sygus-sym-break2") << "repeated lemma for " << prog << " from " << a << std::endl;
     }
-    return false;
-  }else{
-    return true;
+    //for now, continue adding lemmas (since we are not forcing conflicts)
+    //return false;
   }
+  return true;
 }
 
 bool SygusSymBreak::isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers ) {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index e1188d5c9..b694bbe9c 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -45,6 +45,7 @@ private:
   std::map< TypeNode, TypeNode > d_register;  //stores sygus type
   // type to (rewritten) to original
   std::map< TypeNode, std::map< Node, Node > > d_gen_terms;
+  std::map< TypeNode, std::map< Node, Node > > d_gen_terms_inactive;
   std::map< TypeNode, std::map< Node, bool > > d_gen_redundant;
 private:
   /** register sygus type */
@@ -64,7 +65,7 @@ private:
   bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
 private:
   // generic cache
-  bool isGenericRedundant( TypeNode tn, Node g );
+  bool isGenericRedundant( TypeNode tn, Node g, bool active = true );
 public:
   SygusSplit( SygusUtil * util ) : d_util( util ) {}
   /** get sygus splits */
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c73ec8039..8d1ebd4fa 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -984,7 +984,8 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
       }else{
         //check if we have reached the maximum number of testers
         // in this case, add the positive tester
-        if( lbl->size()==dt.getNumConstructors()-1 ){
+        //this should not be done for sygus, since cases may be limited
+        if( lbl->size()==dt.getNumConstructors()-1 && !dt.isSygus() ){
           std::vector< bool > pcons;
           getPossibleCons( eqc, n, pcons );
           int testerIndex = -1;
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 91c04bc80..dda3b1be4 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -179,20 +179,7 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,
     std::map< Node, Node > msum;
     if (QuantArith::getMonomialSumLit( lit, msum )){
       Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
-      for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-        Trace("bound-int-debug") << "  ";
-        if( !it->second.isNull() ){
-          Trace("bound-int-debug") << it->second;
-          if( !it->first.isNull() ){
-            Trace("bound-int-debug") << " * ";
-          }
-        }
-        if( !it->first.isNull() ){
-          Trace("bound-int-debug") << it->first;
-        }
-        Trace("bound-int-debug") << std::endl;
-      }
-      Trace("bound-int-debug") << std::endl;
+      QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" );
       for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
         if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){
           Node veq;
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index a64362c14..addcd5337 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -29,21 +29,12 @@ using namespace std;
 
 namespace CVC4 {
 
-void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
-  if( n.getKind()==OR ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      collectDisjuncts( n[i], d );
-    }
-  }else{
-    d.push_back( n );
-  }
-}
-
-CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
+CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
   d_refine_count = 0;
+  d_ceg_si = NULL;
 }
 
-void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
+void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
   Assert( d_quant.isNull() );
   Assert( q.getKind()==FORALL );
   d_quant = q;
@@ -68,8 +59,9 @@ void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
       }
     }
     d_syntax_guided = true;
-    if( options::sygusSingleInv() ){
-      analyzeSygusConjecture();
+    if( options::cegqiSingleInv() ){
+      d_ceg_si = new CegConjectureSingleInv( q, this );
+      d_ceg_si->initialize();
     }
   }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
     d_syntax_guided = false;
@@ -78,282 +70,7 @@ void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
   }
 }
 
-
-
-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;
-        d_single_inv_map_to_prog[pv] = prog;
-        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 );
-      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 > 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;
-        }
-        d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
-        //equality resolution
-        for( unsigned j=0; j<tmp.size(); j++ ){
-          Node conj = tmp[j];
-          std::map< Node, std::vector< Node > > case_vals;
-          bool exh = processSingleInvLiteral( conj, false, case_vals );
-          Trace("cegqi-analyze-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl;
-          for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){
-            Trace("cegqi-analyze-er") << "  " << it->first << " -> ";
-            for( unsigned k=0; k<it->second.size(); k++ ){
-              Trace("cegqi-analyze-er") << it->second[k] << " ";
-            }
-            Trace("cegqi-analyze-er") << std::endl;
-          }
-
-        }
-      }
-      Trace("cegqi-analyze-debug") << "...formula is : " << d_single_inv << std::endl;
-    }else{
-      Trace("cegqi-analyze") << "Property is not single invocation." << std::endl;
-    }
-  }
-}
-
-bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
-  if( lit.getKind()==NOT ){
-    return processSingleInvLiteral( lit[0], !pol, case_vals );
-  }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
-    bool exh = true;
-    for( unsigned k=0; k<lit.getNumChildren(); k++ ){
-      bool curr = processSingleInvLiteral( lit[k], pol, case_vals );
-      exh = exh && curr;
-    }
-    return exh;
-  }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
-    if( pol ){
-      for( unsigned r=0; r<2; r++ ){
-        std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] );
-        if( it!=d_single_inv_map_to_prog.end() ){
-          if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
-            case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] );
-            return true;
-          }
-        }
-      }
-    }
-  }
-  return false;
-}
-
-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 ){
+void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
   if( d_guard.isNull() ){
     d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
     //specify guard behavior
@@ -365,30 +82,21 @@ 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;
-      qe->getOutputChannel().lemma( lem );
-      if( Trace.isOn("cegqi-debug") ){
-        lem = Rewriter::rewrite( lem );
-        Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
+    }else if( d_ceg_si ){
+      Node lem = d_ceg_si->getSingleInvLemma( d_guard );
+      if( !lem.isNull() ){
+        Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl;
+        qe->getOutputChannel().lemma( lem );
+        if( Trace.isOn("cegqi-debug") ){
+          lem = Rewriter::rewrite( lem );
+          Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
+        }
       }
     }
   }
 }
 
-Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
+Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
   if( d_measure_term.isNull() ){
     return Node::null();
   }else{
@@ -424,6 +132,7 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i
 
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
   d_conj = new CegConjecture( d_quantEngine->getSatContext() );
+  d_last_inst_si = false;
 }
 
 bool CegInstantiation::needsCheck( Theory::Effort e ) {
@@ -544,59 +253,72 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   if( conj->d_ce_sk.empty() ){
     Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
     if( getTermDatabase()->isQAttrSygus( q ) ){
-
+      if( conj->d_ceg_si ){
+        std::vector< Node > lems;
+        conj->d_ceg_si->check( d_quantEngine, lems );
+        if( !lems.empty() ){
+          d_last_inst_si = true;
+          for( unsigned j=0; j<lems.size(); j++ ){
+            Trace("cegqi-lemma") << "Single invocation lemma : " << lems[j] << std::endl;
+            d_quantEngine->addLemma( lems[j] );
+          }
+          Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
+          return;
+        }
+      }
       std::vector< Node > model_values;
       if( getModelValues( conj, conj->d_candidates, model_values ) ){
         //check if we must apply fairness lemmas
-        std::vector< Node > lems;
         if( options::ceGuidedInstFair()==CEGQI_FAIR_UF_DT_SIZE ){
+          std::vector< Node > lems;
           for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
             getMeasureLemmas( conj->d_candidates[j], model_values[j], lems );
           }
-        }
-        if( !lems.empty() ){
-          for( unsigned j=0; j<lems.size(); j++ ){
-            Trace("cegqi-lemma") << "Measure lemma : " << lems[j] << std::endl;
-            d_quantEngine->addLemma( lems[j] );
-          }
-          Trace("cegqi-engine") << "  ...refine size." << std::endl;
-        }else{
-          //must get a counterexample to the value of the current candidate
-          Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
-          //check whether we will run CEGIS on inner skolem variables
-          bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 );
-          if( sk_refine ){
-            conj->d_ce_sk.push_back( std::vector< Node >() );
+          if( !lems.empty() ){
+            for( unsigned j=0; j<lems.size(); j++ ){
+              Trace("cegqi-lemma") << "Measure lemma : " << lems[j] << std::endl;
+              d_quantEngine->addLemma( lems[j] );
+            }
+            Trace("cegqi-engine") << "  ...refine size." << std::endl;
+            return;
           }
-          std::vector< Node > ic;
-          ic.push_back( q.negate() );
-          std::vector< Node > d;
-          collectDisjuncts( inst, d );
-          Assert( d.size()==conj->d_base_disj.size() );
-          //immediately skolemize inner existentials
-          for( unsigned i=0; i<d.size(); i++ ){
-            Node dr = Rewriter::rewrite( d[i] );
-            if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
-              ic.push_back( getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
-              if( sk_refine ){
-                conj->d_ce_sk.back().push_back( dr[0] );
-              }
-            }else{
-              ic.push_back( dr );
-              if( sk_refine ){
-                conj->d_ce_sk.back().push_back( Node::null() );
-              }
-              if( !conj->d_inner_vars_disj[i].empty() ){
-                Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
-              }
+        }
+        //must get a counterexample to the value of the current candidate
+        Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
+        //check whether we will run CEGIS on inner skolem variables
+        bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 );
+        if( sk_refine ){
+          conj->d_ce_sk.push_back( std::vector< Node >() );
+        }
+        std::vector< Node > ic;
+        ic.push_back( q.negate() );
+        std::vector< Node > d;
+        collectDisjuncts( inst, d );
+        Assert( d.size()==conj->d_base_disj.size() );
+        //immediately skolemize inner existentials
+        for( unsigned i=0; i<d.size(); i++ ){
+          Node dr = Rewriter::rewrite( d[i] );
+          if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
+            ic.push_back( getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
+            if( sk_refine ){
+              conj->d_ce_sk.back().push_back( dr[0] );
+            }
+          }else{
+            ic.push_back( dr );
+            if( sk_refine ){
+              conj->d_ce_sk.back().push_back( Node::null() );
+            }
+            if( !conj->d_inner_vars_disj[i].empty() ){
+              Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
             }
           }
-          Node lem = NodeManager::currentNM()->mkNode( OR, ic );
-          lem = Rewriter::rewrite( lem );
-          Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
-          d_quantEngine->addLemma( lem );
-          Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
         }
+        Node lem = NodeManager::currentNM()->mkNode( OR, ic );
+        lem = Rewriter::rewrite( lem );
+        d_last_inst_si = false;
+        Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+        d_quantEngine->addLemma( lem );
+        Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
       }
 
     }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
@@ -768,10 +490,16 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       Assert( dt.isSygus() );
       out << dt.getSygusVarList() << " ";
       out << dt.getSygusType() << " ";
-      if( d_conj->d_candidate_inst[i].empty() ){
-        out << "?";
+      if( d_last_inst_si ){
+        Assert( d_conj->d_ceg_si );
+        Node sol = d_conj->d_ceg_si->getSolution( i, Node::fromExpr( dt.getSygusVarList() ) );
+        out << sol;
       }else{
-        printSygusTerm( out, d_conj->d_candidate_inst[i].back() );
+        if( d_conj->d_candidate_inst[i].empty() ){
+          out << "?";
+        }else{
+          printSygusTerm( out, d_conj->d_candidate_inst[i].back() );
+        }
       }
       out << ")" << std::endl;
     }
@@ -802,4 +530,14 @@ void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) {
   out << n;
 }
 
+void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
+  if( n.getKind()==OR ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectDisjuncts( n[i], d );
+    }
+  }else{
+    d.push_back( n );
+  }
+}
+
 }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index aa553fb58..95f491dc9 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -14,94 +14,81 @@
 
 #include "cvc4_private.h"
 
-#ifndef CE_GUIDED_INSTANTIATION_H
-#define CE_GUIDED_INSTANTIATION_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
 
 #include "context/cdhashmap.h"
 #include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+/** a synthesis conjecture */
+class CegConjecture {
+public:
+  CegConjecture( context::Context* c );
+  /** is conjecture active */
+  context::CDO< bool > d_active;
+  /** is conjecture infeasible */
+  context::CDO< bool > d_infeasible;
+  /** quantified formula */
+  Node d_quant;
+  /** guard */
+  Node d_guard;
+  /** base instantiation */
+  Node d_base_inst;
+  /** expand base inst to disjuncts */
+  std::vector< Node > d_base_disj;
+  /** guard split */
+  Node d_guard_split;
+  /** is syntax-guided */
+  bool d_syntax_guided;
+  /** list of constants for quantified formula */
+  std::vector< Node > d_candidates;
+  /** list of variables on inner quantification */
+  std::vector< Node > d_inner_vars;    
+  std::vector< std::vector< Node > > d_inner_vars_disj;
+  /** list of terms we have instantiated candidates with */
+  std::map< int, std::vector< Node > > d_candidate_inst;
+  /** initialize guard */
+  void initializeGuard( QuantifiersEngine * qe );
+  /** measure term */
+  Node d_measure_term;
+  /** measure sum size */
+  int d_measure_term_size;
+  /** refine count */
+  unsigned d_refine_count;
+  /** assign */
+  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;
+  /** single invocation utility */
+  CegConjectureSingleInv * d_ceg_si;
+public:  //for fairness
+  /** the cardinality literals */
+  std::map< int, Node > d_lits;
+  /** current cardinality */
+  context::CDO< int > d_curr_lit;
+  /** allocate literal */
+  Node getLiteral( QuantifiersEngine * qe, int i );
+  /** is ground */
+  bool isGround() { return d_inner_vars.empty(); }
+};
+  
+  
 class CegInstantiation : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 private:
-  /** collect disjuncts */
-  static void collectDisjuncts( Node n, std::vector< Node >& ex );
-  /** a synthesis conjecture */
-  class CegConjecture {
-  public:
-    CegConjecture( context::Context* c );
-    /** is conjecture active */
-    context::CDO< bool > d_active;
-    /** is conjecture infeasible */
-    context::CDO< bool > d_infeasible;
-    /** quantified formula */
-    Node d_quant;
-    /** guard */
-    Node d_guard;
-    /** base instantiation */
-    Node d_base_inst;
-    /** expand base inst to disjuncts */
-    std::vector< Node > d_base_disj;
-    /** guard split */
-    Node d_guard_split;
-    /** is syntax-guided */
-    bool d_syntax_guided;
-    /** list of constants for quantified formula */
-    std::vector< Node > d_candidates;
-    /** list of variables on inner quantification */
-    std::vector< Node > d_inner_vars;    
-    std::vector< std::vector< Node > > d_inner_vars_disj;
-    /** list of terms we have instantiated candidates with */
-    std::map< int, std::vector< Node > > d_candidate_inst;
-    /** initialize guard */
-    void initializeGuard( QuantifiersEngine * qe );
-    /** measure term */
-    Node d_measure_term;
-    /** measure sum size */
-    int d_measure_term_size;
-    /** refine count */
-    unsigned d_refine_count;
-    /** assign */
-    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 );
-    bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
-  public:
-    Node d_single_inv;
-    //map from programs to variables in single invocation property
-    std::map< Node, Node > d_single_inv_map;
-    std::map< Node, Node > d_single_inv_map_to_prog;
-    //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;
-    /** current cardinality */
-    context::CDO< int > d_curr_lit;
-    /** allocate literal */
-    Node getLiteral( QuantifiersEngine * qe, int i );
-    /** is ground */
-    bool isGround() { return d_inner_vars.empty(); }
-  };
   /** the quantified formula stating the synthesis conjecture */
   CegConjecture * d_conj;
+  /** last instantiation by single invocation module? */
+  bool d_last_inst_si;
 private: //for enforcing fairness
   /** measure functions */
   std::map< TypeNode, Node > d_uf_measure;
@@ -143,6 +130,8 @@ public:
   std::string identify() const { return "CegInstantiation"; }
   /** print solution for synthesis conjectures */
   void printSynthSolution( std::ostream& out );  
+  /** collect disjuncts */
+  static void collectDisjuncts( Node n, std::vector< Node >& ex );
 };
 
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
new file mode 100644
index 000000000..efe23d6cb
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -0,0 +1,581 @@
+/*********************                                                        */
+/*! \file ce_guided_single_inv.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief utility for processing single invocation synthesis conjectures
+ **
+ **/
+
+#include "theory/quantifiers/ce_guided_single_inv.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "util/datatype.h"
+#include "theory/quantifiers/quant_util.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+CegConjectureSingleInv::CegConjectureSingleInv( Node q, CegConjecture * p ) : d_parent( p ), d_quant( q ){
+
+}
+
+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() );
+    Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
+    return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst.negate() );
+  }else{
+    return Node::null();
+  }
+}
+
+void CegConjectureSingleInv::initialize() {
+  Node q = d_quant;
+  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
+  if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
+    //try to phrase as single invocation property
+    bool singleInvocation = true;
+    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 ){
+            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-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 > 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-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 );
+          Trace("cegqi-si") << "    " << curr;
+          tmp.push_back( curr.negate() );
+          if( !it->first.isNull() ){
+            Trace("cegqi-si-debug") << " under " << it->first;
+          }
+          Trace("cegqi-si") << 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-si-debug") << "    -> " << bd << std::endl;
+        }
+        d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+        //equality resolution
+        for( unsigned j=0; j<tmp.size(); j++ ){
+          Node conj = tmp[j];
+          std::map< Node, std::vector< Node > > case_vals;
+          bool exh = processSingleInvLiteral( conj, false, case_vals );
+          Trace("cegqi-si-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl;
+          for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){
+            Trace("cegqi-si-er") << "  " << it->first << " -> ";
+            for( unsigned k=0; k<it->second.size(); k++ ){
+              Trace("cegqi-si-er") << it->second[k] << " ";
+            }
+            Trace("cegqi-si-er") << std::endl;
+          }
+
+        }
+      }
+      Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
+    }else{
+      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::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
+  if( lit.getKind()==NOT ){
+    return processSingleInvLiteral( lit[0], !pol, case_vals );
+  }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
+    bool exh = true;
+    for( unsigned k=0; k<lit.getNumChildren(); k++ ){
+      bool curr = processSingleInvLiteral( lit[k], pol, case_vals );
+      exh = exh && curr;
+    }
+    return exh;
+  }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
+    if( pol ){
+      for( unsigned r=0; r<2; r++ ){
+        std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] );
+        if( it!=d_single_inv_map_to_prog.end() ){
+          if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
+            case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] );
+            return true;
+          }
+        }
+      }
+    }
+  }
+  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 = n.negate();
+    }
+    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::check( QuantifiersEngine * qe, std::vector< Node >& lems ) {
+  if( !d_single_inv.isNull() ) { 
+    eq::EqualityEngine* ee = qe->getMasterEqualityEngine();
+    Trace("cegqi-engine") << "  * single invocation: " << std::endl;
+    std::vector< Node > subs;
+    std::map< Node, int > subs_from_model;
+    std::vector< Node > waiting_to_slv;
+    for( unsigned i=0; i<d_single_inv_sk.size(); i++ ){
+      Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
+      Node pv = d_single_inv_sk[i];
+      Trace("cegqi-engine") << "    * " << v;
+      Trace("cegqi-engine") << " (" << pv << ")";
+      Trace("cegqi-engine") << " -> "; 
+      Node slv;
+      if( ee->hasTerm( pv ) ){
+        Node r = ee->getRepresentative( pv );
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+        bool isWaitingSlv = false;
+        while( !eqc_i.isFinished() ){
+          Node n = *eqc_i;
+          if( n!=pv ){
+            if( slv.isNull() || isWaitingSlv ){
+              std::vector< Node > vars;
+              collectProgVars( n, vars );
+              if( slv.isNull() || vars.empty() ){
+                // n cannot contain pv
+                bool isLoop = std::find( vars.begin(), vars.end(), pv )!=vars.end();
+                if( !isLoop ){
+                  for( unsigned j=0; j<vars.size(); j++ ){
+                    if( std::find( waiting_to_slv.begin(), waiting_to_slv.end(), vars[j] )!=waiting_to_slv.end() ){
+                      isLoop = true;
+                      break;
+                    }
+                  }
+                  if( !isLoop ){
+                    slv = n;
+                    isWaitingSlv = !vars.empty();
+                  }
+                }
+              }
+            }
+          }
+          ++eqc_i;
+        }
+        if( isWaitingSlv ){
+          Trace("cegqi-engine-debug") << "waiting:";
+          waiting_to_slv.push_back( pv );
+        }
+      }else{
+        Trace("cegqi-engine-debug") << "N/A:";
+      }
+      if( slv.isNull() ){
+        //get model value
+        Node mv = qe->getModel()->getValue( pv );
+        subs.push_back( mv );
+        subs_from_model[pv] = i;
+        if( Trace.isOn("cegqi-engine") || Trace.isOn("cegqi-engine-debug") ){
+          Trace("cegqi-engine") << "M:" << mv;
+        }
+      }else{
+        subs.push_back( slv );
+        Trace("cegqi-engine") << slv;
+      }
+      Trace("cegqi-engine") << std::endl;
+    }
+    for( int i=(int)(waiting_to_slv.size()-1); i>=0; --i ){
+      int index = d_single_inv_sk_index[waiting_to_slv[i]];
+      Trace("cegqi-engine-debug") << "Go back and solve " << d_single_inv_sk[index] << std::endl;
+      Trace("cegqi-engine-debug") << "Substitute " << subs[index] << " to ";
+      subs[index] = applyProgVarSubstitution( subs[index], subs_from_model, subs );
+      Trace("cegqi-engine-debug") << subs[index] << std::endl;
+    }
+    //try to improve substitutions : look for terms that contain terms in question
+    if( !subs_from_model.empty() ){
+      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+      while( !eqcs_i.isFinished() ){
+        Node r = *eqcs_i;
+        int res = -1;
+        Node slv_n;
+        Node const_n;
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+        while( !eqc_i.isFinished() ){
+          Node n = *eqc_i;
+          if( slv_n.isNull() || const_n.isNull() ){
+            std::vector< Node > vars;
+            int curr_res = classifyTerm( n, subs_from_model );
+            Trace("cegqi-si-debug2") << "Term : " << n << " classify : " << curr_res << std::endl;
+            if( curr_res!=-2 ){
+              if( curr_res!=-1 && slv_n.isNull() ){
+                res = curr_res;
+                slv_n = n;
+              }else if( const_n.isNull() ){
+                const_n = n;
+              }
+            }
+          }
+          ++eqc_i;
+        }
+        if( !slv_n.isNull() && !const_n.isNull() ){
+          if( slv_n.getType().isInteger() || slv_n.getType().isReal() ){
+            Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[res] << " based on " << slv_n << " = " << const_n << std::endl;
+            subs_from_model.erase( d_single_inv_sk[res] );
+            Node prev_subs_res = subs[res];
+            subs[res] = d_single_inv_sk[res];
+            Node eq = slv_n.eqNode( const_n );
+            bool success = false;
+            std::map< Node, Node > msum;
+            if( QuantArith::getMonomialSumLit( eq, msum ) ){
+              Trace("cegqi-si-debug") << "As monomial sum : " << std::endl;
+              QuantArith::debugPrintMonomialSum( msum, "cegqi-si");
+              Node veq;
+              if( QuantArith::isolate( d_single_inv_sk[res], msum, veq, EQUAL ) ){
+                Trace("cegqi-si-debug") << "Isolated for " << d_single_inv_sk[res] << " : " << veq << std::endl;
+                Node sol;
+                for( unsigned r=0; r<2; r++ ){
+                  if( veq[r]==d_single_inv_sk[res] ){
+                    sol = veq[ r==0 ? 1 : 0 ];
+                  }
+                }
+                if( !sol.isNull() ){
+                  sol = applyProgVarSubstitution( sol, subs_from_model, subs );
+                  Trace("cegqi-si-debug") << "Substituted solution is : " << sol << std::endl;
+                  subs[res] = sol;
+                  Trace("cegqi-engine") << "  ...by arithmetic, " << d_single_inv_sk[res] << " -> " << sol << std::endl;
+                  success = true;
+                }
+              }
+            }
+            if( !success ){
+              subs[res] = prev_subs_res;
+            }
+          }
+        }
+        ++eqcs_i;
+      }
+    }
+    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() );
+    }
+  }
+}
+
+Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) {
+  std::vector< Node > vars;
+  collectProgVars( n, vars );
+  if( !vars.empty() ){
+    std::vector< Node > ssubs;
+    //get substitution
+    for( unsigned i=0; i<vars.size(); i++ ){
+      Assert( d_single_inv_sk_index.find( vars[i] )!=d_single_inv_sk_index.end() );
+      int index = d_single_inv_sk_index[vars[i]];
+      ssubs.push_back( subs[index] );
+      //it is now constrained
+      if( subs_from_model.find( vars[i] )!=subs_from_model.end() ){
+        subs_from_model.erase( vars[i] );
+      }
+    }
+    return n.substitute( vars.begin(), vars.end(), ssubs.begin(), ssubs.end() );
+  }else{
+    return n;
+  }
+}
+
+int CegConjectureSingleInv::classifyTerm( Node n, std::map< Node, int >& subs_from_model ) {
+  if( n.getKind()==SKOLEM ){
+    std::map< Node, int >::iterator it = subs_from_model.find( n );
+    if( it!=subs_from_model.end() ){
+      return it->second;
+    }else{
+      // if it is symbolic argument, we are also fine
+      if( std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end() ){
+        return -1;
+      }else{
+        //if it is another program, we are also fine
+        if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
+          return -1;
+        }else{
+          return -2;
+        }
+      }
+    }
+  }else{
+    int curr_res = -1;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      int res = classifyTerm( n[i], subs_from_model );
+      if( res==-2 ){
+        return res;
+      }else if( res!=-1 ){
+        curr_res = res;
+      }
+    }
+    return curr_res;
+  }
+}
+
+void CegConjectureSingleInv::collectProgVars( Node n, std::vector< Node >& vars ) {
+  if( n.getKind()==SKOLEM ){
+    if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
+      if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
+        vars.push_back( n );
+      }
+    }
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectProgVars( n[i], vars );
+    }
+  }
+}
+
+Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
+  Assert( index<d_inst.size() );
+  Assert( i<d_inst[index].size() );
+  if( index==d_inst.size()-1 ){
+    return d_inst[index][i];
+  }else{
+    Node cond = d_lemmas_produced[index];
+    Node ite1 = d_inst[index][i];
+    Node ite2 = constructSolution( i, index+1 );
+    return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
+  }
+}
+
+Node CegConjectureSingleInv::getSolution( unsigned i, Node varList ){
+  Assert( !d_lemmas_produced.empty() );
+  Node s = constructSolution( i, 0 );
+  //TODO : not in grammar
+  std::vector< Node > vars;
+  for( unsigned i=0; i<varList.getNumChildren(); i++ ){
+    vars.push_back( varList[i] );
+  }
+  Assert( vars.size()==d_single_inv_arg_sk.size() );
+  s = s.substitute( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), vars.begin(), vars.end() );
+  return s;  
+}
+
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
new file mode 100644
index 000000000..64c65a2fe
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -0,0 +1,80 @@
+/*********************                                                        */
+/*! \file ce_guided_single_inv.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief utility for processing single invocation synthesis conjectures
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegConjecture;
+
+class CegConjectureSingleInv
+{
+private: 
+  CegConjecture * d_parent;
+  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 );
+  bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
+  
+  Node constructSolution( unsigned i, unsigned index );
+  int classifyTerm( Node n, std::map< Node, int >& subs_from_model );
+  void collectProgVars( Node n, std::vector< Node >& vars );
+  Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
+public:
+  CegConjectureSingleInv( Node q, CegConjecture * p );
+  // original conjecture
+  Node d_quant;
+  // single invocation version of quant
+  Node d_single_inv;
+  //map from programs to variables in single invocation property
+  std::map< Node, Node > d_single_inv_map;
+  std::map< Node, Node > d_single_inv_map_to_prog;
+  //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;
+  std::map< Node, int > d_single_inv_sk_index;
+  //list of skolems for each program
+  std::vector< Node > d_single_inv_var;
+  //lemmas produced
+  std::vector< Node > d_lemmas_produced;
+  std::vector< std::vector< Node > > d_inst;
+public:
+  //get the single invocation lemma
+  Node getSingleInvLemma( Node guard );
+  //initialize 
+  void initialize();
+  //check
+  void check( QuantifiersEngine * qe, std::vector< Node >& lems );
+  //get solution
+  Node getSolution( unsigned i, Node varList );
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 92285bf12..214f3974e 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -196,8 +196,13 @@ option ceGuidedInst --cegqi bool :default false :read-write
   counterexample-guided quantifier instantiation
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
   if and how to apply fairness for cegqi
-option sygusSingleInv --sygus-single-inv bool :default false
+option cegqiSingleInv --cegqi-si bool :default false
   process single invocation synthesis conjectures
+option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
+  reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvAbort --cegqi-si-abort bool :default false
+  abort if our synthesis conjecture is not single invocation
+  
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
 option sygusNormalFormArg --sygus-nf-arg bool :default true
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index f73bc7bb2..2dd800592 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -92,7 +92,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
         if( r.isOne() ){
           veq = negate(veq);
         }else{
-          //TODO
+          //TODO : lcd computation
           return false;
         }
       }
@@ -118,6 +118,23 @@ Node QuantArith::offset( Node t, int i ) {
   return tt;
 }
 
+void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ) {
+  for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+    Trace(c) << "  ";
+    if( !it->second.isNull() ){
+      Trace(c) << it->second;
+      if( !it->first.isNull() ){
+        Trace(c) << " * ";
+      }
+    }
+    if( !it->first.isNull() ){
+      Trace(c) << it->first;
+    }
+    Trace(c) << std::endl;
+  }
+  Trace(c) << std::endl;
+}
+
 
 void QuantRelevance::registerQuantifier( Node f ){
   //compute symbols in f
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index d7e220b2e..1b053cf6a 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -38,6 +38,7 @@ public:
   static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k );
   static Node negate( Node t );
   static Node offset( Node t, int i );
+  static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c );
 };