diff options
55 files changed, 1464 insertions, 625 deletions
diff --git a/contrib/addsourcedir b/contrib/addsourcedir index ee507f0c6..8c7d74d90 100644 --- a/contrib/addsourcedir +++ b/contrib/addsourcedir @@ -2,6 +2,7 @@ # # addsourcedir # Morgan Deters <mdeters@cs.nyu.edu> for the CVC4 project +# Copyright (c) 2010 The CVC4 Project # # usage: addsourcedir paths... # diff --git a/contrib/configure-in-place b/contrib/configure-in-place new file mode 100755 index 000000000..09771676e --- /dev/null +++ b/contrib/configure-in-place @@ -0,0 +1,26 @@ +#!/bin/sh +# +# configure-in-place +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project +# +# usage: configure-in-place [ arguments... ] +# +# This script configures CVC4 in the source directory (from where it +# should be invoked). +# + +if [ -e .svn ]; then + echo + echo "DO NOT USE THIS IN SUBVERSION WORKING DIRECTORIES!" + echo + echo "You might accidentally commit Makefiles in the source directories" + echo "improperly, since they exist in the source directory for" + echo "another purpose." + echo + exit 1 +fi + +./configure "$@" +. builds/current +builds/$(CURRENT_BUILD)/config.status diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl index 305db1d8e..6c1e0eeea 100755 --- a/contrib/dimacs_to_smt.pl +++ b/contrib/dimacs_to_smt.pl @@ -1,6 +1,7 @@ #!/usr/bin/perl -w # DIMACS to SMT -# Morgan Deters 2009 +# Morgan Deters +# Copyright (c) 2009, 2010 The CVC4 Project use strict; diff --git a/contrib/get-authors b/contrib/get-authors index 40aaf6a6d..dbe878d6b 100755 --- a/contrib/get-authors +++ b/contrib/get-authors @@ -2,6 +2,7 @@ # # get-authors # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2009, 2010 The CVC4 Project # # usage: get-authors [ files... ] # diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 22128ea6d..79e5986de 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -2,6 +2,7 @@ # # update-copyright.pl # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2009, 2010 The CVC4 Project # # usage: update-copyright [ files/directories... ] # diff --git a/src/Makefile.am b/src/Makefile.am index 11173b7e4..e021cca8d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -17,7 +17,7 @@ AM_CPPFLAGS = -I@srcdir@/include -I@srcdir@ AM_CXXFLAGS = -Wall -fvisibility=hidden -SUBDIRS = expr util context prop smt theory . parser main +SUBDIRS = expr util context theory prop smt . parser main lib_LTLIBRARIES = libcvc4.la 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 */ diff --git a/src/main/main.cpp b/src/main/main.cpp index a12c69df7..745fa30e9 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -39,94 +39,19 @@ using namespace CVC4::main; static Result lastResult; static struct Options options; +int runCvc4(int argc, char *argv[]); void doCommand(SmtEngine&, Command*); +/** + * CVC4's main() routine is just an exception-safe wrapper around CVC4. + * Please don't construct anything here. Even if the constructor is + * inside the try { }, an exception during destruction can cause + * problems. That's why main() wraps runCvc4() in the first place. + * Put everything in runCvc4(). + */ int main(int argc, char *argv[]) { - try { - - // Initialize the signal handlers - cvc4_init(); - - // Parse the options - int firstArgIndex = parseOptions(argc, argv, &options); - - // If in competition mode, set output stream option to flush immediately - if(options.smtcomp_mode) { - cout << unitbuf; - } - - // We only accept one input file - if(argc > firstArgIndex + 1) { - throw Exception("Too many input files specified."); - } - - // Create the expression manager - ExprManager exprMgr; - - // Create the SmtEngine - SmtEngine smt(&exprMgr, &options); - - // If no file supplied we read from standard input - bool inputFromStdin = firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); - - // Auto-detect input language by filename extension - if(!inputFromStdin && options.lang == Parser::LANG_AUTO) { - const char* filename = argv[firstArgIndex]; - unsigned len = strlen(filename); - if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - options.lang = Parser::LANG_SMTLIB; - } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) - || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - options.lang = Parser::LANG_CVC4; - } - } - - // Determine which messages to show based on smtcomp_mode and verbosity - if(options.smtcomp_mode) { - Debug.setStream(CVC4::null_os); - Trace.setStream(CVC4::null_os); - Notice.setStream(CVC4::null_os); - Chat.setStream(CVC4::null_os); - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } else { - if(options.verbosity < 2) { - Chat.setStream(CVC4::null_os); - } - if(options.verbosity < 1) { - Notice.setStream(CVC4::null_os); - } - if(options.verbosity < 0) { - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } - } - - // Create the parser - Parser* parser; - if(inputFromStdin) { - parser = Parser::getNewParser(&exprMgr, options.lang, cin); - } else { - parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]); - } - - if(!options.semanticChecks) { - parser->disableChecks(); - } - - // Parse and execute commands until we are done - Command* cmd; - while((cmd = parser->parseNextCommand())) { - if( !options.parseOnly ) { - doCommand(smt, cmd); - } - delete cmd; - } - - // Remove the parser - delete parser; - + return runCvc4(argc, argv); } catch(OptionException& e) { if(options.smtcomp_mode) { cout << "unknown" << endl; @@ -153,6 +78,91 @@ int main(int argc, char *argv[]) { cerr << "CVC4 threw an exception of unknown type." << endl; abort(); } +} + +int runCvc4(int argc, char *argv[]) { + + // Initialize the signal handlers + cvc4_init(); + + // Parse the options + int firstArgIndex = parseOptions(argc, argv, &options); + + // If in competition mode, set output stream option to flush immediately + if(options.smtcomp_mode) { + cout << unitbuf; + } + + // We only accept one input file + if(argc > firstArgIndex + 1) { + throw Exception("Too many input files specified."); + } + + // Create the expression manager + ExprManager exprMgr; + + // Create the SmtEngine + SmtEngine smt(&exprMgr, &options); + + // If no file supplied we read from standard input + bool inputFromStdin = firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + + // Auto-detect input language by filename extension + if(!inputFromStdin && options.lang == Parser::LANG_AUTO) { + const char* filename = argv[firstArgIndex]; + unsigned len = strlen(filename); + if(len >= 4 && !strcmp(".smt", filename + len - 4)) { + options.lang = Parser::LANG_SMTLIB; + } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) + || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { + options.lang = Parser::LANG_CVC4; + } + } + + // Determine which messages to show based on smtcomp_mode and verbosity + if(options.smtcomp_mode) { + Debug.setStream(CVC4::null_os); + Trace.setStream(CVC4::null_os); + Notice.setStream(CVC4::null_os); + Chat.setStream(CVC4::null_os); + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } else { + if(options.verbosity < 2) { + Chat.setStream(CVC4::null_os); + } + if(options.verbosity < 1) { + Notice.setStream(CVC4::null_os); + } + if(options.verbosity < 0) { + Message.setStream(CVC4::null_os); + Warning.setStream(CVC4::null_os); + } + } + + // Create the parser + Parser* parser; + if(inputFromStdin) { + parser = Parser::getNewParser(&exprMgr, options.lang, cin); + } else { + parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]); + } + + if(!options.semanticChecks) { + parser->disableChecks(); + } + + // Parse and execute commands until we are done + Command* cmd; + while((cmd = parser->parseNextCommand())) { + if( !options.parseOnly ) { + doCommand(smt, cmd); + } + delete cmd; + } + + // Remove the parser + delete parser; switch(lastResult.asSatisfiabilityResult().isSAT()) { diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 066cb3aed..6eb269bca 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -32,6 +32,7 @@ using namespace std; using namespace CVC4; using namespace CVC4::parser; +using namespace CVC4::kind; namespace CVC4 { namespace parser { diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index bfdc4c0f2..9492b36d9 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -216,7 +216,7 @@ iffFormula returns [CVC4::Expr f] } : f = impliesFormula ( IFF e = iffFormula - { f = mkExpr(CVC4::IFF, f, e); } + { f = mkExpr(CVC4::kind::IFF, f, e); } )? ; @@ -230,7 +230,7 @@ impliesFormula returns [CVC4::Expr f] } : f = orFormula ( IMPLIES e = impliesFormula - { f = mkExpr(CVC4::IMPLIES, f, e); } + { f = mkExpr(CVC4::kind::IMPLIES, f, e); } )? ; @@ -246,7 +246,7 @@ orFormula returns [CVC4::Expr f] : e = xorFormula { exprs.push_back(e); } ( OR e = xorFormula { exprs.push_back(e); } )* { - f = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); + f = (exprs.size() > 1 ? mkExpr(CVC4::kind::OR, exprs) : exprs[0]); } ; @@ -260,7 +260,7 @@ xorFormula returns [CVC4::Expr f] } : f = andFormula ( XOR e = andFormula - { f = mkExpr(CVC4::XOR,f, e); } + { f = mkExpr(CVC4::kind::XOR,f, e); } )* ; @@ -276,7 +276,7 @@ andFormula returns [CVC4::Expr f] : e = notFormula { exprs.push_back(e); } ( AND e = notFormula { exprs.push_back(e); } )* { - f = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); + f = (exprs.size() > 1 ? mkExpr(CVC4::kind::AND, exprs) : exprs[0]); } ; @@ -290,7 +290,7 @@ notFormula returns [CVC4::Expr f] } : /* negation */ NOT f = notFormula - { f = mkExpr(CVC4::NOT, f); } + { f = mkExpr(CVC4::kind::NOT, f); } | /* a boolean atom */ f = predFormula ; @@ -302,7 +302,7 @@ predFormula returns [CVC4::Expr f] : { Expr e; } f = term (EQUAL e = term - { f = mkExpr(CVC4::EQUAL, f, e); } + { f = mkExpr(CVC4::kind::EQUAL, f, e); } )? ; // TODO: lt, gt, etc. @@ -323,7 +323,7 @@ term returns [CVC4::Expr t] LPAREN formulaList[args] RPAREN // TODO: check arity - { t = mkExpr(CVC4::APPLY, args); } + { t = mkExpr(CVC4::kind::APPLY, args); } | /* if-then-else */ t = iteTerm @@ -352,7 +352,7 @@ iteTerm returns [CVC4::Expr t] THEN iteThen = formula iteElse = iteElseTerm ENDIF - { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } ; /** @@ -367,7 +367,7 @@ iteElseTerm returns [CVC4::Expr t] | ELSEIF iteCondition = formula THEN iteThen = formula iteElse = iteElseTerm - { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } ; /** diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 84796f093..85b6c9865 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -124,6 +124,9 @@ Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, string filename) { istream* input = new ifstream(filename.c_str()); + if(!*input) { + throw Exception("file does not exist or is unreadable: " + filename); + } return getNewParser(em, lang, input, filename, true); } diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 39cadd47f..be6f6cf83 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -117,7 +117,7 @@ benchAttribute returns [Command* smt_command = 0] annotatedFormula returns [CVC4::Expr formula] { Debug("parser") << "annotated formula: " << LT(1)->getText() << endl; - Kind kind = UNDEFINED_KIND; + Kind kind = CVC4::kind::UNDEFINED_KIND; vector<Expr> args; } : /* a built-in operator application */ @@ -136,7 +136,7 @@ annotatedFormula returns [CVC4::Expr formula] { args.push_back(f); } annotatedFormulas[args] RPAREN // TODO: check arity - { formula = mkExpr(CVC4::APPLY,args); } + { formula = mkExpr(CVC4::kind::APPLY,args); } | /* An ite expression */ LPAREN (ITE | IF_THEN_ELSE) @@ -145,7 +145,7 @@ annotatedFormula returns [CVC4::Expr formula] trueExpr = annotatedFormula falseExpr = annotatedFormula RPAREN - { formula = mkExpr(CVC4::ITE, test, trueExpr, falseExpr); } + { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); } | /* a variable */ { std::string name; } @@ -178,13 +178,13 @@ builtinOp returns [CVC4::Kind kind] { Debug("parser") << "builtin: " << LT(1)->getText() << endl; } - : NOT { kind = CVC4::NOT; } - | IMPLIES { kind = CVC4::IMPLIES; } - | AND { kind = CVC4::AND; } - | OR { kind = CVC4::OR; } - | XOR { kind = CVC4::XOR; } - | IFF { kind = CVC4::IFF; } - | EQUAL { kind = CVC4::EQUAL; } + : NOT { kind = CVC4::kind::NOT; } + | IMPLIES { kind = CVC4::kind::IMPLIES; } + | AND { kind = CVC4::kind::AND; } + | OR { kind = CVC4::kind::OR; } + | XOR { kind = CVC4::kind::XOR; } + | IFF { kind = CVC4::kind::IFF; } + | EQUAL { kind = CVC4::kind::EQUAL; } /* TODO: lt, gt, plus, minus, etc. */ ; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index a66e36a07..6e3b6ae2f 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -23,6 +23,7 @@ #include <queue> using namespace std; +using namespace CVC4::kind; namespace CVC4 { namespace prop { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5dd57610d..76be5d6d8 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -49,14 +49,14 @@ PropEngine::~PropEngine() { delete d_satSolver; } -void PropEngine::assertFormula(const Node& node) { +void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable d_cnfStream->convertAndAssert(node); } -void PropEngine::assertLemma(const Node& node) { +void PropEngine::assertLemma(TNode node) { Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as removable d_cnfStream->convertAndAssert(node); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d4007e73a..4ea5e3b78 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -77,14 +77,14 @@ public: * The formula is asserted permanently for the current context. * @param node the formula to assert */ - void assertFormula(const Node& node); + void assertFormula(TNode node); /** * Converts the given formula to CNF and assert the CNF to the sat solver. * The formula can be removed by the sat solver. * @param node the formula to assert */ - void assertLemma(const Node& node); + void assertLemma(TNode node); /** * Checks the current context for satisfiability. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ea1fe0306..ae676e48d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -21,16 +21,18 @@ #include "prop/prop_engine.h" using namespace CVC4::prop; +using CVC4::context::Context; namespace CVC4 { SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : + d_ctxt(new Context), d_exprManager(em), d_nodeManager(em->getNodeManager()), - d_options(opts) -{ - d_decisionEngine = new DecisionEngine(); - d_theoryEngine = new TheoryEngine(this); + d_options(opts) { + NodeManagerScope nms(d_nodeManager); + d_decisionEngine = new DecisionEngine; + d_theoryEngine = new TheoryEngine(this, d_ctxt); d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine); } @@ -38,6 +40,7 @@ SmtEngine::~SmtEngine() { delete d_propEngine; delete d_theoryEngine; delete d_decisionEngine; + delete d_ctxt; } void SmtEngine::doCommand(Command* c) { @@ -45,7 +48,7 @@ void SmtEngine::doCommand(Command* c) { c->invoke(this); } -Node SmtEngine::preprocess(const Node& e) { +Node SmtEngine::preprocess(TNode e) { return e; } @@ -59,7 +62,7 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN); } -void SmtEngine::addFormula(const Node& e) { +void SmtEngine::addFormula(TNode e) { Debug("smt") << "push_back assertion " << e << std::endl; d_propEngine->assertFormula(preprocess(e)); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 838f9cd7a..afb62fe6a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -112,6 +112,9 @@ public: private: + /** Our Context */ + CVC4::context::Context* d_ctxt; + /** Our expression manager */ ExprManager* d_exprManager; @@ -136,12 +139,12 @@ private: * passes over the Node. TODO: may need to specify a LEVEL of * preprocessing (certain contexts need more/less ?). */ - Node preprocess(const Node& node); + Node preprocess(TNode node); /** * Adds a formula to the current context. */ - void addFormula(const Node& node); + void addFormula(TNode node); /** * Full check of consistency in current context. Returns true iff diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index f6f4ae07e..951dbeb78 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -6,14 +6,34 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LTLIBRARIES = libtheory.la libtheory_la_SOURCES = \ + @srcdir@/theoryof_table.h \ theory_engine.h \ theory_engine.cpp \ theory.h \ theory.cpp libtheory_la_LIBADD = \ - @builddir@/bool/libbool.la - @builddir@/uf/libuf.la - @builddir@/uf/libarith.la + @builddir@/booleans/libbooleans.la \ + @builddir@/uf/libuf.la \ + @builddir@/arith/libarith.la -SUBDIRS = bool uf arith +EXTRA_DIST = \ + @srcdir@/theoryof_table.h \ + theoryof_table_prologue.h \ + theoryof_table_middle.h \ + theoryof_table_epilogue.h + +@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_prologue.h theoryof_table_middle.h theoryof_table_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds + chmod +x @srcdir@/mktheoryof + (@srcdir@/mktheoryof \ + @srcdir@/theoryof_table_prologue.h \ + @srcdir@/theoryof_table_middle.h \ + @srcdir@/theoryof_table_epilogue.h \ + `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + > @srcdir@/theoryof_table.h) || (rm -f @srcdir@/theoryof_table.h && exit 1) + +BUILT_SOURCES = @srcdir@/theoryof_table.h +dist-hook: @srcdir@/theoryof_table.h +MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h + +SUBDIRS = booleans uf arith diff --git a/src/theory/arith/Makefile b/src/theory/arith/Makefile new file mode 100644 index 000000000..5016522e8 --- /dev/null +++ b/src/theory/arith/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/arith + +include $(topdir)/Makefile.subdir diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 461659765..226d5af12 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -5,6 +5,8 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LTLIBRARIES = libarith.la -libarith_la_SOURCES = +libarith_la_SOURCES = \ + theory_def.h \ + theory_arith.h EXTRA_DIST = kinds diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h new file mode 100644 index 000000000..5b596afd4 --- /dev/null +++ b/src/theory/arith/theory_arith.h @@ -0,0 +1,23 @@ +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class TheoryArith : public TheoryImpl<TheoryArith> { +public: + TheoryArith(context::Context* c, OutputChannel& out) : + TheoryImpl<TheoryArith>(c, out) { + } + + void preRegisterTerm(TNode n) { Unimplemented(); } + void registerTerm(TNode n) { Unimplemented(); } + void check(Effort e) { Unimplemented(); } + void propagate(Effort e) { Unimplemented(); } + void explain(TNode n, Effort e) { Unimplemented(); } +}; + +} +} +} + diff --git a/src/theory/arith/theory_def.h b/src/theory/arith/theory_def.h new file mode 100644 index 000000000..9b01a458e --- /dev/null +++ b/src/theory/arith/theory_def.h @@ -0,0 +1,9 @@ +#include "theory/arith/theory_arith.h" + +namespace CVC4 { + namespace theory { + namespace arith { + typedef TheoryArith TheoryARITH; + } + } +} diff --git a/src/theory/booleans/Makefile b/src/theory/booleans/Makefile new file mode 100644 index 000000000..a74a72d83 --- /dev/null +++ b/src/theory/booleans/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/bool + +include $(topdir)/Makefile.subdir diff --git a/src/theory/bool/Makefile.am b/src/theory/booleans/Makefile.am index 9c8b8365e..cbdf13add 100644 --- a/src/theory/bool/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -3,8 +3,10 @@ AM_CPPFLAGS = \ -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden -noinst_LTLIBRARIES = libbool.la +noinst_LTLIBRARIES = libbooleans.la -libbool_la_SOURCES = +libbooleans_la_SOURCES = \ + theory_def.h \ + theory_bool.h EXTRA_DIST = kinds diff --git a/src/theory/bool/kinds b/src/theory/booleans/kinds index 7f1267383..7f1267383 100644 --- a/src/theory/bool/kinds +++ b/src/theory/booleans/kinds diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h new file mode 100644 index 000000000..26e5a69fb --- /dev/null +++ b/src/theory/booleans/theory_bool.h @@ -0,0 +1,24 @@ +#include "theory/theory.h" +#include "context/context.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +class TheoryBool : public TheoryImpl<TheoryBool> { +public: + TheoryBool(context::Context* c, OutputChannel& out) : + TheoryImpl<TheoryBool>(c, out) { + } + + void preRegisterTerm(TNode n) { Unimplemented(); } + void registerTerm(TNode n) { Unimplemented(); } + void check(Effort e) { Unimplemented(); } + void propagate(Effort e) { Unimplemented(); } + void explain(TNode n, Effort e) { Unimplemented(); } +}; + +} +} +} + diff --git a/src/theory/booleans/theory_def.h b/src/theory/booleans/theory_def.h new file mode 100644 index 000000000..37aacb353 --- /dev/null +++ b/src/theory/booleans/theory_def.h @@ -0,0 +1,9 @@ +#include "theory/booleans/theory_bool.h" + +namespace CVC4 { + namespace theory { + namespace booleans { + typedef TheoryBool TheoryBOOLEANS; + } + } +} diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof new file mode 100755 index 000000000..38c2153d6 --- /dev/null +++ b/src/theory/mktheoryof @@ -0,0 +1,57 @@ +#!/bin/bash +# +# mktheoryof +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project +# +# The purpose of this script is to create theoryof_table.h from a +# prologue, epilogue, and a list of theory kinds. +# +# Invocation: +# +# mktheoryof prologue-file epilogue-file theory-kind-files... +# +# Output is to standard out. +# + +cat <<EOF +/********************* -*- C++ -*- */ +/** theoryof_table.h + ** + ** Copyright 2010 The AcSys Group, New York University, and as below. + ** + ** This header file automatically generated by: + ** + ** $0 $@ + ** + ** for the CVC4 project. + **/ + +EOF + +prologue=$1; shift +middle=$1; shift +epilogue=$1; shift + +registers= +cat "$prologue" +while [ $# -gt 0 ]; do + b=$(basename $(dirname "$1")) + B=$(echo "$b" | tr 'a-z' 'A-Z') + echo "#include \"theory/$b/theory_def.h\"" + registers="$registers + /* from $b */ + void registerTheory(::CVC4::theory::$b::Theory$B* th) { +" + for r in `cat "$1"`; do + registers="$registers d_table[::CVC4::kind::$r] = th; +" + done + registers="$registers } +" + shift +done +echo +cat "$middle" +echo "$registers" +cat "$epilogue" diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index c530434f5..ad558e115 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -25,9 +25,21 @@ namespace theory { * Generic "theory output channel" interface. */ class OutputChannel { + /** Disallow copying: private constructor */ + OutputChannel(const OutputChannel&); + + /** Disallow assignment: private operator=() */ + OutputChannel& operator=(const OutputChannel&); + public: /** + * Construct an OutputChannel. + */ + OutputChannel() { + } + + /** * Destructs an OutputChannel. This implementation does nothing, * but we need a virtual destructor for safety in case subclasses * have a destructor. @@ -39,24 +51,28 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint() throw(Interrupted&) { + virtual void safePoint() throw(Interrupted) { } /** * Indicate a theory conflict has arisen. * - * @param n - a conflict at the current decision level + * @param n - a conflict at the current decision level. This should + * be an OR-kinded node of literals that are false in the current + * assignment. + * * @param safe - whether it is safe to be interrupted */ - virtual void conflict(Node n, bool safe = false) throw(Interrupted&) = 0; + virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0; /** * Propagate a theory literal. * - * @param n - a theory consequence at the current decision level + * @param n - a theory consequence at the current decision level. + * * @param safe - whether it is safe to be interrupted */ - virtual void propagate(Node n, bool safe = false) throw(Interrupted&) = 0; + virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -65,31 +81,7 @@ public: * @param n - a theory lemma valid at decision level 0 * @param safe - whether it is safe to be interrupted */ - virtual void lemma(Node n, bool safe = false) throw(Interrupted&) = 0; - -};/* class OutputChannel */ - -/** - * Generic "theory output channel" interface for explanations. - */ -class ExplainOutputChannel { -public: - - /** - * Destructs an ExplainOutputChannel. This implementation does - * nothing, but we need a virtual destructor for safety in case - * subclasses have a destructor. - */ - virtual ~ExplainOutputChannel() { - } - - /** - * With safePoint(), the theory signals that it is at a safe point - * and can be interrupted. The default implementation never - * interrupts. - */ - virtual void safePoint() throw(Interrupted&) { - } + virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0; /** * Provide an explanation in response to an explanation request. @@ -97,8 +89,9 @@ public: * @param n - an explanation * @param safe - whether it is safe to be interrupted */ - virtual void explanation(Node n, bool safe = false) throw(Interrupted&) = 0; -};/* class ExplainOutputChannel */ + virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0; + +};/* class OutputChannel */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index cf52de75e..17a35f2ed 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -14,24 +14,14 @@ **/ #include "theory/theory.h" +#include "util/Assert.h" -namespace CVC4 { -namespace theory { - -bool Theory::done() { - return d_nextAssertion >= d_assertions.size(); -} +#include <vector> +using namespace std; -Node Theory::get() { - Node n = d_assertions[d_nextAssertion]; - d_nextAssertion = d_nextAssertion + 1; - return n; -} - -void Theory::assertFact(const Node& n){ - d_assertions.push_back(n); -} +namespace CVC4 { +namespace theory { }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 76b9697dc..e079d67bd 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -17,25 +17,91 @@ #define __CVC4__THEORY__THEORY_H #include "expr/node.h" +#include "expr/attribute.h" #include "theory/output_channel.h" #include "context/context.h" +#include <queue> +#include <vector> + +#include <typeinfo> + namespace CVC4 { namespace theory { +template <class T> +class TheoryImpl; + /** * Base class for T-solvers. Abstract DPLL(T). + * + * This is essentially an interface class. The TheoryEngine has + * pointers to Theory. But each individual theory implementation T + * should inherit from TheoryImpl<T>, which specializes a few things + * for that theory. */ class Theory { +private: + + template <class T> + friend class TheoryImpl; + + /** + * Construct a Theory. + */ + Theory(context::Context* ctxt, OutputChannel& out) throw() : + d_context(ctxt), + d_out(&out) { + } + + /** + * Disallow default construction. + */ + Theory(); + +protected: + + /** + * The output channel for the Theory. + */ + context::Context* d_context; + + /** + * The output channel for the Theory. + */ + OutputChannel* d_out; + + /** + * The assertFact() queue. + */ + // FIXME CD: on backjump we clear the facts IFF the queue gets + // emptied on every DL. In general I guess we need a CDQueue<>? + // Perhaps one that asserts it's empty at each push? + std::queue<Node> d_facts; /** * Return whether a node is shared or not. Used by setup(). */ - bool isShared(const Node& n); + bool isShared(TNode n) throw(); + + /** + * Returns true if the assertFact queue is empty + */ + bool done() throw() { + return d_facts.empty(); + } public: /** + * Destructs a Theory. This implementation does nothing, but we + * need a virtual destructor for safety in case subclasses have a + * destructor. + */ + virtual ~Theory() { + } + + /** * Subclasses of Theory may add additional efforts. DO NOT CHECK * equality with one of these values (e.g. if STANDARD xxx) but * rather use range checks (or use the helper functions below). @@ -58,20 +124,34 @@ public: static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** - * Construct a Theory. + * Set the output channel associated to this theory. */ - Theory(context::Context* c) : d_assertions(c), d_nextAssertion(c, 0){} + void setOutputChannel(OutputChannel& out) { + d_out = &out; + } /** - * Destructs a Theory. This implementation does nothing, but we - * need a virtual destructor for safety in case subclasses have a - * destructor. + * Get the output channel associated to this theory. */ - virtual ~Theory() { + OutputChannel& getOutputChannel() { + return *d_out; + } + + /** + * Get the output channel associated to this theory [const]. + */ + const OutputChannel& getOutputChannel() const { + return *d_out; } /** - * Prepare for a Node. + * Pre-register a term. Done one time for a Node, ever. + * + */ + virtual void preRegisterTerm(TNode) = 0; + + /** + * Register a term. * * When get() is called to get the next thing off the theory queue, * setup() is called on its subterms (in TheoryEngine). Then setup() @@ -81,55 +161,189 @@ public: * setup() MUST NOT MODIFY context-dependent objects that it hasn't * itself just created. */ - - /*virtual void setup(const Node& n) = 0;*/ - - virtual void registerTerm(TNode n) = 0; + virtual void registerTerm(TNode) = 0; /** * Assert a fact in the current context. */ - void assertFact(const Node& n); + void assertFact(TNode n) { + d_facts.push(n); + } /** * Check the current assignment's consistency. */ - virtual void check(OutputChannel& out, - Effort level = FULL_EFFORT) = 0; + virtual void check(Effort level = FULL_EFFORT) = 0; /** * T-propagate new literal assignments in the current context. */ - virtual void propagate(OutputChannel& out, - Effort level = FULL_EFFORT) = 0; + virtual void propagate(Effort level = FULL_EFFORT) = 0; /** * Return an explanation for the literal represented by parameter n * (which was previously propagated by this theory). Report * explanations to an output channel. */ - virtual void explain(OutputChannel& out, - const Node& n, - Effort level = FULL_EFFORT) = 0; -private: - context::CDList<Node> d_assertions; - context::CDO<unsigned> d_nextAssertion; + virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0; + + // + // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS) + // -protected: /** - * Returns the next atom in the assertFact() queue. - * Guarentees that registerTerm is called on the theory specific subterms. - * @return the next atom in the assertFact() queue. + * Different states at which invariants are checked. */ - Node get(); + enum ReadyState { + ABOUT_TO_PUSH, + ABOUT_TO_POP + };/* enum ReadyState */ /** - * Returns true if the assertFactQueue is empty + * Public invariant checker. Assert that this theory is in a valid + * state for the (external) system state. This implementation + * checks base invariants and then calls theoryReady(). This + * function may abort in the case of a failed assert, or return + * false (the caller should assert that the return value is true). + * + * @param s the state about which to check invariants */ - bool done(); + bool ready(ReadyState s) { + if(s == ABOUT_TO_PUSH) { + Assert(d_facts.empty(), "Theory base code invariant broken: " + "fact queue is nonempty on context push"); + } + + return theoryReady(s); + } + +protected: + + /** + * Check any invariants at the ReadyState given. Only called by + * Theory class, and then only with CVC4_ASSERTIONS enabled. This + * function may abort in the case of a failed assert, or return + * false (the caller should assert that the return value is true). + * + * @param s the state about which to check invariants + */ + virtual bool theoryReady(ReadyState s) { + return true; + } };/* class Theory */ + +/** + * Base class for T-solver implementations. Each individual + * implementation T of the Theory interface should inherit from + * TheoryImpl<T>. This class specializes some things for a particular + * theory implementation. + * + * The problem with this is that Theory implementations cannot be + * further subclassed without designing all non-children in the type + * DAG to play the same trick as here (be template-polymorphic in their + * most-derived child), linearizing the inheritance hierarchy (viewing + * each instantiation separately). + */ +template <class T> +class TheoryImpl : public Theory { + +protected: + + /** + * Construct a Theory. + */ + TheoryImpl(context::Context* ctxt, OutputChannel& out) : + Theory(ctxt, out) { + /* FIXME: assert here that a TheoryImpl<T> doesn't already exist + * for this NodeManager?? If it does, we're hosed because they'll + * share per-theory node attributes. */ + } + + /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ + struct Registered {}; + /** The "registerTerm()-has-been-called" flag on Nodes */ + typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; + + /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */ + struct PreRegistered {}; + /** The "preRegisterTerm()-has-been-called" flag on Nodes */ + typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr; + + /** + * Returns the next atom in the assertFact() queue. Guarantees that + * registerTerm() has been called on the theory specific subterms. + * + * @return the next atom in the assertFact() queue. + */ + Node get(); +};/* class TheoryImpl<T> */ + +template <class T> +Node TheoryImpl<T>::get() { + Warning.printf("testing %s == %s\n", typeid(*this).name(), typeid(T).name()); + /*Assert(typeid(*this) == typeid(T), + "Improper Theory inheritance chain detected.");*/ + + Assert( !d_facts.empty(), + "Theory::get() called with assertion queue empty!" ); + + Node fact = d_facts.front(); + d_facts.pop(); + + if(! fact.getAttribute(RegisteredAttr())) { + std::vector<TNode> toReg; + toReg.push_back(fact); + + /* Essentially this is doing a breadth-first numbering of + * non-registered subterms with children. Any non-registered + * leaves are immediately registered. */ + for(std::vector<TNode>::iterator workp = toReg.begin(); + workp != toReg.end(); + ++workp) { + + TNode n = *workp; + + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + TNode c = *i; + + if(! c.getAttribute(RegisteredAttr())) { + if(c.getNumChildren() == 0) { + c.setAttribute(RegisteredAttr(), true); + registerTerm(c); + } else { + toReg.push_back(c); + } + } + } + } + + /* Now register the list of terms in reverse order. Between this + * and the above registration of leaves, this should ensure that + * all subterms in the entire tree were registered in + * reverse-topological order. */ + for(std::vector<TNode>::reverse_iterator i = toReg.rend(); + i != toReg.rbegin(); + ++i) { + + TNode n = *i; + + /* Note that a shared TNode in the DAG rooted at "fact" could + * appear twice on the list, so we have to avoid hitting it + * twice. */ + // FIXME when ExprSets are online, use one of those to avoid + // duplicates in the above? + if(! n.getAttribute(RegisteredAttr())) { + n.setAttribute(RegisteredAttr(), true); + registerTerm(n); + } + } + } + + return fact; +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 348d7e6df..7d630f667 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -18,6 +18,8 @@ #include "expr/node.h" #include "theory/theory.h" +#include "theory/uf/theory_uf.h" +#include "theory/theoryof_table.h" namespace CVC4 { @@ -34,20 +36,67 @@ class SmtEngine; */ class TheoryEngine { + /** Associated SMT engine */ SmtEngine* d_smt; + /** A table of Kinds to pointers to Theory */ + theory::TheoryOfTable theoryOfTable; + + /** + * An output channel for Theory that passes messages + * back to a TheoryEngine. + */ + class EngineOutputChannel : public theory::OutputChannel { + TheoryEngine* d_engine; + public: + void setEngine(TheoryEngine& engine) throw() { + d_engine = &engine; + } + + void conflict(TNode, bool) throw(theory::Interrupted) { + } + + void propagate(TNode, bool) throw(theory::Interrupted) { + } + + void lemma(TNode, bool) throw(theory::Interrupted) { + } + + void explanation(TNode, bool) throw(theory::Interrupted) { + } + }; + + EngineOutputChannel d_theoryOut; + theory::booleans::TheoryBool d_bool; + theory::uf::TheoryUF d_uf; + theory::arith::TheoryArith d_arith; + public: /** * Construct a theory engine. */ - TheoryEngine(SmtEngine* smt) : d_smt(smt) { + TheoryEngine(SmtEngine* smt, context::Context* ctxt) : + d_smt(smt), + d_theoryOut(), + d_bool(ctxt, d_theoryOut), + d_uf(ctxt, d_theoryOut), + d_arith(ctxt, d_theoryOut) { + d_theoryOut.setEngine(*this); + theoryOfTable.registerTheory(&d_bool); + theoryOfTable.registerTheory(&d_uf); + theoryOfTable.registerTheory(&d_arith); } /** * Get the theory associated to a given Node. + * + * @returns the theory, or NULL if the TNode is + * of built-in type. */ - CVC4::theory::Theory* theoryOf(const Node& n); + theory::Theory* theoryOf(TNode n) { + return theoryOfTable[n]; + } };/* class TheoryEngine */ diff --git a/src/theory/theoryof_table_epilogue.h b/src/theory/theoryof_table_epilogue.h new file mode 100644 index 000000000..7483248ec --- /dev/null +++ b/src/theory/theoryof_table_epilogue.h @@ -0,0 +1,21 @@ +/********************* */ +/** theoryof_table_epilogue.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. + ** + ** The theoryOf table. + **/ + +};/* class TheoryOfTable */ + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__THEORYOF_TABLE_H */ diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h new file mode 100644 index 000000000..17a945d01 --- /dev/null +++ b/src/theory/theoryof_table_middle.h @@ -0,0 +1,35 @@ +/********************* */ +/** theoryof_table_middle.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. + ** + ** The theoryOf table. + **/ + +namespace CVC4 { +namespace theory { + +class Theory; + +class TheoryOfTable { + + Theory** d_table; + +public: + + TheoryOfTable() : + d_table(new Theory*[::CVC4::kind::LAST_KIND]) { + } + + Theory* operator[](TNode n) { + Assert(n.getKind() >= 0 && n.getKind() < ::CVC4::kind::LAST_KIND, + "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)"); + return d_table[n.getKind()]; + } diff --git a/src/theory/theoryof_table_prologue.h b/src/theory/theoryof_table_prologue.h new file mode 100644 index 000000000..5f8c28723 --- /dev/null +++ b/src/theory/theoryof_table_prologue.h @@ -0,0 +1,21 @@ +/********************* */ +/** theoryof_table_prologue.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. + ** + ** The theoryOf table. + **/ + +#ifndef __CVC4__THEORY__THEORYOF_TABLE_H +#define __CVC4__THEORY__THEORYOF_TABLE_H + +#include "expr/kind.h" +#include "util/Assert.h" + diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 537b8b124..156733c5b 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LTLIBRARIES = libuf.la libuf_la_SOURCES = \ + theory_def.h \ ecdata.h \ ecdata.cpp \ theory_uf.h \ diff --git a/src/theory/uf/theory_def.h b/src/theory/uf/theory_def.h new file mode 100644 index 000000000..8e3f5e9f1 --- /dev/null +++ b/src/theory/uf/theory_def.h @@ -0,0 +1,7 @@ +namespace CVC4 { + namespace theory { + namespace uf { + class TheoryUF; + } + } +} diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1efe13b9b..47bda5bc4 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -19,9 +19,10 @@ #include "expr/kind.h" using namespace CVC4; -using namespace context; -using namespace theory; -using namespace uf; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; @@ -30,8 +31,8 @@ Node getOperator(Node x) { return Node::null(); } -TheoryUF::TheoryUF(Context* c) : - Theory(c), +TheoryUF::TheoryUF(Context* c, OutputChannel& out) : + TheoryImpl<TheoryUF>(c, out), d_pending(c), d_currentPendingIdx(c,0), d_disequality(c), @@ -40,13 +41,16 @@ TheoryUF::TheoryUF(Context* c) : TheoryUF::~TheoryUF(){} +void TheoryUF::preRegisterTerm(TNode n){ +} + void TheoryUF::registerTerm(TNode n){ d_registered.push_back(n); ECData* ecN; - if(n.hasAttribute(ECAttr(),&ecN)){ + if(n.hasAttribute(ECAttr(), ecN)){ /* registerTerm(n) is only called when a node has not been seen in the * current context. ECAttr() is not a context-dependent attribute. * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call, @@ -222,9 +226,9 @@ void TheoryUF::merge(){ } } -void TheoryUF::check(OutputChannel& out, Effort level){ +void TheoryUF::check(Effort level){ while(!done()){ - Node assertion = get(); + Node assertion;// = get(); switch(assertion.getKind()){ case EQUAL: @@ -252,7 +256,7 @@ void TheoryUF::check(OutputChannel& out, Effort level){ TNode left = (*diseqIter)[0]; TNode right = (*diseqIter)[1]; if(sameCongruenceClass(left, right)){ - out.conflict(*diseqIter, true); + d_out->conflict(*diseqIter, true); } } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index b68a96e65..4bb18bd43 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -21,7 +21,6 @@ #include "expr/attribute.h" #include "theory/theory.h" -#include "theory/output_channel.h" #include "context/context.h" #include "theory/uf/ecdata.h" @@ -30,9 +29,8 @@ namespace CVC4 { namespace theory { namespace uf { +class TheoryUF : public TheoryImpl<TheoryUF> { - -class TheoryUF : public Theory { private: @@ -72,7 +70,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c); + TheoryUF(context::Context* c, OutputChannel& out); /** Destructor for the TheoryUF object. */ ~TheoryUF(); @@ -82,14 +80,13 @@ public: //has pending changes to the contracts void registerTerm(TNode n); + void preRegisterTerm(TNode n); - void check(OutputChannel& out, Effort level= FULL_EFFORT); + void check(Effort level); - void propagate(OutputChannel& out, Effort level= FULL_EFFORT){} + void propagate(Effort level) {} - void explain(OutputChannel& out, - const Node& n, - Effort level = FULL_EFFORT){} + void explain(TNode n, Effort level) {} private: /** diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h index 35c5fde16..a9db0262e 100644 --- a/test/unit/expr/kind_black.h +++ b/test/unit/expr/kind_black.h @@ -22,6 +22,7 @@ #include "expr/kind.h" using namespace CVC4; +using namespace CVC4::kind; using namespace std; class KindBlack : public CxxTest::TestSuite { diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 75ab25f4c..4731810ea 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -24,6 +24,7 @@ #include "expr/node.h" using namespace CVC4; +using namespace CVC4::kind; using namespace std; class NodeBlack : public CxxTest::TestSuite { @@ -40,8 +41,8 @@ public: } void tearDown() { - delete d_nm; delete d_scope; + delete d_nm; } bool imp(bool a, bool b) const { @@ -381,20 +382,6 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - void testPlusNode() { - /*Node plusNode(const Node& right) const;*/ - TS_WARN( "TODO: No implementation to test." ); - } - - void testUMinusNode() { - /*Node uMinusNode() const;*/ - TS_WARN( "TODO: No implementation to test." ); - } - void testMultNode() { - /* Node multNode(const Node& right) const;*/ - TS_WARN( "TODO: No implementation to test." ); - } - void testKindSingleton(Kind k) { Node n = d_nm->mkNode(k); TS_ASSERT(k == n.getKind()); diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 10d761166..5dc327a67 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -26,6 +26,7 @@ #include "expr/kind.h" using namespace CVC4; +using namespace CVC4::kind; using namespace std; class NodeBuilderBlack : public CxxTest::TestSuite { diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 1b57d01df..871abe232 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -24,7 +24,9 @@ #include "expr/attribute.h" using namespace CVC4; +using namespace CVC4::kind; using namespace CVC4::expr; +using namespace CVC4::expr::attr; using namespace std; struct Test1; @@ -36,12 +38,27 @@ struct Test5; typedef Attribute<Test1, std::string> TestStringAttr1; typedef Attribute<Test2, std::string> TestStringAttr2; +// it would be nice to have CDAttribute<> for context-dependence +typedef CDAttribute<Test1, bool> TestCDFlag; + +struct ecdata; +struct cleanupfcn { + static void cleanup(ecdata* ec) { /* clean up */ } +}; + +// ManagedAttribute<> has a cleanup function deleting the value +typedef ManagedAttribute<Test1, ecdata*, cleanupfcn> TestECDataAttr; + typedef Attribute<Test1, bool> TestFlag1; typedef Attribute<Test2, bool> TestFlag2; typedef Attribute<Test3, bool> TestFlag3; typedef Attribute<Test4, bool> TestFlag4; typedef Attribute<Test5, bool> TestFlag5; +struct FooBar {}; +struct Test6; +typedef Attribute<Test6, FooBar> TestFlag6; + class NodeWhite : public CxxTest::TestSuite { NodeManagerScope *d_scope; @@ -55,8 +72,8 @@ public: } void tearDown() { - delete d_nm; delete d_scope; + delete d_nm; } void testNull() { @@ -89,7 +106,6 @@ public: TS_ASSERT(TestFlag3::s_id == 2); TS_ASSERT(TestFlag4::s_id == 3); TS_ASSERT(TestFlag5::s_id == 4); - TS_ASSERT(attr::LastAttributeId<bool>::s_id == 5); } void testAttributes() { @@ -201,68 +217,68 @@ public: // test two-arg version of hasAttribute() bool bb; Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag1(), &bb)); + TS_ASSERT(a.hasAttribute(TestFlag1(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag1(), &bb)); + TS_ASSERT(b.hasAttribute(TestFlag1(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag1(), &bb)); + TS_ASSERT(c.hasAttribute(TestFlag1(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag1(), &bb)); + TS_ASSERT(unnamed.hasAttribute(TestFlag1(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 2 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag2(), &bb)); + TS_ASSERT(a.hasAttribute(TestFlag2(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 2 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag2(), &bb)); + TS_ASSERT(b.hasAttribute(TestFlag2(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 2 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag2(), &bb)); + TS_ASSERT(c.hasAttribute(TestFlag2(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag2(), &bb)); + TS_ASSERT(unnamed.hasAttribute(TestFlag2(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 3 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag3(), &bb)); + TS_ASSERT(a.hasAttribute(TestFlag3(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 3 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag3(), &bb)); + TS_ASSERT(b.hasAttribute(TestFlag3(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 3 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag3(), &bb)); + TS_ASSERT(c.hasAttribute(TestFlag3(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag3(), &bb)); + TS_ASSERT(unnamed.hasAttribute(TestFlag3(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 4 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag4(), &bb)); + TS_ASSERT(a.hasAttribute(TestFlag4(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 4 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag4(), &bb)); + TS_ASSERT(b.hasAttribute(TestFlag4(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 4 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag4(), &bb)); + TS_ASSERT(c.hasAttribute(TestFlag4(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag4(), &bb)); + TS_ASSERT(unnamed.hasAttribute(TestFlag4(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 5 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag5(), &bb)); + TS_ASSERT(a.hasAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 5 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag5(), &bb)); + TS_ASSERT(b.hasAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 5 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag5(), &bb)); + TS_ASSERT(c.hasAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag5(), &bb)); + TS_ASSERT(unnamed.hasAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); // setting boolean flags |