diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-24 10:45:55 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-24 10:45:55 -0500 |
commit | e648859c74339fb1b5838c6d439e9dfa1f490bcc (patch) | |
tree | 0a76e78af2a2e67d6503514efd0a016bb5965904 /src/theory/quantifiers | |
parent | d6f99b015e8879229b8599316e19b5467863db2f (diff) |
Restrict partial triggers to standard quantified formulas (#4144)
Fixes #4143.
Diffstat (limited to 'src/theory/quantifiers')
-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 ); |