From: Andrew Reynolds Date: Wed, 4 Sep 2019 19:45:21 +0000 (-0500) Subject: Move getCounterexampleLiteral out of term utilities (#3238) X-Git-Tag: cvc5-1.0.0~3980 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9ee2ae563b031547e76245d9f01fb24b95bc8cb;p=cvc5.git Move getCounterexampleLiteral out of term utilities (#3238) --- diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 0f866208d..ab5bbc25f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -93,7 +93,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; //add cbqi lemma //get the counterexample literal - Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + Node ceLit = getCounterexampleLiteral(q); Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q ); if( !ceBody.isNull() ){ //add counterexample lemma @@ -148,7 +148,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) d_parent_quant[q].push_back( qi ); d_children_quant[qi].push_back( q ); Assert( hasAddedCbqiLemma( qi ) ); - Node qicel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( qi ); + Node qicel = getCounterexampleLiteral(qi); dep.push_back( qi ); dep.push_back( qicel ); } @@ -220,7 +220,7 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ d_active_quant[q] = true; Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; - Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + Node cel = getCounterexampleLiteral(q); bool value; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; @@ -620,6 +620,21 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { } } +Node InstStrategyCegqi::getCounterexampleLiteral(Node q) +{ + std::map::iterator it = d_ce_lit.find(q); + if (it != d_ce_lit.end()) + { + return it->second; + } + NodeManager * nm = NodeManager::currentNM(); + Node g = nm->mkSkolem("g", nm->booleanType()); + // ensure that it is a SAT literal + Node ceLit = d_quantEngine->getValuation().ensureLiteral(g); + d_ce_lit[q] = ceLit; + return ceLit; +} + bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index c6a9ddd11..ecae4ab64 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -171,6 +171,15 @@ class InstStrategyCegqi : public QuantifiersModule bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } /** process functions */ void process(Node q, Theory::Effort effort, int e); + /** + * Get counterexample literal. This is the fresh Boolean variable whose + * semantics is "there exists a set of values for which the body of + * quantified formula q does not hold". These literals are cached by this + * class. + */ + Node getCounterexampleLiteral(Node q); + /** map from universal quantifiers to their counterexample literals */ + std::map d_ce_lit; //for identification uint64_t d_qid_count; diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 94bc2c3f8..ffd808ed3 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -200,26 +200,6 @@ Node TermUtil::getInstConstantBody( Node q ){ } } -Node TermUtil::getCounterexampleLiteral( Node q ){ - if( d_ce_lit.find( q )==d_ce_lit.end() ){ - /* - Node ceBody = getInstConstantBody( f ); - //check if any variable are of bad types, and fail if so - for( size_t i=0; imkSkolem( "g", NodeManager::currentNM()->booleanType() ); - //otherwise, ensure literal - Node ceLit = d_quantEngine->getValuation().ensureLiteral( g ); - d_ce_lit[ q ] = ceLit; - } - return d_ce_lit[ q ]; -} - Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q) { registerQuantifier( q ); diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 302901625..b39a4e129 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -125,8 +125,6 @@ public: std::map< Node, std::map< Node, unsigned > > d_var_num; /** map from universal quantifiers to their inst constant body */ std::map< Node, Node > d_inst_const_body; - /** map from universal quantifiers to their counterexample literals */ - std::map< Node, Node > d_ce_lit; /** instantiation constants to universal quantifiers */ std::map< Node, Node > d_inst_constants_map; public: @@ -140,8 +138,6 @@ public: unsigned getNumInstantiationConstants( Node q ) const; /** get the ce body q[e/x] */ Node getInstConstantBody( Node q ); - /** get counterexample literal (for cbqi) */ - Node getCounterexampleLiteral( Node q ); /** returns node n with bound vars of q replaced by instantiation constants of q node n : is the future pattern node q : is the quantifier containing which bind the variable