diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 40216f7c9..46216a17d 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -360,7 +360,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( d_num_trigger_vars[f]>0 && d_num_trigger_vars[f]<f[0].getNumChildren() ){ Trace("auto-gen-trigger-partial") << "Quantified formula : " << f << std::endl; Trace("auto-gen-trigger-partial") << "...does not contain all variables in triggers!!!" << std::endl; - if( options::partialTriggers() ){ + // Invoke partial trigger strategy: partition variables of quantified + // formula into (X,Y) where X are contained in a trigger and Y are not. + // We then force a split of the quantified formula so that it becomes: + // forall X. forall Y. P( X, Y ) + // and hence is treatable by E-matching. We only do this for "standard" + // quantified formulas (those with only two children), since this + // technique should not be used for e.g. quantifiers marked for + // quantifier elimination. + QAttributes qa; + QuantAttributes::computeQuantAttributes(f, qa); + if (options::partialTriggers() && qa.isStandard()) + { std::vector< Node > vcs[2]; for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ); |