summaryrefslogtreecommitdiff
path: root/src/expr/node.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node.h')
-rw-r--r--src/expr/node.h105
1 files changed, 52 insertions, 53 deletions
diff --git a/src/expr/node.h b/src/expr/node.h
index e0231bef6..cd3c99a78 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -33,15 +33,15 @@
#include <utility>
#include <vector>
+#include "base/check.h"
#include "base/configuration.h"
-#include "base/cvc4_assert.h"
#include "base/exception.h"
#include "base/output.h"
-#include "expr/type.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
#include "expr/expr.h"
#include "expr/expr_iomanip.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "expr/type.h"
#include "options/language.h"
#include "options/set_language.h"
#include "util/hash.h"
@@ -226,7 +226,7 @@ class NodeTemplate {
inline void assertTNodeNotExpired() const
{
if(!ref_count) {
- Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
+ Assert(d_nv->d_rc > 0) << "TNode pointing to an expired NodeValue";
}
}
@@ -1022,9 +1022,9 @@ template <bool ref_count>
template <class AttrKind>
inline typename AttrKind::value_type NodeTemplate<ref_count>::
getAttribute(const AttrKind&) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ Assert(NodeManager::currentNM() != NULL)
+ << "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?";
assertTNodeNotExpired();
@@ -1035,9 +1035,9 @@ template <bool ref_count>
template <class AttrKind>
inline bool NodeTemplate<ref_count>::
hasAttribute(const AttrKind&) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ Assert(NodeManager::currentNM() != NULL)
+ << "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?";
assertTNodeNotExpired();
@@ -1048,9 +1048,9 @@ template <bool ref_count>
template <class AttrKind>
inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
typename AttrKind::value_type& ret) const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ Assert(NodeManager::currentNM() != NULL)
+ << "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?";
assertTNodeNotExpired();
@@ -1061,9 +1061,9 @@ template <bool ref_count>
template <class AttrKind>
inline void NodeTemplate<ref_count>::
setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ Assert(NodeManager::currentNM() != NULL)
+ << "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?";
assertTNodeNotExpired();
@@ -1080,12 +1080,12 @@ NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::null()
template <bool ref_count>
NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
d_nv(const_cast<expr::NodeValue*> (ev)) {
- Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+ Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
if(ref_count) {
d_nv->inc();
} else {
- Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null(),
- "TNode constructed from NodeValue with rc == 0");
+ Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null())
+ << "TNode constructed from NodeValue with rc == 0";
}
}
@@ -1095,37 +1095,37 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
template <bool ref_count>
NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
- Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
+ Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!";
d_nv = e.d_nv;
if(ref_count) {
- Assert(d_nv->d_rc > 0, "Node constructed from TNode with rc == 0");
+ Assert(d_nv->d_rc > 0) << "Node constructed from TNode with rc == 0";
d_nv->inc();
} else {
// shouldn't ever fail
- Assert(d_nv->d_rc > 0, "TNode constructed from Node with rc == 0");
+ Assert(d_nv->d_rc > 0) << "TNode constructed from Node with rc == 0";
}
}
template <bool ref_count>
NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
- Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
+ Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!";
d_nv = e.d_nv;
if(ref_count) {
// shouldn't ever fail
- Assert(d_nv->d_rc > 0, "Node constructed from Node with rc == 0");
+ Assert(d_nv->d_rc > 0) << "Node constructed from Node with rc == 0";
d_nv->inc();
} else {
- Assert(d_nv->d_rc > 0, "TNode constructed from TNode with rc == 0");
+ Assert(d_nv->d_rc > 0) << "TNode constructed from TNode with rc == 0";
}
}
template <bool ref_count>
NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
- Assert(e.d_node != NULL, "Expecting a non-NULL expression value!");
- Assert(e.d_node->d_nv != NULL, "Expecting a non-NULL expression value!");
+ Assert(e.d_node != NULL) << "Expecting a non-NULL expression value!";
+ Assert(e.d_node->d_nv != NULL) << "Expecting a non-NULL expression value!";
d_nv = e.d_node->d_nv;
// shouldn't ever fail
- Assert(d_nv->d_rc > 0, "Node constructed from Expr with rc == 0");
+ Assert(d_nv->d_rc > 0) << "Node constructed from Expr with rc == 0";
if(ref_count) {
d_nv->inc();
}
@@ -1133,10 +1133,10 @@ NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
template <bool ref_count>
NodeTemplate<ref_count>::~NodeTemplate() {
- Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+ Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
if(ref_count) {
// shouldn't ever fail
- Assert(d_nv->d_rc > 0, "Node reference count would be negative");
+ Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
d_nv->dec();
}
}
@@ -1147,29 +1147,28 @@ void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
if(ref_count) {
d_nv->inc();
} else {
- Assert(d_nv->d_rc > 0, "TNode assigned to NodeValue with rc == 0");
+ Assert(d_nv->d_rc > 0) << "TNode assigned to NodeValue with rc == 0";
}
}
template <bool ref_count>
NodeTemplate<ref_count>& NodeTemplate<ref_count>::
operator=(const NodeTemplate& e) {
- Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
- Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+ Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
+ Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!";
if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
if(ref_count) {
// shouldn't ever fail
- Assert(d_nv->d_rc > 0,
- "Node reference count would be negative");
+ Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
d_nv->dec();
}
d_nv = e.d_nv;
if(ref_count) {
// shouldn't ever fail
- Assert(d_nv->d_rc > 0, "Node assigned from Node with rc == 0");
+ Assert(d_nv->d_rc > 0) << "Node assigned from Node with rc == 0";
d_nv->inc();
} else {
- Assert(d_nv->d_rc > 0, "TNode assigned from TNode with rc == 0");
+ Assert(d_nv->d_rc > 0) << "TNode assigned from TNode with rc == 0";
}
}
return *this;
@@ -1178,21 +1177,21 @@ operator=(const NodeTemplate& e) {
template <bool ref_count>
NodeTemplate<ref_count>& NodeTemplate<ref_count>::
operator=(const NodeTemplate<!ref_count>& e) {
- Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
- Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+ Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
+ Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!";
if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
if(ref_count) {
// shouldn't ever fail
- Assert(d_nv->d_rc > 0, "Node reference count would be negative");
+ Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
d_nv->dec();
}
d_nv = e.d_nv;
if(ref_count) {
- Assert(d_nv->d_rc > 0, "Node assigned from TNode with rc == 0");
+ Assert(d_nv->d_rc > 0) << "Node assigned from TNode with rc == 0";
d_nv->inc();
} else {
// shouldn't ever happen
- Assert(d_nv->d_rc > 0, "TNode assigned from Node with rc == 0");
+ Assert(d_nv->d_rc > 0) << "TNode assigned from Node with rc == 0";
}
}
return *this;
@@ -1273,9 +1272,9 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
*/
template <bool ref_count>
NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ Assert(NodeManager::currentNM() != NULL)
+ << "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?";
assertTNodeNotExpired();
@@ -1301,8 +1300,7 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
case kind::metakind::NULLARY_OPERATOR:
IllegalArgument(*this, "getOperator() called on Node with NULLARY_OPERATOR-kinded kind");
- default:
- Unhandled(mk);
+ default: Unhandled() << mk;
}
}
@@ -1319,9 +1317,9 @@ inline bool NodeTemplate<ref_count>::hasOperator() const {
template <bool ref_count>
TypeNode NodeTemplate<ref_count>::getType(bool check) const
{
- Assert( NodeManager::currentNM() != NULL,
- "There is no current CVC4::NodeManager associated to this thread.\n"
- "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ Assert(NodeManager::currentNM() != NULL)
+ << "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?";
assertTNodeNotExpired();
@@ -1409,8 +1407,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
}
// otherwise compute
- Assert( std::distance(nodesBegin, nodesEnd) == std::distance(replacementsBegin, replacementsEnd),
- "Substitution iterator ranges must be equal size" );
+ Assert(std::distance(nodesBegin, nodesEnd)
+ == std::distance(replacementsBegin, replacementsEnd))
+ << "Substitution iterator ranges must be equal size";
Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this));
if(j != nodesEnd) {
Iterator2 b = replacementsBegin;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback