From: Dejan Jovanović Date: Mon, 22 Feb 2010 23:15:48 +0000 (+0000) Subject: finally works X-Git-Tag: cvc5-1.0.0~9229 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad223d3d5e5d19b04790dd48e586774e64735e3b;p=cvc5.git finally works --- diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index c3090e40f..a75b97b74 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -15,7 +15,6 @@ libexpr_la_SOURCES = \ expr_manager.h \ attribute.h \ @srcdir@/kind.h \ - node.cpp \ node_builder.cpp \ node_manager.cpp \ expr_manager.cpp \ diff --git a/src/expr/node.cpp b/src/expr/node.cpp deleted file mode 100644 index b9d3d13bb..000000000 --- a/src/expr/node.cpp +++ /dev/null @@ -1,203 +0,0 @@ -<<<<<<< .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 - -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(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 diff --git a/src/expr/node.h b/src/expr/node.h index 280c85fb3..46ffcef35 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -108,15 +108,13 @@ template /** 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 NodeTemplate(const NodeTemplate&); ->>>>>>> .merge-right.r241 /** Destructor. Decrements the reference count and, if zero, * collects the NodeValue. */ @@ -129,26 +127,14 @@ template 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 + NodeTemplate& operator=(const NodeTemplate&); size_t hash() const { return d_ev->getId(); @@ -157,7 +143,6 @@ template uint64_t getId() const { return d_ev->getId(); } - const Type* getType() const; const Type* getType() const; @@ -179,21 +164,11 @@ template inline size_t getNumChildren() const; -<<<<<<< .working - template - inline typename AttrKind::value_type getAttribute(const AttrKind&) const; -======= + static NodeTemplate null(); ->>>>>>> .merge-right.r241 -<<<<<<< .working - template - inline bool hasAttribute(const AttrKind&, - typename AttrKind::value_type* = NULL) const; -======= typedef typename NodeValue::iterator iterator; typedef typename NodeValue::iterator const_iterator; ->>>>>>> .merge-right.r241 inline iterator begin(); inline iterator end(); @@ -336,39 +311,22 @@ template template template -<<<<<<< .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::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 template -<<<<<<< .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::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); } @@ -458,8 +416,9 @@ template } template +template NodeTemplate& NodeTemplate::operator= - (const NodeTemplate& e) { + (const NodeTemplate& 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 )) {