diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rwxr-xr-x[-rw-r--r--] | src/theory/quantifiers/model_engine.cpp | 56 |
1 files changed, 26 insertions, 30 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 0bbca88eb..5d575969f 100644..100755 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -153,27 +153,23 @@ int ModelEngine::checkModel(){ //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps ); //for debugging - if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){ - for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); - it != fm->d_rep_set.d_type_reps.end(); ++it ){ - if( it->first.isSort() ){ - Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - if( Trace.isOn("model-engine-debug") ){ - Trace("model-engine-debug") << " Reps : "; - for( size_t i=0; i<it->second.size(); i++ ){ - Trace("model-engine-debug") << it->second[i] << " "; - } - Trace("model-engine-debug") << std::endl; - Trace("model-engine-debug") << " Term reps : "; - for( size_t i=0; i<it->second.size(); i++ ){ - Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); - Trace("model-engine-debug") << r << " "; - } - Trace("model-engine-debug") << std::endl; - Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); - Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; - } + for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); + it != fm->d_rep_set.d_type_reps.end(); ++it ){ + if( it->first.isSort() ){ + Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + Trace("model-engine-debug") << " Reps : "; + for( size_t i=0; i<it->second.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; } + Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Term reps : "; + for( size_t i=0; i<it->second.size(); i++ ){ + Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); + Trace("model-engine-debug") << r << " "; + } + Trace("model-engine-debug") << std::endl; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; } } @@ -221,11 +217,12 @@ int ModelEngine::checkModel(){ //print debug information if( d_quantEngine->inConflict() ){ - Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl; + Trace("model-engine") << "Conflict, added lemmas = "; }else{ - Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; - Trace("model-engine") << d_totalLemmas << std::endl; - } + Trace("model-engine") << "Added Lemmas = "; + } + Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_totalLemmas << std::endl; return d_addedLemmas; } @@ -281,15 +278,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //create a rep set iterator and iterate over the (relevant) domain of the quantifier RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ - Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl; - if( !riter.d_incomplete ){ + Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl; + if( !riter.isIncomplete() ){ int triedLemmas = 0; int addedLemmas = 0; while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m( f ); for( int i=0; i<riter.getNumTerms(); i++ ){ - m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) ); + m.set( d_quantEngine, i, riter.getCurrentTerm( i ) ); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; @@ -309,11 +306,10 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ d_statistics.d_exh_inst_lemmas += addedLemmas; } }else{ - Trace("fmf-exh-inst") << "...exhaustive instantiation failed to set, incomplete=" << riter.d_incomplete << "..." << std::endl; - Assert( riter.d_incomplete ); + Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl; } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = d_incomplete_check || riter.d_incomplete; + d_incomplete_check = d_incomplete_check || riter.isIncomplete(); } } |