From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 17 Apr 2013 00:49:25 +0000 (-0400)
Subject: generalize to handle and
X-Git-Tag: cvc5-1.0.0~7321
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8bde75053b59023c2c4b911b83666d48fa6056d9;p=cvc5.git

generalize to handle and
---

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index c9615d9cd..b8a874209 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -22,12 +22,25 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-RewriteResponse flattenOrNode(TNode n, TNode trueNode, TNode falseNode)
+/**
+ * flattenNode looks for children of same kind, and if found merges
+ * them into the parent.
+ *
+ * It simultaneously handles a couple of other optimizations: 
+ * - trivialNode - if found during exploration, return that node itself
+ *    (like in case of OR, if "true" is found, makes sense to replace
+ *     whole formula with "true")
+ * - skipNode - as name suggests, skip them
+ *    (like in case of OR, you may want to skip any "false" nodes found)
+ *
+ * Use a null node if you want to ignore any of the optimizations.
+ */
+RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
 {
   typedef std::hash_set<TNode, TNodeHashFunction> node_set;
 
   node_set visited;
-  visited.insert(falseNode);
+  visited.insert(skipNode);
 
   std::vector<TNode> toProcess;
   toProcess.push_back(n);
@@ -41,8 +54,8 @@ RewriteResponse flattenOrNode(TNode n, TNode trueNode, TNode falseNode)
       TNode child = current[j];
       if(visited.find(child) != visited.end()) {
         continue;
-      } else if(child == trueNode) {
-        return RewriteResponse(REWRITE_DONE, trueNode);
+      } else if(child == trivialNode) {
+        return RewriteResponse(REWRITE_DONE, trivialNode);
       } else {
         if(child.getKind() == k)
           toProcess.push_back(child);
@@ -51,7 +64,7 @@ RewriteResponse flattenOrNode(TNode n, TNode trueNode, TNode falseNode)
       }
     }
   }
-  if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, falseNode);
+  if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, skipNode);
   if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
   return RewriteResponse(REWRITE_AGAIN, nb.constructNode());
 }
@@ -77,35 +90,22 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
       if ((*i).getKind() == kind::OR) done = false;
     }
     if (!done) {
-      return flattenOrNode(n, /*trueNode = */ tt, /* falseNode = */ ff);
+      return flattenNode(n, /*trivialNode = */ tt, /* skipNode = */ ff);
     }
     break;
   }
   case kind::AND: {
-    //TODO: Why REWRITE_AGAIN here?
-    if (n.getNumChildren() == 2) {
-      if (n[0] == ff || n[1] == ff) return RewriteResponse(REWRITE_DONE, ff);
-      if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
-      if (n[1] == tt) return RewriteResponse(REWRITE_AGAIN, n[0]);
+    bool done = true;
+    TNode::iterator i = n.begin(), iend = n.end();
+    for(; i != iend; ++i) {
+      if (*i == ff) return RewriteResponse(REWRITE_DONE, ff);
+      if (*i == tt) done = false;
+      if ((*i).getKind() == kind::AND) done = false;
     }
-    else {
-      bool done = true;
-      TNode::iterator i = n.begin(), iend = n.end();
-      for(; i != iend; ++i) {
-        if (*i == ff) return RewriteResponse(REWRITE_DONE, ff);
-        if (*i == tt) done = false;
-      }
-      if (!done) {
-        NodeBuilder<> nb(kind::AND);
-        for(i = n.begin(); i != iend; ++i) {
-          if (*i != tt) {
-            nb << *i;
-          }
-        }
-        if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, tt);
-        if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
-        return RewriteResponse(REWRITE_AGAIN, nb.constructNode());
-      }
+    if (!done) {
+      RewriteResponse ret = flattenNode(n, /*trivialNode = */ ff, /* skipNode = */ tt);
+      Debug("bool-flatten") << n << ": " << ret.node << std::endl;
+      return ret;
     }
     break;
   }
diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index 42f763f07..f8cd0fb9a 100644
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -38,7 +38,8 @@ CVC_TESTS = \
 	preprocess_10.cvc \
 	preprocess_11.cvc \
 	preprocess_12.cvc \
-	preprocess_13.cvc
+	preprocess_13.cvc \
+	preprocess_14.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = 
diff --git a/test/regress/regress0/preprocess/preprocess_14.cvc b/test/regress/regress0/preprocess/preprocess_14.cvc
new file mode 100644
index 000000000..04a6f4c50
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_14.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a6 AND (a7 AND (a8 AND a9))))))))));
+
+CHECKSAT;
+
+% EXIT: 10
+