diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-28 01:57:20 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-28 01:57:20 -0600 |
| commit | c5d1a5d8f898bf22c6bbc98f1d484b07706c035b (patch) | |
| tree | 49b5cc92ea74d720178d60bab2837bf897559813 /src/theory/quantifiers/instantiation_engine.cpp | |
| parent | bcbf52ffbe0416ecf70bdb644017c338c0540793 (diff) | |
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 653016d1c..53977ee4f 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -48,8 +48,8 @@ void InstantiationEngine::finishInit(){ }else{ d_isup = NULL; } - InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, - InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 ); + int rlv = options::relevantTriggers() ? InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT : InstStrategyAutoGenTriggers::RELEVANCE_NONE; + InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, rlv, 3 ); i_ag->setGenerateAdditional( true ); addInstStrategy( i_ag ); //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) ); |