From 426b8722e6e32f7fab46769e4d71184bf510fd0e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 16 Dec 2009 23:30:21 +0000 Subject: [PATCH] + refactoring fixes for expr package based on code review (see bug #4) + minor autogen/configure fixes for old versions of autotools --- autogen.sh | 4 ++-- config/cvc4.m4 | 2 +- src/expr/node.cpp | 3 ++- src/expr/node_manager.cpp | 4 ++++ src/expr/node_manager.h | 18 --------------- src/expr/node_value.cpp | 47 ++++++--------------------------------- src/expr/node_value.h | 12 ++-------- 7 files changed, 18 insertions(+), 72 deletions(-) diff --git a/autogen.sh b/autogen.sh index eed091821..70e6ff98a 100755 --- 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 eea9478c6..1926fa54a 100644 --- 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 f1b3c5980..40dd70457 100644 --- 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 ab52b9f40..4b550ee3d 100644 --- 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 bdbedbb4a..8caa797fa 100644 --- 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 7af2cd2b5..42b7b05e4 100644 --- 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 9bdbb7f8c..75c694ec9 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -70,8 +70,8 @@ class NodeValue { template 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; } -- 2.30.2