diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-01 13:09:49 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-01 13:11:13 +0200 |
commit | 3ac872f4a3f65bd1b38c1362b8ca9d351ed89333 (patch) | |
tree | c62a424af1b419155af0f59612d376fc10e7a6b6 /src/theory/quantifiers/instantiation_engine.cpp | |
parent | 9350915de95c1b569eea8262c4602708dfa6c3fa (diff) |
Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun-def. Add skolemization options.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 9c3035c85..cb01fd373 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -143,9 +143,9 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //check each instantiation strategy for( size_t i=0; i<d_instStrategies.size(); ++i ){ InstStrategy* is = d_instStrategies[i]; - Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; + Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; int quantStatus = is->process( f, effort, e_use ); - Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl; + Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl; if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ finished = false; } @@ -185,11 +185,14 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); + Debug("quantifiers") << "Process " << n << "..." << std::endl; //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( !d_quantEngine->hasOwnership( n, this ) ){ d_quant_active[n] = false; + Debug("quantifiers") << " Quantifier has owner." << std::endl; }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){ d_quant_active[n] = false; + Debug("quantifiers") << " Quantifier is not active (from model)." << std::endl; //it is not active if we have found the skolemized negation is unsat }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n ); |