More work on --cegqi-si-partial, incomplete.

7 files changed, 287 insertions, 68 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 3c482413b..fe38ddf71 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -333,6 +333,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/ce_guided_single_inv.cpp \
 	theory/quantifiers/ce_guided_single_inv_sol.h \
 	theory/quantifiers/ce_guided_single_inv_sol.cpp \
+	theory/quantifiers/ce_guided_single_inv_ei.h \
+	theory/quantifiers/ce_guided_single_inv_ei.cpp \
 	theory/quantifiers/local_theory_ext.h \
 	theory/quantifiers/local_theory_ext.cpp \
 	theory/quantifiers/fun_def_process.h \
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index f11153f5f..dcbfba3ff 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -78,22 +78,23 @@ void CegConjecture::assign( Node q ) {
 }
 
 void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
-  if( isAssigned() && d_guard.isNull() ){
-    d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
-    //specify guard behavior
-    d_guard = qe->getValuation().ensureLiteral( d_guard );
-    AlwaysAssert( !d_guard.isNull() );
-    qe->getOutputChannel().requirePhase( d_guard, true );
+  if( isAssigned() ){
     if( !d_syntax_guided ){
-      //add immediate lemma
-      Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() );
-      Trace("cegqi-lemma") << "Add candidate lemma : " << lem << std::endl;
-      qe->getOutputChannel().lemma( lem );
-    }else if( d_ceg_si ){
+      if( d_nsg_guard.isNull() ){
+        d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+        d_nsg_guard = qe->getValuation().ensureLiteral( d_nsg_guard );
+        AlwaysAssert( !d_nsg_guard.isNull() );
+        qe->getOutputChannel().requirePhase( d_nsg_guard, true );
+        //add immediate lemma
+        Node lem = NodeManager::currentNM()->mkNode( OR, d_nsg_guard.negate(), d_base_inst.negate() );
+        Trace("cegqi-lemma") << "Cegqi::Lemma : non-syntax-guided : " << lem << std::endl;
+        qe->getOutputChannel().lemma( lem );
+      }
+    }else if( d_ceg_si->d_si_guard.isNull() ){
       std::vector< Node > lems;
-      d_ceg_si->getInitialSingleInvLemma( d_guard, lems );
+      d_ceg_si->getInitialSingleInvLemma( lems );
       for( unsigned i=0; i<lems.size(); i++ ){
-        Trace("cegqi-lemma") << "Add single invocation lemma " << i << " : " << lems[i] << std::endl;
+        Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
         qe->getOutputChannel().lemma( lems[i] );
         if( Trace.isOn("cegqi-debug") ){
           Node rlem = Rewriter::rewrite( lems[i] );
@@ -101,6 +102,7 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
         }
       }
     }
+    Assert( !getGuard().isNull() );
   }
 }
 
@@ -117,7 +119,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
       d_lits[i] = lit;
 
       Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
-      Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl;
+      Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness split : " << lem << std::endl;
       qe->getOutputChannel().lemma( lem );
       qe->getOutputChannel().requirePhase( lit, true );
 
@@ -128,7 +130,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
           lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) );
         }
         Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) );
-        Trace("cegqi-lemma") << "Fairness expansion (dt-height-pred) : " << hlem << std::endl;
+        Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (dt-height-pred) : " << hlem << std::endl;
         qe->getOutputChannel().lemma( hlem );
       }
       return lit;
@@ -138,6 +140,10 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
   }
 }
 
+Node CegConjecture::getGuard() {
+  return !d_syntax_guided ? d_nsg_guard : d_ceg_si->d_si_guard;
+}
+
 CegqiFairMode CegConjecture::getCegqiFairMode() {
   return isSingleInvocation() ? CEGQI_FAIR_NONE : options::ceGuidedInstFair();
 }
@@ -150,8 +156,52 @@ bool CegConjecture::isFullySingleInvocation() {
   return d_ceg_si->isFullySingleInvocation();
 }
 
