diff options
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 105 |
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; |