summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2009-12-16 19:51:02 +0000
committerTim King <taking@cs.nyu.edu>2009-12-16 19:51:02 +0000
commitb33a35b720059370ffb1507f31603cdb5347503a (patch)
treee4a2de1f99491d5ea066a7cee6d5d60a96624bb8 /src/expr
parente2cbeb69ca3a56af6ad7cc65a70f554d08e4df76 (diff)
Small refactoring changes for the expr package.
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/attr_type.h5
-rw-r--r--src/expr/expr.cpp13
-rw-r--r--src/expr/expr.h1
-rw-r--r--src/expr/expr_manager.h6
-rw-r--r--src/expr/node.cpp2
-rw-r--r--src/expr/node.h4
-rw-r--r--src/expr/node_manager.h2
7 files changed, 22 insertions, 11 deletions
diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index 2e0a8b675..597be0fe7 100644
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -23,7 +23,10 @@ class Type;
// this is essentially a traits structure
class Type_attr {
public:
- enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
+
+ // could use typeid but then different on different machines/compiles
+ enum { hash_value = 11 };
+
typedef Type value_type;//Node?
static const Type_attr marker;
};
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index af685aced..eacd1cb24 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -46,8 +46,11 @@ Expr& Expr::operator=(const Expr& e) {
}
bool Expr::operator==(const Expr& e) const {
- if(d_em != e.d_em)
- return false;Assert(d_node != NULL, "Unexpected NULL expression pointer!");Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+ if(d_em != e.d_em){
+ return false;
+ }
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
return *d_node == *e.d_node;
}
@@ -56,9 +59,11 @@ bool Expr::operator!=(const Expr& e) const {
}
bool Expr::operator<(const Expr& e) const {
- Assert(d_node != NULL, "Unexpected NULL expression pointer!");Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
- if(d_em != e.d_em)
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+ if(d_em != e.d_em){
return false;
+ }
return *d_node < *e.d_node;
}
diff --git a/src/expr/expr.h b/src/expr/expr.h
index 34a94ee66..a0a646900 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -95,6 +95,7 @@ public:
/**
* Returns the string representation of the expression.
+ * @return a string representation of the expression
*/
std::string toString() const;
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 4a7f359e9..645193ecf 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -23,7 +23,7 @@ class CVC4_PUBLIC ExprManager {
public:
/**
- * Creates an expressio manager.
+ * Creates an expression manager.
*/
ExprManager();
@@ -49,8 +49,10 @@ public:
Expr mkExpr(Kind kind, const Expr& child1);
/**
- * Make a ternary expression of a given kind (AND, PLUS, ...).
+ * Make a binary expression of a given kind (AND, PLUS, ...).
* @param kind the kind of expression
+ * @param child1 the first child of the new expression
+ * @param child2 the second child of the new expression
* @return the expression
*/
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 1a549973f..f1b3c5980 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -67,7 +67,7 @@ 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) {
+ if((this != &e) && (d_ev != e.d_ev)) {
d_ev->dec();
d_ev = e.d_ev;
d_ev->inc();
diff --git a/src/expr/node.h b/src/expr/node.h
index 5415a5b3c..aad0689bb 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -74,8 +74,8 @@ class Node {
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
+ * 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
* doing.
*
* @param ev the expression value to assign
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3a28a22ff..bdbedbb4a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,5 +1,5 @@
/********************* -*- C++ -*- */
-/** expr_manager.h
+/** node_manager.h
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback