diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-15 09:09:51 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-15 09:09:51 +0200 |
commit | 3ce21ef9a8b6daa1eef1dbe9af10a84e8c87e413 (patch) | |
tree | 2686fa03573e19593e3395d4097ce1e7943ba04a /src/theory/quantifiers/instantiation_engine.cpp | |
parent | e7439fc0daf1049f59540b9aeb890a52d86a77bd (diff) |
Avoid ensureLiteral on unpreprocessed formulas in cbqi.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 12d6bed8d..f530f7b9d 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -95,21 +95,20 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){ d_added_cbqi_lemma[f] = true; - Debug("cbqi") << "Do cbqi for " << f << std::endl; + Trace("cbqi") << "Do cbqi for " << f << std::endl; //add cbqi lemma //get the counterexample literal Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); - if( !ceLit.isNull() ){ + Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); + if( !ceBody.isNull() ){ + //add counterexample lemma + Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); //require any decision on cel to be phase=true - //d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); d_quantEngine->addRequirePhase( ceLit, true ); Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; //add counterexample lemma - NodeBuilder<> nb(kind::OR); - nb << f << ceLit; - Node lem = nb; + lem = Rewriter::rewrite( lem ); Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - //d_quantEngine->getOutputChannel().lemma( lem, false, true ); d_quantEngine->addLemma( lem, false ); addedLemma = true; } @@ -125,7 +124,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ InstStrategy* is = d_instStrategies[i]; is->processResetInstantiationRound( effort ); } - + //iterate over an internal effort level e int e = 0; int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2; |