From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 24 Mar 2020 15:45:55 +0000 (-0500)
Subject: Restrict partial triggers to standard quantified formulas (#4144)
X-Git-Tag: cvc5-1.0.0~3450
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e648859c74339fb1b5838c6d439e9dfa1f490bcc;p=cvc5.git

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 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 );