Restrict partial triggers to standard quantified formulas (#4144)

Fixes #4143.

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 40216f7c9d5fb68417dcaba623789d2ba1c9d639..46216a17d48aa91b3d01f228a6971e47112378c3 100644 (file)
--- 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 );