summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xautogen.sh4
-rw-r--r--config/cvc4.m42
-rw-r--r--src/expr/node.cpp3
-rw-r--r--src/expr/node_manager.cpp4
-rw-r--r--src/expr/node_manager.h18
-rw-r--r--src/expr/node_value.cpp47
-rw-r--r--src/expr/node_value.h12
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 <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; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback