New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.

1 files changed, 11 insertions, 6 deletions

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 16a9d3bc7..8abc3f65a 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -54,12 +54,17 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE
     aen->d_quant = q;
     return true;
   }else{
-    //lemma ( q <=> d_quant )
-    Trace("quant-ae") << "Alpha equivalent : " << std::endl;
-    Trace("quant-ae") << "  " << q << std::endl;
-    Trace("quant-ae") << "  " << aen->d_quant << std::endl;
-    qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
-    return false;
+    if( q.getNumChildren()==2 ){
+      //lemma ( q <=> d_quant )
+      Trace("quant-ae") << "Alpha equivalent : " << std::endl;
+      Trace("quant-ae") << "  " << q << std::endl;
+      Trace("quant-ae") << "  " << aen->d_quant << std::endl;
+      qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
+      return false;
+    }else{
+      //do not reduce annotated quantified formulas based on alpha equivalence 
+      return true;
+    }
   }
 }