diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-03-06 10:46:07 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-03-06 10:46:19 -0600 |
| commit | 44d9a7c29f565dbba0baea3f9df23d6d3e5bd74f (patch) | |
| tree | f9a0b47038e393553a2d6a315138ae8b128915a1 /src/theory/quantifiers/model_engine.cpp | |
| parent | 66b99ac64a6920787905948315e74ca1c5b3e90b (diff) | |
fixed two bugs for the new E-matching implementation, added aggressive miniscoping option --ag-miniscope-quant, minor cleanup
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 39377d11c..1522d0828 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -224,7 +224,7 @@ int ModelEngine::checkModel( int checkOption ){ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ int addedLemmas = 0; - Debug("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl; + Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl; Debug("inst-fmf-ei") << " Instantiation Constants: "; for( size_t i=0; i<f[0].getNumChildren(); i++ ){ Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; @@ -298,12 +298,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ relevantInst = relevantInst * (int)riter.d_domain[i].size(); } d_relevantLemmas += relevantInst; - Debug("inst-fmf-ei") << "Finished: " << std::endl; + Trace("inst-fmf-ei") << "Finished: " << std::endl; //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; - Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; - Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; - Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; - Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl; + Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; + Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; + Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; + Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl; if( addedLemmas>1000 ){ Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl; |