Merging in bvprop branch, with proper bit-vector propagation.

This should also fix bug 325. 

1 files changed, 22 insertions, 0 deletions

diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index 0dec26717..687272b56 100644
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -31,6 +31,23 @@ namespace CVC4 {
 template<typename Visitor>
 class NodeVisitor {
 
+  /** For re-entry checking */
+  static bool d_inRun;
+
+  class GuardReentry {
+    bool& d_guard;
+  public:
+    GuardReentry(bool& guard)
+    : d_guard(guard) {
+      Assert(!d_guard);
+      d_guard = true;
+    }
+    ~GuardReentry() {
+      Assert(d_guard);
+      d_guard = false;
+    }
+  };
+
 public:
 
   /**
@@ -52,6 +69,8 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
+    GuardReentry guard(d_inRun);
+
     // Notify of a start
     visitor.start(node);
 
@@ -91,5 +110,8 @@ public:
 
 };
 
+template <typename Visitor>
+bool NodeVisitor<Visitor>::d_inRun = false;
+
 }