+ refactoring fixes for expr package based on code review (see bug #4)

+ minor autogen/configure fixes for old versions of autotools

diff --git a/autogen.sh b/autogen.sh
index eed0918216fb50a4479256c34627f23413361021..70e6ff98a6b2e206d2c93508bcf39c7835ae9b85 100755 (executable)
--- a/autogen.sh
+++ b/autogen.sh
@@ -33,8 +33,8 @@ fi
 set -ex
 
 cd "$(dirname "$0")"
-libtoolize -cf || glibtoolize -cf
-aclocal -I config --force --install -Wall
+libtoolize -c -f || glibtoolize -c -f
+aclocal -I config --force --install -Wall || aclocal -I config --force
 autoheader -I config -f -Wall
 touch NEWS README AUTHORS ChangeLog
 touch stamp-h

diff --git a/config/cvc4.m4 b/config/cvc4.m4
index eea9478c66e29acf74fe4e6b3544d6f1bd82502e..1926fa54a72dc5de99b1a77cf6d18aba852c4923 100644 (file)
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -25,6 +25,6 @@ do
 done
 eval set x $ac_cvc4_rewritten_args
 shift
-echo "args are now:" "${@}"
+dnl echo "args are now:" "${@}"
 m4_divert_pop([PARSE_ARGS])dnl
 ])# CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index f1b3c5980d29e1250e18aedd8d919605aeda4ebf..40dd70457b162578e00fa5796ae78e21e52fc80f 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -67,7 +67,8 @@ void Node::assignNodeValue(NodeValue* ev) {
 
 Node& Node::operator=(const Node& e) {
   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
-  if((this != &e) && (d_ev != e.d_ev)) {
+  Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!");
+  if(EXPECT_TRUE( d_ev != e.d_ev )) {
     d_ev->dec();
     d_ev = e.d_ev;
     d_ev->inc();

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index ab52b9f4046953b62f281f27a21f1811a2d2aa79..4b550ee3d837773587398c00622e6583c9cd864b 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -20,6 +20,8 @@ __thread NodeManager* NodeManager::s_current = 0;
 
 Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
   Assert(this != NULL, "Whoops, we have a bad expression manager!");
+  Assert(ev != NULL, "lookup() expects a non-NULL NodeValue!");
+
   hash_t::iterator i = d_hash.find(hash);
   if(i == d_hash.end()) {
     // insert
@@ -63,6 +65,8 @@ Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
 
 NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
   Assert(this != NULL, "Whoops, we have a bad expression manager!");
+  Assert(ev != NULL, "lookupNoInsert() expects a non-NULL NodeValue!");
+
   hash_t::iterator i = d_hash.find(hash);
   if(i == d_hash.end()) {
     return NULL;

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index bdbedbb4a1e3e55e13acb4b2e807cee655b2c2da..8caa797fa03d539d8e73a7004e6555a30e197a95 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -47,24 +47,6 @@ public:
 
   // variables are special, because duplicates are permitted
   Node mkVar();
-
-  // TODO: these use the current NM (but must be renamed)
-  /*
-  static Node mkExpr(Kind kind)
-  { currentNM()->mkExpr(kind); }
-  static Node mkExpr(Kind kind, Node child1);
-  { currentNM()->mkExpr(kind, child1); }
-  static Node mkExpr(Kind kind, Node child1, Node child2);
-  { currentNM()->mkExpr(kind, child1, child2); }
-  static Node mkExpr(Kind kind, Node child1, Node child2, Node child3);
-  { currentNM()->mkExpr(kind, child1, child2, child3); }
-  static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4);
-  { currentNM()->mkExpr(kind, child1, child2, child3, child4); }
-  static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5);
-  { currentNM()->mkExpr(kind, child1, child2, child3, child4, child5); }
-  */
-
-  // do we want a varargs one?  perhaps not..
 };
 
 }/* CVC4 namespace */

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 7af2cd2b5e1e5be4f19e7397a9287472223a5ec5..42b7b05e4894070eda221c3bc3dab6c5fc472837 100644 (file)
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -41,22 +41,21 @@ uint64_t NodeValue::hash() const {
   return computeHash(d_kind, ev_begin(), ev_end());
 }
 
-NodeValue* NodeValue::inc() {
+void NodeValue::inc() {
   // FIXME multithreading
-  if(d_rc < MAX_RC)
+  if(EXPECT_TRUE( d_rc < MAX_RC )) {
     ++d_rc;
-  return this;
+  }
 }
 
-NodeValue* NodeValue::dec() {
+void NodeValue::dec() {
   // FIXME multithreading
-  if(d_rc < MAX_RC) {
-    if(--d_rc == 0) {
+  if(EXPECT_TRUE( d_rc < MAX_RC )) {
+    --d_rc;
+    if(EXPECT_FALSE( d_rc == 0 )) {
       // FIXME gc
-      return 0;
     }
   }
-  return this;
 }
 
 NodeValue::iterator NodeValue::begin() {
@@ -67,14 +66,6 @@ NodeValue::iterator NodeValue::end() {
   return node_iterator(d_children + d_nchildren);
 }
 
-NodeValue::iterator NodeValue::rbegin() {
-  return node_iterator(d_children + d_nchildren - 1);
-}
-
-NodeValue::iterator NodeValue::rend() {
-  return node_iterator(d_children - 1);
-}
-
 NodeValue::const_iterator NodeValue::begin() const {
   return const_node_iterator(d_children);
 }
@@ -83,14 +74,6 @@ NodeValue::const_iterator NodeValue::end() const {
   return const_node_iterator(d_children + d_nchildren);
 }
 
-NodeValue::const_iterator NodeValue::rbegin() const {
-  return const_node_iterator(d_children + d_nchildren - 1);
-}
-
-NodeValue::const_iterator NodeValue::rend() const {
-  return const_node_iterator(d_children - 1);
-}
-
 NodeValue::ev_iterator NodeValue::ev_begin() {
   return d_children;
 }
@@ -99,14 +82,6 @@ NodeValue::ev_iterator NodeValue::ev_end() {
   return d_children + d_nchildren;
 }
 
-NodeValue::ev_iterator NodeValue::ev_rbegin() {
-  return d_children + d_nchildren - 1;
-}
-
-NodeValue::ev_iterator NodeValue::ev_rend() {
-  return d_children - 1;
-}
-
 NodeValue::const_ev_iterator NodeValue::ev_begin() const {
   return d_children;
 }
@@ -115,14 +90,6 @@ NodeValue::const_ev_iterator NodeValue::ev_end() const {
   return d_children + d_nchildren;
 }
 
-NodeValue::const_ev_iterator NodeValue::ev_rbegin() const {
-  return d_children + d_nchildren - 1;
-}
-
-NodeValue::const_ev_iterator NodeValue::ev_rend() const {
-  return d_children - 1;
-}
-
 string NodeValue::toString() const {
   stringstream ss;
   toStream(ss);

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 9bdbb7f8cdc149002428c8a9a3abf09faacd47f2..75c694ec9e5a1c60767a1ea7536becc1de060a4b 100644 (file)
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -70,8 +70,8 @@ class NodeValue {
   template <unsigned> friend class CVC4::NodeBuilder;
   friend class CVC4::NodeManager;
 
-  NodeValue* inc();
-  NodeValue* dec();
+  void inc();
+  void dec();
 
   static size_t next_id;
 
@@ -110,13 +110,9 @@ class NodeValue {
 
   ev_iterator ev_begin();
   ev_iterator ev_end();
-  ev_iterator ev_rbegin();
-  ev_iterator ev_rend();
 
   const_ev_iterator ev_begin() const;
   const_ev_iterator ev_end() const;
-  const_ev_iterator ev_rbegin() const;
-  const_ev_iterator ev_rend() const;
 
   class node_iterator {
     const_ev_iterator d_i;
@@ -156,13 +152,9 @@ public:
 
   iterator begin();
   iterator end();
-  iterator rbegin();
-  iterator rend();
 
   const_iterator begin() const;
   const_iterator end() const;
-  const_iterator rbegin() const;
-  const_iterator rend() const;
 
   unsigned getId() const { return d_id; }
   Kind getKind() const { return (Kind) d_kind; }