From 59b935c1af18ec51efacf87b0e45d9134d3aaa1e Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2016 09:38:41 -0500
Subject: Refactor trigger selection, revisions to --relational-trigger.
 Properly process non-standard user-provided triggers. Avoid entailed
 instantiations based on equality earlier. Refactor core addInstantiation
 method, add notification mechanism. Add optional argument to entailment
 checks. Fix bug for duplicate triggers.

---
 src/theory/quantifiers/quantifiers_rewriter.cpp | 26 ++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

(limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 79c300401..5aae4d640 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -244,17 +244,21 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
     ret = ret.negate();
     status = REWRITE_AGAIN_FULL;
   }else if( in.getKind()==FORALL ){
-    //compute attributes
-    QAttributes qa;
-    TermDb::computeQuantAttributes( in, qa );
-    if( !qa.isRewriteRule() ){
-      for( int op=0; op<COMPUTE_LAST; op++ ){
-        if( doOperation( in, op, qa ) ){
-          ret = computeOperation( in, op, qa );
-          if( ret!=in ){
-            rew_op = op;
-            status = REWRITE_AGAIN_FULL;
-            break;
+    if( in[1].isConst() ){
+      return RewriteResponse( status, in[1] );
+    }else{
+      //compute attributes
+      QAttributes qa;
+      TermDb::computeQuantAttributes( in, qa );
+      if( !qa.isRewriteRule() ){
+        for( int op=0; op<COMPUTE_LAST; op++ ){
+          if( doOperation( in, op, qa ) ){
+            ret = computeOperation( in, op, qa );
+            if( ret!=in ){
+              rew_op = op;
+              status = REWRITE_AGAIN_FULL;
+              break;
+            }
           }
         }
       }
-- 
cgit v1.2.3