diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-10 18:44:51 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-10 18:44:51 +0000 |
commit | f79afa96e7e7176b974252dd05a9f7bdf70194e8 (patch) | |
tree | cb12c0a880f8fbb356516a86699b0063a7bb8981 /src/expr | |
parent | 8b2d1d64b886db4cff74e2a7b1370841979001b2 (diff) |
killing expr into node...
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 14 | ||||
-rw-r--r-- | src/expr/Makefile.in | 22 | ||||
-rw-r--r-- | src/expr/attr_type.h | 2 | ||||
-rw-r--r-- | src/expr/attr_var_name.h | 2 | ||||
-rw-r--r-- | src/expr/expr.cpp | 115 | ||||
-rw-r--r-- | src/expr/expr_manager.cpp | 93 | ||||
-rw-r--r-- | src/expr/expr_value.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_value.h | 22 | ||||
-rw-r--r-- | src/expr/node.cpp | 115 | ||||
-rw-r--r-- | src/expr/node.h (renamed from src/expr/expr.h) | 86 | ||||
-rw-r--r-- | src/expr/node_attribute.h (renamed from src/expr/expr_attribute.h) | 22 | ||||
-rw-r--r-- | src/expr/node_builder.cpp (renamed from src/expr/expr_builder.cpp) | 72 | ||||
-rw-r--r-- | src/expr/node_builder.h (renamed from src/expr/expr_builder.h) | 178 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 93 | ||||
-rw-r--r-- | src/expr/node_manager.h (renamed from src/expr/expr_manager.h) | 42 |
15 files changed, 440 insertions, 440 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 630850387..6ca68d35c 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -7,13 +7,13 @@ noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ attr_type.h \ attr_var_name.h \ - expr.h \ - expr_builder.h \ + node.h \ + node_builder.h \ expr_value.h \ - expr_manager.h \ - expr_attribute.h \ + node_manager.h \ + node_attribute.h \ kind.h \ - expr.cpp \ - expr_builder.cpp \ - expr_manager.cpp \ + node.cpp \ + node_builder.cpp \ + node_manager.cpp \ expr_value.cpp diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in index 9d410cea8..de0bad1bd 100644 --- a/src/expr/Makefile.in +++ b/src/expr/Makefile.in @@ -52,7 +52,7 @@ CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = LTLIBRARIES = $(noinst_LTLIBRARIES) libexpr_la_LIBADD = -am_libexpr_la_OBJECTS = expr.lo expr_builder.lo expr_manager.lo \ +am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \ expr_value.lo libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) @@ -223,15 +223,15 @@ noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ attr_type.h \ attr_var_name.h \ - expr.h \ - expr_builder.h \ + node.h \ + node_builder.h \ expr_value.h \ - expr_manager.h \ - expr_attribute.h \ + node_manager.h \ + node_attribute.h \ kind.h \ - expr.cpp \ - expr_builder.cpp \ - expr_manager.cpp \ + node.cpp \ + node_builder.cpp \ + node_manager.cpp \ expr_value.cpp all: all-am @@ -286,10 +286,10 @@ mostlyclean-compile: distclean-compile: -rm -f *.tab.c -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_builder.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_manager.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_value.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_builder.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_manager.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h index 1d5e8eb0c..2e0a8b675 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -24,7 +24,7 @@ class Type; class Type_attr { public: enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles - typedef Type value_type;//Expr? + typedef Type value_type;//Node? static const Type_attr marker; }; diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h index a0780d575..13a2ec36f 100644 --- a/src/expr/attr_var_name.h +++ b/src/expr/attr_var_name.h @@ -24,7 +24,7 @@ class VarName; class VarName_attr { public: enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles - typedef Type value_type;//Expr? + typedef Type value_type;//Node? static const Type_attr marker; }; diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp deleted file mode 100644 index fa273dfa5..000000000 --- a/src/expr/expr.cpp +++ /dev/null @@ -1,115 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr.cpp - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 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/expr.h" -#include "expr_value.h" -#include "expr_builder.h" -#include "util/Assert.h" - -using namespace CVC4::expr; - -namespace CVC4 { - -ExprValue ExprValue::s_null; - -Expr Expr::s_null(&ExprValue::s_null); - -bool Expr::isNull() const { - return d_ev == &ExprValue::s_null; -} - -Expr::Expr() : - d_ev(&ExprValue::s_null) { - // No refcount needed -} - -Expr::Expr(ExprValue* ev) - : d_ev(ev) { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - d_ev->inc(); -} - -Expr::Expr(const Expr& e) { - Assert(e.d_ev != NULL, "Expecting a non-NULL evpression value!"); - d_ev = e.d_ev; - d_ev->inc(); -} - -Expr::~Expr() { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - d_ev->dec(); -} - -void Expr::assignExprValue(ExprValue* ev) { - d_ev = ev; - d_ev->inc(); -} - -Expr& Expr::operator=(const Expr& e) { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - if(this != &e && d_ev != e.d_ev) { - d_ev->dec(); - d_ev = e.d_ev; - d_ev->inc(); - } - return *this; -} - -ExprValue const* Expr::operator->() const { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - return d_ev; -} - -uint64_t Expr::hash() const { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - return d_ev->hash(); -} - -Expr Expr::eqExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(EQUAL, *this, right); -} - -Expr Expr::notExpr() const { - return ExprManager::currentEM()->mkExpr(NOT, *this); -} - -// FIXME: What does this do and why? -Expr Expr::negate() const { // avoid double-negatives - return ExprBuilder(*this).negate(); -} - - -Expr Expr::andExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(AND, *this, right); -} - -Expr Expr::orExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(OR, *this, right); -} - -Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { - return ExprManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart); -} - -Expr Expr::iffExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(IFF, *this, right); -} - -Expr Expr::impExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(IMPLIES, *this, right); -} - -Expr Expr::xorExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(XOR, *this, right); -} - -}/* CVC4 namespace */ diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp deleted file mode 100644 index 3b5347301..000000000 --- a/src/expr/expr_manager.cpp +++ /dev/null @@ -1,93 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr_manager.cpp - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 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. - ** - ** Expression manager implementation. - **/ - -#include "expr_builder.h" -#include "expr_manager.h" -#include "expr/expr.h" - -namespace CVC4 { - -__thread ExprManager* ExprManager::s_current = 0; - -Expr ExprManager::lookup(uint64_t hash, const Expr& e) { - Assert(this != NULL, "Woops, we have a bad expression manager!"); - hash_t::iterator i = d_hash.find(hash); - if(i == d_hash.end()) { - // insert - std::vector<Expr> v; - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } else { - for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) { - if(e.getKind() != j->getKind()) - continue; - - if(e.numChildren() != j->numChildren()) - continue; - - Expr::const_iterator c1 = e.begin(); - Expr::iterator c2 = j->begin(); - for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { - if(c1->d_ev != c2->d_ev) - break; - } - - if(c1 != e.end() || c2 != j->end()) - continue; - - return *j; - } - // didn't find it, insert - std::vector<Expr> v; - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } -} - -// general expression-builders - -Expr ExprManager::mkExpr(Kind kind) { - return ExprBuilder(this, kind); -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { - return ExprBuilder(this, kind) << child1; -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { - return ExprBuilder(this, kind) << child1 << child2; -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3) { - return ExprBuilder(this, kind) << child1 << child2 << child3; -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4) { - return ExprBuilder(this, kind) << child1 << child2 << child3 << child4; -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5) { - return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; -} - -// N-ary version -Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) { - return ExprBuilder(this, kind).append(children); -} - -Expr ExprManager::mkVar() { - return ExprBuilder(this, VARIABLE); -} - -}/* CVC4 namespace */ diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index 17f3b64c3..9ce7c3e12 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -10,7 +10,7 @@ ** An expression node. ** ** Instances of this class are generally referenced through - ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the + ** cvc4::Node rather than by pointer; cvc4::Node maintains the ** reference count on ExprValue instances and **/ diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index b334e1c2d..10f09e565 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -10,13 +10,13 @@ ** An expression node. ** ** Instances of this class are generally referenced through - ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the + ** cvc4::Node rather than by pointer; cvc4::Node maintains the ** reference count on ExprValue instances and **/ /* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */ /* to resolve a circular dependency */ -#include "expr/expr.h" +#include "expr/node.h" #ifndef __CVC4__EXPR__EXPR_VALUE_H #define __CVC4__EXPR__EXPR_VALUE_H @@ -27,8 +27,8 @@ namespace CVC4 { -class Expr; -class ExprBuilder; +class Node; +class NodeBuilder; namespace expr { @@ -49,7 +49,7 @@ class ExprValue { /** The ID (0 is reserved for the null value) */ unsigned d_id : 32; - /** The expression's reference count. @see cvc4::Expr. */ + /** The expression's reference count. @see cvc4::Node. */ unsigned d_rc : 8; /** Kind of the expression */ @@ -59,12 +59,12 @@ class ExprValue { unsigned d_nchildren : 16; /** Variable number of child nodes */ - Expr d_children[0]; + Node d_children[0]; // todo add exprMgr ref in debug case - friend class CVC4::Expr; - friend class CVC4::ExprBuilder; + friend class CVC4::Node; + friend class CVC4::NodeBuilder; ExprValue* inc(); ExprValue* dec(); @@ -76,7 +76,7 @@ class ExprValue { /** * Computes the hash over the given iterator span of children, and the - * root hash. The iterator should be either over a range of Expr or pointers + * root hash. The iterator should be either over a range of Node or pointers * to ExprValue. * @param hash the initial value for the hash * @param begin the begining of the range @@ -97,8 +97,8 @@ public: // Iterator support - typedef Expr* iterator; - typedef Expr const* const_iterator; + typedef Node* iterator; + typedef Node const* const_iterator; iterator begin(); iterator end(); diff --git a/src/expr/node.cpp b/src/expr/node.cpp new file mode 100644 index 000000000..22a905470 --- /dev/null +++ b/src/expr/node.cpp @@ -0,0 +1,115 @@ +/********************* -*- C++ -*- */ +/** expr.cpp + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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/expr_value.h" +#include "expr/node_builder.h" +#include "util/Assert.h" + +using namespace CVC4::expr; + +namespace CVC4 { + +ExprValue ExprValue::s_null; + +Node Node::s_null(&ExprValue::s_null); + +bool Node::isNull() const { + return d_ev == &ExprValue::s_null; +} + +Node::Node() : + d_ev(&ExprValue::s_null) { + // No refcount needed +} + +Node::Node(ExprValue* ev) + : d_ev(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::assignExprValue(ExprValue* ev) { + d_ev = ev; + d_ev->inc(); +} + +Node& Node::operator=(const Node& e) { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + if(this != &e && d_ev != e.d_ev) { + d_ev->dec(); + d_ev = e.d_ev; + d_ev->inc(); + } + return *this; +} + +ExprValue const* Node::operator->() const { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + return d_ev; +} + +uint64_t Node::hash() const { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + return d_ev->hash(); +} + +Node Node::eqExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(EQUAL, *this, right); +} + +Node Node::notExpr() const { + return NodeManager::currentEM()->mkExpr(NOT, *this); +} + +// FIXME: What does this do and why? +Node Node::negate() const { // avoid double-negatives + return NodeBuilder(*this).negate(); +} + + +Node Node::andExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(AND, *this, right); +} + +Node Node::orExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(OR, *this, right); +} + +Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { + return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart); +} + +Node Node::iffExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(IFF, *this, right); +} + +Node Node::impExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right); +} + +Node Node::xorExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(XOR, *this, right); +} + +}/* CVC4 namespace */ diff --git a/src/expr/expr.h b/src/expr/node.h index 7440974d8..aec50000e 100644 --- a/src/expr/expr.h +++ b/src/expr/node.h @@ -21,14 +21,14 @@ #include "expr/kind.h" namespace CVC4 { - class Expr; + class Node; }/* CVC4 namespace */ namespace CVC4 { -inline std::ostream& operator<<(std::ostream&, const Expr&) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC; -class ExprManager; +class NodeManager; namespace expr { class ExprValue; @@ -40,25 +40,25 @@ using CVC4::expr::ExprValue; * Encapsulation of an ExprValue pointer. The reference count is * maintained in the ExprValue. */ -class CVC4_PUBLIC Expr { +class CVC4_PUBLIC Node { friend class ExprValue; /** A convenient null-valued encapsulated pointer */ - static Expr s_null; + static Node s_null; /** The referenced ExprValue */ ExprValue* d_ev; - /** This constructor is reserved for use by the Expr package; one - * must construct an Expr using one of the build mechanisms of the - * Expr package. + /** This constructor is reserved for use by the Node package; one + * must construct an Node using one of the build mechanisms of the + * Node package. * * Increments the reference count. */ - explicit Expr(ExprValue*); + explicit Node(ExprValue*); - friend class ExprBuilder; - friend class ExprManager; + friend class NodeBuilder; + friend class NodeManager; /** Access to the encapsulated expression. * @return the encapsulated expression. */ @@ -76,49 +76,49 @@ class CVC4_PUBLIC Expr { public: /** Default constructor, makes a null expression. */ - Expr(); + Node(); - Expr(const Expr&); + Node(const Node&); /** Destructor. Decrements the reference count and, if zero, * collects the ExprValue. */ - ~Expr(); + ~Node(); - bool operator==(const Expr& e) const { return d_ev == e.d_ev; } - bool operator!=(const Expr& e) const { return d_ev != e.d_ev; } + bool operator==(const Node& e) const { return d_ev == e.d_ev; } + bool operator!=(const Node& e) const { return d_ev != e.d_ev; } /** * 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 Expr& e) const; + inline bool operator<(const Node& e) const; - Expr& operator=(const Expr&); + Node& operator=(const Node&); uint64_t hash() const; - Expr eqExpr(const Expr& right) const; - Expr notExpr() const; - Expr negate() const; // avoid double-negatives - Expr andExpr(const Expr& right) const; - Expr orExpr(const Expr& right) const; - Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const; - Expr iffExpr(const Expr& right) const; - Expr impExpr(const Expr& right) const; - Expr xorExpr(const Expr& right) const; + Node eqExpr(const Node& right) const; + Node notExpr() const; + Node negate() const; // avoid double-negatives + Node andExpr(const Node& right) const; + Node orExpr(const Node& right) const; + Node iteExpr(const Node& thenpart, const Node& elsepart) const; + Node iffExpr(const Node& right) const; + Node impExpr(const Node& right) const; + Node xorExpr(const Node& right) const; - Expr plusExpr(const Expr& right) const; - Expr uMinusExpr() const; - Expr multExpr(const Expr& right) const; + Node plusExpr(const Node& right) const; + Node uMinusExpr() const; + Node multExpr(const Node& right) const; inline Kind getKind() const; inline size_t numChildren() const; - static Expr null() { return s_null; } + static Node null() { return s_null; } - typedef Expr* iterator; - typedef Expr const* const_iterator; + typedef Node* iterator; + typedef Node const* const_iterator; inline iterator begin(); inline iterator end(); @@ -129,7 +129,7 @@ public: bool isNull() const; -};/* class Expr */ +};/* class Node */ }/* CVC4 namespace */ @@ -137,42 +137,42 @@ public: namespace CVC4 { -inline bool Expr::operator<(const Expr& e) const { +inline bool Node::operator<(const Node& e) const { return d_ev->d_id < e.d_ev->d_id; } -inline std::ostream& operator<<(std::ostream& out, const Expr& e) { +inline std::ostream& operator<<(std::ostream& out, const Node& e) { e.toString(out); return out; } -inline Kind Expr::getKind() const { +inline Kind Node::getKind() const { return Kind(d_ev->d_kind); } -inline void Expr::toString(std::ostream& out) const { +inline void Node::toString(std::ostream& out) const { if(d_ev) d_ev->toString(out); else out << "null"; } -inline Expr::iterator Expr::begin() { +inline Node::iterator Node::begin() { return d_ev->begin(); } -inline Expr::iterator Expr::end() { +inline Node::iterator Node::end() { return d_ev->end(); } -inline Expr::const_iterator Expr::begin() const { +inline Node::const_iterator Node::begin() const { return d_ev->begin(); } -inline Expr::const_iterator Expr::end() const { +inline Node::const_iterator Node::end() const { return d_ev->end(); } -inline size_t Expr::numChildren() const { +inline size_t Node::numChildren() const { return d_ev->d_nchildren; } diff --git a/src/expr/expr_attribute.h b/src/expr/node_attribute.h index b68a9d19d..b978f097d 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/node_attribute.h @@ -15,7 +15,7 @@ #include <stdint.h> #include "config.h" #include "context/context.h" -#include "expr/expr.h" +#include "expr/node.h" namespace CVC4 { namespace expr { @@ -26,7 +26,7 @@ class AttrTables; // global (or TSS) extern CDMap<uint64_t> g_hash_bool; extern CDMap<uint64_t> g_hash_int; -extern CDMap<Expr> g_hash_expr; +extern CDMap<Node> g_hash_expr; extern CDMap<void*> g_hash_ptr; template <class T> @@ -47,10 +47,10 @@ public: static CDMap<uint64_t> *s_hash; template <class Attr> - BitAccessor& find(Expr e, const Attr&); + BitAccessor& find(Node e, const Attr&); template <class Attr> - bool find(Expr e, const Attr&) const; + bool find(Node e, const Attr&) const; }; template <> @@ -58,8 +58,8 @@ class AttrTable<uint64_t> { public: // int(egral) specialization static CDMap<uint64_t> *s_hash; - uint64_t& find(Expr); - uint64_t& find(Expr) const; + uint64_t& find(Node); + uint64_t& find(Node) const; }; template <class T> @@ -70,16 +70,16 @@ public: }; template <> -class AttrTable<Expr> { +class AttrTable<Node> { public: - // Expr specialization - static CDMap<Expr> *s_hash; - Expr find(Expr); + // Node specialization + static CDMap<Node> *s_hash; + Node find(Node); }; CDMap<uint64_t>* AttrTable<bool>::s_hash = &g_hash_bool; CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int; -CDMap<Expr>* AttrTable<Expr>::s_hash = &g_hash_expr; +CDMap<Node>* AttrTable<Node>::s_hash = &g_hash_expr; template <class T> CDMap<void*>* AttrTable<T*>::s_hash = &g_hash_ptr; diff --git a/src/expr/expr_builder.cpp b/src/expr/node_builder.cpp index 10152a338..83d2ae41d 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/node_builder.cpp @@ -9,46 +9,46 @@ ** **/ -#include "expr_builder.h" -#include "expr_manager.h" -#include "expr_value.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/expr_value.h" #include "util/output.h" using namespace std; namespace CVC4 { -ExprBuilder::ExprBuilder() : - d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), +NodeBuilder::NodeBuilder() : + d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(Kind k) : - d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) { +NodeBuilder::NodeBuilder(Kind k) : + d_em(NodeManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(const Expr& e) : - d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { +NodeBuilder::NodeBuilder(const Node& e) : + d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { d_children.u_arr[0] = e.d_ev->inc();; } -ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { - this->~ExprBuilder(); +NodeBuilder& NodeBuilder::reset(const ExprValue* ev) { + this->~NodeBuilder(); d_kind = Kind(ev->d_kind); d_used = false; d_nchildren = ev->d_nchildren; - for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i) + for(Node::const_iterator i = ev->begin(); i != ev->end(); ++i) addChild(i->d_ev); return *this; } -ExprBuilder::ExprBuilder(const ExprBuilder& eb) : +NodeBuilder::NodeBuilder(const NodeBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) { Assert( !d_used ); if(d_nchildren > nchild_thresh) { - d_children.u_vec = new vector<Expr> (); + d_children.u_vec = new vector<Node> (); d_children.u_vec->reserve(d_nchildren + 5); copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec)); @@ -61,20 +61,20 @@ ExprBuilder::ExprBuilder(const ExprBuilder& eb) : } } -ExprBuilder::ExprBuilder(ExprManager* em) : +NodeBuilder::NodeBuilder(NodeManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : +NodeBuilder::NodeBuilder(NodeManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : +NodeBuilder::NodeBuilder(NodeManager* em, const Node& e) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { d_children.u_arr[0] = e.d_ev->inc(); } -ExprBuilder::~ExprBuilder() { +NodeBuilder::~NodeBuilder() { if(d_nchildren > nchild_thresh) { delete d_children.u_vec; } else { @@ -87,7 +87,7 @@ ExprBuilder::~ExprBuilder() { } // Compound expression constructors -ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { +NodeBuilder& NodeBuilder::eqExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(EXPECT_TRUE( d_kind != EQUAL )) { collapse(); @@ -97,7 +97,7 @@ ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::notExpr() { +NodeBuilder& NodeBuilder::notExpr() { Assert( d_kind != UNDEFINED_KIND ); collapse(); d_kind = NOT; @@ -105,7 +105,7 @@ ExprBuilder& ExprBuilder::notExpr() { } // avoid double-negatives -ExprBuilder& ExprBuilder::negate() { +NodeBuilder& NodeBuilder::negate() { if(EXPECT_FALSE( d_kind == NOT )) return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND ); collapse(); @@ -113,7 +113,7 @@ ExprBuilder& ExprBuilder::negate() { return *this; } -ExprBuilder& ExprBuilder::andExpr(const Expr& right) { +NodeBuilder& NodeBuilder::andExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(d_kind != AND) { collapse(); @@ -123,7 +123,7 @@ ExprBuilder& ExprBuilder::andExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::orExpr(const Expr& right) { +NodeBuilder& NodeBuilder::orExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(EXPECT_TRUE( d_kind != OR )) { collapse(); @@ -133,7 +133,7 @@ ExprBuilder& ExprBuilder::orExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) { +NodeBuilder& NodeBuilder::iteExpr(const Node& thenpart, const Node& elsepart) { Assert( d_kind != UNDEFINED_KIND ); collapse(); d_kind = ITE; @@ -142,7 +142,7 @@ ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) { return *this; } -ExprBuilder& ExprBuilder::iffExpr(const Expr& right) { +NodeBuilder& NodeBuilder::iffExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(EXPECT_TRUE( d_kind != IFF )) { collapse(); @@ -152,7 +152,7 @@ ExprBuilder& ExprBuilder::iffExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::impExpr(const Expr& right) { +NodeBuilder& NodeBuilder::impExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); collapse(); d_kind = IMPLIES; @@ -160,7 +160,7 @@ ExprBuilder& ExprBuilder::impExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { +NodeBuilder& NodeBuilder::xorExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(EXPECT_TRUE( d_kind != XOR )) { collapse(); @@ -171,12 +171,12 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { } // "Stream" expression constructor syntax -ExprBuilder& ExprBuilder::operator<<(const Kind& op) { +NodeBuilder& NodeBuilder::operator<<(const Kind& op) { d_kind = op; return *this; } -ExprBuilder& ExprBuilder::operator<<(const Expr& child) { +NodeBuilder& NodeBuilder::operator<<(const Node& child) { addChild(child); return *this; } @@ -190,28 +190,28 @@ ExprBuilder& ExprBuilder::operator<<(const Expr& child) { * reference count for each child. * (c) Otherwise we just add to the end of the vector. */ -void ExprBuilder::addChild(ExprValue* ev) { +void NodeBuilder::addChild(ExprValue* ev) { Assert(d_nchildren <= nchild_thresh || d_nchildren == d_children.u_vec->size(), "children count doesn't reflect the size of the vector!"); Debug("expr") << "adding child ev " << ev << endl; if(d_nchildren == nchild_thresh) { Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl; - vector<Expr>* v = new vector<Expr> (); + vector<Node>* v = new vector<Node> (); v->reserve(nchild_thresh + 5); ExprValue** i = d_children.u_arr; ExprValue** i_end = i + nchild_thresh; for(;i != i_end; ++ i) { - v->push_back(Expr(*i)); + v->push_back(Node(*i)); (*i)->dec(); } - v->push_back(Expr(ev)); + v->push_back(Node(ev)); d_children.u_vec = v; ++d_nchildren; } else if(d_nchildren > nchild_thresh) { Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl; - d_children.u_vec->push_back(Expr(ev)); + d_children.u_vec->push_back(Node(ev)); // ++d_nchildren; no need for this } else { Debug("expr") << "under thresh " << d_nchildren @@ -220,9 +220,9 @@ void ExprBuilder::addChild(ExprValue* ev) { } } -ExprBuilder& ExprBuilder::collapse() { +NodeBuilder& NodeBuilder::collapse() { if(d_nchildren == nchild_thresh) { - vector<Expr>* v = new vector<Expr> (); + vector<Node>* v = new vector<Node> (); v->reserve(nchild_thresh + 5); // Unreachable();// unimplemented diff --git a/src/expr/expr_builder.h b/src/expr/node_builder.h index 34e34bf6e..be96c2e77 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/node_builder.h @@ -15,8 +15,8 @@ #include <vector> #include <cstdlib> -#include "expr_manager.h" -#include "kind.h" +#include "expr/node_manager.h" +#include "expr/kind.h" #include "util/Assert.h" namespace CVC4 { @@ -27,12 +27,12 @@ class PlusExprBuilder; class MinusExprBuilder; class MultExprBuilder; -class ExprBuilder { - ExprManager* d_em; +class NodeBuilder { + NodeManager* d_em; Kind d_kind; - // initially false, when you extract the Expr this is set and you can't + // initially false, when you extract the Node this is set and you can't // extract another bool d_used; @@ -41,12 +41,12 @@ class ExprBuilder { unsigned d_nchildren; union { ExprValue* u_arr[nchild_thresh]; - std::vector<Expr>* u_vec; + std::vector<Node>* u_vec; } d_children; - void addChild(const Expr& e) { addChild(e.d_ev); } + void addChild(const Node& e) { addChild(e.d_ev); } void addChild(ExprValue*); - ExprBuilder& collapse(); + NodeBuilder& collapse(); typedef ExprValue** ev_iterator; typedef ExprValue const** const_ev_iterator; @@ -59,148 +59,148 @@ class ExprBuilder { return d_children.u_arr + d_nchildren; } - ExprBuilder& reset(const ExprValue*); + NodeBuilder& reset(const ExprValue*); public: - ExprBuilder(); - ExprBuilder(Kind k); - ExprBuilder(const Expr&); - ExprBuilder(const ExprBuilder&); + NodeBuilder(); + NodeBuilder(Kind k); + NodeBuilder(const Node&); + NodeBuilder(const NodeBuilder&); - ExprBuilder(ExprManager*); - ExprBuilder(ExprManager*, Kind k); - ExprBuilder(ExprManager*, const Expr&); - ExprBuilder(ExprManager*, const ExprBuilder&); + NodeBuilder(NodeManager*); + NodeBuilder(NodeManager*, Kind k); + NodeBuilder(NodeManager*, const Node&); + NodeBuilder(NodeManager*, const NodeBuilder&); - ~ExprBuilder(); + ~NodeBuilder(); // Compound expression constructors - ExprBuilder& eqExpr(const Expr& right); - ExprBuilder& notExpr(); - ExprBuilder& negate(); // avoid double-negatives - ExprBuilder& andExpr(const Expr& right); - ExprBuilder& orExpr(const Expr& right); - ExprBuilder& iteExpr(const Expr& thenpart, const Expr& elsepart); - ExprBuilder& iffExpr(const Expr& right); - ExprBuilder& impExpr(const Expr& right); - ExprBuilder& xorExpr(const Expr& right); - - /* TODO design: these modify ExprBuilder */ - ExprBuilder& operator!() { return notExpr(); } - ExprBuilder& operator&&(const Expr& right) { return andExpr(right); } - ExprBuilder& operator||(const Expr& right) { return orExpr(right); } + NodeBuilder& eqExpr(const Node& right); + NodeBuilder& notExpr(); + NodeBuilder& negate(); // avoid double-negatives + NodeBuilder& andExpr(const Node& right); + NodeBuilder& orExpr(const Node& right); + NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart); + NodeBuilder& iffExpr(const Node& right); + NodeBuilder& impExpr(const Node& right); + NodeBuilder& xorExpr(const Node& right); + + /* TODO design: these modify NodeBuilder */ + NodeBuilder& operator!() { return notExpr(); } + NodeBuilder& operator&&(const Node& right) { return andExpr(right); } + NodeBuilder& operator||(const Node& right) { return orExpr(right); } // "Stream" expression constructor syntax - ExprBuilder& operator<<(const Kind& op); - ExprBuilder& operator<<(const Expr& child); + NodeBuilder& operator<<(const Kind& op); + NodeBuilder& operator<<(const Node& child); // For pushing sequences of children - ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); } - ExprBuilder& append(Expr child) { return append(&child, (&child) + 1); } - template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end); + NodeBuilder& append(const std::vector<Node>& children) { return append(children.begin(), children.end()); } + NodeBuilder& append(Node child) { return append(&child, (&child) + 1); } + template <class Iterator> NodeBuilder& append(const Iterator& begin, const Iterator& end); - operator Expr();// not const + operator Node();// not const - AndExprBuilder operator&&(Expr); - OrExprBuilder operator||(Expr); - PlusExprBuilder operator+ (Expr); - PlusExprBuilder operator- (Expr); - MultExprBuilder operator* (Expr); + AndExprBuilder operator&&(Node); + OrExprBuilder operator||(Node); + PlusExprBuilder operator+ (Node); + PlusExprBuilder operator- (Node); + MultExprBuilder operator* (Node); friend class AndExprBuilder; friend class OrExprBuilder; friend class PlusExprBuilder; friend class MultExprBuilder; -};/* class ExprBuilder */ +};/* class NodeBuilder */ class AndExprBuilder { - ExprBuilder d_eb; + NodeBuilder d_eb; public: - AndExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != AND) { d_eb.collapse(); d_eb.d_kind = AND; } } - AndExprBuilder& operator&&(Expr); - OrExprBuilder operator||(Expr); + AndExprBuilder& operator&&(Node); + OrExprBuilder operator||(Node); - operator ExprBuilder() { return d_eb; } + operator NodeBuilder() { return d_eb; } };/* class AndExprBuilder */ class OrExprBuilder { - ExprBuilder d_eb; + NodeBuilder d_eb; public: - OrExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != OR) { d_eb.collapse(); d_eb.d_kind = OR; } } - AndExprBuilder operator&&(Expr); - OrExprBuilder& operator||(Expr); + AndExprBuilder operator&&(Node); + OrExprBuilder& operator||(Node); - operator ExprBuilder() { return d_eb; } + operator NodeBuilder() { return d_eb; } };/* class OrExprBuilder */ class PlusExprBuilder { - ExprBuilder d_eb; + NodeBuilder d_eb; public: - PlusExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != PLUS) { d_eb.collapse(); d_eb.d_kind = PLUS; } } - PlusExprBuilder& operator+(Expr); - PlusExprBuilder& operator-(Expr); - MultExprBuilder operator*(Expr); + PlusExprBuilder& operator+(Node); + PlusExprBuilder& operator-(Node); + MultExprBuilder operator*(Node); - operator ExprBuilder() { return d_eb; } + operator NodeBuilder() { return d_eb; } };/* class PlusExprBuilder */ class MultExprBuilder { - ExprBuilder d_eb; + NodeBuilder d_eb; public: - MultExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != MULT) { d_eb.collapse(); d_eb.d_kind = MULT; } } - PlusExprBuilder operator+(Expr); - PlusExprBuilder operator-(Expr); - MultExprBuilder& operator*(Expr); + PlusExprBuilder operator+(Node); + PlusExprBuilder operator-(Node); + MultExprBuilder& operator*(Node); - operator ExprBuilder() { return d_eb; } + operator NodeBuilder() { return d_eb; } };/* class MultExprBuilder */ template <class Iterator> -inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { +inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) { for(Iterator i = begin; i != end; ++i) addChild(*i); return *this; } // not const -inline ExprBuilder::operator Expr() { +inline NodeBuilder::operator Node() { ExprValue *ev; uint64_t hash; @@ -213,7 +213,7 @@ inline ExprBuilder::operator Expr() { } else { if(d_nchildren <= nchild_thresh) { hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end()); - void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr)); + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); ev = new (space) ExprValue; size_t nc = 0; ev_iterator i = ev_begin(); @@ -224,12 +224,12 @@ inline ExprBuilder::operator Expr() { ev->d_children[nc++].assignExprValue(*i); } } else { - hash = ExprValue::computeHash<std::vector<Expr>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end()); - void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr)); + hash = ExprValue::computeHash<std::vector<Node>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end()); + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); ev = new (space) ExprValue; size_t nc = 0; - for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) - ev->d_children[nc++] = Expr(*i); + for(std::vector<Node>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) + ev->d_children[nc++] = Node(*i); } } @@ -237,72 +237,72 @@ inline ExprBuilder::operator Expr() { ev->d_kind = d_kind; ev->d_id = ExprValue::next_id++;// FIXME multithreading ev->d_rc = 0; - Expr e(ev); + Node e(ev); return d_em->lookup(hash, e); } -inline AndExprBuilder ExprBuilder::operator&&(Expr e) { +inline AndExprBuilder NodeBuilder::operator&&(Node e) { return AndExprBuilder(*this) && e; } -inline OrExprBuilder ExprBuilder::operator||(Expr e) { +inline OrExprBuilder NodeBuilder::operator||(Node e) { return OrExprBuilder(*this) || e; } -inline PlusExprBuilder ExprBuilder::operator+ (Expr e) { +inline PlusExprBuilder NodeBuilder::operator+ (Node e) { return PlusExprBuilder(*this) + e; } -inline PlusExprBuilder ExprBuilder::operator- (Expr e) { +inline PlusExprBuilder NodeBuilder::operator- (Node e) { return PlusExprBuilder(*this) - e; } -inline MultExprBuilder ExprBuilder::operator* (Expr e) { +inline MultExprBuilder NodeBuilder::operator* (Node e) { return MultExprBuilder(*this) * e; } -inline AndExprBuilder& AndExprBuilder::operator&&(Expr e) { +inline AndExprBuilder& AndExprBuilder::operator&&(Node e) { d_eb.append(e); return *this; } -inline OrExprBuilder AndExprBuilder::operator||(Expr e) { +inline OrExprBuilder AndExprBuilder::operator||(Node e) { return OrExprBuilder(d_eb.collapse()) || e; } -inline AndExprBuilder OrExprBuilder::operator&&(Expr e) { +inline AndExprBuilder OrExprBuilder::operator&&(Node e) { return AndExprBuilder(d_eb.collapse()) && e; } -inline OrExprBuilder& OrExprBuilder::operator||(Expr e) { +inline OrExprBuilder& OrExprBuilder::operator||(Node e) { d_eb.append(e); return *this; } -inline PlusExprBuilder& PlusExprBuilder::operator+(Expr e) { +inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) { d_eb.append(e); return *this; } -inline PlusExprBuilder& PlusExprBuilder::operator-(Expr e) { +inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) { d_eb.append(e.negate()); return *this; } -inline MultExprBuilder PlusExprBuilder::operator*(Expr e) { +inline MultExprBuilder PlusExprBuilder::operator*(Node e) { return MultExprBuilder(d_eb.collapse()) * e; } -inline PlusExprBuilder MultExprBuilder::operator+(Expr e) { +inline PlusExprBuilder MultExprBuilder::operator+(Node e) { return MultExprBuilder(d_eb.collapse()) + e; } -inline PlusExprBuilder MultExprBuilder::operator-(Expr e) { +inline PlusExprBuilder MultExprBuilder::operator-(Node e) { return MultExprBuilder(d_eb.collapse()) - e; } -inline MultExprBuilder& MultExprBuilder::operator*(Expr e) { +inline MultExprBuilder& MultExprBuilder::operator*(Node e) { d_eb.append(e); return *this; } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp new file mode 100644 index 000000000..3c15aa9c4 --- /dev/null +++ b/src/expr/node_manager.cpp @@ -0,0 +1,93 @@ +/********************* -*- C++ -*- */ +/** expr_manager.cpp + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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. + ** + ** Expression manager implementation. + **/ + +#include "node_builder.h" +#include "node_manager.h" +#include "expr/node.h" + +namespace CVC4 { + +__thread NodeManager* NodeManager::s_current = 0; + +Node NodeManager::lookup(uint64_t hash, const Node& e) { + Assert(this != NULL, "Woops, we have a bad expression manager!"); + hash_t::iterator i = d_hash.find(hash); + if(i == d_hash.end()) { + // insert + std::vector<Node> v; + v.push_back(e); + d_hash.insert(std::make_pair(hash, v)); + return e; + } else { + for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) { + if(e.getKind() != j->getKind()) + continue; + + if(e.numChildren() != j->numChildren()) + continue; + + Node::const_iterator c1 = e.begin(); + Node::iterator c2 = j->begin(); + for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { + if(c1->d_ev != c2->d_ev) + break; + } + + if(c1 != e.end() || c2 != j->end()) + continue; + + return *j; + } + // didn't find it, insert + std::vector<Node> v; + v.push_back(e); + d_hash.insert(std::make_pair(hash, v)); + return e; + } +} + +// general expression-builders + +Node NodeManager::mkExpr(Kind kind) { + return NodeBuilder(this, kind); +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1) { + return NodeBuilder(this, kind) << child1; +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) { + return NodeBuilder(this, kind) << child1 << child2; +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) { + return NodeBuilder(this, kind) << child1 << child2 << child3; +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) { + return NodeBuilder(this, kind) << child1 << child2 << child3 << child4; +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) { + return NodeBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; +} + +// N-ary version +Node NodeManager::mkExpr(Kind kind, std::vector<Node> children) { + return NodeBuilder(this, kind).append(children); +} + +Node NodeManager::mkVar() { + return NodeBuilder(this, VARIABLE); +} + +}/* CVC4 namespace */ diff --git a/src/expr/expr_manager.h b/src/expr/node_manager.h index 542d1040d..ca15d88b4 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/node_manager.h @@ -15,7 +15,7 @@ #include <vector> #include <map> -#include "expr/expr.h" +#include "node.h" #include "kind.h" namespace CVC4 { @@ -24,45 +24,45 @@ namespace expr { class ExprBuilder; }/* CVC4::expr namespace */ -class CVC4_PUBLIC ExprManager { - static __thread ExprManager* s_current; +class CVC4_PUBLIC NodeManager { + static __thread NodeManager* s_current; - friend class CVC4::ExprBuilder; + friend class CVC4::NodeBuilder; - typedef std::map<uint64_t, std::vector<Expr> > hash_t; + typedef std::map<uint64_t, std::vector<Node> > hash_t; hash_t d_hash; - Expr lookup(uint64_t hash, const Expr& e); + Node lookup(uint64_t hash, const Node& e); public: - static ExprManager* currentEM() { return s_current; } + static NodeManager* currentEM() { return s_current; } // general expression-builders - Expr mkExpr(Kind kind); - Expr mkExpr(Kind kind, const Expr& child1); - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2); - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3); - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4); - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5); + Node mkExpr(Kind kind); + Node mkExpr(Kind kind, const Node& child1); + Node mkExpr(Kind kind, const Node& child1, const Node& child2); + Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3); + Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4); + Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5); // N-ary version - Expr mkExpr(Kind kind, std::vector<Expr> children); + Node mkExpr(Kind kind, std::vector<Node> children); // variables are special, because duplicates are permitted - Expr mkVar(); + Node mkVar(); // TODO: these use the current EM (but must be renamed) /* - static Expr mkExpr(Kind kind) + static Node mkExpr(Kind kind) { currentEM()->mkExpr(kind); } - static Expr mkExpr(Kind kind, Expr child1); + static Node mkExpr(Kind kind, Node child1); { currentEM()->mkExpr(kind, child1); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2); + static Node mkExpr(Kind kind, Node child1, Node child2); { currentEM()->mkExpr(kind, child1, child2); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3); { currentEM()->mkExpr(kind, child1, child2, child3); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4); { currentEM()->mkExpr(kind, child1, child2, child3, child4); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5); { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } */ |