diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-18 20:42:55 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-18 20:42:55 -0500 |
commit | 236337b3df1fa6c7627537f0d783d3d3f568b068 (patch) | |
tree | aee0ee98181375af32ad082ae727a55f8a10f9f6 /src/theory/quantifiers/cegqi | |
parent | f1b58cf3d090d252e9349d491c4b43c46bf52b0e (diff) |
Always enable cbqi literal dependency (#4116)
Fixes #4105.
It appears that the two (experimental) options in that issue were incompatible.
A block of code changed indentation in this PR and was updated to guidelines.
Diffstat (limited to 'src/theory/quantifiers/cegqi')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 48 |
1 files changed, 26 insertions, 22 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 4f670bef4..dafcc365e 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -94,6 +94,7 @@ QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e) bool InstStrategyCegqi::registerCbqiLemma(Node q) { if( !hasAddedCbqiLemma( q ) ){ + NodeManager* nm = NodeManager::currentNM(); d_added_cbqi_lemma.insert( q ); Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; //add cbqi lemma @@ -141,30 +142,33 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) } //compute dependencies between quantified formulas - if( options::cbqiLitDepend() || options::cbqiInnermost() ){ - std::vector< Node > ics; - TermUtil::computeInstConstContains(q, ics); - d_parent_quant[q].clear(); - d_children_quant[q].clear(); - std::vector< Node > dep; - for( unsigned i=0; i<ics.size(); i++ ){ - Node qi = ics[i].getAttribute(InstConstantAttribute()); - if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){ - d_parent_quant[q].push_back( qi ); - d_children_quant[qi].push_back( q ); - Assert(hasAddedCbqiLemma(qi)); - Node qicel = getCounterexampleLiteral(qi); - dep.push_back( qi ); - dep.push_back( qicel ); - } - } - if( !dep.empty() ){ - Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) ); - Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; - d_quantEngine->getOutputChannel().lemma( dep_lemma ); + std::vector<Node> ics; + TermUtil::computeInstConstContains(q, ics); + d_parent_quant[q].clear(); + d_children_quant[q].clear(); + std::vector<Node> dep; + for (const Node& ic : ics) + { + Node qi = ic.getAttribute(InstConstantAttribute()); + if (std::find(d_parent_quant[q].begin(), d_parent_quant[q].end(), qi) + == d_parent_quant[q].end()) + { + d_parent_quant[q].push_back(qi); + d_children_quant[qi].push_back(q); + Assert(hasAddedCbqiLemma(qi)); + Node qicel = getCounterexampleLiteral(qi); + dep.push_back(qi); + dep.push_back(qicel); } } - + if (!dep.empty()) + { + Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep)); + Trace("cbqi-lemma") + << "Counterexample dependency lemma : " << dep_lemma << std::endl; + d_quantEngine->getOutputChannel().lemma(dep_lemma); + } + //must register all sub-quantifiers of counterexample lemma, register their lemmas std::vector< Node > quants; TermUtil::computeQuantContains( lem, quants ); |