diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 17:34:23 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 17:34:23 -0500 |
| commit | 2bf0735176e0ff5fb9720bfb255ca22443584dcc (patch) | |
| tree | 16926686e86f182e383efd8153b7d0e11bbc694a /src/theory/quantifiers/model_engine.cpp | |
| parent | b48a369333f077fa7cce117976f760cd6332691a (diff) | |
Significant work on bounded integer quantification to handle non-trivial bounds. Refactoring of InstConstantAttribute to be internal to TermDb.
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index b9dcef282..c91d9d3ab 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -187,7 +187,7 @@ int ModelEngine::checkModel(){ d_relevantLemmas = 0; d_totalLemmas = 0; Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - int e_max = options::fmfFullModelCheck() ? 2 : 1; + int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1; for( int e=0; e<e_max; e++) { if (addedLemmas==0) { for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ @@ -238,8 +238,8 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } Debug("inst-fmf-ei") << std::endl; //create a rep set iterator and iterate over the (relevant) domain of the quantifier - RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); - if( riter.setQuantifier( d_quantEngine, f ) ){ + RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); + if( riter.setQuantifier( f ) ){ Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; d_quantEngine->getModel()->resetEvaluate(); Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; |