diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
commit | f62d9456b41bf17df1d339e46776c9213cb3705a (patch) | |
tree | 01d3448b3c9fe89ead56c72b18f8516292092e13 /src/theory/quantifiers/ce_guided_instantiation.cpp | |
parent | 7943953741c67d8246f983e193d26812d959b4cd (diff) |
Squashed merge of SygusComp 2015 branch.
Diffstat (limited to 'src/theory/quantifiers/ce_guided_instantiation.cpp')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 56 |
1 files changed, 33 insertions, 23 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 5f3498f49..045407bf0 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -70,7 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ - if( d_guard.isNull() ){ + 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 ); @@ -137,6 +137,10 @@ bool CegConjecture::isSingleInvocation() { return d_ceg_si->isSingleInvocation(); } +bool CegConjecture::needsCheck() { + return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() ); +} + CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ d_conj = new CegConjecture( qe->getSatContext() ); d_last_inst_si = false; @@ -155,7 +159,7 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("cegqi-engine-debug") << std::endl; Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl; - if( d_conj->d_active && !d_conj->d_infeasible ){ + if( d_conj->needsCheck() ){ checkCegConjecture( d_conj ); } Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; @@ -213,29 +217,32 @@ void CegInstantiation::assertNode( Node n ) { } Node CegInstantiation::getNextDecisionRequest() { - d_conj->initializeGuard( d_quantEngine ); - bool value; - if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { - //if( d_conj->d_guard_split.isNull() ){ - // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); - // d_quantEngine->getOutputChannel().lemma( lem ); - //} - Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; - return d_conj->d_guard; - } //enforce fairness - if( d_conj->isAssigned() && d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ - Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); - if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { - if( !value ){ - d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); - lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); - Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + if( d_conj->isAssigned() ){ + d_conj->initializeGuard( d_quantEngine ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { + //if( d_conj->d_guard_split.isNull() ){ + // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); + // d_quantEngine->getOutputChannel().lemma( lem ); + //} + Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; + return d_conj->d_guard; + } + + if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ + Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { + if( !value ){ + d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); + lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + return lit; + } + }else{ + Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; return lit; } - }else{ - Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; - return lit; } } @@ -484,7 +491,8 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le } void CegInstantiation::printSynthSolution( std::ostream& out ) { - if( d_conj ){ + if( d_conj->isAssigned() ){ + Trace("cegqi-debug") << "Printing synth solution..." << std::endl; //if( !(Trace.isOn("cegqi-stats")) ){ // out << "Solution:" << std::endl; //} @@ -530,6 +538,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { out << ")" << std::endl; } } + }else{ + Assert( false ); } } |