Minor fixes for cegqi-si-partial.

3 files changed, 40 insertions, 24 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index dcbfba3ff..398ae1ffe 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -238,9 +238,10 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
     if( active && d_conj->needsCheck( lem ) ){
       checkCegConjecture( d_conj );
     }else{
+      Trace("cegqi-engine-debug") << "...does not need check." << std::endl;
       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] );
+        d_quantEngine->addLemma( lem[i] );
       }
     }
     Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
@@ -292,20 +293,21 @@ Node CegInstantiation::getNextDecisionRequest() {
   if( d_conj->isAssigned() ){
     d_conj->initializeGuard( d_quantEngine );
     std::vector< Node > req_dec;
-    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 );
-      }
+    if( !d_conj->d_ceg_si->d_full_guard.isNull() ){
+      req_dec.push_back( d_conj->d_ceg_si->d_full_guard );
     }
+    //must decide ns guard before s guard
+    if( !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() );
     for( unsigned i=0; i<req_dec.size(); i++ ){
       bool value;
       if( !d_quantEngine->getValuation().hasSatValue( req_dec[i], value ) ) {
         Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl;
         return req_dec[i];
+      }else{
+        Trace("cegqi-debug") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl;
       }
     }
 
@@ -347,15 +349,16 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
     if( conj->d_syntax_guided ){
       if( conj->d_ceg_si ){
         std::vector< Node > lems;
-        conj->d_ceg_si->check( lems );
-        if( !lems.empty() ){
-          d_last_inst_si = true;
-          for( unsigned j=0; j<lems.size(); j++ ){
-            Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << lems[j] << std::endl;
-            d_quantEngine->addLemma( lems[j] );
+        if( conj->d_ceg_si->check( lems ) ){
+          if( !lems.empty() ){
+            d_last_inst_si = true;
+            for( unsigned j=0; j<lems.size(); j++ ){
+              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();
+            Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
           }
-          d_statistics.d_cegqi_si_lemmas += lems.size();
-          Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
           return;
         }
       }
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index f309ae0cd..f533a2bbb 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -320,6 +320,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
       if( !d_sip->d_all_vars.empty() ){
         fbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_all_vars );
       }
+      //should construct this conjunction directly since miniscoping is disabled
       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];
@@ -504,7 +505,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() {
   }else{
     d_inst_match_trie.clear();
   }
-  Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture, guard = " << d_ns_guard << std::endl;
+  Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture, ns guard = " << d_ns_guard << std::endl;
   Trace("cegqi-nsi") << "NSI : conjecture is " << d_single_inv << std::endl;
 }
 
@@ -561,7 +562,7 @@ bool CegConjectureSingleInv::addLemma( Node n ) {
   return true;
 }
 
-void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
+bool CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   if( !d_single_inv.isNull() ) {
     if( !d_ns_guard.isNull() ){
       //if partially single invocation, check if we have constructed a candidate by refutation
@@ -596,9 +597,18 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
             subs.push_back( NodeManager::currentNM()->mkSkolem( "kv", d_sip->d_all_vars[i].getType(), "created for verifying nsi" ) );
           }
           inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() );
-          Trace("cegqi-nsi") << "NSI : verification lemma : " << inst << std::endl;
-          lems.push_back( inst );
-          return;
+          Trace("cegqi-nsi") << "NSI : verification : " << inst << std::endl;
+          Trace("cegqi-lemma") << "Cegqi::Lemma : verification lemma : " << inst << std::endl;
+          d_qe->addLemma( inst );
+          /*
+          Node finst = d_sip->getFullSpecification();
+          finst = finst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() );
+          Trace("cegqi-nsi") << "NSI : check refinement : " << finst << std::endl;
+          Node finst_lem = NodeManager::currentNM()->mkNode( OR, d_full_guard.negate(), finst );
+          Trace("cegqi-lemma") << "Cegqi::Lemma : verification, refinement lemma : " << inst << std::endl;
+          d_qe->addLemma( finst_lem );
+          */
+          return true;
         }else{
           //currently trying to construct candidate by refutation (by d_cinst->check below)
         }
@@ -612,7 +622,7 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
       //construct d_single_inv
       d_single_inv = Node::null();
       initializeNextSiConjecture();
-      return;
+      return true;
     }
     d_curr_lemmas.clear();
     //call check for instantiator
@@ -627,6 +637,9 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
     }else{
       lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
     }
+    return !lems.empty();
+  }else{
+    return false;
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index dfa0554d0..c414a51bd 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -128,7 +128,7 @@ public:
   //initialize
   void initialize( Node q );
   //check
-  void check( std::vector< Node >& lems );
+  bool check( std::vector< Node >& lems );
   //get solution
   Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus = true );
   //reconstruct to syntax