From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 18 Dec 2009 19:47:42 +0000 (+0000)
Subject: numerous fixes to nodes; more coming
X-Git-Tag: cvc5-1.0.0~9350
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e112de2be02760f66505a09e76269cca272dc988;p=cvc5.git

numerous fixes to nodes; more coming
---

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 9c73b982c..b87acb1f2 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -79,11 +79,6 @@ Node& Node::operator=(const Node& e) {
   return *this;
 }
 
-NodeValue const* Node::operator->() const {
-  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
-  return d_ev;
-}
-
 uint64_t Node::hash() const {
   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
   return d_ev->hash();
diff --git a/src/expr/node.h b/src/expr/node.h
index 9bb138b21..fd2603ffa 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -67,15 +67,13 @@ class Node {
    *  don't change their arguments, and it's nice to have
    *  const_iterators over them.  See notes in .cpp file for
    *  details. */
+  // this really does needs to be explicit to avoid hard to track
+  // errors with Nodes implicitly wrapping NodeValues
   explicit Node(const NodeValue*);
 
   template <unsigned> friend class NodeBuilder;
   friend class NodeManager;
 
-  /** Access to the encapsulated expression.
-   *  @return the encapsulated expression. */
-  NodeValue const* operator->() const;
-
   /**
    * Assigns the expression value and does reference counting. No assumptions
    * are made on the expression, and should only be used if we know what we are
@@ -85,8 +83,8 @@ class Node {
    */
   void assignNodeValue(NodeValue* ev);
 
-  typedef NodeValue::iterator ev_iterator;
-  typedef NodeValue::const_iterator const_ev_iterator;
+  typedef NodeValue::ev_iterator ev_iterator;
+  typedef NodeValue::const_ev_iterator const_ev_iterator;
 
   inline ev_iterator ev_begin();
   inline ev_iterator ev_end();
@@ -161,7 +159,9 @@ inline bool Node::operator<(const Node& e) const {
   return d_ev->d_id < e.d_ev->d_id;
 }
 
-inline std::ostream& operator<<(std::ostream& out, const Node& e) {
+inline std::ostream& 
+
+operator<<(std::ostream& out, const Node& e) {
   e.toStream(out);
   return out;
 }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index b974ecc67..1dee91735 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -32,6 +32,7 @@ namespace CVC4 {
 #include "expr/kind.h"
 #include "util/Assert.h"
 #include "expr/node_value.h"
+#include "util/output.h"
 
 namespace CVC4 {
 
@@ -82,6 +83,15 @@ class NodeBuilder {
     }
   }
 
+  void crop() {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    if(EXPECT_FALSE( evIsAllocated() ) && EXPECT_TRUE( d_size > d_ev->d_nchildren )) {
+      d_ev = (NodeValue*)
+        std::realloc(d_ev, sizeof(NodeValue) +
+                     ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) ));
+    }
+  }
+
 public:
 
   inline NodeBuilder();
@@ -95,10 +105,22 @@ public:
   typedef NodeValue::ev_iterator iterator;
   typedef NodeValue::const_ev_iterator const_iterator;
 
-  iterator begin() { return d_ev->ev_begin(); }
-  iterator end() { return d_ev->ev_end(); }
-  const_iterator begin() const { return d_ev->ev_begin(); }
-  const_iterator end() const { return d_ev->ev_end(); }
+  iterator begin() {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    return d_ev->ev_begin();
+  }
+  iterator end() {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    return d_ev->ev_end();
+  }
+  const_iterator begin() const {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    return d_ev->ev_begin();
+  }
+  const_iterator end() const {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    return d_ev->ev_end();
+  }
 
   // Compound expression constructors
   /*
@@ -127,21 +149,25 @@ public:
   // "Stream" expression constructor syntax
 
   NodeBuilder& operator<<(const Kind& k) {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     Assert(d_ev->d_kind == UNDEFINED_KIND);
     d_ev->d_kind = k;
     return *this;
   }
 
   NodeBuilder& operator<<(const Node& n) {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     return append(n);
   }
 
   // For pushing sequences of children
   NodeBuilder& append(const std::vector<Node>& children) {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     return append(children.begin(), children.end());
   }
 
   NodeBuilder& append(const Node& n) {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     allocateEvIfNecessaryForAppend();
     NodeValue* ev = n.d_ev;
     d_hash = NodeValue::computeHash(d_hash, ev);
@@ -152,20 +178,13 @@ public:
 
   template <class Iterator>
   NodeBuilder& append(const Iterator& begin, const Iterator& end) {
+    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     for(Iterator i = begin; i != end; ++i) {
       append(*i);
     }
     return *this;
   }
 
-  void crop() {
-    if(EXPECT_FALSE( evIsAllocated() ) && d_size > d_ev->d_nchildren) {
-      d_ev = (NodeValue*)
-        std::realloc(d_ev, sizeof(NodeValue) +
-                     ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) ));
-    }
-  }
-
   // not const
   operator Node();
 
@@ -356,6 +375,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
   d_inlineEv(0),
   d_childrenStorage(0) {
 
+  Message() << "kind " << k << std::endl;
   d_inlineEv.d_kind = k;
 }
 
@@ -412,19 +432,25 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
   d_inlineEv(0),
   d_childrenStorage() {
 
+  Message() << "kind " << k << std::endl;
   d_inlineEv.d_kind = k;
 }
 
 template <unsigned nchild_thresh>
 inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
-  for(iterator i = begin();
-      i != end();
+  Assert(d_used, "NodeBuilder unused at destruction");
+  
+  return;
+  /*
+  for(iterator i = d_ev->ev_begin();
+      i != d_ev->ev_end();
       ++i) {
     (*i)->dec();
   }
   if(evIsAllocated()) {
     free(d_ev);
   }
+  */
 }
 
 template <unsigned nchild_thresh>
@@ -472,33 +498,35 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
 
 template <unsigned nchild_thresh>
 NodeBuilder<nchild_thresh>::operator Node() {// not const
+  Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
   Assert(d_ev->d_kind != UNDEFINED_KIND,
          "Can't make an expression of an undefined kind!");
-  Assert(! d_used, "This NodeBuilder has already been used!");
 
   // implementation differs depending on whether the expression value
   // was malloc'ed or not
 
   if(EXPECT_FALSE( evIsAllocated() )) {
     NodeValue *ev = d_nm->lookupNoInsert(d_hash, d_ev);
-    if(ev != d_ev) {
+    if(ev != NULL) {
       // expression already exists in node manager
+      d_used = true;
       return Node(ev);
     }
 
     // otherwise create the canonical expression value for this node
     crop();
-    d_used = true;
     ev = d_ev;
     d_ev = NULL;
     // this inserts into the NodeManager;
     // return the result of lookup() in case another thread beat us to it
+    d_used = true;
     return d_nm->lookup(d_hash, ev);
   }
 
   NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv);
-  if(ev != &d_inlineEv) {
+  if(ev != NULL) {
     // expression already exists in node manager
+    d_used = true;
     return Node(ev);
   }
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index d752db88f..eba8c4d18 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -16,6 +16,7 @@
 #include "node_builder.h"
 #include "node_manager.h"
 #include "expr/node.h"
+#include "util/output.h"
 
 namespace CVC4 {
 
@@ -43,15 +44,15 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
         continue;
       }
 
-      NodeValue::const_iterator c1 = ev->ev_begin();
-      NodeValue::iterator c2 = j->d_ev->ev_begin();
+      NodeValue::const_ev_iterator c1 = ev->ev_begin();
+      NodeValue::ev_iterator c2 = j->d_ev->ev_begin();
       for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
-        if((*c1).d_ev != (*c2).d_ev) {
+        if(*c1 != *c2) {
           break;
         }
       }
 
-      if(c1 != ev->ev_end() || c2 != j->end()) {
+      if(c1 != ev->ev_end() || c2 != j->d_ev->ev_end()) {
         continue;
       }
 
@@ -83,21 +84,22 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
         continue;
       }
 
-      NodeValue::const_iterator c1 = ev->ev_begin();
-      NodeValue::iterator c2 = j->d_ev->ev_begin();
+      NodeValue::const_ev_iterator c1 = ev->ev_begin();
+      NodeValue::ev_iterator c2 = j->d_ev->ev_begin();
       for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
-        if((*c1).d_ev != (*c2).d_ev) {
+        Debug("expr") << "comparing " << c1 << " and " << c2 << std::endl;
+        if(*c1 != *c2) {
           break;
         }
       }
 
-      if(c1 != ev->ev_end() || c2 != j->end()) {
+      if(c1 != ev->ev_end() || c2 != j->d_ev->ev_end()) {
         continue;
       }
 
       return j->d_ev;
     }
-    // didn't find it
+    // didn't find it, don't insert
     return 0;
   }
 }
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 6724b0771..554655573 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -104,8 +104,8 @@ void NodeValue::toStream(std::ostream& out) const {
   if(d_kind == VARIABLE) {
     out << ":" << this;
   } else {
-    for(const_iterator i = begin(); i != end(); ++i) {
-      if(i != end()) {
+    for(const_ev_iterator i = ev_begin(); i != ev_end(); ++i) {
+      if(i != ev_end()) {
         out << " ";
       }
       out << *i;
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 352be7d27..954fe0aaa 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -97,7 +97,8 @@ class NodeValue {
    * @return the hash value
    */
   template<typename const_iterator_type>
-  static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) {
+  static uint64_t computeHash(uint64_t hash, const_iterator_type begin,
+                              const_iterator_type end) {
     for(const_iterator_type i = begin; i != end; ++i) {
       hash = computeHash(hash, *i);
     }
@@ -105,7 +106,8 @@ class NodeValue {
   }
 
   static uint64_t computeHash(uint64_t hash, const NodeValue* ev) {
-    return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId();
+    return
+      ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId();
   }
 
   typedef NodeValue** ev_iterator;
@@ -120,7 +122,7 @@ class NodeValue {
   class node_iterator {
     const_ev_iterator d_i;
   public:
-    node_iterator(const_ev_iterator i) : d_i(i) {}
+    explicit node_iterator(const_ev_iterator i) : d_i(i) {}
 
     inline Node operator*();
 
@@ -132,7 +134,7 @@ class NodeValue {
       return d_i != i.d_i;
     }
 
-    node_iterator& operator++() {
+    node_iterator operator++() {
       ++d_i;
       return *this;
     }
@@ -175,7 +177,7 @@ namespace CVC4 {
 namespace expr {
 
 inline Node NodeValue::node_iterator::operator*() {
-  return Node(*d_i);
+  return Node((NodeValue*) d_i);
 }
 
 }/* CVC4::expr namespace */