From: ajreynol Date: Sat, 1 Nov 2014 15:05:49 +0000 (+0100) Subject: Fix cegqi for synthesis without syntax. X-Git-Tag: cvc5-1.0.0~6530 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=442b8f2c7070321aa167d9454f92bd1be88fe0cc;p=cvc5.git Fix cegqi for synthesis without syntax. --- diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 2ec15f538..5c7b31d33 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -47,6 +47,12 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ d_guard = qe->getValuation().ensureLiteral( d_guard ); AlwaysAssert( !d_guard.isNull() ); qe->getOutputChannel().requirePhase( d_guard, true ); + if( !d_syntax_guided ){ + //add immediate lemma + 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 ); + } } } @@ -109,10 +115,11 @@ void CegInstantiation::registerQuantifier( Node q ) { for( unsigned j=0; jd_base_inst[0][0].getNumChildren(); j++ ){ d_conj->d_inner_vars.push_back( d_conj->d_base_inst[0][0][j] ); } + d_conj->d_syntax_guided = true; }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ - //add immediate lemma - Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_base_inst ); - d_quantEngine->getOutputChannel().lemma( lem ); + d_conj->d_syntax_guided = false; + }else{ + Assert( false ); } //fairness if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){ @@ -233,11 +240,14 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ + Trace("cegqi-engine") << " * Value is : "; std::vector< Node > model_terms; for( unsigned i=0; id_candidates.size(); i++ ){ Node t = getModelTerm( conj->d_candidates[i] ); model_terms.push_back( t ); + Trace("cegqi-engine") << t << " "; } + Trace("cegqi-engine") << std::endl; d_quantEngine->addInstantiation( q, model_terms, false ); } }else{ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 2502416bd..67125a8ad 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -44,6 +44,8 @@ private: Node d_base_inst; /** 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 */