From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 26 Jan 2010 15:06:24 +0000 (+0000)
Subject: cnf conversion
X-Git-Tag: cvc5-1.0.0~9339
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3d0ea6ed6d92943d9a52abbe30e944e9887516d;p=cvc5.git

cnf conversion
---

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 747854d23..13aa0b0ff 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -390,7 +390,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>&
   d_childrenStorage() {
 
   if(evIsAllocated(nb)) {
-    realloc(nb->d_size, false);
+    realloc(nb.d_size, false);
     std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin());
   } else {
     std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin());
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 985ad15a7..84df5957a 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -29,6 +29,7 @@
 #include "kind.h"
 
 #include <string>
+#include <iterator>
 
 namespace CVC4 {
 
@@ -142,6 +143,12 @@ class NodeValue {
     node_iterator operator++(int) {
       return node_iterator(d_i++);
     }
+
+    typedef std::input_iterator_tag iterator_category;
+    typedef Node value_type;
+    typedef ptrdiff_t difference_type;
+    typedef Node* pointer;
+    typedef Node& reference;
   };
   typedef node_iterator const_node_iterator;
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 018936f7c..db9dc4edf 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -31,7 +31,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() :
 }
 
 SmtEngine::~SmtEngine() {
-
 }
 
 void SmtEngine::doCommand(Command* c) {
@@ -39,16 +38,95 @@ void SmtEngine::doCommand(Command* c) {
   c->invoke(this);
 }
 
+void SmtEngine::orHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result) {
+  if(p == end) {
+    return;
+  } else if((*p).getKind() == AND) {
+    NodeBuilder<> resultPrefix = result;
+    result = NodeBuilder<>(AND);
+
+    for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) {
+      NodeBuilder<> r = resultPrefix;
+
+      r << preprocess(*i);
+      Node::iterator p2 = p;
+      orHelper(++p2, end, r);
+
+      result << r;
+    }
+  } else {
+    result << preprocess(*p);
+  }
+}
+
 Node SmtEngine::preprocess(const Node& e) {
   if(e.getKind() == NOT) {
+    // short-circuit trivial NOTs
     if(e[0].getKind() == TRUE) {
       return d_nm->mkNode(FALSE);
     } else if(e[0].getKind() == FALSE) {
       return d_nm->mkNode(TRUE);
     } else if(e[0].getKind() == NOT) {
       return preprocess(e[0][0]);
+    } else {
+      Node f = preprocess(e[0]);
+      // push NOTs inside of ANDs and ORs
+      if(f.getKind() == AND) {
+        NodeBuilder<> n(OR);
+        for(Node::iterator i = f.begin(); i != f.end(); ++i) {
+          if((*i).getKind() == NOT) {
+            n << (*i)[0];
+          } else {
+            n << d_nm->mkNode(NOT, *i);
+          }
+        }
+        return n;
+      }
+      if(f.getKind() == OR) {
+        NodeBuilder<> n(AND);
+        for(Node::iterator i = f.begin(); i != f.end(); ++i) {
+          if((*i).getKind() == NOT) {
+            n << (*i)[0];
+          } else {
+            n << d_nm->mkNode(NOT, *i);
+          }
+        }
+        return n;
+      }
+    }
+  } else if(e.getKind() == AND) {
+    NodeBuilder<> n(AND);
+    // flatten ANDs
+    for(Node::iterator i = e.begin(); i != e.end(); ++i) {
+      Node f = preprocess(*i);
+      if((*i).getKind() == AND) {
+        for(Node::iterator j = f.begin(); j != f.end(); ++j) {
+          n << *j;
+        }
+      } else {
+        n << *i;        
+      }
+    }
+    return n;
+  } else if(e.getKind() == OR) {
+    NodeBuilder<> n(OR);
+    // flatten ORs
+    for(Node::iterator i = e.begin(); i != e.end(); ++i) {
+      if((*i).getKind() == OR) {
+        Node f = preprocess(*i);
+        for(Node::iterator j = f.begin(); j != f.end(); ++j) {
+          n << *j;
+        }
+      }
     }
+
+    Node nod = n;
+    NodeBuilder<> m(OR);
+    orHelper(nod.begin(), nod.end(), m);
+
+    return m;
   }
+
   return e;
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 027d3d603..e06a36128 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -22,6 +22,7 @@
 #include "expr/node.h"
 #include "expr/expr.h"
 #include "expr/node_manager.h"
+#include "expr/node_builder.h"
 #include "expr/expr_manager.h"
 #include "util/result.h"
 #include "util/model.h"
@@ -164,6 +165,10 @@ private:
    */
   Node processAssertionList();
 
+  /**
+   * Helper method for CNF preprocessing.  CNF-converts an OR.
+   */
+  void orHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result);
 
 };/* class SmtEngine */