diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-16 13:57:53 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-16 13:57:53 -0500 |
| commit | eb27070783709a410e6655ba9af6da6de5b0da9d (patch) | |
| tree | c4fcb9203e2e72c9a96a51641ac15207f292a75b /src/theory/quantifiers/model_engine.cpp | |
| parent | fd3844131f334e929bfb04eb2dcb6229cf1190cd (diff) | |
Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification.
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 4b173c833..70ee01b92 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -274,7 +274,7 @@ 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 incomplete=" << riter.d_incomplete << "..." << std::endl; + Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl; if( !riter.d_incomplete ){ int triedLemmas = 0; int addedLemmas = 0; @@ -299,6 +299,7 @@ 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 ); } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round |