-bool CegConjecture::needsCheck() {
-  return !isSingleInvocation() || d_ceg_si->needsCheck();
+bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
+  if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
+    return false;
+  }else{
+    bool value;
+    if( !isSingleInvocation() || isFullySingleInvocation() ){
+      Assert( !getGuard().isNull() );
+      // non or fully single invocation : look at guard only
+      if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) {
+        if( !value ){
+          Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
+          return false;
+        }
+      }else{
+        Assert( false );
+      }
+    }else{
+      // not fully single invocation : infeasible if overall specification is infeasible
+      Assert( !d_ceg_si->d_full_guard.isNull() );
+      if( d_qe->getValuation().hasSatValue( d_ceg_si->d_full_guard, value ) ) {
+        if( !value ){
+          Trace("cegqi-nsi") << "NSI : found full specification is infeasible." << std::endl;
+          return false;
+        }else{
+          Assert( !d_ceg_si->d_si_guard.isNull() );
+          if( d_qe->getValuation().hasSatValue( d_ceg_si->d_si_guard, value ) ) {
+            if( !value ){
+              if( !d_ceg_si->d_single_inv_exp.isNull() ){
+                //this should happen infrequently : only if cegqi determines infeasibility of a false candidate before E-matching does
+                Trace("cegqi-nsi") << "NSI : current single invocation lemma was infeasible, block assignment upon which conjecture was based." << std::endl;
+                Node l = NodeManager::currentNM()->mkNode( OR, d_ceg_si->d_full_guard.negate(), d_ceg_si->d_single_inv_exp );
+                lem.push_back( l );
+                d_ceg_si->initializeNextSiConjecture();
+              }
+              return false;
+            }
+          }else{
+            Assert( false );
+          }
+        }
+      }else{
+        Assert( false );
+      }
+    }
+    return true;
+  }
 }
 
 void CegConjecture::preregisterConjecture( Node q ) {
@@ -168,29 +218,30 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 }
 
 unsigned CegInstantiation::needsModel( Theory::Effort e ) {
-  return QuantifiersEngine::QEFFORT_MODEL;
+  return d_conj->d_ceg_si->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
 }
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
-  if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
+  unsigned echeck = d_conj->d_ceg_si->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
+  if( quant_e==echeck ){
     Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
     Trace("cegqi-engine-debug") << std::endl;
     bool active = false;
-    bool feasible = false;
     bool value;
     if( d_quantEngine->getValuation().hasSatValue( d_conj->d_assert_quant, value ) ) {
       active = value;
     }else{
       Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl;
     }
-    if( d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
-      feasible = value;
-    }else{
-      Trace("cegqi-engine-debug") << "...no value for guard." << std::endl;
-    }
-    Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << " feasible : " << feasible << std::endl;
-    if( active && feasible && d_conj->needsCheck() ){
+    Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << std::endl;
+    std::vector< Node > lem;
+    if( active && d_conj->needsCheck( lem ) ){
       checkCegConjecture( d_conj );
+    }else{
+      for( unsigned i=0; i<lem.size(); i++ ){
+        Trace("cegqi-lemma") << "Cegqi::Lemma : check lemma : " << lem[i] << std::endl;
+        d_quantEngine->getOutputChannel().lemma( lem[i] );
+      }
     }
     Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
   }
@@ -241,9 +292,14 @@ Node CegInstantiation::getNextDecisionRequest() {
   if( d_conj->isAssigned() ){
     d_conj->initializeGuard( d_quantEngine );
     std::vector< Node > req_dec;
-    req_dec.push_back( d_conj->d_guard );
-    if( d_conj->d_ceg_si && !d_conj->d_ceg_si->d_ns_guard.isNull() ){
-      req_dec.push_back( d_conj->d_ceg_si->d_ns_guard );
+    req_dec.push_back( d_conj->getGuard() );
+    if( d_conj->d_ceg_si ){
+      if( !d_conj->d_ceg_si->d_full_guard.isNull() ){
+        req_dec.push_back( d_conj->d_ceg_si->d_full_guard );
+      }
+      if( !d_conj->d_ceg_si->d_ns_guard.isNull() ){
+        req_dec.push_back( d_conj->d_ceg_si->d_ns_guard );
+      }
     }
     for( unsigned i=0; i<req_dec.size(); i++ ){
       bool value;
@@ -295,7 +351,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         if( !lems.empty() ){
           d_last_inst_si = true;
           for( unsigned j=0; j<lems.size(); j++ ){
-            Trace("cegqi-lemma") << "Single invocation instantiation lemma : " << lems[j] << std::endl;
+            Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << lems[j] << std::endl;
             d_quantEngine->addLemma( lems[j] );
           }
           d_statistics.d_cegqi_si_lemmas += lems.size();
@@ -313,7 +369,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           }
           if( !lems.empty() ){
             for( unsigned j=0; j<lems.size(); j++ ){
-              Trace("cegqi-lemma") << "Measure lemma : " << lems[j] << std::endl;
+              Trace("cegqi-lemma") << "Cegqi::Lemma : measure : " << lems[j] << std::endl;
               d_quantEngine->addLemma( lems[j] );
             }
             Trace("cegqi-engine") << "  ...refine size." << std::endl;
@@ -353,7 +409,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         Node lem = NodeManager::currentNM()->mkNode( OR, ic );
         lem = Rewriter::rewrite( lem );
         d_last_inst_si = false;
-        Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+        Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl;
         d_quantEngine->addLemma( lem );
         ++(d_statistics.d_cegqi_lemmas_ce);
         Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
@@ -399,9 +455,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       }
       if( success ){
         Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
-        lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), lem );
+        lem = NodeManager::currentNM()->mkNode( OR, conj->getGuard().negate(), lem );
         lem = Rewriter::rewrite( lem );
-        Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
+        Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl;
         Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
         d_quantEngine->addLemma( lem );
         ++(d_statistics.d_cegqi_lemmas_refine);
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 82c57b3d8..6fcfdbc58 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -37,16 +37,10 @@ public:
   Node d_assert_quant;
   /** quantified formula (after processing) */
   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 */
@@ -54,22 +48,20 @@ public:
   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( 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: //non-syntax guided (deprecated)
+  /** guard */
+  bool d_syntax_guided;
+  Node d_nsg_guard;  
 public:  //for fairness
   /** the cardinality literals */
   std::map< int, Node > d_lits;
@@ -77,6 +69,8 @@ public:  //for fairness
   context::CDO< int > d_curr_lit;
   /** allocate literal */
   Node getLiteral( QuantifiersEngine * qe, int i );
+  /** get guard */
+  Node getGuard();
   /** is ground */
   bool isGround() { return d_inner_vars.empty(); }
   /** fairness */
@@ -86,9 +80,15 @@ public:  //for fairness
   /** is single invocation */
   bool isFullySingleInvocation();
   /** needs check */
-  bool needsCheck();
+  bool needsCheck( std::vector< Node >& lem );
   /** preregister conjecture */
   void preregisterConjecture( Node q );
+  /** initialize guard */
+  void initializeGuard( QuantifiersEngine * qe );
+  /** assign */
+  void assign( Node q );
+  /** is assigned */
+  bool isAssigned() { return !d_quant.isNull(); }
 };
 
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index c9f71b76a..f309ae0cd 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/ce_guided_single_inv.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/ce_guided_single_inv_ei.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
@@ -52,17 +53,31 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje
   }else{
     d_c_inst_match_trie = NULL;
   }
-  CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
+  d_cosi = new CegqiOutputSingleInv( this );
   //  third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity
-  d_cinst = new CegInstantiator( qe, cosi, false, false );
+  d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );   
 
   d_sol = new CegConjectureSingleInvSol( qe );
 
   d_sip = new SingleInvocationPartition;
+  
+  if( options::cegqiSingleInvPartial() ){
+    d_ei = new CegEntailmentInfer( qe, d_sip );
+  }else{
+    d_ei = NULL;
+  }
 }
 
-void CegConjectureSingleInv::getInitialSingleInvLemma( Node guard, std::vector< Node >& lems ) {
+void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) {
+  Assert( d_si_guard.isNull() );
+  //single invocation guard
+  d_si_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+  d_si_guard = d_qe->getValuation().ensureLiteral( d_si_guard );
+  AlwaysAssert( !d_si_guard.isNull() );
+  d_qe->getOutputChannel().requirePhase( d_si_guard, true );
+
   if( !d_single_inv.isNull() ) {
+    //make for new var/sk
     d_single_inv_var.clear();
     d_single_inv_sk.clear();
     Node inst;
@@ -83,8 +98,13 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( Node guard, std::vector<
     Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
 
     //register with the instantiator
-    Node ginst = NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
+    Node ginst = NodeManager::currentNM()->mkNode( OR, d_si_guard.negate(), inst );
     lems.push_back( ginst );
+    //make and register the instantiator
+    if( d_cinst ){
+      delete d_cinst;
+    }
+    d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );   
     d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
   }
 }
@@ -162,13 +182,12 @@ void CegConjectureSingleInv::initialize( Node q ) {
     if( !d_sip->d_conjuncts[1].empty() ){
       singleInvocation = false;
       if( options::cegqiSingleInvPartial() ){
-        /*  TODO : this enables partially single invocation techniques
+        //this enables partially single invocation techniques
         d_nsingle_inv = d_sip->getNonSingleInvocation();
         d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv );
         d_full_inv = d_sip->getFullSpecification();
         d_full_inv = TermDb::simpleNegate( d_full_inv );
         singleInvocation = true;
-        */
       }else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
         //if we are doing invariant templates, then construct the template
         std::map< Node, bool > has_inv;
@@ -287,11 +306,33 @@ void CegConjectureSingleInv::initialize( Node q ) {
       //just invoke the presolve now
       d_cinst->presolve( d_single_inv );
     }
-    if( !d_nsingle_inv.isNull() ){
+    if( !isFullySingleInvocation() ){
       //initialize information as next single invocation conjecture
       initializeNextSiConjecture();
       Trace("cegqi-si") << "Non-single invocation formula is : " << d_nsingle_inv << std::endl;
       Trace("cegqi-si") << "Full specification is : " << d_full_inv << std::endl;
+      //add full specification lemma : will use for testing infeasibility/deriving entailments
+      d_full_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GF", NodeManager::currentNM()->booleanType() ) );
+      d_full_guard = d_qe->getValuation().ensureLiteral( d_full_guard );
+      AlwaysAssert( !d_full_guard.isNull() );
+      d_qe->getOutputChannel().requirePhase( d_full_guard, true );
+      Node fbvl;
+      if( !d_sip->d_all_vars.empty() ){
+        fbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_all_vars );
+      }
+      std::vector< Node > flem_c;
+      for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){
+        Node flemi = d_sip->d_conjuncts[2][i];
+        if( !fbvl.isNull() ){
+          flemi = NodeManager::currentNM()->mkNode( FORALL, fbvl, flemi );
+        }
+        flem_c.push_back( flemi );
+      }
+      Node flem = flem_c.empty() ? d_qe->getTermDatabase()->d_true : ( flem_c.size()==1 ? flem_c[0] : NodeManager::currentNM()->mkNode( AND, flem_c ) );
+      flem = NodeManager::currentNM()->mkNode( OR, d_full_guard.negate(), flem );
+      flem = Rewriter::rewrite( flem );
+      Trace("cegqi-lemma") << "Cegqi::Lemma : full specification " << flem << std::endl;
+      d_qe->getOutputChannel().lemma( flem );
     }
   }else{
     Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
@@ -435,6 +476,23 @@ Node CegConjectureSingleInv::addDeepEmbedding( Node n, std::map< Node, Node >& v
 }
 
 void CegConjectureSingleInv::initializeNextSiConjecture() {
+  Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture..." << std::endl;
+  if( d_single_inv.isNull() ){
+    if( d_ei->getEntailedConjecture( d_single_inv, d_single_inv_exp ) ){
+      Trace("cegqi-nsi") << "NSI : got : " << d_single_inv << std::endl;
+      Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl; 
+    }else{
+      Trace("cegqi-nsi") << "NSI : failed to construct next conjecture." << std::endl;
+      Notice() << "Incomplete due to --cegqi-si-partial." << std::endl;
+      exit( 10 );
+    }
+  }else{
+    //initial call
+    Trace("cegqi-nsi") << "NSI : have : " << d_single_inv << std::endl;
+    Assert( d_single_inv_exp.isNull() );
+  }
+  
+  d_si_guard = Node::null();
   d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) );
   d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard );
   AlwaysAssert( !d_ns_guard.isNull() );
