summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/Makefile.am94
-rw-r--r--src/expr/attribute.cpp23
-rw-r--r--src/expr/attribute.h755
-rw-r--r--src/expr/attribute_internals.h695
-rw-r--r--src/expr/builtin_kinds8
-rw-r--r--src/expr/command.h3
-rw-r--r--src/expr/expr_manager_template.cpp (renamed from src/expr/expr_manager.cpp)51
-rw-r--r--src/expr/expr_manager_template.h (renamed from src/expr/expr_manager.h)160
-rw-r--r--src/expr/expr_template.cpp (renamed from src/expr/expr.cpp)83
-rw-r--r--src/expr/expr_template.h (renamed from src/expr/expr.h)99
-rw-r--r--src/expr/kind_template.h7
-rw-r--r--src/expr/metakind_template.h10
-rwxr-xr-xsrc/expr/mkexpr177
-rwxr-xr-xsrc/expr/mkkind17
-rwxr-xr-xsrc/expr/mkmetakind92
-rw-r--r--src/expr/node.h30
-rw-r--r--src/expr/node_manager.h50
-rw-r--r--src/expr/node_value.h3
-rw-r--r--src/expr/type.h5
19 files changed, 1428 insertions, 934 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 7b34fe431..76f6ef1a4 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -9,19 +9,19 @@ libexpr_la_SOURCES = \
node.h \
node.cpp \
node_builder.h \
- expr.h \
+ @srcdir@/expr.h \
type.h \
node_value.h \
node_manager.h \
- expr_manager.h \
+ @srcdir@/expr_manager.h \
attribute.h \
attribute.cpp \
@srcdir@/kind.h \
@srcdir@/metakind.h \
node_manager.cpp \
- expr_manager.cpp \
+ @srcdir@/expr_manager.cpp \
node_value.cpp \
- expr.cpp \
+ @srcdir@/expr.cpp \
type.cpp \
command.h \
command.cpp
@@ -29,25 +29,91 @@ libexpr_la_SOURCES = \
EXTRA_DIST = \
@srcdir@/kind.h \
@srcdir@/metakind.h \
+ @srcdir@/expr_manager.h \
+ @srcdir@/expr.h \
+ @srcdir@/expr_manager.cpp \
+ @srcdir@/expr.cpp \
kind_template.h \
- metakind_template.h
+ metakind_template.h \
+ expr_manager_template.h \
+ expr_manager_template.cpp \
+ expr_template.h \
+ expr_template.cpp
-@srcdir@/kind.h: mkkind kind_template.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+@srcdir@/kind.h: kind_template.h mkkind builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkkind
+ $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkkind \
- @srcdir@/kind_template.h \
+ $< \
@srcdir@/builtin_kinds \
`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
- > @srcdir@/kind.h) || (rm -f @srcdir@/kind.h && exit 1)
+ > $@) || (rm -f $@ && exit 1)
-@srcdir@/metakind.h: mkmetakind metakind_template.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+@srcdir@/metakind.h: metakind_template.h mkmetakind builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkmetakind
+ $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkmetakind \
- @srcdir@/metakind_template.h \
+ $< \
@srcdir@/builtin_kinds \
`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
- > @srcdir@/metakind.h) || (rm -f @srcdir@/metakind.h && exit 1)
+ > $@) || (rm -f $@ && exit 1)
-BUILT_SOURCES = @srcdir@/kind.h @srcdir@/metakind.h
-dist-hook: @srcdir@/kind.h @srcdir@/metakind.h
-MAINTAINERCLEANFILES = @srcdir@/kind.h @srcdir@/metakind.h
+@srcdir@/expr.h: expr_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+ $(AM_V_at)chmod +x @srcdir@/mkexpr
+ $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
+ $(AM_V_GEN)(@srcdir@/mkexpr \
+ $< \
+ @srcdir@/builtin_kinds \
+ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+ > $@) || (rm -f $@ && exit 1)
+
+@srcdir@/expr.cpp: expr_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+ $(AM_V_at)chmod +x @srcdir@/mkexpr
+ $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
+ $(AM_V_GEN)(@srcdir@/mkexpr \
+ $< \
+ @srcdir@/builtin_kinds \
+ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+ > $@) || (rm -f $@ && exit 1)
+
+@srcdir@/expr_manager.h: expr_manager_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+ $(AM_V_at)chmod +x @srcdir@/mkexpr
+ $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
+ $(AM_V_GEN)(@srcdir@/mkexpr \
+ $< \
+ @srcdir@/builtin_kinds \
+ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+ > $@) || (rm -f $@ && exit 1)
+
+@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+ $(AM_V_at)chmod +x @srcdir@/mkexpr
+ $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
+ $(AM_V_GEN)(@srcdir@/mkexpr \
+ $< \
+ @srcdir@/builtin_kinds \
+ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+ > $@) || (rm -f $@ && exit 1)
+
+BUILT_SOURCES = \
+ @srcdir@/kind.h \
+ @srcdir@/metakind.h \
+ @srcdir@/expr.h \
+ @srcdir@/expr.cpp \
+ @srcdir@/expr_manager.h \
+ @srcdir@/expr_manager.cpp
+
+dist-hook: \
+ @srcdir@/kind.h \
+ @srcdir@/metakind.h \
+ @srcdir@/expr.h \
+ @srcdir@/expr.cpp \
+ @srcdir@/expr_manager.h \
+ @srcdir@/expr_manager.cpp
+
+MAINTAINERCLEANFILES = \
+ @srcdir@/kind.h \
+ @srcdir@/metakind.h \
+ @srcdir@/expr.h \
+ @srcdir@/expr.cpp \
+ @srcdir@/expr_manager.h \
+ @srcdir@/expr_manager.cpp
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 26cb96646..5e8918133 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -25,29 +25,6 @@ namespace CVC4 {
namespace expr {
namespace attr {
-/**
- * Search for the NodeValue in all attribute tables and remove it,
- * calling the cleanup function if one is defined.
- */
-template <class T>
-inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
- NodeValue* nv) {
- for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
- typedef AttributeTraits<T, false> traits_t;
- typedef AttrHash<T> hash_t;
- pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv);
- if(traits_t::cleanup[id] != NULL) {
- typename hash_t::iterator i = table.find(pr);
- if(i != table.end()) {
- traits_t::cleanup[id]((*i).second);
- table.erase(pr);
- }
- } else {
- table.erase(pr);
- }
- }
-}
-
void AttributeManager::deleteAllAttributes(NodeValue* nv) {
d_bools.erase(nv);
deleteFromTable(d_ints, nv);
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index efd33d83b..358755192 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -27,678 +27,22 @@
#include <string>
#include <ext/hash_map>
-#include "config.h"
#include "context/cdmap.h"
#include "expr/node.h"
#include "expr/type.h"
-
#include "util/output.h"
+// include supporting templates
+#define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+#include "expr/attribute_internals.h"
+#undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+
namespace CVC4 {
namespace expr {
-
-// ATTRIBUTE HASH FUNCTIONS ====================================================
-
-namespace attr {
-
-/**
- * A hash function for attribute table keys. Attribute table keys are
- * pairs, (unique-attribute-id, Node).
- */
-struct AttrHashStrategy {
- enum { LARGE_PRIME = 32452843ul };
- std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
- return p.first * LARGE_PRIME + p.second->getId();
- }
-};
-
-/**
- * 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 AttrHashBoolStrategy {
- std::size_t operator()(NodeValue* nv) const {
- return (size_t)nv->getId();
- }
-};
-
-}/* 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; }
-};
-
-/**
- * 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);
- }
-};
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE HASH TABLES =======================================================
-
-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, NodeValue*>,
- value_type,
- AttrHashStrategy> {
-};
-
-/**
- * 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<NodeValue*,
- uint64_t,
- AttrHashBoolStrategy> {
-
- /** A "super" type, like in Java, for easy reference below. */
- typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> 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;
-
- unsigned d_bit;
-
- public:
-
- BitAccessor(uint64_t& word, unsigned bit) :
- d_word(word),
- d_bit(bit) {
- }
-
- BitAccessor& operator=(bool b) {
- if(b) {
- // set the bit
- d_word |= (1 << d_bit);
- } else {
- // clear the bit
- d_word &= ~(1 << d_bit);
- }
-
- return *this;
- }
-
- operator bool() const {
- return (d_word & (1 << d_bit)) ? true : false;
- }
- };
-
- /**
- * 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<NodeValue* const, uint64_t>* d_entry;
-
- unsigned d_bit;
-
- public:
-
- BitIterator() :
- d_entry(NULL),
- d_bit(0) {
- }
-
- BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
- d_entry(&entry),
- d_bit(bit) {
- }
-
- std::pair<NodeValue* const, BitAccessor> operator*() {
- return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit));
- }
-
- bool operator==(const BitIterator& b) {
- return d_entry == b.d_entry && d_bit == b.d_bit;
- }
- };
-
- /**
- * 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<NodeValue* const, uint64_t>* d_entry;
-
- unsigned d_bit;
-
- public:
-
- ConstBitIterator() :
- d_entry(NULL),
- d_bit(0) {
- }
-
- ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
- d_entry(&entry),
- d_bit(bit) {
- }
-
- std::pair<NodeValue* const, bool> operator*() {
- return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false);
- }
-
- bool operator==(const ConstBitIterator& b) {
- return d_entry == b.d_entry && d_bit == b.d_bit;
- }
- };
-
-public:
-
- typedef std::pair<uint64_t, NodeValue*> 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;
-
- /**
- * Find the boolean value in the hash table. Returns something ==
- * end() if not found.
- */
- BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
- super::iterator i = super::find(k.second);
- if(i == super::end()) {
- return BitIterator();
- }
- Debug.printf("boolattr",
- "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
- &(*i).second,
- (unsigned long long)((*i).second),
- unsigned(k.first));
- return BitIterator(*i, k.first);
- }
-
- /** The "off the end" iterator */
- BitIterator end() {
- return BitIterator();
- }
-
- /**
- * Find the boolean value in the hash table. Returns something ==
- * end() if not found.
- */
- ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
- super::const_iterator i = super::find(k.second);
- if(i == super::end()) {
- return ConstBitIterator();
- }
- Debug.printf("boolattr",
- "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
- &(*i).second,
- (unsigned long long)((*i).second),
- unsigned(k.first));
- return ConstBitIterator(*i, k.first);
- }
-
- /** The "off the end" const_iterator */
- ConstBitIterator end() const {
- return ConstBitIterator();
- }
-
- /**
- * 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, NodeValue*>& k) {
- uint64_t& word = super::operator[](k.second);
- return BitAccessor(word, k.first);
- }
-
- /**
- * Delete all flags from the given node.
- */
- void erase(NodeValue* nv) {
- super::erase(nv);
- }
-
-};/* class AttrHash<bool> */
-
-/**
- * A "CDAttrHash<value_type>"---the hash table underlying
- * attributes---is simply a context-dependent mapping of
- * pair<unique-attribute-id, Node> to value_type using our specialized
- * hash function for these pairs.
- */
-template <class value_type>
-class CDAttrHash :
- public CVC4::context::CDMap<std::pair<uint64_t, NodeValue*>,
- value_type,
- AttrHashStrategy> {
-public:
- CDAttrHash(context::Context* ctxt) :
- context::CDMap<std::pair<uint64_t, NodeValue*>,
- value_type,
- AttrHashStrategy>(ctxt) {
- }
-};
-
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE CLEANUP FUNCTIONS =================================================
-
namespace attr {
-/** Default cleanup for unmanaged Attribute<> */
-struct NullCleanupStrategy {
-};/* struct NullCleanupStrategy */
-
-/** Default cleanup for ManagedAttribute<> */
-template <class T>
-struct ManagedAttributeCleanupStrategy {
-};/* struct ManagedAttributeCleanupStrategy<> */
-
-/** Specialization for T* */
-template <class T>
-struct ManagedAttributeCleanupStrategy<T*> {
- static inline void cleanup(T* p) { delete p; }
-};/* struct ManagedAttributeCleanupStrategy<T*> */
-
-/** Specialization for const T* */
-template <class T>
-struct ManagedAttributeCleanupStrategy<const T*> {
- static inline void cleanup(const T* p) { delete p; }
-};/* struct ManagedAttributeCleanupStrategy<const T*> */
-
-/**
- * Helper for Attribute<> class below to determine whether a cleanup
- * is defined or not.
- */
-template <class T, class C>
-struct getCleanupStrategy {
- typedef T value_type;
- typedef KindValueToTableValueMapping<value_type> mapping;
- static void fn(typename mapping::table_value_type t) {
- C::cleanup(mapping::convertBack(t));
- }
-};/* struct getCleanupStrategy<> */
-
-/**
- * Specialization for NullCleanupStrategy.
- */
-template <class T>
-struct getCleanupStrategy<T, NullCleanupStrategy> {
- typedef T value_type;
- typedef KindValueToTableValueMapping<value_type> mapping;
- static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupStrategy<T, NullCleanupStrategy> */
-
-// out-of-class initialization required (because it's a non-integral type)
-template <class T>
-void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)(typename getCleanupStrategy<T, NullCleanupStrategy>::mapping::table_value_type) = NULL;
-
-/**
- * Specialization for ManagedAttributeCleanupStrategy<T>.
- */
-template <class T>
-struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > {
- typedef T value_type;
- typedef KindValueToTableValueMapping<value_type> mapping;
- static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */
-
-// out-of-class initialization required (because it's a non-integral type)
-template <class T>
-void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn)(typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::mapping::table_value_type) = NULL;
-
-/**
- * Specialization for ManagedAttributeCleanupStrategy<T*>.
- */
-template <class T>
-struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > {
- typedef T* value_type;
- typedef ManagedAttributeCleanupStrategy<value_type> C;
- typedef KindValueToTableValueMapping<value_type> mapping;
- static void fn(typename mapping::table_value_type t) {
- C::cleanup(mapping::convertBack(t));
- }
-};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */
-
-/**
- * Specialization for ManagedAttributeCleanupStrategy<const T*>.
- */
-template <class T>
-struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > {
- typedef const T* value_type;
- typedef ManagedAttributeCleanupStrategy<value_type> C;
- typedef KindValueToTableValueMapping<value_type> mapping;
- static void fn(typename mapping::table_value_type t) {
- C::cleanup(mapping::convertBack(t));
- }
-};/* struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > */
-
-/**
- * Cause compile-time error for improperly-instantiated
- * getCleanupStrategy<>.
- */
-template <class T, class U>
-struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >;
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
-
-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, bool context_dep>
-struct LastAttributeId {
- static uint64_t s_id;
-};
-
-/** Initially zero. */
-template <class T, bool context_dep>
-uint64_t LastAttributeId<T, context_dep>::s_id = 0;
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE TRAITS ============================================================
-
-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, bool context_dep>
-struct AttributeTraits {
- typedef void (*cleanup_t)(T);
- static std::vector<cleanup_t> cleanup;
-};
-
-template <class T, bool context_dep>
-std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
- AttributeTraits<T, context_dep>::cleanup;
-
-}/* 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 CleanupStrategy 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_dep whether this attribute kind is
- * context-dependent
- */
-template <class T,
- class value_t,
- class CleanupStrategy = attr::NullCleanupStrategy,
- bool context_dep = false>
-class Attribute {
- /**
- * The unique ID associated to this attribute. Assigned statically,
- * at load time.
- */
- static const uint64_t s_id;
-
-public:
-
- /** The value type for this attribute. */
- typedef value_t value_type;
-
- /** Get the unique ID associated to this attribute. */
- static inline uint64_t getId() { return s_id; }
-
- /**
- * 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;
-
- /**
- * Expose this setting to the users of this Attribute kind.
- */
- static const bool context_dependent = context_dep;
-
- /**
- * Register this attribute kind and 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 registerAttribute() {
- typedef typename attr::KindValueToTableValueMapping<value_t>::table_value_type table_value_type;
- typedef attr::AttributeTraits<table_value_type, context_dep> traits;
- uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
- Assert(traits::cleanup.size() == id);// sanity check
- traits::cleanup.push_back(attr::getCleanupStrategy<value_t, CleanupStrategy>::fn);
- return id;
- }
-};/* class Attribute<> */
-
-/**
- * An "attribute type" structure for boolean flags (special). The
- * full one is below; the existence of this one disallows for boolean
- * flag attributes with a specialized cleanup function.
- */
-/* -- doesn't work; other specialization is "more specific" ??
-template <class T, class CleanupStrategy, bool context_dep>
-class Attribute<T, bool, CleanupStrategy, context_dep> {
- template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
- ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
-};
-*/
-
-/**
- * An "attribute type" structure for boolean flags (special).
- */
-template <class T, bool context_dep>
-class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> {
- /** IDs for bool-valued attributes are actually bit assignments. */
- static const uint64_t s_id;
-
-public:
-
- /** The value type for this attribute; here, bool. */
- typedef bool value_type;
-
- /** Get the unique ID associated to this attribute. */
- static inline uint64_t getId() { return s_id; }
-
- /**
- * 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;
-
- /**
- * Expose this setting to the users of this Attribute kind.
- */
- static const bool context_dependent = context_dep;
-
- /**
- * Register this attribute kind and 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 registerAttribute() {
- uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++;
- AlwaysAssert( id <= 63,
- "Too many boolean node attributes registered "
- "during initialization !" );
- return id;
- }
-};/* class Attribute<..., bool, ...> */
-
-/**
- * This is a context-dependent attribute kind (the only difference
- * between CDAttribute<> and Attribute<> (with the fourth argument
- * "true") is that you cannot supply a cleanup function (a no-op one
- * is used).
- */
-template <class T,
- class value_type>
-struct CDAttribute :
- public Attribute<T, value_type, attr::NullCleanupStrategy, true> {};
-
-/**
- * This is a managed attribute kind (the only difference between
- * ManagedAttribute<> and Attribute<> is the default cleanup function
- * and the fact that ManagedAttributes cannot be context-dependent).
- * In the default ManagedAttribute cleanup function, the value is
- * destroyed with the delete operator. If the value is allocated with
- * the array version of new[], an alternate cleanup function should be
- * provided that uses array delete[]. It is an error to create a
- * ManagedAttribute<> kind with a non-pointer value_type if you don't
- * also supply a custom cleanup function.
- */
-template <class T,
- class value_type,
- class CleanupStrategy = attr::ManagedAttributeCleanupStrategy<value_type> >
-struct ManagedAttribute :
- public Attribute<T, value_type, CleanupStrategy, false> {};
-
-// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
-
-/** Assign unique IDs to attributes at load time. */
-// Use of the comma-operator here forces instantiation (and
-// initialization) of the AttributeTraits<> structure and its
-// "cleanup" vector before registerAttribute() is called. This is
-// important because otherwise the vector is initialized later,
-// clearing the first-pushed cleanup function.
-template <class T, class value_t, class CleanupStrategy, bool context_dep>
-const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
- ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(),
- Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
-
-/** Assign unique IDs to attributes at load time. */
-template <class T, bool context_dep>
-const uint64_t Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::s_id =
- Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::registerAttribute();
-
// ATTRIBUTE MANAGER ===========================================================
-namespace attr {
-
/**
* A container for the main attribute tables of the system. There's a
* one-to-one NodeManager : AttributeManager correspondence.
@@ -868,7 +212,7 @@ struct getTable<uint64_t, false> {
/** Access the "d_exprs" member of AttributeManager. */
template <>
-struct getTable<Node, false> {
+struct getTable<TNode, false> {
typedef AttrHash<TNode> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_exprs;
@@ -940,7 +284,7 @@ struct getTable<uint64_t, true> {
/** Access the "d_cdexprs" member of AttributeManager. */
template <>
-struct getTable<Node, true> {
+struct getTable<TNode, true> {
typedef CDAttrHash<TNode> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_cdexprs;
@@ -994,15 +338,17 @@ namespace attr {
// implementation for AttributeManager::getAttribute()
template <class AttrKind>
-typename AttrKind::value_type AttributeManager::getAttribute(NodeValue* nv,
- const AttrKind&) const {
-
+typename AttrKind::value_type
+AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::
+ table_type table_type;
- const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
- typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
+ const table_type& ah =
+ getTable<value_type, AttrKind::context_dependent>::get(*this);
+ typename table_type::const_iterator i =
+ ah.find(std::make_pair(AttrKind::getId(), nv));
if(i == ah.end()) {
return typename AttrKind::value_type();
@@ -1038,10 +384,14 @@ struct HasAttribute<true, AttrKind> {
typename AttrKind::value_type& ret) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+ typedef typename getTable<value_type,
+ AttrKind::context_dependent>::table_type
+ table_type;
- const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
- typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
+ const table_type& ah =
+ getTable<value_type, AttrKind::context_dependent>::get(*am);
+ typename table_type::const_iterator i =
+ ah.find(std::make_pair(AttrKind::getId(), nv));
if(i == ah.end()) {
ret = AttrKind::default_value;
@@ -1063,10 +413,13 @@ struct HasAttribute<false, AttrKind> {
NodeValue* nv) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::
+ table_type table_type;
- const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
- typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
+ const table_type& ah =
+ getTable<value_type, AttrKind::context_dependent>::get(*am);
+ typename table_type::const_iterator i =
+ ah.find(std::make_pair(AttrKind::getId(), nv));
if(i == ah.end()) {
return false;
@@ -1080,10 +433,13 @@ struct HasAttribute<false, AttrKind> {
typename AttrKind::value_type& ret) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::
+ table_type table_type;
- const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
- typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
+ const table_type& ah =
+ getTable<value_type, AttrKind::context_dependent>::get(*am);
+ typename table_type::const_iterator i =
+ ah.find(std::make_pair(AttrKind::getId(), nv));
if(i == ah.end()) {
return false;
@@ -1098,29 +454,56 @@ struct HasAttribute<false, AttrKind> {
template <class AttrKind>
bool AttributeManager::hasAttribute(NodeValue* nv,
const AttrKind&) const {
- return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, nv);
+ return HasAttribute<AttrKind::has_default_value, AttrKind>::
+ hasAttribute(this, nv);
}
template <class AttrKind>
bool AttributeManager::getAttribute(NodeValue* nv,
const AttrKind&,
typename AttrKind::value_type& ret) const {
- return HasAttribute<AttrKind::has_default_value, AttrKind>::getAttribute(this, nv, ret);
+ return HasAttribute<AttrKind::has_default_value, AttrKind>::
+ getAttribute(this, nv, ret);
}
template <class AttrKind>
-inline void AttributeManager::setAttribute(NodeValue* nv,
- const AttrKind&,
- const typename AttrKind::value_type& value) {
-
+inline void
+AttributeManager::setAttribute(NodeValue* nv,
+ const AttrKind&,
+ const typename AttrKind::value_type& value) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::
+ table_type table_type;
- table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
+ table_type& ah =
+ getTable<value_type, AttrKind::context_dependent>::get(*this);
ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
}
+/**
+ * Search for the NodeValue in all attribute tables and remove it,
+ * calling the cleanup function if one is defined.
+ */
+template <class T>
+inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
+ NodeValue* nv) {
+ for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
+ typedef AttributeTraits<T, false> traits_t;
+ typedef AttrHash<T> hash_t;
+ std::pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv);
+ if(traits_t::cleanup[id] != NULL) {
+ typename hash_t::iterator i = table.find(pr);
+ if(i != table.end()) {
+ traits_t::cleanup[id]((*i).second);
+ table.erase(pr);
+ }
+ } else {
+ table.erase(pr);
+ }
+ }
+}
+
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
}/* CVC4 namespace */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
new file mode 100644
index 000000000..d50c2284d
--- /dev/null
+++ b/src/expr/attribute_internals.h
@@ -0,0 +1,695 @@
+/********************* */
+/** attribute_internals.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.
+ **
+ ** Node attributes' internals.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+# error expr/attribute_internals.h should only be included by expr/attribute.h
+#endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
+
+#ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+#define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+
+namespace CVC4 {
+namespace expr {
+
+// ATTRIBUTE HASH FUNCTIONS ====================================================
+
+namespace attr {
+
+/**
+ * A hash function for attribute table keys. Attribute table keys are
+ * pairs, (unique-attribute-id, Node).
+ */
+struct AttrHashStrategy {
+ enum { LARGE_PRIME = 32452843ul };
+ std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
+ return p.first * LARGE_PRIME + p.second->getId();
+ }
+};
+
+/**
+ * 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 AttrHashBoolStrategy {
+ std::size_t operator()(NodeValue* nv) const {
+ return (size_t)nv->getId();
+ }
+};
+
+}/* 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; }
+};
+
+/**
+ * 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);
+ }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE HASH TABLES =======================================================
+
+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, NodeValue*>,
+ value_type,
+ AttrHashStrategy> {
+};
+
+/**
+ * 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<NodeValue*,
+ uint64_t,
+ AttrHashBoolStrategy> {
+
+ /** A "super" type, like in Java, for easy reference below. */
+ typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> 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;
+
+ unsigned d_bit;
+
+ public:
+
+ BitAccessor(uint64_t& word, unsigned bit) :
+ d_word(word),
+ d_bit(bit) {
+ }
+
+ BitAccessor& operator=(bool b) {
+ if(b) {
+ // set the bit
+ d_word |= (1 << d_bit);
+ } else {
+ // clear the bit
+ d_word &= ~(1 << d_bit);
+ }
+
+ return *this;
+ }
+
+ operator bool() const {
+ return (d_word & (1 << d_bit)) ? true : false;
+ }
+ };
+
+ /**
+ * 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<NodeValue* const, uint64_t>* d_entry;
+
+ unsigned d_bit;
+
+ public:
+
+ BitIterator() :
+ d_entry(NULL),
+ d_bit(0) {
+ }
+
+ BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
+ d_entry(&entry),
+ d_bit(bit) {
+ }
+
+ std::pair<NodeValue* const, BitAccessor> operator*() {
+ return std::make_pair(d_entry->first,
+ BitAccessor(d_entry->second, d_bit));
+ }
+
+ bool operator==(const BitIterator& b) {
+ return d_entry == b.d_entry && d_bit == b.d_bit;
+ }
+ };
+
+ /**
+ * 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<NodeValue* const, uint64_t>* d_entry;
+
+ unsigned d_bit;
+
+ public:
+
+ ConstBitIterator() :
+ d_entry(NULL),
+ d_bit(0) {
+ }
+
+ ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
+ unsigned bit) :
+ d_entry(&entry),
+ d_bit(bit) {
+ }
+
+ std::pair<NodeValue* const, bool> operator*() {
+ return std::make_pair(d_entry->first,
+ (d_entry->second & (1 << d_bit)) ? true : false);
+ }
+
+ bool operator==(const ConstBitIterator& b) {
+ return d_entry == b.d_entry && d_bit == b.d_bit;
+ }
+ };
+
+public:
+
+ typedef std::pair<uint64_t, NodeValue*> 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;
+
+ /**
+ * Find the boolean value in the hash table. Returns something ==
+ * end() if not found.
+ */
+ BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
+ super::iterator i = super::find(k.second);
+ if(i == super::end()) {
+ return BitIterator();
+ }
+ Debug.printf("boolattr",
+ "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+ &(*i).second,
+ (unsigned long long)((*i).second),
+ unsigned(k.first));
+ return BitIterator(*i, k.first);
+ }
+
+ /** The "off the end" iterator */
+ BitIterator end() {
+ return BitIterator();
+ }
+
+ /**
+ * Find the boolean value in the hash table. Returns something ==
+ * end() if not found.
+ */
+ ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
+ super::const_iterator i = super::find(k.second);
+ if(i == super::end()) {
+ return ConstBitIterator();
+ }
+ Debug.printf("boolattr",
+ "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+ &(*i).second,
+ (unsigned long long)((*i).second),
+ unsigned(k.first));
+ return ConstBitIterator(*i, k.first);
+ }
+
+ /** The "off the end" const_iterator */
+ ConstBitIterator end() const {
+ return ConstBitIterator();
+ }
+
+ /**
+ * 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, NodeValue*>& k) {
+ uint64_t& word = super::operator[](k.second);
+ return BitAccessor(word, k.first);
+ }
+
+ /**
+ * Delete all flags from the given node.
+ */
+ void erase(NodeValue* nv) {
+ super::erase(nv);
+ }
+
+};/* class AttrHash<bool> */
+
+/**
+ * A "CDAttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a context-dependent mapping of
+ * pair<unique-attribute-id, Node> to value_type using our specialized
+ * hash function for these pairs.
+ */
+template <class value_type>
+class CDAttrHash :
+ public context::CDMap<std::pair<uint64_t, NodeValue*>,
+ value_type,
+ AttrHashStrategy> {
+public:
+ CDAttrHash(context::Context* ctxt) :
+ context::CDMap<std::pair<uint64_t, NodeValue*>,
+ value_type,
+ AttrHashStrategy>(ctxt) {
+ }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE CLEANUP FUNCTIONS =================================================
+
+namespace attr {
+
+/** Default cleanup for unmanaged Attribute<> */
+struct NullCleanupStrategy {
+};/* struct NullCleanupStrategy */
+
+/** Default cleanup for ManagedAttribute<> */
+template <class T>
+struct ManagedAttributeCleanupStrategy {
+};/* struct ManagedAttributeCleanupStrategy<> */
+
+/** Specialization for T* */
+template <class T>
+struct ManagedAttributeCleanupStrategy<T*> {
+ static inline void cleanup(T* p) { delete p; }
+};/* struct ManagedAttributeCleanupStrategy<T*> */
+
+/** Specialization for const T* */
+template <class T>
+struct ManagedAttributeCleanupStrategy<const T*> {
+ static inline void cleanup(const T* p) { delete p; }
+};/* struct ManagedAttributeCleanupStrategy<const T*> */
+
+/**
+ * Helper for Attribute<> class below to determine whether a cleanup
+ * is defined or not.
+ */
+template <class T, class C>
+struct getCleanupStrategy {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupStrategy<> */
+
+/**
+ * Specialization for NullCleanupStrategy.
+ */
+template <class T>
+struct getCleanupStrategy<T, NullCleanupStrategy> {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupStrategy<T, NullCleanupStrategy> */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)
+ (typename getCleanupStrategy<T, NullCleanupStrategy>::
+ mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupStrategy<T>.
+ */
+template <class T>
+struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn)
+ (typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::
+ mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupStrategy<T*>.
+ */
+template <class T>
+struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > {
+ typedef T* value_type;
+ typedef ManagedAttributeCleanupStrategy<value_type> C;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */
+
+/**
+ * Specialization for ManagedAttributeCleanupStrategy<const T*>.
+ */
+template <class T>
+struct getCleanupStrategy<const T*,
+ ManagedAttributeCleanupStrategy<const T*> > {
+ typedef const T* value_type;
+ typedef ManagedAttributeCleanupStrategy<value_type> C;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupStrategy<const T*,
+ ManagedAttributeCleanupStrategy<const T*> > */
+
+/**
+ * Cause compile-time error for improperly-instantiated
+ * getCleanupStrategy<>.
+ */
+template <class T, class U>
+struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
+
+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, bool context_dep>
+struct LastAttributeId {
+ static uint64_t s_id;
+};
+
+/** Initially zero. */
+template <class T, bool context_dep>
+uint64_t LastAttributeId<T, context_dep>::s_id = 0;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE TRAITS ============================================================
+
+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, bool context_dep>
+struct AttributeTraits {
+ typedef void (*cleanup_t)(T);
+ static std::vector<cleanup_t> cleanup;
+};
+
+template <class T, bool context_dep>
+std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
+ AttributeTraits<T, context_dep>::cleanup;
+
+}/* 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 CleanupStrategy 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_dep whether this attribute kind is
+ * context-dependent
+ */
+template <class T,
+ class value_t,
+ class CleanupStrategy = attr::NullCleanupStrategy,
+ bool context_dep = false>
+class Attribute {
+ /**
+ * The unique ID associated to this attribute. Assigned statically,
+ * at load time.
+ */
+ static const uint64_t s_id;
+
+public:
+
+ /** The value type for this attribute. */
+ typedef value_t value_type;
+
+ /** Get the unique ID associated to this attribute. */
+ static inline uint64_t getId() { return s_id; }
+
+ /**
+ * 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;
+
+ /**
+ * Expose this setting to the users of this Attribute kind.
+ */
+ static const bool context_dependent = context_dep;
+
+ /**
+ * Register this attribute kind and 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 registerAttribute() {
+ typedef typename attr::KindValueToTableValueMapping<value_t>::
+ table_value_type table_value_type;
+ typedef attr::AttributeTraits<table_value_type, context_dep> traits;
+ uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
+ Assert(traits::cleanup.size() == id);// sanity check
+ traits::cleanup.push_back(attr::getCleanupStrategy<value_t,
+ CleanupStrategy>::fn);
+ return id;
+ }
+};/* class Attribute<> */
+
+/**
+ * An "attribute type" structure for boolean flags (special). The
+ * full one is below; the existence of this one disallows for boolean
+ * flag attributes with a specialized cleanup function.
+ */
+/* -- doesn't work; other specialization is "more specific" ??
+template <class T, class CleanupStrategy, bool context_dep>
+class Attribute<T, bool, CleanupStrategy, context_dep> {
+ template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
+ ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
+};
+*/
+
+/**
+ * An "attribute type" structure for boolean flags (special).
+ */
+template <class T, bool context_dep>
+class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> {
+ /** IDs for bool-valued attributes are actually bit assignments. */
+ static const uint64_t s_id;
+
+public:
+
+ /** The value type for this attribute; here, bool. */
+ typedef bool value_type;
+
+ /** Get the unique ID associated to this attribute. */
+ static inline uint64_t getId() { return s_id; }
+
+ /**
+ * 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;
+
+ /**
+ * Expose this setting to the users of this Attribute kind.
+ */
+ static const bool context_dependent = context_dep;
+
+ /**
+ * Register this attribute kind and 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 registerAttribute() {
+ uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++;
+ AlwaysAssert( id <= 63,
+ "Too many boolean node attributes registered "
+ "during initialization !" );
+ return id;
+ }
+};/* class Attribute<..., bool, ...> */
+
+/**
+ * This is a context-dependent attribute kind (the only difference
+ * between CDAttribute<> and Attribute<> (with the fourth argument
+ * "true") is that you cannot supply a cleanup function (a no-op one
+ * is used).
+ */
+template <class T,
+ class value_type>
+struct CDAttribute :
+ public Attribute<T, value_type, attr::NullCleanupStrategy, true> {};
+
+/**
+ * This is a managed attribute kind (the only difference between
+ * ManagedAttribute<> and Attribute<> is the default cleanup function
+ * and the fact that ManagedAttributes cannot be context-dependent).
+ * In the default ManagedAttribute cleanup function, the value is
+ * destroyed with the delete operator. If the value is allocated with
+ * the array version of new[], an alternate cleanup function should be
+ * provided that uses array delete[]. It is an error to create a
+ * ManagedAttribute<> kind with a non-pointer value_type if you don't
+ * also supply a custom cleanup function.
+ */
+template <class T,
+ class value_type,
+ class CleanupStrategy =
+ attr::ManagedAttributeCleanupStrategy<value_type> >
+struct ManagedAttribute :
+ public Attribute<T, value_type, CleanupStrategy, false> {};
+
+// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
+
+/** Assign unique IDs to attributes at load time. */
+// Use of the comma-operator here forces instantiation (and
+// initialization) of the AttributeTraits<> structure and its
+// "cleanup" vector before registerAttribute() is called. This is
+// important because otherwise the vector is initialized later,
+// clearing the first-pushed cleanup function.
+template <class T, class value_t, class CleanupStrategy, bool context_dep>
+const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
+ ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::
+ table_value_type,
+ context_dep>::cleanup.size(),
+ Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
+
+/** Assign unique IDs to attributes at load time. */
+template <class T, bool context_dep>
+const uint64_t Attribute<T,
+ bool,
+ attr::NullCleanupStrategy, context_dep>::s_id =
+ Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::
+ registerAttribute();
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__ATTRIBUTE_INTERNALS_H */
diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index bb224aa91..c4eb3af1c 100644
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -17,10 +17,13 @@
# SKOLEM.
#
# operator K #children ["comment"]
+# nonatomic_operator K #children ["comment"]
#
# Declares a "built-in" operator kind K. Really this is the same
# as "variable" except that it has an operator (automatically
-# generated by NodeManager).
+# generated by NodeManager). These two commands are identical,
+# except that kinds declared with nonatomic_operator answer false
+# to Node::isAtomic().
#
# You can specify an exact # of children required as the second
# argument to the operator command. In debug mode, assertions are
@@ -109,12 +112,11 @@ theory builtin
# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
# not stored that way. If you ask for the operator of (EQUAL a b),
# you'll get a special, singleton (BUILTIN EQUAL) Node.
-constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashFcn \
+constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \
"expr/kind.h" "The kind of nodes representing built-in operators"
operator EQUAL 2 "equality"
operator DISTINCT 2: "disequality"
-operator ITE 3 "if-then-else"
variable SKOLEM "skolem var"
variable VARIABLE "variable"
operator TUPLE 2: "a tuple"
diff --git a/src/expr/command.h b/src/expr/command.h
index e5994b3c7..6a4bb67ed 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -16,6 +16,8 @@
** client code.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__COMMAND_H
#define __CVC4__COMMAND_H
@@ -24,7 +26,6 @@
#include <string>
#include <vector>
-#include "cvc4_config.h"
#include "expr/expr.h"
#include "util/result.h"
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager_template.cpp
index 4eda9805a..2e25b4574 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1,5 +1,5 @@
/********************* */
-/** expr_manager.cpp
+/** expr_manager_template.cpp
** Original author: dejan
** Major contributors: cconway, mdeters
** Minor contributors (to current version): none
@@ -10,23 +10,25 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ ** Public-facing expression manager interface, implementation.
**/
-/*
- * expr_manager.cpp
- *
- * Created on: Dec 10, 2009
- * Author: dejan
- */
-
-#include "context/context.h"
+#include "expr/node.h"
#include "expr/expr.h"
-#include "expr/expr_manager.h"
#include "expr/kind.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
+#include "expr/metakind.h"
#include "expr/type.h"
+#include "expr/node_manager.h"
+#include "expr/expr_manager.h"
+#include "context/context.h"
+
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one. We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 32 "${template}"
using namespace std;
using namespace CVC4::context;
@@ -122,15 +124,13 @@ FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
return d_nodeManager->mkFunctionType(argTypes, range);
}
-FunctionType*
-ExprManager::mkFunctionType(const std::vector<Type*>& sorts) {
+FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& sorts) {
Assert( sorts.size() >= 2 );
NodeManagerScope nms(d_nodeManager);
return d_nodeManager->mkFunctionType(sorts);
}
-FunctionType*
-ExprManager::mkPredicateType(const std::vector<Type*>& sorts) {
+FunctionType* ExprManager::mkPredicateType(const std::vector<Type*>& sorts) {
Assert( sorts.size() >= 1 );
NodeManagerScope nms(d_nodeManager);
return d_nodeManager->mkPredicateType(sorts);
@@ -151,11 +151,12 @@ Expr ExprManager::mkVar(Type* type) {
return Expr(this, new Node(d_nodeManager->mkVar(type)));
}
-unsigned int ExprManager::minArity(Kind kind) {
+unsigned ExprManager::minArity(Kind kind) {
+ // FIXME: should be implemented this way, but parser depends on *parse*-level.
+ // See bug 75.
+ //return metakind::getLowerBoundForKind(kind);
switch(kind) {
- case FALSE:
case SKOLEM:
- case TRUE:
case VARIABLE:
return 0;
@@ -181,11 +182,12 @@ unsigned int ExprManager::minArity(Kind kind) {
}
}
-unsigned int ExprManager::maxArity(Kind kind) {
+unsigned ExprManager::maxArity(Kind kind) {
+ // FIXME: should be implemented this way, but parser depends on *parse*-level.
+ // See bug 75.
+ //return metakind::getUpperBoundForKind(kind);
switch(kind) {
- case FALSE:
case SKOLEM:
- case TRUE:
case VARIABLE:
return 0;
@@ -213,7 +215,6 @@ unsigned int ExprManager::maxArity(Kind kind) {
}
}
-
NodeManager* ExprManager::getNodeManager() const {
return d_nodeManager;
}
@@ -222,4 +223,6 @@ Context* ExprManager::getContext() const {
return d_ctxt;
}
+${mkConst_implementations}
+
}/* CVC4 namespace */
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager_template.h
index f2009ad80..523c12e3b 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager_template.h
@@ -1,5 +1,5 @@
/********************* */
-/** expr_manager.h
+/** expr_manager_template.h
** Original author: dejan
** Major contributors: cconway, mdeters
** Minor contributors (to current version): taking
@@ -13,20 +13,27 @@
** Public-facing expression manager interface.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__EXPR_MANAGER_H
#define __CVC4__EXPR_MANAGER_H
-#include "cvc4_config.h"
-#include "expr/kind.h"
#include <vector>
+#include "expr/kind.h"
+#include "expr/type.h"
+
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one. We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 33 "${template}"
+
namespace CVC4 {
class Expr;
-class Type;
-class BooleanType;
-class FunctionType;
-class KindType;
class SmtEngine;
class NodeManager;
@@ -35,6 +42,33 @@ namespace context {
}/* CVC4::context namespace */
class CVC4_PUBLIC ExprManager {
+private:
+ /** The context */
+ context::Context* d_ctxt;
+
+ /** The internal node manager */
+ NodeManager* d_nodeManager;
+
+ /**
+ * Returns the internal node manager. This should only be used by
+ * internal users, i.e. the friend classes.
+ */
+ NodeManager* getNodeManager() const;
+
+ /**
+ * Returns the internal Context. Used by internal users, i.e. the
+ * friend classes.
+ */
+ context::Context* getContext() const;
+
+ /**
+ * SmtEngine will use all the internals, so it will grab the
+ * NodeManager.
+ */
+ friend class SmtEngine;
+
+ /** ExprManagerScope reaches in to get the NodeManager */
+ friend class ExprManagerScope;
public:
@@ -65,7 +99,7 @@ public:
/**
* Make a unary expression of a given kind (NOT, BVNOT, ...).
- * @param kind the kind of expression
+ * @param child1 kind the kind of expression
* @return the expression
*/
Expr mkExpr(Kind kind, const Expr& child1);
@@ -79,10 +113,39 @@ public:
*/
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
+ /**
+ * Make a 3-ary expression of a given kind (AND, PLUS, ...).
+ * @param kind the kind of expression
+ * @param child1 the first child of the new expression
+ * @param child2 the second child of the new expression
+ * @param child3 the third child of the new expression
+ * @return the expression
+ */
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3);
+
+ /**
+ * Make a 4-ary expression of a given kind (AND, PLUS, ...).
+ * @param kind the kind of expression
+ * @param child1 the first child of the new expression
+ * @param child2 the second child of the new expression
+ * @param child3 the third child of the new expression
+ * @param child4 the fourth child of the new expression
+ * @return the expression
+ */
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3, const Expr& child4);
+
+ /**
+ * Make a 5-ary expression of a given kind (AND, PLUS, ...).
+ * @param kind the kind of expression
+ * @param child1 the first child of the new expression
+ * @param child2 the second child of the new expression
+ * @param child3 the third child of the new expression
+ * @param child4 the fourth child of the new expression
+ * @param child5 the fifth child of the new expression
+ * @return the expression
+ */
Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3, const Expr& child4, const Expr& child5);
@@ -94,30 +157,36 @@ public:
*/
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
+ /** Create a constant of type T */
+ template <class T>
+ Expr mkConst(const T&);
+
/** Make a function type from domain to range. */
- FunctionType*
- mkFunctionType(Type* domain,
- Type* range);
-
- /** Make a function type with input types from argTypes. <code>argTypes</code>
- * must have at least one element. */
- FunctionType*
- mkFunctionType(const std::vector<Type*>& argTypes,
- Type* range);
-
- /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
- * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
- * least 2 elements.
+ FunctionType* mkFunctionType(Type* domain,
+ Type* range);
+
+ /**
+ * Make a function type with input types from argTypes.
+ * <code>argTypes</code> must have at least one element.
*/
- FunctionType*
- mkFunctionType(const std::vector<Type*>& sorts);
+ FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
+ Type* range);
- /** Make a predicate type with input types from <code>sorts</code>. The result with
- * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
- * least one element.
+ /**
+ * Make a function type with input types from
+ * <code>sorts[0..sorts.size()-2]</code> and result type
+ * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
+ * at least 2 elements.
*/
- FunctionType*
- mkPredicateType(const std::vector<Type*>& sorts);
+ FunctionType* mkFunctionType(const std::vector<Type*>& sorts);
+
+ /**
+ * Make a predicate type with input types from
+ * <code>sorts</code>. The result with be a function type with range
+ * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
+ * element.
+ */
+ FunctionType* mkPredicateType(const std::vector<Type*>& sorts);
/** Make a new sort with the given name. */
Type* mkSort(const std::string& name);
@@ -127,41 +196,14 @@ public:
Expr mkVar(Type* type);
/** Returns the minimum arity of the given kind. */
- static unsigned int minArity(Kind kind);
+ static unsigned minArity(Kind kind);
/** Returns the maximum arity of the given kind. */
- static unsigned int maxArity(Kind kind);
-
-private:
- /** The context */
- context::Context* d_ctxt;
-
- /** The internal node manager */
- NodeManager* d_nodeManager;
-
- /**
- * Returns the internal node manager. This should only be used by
- * internal users, i.e. the friend classes.
- */
- NodeManager* getNodeManager() const;
-
- /**
- * Returns the internal Context. Used by internal users, i.e. the
- * friend classes.
- */
- context::Context* getContext() const;
-
- /**
- * SmtEngine will use all the internals, so it will grab the
- * NodeManager.
- */
- friend class SmtEngine;
-
- /** ExprManagerScope reaches in to get the NodeManager */
- friend class ExprManagerScope;
+ static unsigned maxArity(Kind kind);
};
+${mkConst_instantiations}
+
}/* CVC4 namespace */
#endif /* __CVC4__EXPR_MANAGER_H */
-
diff --git a/src/expr/expr.cpp b/src/expr/expr_template.cpp
index 2bcd28422..d02272320 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr_template.cpp
@@ -1,5 +1,5 @@
/********************* */
-/** expr.cpp
+/** expr_template.cpp
** Original author: dejan
** Major contributors: mdeters
** Minor contributors (to current version): taking
@@ -10,7 +10,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ ** Public-facing expression interface, implementation.
**/
#include "expr/expr.h"
@@ -19,6 +19,14 @@
#include "util/output.h"
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one. We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 29 "${template}"
+
using namespace CVC4::kind;
namespace CVC4 {
@@ -29,25 +37,25 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) {
}
Expr::Expr() :
- d_node(new Node()), d_exprManager(NULL) {
+ d_node(new Node),
+ d_exprManager(NULL) {
}
Expr::Expr(ExprManager* em, Node* node) :
- d_node(node), d_exprManager(em) {
+ d_node(node),
+ d_exprManager(em) {
}
Expr::Expr(const Expr& e) :
- d_node(new Node(*e.d_node)), d_exprManager(e.d_exprManager) {
+ d_node(new Node(*e.d_node)),
+ d_exprManager(e.d_exprManager) {
}
Expr::Expr(uintptr_t n) :
- d_node(new Node()),
- d_exprManager(NULL) {
- AlwaysAssert(n==0);
-}
+ d_node(new Node),
+ d_exprManager(NULL) {
-ExprManager* Expr::getExprManager() const {
- return d_exprManager;
+ AlwaysAssert(n == 0);
}
Expr::~Expr() {
@@ -55,33 +63,37 @@ Expr::~Expr() {
delete d_node;
}
+ExprManager* Expr::getExprManager() const {
+ return d_exprManager;
+}
+
Expr& Expr::operator=(const Expr& e) {
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+
ExprManagerScope ems(*this);
*d_node = *e.d_node;
d_exprManager = e.d_exprManager;
+
return *this;
}
/* This should only ever be assigning NULL to a null Expr! */
Expr& Expr::operator=(uintptr_t n) {
- AlwaysAssert(n==0);
+ AlwaysAssert(n == 0);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- if( EXPECT_FALSE(!isNull()) ) {
+
+ if(EXPECT_FALSE( !isNull() )) {
*d_node = Node::null();
}
return *this;
-/*
- Assert(isNull());
- return *this;
-*/
}
bool Expr::operator==(const Expr& e) const {
if(d_exprManager != e.d_exprManager) {
return false;
}
+ ExprManagerScope ems(*this);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
return *d_node == *e.d_node;
@@ -94,22 +106,39 @@ bool Expr::operator!=(const Expr& e) const {
bool Expr::operator<(const Expr& e) const {
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
- if(d_exprManager != e.d_exprManager) {
- return false;
+ if(isNull() && !e.isNull()) {
+ return true;
}
+ ExprManagerScope ems(*this);
return *d_node < *e.d_node;
}
Kind Expr::getKind() const {
+ ExprManagerScope ems(*this);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
return d_node->getKind();
}
size_t Expr::getNumChildren() const {
+ ExprManagerScope ems(*this);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
return d_node->getNumChildren();
}
+bool Expr::hasOperator() const {
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ return d_node->hasOperator();
+}
+
+Expr Expr::getOperator() const {
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ CheckArgument(d_node->hasOperator(),
+ "Expr::getOperator() called on an Expr with no operator");
+ return Expr(d_exprManager, new Node(d_node->getOperator()));
+}
+
Type* Expr::getType() const {
ExprManagerScope ems(*this);
return d_node->getType();
@@ -122,6 +151,7 @@ std::string Expr::toString() const {
}
bool Expr::isNull() const {
+ ExprManagerScope ems(*this);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
return d_node->isNull();
}
@@ -130,6 +160,18 @@ Expr::operator bool() const {
return !isNull();
}
+bool Expr::isConst() const {
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ return d_node->isConst();
+}
+
+bool Expr::isAtomic() const {
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ return d_node->isAtomic();
+}
+
void Expr::toStream(std::ostream& out) const {
ExprManagerScope ems(*this);
d_node->toStream(out);
@@ -207,5 +249,6 @@ void Expr::debugPrint() {
#endif /* ! CVC4_MUZZLE */
}
+${getConst_implementations}
-} // End namespace CVC4
+}/* CVC4 namespace */
diff --git a/src/expr/expr.h b/src/expr/expr_template.h
index 48b64fd17..12307e679 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr_template.h
@@ -1,5 +1,5 @@
/********************* */
-/** expr.h
+/** expr_template.h
** Original author: dejan
** Major contributors: none
** Minor contributors (to current version): taking, mdeters
@@ -13,22 +13,30 @@
** Public-facing expression interface.
**/
+#include "cvc4_public.h"
+
// circular dependency: force expr_manager.h first
#include "expr/expr_manager.h"
#ifndef __CVC4__EXPR_H
#define __CVC4__EXPR_H
-#include "cvc4_config.h"
-
#include <string>
#include <iostream>
#include <stdint.h>
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one. We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 35 "${template}"
+
namespace CVC4 {
// The internal expression representation
-template <bool count_ref>
+template <bool ref_count>
class NodeTemplate;
/**
@@ -36,6 +44,20 @@ class NodeTemplate;
* expressions.
*/
class CVC4_PUBLIC Expr {
+protected:
+
+ /** The internal expression representation */
+ NodeTemplate<true>* d_node;
+
+ /** The responsible expression manager */
+ ExprManager* d_exprManager;
+
+ /**
+ * Constructor for internal purposes.
+ * @param em the expression manager that handles this expression
+ * @param node the actual expression node pointer
+ */
+ Expr(ExprManager* em, NodeTemplate<true>* node);
public:
@@ -44,7 +66,7 @@ public:
/**
* Copy constructor, makes a copy of a given expression
- * @param the expression to copy
+ * @param e the expression to copy
*/
Expr(const Expr& e);
@@ -68,7 +90,7 @@ public:
*/
Expr& operator=(const Expr& e);
- /**
+ /*
* Assignment from an integer. Fails if the integer is not 0.
* NOTE: This is here purely to support the auto-initialization
* behavior of the ANTLR3 C backend (i.e., a rule attribute
@@ -104,11 +126,6 @@ public:
bool operator<(const Expr& e) const;
/**
- * Returns true if the expression is not the null expression.
- */
- operator bool() const;
-
- /**
* Returns the kind of the expression (AND, PLUS ...).
* @return the kind of the expression
*/
@@ -120,6 +137,19 @@ public:
*/
size_t getNumChildren() const;
+ /**
+ * Check if this is an expression that has an operator.
+ * @return true if this expression has an operator
+ */
+ bool hasOperator() const;
+
+ /**
+ * Get the operator of this expression.
+ * @throws IllegalArgumentException if it has no operator
+ * @return the operator of this expression
+ */
+ Expr getOperator() const;
+
/** Returns the type of the expression, if it has been computed.
* Returns NULL if the type of the expression is not known.
*/
@@ -133,7 +163,7 @@ public:
/**
* Outputs the string representation of the expression to the stream.
- * @param the output stream
+ * @param out the output stream
*/
void toStream(std::ostream& out) const;
@@ -144,6 +174,28 @@ public:
bool isNull() const;
/**
+ * Check if this is a null expression.
+ * @return true if NOT a null expression
+ */
+ operator bool() const;
+
+ /**
+ * Check if this is an expression representing a constant.
+ * @return true if a constant expression
+ */
+ bool isConst() const;
+
+ /**
+ * Check if this is an expression representing a constant.
+ * @return true if a constant expression
+ */
+ bool isAtomic() const;
+
+ /** Extract a constant of type T */
+ template <class T>
+ const T& getConst() const;
+
+ /**
* Returns the expression reponsible for this expression.
*/
ExprManager* getExprManager() const;
@@ -154,10 +206,10 @@ public:
* @param out output stream to print to.
* @param indent number of spaces to indent the formula by.
*/
- void printAst(std::ostream & out, int indent = 0) const;
-
+ void printAst(std::ostream& out, int indent = 0) const;
+
private:
-
+
/**
* Pretty printer for use within gdb
* This is not intended to be used outside of gdb.
@@ -169,19 +221,6 @@ private:
protected:
/**
- * Constructor for internal purposes.
- * @param em the expression manager that handles this expression
- * @param node the actual expression node pointer
- */
- Expr(ExprManager* em, NodeTemplate<true>* node);
-
- /** The internal expression representation */
- NodeTemplate<true>* d_node;
-
- /** The responsible expression manager */
- ExprManager* d_exprManager;
-
- /**
* Returns the actual internal node.
* @return the internal node
*/
@@ -279,6 +318,8 @@ public:
Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
};
-}
+${getConst_instantiations}
+
+}/* CVC4 namespace */
#endif /* __CVC4__EXPR_H */
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 2b675be0f..96c34a02a 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -13,10 +13,11 @@
** Template for the Node kind header.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__KIND_H
#define __CVC4__KIND_H
-#include "cvc4_config.h"
#include <iostream>
#include <sstream>
@@ -62,9 +63,9 @@ inline std::string kindToString(::CVC4::Kind k) {
return ss.str();
}
-struct KindHashFcn {
+struct KindHashStrategy {
static inline size_t hash(::CVC4::Kind k) { return k; }
-};
+};/* struct KindHashStrategy */
}/* CVC4::kind namespace */
}/* CVC4 namespace */
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 95e107313..052458cbe 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -123,6 +123,16 @@ ${metakind_kinds}
return metaKinds[k];
}/* metaKindOf(k) */
+static inline bool kindIsAtomic(Kind k) {
+ static const bool isAtomic[] = {
+ false, /* NULL_EXPR */
+${metakind_isatomic}
+ false /* LAST_KIND */
+ };/* isAtomic[] */
+
+ return isAtomic[k];
+}/* kindIsAtomic(k) */
+
}/* CVC4::kind namespace */
namespace expr {
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
new file mode 100755
index 000000000..de6de014d
--- /dev/null
+++ b/src/expr/mkexpr
@@ -0,0 +1,177 @@
+#!/bin/bash
+#
+# mkexpr
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010 The CVC4 Project
+#
+# The purpose of this script is to create {expr,expr_manager}.{h,cpp}
+# from template files and a list of theory kinds. Basically it just
+# sets up the public interface for access to constants.
+#
+# Invocation:
+#
+# mkexpr template-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+copyright=2010
+
+filename=`basename "$1" | sed 's,_template,,'`
+
+cat <<EOF
+/********************* */
+/** $filename
+ **
+ ** Copyright $copyright The AcSys Group, New York University, and as below.
+ **
+ ** This file automatically generated by:
+ **
+ ** $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+EOF
+
+me=$(basename "$0")
+
+template=$1; shift
+
+includes=
+getConst_instantiations=
+getConst_implementations=
+mkConst_instantiations=
+mkConst_implementations=
+
+seen_theory=false
+seen_theory_builtin=false
+
+function theory {
+ # theory T header
+
+ lineno=${BASH_LINENO[0]}
+
+ # this script doesn't care about the theory class information, but
+ # makes does make sure it's there
+ seen_theory=true
+ if [ "$1" = builtin ]; then
+ if $seen_theory_builtin; then
+ echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
+ exit 1
+ fi
+ seen_theory_builtin=true
+ elif [ -z "$1" -o -z "$2" ]; then
+ echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
+ exit 1
+ elif ! expr "$1" : '\(::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+ elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+ fi
+}
+
+function variable {
+ # variable K ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+}
+
+function operator {
+ # operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+}
+
+function nonatomic_operator {
+ # nonatomic_operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+}
+
+function parameterized {
+ # parameterized K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+}
+
+function constant {
+ # constant K T Hasher header ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+
+ includes="${includes}
+#include \"$4\""
+ mkConst_instantiations="${mkConst_instantiations}
+template <>
+Expr ExprManager::mkConst($2 const& val);
+"
+ mkConst_implementations="${mkConst_implementations}
+template <>
+Expr ExprManager::mkConst($2 const& val) {
+ return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val)));
+}
+"
+ getConst_instantiations="${getConst_instantiations}
+template <>
+$2 const & Expr::getConst< $2 >() const;
+"
+ getConst_implementations="${getConst_implementations}
+template <>
+$2 const & Expr::getConst() const {
+ return d_node->getConst< $2 >();
+}
+"
+}
+
+function check_theory_seen {
+ if ! $seen_theory; then
+ echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
+ exit 1
+ fi
+}
+
+function check_builtin_theory_seen {
+ if ! $seen_theory_builtin; then
+ echo "$me: warning: no declaration for the builtin theory found" >&2
+ fi
+}
+
+while [ $# -gt 0 ]; do
+ kf=$1
+ seen_theory=false
+ b=$(basename $(dirname "$kf"))
+ source "$kf"
+ check_theory_seen
+ shift
+done
+check_builtin_theory_seen
+
+## output
+
+text=$(cat "$template")
+for var in \
+ includes \
+ template \
+ getConst_instantiations \
+ getConst_implementations \
+ mkConst_instantiations \
+ mkConst_implementations; do
+ eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+done
+error=`expr "$text" : '.*\${\([^}]*\)}.*'`
+if [ -n "$error" ]; then
+ echo "$template:0: error: undefined replacement \${$error}" >&2
+ exit 1
+fi
+echo "$text"
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 6d75164d1..294dc5d7e 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -4,12 +4,12 @@
# 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 section, epilogue, and a list of theory kinds.
+# The purpose of this script is to create kind.h from a template and a
+# list of theory kinds.
#
# Invocation:
#
-# mkkind prologue-file middle-file epilogue-file theory-kind-files...
+# mkkind template-file theory-kind-files...
#
# Output is to standard out.
#
@@ -17,7 +17,7 @@
copyright=2010
cat <<EOF
-/********************* -*- C++ -*- */
+/********************* */
/** kind.h
**
** Copyright $copyright The AcSys Group, New York University, and as below.
@@ -83,6 +83,15 @@ function operator {
register_kind "$1" "$2" "$3"
}
+function nonatomic_operator {
+ # nonatomic_operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_kind "$1" "$2" "$3"
+}
+
function parameterized {
# parameterized K #children ["comment"]
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 15551d54d..3884f636a 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -4,15 +4,15 @@
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
# Copyright (c) 2010 The CVC4 Project
#
-# The purpose of this script is to create metakind.h from a prologue,
-# two middle sections, epilogue, and a list of theory kinds.
+# The purpose of this script is to create metakind.h from a template
+# and a list of theory kinds.
#
# This is kept distinct from kind.h because kind.h is a public header
# and metakind.h is intended for the expr package only.
#
# Invocation:
#
-# mkmetakind prologue-file middle1-file middle2-file epilogue-file theory-kind-files...
+# mkmetakind template-file theory-kind-files...
#
# Output is to standard out.
#
@@ -20,7 +20,7 @@
copyright=2010
cat <<EOF
-/********************* -*- C++ -*- */
+/********************* */
/** metakind.h
**
** Copyright $copyright The AcSys Group, New York University, and as below.
@@ -98,6 +98,15 @@ function operator {
register_metakind OPERATOR "$1" "$2"
}
+function nonatomic_operator {
+ # nonatomic_operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_metakind NONATOMIC_OPERATOR "$1" "$2"
+}
+
function parameterized {
# parameterized K #children ["comment"]
@@ -115,7 +124,14 @@ function constant {
check_theory_seen
if ! expr "$2" : '\(::*\)' >/dev/null; then
- echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
+ if ! primitive_type "$2"; then
+ # if there's an embedded space, we're probably doing something
+ # tricky to specify the CONST payload, like "int const*"; in any
+ # case, this warning gives too many false positives, so disable it
+ if ! expr "$2" : '..* ..*' >/dev/null; then
+ echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
+ fi
+ fi
fi
if ! expr "$3" : '\(::*\)' >/dev/null; then
echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2
@@ -133,14 +149,15 @@ function constant {
namespace expr {
template <>
-inline const $2 & NodeValue::getConst< $2 >() const {
- Assert(getKind() == ::CVC4::kind::$1);
+inline $2 const& NodeValue::getConst< $2 >() const {
+ AssertArgument(getKind() == ::CVC4::kind::$1, *this,
+ \"Improper kind for getConst<$2>()\");
// To support non-inlined CONSTANT-kinded NodeValues (those that are
// \"constructed\" when initially checking them against the NodeManager
// pool), we must check d_nchildren here.
return d_nchildren == 0
- ? *reinterpret_cast< const $2 * >(d_children)
- : *reinterpret_cast< const $2 * >(d_children[0]);
+ ? *reinterpret_cast< $2 const* >(d_children)
+ : *reinterpret_cast< $2 const* >(d_children[0]);
}
}/* CVC4::expr namespace */
@@ -166,10 +183,12 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
"
metakind_constHashes="${metakind_constHashes}
case kind::$1:
+#line $lineno \"$kf\"
return $3::hash(nv->getConst< $2 >());
"
metakind_constPrinters="${metakind_constPrinters}
case kind::$1:
+#line $lineno \"$kf\"
out << nv->getConst< $2 >();
break;
"
@@ -179,17 +198,27 @@ function register_metakind {
mk=$1
k=$2
nc=$3
+
+ if [ $mk = NONATOMIC_OPERATOR ]; then
+ metakind_isatomic="${metakind_isatomic} false, /* $k */
+";
+ mk=OPERATOR
+ else
+ metakind_isatomic="${metakind_isatomic} true, /* $k */
+";
+ fi
+
metakind_kinds="${metakind_kinds} metakind::$mk, /* $k */
";
# figure out the range given by $nc
- if expr "$nc" : '^[0-9]\+$' >/dev/null; then
+ if expr "$nc" : '[0-9]\+$' >/dev/null; then
lb=$nc
ub=$nc
- elif expr "$nc" : '^[0-9]\+:$' >/dev/null; then
+ elif expr "$nc" : '[0-9]\+:$' >/dev/null; then
let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
ub=MAX_CHILDREN
- elif expr "$nc" : '^[0-9]\+:[0-9]\+$' >/dev/null; then
+ elif expr "$nc" : '[0-9]\+:[0-9]\+$' >/dev/null; then
let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
if [ $ub -lt $lb ]; then
echo "$kf:$lineno: error in range \`$nc': LB < UB (in definition of $k)" >&2
@@ -200,12 +229,35 @@ function register_metakind {
exit 1
fi
+ if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then
+ if [ $lb = 0 ]; then
+ echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
+ exit 1
+ fi
+ fi
+
metakind_lbchildren="${metakind_lbchildren}
$lb, /* $k */"
metakind_ubchildren="${metakind_ubchildren}
$ub, /* $k */"
}
+# Returns 0 if arg is a primitive C++ type, or a pointer to same; 1
+# otherwise. Really all this does is check whether we should issue a
+# "not fully qualified" warning or not.
+function primitive_type {
+ strip=`expr "$1" : ' *\(.*\)\* *'`
+ if [ -n "$strip" ]; then
+ primitive_type "$strip" >&2
+ return $?
+ fi
+
+ case "$1" in
+ bool|int|size_t|long|void|char|float|double) return 0;;
+ *) return 1;;
+ esac
+}
+
function check_theory_seen {
if ! $seen_theory; then
echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
@@ -226,6 +278,9 @@ while [ $# -gt 0 ]; do
metakind_kinds="${metakind_kinds}
/* from $b */
"
+ metakind_isatomic="${metakind_isatomic}
+ /* from $b */
+"
source "$kf"
check_theory_seen
shift
@@ -235,9 +290,16 @@ check_builtin_theory_seen
## output
text=$(cat "$template")
-for var in metakind_includes metakind_kinds metakind_constantMaps \
- metakind_compares metakind_constHashes metakind_constPrinters \
- metakind_ubchildren metakind_lbchildren; do
+for var in \
+ metakind_includes \
+ metakind_kinds \
+ metakind_isatomic \
+ metakind_constantMaps \
+ metakind_compares \
+ metakind_constHashes \
+ metakind_constPrinters \
+ metakind_ubchildren \
+ metakind_lbchildren; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
diff --git a/src/expr/node.h b/src/expr/node.h
index 343f03a1f..875760725 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -15,6 +15,7 @@
#include "cvc4_private.h"
+// circular dependency
#include "expr/node_value.h"
#ifndef __CVC4__NODE_H
@@ -25,11 +26,10 @@
#include <iostream>
#include <stdint.h>
-#include "cvc4_config.h"
#include "expr/kind.h"
+#include "expr/metakind.h"
#include "expr/type.h"
#include "util/Assert.h"
-
#include "util/output.h"
namespace CVC4 {
@@ -216,7 +216,15 @@ public:
* Returns true if this node is atomic (has no more Boolean structure)
* @return true if atomic
*/
- bool isAtomic() const;
+ inline bool isAtomic() const;
+
+ /**
+ * Returns true if this node represents a constant
+ * @return true if const
+ */
+ inline bool isConst() const {
+ return getMetaKind() == kind::metakind::CONSTANT;
+ }
/**
* Returns the unique id of this node
@@ -578,23 +586,9 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
template <bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
-////FIXME: This function is a major hack! Should be changed ASAP
-////TODO: Should use positive definition, i.e. what kinds are atomic.
template <bool ref_count>
bool NodeTemplate<ref_count>::isAtomic() const {
- using namespace kind;
- switch(getKind()) {
- case NOT:
- case XOR:
- case ITE:
- case IFF:
- case IMPLIES:
- case OR:
- case AND:
- return false;
- default:
- return true;
- }
+ return kind::kindIsAtomic(getKind());
}
// FIXME: escape from type system convenient but is there a better
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f2718a06c..d17ec9497 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -293,24 +293,28 @@ public:
/** Make a function type from domain to range. */
inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
- /** Make a function type with input types from argTypes. <code>argTypes</code>
- * must have at least one element. */
+ /**
+ * Make a function type with input types from
+ * argTypes. <code>argTypes</code> must have at least one element.
+ */
inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
Type* range) const;
- /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
- * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
- * least 2 elements.
+ /**
+ * Make a function type with input types from
+ * <code>sorts[0..sorts.size()-2]</code> and result type
+ * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
+ * at least 2 elements.
*/
- inline FunctionType*
- mkFunctionType(const std::vector<Type*>& sorts);
+ inline FunctionType* mkFunctionType(const std::vector<Type*>& sorts) const;
- /** Make a predicate type with input types from <code>sorts</code>. The result with
- * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
- * least one element.
+ /**
+ * Make a predicate type with input types from
+ * <code>sorts</code>. The result with be a function type with range
+ * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
+ * element.
*/
- inline FunctionType*
- mkPredicateType(const std::vector<Type*>& sorts);
+ inline FunctionType* mkPredicateType(const std::vector<Type*>& sorts) const;
/** Make a new sort with the given name. */
inline Type* mkSort(const std::string& name) const;
@@ -453,7 +457,7 @@ NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
}
inline FunctionType*
-NodeManager::mkFunctionType(const std::vector<Type*>& sorts) {
+NodeManager::mkFunctionType(const std::vector<Type*>& sorts) const {
Assert( sorts.size() >= 2 );
std::vector<Type*> argTypes(sorts);
Type* rangeType = argTypes.back();
@@ -462,10 +466,11 @@ NodeManager::mkFunctionType(const std::vector<Type*>& sorts) {
}
inline FunctionType*
-NodeManager::mkPredicateType(const std::vector<Type*>& sorts) {
+NodeManager::mkPredicateType(const std::vector<Type*>& sorts) const {
Assert( sorts.size() >= 1 );
return mkFunctionType(sorts,booleanType());
}
+
inline Type* NodeManager::mkSort(const std::string& name) const {
return new SortType(name);
}
@@ -577,23 +582,6 @@ template <class T>
Node NodeManager::mkConst(const T& val) {
// typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
- //
- // TODO: construct a special NodeValue that points to this T but
- // is == an inlined version (like exists in the hash_set).
- //
- // Something similar for (a, b) and (a, b, c) and (a, b, c, d)
- // versions.
- //
- // ALSO TODO: make poolLookup() use hash_set<>::operator[] to auto-insert,
- // and then set = value after to avoid double-hashing. fix in all places
- // where poolLookup is called.
- //
- // THEN ALSO TODO: CDMap<> destruction in attribute.cpp to make valgrind
- // happy
- //
- // THEN: reconsider CVC3 tracing mechanism, experiments..
- //
-
NVStorage<1> nvStorage;
expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 7dd90913f..6408ef01a 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -25,10 +25,9 @@
#ifndef __CVC4__EXPR__NODE_VALUE_H
#define __CVC4__EXPR__NODE_VALUE_H
-#include "cvc4_config.h"
#include "expr/kind.h"
-#include <stdint.h>
+#include <stdint.h>
#include <string>
#include <iterator>
diff --git a/src/expr/type.h b/src/expr/type.h
index b406bfd76..9e6596e84 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -13,10 +13,11 @@
** Interface for expression types
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__TYPE_H
#define __CVC4__TYPE_H
-#include "cvc4_config.h"
#include "util/output.h"
#include "util/Assert.h"
@@ -262,7 +263,7 @@ struct TypeCleanupStrategy {
delete t;
}
}
-};
+};/* struct TypeCleanupStrategy */
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback