diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-13 18:43:40 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-13 18:43:40 -0600 |
| commit | 36f18a81d18fbfe063ec36cc101ff4ba1c069ea2 (patch) | |
| tree | f43d1b4f6ecf27f6b70c03938ee1b19a44fa7c41 /src/theory/quantifiers/model_engine.cpp | |
| parent | c5e230e012c57a4605e99a165934afc98bc4d9fc (diff) | |
(Refactor) Decouple rep set iterator and quantifiers (#1339)
* Refactoring rep set iterator, does not modify rep set externally.
* Decouple quantifiers engine and rep set iterator.
* Documentation
* Clang format
* Minor
* Minor
* More
* Format
* Address review.
* Format
* Minor
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 88b16bfd3..c4a0b5c5d 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -277,8 +277,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ Trace("fmf-exh-inst-debug") << std::endl; } //create a rep set iterator and iterate over the (relevant) domain of the quantifier - RepSetIterator riter(d_quantEngine, - d_quantEngine->getModel()->getRepSetPtr()); + QRepBoundExt qrbe(d_quantEngine); + RepSetIterator riter(d_quantEngine->getModel()->getRepSet(), &qrbe); if( riter.setQuantifier( f ) ){ Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl; if( !riter.isIncomplete() ){ @@ -287,7 +287,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ 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++ ){ + for (unsigned i = 0; i < riter.getNumTerms(); i++) + { m.set( d_quantEngine, i, riter.getCurrentTerm( i ) ); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; |