@@ -481,10 +539,6 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){
       Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
       lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem );
     }
-    //add guard if not fully single invocation
-    if( !isFullySingleInvocation() ){
-      lem = NodeManager::currentNM()->mkNode( OR, d_ns_guard.negate(), lem );
-    }
     Trace("cegqi-engine-debug") << "Rewrite..." << std::endl;
     lem = Rewriter::rewrite( lem );
     Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
@@ -554,14 +608,25 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
       }
     }else if( !isFullySingleInvocation() ){
       //create next candidate conjecture
-      Trace("cegqi-nsi") << "NSI : create next candidate conjecture..." << std::endl;
-      exit( 10 );
+      Assert( d_ei!=NULL );
+      //construct d_single_inv
+      d_single_inv = Node::null();
+      initializeNextSiConjecture();
+      return;
     }
     d_curr_lemmas.clear();
     //call check for instantiator
     d_cinst->check();
     //add lemmas
-    lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
+    //add guard if not fully single invocation
+    if( !isFullySingleInvocation() ){
+      Assert( !d_ns_guard.isNull() );
+      for( unsigned i=0; i<d_curr_lemmas.size(); i++ ){
+        lems.push_back( NodeManager::currentNM()->mkNode( OR, d_ns_guard.negate(), d_curr_lemmas[i] ) );
+      }
+    }else{
+      lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index f058cf196..dfa0554d0 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -29,6 +29,7 @@ namespace quantifiers {
 
 class CegConjecture;
 class CegConjectureSingleInv;
+class CegEntailmentInfer;
 
 class CegqiOutputSingleInv : public CegqiOutput
 {
@@ -52,15 +53,15 @@ private:
   QuantifiersEngine * d_qe;
   CegConjecture * d_parent;
   CegConjectureSingleInvSol * d_sol;
+  CegEntailmentInfer * d_ei;
   //the instantiator
+  CegqiOutputSingleInv * d_cosi;
   CegInstantiator * d_cinst;
   //for recognizing templates for invariant synthesis
   Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
   // partially single invocation
   Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, std::map< Node, Node >& visited );
   Node addDeepEmbedding( Node n, std::map< Node, Node >& visited );
-  //initialize next candidate si conjecture
-  void initializeNextSiConjecture();
   //presolve
   void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
   void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
@@ -104,12 +105,15 @@ public:
   Node d_quant;
   // single invocation portion of quantified formula
   Node d_single_inv;
+  Node d_si_guard;
   // non-single invocation portion of quantified formula
   Node d_nsingle_inv;
+  Node d_ns_guard;
   // full version quantified formula
   Node d_full_inv;
-  // current guard
-  Node d_ns_guard;
+  Node d_full_guard;
+  //explanation for current single invocation conjecture
+  Node d_single_inv_exp;  
   // transition relation version per program
   std::map< Node, Node > d_trans_pre;
   std::map< Node, Node > d_trans_post;
@@ -120,7 +124,7 @@ public:
   std::map< Node, Node > d_prog_to_eval_op;
 public:
   //get the single invocation lemma(s)
-  void getInitialSingleInvLemma( Node guard, std::vector< Node >& lems );
+  void getInitialSingleInvLemma( std::vector< Node >& lems );
   //initialize
   void initialize( Node q );
   //check
@@ -134,11 +138,13 @@ public:
   // is single invocation
   bool isSingleInvocation() { return !d_single_inv.isNull(); }
   // is single invocation
-  bool isFullySingleInvocation() { return d_nsingle_inv.isNull(); }
+  bool isFullySingleInvocation() { return !d_single_inv.isNull() && d_nsingle_inv.isNull(); }
   //needs check
   bool needsCheck();
   /** preregister conjecture */
   void preregisterConjecture( Node q );
+  //initialize next candidate si conjecture (if not fully single invocation)
+  void initializeNextSiConjecture();  
 };
 
 // partitions any formulas given to it into single invocation/non-single invocation
diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp
new file mode 100644
index 000000000..18252e190
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file ce_guided_single_inv_ei.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 inferring entailments for cegqi
+ **
+ **/
+
+#include "theory/quantifiers/ce_guided_single_inv_ei.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/quant_util.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+CegEntailmentInfer::CegEntailmentInfer( QuantifiersEngine * qe, SingleInvocationPartition * sip ) : d_qe( qe ), d_sip( sip ) {
+
+}
+
+bool CegEntailmentInfer::getEntailedConjecture( Node& conj, Node& exp ) {
+  if( Trace.isOn("cegqi-ei") ){
+    Trace("cegqi-ei") << "Infer new conjecture from : " << std::endl;
+    d_sip->debugPrint( "cegqi-ei" );
+    Trace("cegqi-ei") << "Current assertions : " << std::endl;
+    d_qe->getTheoryEngine()->printAssertions("cegqi-ei");
+  }
+  
+  
+  return false;
+}
+
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.h b/src/theory/quantifiers/ce_guided_single_inv_ei.h
new file mode 100644
index 000000000..0645c406a
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_single_inv_ei.h
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file ce_guided_single_inv_ei.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 inferring entailments for cegqi
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_ENTAILMENT_INFERENCE_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_ENTAILMENT_INFERENCE_H
+
+
+#include "theory/quantifiers/ce_guided_single_inv.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+  
+class CegEntailmentInfer {
+private:
+  QuantifiersEngine * d_qe;
+  SingleInvocationPartition * d_sip;
+public:
+  CegEntailmentInfer( QuantifiersEngine * qe, SingleInvocationPartition * sip );
+  virtual ~CegEntailmentInfer(){}
+  
+  bool getEntailedConjecture( Node& conj, Node& exp );
+};
+
+
+}
+}
+}
+
+#endif