From 44d9a7c29f565dbba0baea3f9df23d6d3e5bd74f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 6 Mar 2013 10:46:07 -0600 Subject: fixed two bugs for the new E-matching implementation, added aggressive miniscoping option --ag-miniscope-quant, minor cleanup --- src/theory/quantifiers/model_engine.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/theory/quantifiers/model_engine.cpp') 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; igetTermDatabase()->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; -- cgit v1.2.3