diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-10 15:20:33 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-10 15:20:41 -0500 |
| commit | 5e4ed407978b892e04de00994be535f58fb33257 (patch) | |
| tree | 5ff2dfbf18845113c5ea0fa43e8792532498d2ec /src/theory/quantifiers/full_model_check.cpp | |
| parent | c833e176a81eb193462c0efde0c6c2f28c5159fb (diff) | |
More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index d06e9f7f7..0276cf7ab 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -591,6 +591,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; + Assert( !d_qe->inConflict() ); if( optUseModel() ){ FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc(); if (effort==0) { @@ -684,7 +685,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; - if( options::fmfOneInstPerRound() ){ + if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ break; } }else{ @@ -812,7 +813,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-exh-debug") << " ...success."; addedLemmas++; - if( options::fmfOneInstPerRound() ){ + if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ break; } }else{ |