diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
commit | 826f583ee14b922f39666dc827a5624fff753724 (patch) | |
tree | 03e7f1ad98b003dae5f6406bb990a715041d239c /src/expr | |
parent | f716b67e7bedd90c4dd43617158c0f55c1811334 (diff) |
* src/expr/node.h: add a copy constructor. Apparently GCC doesn't
recognize an instantiation of the join conversion/copy ctor with
ref_count = ref_count_1 as a copy constructor. Problems with
reference counts ensue.
* src/theory/theory.h, src/theory/theory.cpp: Theory base
implementation work. Changed from continuation-style theory calls
to having an data member for the output channel. registerTerm() and
preRegisterTerm() work.
* src/theory/output_channel.h, src/theory/theory.h,
src/theory/theory.cpp, src/theory/uf/theory_uf.h,
src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into
OutputChannel.
* test/unit/expr/node_black.h: remove testPlusNode(),
testUMinusNode(), testMultNode().
* src/expr/attribute.h: new facilities ManagedAttribute<> and
CDAttribute<>, and add new template parameters to Attribute<>. Make
CDAttribute<>s work with context manager.
* src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and
TypeAttr are now "owned" (defined) by the NodeManager. The
AttributeManager knows nothing of specific attributes, it just as
all the code for dealing generically with attributes.
* test/unit/expr/node_white.h: test new attribute facilities.
* src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes
away.
* src/theory/Makefile.am: fixed improper linking of theories
* src/theory/theory_engine.h: some implementation work (mainly stubs
for now, just to make sure TheoryUF can be instantiated properly,
etc.)
* src/expr/node_value.cpp, src/expr/node_value.h: move a number of
function implementations to the header and make them inline
* src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of
function implementations to the header and make them inline
* src/theory/theoryof_table_prologue.h,
src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof,
src/theory/Makefile.am: make the theoryOf() table from kinds and
implement TheoryEngine::theoryOf().
* src/theory/arith/Makefile, src/theory/bool/Makefile: generated these
stub Makefiles (with contrib/addsourcedir) as per policy
* src/theory/arith, src/theory/bool [directory properties]: add .deps
to svn:ignore.
* contrib/configure-in-place: permit configuring "in-place" in the
source directory.
* contrib/get-authors, contrib/dimacs_to_smt.pl,
contrib/update-copyright.pl, contrib/get-authors,
contrib/addsourcedir, src/expr/mkkind: copyright notice
* src/expr/node_manager.h, src/expr/node_builder.h,
src/prop/prop_engine.h, src/prop/prop_engine.cpp,
src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp,
src/theory/output_channel.h: turn "const Node&"-typed formal
parameters into "TNode"
* src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans"
to avoid keyword clash on containing namespace
* src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h,
src/theory/arith/theory_def.h: "define" a theory simply (for automatic
theoryOf() generator).
* src/Makefile.am: build theory subdirectory before prop, smt, etc. so that
src/theory/theoryof_table.h header gets generated before it's needed
* src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a
separate CVC4::kind namespace to avoid its contents from cluttering
the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace
but not the enum values.
* src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h,
src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp,
src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g,
src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp,
test/unit/expr/node_white.h, test/unit/expr/node_black.h,
test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h:
update for having moved Kind into CVC4::kind.
* src/parser/parser.cpp: added file-does-not-exist check (was failing
silently).
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 6 | ||||
-rw-r--r-- | src/expr/attribute.h | 541 | ||||
-rw-r--r-- | src/expr/expr.cpp | 2 | ||||
-rw-r--r-- | src/expr/kind_middle.h | 10 | ||||
-rw-r--r-- | src/expr/kind_prologue.h | 3 | ||||
-rwxr-xr-x | src/expr/mkkind | 3 | ||||
-rw-r--r-- | src/expr/node.h | 95 | ||||
-rw-r--r-- | src/expr/node_builder.h | 41 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 59 | ||||
-rw-r--r-- | src/expr/node_manager.h | 121 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 57 | ||||
-rw-r--r-- | src/expr/node_value.h | 55 | ||||
-rw-r--r-- | src/expr/soft_node.h | 36 |
13 files changed, 663 insertions, 366 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index a75b97b74..27c64e9ef 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -24,7 +24,11 @@ libexpr_la_SOURCES = \ command.h \ command.cpp -EXTRA_DIST = @srcdir@/kind.h kind_prologue.h kind_middle.h kind_epilogue.h +EXTRA_DIST = \ + @srcdir@/kind.h \ + kind_prologue.h \ + kind_middle.h \ + kind_epilogue.h @srcdir@/kind.h: @srcdir@/mkkind kind_prologue.h kind_middle.h kind_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds chmod +x @srcdir@/mkkind diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 5620d7795..4bc569620 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -11,23 +11,6 @@ ** information. ** ** Node attributes. - ** - ** Attribute structures: - ** - ** An attribute structure looks like the following: - ** - ** struct VarNameAttr { - ** - ** // the value type for this attribute - ** typedef std::string value_type; - ** - ** // an extra hash value (to avoid same-value-type collisions) - ** enum { hash_value = 1 }; - ** - ** // cleanup routine when the Node goes away - ** static inline void cleanup(const std::string&) { - ** } - ** } **/ /* There are strong constraints on ordering of declarations of @@ -44,7 +27,7 @@ #include "config.h" #include "context/context.h" -#include "expr/soft_node.h" +#include "expr/node.h" #include "expr/type.h" #include "util/output.h" @@ -54,81 +37,149 @@ namespace expr { // ATTRIBUTE HASH FUNCTIONS ==================================================== +namespace attr { + +/** + * A hash function for attribute table keys. Attribute table keys are + * pairs, (unique-attribute-id, Node). + */ struct AttrHashFcn { - enum { LARGE_PRIME = 1 }; - std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const { + enum { LARGE_PRIME = 32452843ul }; + std::size_t operator()(const std::pair<uint64_t, TNode>& p) const { return p.first * LARGE_PRIME + p.second.hash(); } }; +/** + * A hash function for boolean-valued attribute table keys; here we + * don't have to store a pair as the key, because we use a known bit + * in [0..63] for each attribute + */ struct AttrHashBoolFcn { - std::size_t operator()(const SoftNode& n) const { + std::size_t operator()(TNode n) const { return n.hash(); } }; +}/* CVC4::expr::attr namespace */ + // ATTRIBUTE TYPE MAPPINGS ===================================================== +namespace attr { + +/** + * KindValueToTableValueMapping is a compile-time-only mechanism to + * convert "attribute value types" into "table value types" and back + * again. + * + * Each instantiation <T> is expected to have three members: + * + * typename table_value_type + * + * A type representing the underlying table's value_type for + * attribute value type (T). It may be different from T, e.g. T + * could be a pointer-to-Foo, but the underlying table value_type + * might be pointer-to-void. + * + * static [convertible-to-table_value_type] convert([convertible-from-T]) + * + * Converts a T into a table_value_type. Used to convert an + * attribute value on setting it (and assigning it into the + * underlying table). See notes on specializations of + * KindValueToTableValueMapping, below. + * + * static [convertible-to-T] convertBack([convertible-from-table_value_type]) + * + * Converts a table_value_type back into a T. Used to convert an + * underlying table value back into the attribute's expected type + * when retrieving it from the table. See notes on + * specializations of KindValueToTableValueMapping, below. + * + * This general (non-specialized) implementation of the template does + * nothing. + */ template <class T> struct KindValueToTableValueMapping { + /** Simple case: T == table_value_type */ typedef T table_value_type; + /** No conversion necessary */ inline static T convert(const T& t) { return t; } + /** No conversion necessary */ inline static T convertBack(const T& t) { return t; } }; -template <> -struct KindValueToTableValueMapping<bool> { - typedef uint64_t table_value_type; - inline static uint64_t convert(const bool& t) { return t; } - inline static bool convertBack(const uint64_t& t) { return t; } -}; - +/** + * Specialization of KindValueToTableValueMapping<> for pointer-valued + * attributes. + */ template <class T> struct KindValueToTableValueMapping<T*> { + /** Table's value type is void* */ typedef void* table_value_type; + /** A simple reinterpret_cast<>() conversion from T* to void* */ inline static void* convert(const T* const& t) { return reinterpret_cast<void*>(const_cast<T*>(t)); } + /** A simple reinterpret_cast<>() conversion from void* to T* */ inline static T* convertBack(void* const& t) { return reinterpret_cast<T*>(t); } }; +/** + * Specialization of KindValueToTableValueMapping<> for const + * pointer-valued attributes. + */ template <class T> struct KindValueToTableValueMapping<const T*> { + /** Table's value type is void* */ typedef void* table_value_type; + /** A simple reinterpret_cast<>() conversion from const T* const to void* */ inline static void* convert(const T* const& t) { return reinterpret_cast<void*>(const_cast<T*>(t)); } + /** A simple reinterpret_cast<>() conversion from const void* const to T* */ inline static const T* convertBack(const void* const& t) { return reinterpret_cast<const T*>(t); } }; -template <class AttrKind, class T> -struct OwnTable; - -template <class AttrKind, class T> -struct KindValueToTableValueMapping<OwnTable<AttrKind, T> > { - typedef typename KindValueToTableValueMapping<T>::table_value_type table_value_type; -}; - -template <class AttrKind> -struct KindTableMapping { - typedef typename AttrKind::value_type table_identifier; -}; +}/* CVC4::expr::attr namespace */ // ATTRIBUTE HASH TABLES ======================================================= -// use a TAG to indicate which table it should be in +namespace attr { + +/** + * An "AttrHash<value_type>"---the hash table underlying + * attributes---is simply a mapping of pair<unique-attribute-id, Node> + * to value_type using our specialized hash function for these pairs. + */ template <class value_type> -struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {}; +struct AttrHash : + public __gnu_cxx::hash_map<std::pair<uint64_t, TNode>, + value_type, + AttrHashFcn> { +}; +/** + * In the case of Boolean-valued attributes we have a special + * "AttrHash<bool>" to pack bits together in words. + */ template <> -class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> { - - typedef __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> super; - +class AttrHash<bool> : + protected __gnu_cxx::hash_map<TNode, + uint64_t, + AttrHashBoolFcn> { + + /** A "super" type, like in Java, for easy reference below. */ + typedef __gnu_cxx::hash_map<TNode, uint64_t, AttrHashBoolFcn> super; + + /** + * BitAccessor allows us to return a bit "by reference." Of course, + * we don't require bit-addressibility supported by the system, we + * do it with a complex type. + */ class BitAccessor { uint64_t& d_word; @@ -159,9 +210,15 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas } }; + /** + * A (somewhat degenerate) iterator over boolean-valued attributes. + * This iterator doesn't support anything except comparison and + * dereference. It's intended just for the result of find() on the + * table. + */ class BitIterator { - std::pair<const SoftNode, uint64_t>* d_entry; + std::pair<const TNode, uint64_t>* d_entry; unsigned d_bit; @@ -172,12 +229,12 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas d_bit(0) { } - BitIterator(std::pair<const SoftNode, uint64_t>& entry, unsigned bit) : + BitIterator(std::pair<const TNode, uint64_t>& entry, unsigned bit) : d_entry(&entry), d_bit(bit) { } - std::pair<const SoftNode, BitAccessor> operator*() { + std::pair<const TNode, BitAccessor> operator*() { return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit)); } @@ -186,9 +243,15 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas } }; + /** + * A (somewhat degenerate) const_iterator over boolean-valued + * attributes. This const_iterator doesn't support anything except + * comparison and dereference. It's intended just for the result of + * find() on the table. + */ class ConstBitIterator { - const std::pair<const SoftNode, uint64_t>* d_entry; + const std::pair<const TNode, uint64_t>* d_entry; unsigned d_bit; @@ -199,12 +262,12 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas d_bit(0) { } - ConstBitIterator(const std::pair<const SoftNode, uint64_t>& entry, unsigned bit) : + ConstBitIterator(const std::pair<const TNode, uint64_t>& entry, unsigned bit) : d_entry(&entry), d_bit(bit) { } - std::pair<const SoftNode, bool> operator*() { + std::pair<const TNode, bool> operator*() { return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false); } @@ -215,14 +278,20 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas public: - typedef std::pair<uint64_t, SoftNode> key_type; + typedef std::pair<uint64_t, TNode> key_type; typedef bool data_type; typedef std::pair<const key_type, data_type> value_type; + /** an iterator type; see above for limitations */ typedef BitIterator iterator; + /** a const_iterator type; see above for limitations */ typedef ConstBitIterator const_iterator; - BitIterator find(const std::pair<uint64_t, SoftNode>& k) { + /** + * Find the boolean value in the hash table. Returns something == + * end() if not found. + */ + BitIterator find(const std::pair<uint64_t, TNode>& k) { super::iterator i = super::find(k.second); if(i == super::end()) { return BitIterator(); @@ -235,11 +304,16 @@ public: return BitIterator(*i, k.first); } + /** The "off the end" iterator */ BitIterator end() { return BitIterator(); } - ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const { + /** + * Find the boolean value in the hash table. Returns something == + * end() if not found. + */ + ConstBitIterator find(const std::pair<uint64_t, TNode>& k) const { super::const_iterator i = super::find(k.second); if(i == super::end()) { return ConstBitIterator(); @@ -252,154 +326,301 @@ public: return ConstBitIterator(*i, k.first); } + /** The "off the end" const_iterator */ ConstBitIterator end() const { return ConstBitIterator(); } - BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) { + /** + * Access the hash table using the underlying operator[]. Inserts + * the key into the table (associated to default value) if it's not + * already there. + */ + BitAccessor operator[](const std::pair<uint64_t, TNode>& k) { uint64_t& word = super::operator[](k.second); return BitAccessor(word, k.first); } };/* class AttrHash<bool> */ -// ATTRIBUTE PATTERN =========================================================== +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE CLEANUP FUNCTIONS ================================================= + +namespace attr { + +/** Default cleanup for unmanaged Attribute<> */ +template <class T> +struct AttributeCleanupFcn { + inline void cleanup(const T&) {} +}; + +/** Default cleanup for ManagedAttribute<> */ +template <class T> +struct ManagedAttributeCleanupFcn { +}; + +/** Specialization for T* */ +template <class T> +struct ManagedAttributeCleanupFcn<T*> { + inline void cleanup(T* p) { delete p; } +}; + +/** Specialization for const T* */ +template <class T> +struct ManagedAttributeCleanupFcn<const T*> { + inline void cleanup(const T* p) { delete p; } +}; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE DEFINITION ======================================================== /** * An "attribute type" structure. + * + * @param T the tag for the attribute kind. + * + * @param value_t the underlying value_type for the attribute kind + * + * @param CleanupFcn Clean-up routine for associated values when the + * Node goes away. Useful, e.g., for pointer-valued attributes when + * the values are "owned" by the table. + * + * @param context_dependent whether this attribute kind is + * context-dependent */ -template <class T, class value_t> +template <class T, + class value_t, + class CleanupFcn = attr::AttributeCleanupFcn<value_t>, + bool context_dependent = false> struct Attribute { - /** the value type for this attribute */ + /** The value type for this attribute. */ typedef value_t value_type; - /** cleanup routine when the Node goes away */ - static inline void cleanup(const value_t&) {} - + /** Get the unique ID associated to this attribute. */ static inline uint64_t getId() { return s_id; } - static inline uint64_t getHashValue() { return s_hashValue; } + /** + * This attribute does not have a default value: calling + * hasAttribute() for a Node that hasn't had this attribute set will + * return false, and getAttribute() for the Node will return a + * default-constructed value_type. + */ static const bool has_default_value = false; private: - /** an id */ + /** + * The unique ID associated to this attribute. Assigned statically, + * at load time. + */ static const uint64_t s_id; - - /** an extra hash value (to avoid same-value-type collisions) */ - static const uint64_t s_hashValue; }; /** * An "attribute type" structure for boolean flags (special). */ -template <class T> -struct Attribute<T, bool> { +template <class T, class CleanupFcn, bool context_dependent> +struct Attribute<T, bool, CleanupFcn, context_dependent> { - /** the value type for this attribute */ + /** The value type for this attribute; here, bool. */ typedef bool value_type; - /** cleanup routine when the Node goes away */ - static inline void cleanup(const bool&) {} - + /** Get the unique ID associated to this attribute. */ static inline uint64_t getId() { return s_id; } - static inline uint64_t getHashValue() { return s_hashValue; } + /** + * Such bool-valued attributes ("flags") have a default value: they + * are false for all nodes on entry. Calling hasAttribute() for a + * Node that hasn't had this attribute set will return true, and + * getAttribute() for the Node will return the default_value below. + */ static const bool has_default_value = true; + + /** + * Default value of the attribute for Nodes without one explicitly + * set. + */ static const bool default_value = false; + /** + * Check that the ID is a valid ID for bool-valued attributes. Fail + * an assert if not. Otherwise return the id. + */ static inline uint64_t checkID(uint64_t id) { - AlwaysAssert(id <= 63, - "Too many boolean node attributes registered during initialization !"); + AlwaysAssert( id <= 63, + "Too many boolean node attributes registered " + "during initialization !" ); return id; } private: - /** a bit assignment */ + /** IDs for bool-valued attributes are actually bit assignments. */ static const uint64_t s_id; - - /** an extra hash value (to avoid same-value-type collisions) */ - static const uint64_t s_hashValue; }; -// SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ====================================== - -namespace attr { - struct VarName {}; - struct Type {}; - - template <class T> - struct LastAttributeId { - static uint64_t s_id; - }; - - template <class T> - uint64_t LastAttributeId<T>::s_id = 0; -}/* CVC4::expr::attr namespace */ +// FIXME make context-dependent +template <class T, + class value_type> +struct CDAttribute : + public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, true> {}; -typedef Attribute<attr::VarName, std::string> VarNameAttr; -typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr; +// FIXME make context-dependent +template <class T, + class value_type, + class CleanupFcn = attr::ManagedAttributeCleanupFcn<value_type> > +struct ManagedAttribute : + public Attribute<T, value_type, CleanupFcn, false> {}; // ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= -template <class T, class value_t> -const uint64_t Attribute<T, value_t>::s_id = - attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++; -template <class T, class value_t> -const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id; +namespace attr { +/** + * This is the last-attribute-assigner. IDs are not globally + * unique; rather, they are unique for each table_value_type. + */ template <class T> -const uint64_t Attribute<T, bool>::s_id = - Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++); +struct LastAttributeId { + static uint64_t s_id; +}; + +/** Initially zero. */ template <class T> -const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id; +uint64_t LastAttributeId<T>::s_id = 0; -class AttributeManager; +}/* CVC4::expr::attr namespace */ -template <class T> -struct getTable { - //inline AttrHash<KindTableValueMapping<T> >& get(AttributeManager& am); -}; +/** Assign unique IDs to attributes at load time. */ +template <class T, class value_t, class CleanupFcn, bool context_dependent> +const uint64_t Attribute<T, value_t, CleanupFcn, context_dependent>::s_id = + attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type>::s_id++; + +/** + * Assign unique IDs to bool-valued attributes at load time, checking + * that they are in range. + */ +template <class T, class CleanupFcn, bool context_dependent> +const uint64_t Attribute<T, bool, CleanupFcn, context_dependent>::s_id = + Attribute<T, bool, CleanupFcn, context_dependent>::checkID(attr::LastAttributeId<bool>::s_id++); // ATTRIBUTE MANAGER =========================================================== +namespace attr { + +/** + * A container for the main attribute tables of the system. There's a + * one-to-one NodeManager : AttributeManager correspondence. + */ class AttributeManager { - NodeManager* d_nm; - AttrHash<bool> d_bools; + /** Underlying hash table for boolean-valued attributes */ + AttrHash<bool> d_bools; + /** Underlying hash table for integral-valued attributes */ AttrHash<uint64_t> d_ints; - AttrHash<SoftNode> d_exprs; + /** Underlying hash table for node-valued attributes */ + AttrHash<TNode> d_exprs; + /** Underlying hash table for string-valued attributes */ AttrHash<std::string> d_strings; + /** Underlying hash table for pointer-valued attributes */ AttrHash<void*> d_ptrs; + /** + * getTable<> is a helper template that gets the right table from an + * AttributeManager given its type. + */ template <class T> friend struct getTable; public: - AttributeManager(NodeManager* nm) : d_nm(nm) {} + /** Construct an attribute manager. */ + AttributeManager() {} + + /** + * Get a particular attribute on a particular node. + * + * @param n the node about which to inquire + * + * @param const AttrKind& the attribute kind to get + * + * @return the attribute value, if set, or a default-constructed + * AttrKind::value_type if not. + */ template <class AttrKind> - typename AttrKind::value_type getAttribute(const Node& n, + typename AttrKind::value_type getAttribute(TNode n, const AttrKind&) const; + // Note that there are two, distinct hasAttribute() declarations for + // a reason (rather than using a default argument): they permit more + // optimized code. The first (without parameter "ret") need never + // check whether its parameter is NULL. + + /** + * Determine if a particular attribute exists for a particular node. + * + * @param n the node about which to inquire + * + * @param const AttrKind& the attribute kind to inquire about + * + * @return true if the given node has the given attribute + */ template <class AttrKind> - bool hasAttribute(const Node& n, + bool hasAttribute(TNode n, const AttrKind&) const; + /** + * Determine if a particular attribute exists for a particular node, + * and get it if it does. + * + * @param n the node about which to inquire + * + * @param const AttrKind& the attribute kind to inquire about + * + * @param ret a pointer to a return value, set in case the node has + * the attribute + * + * @return true if the given node has the given attribute + */ template <class AttrKind> - bool hasAttribute(const Node& n, + bool hasAttribute(TNode n, const AttrKind&, - typename AttrKind::value_type*) const; - + typename AttrKind::value_type& ret) const; + + /** + * Set a particular attribute on a particular node. + * + * @param n the node for which to set the attribute + * + * @param const AttrKind& the attribute kind to set + * + * @param ret a pointer to a return value, set in case the node has + * the attribute + * + * @return true if the given node has the given attribute + */ template <class AttrKind> - void setAttribute(const Node& n, + void setAttribute(TNode n, const AttrKind&, const typename AttrKind::value_type& value); }; +}/* CVC4::expr::attr namespace */ + // MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER =============== +namespace attr { + +/** + * The getTable<> template provides (static) access to the + * AttributeManager field holding the table. + */ +template <class T> +struct getTable; + +/** Access the "d_bools" member of AttributeManager. */ template <> struct getTable<bool> { typedef AttrHash<bool> table_type; @@ -411,6 +632,7 @@ struct getTable<bool> { } }; +/** Access the "d_ints" member of AttributeManager. */ template <> struct getTable<uint64_t> { typedef AttrHash<uint64_t> table_type; @@ -422,9 +644,10 @@ struct getTable<uint64_t> { } }; +/** Access the "d_exprs" member of AttributeManager. */ template <> struct getTable<Node> { - typedef AttrHash<SoftNode> table_type; + typedef AttrHash<TNode> table_type; static inline table_type& get(AttributeManager& am) { return am.d_exprs; } @@ -433,6 +656,7 @@ struct getTable<Node> { } }; +/** Access the "d_strings" member of AttributeManager. */ template <> struct getTable<std::string> { typedef AttrHash<std::string> table_type; @@ -444,8 +668,9 @@ struct getTable<std::string> { } }; +/** Access the "d_ptrs" member of AttributeManager. */ template <class T> -struct getTable<const T*> { +struct getTable<T*> { typedef AttrHash<void*> table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; @@ -455,8 +680,9 @@ struct getTable<const T*> { } }; +/** Access the "d_ptrs" member of AttributeManager. */ template <class T> -struct getTable<T*> { +struct getTable<const T*> { typedef AttrHash<void*> table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; @@ -466,10 +692,15 @@ struct getTable<T*> { } }; +}/* CVC4::expr::attr namespace */ + // ATTRIBUTE MANAGER IMPLEMENTATIONS =========================================== +namespace attr { + +// implementation for AttributeManager::getAttribute() template <class AttrKind> -typename AttrKind::value_type AttributeManager::getAttribute(const Node& n, +typename AttrKind::value_type AttributeManager::getAttribute(TNode n, const AttrKind&) const { typedef typename AttrKind::value_type value_type; @@ -486,45 +717,56 @@ typename AttrKind::value_type AttributeManager::getAttribute(const Node& n, return mapping::convertBack((*i).second); } -/* helper template class for hasAttribute(), specialized based on +/* Helper template class for hasAttribute(), specialized based on * whether AttrKind has a "default value" that all Nodes implicitly * have or not. */ template <bool has_default, class AttrKind> struct HasAttribute; +/** + * Specialization of HasAttribute<> helper template for AttrKinds + * with a default value. + */ template <class AttrKind> struct HasAttribute<true, AttrKind> { + /** This implementation is simple; it's always true. */ static inline bool hasAttribute(const AttributeManager* am, - const Node& n) { + TNode n) { return true; } + /** + * This implementation returns the AttrKind's default value if the + * Node doesn't have the given attribute. + */ static inline bool hasAttribute(const AttributeManager* am, - const Node& n, - typename AttrKind::value_type* ret) { - if(ret != NULL) { - typedef typename AttrKind::value_type value_type; - typedef KindValueToTableValueMapping<value_type> mapping; - typedef typename getTable<value_type>::table_type table_type; - - const table_type& ah = getTable<value_type>::get(*am); - typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); - - if(i == ah.end()) { - *ret = AttrKind::default_value; - } else { - *ret = mapping::convertBack((*i).second); - } + TNode n, + typename AttrKind::value_type& ret) { + typedef typename AttrKind::value_type value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + typedef typename getTable<value_type>::table_type table_type; + + const table_type& ah = getTable<value_type>::get(*am); + typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + + if(i == ah.end()) { + ret = AttrKind::default_value; + } else { + ret = mapping::convertBack((*i).second); } return true; } }; +/** + * Specialization of HasAttribute<> helper template for AttrKinds + * without a default value. + */ template <class AttrKind> struct HasAttribute<false, AttrKind> { static inline bool hasAttribute(const AttributeManager* am, - const Node& n) { + TNode n) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; typedef typename getTable<value_type>::table_type table_type; @@ -540,8 +782,8 @@ struct HasAttribute<false, AttrKind> { } static inline bool hasAttribute(const AttributeManager* am, - const Node& n, - typename AttrKind::value_type* ret) { + TNode n, + typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping<value_type> mapping; typedef typename getTable<value_type>::table_type table_type; @@ -553,29 +795,27 @@ struct HasAttribute<false, AttrKind> { return false; } - if(ret != NULL) { - *ret = mapping::convertBack((*i).second); - } + ret = mapping::convertBack((*i).second); return true; } }; template <class AttrKind> -bool AttributeManager::hasAttribute(const Node& n, +bool AttributeManager::hasAttribute(TNode n, const AttrKind&) const { return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n); } template <class AttrKind> -bool AttributeManager::hasAttribute(const Node& n, +bool AttributeManager::hasAttribute(TNode n, const AttrKind&, - typename AttrKind::value_type* ret) const { + typename AttrKind::value_type& ret) const { return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n, ret); } template <class AttrKind> -inline void AttributeManager::setAttribute(const Node& n, +inline void AttributeManager::setAttribute(TNode n, const AttrKind&, const typename AttrKind::value_type& value) { @@ -587,6 +827,7 @@ inline void AttributeManager::setAttribute(const Node& n, ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value); } +}/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 7dc8c8f96..35bdc947a 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -19,6 +19,8 @@ #include "util/output.h" +using namespace CVC4::kind; + namespace CVC4 { std::ostream& operator<<(std::ostream& out, const Expr& e) { diff --git a/src/expr/kind_middle.h b/src/expr/kind_middle.h index 49e43ba68..a4ba5a92b 100644 --- a/src/expr/kind_middle.h +++ b/src/expr/kind_middle.h @@ -16,11 +16,17 @@ LAST_KIND -};/* enum Kind */ +};/* enum Kind_t */ + +}/* CVC4::kind namespace */ + +// import Kind into the "CVC4" namespace but keep the individual kind +// constants under kind:: +typedef ::CVC4::kind::Kind_t Kind; inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) { - using namespace CVC4; + using namespace CVC4::kind; switch(k) { diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h index 7f4a0a3a2..08468385b 100644 --- a/src/expr/kind_prologue.h +++ b/src/expr/kind_prologue.h @@ -20,8 +20,9 @@ #include <iostream> namespace CVC4 { +namespace kind { -enum Kind { +enum Kind_t { /* undefined */ UNDEFINED_KIND = -1, /** Null Kind */ diff --git a/src/expr/mkkind b/src/expr/mkkind index b0a8f4565..bc10f1e2c 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -2,6 +2,7 @@ # # mkkind # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project # # The purpose of this script is to create kind.h from a prologue, # middle, epilogue, and a list of theory kinds. @@ -17,7 +18,7 @@ cat <<EOF /********************* -*- C++ -*- */ /** kind.h ** - ** Copyright 2009, 2010 The AcSys Group, New York University, and as below. + ** Copyright 2010 The AcSys Group, New York University, and as below. ** ** This header file automatically generated by: ** diff --git a/src/expr/node.h b/src/expr/node.h index 03f3e9da3..19e50c5c2 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -28,6 +28,8 @@ #include "expr/type.h" #include "util/Assert.h" +#include "util/output.h" + namespace CVC4 { class Type; @@ -107,14 +109,22 @@ template<bool ref_count> NodeTemplate() : d_nv(&NodeValue::s_null) { } /** - * Copy constructor for nodes that can accept the nodes that are reference - * counted or not. + * Conversion between nodes that are reference-counted and those that are + * not. * @param node the node to make copy of */ template<bool ref_count_1> NodeTemplate(const NodeTemplate<ref_count_1>& node); /** + * Copy constructor. Note that GCC does NOT recognize an instantiation of + * the above template as a copy constructor and problems ensue. So we + * provide an explicit one here. + * @param node the node to make copy of + */ + NodeTemplate(const NodeTemplate<ref_count>& node); + + /** * Assignment operator for nodes, copies the relevant information from node * to this node. * @param node the node to copy @@ -233,9 +243,24 @@ template<bool ref_count> * @param attKind the kind of the attribute * @return the value of the attribute */ - template<class AttrKind> + template <class AttrKind> inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const; + // Note that there are two, distinct hasAttribute() declarations for + // a reason (rather than using a pointer-valued argument with a + // default value): they permit more optimized code in the underlying + // hasAttribute() implementations. + + /** + * Returns true if this node has been associated an attribute of given kind. + * Additionaly, if a pointer to the value_kind is give, and the attribute + * value has been set for this node, it will be returned. + * @param attKind the kind of the attribute + * @return true if this node has the requested attribute + */ + template <class AttrKind> + inline bool hasAttribute(const AttrKind& attKind) const; + /** * Returns true if this node has been associated an attribute of given kind. * Additionaly, if a pointer to the value_kind is give, and the attribute @@ -244,8 +269,17 @@ template<bool ref_count> * @param value where to store the value if it exists * @return true if this node has the requested attribute */ - template<class AttrKind> - inline bool hasAttribute(const AttrKind& attKind, typename AttrKind::value_type* value = NULL) const; + template <class AttrKind> + inline bool hasAttribute(const AttrKind& attKind, typename AttrKind::value_type& value) const; + + /** + * Sets the given attribute of this node to the given value. + * @param attKind the kind of the atribute + * @param value the value to set the attribute to + */ + template <class AttrKind> + inline void setAttribute(const AttrKind& attKind, + const typename AttrKind::value_type& value); /** Iterator allowing for scanning through the children. */ typedef typename NodeValue::iterator<ref_count> iterator; @@ -325,15 +359,6 @@ template<bool ref_count> NodeTemplate uMinusNode() const; NodeTemplate multNode(const NodeTemplate& right) const; - /** - * Sets the given attribute of this node to the given value. - * @param attKind the kind of the atribute - * @param value the value to set the attribute to - */ - template<class AttrKind> - inline void setAttribute(const AttrKind& attKind, - const typename AttrKind::value_type& value); - private: /** @@ -343,7 +368,6 @@ template<bool ref_count> */ void debugPrint(); - /** * Indents the given stream a given amount of spaces. * @param out the stream to indent @@ -404,7 +428,17 @@ template<bool ref_count> template<bool ref_count> template<class AttrKind> inline bool NodeTemplate<ref_count>:: - hasAttribute(const AttrKind&, typename AttrKind::value_type* ret) const { + 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 ?" ); + return NodeManager::currentNM()->hasAttribute(*this, AttrKind()); + } + +template<bool ref_count> + template<class AttrKind> + 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 ?" ); @@ -428,6 +462,7 @@ template<bool ref_count> ////TODO: Should use positive definition, i.e. what kinds are atomic. template<bool ref_count> bool NodeTemplate<ref_count>::isAtomic() const { + using namespace kind; switch(getKind()) { case NOT: case XOR: @@ -454,6 +489,8 @@ template<bool ref_count> d_nv->inc(); } +// the code for these two "conversion/copy constructors" is identical, but +// apparently we need both. see comment in the class. template<bool ref_count> template<bool ref_count_1> NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count_1>& e) { @@ -464,6 +501,14 @@ template<bool ref_count> } template<bool ref_count> + NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count>& e) { + Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); + d_nv = e.d_nv; + if(ref_count) + d_nv->inc(); + } + +template<bool ref_count> NodeTemplate<ref_count>::~NodeTemplate() { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); if(ref_count) @@ -498,48 +543,48 @@ template<bool ref_count> template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::eqNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(EQUAL, *this, right); + return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::notNode() const { - return NodeManager::currentNM()->mkNode(NOT, *this); + return NodeManager::currentNM()->mkNode(kind::NOT, *this); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::andNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(AND, *this, right); + return NodeManager::currentNM()->mkNode(kind::AND, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::orNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(OR, *this, right); + return NodeManager::currentNM()->mkNode(kind::OR, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::iteNode(const NodeTemplate< ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const { - return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); + return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::iffNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(IFF, *this, right); + return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::impNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); + return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); } template<bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::xorNode(const NodeTemplate< ref_count>& right) const { - return NodeManager::currentNM()->mkNode(XOR, *this, right); + return NodeManager::currentNM()->mkNode(kind::XOR, *this, right); } template<bool ref_count> @@ -547,7 +592,7 @@ template<bool ref_count> indent(out, ind); out << '('; out << getKind(); - if(getKind() == VARIABLE) { + if(getKind() == kind::VARIABLE) { out << ' ' << getId(); } else if(getNumChildren() >= 1) { diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index cd34c415b..0b89fcb5e 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -13,6 +13,9 @@ ** A builder interface for nodes. **/ +/* strong dependency; make sure node is included first */ +#include "node.h" + #ifndef __CVC4__NODE_BUILDER_H #define __CVC4__NODE_BUILDER_H @@ -145,42 +148,42 @@ public: return Node(d_nv->d_children[i]); } - void clear(Kind k = UNDEFINED_KIND); + void clear(Kind k = kind::UNDEFINED_KIND); // Compound expression constructors /* - NodeBuilder& eqExpr(const Node& right); + NodeBuilder& eqExpr(TNode right); NodeBuilder& notExpr(); - 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); + NodeBuilder& andExpr(TNode right); + NodeBuilder& orExpr(TNode right); + NodeBuilder& iteExpr(TNode thenpart, TNode elsepart); + NodeBuilder& iffExpr(TNode right); + NodeBuilder& impExpr(TNode right); + NodeBuilder& xorExpr(TNode 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); } + NodeBuilder& operator&&(TNode right) { return andExpr(right); } + NodeBuilder& operator||(TNode right) { return orExpr(right); } */ /* - NodeBuilder& operator&&=(const Node& right) { return andExpr(right); } - NodeBuilder& operator||=(const Node& right) { return orExpr(right); } + NodeBuilder& operator&&=(TNode right) { return andExpr(right); } + NodeBuilder& operator||=(TNode right) { return orExpr(right); } */ // "Stream" expression constructor syntax NodeBuilder& operator<<(const Kind& k) { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Assert(d_nv->getKind() == UNDEFINED_KIND); + Assert(d_nv->getKind() == kind::UNDEFINED_KIND); d_nv->d_kind = k; return *this; } - NodeBuilder& operator<<(const Node& n) { + NodeBuilder& operator<<(TNode n) { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); return append(n); } @@ -191,7 +194,7 @@ public: return append(children.begin(), children.end()); } - NodeBuilder& append(const Node& n) { + NodeBuilder& append(TNode n) { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); Debug("prop") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl; allocateEvIfNecessaryForAppend(); @@ -466,7 +469,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) : d_nv(&d_inlineNv), d_inlineNv(0), d_childrenStorage() { - d_inlineNv.d_kind = UNDEFINED_KIND; + d_inlineNv.d_kind = NodeValue::kindToDKind(kind::UNDEFINED_KIND); } template <unsigned nchild_thresh> @@ -573,16 +576,16 @@ inline void NodeBuilder<nchild_thresh>::dealloc() { template <unsigned nchild_thresh> NodeBuilder<nchild_thresh>::operator Node() {// not const Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Assert(d_nv->getKind() != UNDEFINED_KIND, + Assert(d_nv->getKind() != kind::UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); - if(d_nv->d_kind == VARIABLE) { + if(d_nv->d_kind == kind::VARIABLE) { Assert(d_nv->d_nchildren == 0); NodeValue *nv = (NodeValue*) std::malloc(sizeof(NodeValue) + ( sizeof(NodeValue*) * d_inlineNv.d_nchildren )); nv->d_nchildren = 0; - nv->d_kind = VARIABLE; + nv->d_kind = kind::VARIABLE; nv->d_id = NodeValue::next_id++;// FIXME multithreading nv->d_rc = 0; d_used = true; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 556b577e5..b11361827 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -13,11 +13,7 @@ ** Expression manager implementation. **/ -#include "node_builder.h" #include "node_manager.h" -#include "expr/node.h" -#include "expr/attribute.h" -#include "util/output.h" using namespace std; using namespace CVC4::expr; @@ -28,64 +24,11 @@ __thread NodeManager* NodeManager::s_current = 0; NodeValue* NodeManager::poolLookup(NodeValue* nv) const { NodeValueSet::const_iterator find = d_nodeValueSet.find(nv); - if (find == d_nodeValueSet.end()) { + if(find == d_nodeValueSet.end()) { return NULL; } else { return *find; } } -void NodeManager::poolInsert(NodeValue* nv) { - Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in" - "the pool!"); - d_nodeValueSet.insert(nv); -} - -// general expression-builders - -Node NodeManager::mkNode(Kind kind) { - return NodeBuilder<>(this, kind); -} - -Node NodeManager::mkNode(Kind kind, const Node& child1) { - return NodeBuilder<>(this, kind) << child1; -} - -Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) { - return NodeBuilder<>(this, kind) << child1 << child2; -} - -Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) { - return NodeBuilder<>(this, kind) << child1 << child2 << child3; -} - -Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) { - return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4; -} - -Node NodeManager::mkNode(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::mkNode(Kind kind, const vector<Node>& children) { - return NodeBuilder<>(this, kind).append(children); -} - -Node NodeManager::mkVar(const Type* type, const std::string& name) { - Node n = mkVar(type); - n.setAttribute(VarNameAttr(), name); - return n; -} - -Node NodeManager::mkVar(const Type* type) { - Node n = NodeBuilder<>(this, VARIABLE); - n.setAttribute(TypeAttr(), type); - return n; -} - -Node NodeManager::mkVar() { - return NodeBuilder<>(this, VARIABLE); -} - }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1c46743e9..bcb5f6d47 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -40,6 +40,19 @@ namespace CVC4 { class Type; +namespace expr { +namespace attr { + +struct VarName {}; +struct Type {}; + +}/* CVC4::expr::attr namespace */ + +typedef Attribute<attr::VarName, std::string> VarNameAttr; +typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr; + +}/* CVC4::expr namespace */ + class NodeManager { static __thread NodeManager* s_current; @@ -48,7 +61,7 @@ class NodeManager { typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet; NodeValueSet d_nodeValueSet; - expr::AttributeManager d_attrManager; + expr::attr::AttributeManager d_attrManager; NodeValue* poolLookup(NodeValue* nv) const; void poolInsert(NodeValue* nv); @@ -57,7 +70,7 @@ class NodeManager { public: - NodeManager() : d_attrManager(this) { + NodeManager() { poolInsert( &NodeValue::s_null ); } @@ -65,11 +78,11 @@ public: // general expression-builders Node mkNode(Kind kind); - Node mkNode(Kind kind, const Node& child1); - Node mkNode(Kind kind, const Node& child1, const Node& child2); - Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3); - Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4); - Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5); + Node mkNode(Kind kind, TNode child1); + Node mkNode(Kind kind, TNode child1, TNode child2); + Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3); + Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4); + Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5); // N-ary version Node mkNode(Kind kind, const std::vector<Node>& children); @@ -79,20 +92,29 @@ public: Node mkVar(); template <class AttrKind> - inline typename AttrKind::value_type getAttribute(const Node& n, + inline typename AttrKind::value_type getAttribute(TNode n, const AttrKind&) const; + // Note that there are two, distinct hasAttribute() declarations for + // a reason (rather than using a pointer-valued argument with a + // default value): they permit more optimized code in the underlying + // hasAttribute() implementations. + + template <class AttrKind> + inline bool hasAttribute(TNode n, + const AttrKind&) const; + template <class AttrKind> - inline bool hasAttribute(const Node& n, + inline bool hasAttribute(TNode n, const AttrKind&, - typename AttrKind::value_type* = NULL) const; + typename AttrKind::value_type&) const; template <class AttrKind> - inline void setAttribute(const Node& n, + inline void setAttribute(TNode n, const AttrKind&, const typename AttrKind::value_type& value); - inline const Type* getType(const Node& n); + inline const Type* getType(TNode n); }; class NodeManagerScope { @@ -112,29 +134,94 @@ public: }; template <class AttrKind> -inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n, +inline typename AttrKind::value_type NodeManager::getAttribute(TNode n, const AttrKind&) const { return d_attrManager.getAttribute(n, AttrKind()); } template <class AttrKind> -inline bool NodeManager::hasAttribute(const Node& n, +inline bool NodeManager::hasAttribute(TNode n, + const AttrKind&) const { + return d_attrManager.hasAttribute(n, AttrKind()); +} + +template <class AttrKind> +inline bool NodeManager::hasAttribute(TNode n, const AttrKind&, - typename AttrKind::value_type* ret) const { + typename AttrKind::value_type& ret) const { return d_attrManager.hasAttribute(n, AttrKind(), ret); } template <class AttrKind> -inline void NodeManager::setAttribute(const Node& n, +inline void NodeManager::setAttribute(TNode n, const AttrKind&, const typename AttrKind::value_type& value) { d_attrManager.setAttribute(n, AttrKind(), value); } -inline const Type* NodeManager::getType(const Node& n) { +inline const Type* NodeManager::getType(TNode n) { return getAttribute(n,CVC4::expr::TypeAttr()); } +inline void NodeManager::poolInsert(NodeValue* nv) { + Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in" + "the pool!"); + d_nodeValueSet.insert(nv); +} + +}/* CVC4 namespace */ + +#include "expr/node_builder.h" + +namespace CVC4 { + +// general expression-builders + +inline Node NodeManager::mkNode(Kind kind) { + return NodeBuilder<>(this, kind); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1) { + return NodeBuilder<>(this, kind) << child1; +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { + return NodeBuilder<>(this, kind) << child1 << child2; +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { + return NodeBuilder<>(this, kind) << child1 << child2 << child3; +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) { + return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4; +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { + return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5; +} + +// N-ary version +inline Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) { + return NodeBuilder<>(this, kind).append(children); +} + +inline Node NodeManager::mkVar(const Type* type, const std::string& name) { + Node n = mkVar(type); + n.setAttribute(expr::VarNameAttr(), name); + return n; +} + +inline Node NodeManager::mkVar(const Type* type) { + Node n = NodeBuilder<>(this, kind::VARIABLE); + n.setAttribute(expr::TypeAttr(), type); + return n; +} + +inline Node NodeManager::mkVar() { + return NodeBuilder<>(this, kind::VARIABLE); +} + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 863ddf649..63fe0c84a 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -29,59 +29,6 @@ size_t NodeValue::next_id = 1; NodeValue NodeValue::s_null; -NodeValue::NodeValue() : - d_id(0), - d_rc(MAX_RC), - d_kind(NULL_EXPR), - d_nchildren(0) { -} - -NodeValue::NodeValue(int) : - d_id(0), - d_rc(0), - d_kind(kindToDKind(UNDEFINED_KIND)), - d_nchildren(0) { -} - -NodeValue::~NodeValue() { - for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { - (*i)->dec(); - } -} - -void NodeValue::inc() { - // FIXME multithreading - if(EXPECT_TRUE( d_rc < MAX_RC )) { - ++d_rc; - } -} - -void NodeValue::dec() { - // FIXME multithreading - if(EXPECT_TRUE( d_rc < MAX_RC )) { - --d_rc; - if(EXPECT_FALSE( d_rc == 0 )) { - // FIXME gc - } - } -} - -NodeValue::nv_iterator NodeValue::nv_begin() { - return d_children; -} - -NodeValue::nv_iterator NodeValue::nv_end() { - return d_children + d_nchildren; -} - -NodeValue::const_nv_iterator NodeValue::nv_begin() const { - return d_children; -} - -NodeValue::const_nv_iterator NodeValue::nv_end() const { - return d_children + d_nchildren; -} - string NodeValue::toString() const { stringstream ss; toStream(ss); @@ -90,10 +37,10 @@ string NodeValue::toString() const { void NodeValue::toStream(std::ostream& out) const { out << "(" << Kind(d_kind); - if(d_kind == VARIABLE) { + if(d_kind == kind::VARIABLE) { Node n(this); string s; - if(n.hasAttribute(VarNameAttr(), &s)) { + if(n.hasAttribute(VarNameAttr(), s)) { out << ":" << s; } else { out << ":" << this; diff --git a/src/expr/node_value.h b/src/expr/node_value.h index f0220d37a..85b8a6d60 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -191,10 +191,63 @@ public: return ((unsigned) k) & kindMask; } static inline Kind dKindToKind(unsigned d) { - return (d == kindMask) ? UNDEFINED_KIND : Kind(d); + return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } }; +inline NodeValue::NodeValue() : + d_id(0), + d_rc(MAX_RC), + d_kind(kind::NULL_EXPR), + d_nchildren(0) { +} + +inline NodeValue::NodeValue(int) : + d_id(0), + d_rc(0), + d_kind(kindToDKind(kind::UNDEFINED_KIND)), + d_nchildren(0) { +} + +inline NodeValue::~NodeValue() { + for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { + (*i)->dec(); + } +} + +inline void NodeValue::inc() { + // FIXME multithreading + if(EXPECT_TRUE( d_rc < MAX_RC )) { + ++d_rc; + } +} + +inline void NodeValue::dec() { + // FIXME multithreading + if(EXPECT_TRUE( d_rc < MAX_RC )) { + --d_rc; + if(EXPECT_FALSE( d_rc == 0 )) { + // FIXME gc + } + } +} + +inline NodeValue::nv_iterator NodeValue::nv_begin() { + return d_children; +} + +inline NodeValue::nv_iterator NodeValue::nv_end() { + return d_children + d_nchildren; +} + +inline NodeValue::const_nv_iterator NodeValue::nv_begin() const { + return d_children; +} + +inline NodeValue::const_nv_iterator NodeValue::nv_end() const { + return d_children + d_nchildren; +} + }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/soft_node.h b/src/expr/soft_node.h deleted file mode 100644 index 0bf9b47cf..000000000 --- a/src/expr/soft_node.h +++ /dev/null @@ -1,36 +0,0 @@ -/********************* */ -/** soft_node.h - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** 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. - ** - ** Encapsulation of a pointer to node information that is explicitly - ** NOT reference-counted. These "smart pointers" do NOT keep live - ** the NodeValue object to which they refer. - **/ - -#ifndef __CVC4__SOFT_NODE_H -#define __CVC4__SOFT_NODE_H - -#include "expr/node.h" - -namespace CVC4 { -namespace expr { - -/** - * For now, treat SoftNodes as regular Nodes. We'll address this - * later. - */ -typedef CVC4::Node SoftNode; -typedef CVC4::Node TNode; - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__SOFT_NODE_H */ |