From: ajreynol Date: Wed, 2 Dec 2015 16:45:07 +0000 (+0100) Subject: Minor fixes for cegqi-si-partial. X-Git-Tag: cvc5-1.0.0~6152 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e045d50c0c0f65d44868fead684094746df70108;p=cvc5.git Minor fixes for cegqi-si-partial. --- 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; igetOutputChannel().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; igetValuation().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; jaddLemma( lems[j] ); + if( conj->d_ceg_si->check( lems ) ){ + if( !lems.empty() ){ + d_last_inst_si = true; + for( unsigned j=0; jaddLemma( 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; id_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