+++ /dev/null
-<<<<<<< .working
-/********************* */
-/** node.cpp
- ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): taking
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **/
-
-#include "expr/node.h"
-#include "expr/node_value.h"
-#include "expr/node_builder.h"
-#include "util/Assert.h"
-
-#include <sstream>
-
-using namespace CVC4::expr;
-using namespace std;
-
-namespace CVC4 {
-
-NodeValue NodeValue::s_null;
-
-Node Node::s_null(&NodeValue::s_null);
-
-Node Node::null() {
- return s_null;
-}
-
-bool Node::isNull() const {
- return d_ev == &NodeValue::s_null;
-}
-
-////FIXME: This function is a major hack! Should be changed ASAP
-////TODO: Should use positive definition, i.e. what kinds are atomic.
-bool Node::isAtomic() const {
- switch(getKind()) {
- case NOT:
- case XOR:
- case ITE:
- case IFF:
- case IMPLIES:
- case OR:
- case AND:
- return false;
- default:
- return true;
- }
-}
-
-Node::Node() :
- d_ev(&NodeValue::s_null) {
- // No refcount needed
-}
-
-// FIXME: escape from type system convenient but is there a better
-// way? Nodes conceptually don't change their expr values but of
-// course they do modify the refcount. But it's nice to be able to
-// support node_iterators over const NodeValue*. So.... hm.
-Node::Node(const NodeValue* ev)
- : d_ev(const_cast<NodeValue*>(ev)) {
- Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
- d_ev->inc();
-}
-
-Node::Node(const Node& e) {
- Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
- d_ev = e.d_ev;
- d_ev->inc();
-}
-
-Node::~Node() {
- Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
- d_ev->dec();
-}
-
-void Node::assignNodeValue(NodeValue* ev) {
- d_ev = ev;
- d_ev->inc();
-}
-
-Node& Node::operator=(const Node& e) {
- Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
- 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();
- }
- return *this;
-}
-
-Node Node::eqExpr(const Node& right) 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 ?" );
-
- return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
-}
-
-Node Node::notExpr() 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 ?" );
-
- return NodeManager::currentNM()->mkNode(NOT, *this);
-}
-
-Node Node::andExpr(const Node& right) 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 ?" );
-
- return NodeManager::currentNM()->mkNode(AND, *this, right);
-}
-
-Node Node::orExpr(const Node& right) 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 ?" );
-
- return NodeManager::currentNM()->mkNode(OR, *this, right);
-}
-
-Node Node::iteExpr(const Node& thenpart, const Node& elsepart) 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 ?" );
-
- return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
-}
-
-Node Node::iffExpr(const Node& right) 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 ?" );
-
- return NodeManager::currentNM()->mkNode(IFF, *this, right);
-}
-
-Node Node::impExpr(const Node& right) 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 ?" );
-
- return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
-}
-
-Node Node::xorExpr(const Node& right) 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 ?" );
-
- return NodeManager::currentNM()->mkNode(XOR, *this, right);
-}
-
-const Type* Node::getType() 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 ?" );
- return NodeManager::currentNM()->getType(*this);
-}
-
-static void indent(ostream & o, int indent) {
- for(int i=0; i < indent; i++) {
- o << ' ';
- }
-}
-
-void Node::printAst(ostream & o, int ind) const {
- indent(o, ind);
- o << '(';
- o << getKind();
- if(getKind() == VARIABLE) {
- o << ' ' << getId();
- } else if(getNumChildren() >= 1) {
- for(Node::iterator child = begin(); child != end(); ++child) {
- o << endl;
- (*child).printAst(o, ind + 1);
- }
- o << endl;
- indent(o, ind);
- }
- o << ')';
-}
-
-void Node::debugPrint() {
-#ifndef CVC4_MUZZLE
- printAst(Warning(), 0);
- Warning().flush();
-#endif /* ! CVC4_MUZZLE */
-}
-
-}/* CVC4 namespace */
-=======
->>>>>>> .merge-right.r241
/** Default constructor, makes a null expression. */
NodeTemplate();
-<<<<<<< .working
- Node operator[](int i) const {
- Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
- return Node(d_ev->d_children[i]);
- }
-=======
+ NodeTemplate operator[](int i) const {
+ Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
+ return NodeTemplate(d_ev->d_children[i]);
+ }
+
template <bool ref_count_1>
NodeTemplate(const NodeTemplate<ref_count_1>&);
->>>>>>> .merge-right.r241
/** Destructor. Decrements the reference count and, if zero,
* collects the NodeValue. */
return d_ev != e.d_ev;
}
- NodeTemplate operator[](int i) const {
- Assert(i >= 0 && i < d_ev->d_nchildren);
- return NodeTemplate(d_ev->d_children[i]);
- }
-
/**
* We compare by expression ids so, keeping things deterministic and having
* that subexpressions have to be smaller than the enclosing expressions.
*/
inline bool operator<(const NodeTemplate& e) const;
-<<<<<<< .working
- /*
- Node plusExpr(const Node& right) const;
- Node uMinusExpr() const;
- Node multExpr(const Node& right) const;
-=======
- NodeTemplate& operator=(const NodeTemplate&);
->>>>>>> .merge-right.r241
- */
+ template <bool ref_count_1>
+ NodeTemplate& operator=(const NodeTemplate<ref_count_1>&);
size_t hash() const {
return d_ev->getId();
uint64_t getId() const {
return d_ev->getId();
}
- const Type* getType() const;
const Type* getType() const;
inline size_t getNumChildren() const;
-<<<<<<< .working
- template <class AttrKind>
- inline typename AttrKind::value_type getAttribute(const AttrKind&) const;
-=======
+
static NodeTemplate null();
->>>>>>> .merge-right.r241
-<<<<<<< .working
- template <class AttrKind>
- inline bool hasAttribute(const AttrKind&,
- typename AttrKind::value_type* = NULL) const;
-=======
typedef typename NodeValue::iterator<ref_count> iterator;
typedef typename NodeValue::iterator<ref_count> const_iterator;
->>>>>>> .merge-right.r241
inline iterator begin();
inline iterator end();
template <bool ref_count>
template <class AttrKind>
-<<<<<<< .working
-inline typename AttrKind::value_type Node::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 ?" );
-
-=======
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 ?" );
->>>>>>> .merge-right.r241
return NodeManager::currentNM()->getAttribute(*this, AttrKind());
}
template <bool ref_count>
template <class AttrKind>
-<<<<<<< .working
-inline bool Node::hasAttribute(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 ?" );
-
-=======
inline bool NodeTemplate<ref_count>::hasAttribute(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 ?" );
->>>>>>> .merge-right.r241
return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
}
}
template<bool ref_count>
+template<bool ref_count_1>
NodeTemplate<ref_count>& NodeTemplate<ref_count>::operator=
- (const NodeTemplate<ref_count>& e) {
+ (const NodeTemplate<ref_count_1>& e) {
Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!");
if(EXPECT_TRUE( d_ev != e.d_ev )) {
projects / cvc5.git / commitdiff