Clark's work on array theory - can now solve all QF_AX problems

1 files changed, 37 insertions, 0 deletions

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 18aa71667..d2693268f 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -42,14 +42,51 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
       if (n[0] == ff) return RewriteResponse(REWRITE_AGAIN, n[1]);
       if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0]);
     }
+    else {
+      bool done = true;
+      TNode::iterator i = n.begin(), iend = n.end();
+      for(; i != iend; ++i) {
+        if (*i == tt) return RewriteResponse(REWRITE_DONE, tt);
+        if (*i == ff) done = false;
+      }
+      if (!done) {
+        NodeBuilder<> nb(kind::OR);
+        for(i = n.begin(); i != iend; ++i) {
+          if (*i != ff) nb << *i;
+        }
+        if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, ff);
+        if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
+        return RewriteResponse(REWRITE_AGAIN, nb.constructNode());
+      }
+    }
     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]);
     }
+    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());
+      }
+    }
     break;
   }
   case kind::IMPLIES: {