From 3b016602db8b9beb1f28f144979ab98beb119a59 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 30 Mar 2013 17:29:34 -0500
Subject: [PATCH] do simple ite rewriting within quantifiers

---
 .../quantifiers/quantifiers_rewriter.cpp      | 41 +++++++++++++++++++
 src/theory/quantifiers/quantifiers_rewriter.h |  2 +
 2 files changed, 43 insertions(+)

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index bf6a025f8..35ab3e647 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -273,6 +273,43 @@ Node QuantifiersRewriter::computeNNF( Node body ){
   }
 }
 
+Node QuantifiersRewriter::computeSimpleIteLift( Node body ) {
+  if( body.getKind()==EQUAL ){
+    for( size_t i=0; i<2; i++ ){
+      if( body[i].getKind()==ITE ){
+        Node no = i==0 ? body[1] : body[0];
+        bool doRewrite = false;
+        std::vector< Node > children;
+        children.push_back( body[i][0] );
+        for( size_t j=1; j<=2; j++ ){
+          //check if it rewrites to a constant
+          Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
+          nn = Rewriter::rewrite( nn );
+          children.push_back( nn );
+          if( nn.isConst() ){
+            doRewrite = true;
+          }
+        }
+        if( doRewrite ){
+          return NodeManager::currentNM()->mkNode( ITE, children );
+        }
+      }
+    }
+  }else if( body.getKind()!=APPLY_UF && body.getType()==NodeManager::currentNM()->booleanType() ){
+    bool changed = false;
+    std::vector< Node > children;
+    for( size_t i=0; i<body.getNumChildren(); i++ ){
+      Node nn = computeSimpleIteLift( body[i] );
+      children.push_back( nn );
+      changed = changed || nn!=body[i];
+    }
+    if( changed ){
+      return NodeManager::currentNM()->mkNode( body.getKind(), children );
+    }
+  }
+  return body;
+}
+
 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
   Trace("var-elim-quant") << "Compute var elimination for " << body << std::endl;
   QuantPhaseReq qpr( body );
@@ -521,6 +558,8 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
       return computeAggressiveMiniscoping( args, n, f.hasAttribute(NestedQuantAttribute()) );
     }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
+    }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
+      n = computeSimpleIteLift( n );
     }else if( computeOption==COMPUTE_PRENEX ){
       n = computePrenex( n, args, true );
     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
@@ -771,6 +810,8 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
     return options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_NNF ){
     return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
+  }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
+    return true;
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 75b392e15..73f5d391f 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -46,6 +46,7 @@ private:
   static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false );
   static Node computeNNF( Node body );
+  static Node computeSimpleIteLift( Node body );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
@@ -54,6 +55,7 @@ private:
     COMPUTE_MINISCOPING = 0,
     COMPUTE_AGGRESSIVE_MINISCOPING,
     COMPUTE_NNF,
+    COMPUTE_SIMPLE_ITE_LIFT,
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
     //COMPUTE_FLATTEN_ARGS_UF,
-- 
2.30.2