diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-26 10:04:34 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-26 10:04:34 +0200 |
| commit | e61a79df77924c66e8f6ff3141172bda49301475 (patch) | |
| tree | 1b33e1d054bd3ac948d9bd47a0ea825bca724cea /src/theory/quantifiers/model_engine.cpp | |
| parent | 773963f4342bb860fe4deb1d3c65d801b6acd72f (diff) | |
Better organization of quantifiers modules, promote full saturation to module. Add heuristics for cbqi LIA instantiation with coefficients.
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 752e88c5a..a3a18cf30 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -265,7 +265,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ 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; - if( !riter.d_incomplete || options::fmfFullSaturate() ){ + if( !riter.d_incomplete ){ int triedLemmas = 0; int addedLemmas = 0; while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ |