diff options
| author | Morgan Deters <mdeters@gmail.com> | 2009-12-16 04:25:45 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2009-12-16 04:25:45 +0000 |
| commit | 79df573326e6911d3a97fcc2528105acd1c2c525 (patch) | |
| tree | 70930bcdb620cdf8ff9e3e9c495f67ed8317aa2e /src/expr/node_manager.h | |
| parent | 8cb3a7b556e8b4b85745bffbd1f0246e6af29588 (diff) | |
Fixes to the build system:
Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS
Makefile files in src/ - support "make" under src/ (current build profile)
configure.ac - updates to fix warnings
config/antlr.m4 - updates to fix warnings
autogen.sh - updates to generate warnings from autotools; also support Macs
src/include/cvc4_config.h - guard with #ifdef
total reimplementation of NodeBuilder
ExprValue => NodeValue
context_mm.{h,cpp} - fixed numerous compile errors
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 26 |
1 files changed, 12 insertions, 14 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6c20b29e8..3a28a22ff 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -20,22 +20,20 @@ namespace CVC4 { -namespace expr { - class ExprBuilder; -}/* CVC4::expr namespace */ - class NodeManager { static __thread NodeManager* s_current; - friend class CVC4::NodeBuilder; + template <unsigned> friend class CVC4::NodeBuilder; typedef std::map<uint64_t, std::vector<Node> > hash_t; hash_t d_hash; - Node lookup(uint64_t hash, const Node& e); + Node lookup(uint64_t hash, const Node& e) { return lookup(hash, e.d_ev); } + Node lookup(uint64_t hash, NodeValue* e); + NodeValue* lookupNoInsert(uint64_t hash, NodeValue* e); public: - static NodeManager* currentEM() { return s_current; } + static NodeManager* currentNM() { return s_current; } // general expression-builders Node mkExpr(Kind kind); @@ -50,20 +48,20 @@ public: // variables are special, because duplicates are permitted Node mkVar(); - // TODO: these use the current EM (but must be renamed) + // TODO: these use the current NM (but must be renamed) /* static Node mkExpr(Kind kind) - { currentEM()->mkExpr(kind); } + { currentNM()->mkExpr(kind); } static Node mkExpr(Kind kind, Node child1); - { currentEM()->mkExpr(kind, child1); } + { currentNM()->mkExpr(kind, child1); } static Node mkExpr(Kind kind, Node child1, Node child2); - { currentEM()->mkExpr(kind, child1, child2); } + { currentNM()->mkExpr(kind, child1, child2); } static Node mkExpr(Kind kind, Node child1, Node child2, Node child3); - { currentEM()->mkExpr(kind, child1, child2, child3); } + { currentNM()->mkExpr(kind, child1, child2, child3); } static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4); - { currentEM()->mkExpr(kind, child1, child2, child3, child4); } + { currentNM()->mkExpr(kind, child1, child2, child3, child4); } static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5); - { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } + { currentNM()->mkExpr(kind, child1, child2, child3, child4, child5); } */ // do we want a varargs one? perhaps not.. |