#
# addsourcedir
# Morgan Deters <mdeters@cs.nyu.edu> for the CVC4 project
+# Copyright (c) 2010 The CVC4 Project
#
# usage: addsourcedir paths...
#
--- /dev/null
+#!/bin/sh
+#
+# configure-in-place
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010 The CVC4 Project
+#
+# usage: configure-in-place [ arguments... ]
+#
+# This script configures CVC4 in the source directory (from where it
+# should be invoked).
+#
+
+if [ -e .svn ]; then
+ echo
+ echo "DO NOT USE THIS IN SUBVERSION WORKING DIRECTORIES!"
+ echo
+ echo "You might accidentally commit Makefiles in the source directories"
+ echo "improperly, since they exist in the source directory for"
+ echo "another purpose."
+ echo
+ exit 1
+fi
+
+./configure "$@"
+. builds/current
+builds/$(CURRENT_BUILD)/config.status
#!/usr/bin/perl -w
# DIMACS to SMT
-# Morgan Deters 2009
+# Morgan Deters
+# Copyright (c) 2009, 2010 The CVC4 Project
use strict;
#
# get-authors
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2009, 2010 The CVC4 Project
#
# usage: get-authors [ files... ]
#
#
# update-copyright.pl
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2009, 2010 The CVC4 Project
#
# usage: update-copyright [ files/directories... ]
#
-I@srcdir@/include -I@srcdir@
AM_CXXFLAGS = -Wall -fvisibility=hidden
-SUBDIRS = expr util context prop smt theory . parser main
+SUBDIRS = expr util context theory prop smt . parser main
lib_LTLIBRARIES = libcvc4.la
command.h \
command.cpp
-EXTRA_DIST = @srcdir@/kind.h kind_prologue.h kind_middle.h kind_epilogue.h
+EXTRA_DIST = \
+ @srcdir@/kind.h \
+ kind_prologue.h \
+ kind_middle.h \
+ kind_epilogue.h
@srcdir@/kind.h: @srcdir@/mkkind kind_prologue.h kind_middle.h kind_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
chmod +x @srcdir@/mkkind
** information.
**
** Node attributes.
- **
- ** Attribute structures:
- **
- ** An attribute structure looks like the following:
- **
- ** struct VarNameAttr {
- **
- ** // the value type for this attribute
- ** typedef std::string value_type;
- **
- ** // an extra hash value (to avoid same-value-type collisions)
- ** enum { hash_value = 1 };
- **
- ** // cleanup routine when the Node goes away
- ** static inline void cleanup(const std::string&) {
- ** }
- ** }
**/
/* There are strong constraints on ordering of declarations of
#include "config.h"
#include "context/context.h"
-#include "expr/soft_node.h"
+#include "expr/node.h"
#include "expr/type.h"
#include "util/output.h"
// ATTRIBUTE HASH FUNCTIONS ====================================================
+namespace attr {
+
+/**
+ * A hash function for attribute table keys. Attribute table keys are
+ * pairs, (unique-attribute-id, Node).
+ */
struct AttrHashFcn {
- enum { LARGE_PRIME = 1 };
- std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const {
+ enum { LARGE_PRIME = 32452843ul };
+ std::size_t operator()(const std::pair<uint64_t, TNode>& p) const {
return p.first * LARGE_PRIME + p.second.hash();
}
};
+/**
+ * A hash function for boolean-valued attribute table keys; here we
+ * don't have to store a pair as the key, because we use a known bit
+ * in [0..63] for each attribute
+ */
struct AttrHashBoolFcn {
- std::size_t operator()(const SoftNode& n) const {
+ std::size_t operator()(TNode n) const {
return n.hash();
}
};
+}/* CVC4::expr::attr namespace */
+
// ATTRIBUTE TYPE MAPPINGS =====================================================
+namespace attr {
+
+/**
+ * KindValueToTableValueMapping is a compile-time-only mechanism to
+ * convert "attribute value types" into "table value types" and back
+ * again.
+ *
+ * Each instantiation <T> is expected to have three members:
+ *
+ * typename table_value_type
+ *
+ * A type representing the underlying table's value_type for
+ * attribute value type (T). It may be different from T, e.g. T
+ * could be a pointer-to-Foo, but the underlying table value_type
+ * might be pointer-to-void.
+ *
+ * static [convertible-to-table_value_type] convert([convertible-from-T])
+ *
+ * Converts a T into a table_value_type. Used to convert an
+ * attribute value on setting it (and assigning it into the
+ * underlying table). See notes on specializations of
+ * KindValueToTableValueMapping, below.
+ *
+ * static [convertible-to-T] convertBack([convertible-from-table_value_type])
+ *
+ * Converts a table_value_type back into a T. Used to convert an
+ * underlying table value back into the attribute's expected type
+ * when retrieving it from the table. See notes on
+ * specializations of KindValueToTableValueMapping, below.
+ *
+ * This general (non-specialized) implementation of the template does
+ * nothing.
+ */
template <class T>
struct KindValueToTableValueMapping {
+ /** Simple case: T == table_value_type */
typedef T table_value_type;
+ /** No conversion necessary */
inline static T convert(const T& t) { return t; }
+ /** No conversion necessary */
inline static T convertBack(const T& t) { return t; }
};
-template <>
-struct KindValueToTableValueMapping<bool> {
- typedef uint64_t table_value_type;
- inline static uint64_t convert(const bool& t) { return t; }
- inline static bool convertBack(const uint64_t& t) { return t; }
-};
-
+/**
+ * Specialization of KindValueToTableValueMapping<> for pointer-valued
+ * attributes.
+ */
template <class T>
struct KindValueToTableValueMapping<T*> {
+ /** Table's value type is void* */
typedef void* table_value_type;
+ /** A simple reinterpret_cast<>() conversion from T* to void* */
inline static void* convert(const T* const& t) {
return reinterpret_cast<void*>(const_cast<T*>(t));
}
+ /** A simple reinterpret_cast<>() conversion from void* to T* */
inline static T* convertBack(void* const& t) {
return reinterpret_cast<T*>(t);
}
};
+/**
+ * Specialization of KindValueToTableValueMapping<> for const
+ * pointer-valued attributes.
+ */
template <class T>
struct KindValueToTableValueMapping<const T*> {
+ /** Table's value type is void* */
typedef void* table_value_type;
+ /** A simple reinterpret_cast<>() conversion from const T* const to void* */
inline static void* convert(const T* const& t) {
return reinterpret_cast<void*>(const_cast<T*>(t));
}
+ /** A simple reinterpret_cast<>() conversion from const void* const to T* */
inline static const T* convertBack(const void* const& t) {
return reinterpret_cast<const T*>(t);
}
};
-template <class AttrKind, class T>
-struct OwnTable;
-
-template <class AttrKind, class T>
-struct KindValueToTableValueMapping<OwnTable<AttrKind, T> > {
- typedef typename KindValueToTableValueMapping<T>::table_value_type table_value_type;
-};
-
-template <class AttrKind>
-struct KindTableMapping {
- typedef typename AttrKind::value_type table_identifier;
-};
+}/* CVC4::expr::attr namespace */
// ATTRIBUTE HASH TABLES =======================================================
-// use a TAG to indicate which table it should be in
+namespace attr {
+
+/**
+ * An "AttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a mapping of pair<unique-attribute-id, Node>
+ * to value_type using our specialized hash function for these pairs.
+ */
template <class value_type>
-struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {};
+struct AttrHash :
+ public __gnu_cxx::hash_map<std::pair<uint64_t, TNode>,
+ value_type,
+ AttrHashFcn> {
+};
+/**
+ * In the case of Boolean-valued attributes we have a special
+ * "AttrHash<bool>" to pack bits together in words.
+ */
template <>
-class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
-
- typedef __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> super;
-
+class AttrHash<bool> :
+ protected __gnu_cxx::hash_map<TNode,
+ uint64_t,
+ AttrHashBoolFcn> {
+
+ /** A "super" type, like in Java, for easy reference below. */
+ typedef __gnu_cxx::hash_map<TNode, uint64_t, AttrHashBoolFcn> super;
+
+ /**
+ * BitAccessor allows us to return a bit "by reference." Of course,
+ * we don't require bit-addressibility supported by the system, we
+ * do it with a complex type.
+ */
class BitAccessor {
uint64_t& d_word;
}
};
+ /**
+ * A (somewhat degenerate) iterator over boolean-valued attributes.
+ * This iterator doesn't support anything except comparison and
+ * dereference. It's intended just for the result of find() on the
+ * table.
+ */
class BitIterator {
- std::pair<const SoftNode, uint64_t>* d_entry;
+ std::pair<const TNode, uint64_t>* d_entry;
unsigned d_bit;
d_bit(0) {
}
- BitIterator(std::pair<const SoftNode, uint64_t>& entry, unsigned bit) :
+ BitIterator(std::pair<const TNode, uint64_t>& entry, unsigned bit) :
d_entry(&entry),
d_bit(bit) {
}
- std::pair<const SoftNode, BitAccessor> operator*() {
+ std::pair<const TNode, BitAccessor> operator*() {
return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit));
}
}
};
+ /**
+ * A (somewhat degenerate) const_iterator over boolean-valued
+ * attributes. This const_iterator doesn't support anything except
+ * comparison and dereference. It's intended just for the result of
+ * find() on the table.
+ */
class ConstBitIterator {
- const std::pair<const SoftNode, uint64_t>* d_entry;
+ const std::pair<const TNode, uint64_t>* d_entry;
unsigned d_bit;
d_bit(0) {
}
- ConstBitIterator(const std::pair<const SoftNode, uint64_t>& entry, unsigned bit) :
+ ConstBitIterator(const std::pair<const TNode, uint64_t>& entry, unsigned bit) :
d_entry(&entry),
d_bit(bit) {
}
- std::pair<const SoftNode, bool> operator*() {
+ std::pair<const TNode, bool> operator*() {
return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false);
}
public:
- typedef std::pair<uint64_t, SoftNode> key_type;
+ typedef std::pair<uint64_t, TNode> key_type;
typedef bool data_type;
typedef std::pair<const key_type, data_type> value_type;
+ /** an iterator type; see above for limitations */
typedef BitIterator iterator;
+ /** a const_iterator type; see above for limitations */
typedef ConstBitIterator const_iterator;
- BitIterator find(const std::pair<uint64_t, SoftNode>& k) {
+ /**
+ * Find the boolean value in the hash table. Returns something ==
+ * end() if not found.
+ */
+ BitIterator find(const std::pair<uint64_t, TNode>& k) {
super::iterator i = super::find(k.second);
if(i == super::end()) {
return BitIterator();
return BitIterator(*i, k.first);
}
+ /** The "off the end" iterator */
BitIterator end() {
return BitIterator();
}
- ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const {
+ /**
+ * Find the boolean value in the hash table. Returns something ==
+ * end() if not found.
+ */
+ ConstBitIterator find(const std::pair<uint64_t, TNode>& k) const {
super::const_iterator i = super::find(k.second);
if(i == super::end()) {
return ConstBitIterator();
return ConstBitIterator(*i, k.first);
}
+ /** The "off the end" const_iterator */
ConstBitIterator end() const {
return ConstBitIterator();
}
- BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) {
+ /**
+ * Access the hash table using the underlying operator[]. Inserts
+ * the key into the table (associated to default value) if it's not
+ * already there.
+ */
+ BitAccessor operator[](const std::pair<uint64_t, TNode>& k) {
uint64_t& word = super::operator[](k.second);
return BitAccessor(word, k.first);
}
};/* class AttrHash<bool> */
-// ATTRIBUTE PATTERN ===========================================================
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE CLEANUP FUNCTIONS =================================================
+
+namespace attr {
+
+/** Default cleanup for unmanaged Attribute<> */
+template <class T>
+struct AttributeCleanupFcn {
+ inline void cleanup(const T&) {}
+};
+
+/** Default cleanup for ManagedAttribute<> */
+template <class T>
+struct ManagedAttributeCleanupFcn {
+};
+
+/** Specialization for T* */
+template <class T>
+struct ManagedAttributeCleanupFcn<T*> {
+ inline void cleanup(T* p) { delete p; }
+};
+
+/** Specialization for const T* */
+template <class T>
+struct ManagedAttributeCleanupFcn<const T*> {
+ inline void cleanup(const T* p) { delete p; }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE DEFINITION ========================================================
/**
* An "attribute type" structure.
+ *
+ * @param T the tag for the attribute kind.
+ *
+ * @param value_t the underlying value_type for the attribute kind
+ *
+ * @param CleanupFcn Clean-up routine for associated values when the
+ * Node goes away. Useful, e.g., for pointer-valued attributes when
+ * the values are "owned" by the table.
+ *
+ * @param context_dependent whether this attribute kind is
+ * context-dependent
*/
-template <class T, class value_t>
+template <class T,
+ class value_t,
+ class CleanupFcn = attr::AttributeCleanupFcn<value_t>,
+ bool context_dependent = false>
struct Attribute {
- /** the value type for this attribute */
+ /** The value type for this attribute. */
typedef value_t value_type;
- /** cleanup routine when the Node goes away */
- static inline void cleanup(const value_t&) {}
-
+ /** Get the unique ID associated to this attribute. */
static inline uint64_t getId() { return s_id; }
- static inline uint64_t getHashValue() { return s_hashValue; }
+ /**
+ * This attribute does not have a default value: calling
+ * hasAttribute() for a Node that hasn't had this attribute set will
+ * return false, and getAttribute() for the Node will return a
+ * default-constructed value_type.
+ */
static const bool has_default_value = false;
private:
- /** an id */
+ /**
+ * The unique ID associated to this attribute. Assigned statically,
+ * at load time.
+ */
static const uint64_t s_id;
-
- /** an extra hash value (to avoid same-value-type collisions) */
- static const uint64_t s_hashValue;
};
/**
* An "attribute type" structure for boolean flags (special).
*/
-template <class T>
-struct Attribute<T, bool> {
+template <class T, class CleanupFcn, bool context_dependent>
+struct Attribute<T, bool, CleanupFcn, context_dependent> {
- /** the value type for this attribute */
+ /** The value type for this attribute; here, bool. */
typedef bool value_type;
- /** cleanup routine when the Node goes away */
- static inline void cleanup(const bool&) {}
-
+ /** Get the unique ID associated to this attribute. */
static inline uint64_t getId() { return s_id; }
- static inline uint64_t getHashValue() { return s_hashValue; }
+ /**
+ * Such bool-valued attributes ("flags") have a default value: they
+ * are false for all nodes on entry. Calling hasAttribute() for a
+ * Node that hasn't had this attribute set will return true, and
+ * getAttribute() for the Node will return the default_value below.
+ */
static const bool has_default_value = true;
+
+ /**
+ * Default value of the attribute for Nodes without one explicitly
+ * set.
+ */
static const bool default_value = false;
+ /**
+ * Check that the ID is a valid ID for bool-valued attributes. Fail
+ * an assert if not. Otherwise return the id.
+ */
static inline uint64_t checkID(uint64_t id) {
- AlwaysAssert(id <= 63,
- "Too many boolean node attributes registered during initialization !");
+ AlwaysAssert( id <= 63,
+ "Too many boolean node attributes registered "
+ "during initialization !" );
return id;
}
private:
- /** a bit assignment */
+ /** IDs for bool-valued attributes are actually bit assignments. */
static const uint64_t s_id;
-
- /** an extra hash value (to avoid same-value-type collisions) */
- static const uint64_t s_hashValue;
};
-// SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
-
-namespace attr {
- struct VarName {};
- struct Type {};
-
- template <class T>
- struct LastAttributeId {
- static uint64_t s_id;
- };
-
- template <class T>
- uint64_t LastAttributeId<T>::s_id = 0;
-}/* CVC4::expr::attr namespace */
+// FIXME make context-dependent
+template <class T,
+ class value_type>
+struct CDAttribute :
+ public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, true> {};
-typedef Attribute<attr::VarName, std::string> VarNameAttr;
-typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+// FIXME make context-dependent
+template <class T,
+ class value_type,
+ class CleanupFcn = attr::ManagedAttributeCleanupFcn<value_type> >
+struct ManagedAttribute :
+ public Attribute<T, value_type, CleanupFcn, false> {};
// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
-template <class T, class value_t>
-const uint64_t Attribute<T, value_t>::s_id =
- attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
-template <class T, class value_t>
-const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
+namespace attr {
+/**
+ * This is the last-attribute-assigner. IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
template <class T>
-const uint64_t Attribute<T, bool>::s_id =
- Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
+struct LastAttributeId {
+ static uint64_t s_id;
+};
+
+/** Initially zero. */
template <class T>
-const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+uint64_t LastAttributeId<T>::s_id = 0;
-class AttributeManager;
+}/* CVC4::expr::attr namespace */
-template <class T>
-struct getTable {
- //inline AttrHash<KindTableValueMapping<T> >& get(AttributeManager& am);
-};
+/** Assign unique IDs to attributes at load time. */
+template <class T, class value_t, class CleanupFcn, bool context_dependent>
+const uint64_t Attribute<T, value_t, CleanupFcn, context_dependent>::s_id =
+ attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
+
+/**
+ * Assign unique IDs to bool-valued attributes at load time, checking
+ * that they are in range.
+ */
+template <class T, class CleanupFcn, bool context_dependent>
+const uint64_t Attribute<T, bool, CleanupFcn, context_dependent>::s_id =
+ Attribute<T, bool, CleanupFcn, context_dependent>::checkID(attr::LastAttributeId<bool>::s_id++);
// ATTRIBUTE MANAGER ===========================================================
+namespace attr {
+
+/**
+ * A container for the main attribute tables of the system. There's a
+ * one-to-one NodeManager : AttributeManager correspondence.
+ */
class AttributeManager {
- NodeManager* d_nm;
- AttrHash<bool> d_bools;
+ /** Underlying hash table for boolean-valued attributes */
+ AttrHash<bool> d_bools;
+ /** Underlying hash table for integral-valued attributes */
AttrHash<uint64_t> d_ints;
- AttrHash<SoftNode> d_exprs;
+ /** Underlying hash table for node-valued attributes */
+ AttrHash<TNode> d_exprs;
+ /** Underlying hash table for string-valued attributes */
AttrHash<std::string> d_strings;
+ /** Underlying hash table for pointer-valued attributes */
AttrHash<void*> d_ptrs;
+ /**
+ * getTable<> is a helper template that gets the right table from an
+ * AttributeManager given its type.
+ */
template <class T>
friend struct getTable;
public:
- AttributeManager(NodeManager* nm) : d_nm(nm) {}
+ /** Construct an attribute manager. */
+ AttributeManager() {}
+
+ /**
+ * Get a particular attribute on a particular node.
+ *
+ * @param n the node about which to inquire
+ *
+ * @param const AttrKind& the attribute kind to get
+ *
+ * @return the attribute value, if set, or a default-constructed
+ * AttrKind::value_type if not.
+ */
template <class AttrKind>
- typename AttrKind::value_type getAttribute(const Node& n,
+ typename AttrKind::value_type getAttribute(TNode n,
const AttrKind&) const;
+ // Note that there are two, distinct hasAttribute() declarations for
+ // a reason (rather than using a default argument): they permit more
+ // optimized code. The first (without parameter "ret") need never
+ // check whether its parameter is NULL.
+
+ /**
+ * Determine if a particular attribute exists for a particular node.
+ *
+ * @param n the node about which to inquire
+ *
+ * @param const AttrKind& the attribute kind to inquire about
+ *
+ * @return true if the given node has the given attribute
+ */
template <class AttrKind>
- bool hasAttribute(const Node& n,
+ bool hasAttribute(TNode n,
const AttrKind&) const;
+ /**
+ * Determine if a particular attribute exists for a particular node,
+ * and get it if it does.
+ *
+ * @param n the node about which to inquire
+ *
+ * @param const AttrKind& the attribute kind to inquire about
+ *
+ * @param ret a pointer to a return value, set in case the node has
+ * the attribute
+ *
+ * @return true if the given node has the given attribute
+ */
template <class AttrKind>
- bool hasAttribute(const Node& n,
+ bool hasAttribute(TNode n,
const AttrKind&,
- typename AttrKind::value_type*) const;
-
+ typename AttrKind::value_type& ret) const;
+
+ /**
+ * Set a particular attribute on a particular node.
+ *
+ * @param n the node for which to set the attribute
+ *
+ * @param const AttrKind& the attribute kind to set
+ *
+ * @param ret a pointer to a return value, set in case the node has
+ * the attribute
+ *
+ * @return true if the given node has the given attribute
+ */
template <class AttrKind>
- void setAttribute(const Node& n,
+ void setAttribute(TNode n,
const AttrKind&,
const typename AttrKind::value_type& value);
};
+}/* CVC4::expr::attr namespace */
+
// MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
+namespace attr {
+
+/**
+ * The getTable<> template provides (static) access to the
+ * AttributeManager field holding the table.
+ */
+template <class T>
+struct getTable;
+
+/** Access the "d_bools" member of AttributeManager. */
template <>
struct getTable<bool> {
typedef AttrHash<bool> table_type;
}
};
+/** Access the "d_ints" member of AttributeManager. */
template <>
struct getTable<uint64_t> {
typedef AttrHash<uint64_t> table_type;
}
};
+/** Access the "d_exprs" member of AttributeManager. */
template <>
struct getTable<Node> {
- typedef AttrHash<SoftNode> table_type;
+ typedef AttrHash<TNode> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_exprs;
}
}
};
+/** Access the "d_strings" member of AttributeManager. */
template <>
struct getTable<std::string> {
typedef AttrHash<std::string> table_type;
}
};
+/** Access the "d_ptrs" member of AttributeManager. */
template <class T>
-struct getTable<const T*> {
+struct getTable<T*> {
typedef AttrHash<void*> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_ptrs;
}
};
+/** Access the "d_ptrs" member of AttributeManager. */
template <class T>
-struct getTable<T*> {
+struct getTable<const T*> {
typedef AttrHash<void*> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_ptrs;
}
};
+}/* CVC4::expr::attr namespace */
+
// ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
+namespace attr {
+
+// implementation for AttributeManager::getAttribute()
template <class AttrKind>
-typename AttrKind::value_type AttributeManager::getAttribute(const Node& n,
+typename AttrKind::value_type AttributeManager::getAttribute(TNode n,
const AttrKind&) const {
typedef typename AttrKind::value_type value_type;
return mapping::convertBack((*i).second);
}
-/* helper template class for hasAttribute(), specialized based on
+/* Helper template class for hasAttribute(), specialized based on
* whether AttrKind has a "default value" that all Nodes implicitly
* have or not. */
template <bool has_default, class AttrKind>
struct HasAttribute;
+/**
+ * Specialization of HasAttribute<> helper template for AttrKinds
+ * with a default value.
+ */
template <class AttrKind>
struct HasAttribute<true, AttrKind> {
+ /** This implementation is simple; it's always true. */
static inline bool hasAttribute(const AttributeManager* am,
- const Node& n) {
+ TNode n) {
return true;
}
+ /**
+ * This implementation returns the AttrKind's default value if the
+ * Node doesn't have the given attribute.
+ */
static inline bool hasAttribute(const AttributeManager* am,
- const Node& n,
- typename AttrKind::value_type* ret) {
- if(ret != NULL) {
- typedef typename AttrKind::value_type value_type;
- typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type>::table_type table_type;
-
- const table_type& ah = getTable<value_type>::get(*am);
- typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
-
- if(i == ah.end()) {
- *ret = AttrKind::default_value;
- } else {
- *ret = mapping::convertBack((*i).second);
- }
+ TNode n,
+ typename AttrKind::value_type& ret) {
+ typedef typename AttrKind::value_type value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ typedef typename getTable<value_type>::table_type table_type;
+
+ const table_type& ah = getTable<value_type>::get(*am);
+ typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+
+ if(i == ah.end()) {
+ ret = AttrKind::default_value;
+ } else {
+ ret = mapping::convertBack((*i).second);
}
return true;
}
};
+/**
+ * Specialization of HasAttribute<> helper template for AttrKinds
+ * without a default value.
+ */
template <class AttrKind>
struct HasAttribute<false, AttrKind> {
static inline bool hasAttribute(const AttributeManager* am,
- const Node& n) {
+ TNode n) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
typedef typename getTable<value_type>::table_type table_type;
}
static inline bool hasAttribute(const AttributeManager* am,
- const Node& n,
- typename AttrKind::value_type* ret) {
+ TNode n,
+ typename AttrKind::value_type& ret) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
typedef typename getTable<value_type>::table_type table_type;
return false;
}
- if(ret != NULL) {
- *ret = mapping::convertBack((*i).second);
- }
+ ret = mapping::convertBack((*i).second);
return true;
}
};
template <class AttrKind>
-bool AttributeManager::hasAttribute(const Node& n,
+bool AttributeManager::hasAttribute(TNode n,
const AttrKind&) const {
return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n);
}
template <class AttrKind>
-bool AttributeManager::hasAttribute(const Node& n,
+bool AttributeManager::hasAttribute(TNode n,
const AttrKind&,
- typename AttrKind::value_type* ret) const {
+ typename AttrKind::value_type& ret) const {
return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n, ret);
}
template <class AttrKind>
-inline void AttributeManager::setAttribute(const Node& n,
+inline void AttributeManager::setAttribute(TNode n,
const AttrKind&,
const typename AttrKind::value_type& value) {
ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value);
}
+}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
}/* CVC4 namespace */
#include "util/output.h"
+using namespace CVC4::kind;
+
namespace CVC4 {
std::ostream& operator<<(std::ostream& out, const Expr& e) {
LAST_KIND
-};/* enum Kind */
+};/* enum Kind_t */
+
+}/* CVC4::kind namespace */
+
+// import Kind into the "CVC4" namespace but keep the individual kind
+// constants under kind::
+typedef ::CVC4::kind::Kind_t Kind;
inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
- using namespace CVC4;
+ using namespace CVC4::kind;
switch(k) {
#include <iostream>
namespace CVC4 {
+namespace kind {
-enum Kind {
+enum Kind_t {
/* undefined */
UNDEFINED_KIND = -1,
/** Null Kind */
#
# mkkind
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010 The CVC4 Project
#
# The purpose of this script is to create kind.h from a prologue,
# middle, epilogue, and a list of theory kinds.
/********************* -*- C++ -*- */
/** kind.h
**
- ** Copyright 2009, 2010 The AcSys Group, New York University, and as below.
+ ** Copyright 2010 The AcSys Group, New York University, and as below.
**
** This header file automatically generated by:
**
#include "expr/type.h"
#include "util/Assert.h"
+#include "util/output.h"
+
namespace CVC4 {
class Type;
NodeTemplate() : d_nv(&NodeValue::s_null) { }
/**
- * Copy constructor for nodes that can accept the nodes that are reference
- * counted or not.
+ * Conversion between nodes that are reference-counted and those that are
+ * not.
* @param node the node to make copy of
*/
template<bool ref_count_1>
NodeTemplate(const NodeTemplate<ref_count_1>& node);
+ /**
+ * Copy constructor. Note that GCC does NOT recognize an instantiation of
+ * the above template as a copy constructor and problems ensue. So we
+ * provide an explicit one here.
+ * @param node the node to make copy of
+ */
+ NodeTemplate(const NodeTemplate<ref_count>& node);
+
/**
* Assignment operator for nodes, copies the relevant information from node
* to this node.
* @param attKind the kind of the attribute
* @return the value of the attribute
*/
- template<class AttrKind>
+ template <class AttrKind>
inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
+ // Note that there are two, distinct hasAttribute() declarations for
+ // a reason (rather than using a pointer-valued argument with a
+ // default value): they permit more optimized code in the underlying
+ // hasAttribute() implementations.
+
+ /**
+ * Returns true if this node has been associated an attribute of given kind.
+ * Additionaly, if a pointer to the value_kind is give, and the attribute
+ * value has been set for this node, it will be returned.
+ * @param attKind the kind of the attribute
+ * @return true if this node has the requested attribute
+ */
+ template <class AttrKind>
+ inline bool hasAttribute(const AttrKind& attKind) const;
+
/**
* Returns true if this node has been associated an attribute of given kind.
* Additionaly, if a pointer to the value_kind is give, and the attribute
* @param value where to store the value if it exists
* @return true if this node has the requested attribute
*/
- template<class AttrKind>
- inline bool hasAttribute(const AttrKind& attKind, typename AttrKind::value_type* value = NULL) const;
+ template <class AttrKind>
+ inline bool hasAttribute(const AttrKind& attKind, typename AttrKind::value_type& value) const;
+
+ /**
+ * Sets the given attribute of this node to the given value.
+ * @param attKind the kind of the atribute
+ * @param value the value to set the attribute to
+ */
+ template <class AttrKind>
+ inline void setAttribute(const AttrKind& attKind,
+ const typename AttrKind::value_type& value);
/** Iterator allowing for scanning through the children. */
typedef typename NodeValue::iterator<ref_count> iterator;
NodeTemplate uMinusNode() const;
NodeTemplate multNode(const NodeTemplate& right) const;
- /**
- * Sets the given attribute of this node to the given value.
- * @param attKind the kind of the atribute
- * @param value the value to set the attribute to
- */
- template<class AttrKind>
- inline void setAttribute(const AttrKind& attKind,
- const typename AttrKind::value_type& value);
-
private:
/**
*/
void debugPrint();
-
/**
* Indents the given stream a given amount of spaces.
* @param out the stream to indent
template<bool ref_count>
template<class AttrKind>
inline bool NodeTemplate<ref_count>::
- hasAttribute(const AttrKind&, typename AttrKind::value_type* ret) const {
+ hasAttribute(const AttrKind&) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ return NodeManager::currentNM()->hasAttribute(*this, AttrKind());
+ }
+
+template<bool ref_count>
+ template<class AttrKind>
+ inline bool NodeTemplate<ref_count>::
+ hasAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
"Perhaps a public-facing function is missing a NodeManagerScope ?" );
////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:
d_nv->inc();
}
+// the code for these two "conversion/copy constructors" is identical, but
+// apparently we need both. see comment in the class.
template<bool ref_count>
template<bool ref_count_1>
NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count_1>& e) {
d_nv->inc();
}
+template<bool ref_count>
+ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count>& e) {
+ Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
+ d_nv = e.d_nv;
+ if(ref_count)
+ d_nv->inc();
+ }
+
template<bool ref_count>
NodeTemplate<ref_count>::~NodeTemplate() {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
template<bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::eqNode(const NodeTemplate<
ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
}
template<bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::notNode() const {
- return NodeManager::currentNM()->mkNode(NOT, *this);
+ return NodeManager::currentNM()->mkNode(kind::NOT, *this);
}
template<bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::andNode(const NodeTemplate<
ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(AND, *this, right);
+ return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
}
template<bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::orNode(const NodeTemplate<
ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(OR, *this, right);
+ return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
}
template<bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::iteNode(const NodeTemplate<
ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const {
- return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
+ return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
}
template<bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::iffNode(const NodeTemplate<
ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(IFF, *this, right);
+ return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
}
template<bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::impNode(const NodeTemplate<
ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
+ return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
}
template<bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::xorNode(const NodeTemplate<
ref_count>& right) const {
- return NodeManager::currentNM()->mkNode(XOR, *this, right);
+ return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
}
template<bool ref_count>
indent(out, ind);
out << '(';
out << getKind();
- if(getKind() == VARIABLE) {
+ if(getKind() == kind::VARIABLE) {
out << ' ' << getId();
} else if(getNumChildren() >= 1) {
** A builder interface for nodes.
**/
+/* strong dependency; make sure node is included first */
+#include "node.h"
+
#ifndef __CVC4__NODE_BUILDER_H
#define __CVC4__NODE_BUILDER_H
return Node(d_nv->d_children[i]);
}
- void clear(Kind k = UNDEFINED_KIND);
+ void clear(Kind k = kind::UNDEFINED_KIND);
// Compound expression constructors
/*
- NodeBuilder& eqExpr(const Node& right);
+ NodeBuilder& eqExpr(TNode right);
NodeBuilder& notExpr();
- NodeBuilder& andExpr(const Node& right);
- NodeBuilder& orExpr(const Node& right);
- NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart);
- NodeBuilder& iffExpr(const Node& right);
- NodeBuilder& impExpr(const Node& right);
- NodeBuilder& xorExpr(const Node& right);
+ NodeBuilder& andExpr(TNode right);
+ NodeBuilder& orExpr(TNode right);
+ NodeBuilder& iteExpr(TNode thenpart, TNode elsepart);
+ NodeBuilder& iffExpr(TNode right);
+ NodeBuilder& impExpr(TNode right);
+ NodeBuilder& xorExpr(TNode right);
*/
/* TODO design: these modify NodeBuilder ?? */
/*
NodeBuilder& operator!() { return notExpr(); }
- NodeBuilder& operator&&(const Node& right) { return andExpr(right); }
- NodeBuilder& operator||(const Node& right) { return orExpr(right); }
+ NodeBuilder& operator&&(TNode right) { return andExpr(right); }
+ NodeBuilder& operator||(TNode right) { return orExpr(right); }
*/
/*
- NodeBuilder& operator&&=(const Node& right) { return andExpr(right); }
- NodeBuilder& operator||=(const Node& right) { return orExpr(right); }
+ NodeBuilder& operator&&=(TNode right) { return andExpr(right); }
+ NodeBuilder& operator||=(TNode right) { return orExpr(right); }
*/
// "Stream" expression constructor syntax
NodeBuilder& operator<<(const Kind& k) {
Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
- Assert(d_nv->getKind() == UNDEFINED_KIND);
+ Assert(d_nv->getKind() == kind::UNDEFINED_KIND);
d_nv->d_kind = k;
return *this;
}
- NodeBuilder& operator<<(const Node& n) {
+ NodeBuilder& operator<<(TNode n) {
Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
return append(n);
}
return append(children.begin(), children.end());
}
- NodeBuilder& append(const Node& n) {
+ NodeBuilder& append(TNode n) {
Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
Debug("prop") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl;
allocateEvIfNecessaryForAppend();
d_nv(&d_inlineNv),
d_inlineNv(0),
d_childrenStorage() {
- d_inlineNv.d_kind = UNDEFINED_KIND;
+ d_inlineNv.d_kind = NodeValue::kindToDKind(kind::UNDEFINED_KIND);
}
template <unsigned nchild_thresh>
template <unsigned nchild_thresh>
NodeBuilder<nchild_thresh>::operator Node() {// not const
Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
- Assert(d_nv->getKind() != UNDEFINED_KIND,
+ Assert(d_nv->getKind() != kind::UNDEFINED_KIND,
"Can't make an expression of an undefined kind!");
- if(d_nv->d_kind == VARIABLE) {
+ if(d_nv->d_kind == kind::VARIABLE) {
Assert(d_nv->d_nchildren == 0);
NodeValue *nv = (NodeValue*)
std::malloc(sizeof(NodeValue) +
( sizeof(NodeValue*) * d_inlineNv.d_nchildren ));
nv->d_nchildren = 0;
- nv->d_kind = VARIABLE;
+ nv->d_kind = kind::VARIABLE;
nv->d_id = NodeValue::next_id++;// FIXME multithreading
nv->d_rc = 0;
d_used = true;
** Expression manager implementation.
**/
-#include "node_builder.h"
#include "node_manager.h"
-#include "expr/node.h"
-#include "expr/attribute.h"
-#include "util/output.h"
using namespace std;
using namespace CVC4::expr;
NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
- if (find == d_nodeValueSet.end()) {
+ if(find == d_nodeValueSet.end()) {
return NULL;
} else {
return *find;
}
}
-void NodeManager::poolInsert(NodeValue* nv) {
- Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in"
- "the pool!");
- d_nodeValueSet.insert(nv);
-}
-
-// general expression-builders
-
-Node NodeManager::mkNode(Kind kind) {
- return NodeBuilder<>(this, kind);
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1) {
- return NodeBuilder<>(this, kind) << child1;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) {
- return NodeBuilder<>(this, kind) << child1 << child2;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
- return NodeBuilder<>(this, kind) << child1 << child2 << child3;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
- return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
- return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
-}
-
-// N-ary version
-Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
- return NodeBuilder<>(this, kind).append(children);
-}
-
-Node NodeManager::mkVar(const Type* type, const std::string& name) {
- Node n = mkVar(type);
- n.setAttribute(VarNameAttr(), name);
- return n;
-}
-
-Node NodeManager::mkVar(const Type* type) {
- Node n = NodeBuilder<>(this, VARIABLE);
- n.setAttribute(TypeAttr(), type);
- return n;
-}
-
-Node NodeManager::mkVar() {
- return NodeBuilder<>(this, VARIABLE);
-}
-
}/* CVC4 namespace */
class Type;
+namespace expr {
+namespace attr {
+
+struct VarName {};
+struct Type {};
+
+}/* CVC4::expr::attr namespace */
+
+typedef Attribute<attr::VarName, std::string> VarNameAttr;
+typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+
+}/* CVC4::expr namespace */
+
class NodeManager {
static __thread NodeManager* s_current;
typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
NodeValueSet d_nodeValueSet;
- expr::AttributeManager d_attrManager;
+ expr::attr::AttributeManager d_attrManager;
NodeValue* poolLookup(NodeValue* nv) const;
void poolInsert(NodeValue* nv);
public:
- NodeManager() : d_attrManager(this) {
+ NodeManager() {
poolInsert( &NodeValue::s_null );
}
// general expression-builders
Node mkNode(Kind kind);
- Node mkNode(Kind kind, const Node& child1);
- Node mkNode(Kind kind, const Node& child1, const Node& child2);
- Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3);
- Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
- Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
+ Node mkNode(Kind kind, TNode child1);
+ Node mkNode(Kind kind, TNode child1, TNode child2);
+ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
+ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4);
+ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5);
// N-ary version
Node mkNode(Kind kind, const std::vector<Node>& children);
Node mkVar();
template <class AttrKind>
- inline typename AttrKind::value_type getAttribute(const Node& n,
+ inline typename AttrKind::value_type getAttribute(TNode n,
const AttrKind&) const;
+ // Note that there are two, distinct hasAttribute() declarations for
+ // a reason (rather than using a pointer-valued argument with a
+ // default value): they permit more optimized code in the underlying
+ // hasAttribute() implementations.
+
+ template <class AttrKind>
+ inline bool hasAttribute(TNode n,
+ const AttrKind&) const;
+
template <class AttrKind>
- inline bool hasAttribute(const Node& n,
+ inline bool hasAttribute(TNode n,
const AttrKind&,
- typename AttrKind::value_type* = NULL) const;
+ typename AttrKind::value_type&) const;
template <class AttrKind>
- inline void setAttribute(const Node& n,
+ inline void setAttribute(TNode n,
const AttrKind&,
const typename AttrKind::value_type& value);
- inline const Type* getType(const Node& n);
+ inline const Type* getType(TNode n);
};
class NodeManagerScope {
};
template <class AttrKind>
-inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n,
+inline typename AttrKind::value_type NodeManager::getAttribute(TNode n,
const AttrKind&) const {
return d_attrManager.getAttribute(n, AttrKind());
}
template <class AttrKind>
-inline bool NodeManager::hasAttribute(const Node& n,
+inline bool NodeManager::hasAttribute(TNode n,
+ const AttrKind&) const {
+ return d_attrManager.hasAttribute(n, AttrKind());
+}
+
+template <class AttrKind>
+inline bool NodeManager::hasAttribute(TNode n,
const AttrKind&,
- typename AttrKind::value_type* ret) const {
+ typename AttrKind::value_type& ret) const {
return d_attrManager.hasAttribute(n, AttrKind(), ret);
}
template <class AttrKind>
-inline void NodeManager::setAttribute(const Node& n,
+inline void NodeManager::setAttribute(TNode n,
const AttrKind&,
const typename AttrKind::value_type& value) {
d_attrManager.setAttribute(n, AttrKind(), value);
}
-inline const Type* NodeManager::getType(const Node& n) {
+inline const Type* NodeManager::getType(TNode n) {
return getAttribute(n,CVC4::expr::TypeAttr());
}
+inline void NodeManager::poolInsert(NodeValue* nv) {
+ Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in"
+ "the pool!");
+ d_nodeValueSet.insert(nv);
+}
+
+}/* CVC4 namespace */
+
+#include "expr/node_builder.h"
+
+namespace CVC4 {
+
+// general expression-builders
+
+inline Node NodeManager::mkNode(Kind kind) {
+ return NodeBuilder<>(this, kind);
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1) {
+ return NodeBuilder<>(this, kind) << child1;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
+ return NodeBuilder<>(this, kind) << child1 << child2;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) {
+ return NodeBuilder<>(this, kind) << child1 << child2 << child3;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) {
+ return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) {
+ return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
+}
+
+// N-ary version
+inline Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
+ return NodeBuilder<>(this, kind).append(children);
+}
+
+inline Node NodeManager::mkVar(const Type* type, const std::string& name) {
+ Node n = mkVar(type);
+ n.setAttribute(expr::VarNameAttr(), name);
+ return n;
+}
+
+inline Node NodeManager::mkVar(const Type* type) {
+ Node n = NodeBuilder<>(this, kind::VARIABLE);
+ n.setAttribute(expr::TypeAttr(), type);
+ return n;
+}
+
+inline Node NodeManager::mkVar() {
+ return NodeBuilder<>(this, kind::VARIABLE);
+}
+
}/* CVC4 namespace */
#endif /* __CVC4__EXPR_MANAGER_H */
NodeValue NodeValue::s_null;
-NodeValue::NodeValue() :
- d_id(0),
- d_rc(MAX_RC),
- d_kind(NULL_EXPR),
- d_nchildren(0) {
-}
-
-NodeValue::NodeValue(int) :
- d_id(0),
- d_rc(0),
- d_kind(kindToDKind(UNDEFINED_KIND)),
- d_nchildren(0) {
-}
-
-NodeValue::~NodeValue() {
- for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
- (*i)->dec();
- }
-}
-
-void NodeValue::inc() {
- // FIXME multithreading
- if(EXPECT_TRUE( d_rc < MAX_RC )) {
- ++d_rc;
- }
-}
-
-void NodeValue::dec() {
- // FIXME multithreading
- if(EXPECT_TRUE( d_rc < MAX_RC )) {
- --d_rc;
- if(EXPECT_FALSE( d_rc == 0 )) {
- // FIXME gc
- }
- }
-}
-
-NodeValue::nv_iterator NodeValue::nv_begin() {
- return d_children;
-}
-
-NodeValue::nv_iterator NodeValue::nv_end() {
- return d_children + d_nchildren;
-}
-
-NodeValue::const_nv_iterator NodeValue::nv_begin() const {
- return d_children;
-}
-
-NodeValue::const_nv_iterator NodeValue::nv_end() const {
- return d_children + d_nchildren;
-}
-
string NodeValue::toString() const {
stringstream ss;
toStream(ss);
void NodeValue::toStream(std::ostream& out) const {
out << "(" << Kind(d_kind);
- if(d_kind == VARIABLE) {
+ if(d_kind == kind::VARIABLE) {
Node n(this);
string s;
- if(n.hasAttribute(VarNameAttr(), &s)) {
+ if(n.hasAttribute(VarNameAttr(), s)) {
out << ":" << s;
} else {
out << ":" << this;
return ((unsigned) k) & kindMask;
}
static inline Kind dKindToKind(unsigned d) {
- return (d == kindMask) ? UNDEFINED_KIND : Kind(d);
+ return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
}
};
+inline NodeValue::NodeValue() :
+ d_id(0),
+ d_rc(MAX_RC),
+ d_kind(kind::NULL_EXPR),
+ d_nchildren(0) {
+}
+
+inline NodeValue::NodeValue(int) :
+ d_id(0),
+ d_rc(0),
+ d_kind(kindToDKind(kind::UNDEFINED_KIND)),
+ d_nchildren(0) {
+}
+
+inline NodeValue::~NodeValue() {
+ for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
+ (*i)->dec();
+ }
+}
+
+inline void NodeValue::inc() {
+ // FIXME multithreading
+ if(EXPECT_TRUE( d_rc < MAX_RC )) {
+ ++d_rc;
+ }
+}
+
+inline void NodeValue::dec() {
+ // FIXME multithreading
+ if(EXPECT_TRUE( d_rc < MAX_RC )) {
+ --d_rc;
+ if(EXPECT_FALSE( d_rc == 0 )) {
+ // FIXME gc
+ }
+ }
+}
+
+inline NodeValue::nv_iterator NodeValue::nv_begin() {
+ return d_children;
+}
+
+inline NodeValue::nv_iterator NodeValue::nv_end() {
+ return d_children + d_nchildren;
+}
+
+inline NodeValue::const_nv_iterator NodeValue::nv_begin() const {
+ return d_children;
+}
+
+inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
+ return d_children + d_nchildren;
+}
+
}/* CVC4::expr namespace */
}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/** soft_node.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Encapsulation of a pointer to node information that is explicitly
- ** NOT reference-counted. These "smart pointers" do NOT keep live
- ** the NodeValue object to which they refer.
- **/
-
-#ifndef __CVC4__SOFT_NODE_H
-#define __CVC4__SOFT_NODE_H
-
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace expr {
-
-/**
- * For now, treat SoftNodes as regular Nodes. We'll address this
- * later.
- */
-typedef CVC4::Node SoftNode;
-typedef CVC4::Node TNode;
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SOFT_NODE_H */
static Result lastResult;
static struct Options options;
+int runCvc4(int argc, char *argv[]);
void doCommand(SmtEngine&, Command*);
+/**
+ * CVC4's main() routine is just an exception-safe wrapper around CVC4.
+ * Please don't construct anything here. Even if the constructor is
+ * inside the try { }, an exception during destruction can cause
+ * problems. That's why main() wraps runCvc4() in the first place.
+ * Put everything in runCvc4().
+ */
int main(int argc, char *argv[]) {
-
try {
-
- // Initialize the signal handlers
- cvc4_init();
-
- // Parse the options
- int firstArgIndex = parseOptions(argc, argv, &options);
-
- // If in competition mode, set output stream option to flush immediately
- if(options.smtcomp_mode) {
- cout << unitbuf;
- }
-
- // We only accept one input file
- if(argc > firstArgIndex + 1) {
- throw Exception("Too many input files specified.");
- }
-
- // Create the expression manager
- ExprManager exprMgr;
-
- // Create the SmtEngine
- SmtEngine smt(&exprMgr, &options);
-
- // If no file supplied we read from standard input
- bool inputFromStdin = firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
-
- // Auto-detect input language by filename extension
- if(!inputFromStdin && options.lang == Parser::LANG_AUTO) {
- const char* filename = argv[firstArgIndex];
- unsigned len = strlen(filename);
- if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
- options.lang = Parser::LANG_SMTLIB;
- } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
- || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
- options.lang = Parser::LANG_CVC4;
- }
- }
-
- // Determine which messages to show based on smtcomp_mode and verbosity
- if(options.smtcomp_mode) {
- Debug.setStream(CVC4::null_os);
- Trace.setStream(CVC4::null_os);
- Notice.setStream(CVC4::null_os);
- Chat.setStream(CVC4::null_os);
- Message.setStream(CVC4::null_os);
- Warning.setStream(CVC4::null_os);
- } else {
- if(options.verbosity < 2) {
- Chat.setStream(CVC4::null_os);
- }
- if(options.verbosity < 1) {
- Notice.setStream(CVC4::null_os);
- }
- if(options.verbosity < 0) {
- Message.setStream(CVC4::null_os);
- Warning.setStream(CVC4::null_os);
- }
- }
-
- // Create the parser
- Parser* parser;
- if(inputFromStdin) {
- parser = Parser::getNewParser(&exprMgr, options.lang, cin);
- } else {
- parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]);
- }
-
- if(!options.semanticChecks) {
- parser->disableChecks();
- }
-
- // Parse and execute commands until we are done
- Command* cmd;
- while((cmd = parser->parseNextCommand())) {
- if( !options.parseOnly ) {
- doCommand(smt, cmd);
- }
- delete cmd;
- }
-
- // Remove the parser
- delete parser;
-
+ return runCvc4(argc, argv);
} catch(OptionException& e) {
if(options.smtcomp_mode) {
cout << "unknown" << endl;
cerr << "CVC4 threw an exception of unknown type." << endl;
abort();
}
+}
+
+int runCvc4(int argc, char *argv[]) {
+
+ // Initialize the signal handlers
+ cvc4_init();
+
+ // Parse the options
+ int firstArgIndex = parseOptions(argc, argv, &options);
+
+ // If in competition mode, set output stream option to flush immediately
+ if(options.smtcomp_mode) {
+ cout << unitbuf;
+ }
+
+ // We only accept one input file
+ if(argc > firstArgIndex + 1) {
+ throw Exception("Too many input files specified.");
+ }
+
+ // Create the expression manager
+ ExprManager exprMgr;
+
+ // Create the SmtEngine
+ SmtEngine smt(&exprMgr, &options);
+
+ // If no file supplied we read from standard input
+ bool inputFromStdin = firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
+
+ // Auto-detect input language by filename extension
+ if(!inputFromStdin && options.lang == Parser::LANG_AUTO) {
+ const char* filename = argv[firstArgIndex];
+ unsigned len = strlen(filename);
+ if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
+ options.lang = Parser::LANG_SMTLIB;
+ } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
+ || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
+ options.lang = Parser::LANG_CVC4;
+ }
+ }
+
+ // Determine which messages to show based on smtcomp_mode and verbosity
+ if(options.smtcomp_mode) {
+ Debug.setStream(CVC4::null_os);
+ Trace.setStream(CVC4::null_os);
+ Notice.setStream(CVC4::null_os);
+ Chat.setStream(CVC4::null_os);
+ Message.setStream(CVC4::null_os);
+ Warning.setStream(CVC4::null_os);
+ } else {
+ if(options.verbosity < 2) {
+ Chat.setStream(CVC4::null_os);
+ }
+ if(options.verbosity < 1) {
+ Notice.setStream(CVC4::null_os);
+ }
+ if(options.verbosity < 0) {
+ Message.setStream(CVC4::null_os);
+ Warning.setStream(CVC4::null_os);
+ }
+ }
+
+ // Create the parser
+ Parser* parser;
+ if(inputFromStdin) {
+ parser = Parser::getNewParser(&exprMgr, options.lang, cin);
+ } else {
+ parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]);
+ }
+
+ if(!options.semanticChecks) {
+ parser->disableChecks();
+ }
+
+ // Parse and execute commands until we are done
+ Command* cmd;
+ while((cmd = parser->parseNextCommand())) {
+ if( !options.parseOnly ) {
+ doCommand(smt, cmd);
+ }
+ delete cmd;
+ }
+
+ // Remove the parser
+ delete parser;
switch(lastResult.asSatisfiabilityResult().isSAT()) {
using namespace std;
using namespace CVC4;
using namespace CVC4::parser;
+using namespace CVC4::kind;
namespace CVC4 {
namespace parser {
}
: f = impliesFormula
( IFF e = iffFormula
- { f = mkExpr(CVC4::IFF, f, e); }
+ { f = mkExpr(CVC4::kind::IFF, f, e); }
)?
;
}
: f = orFormula
( IMPLIES e = impliesFormula
- { f = mkExpr(CVC4::IMPLIES, f, e); }
+ { f = mkExpr(CVC4::kind::IMPLIES, f, e); }
)?
;
: e = xorFormula { exprs.push_back(e); }
( OR e = xorFormula { exprs.push_back(e); } )*
{
- f = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
+ f = (exprs.size() > 1 ? mkExpr(CVC4::kind::OR, exprs) : exprs[0]);
}
;
}
: f = andFormula
( XOR e = andFormula
- { f = mkExpr(CVC4::XOR,f, e); }
+ { f = mkExpr(CVC4::kind::XOR,f, e); }
)*
;
: e = notFormula { exprs.push_back(e); }
( AND e = notFormula { exprs.push_back(e); } )*
{
- f = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
+ f = (exprs.size() > 1 ? mkExpr(CVC4::kind::AND, exprs) : exprs[0]);
}
;
}
: /* negation */
NOT f = notFormula
- { f = mkExpr(CVC4::NOT, f); }
+ { f = mkExpr(CVC4::kind::NOT, f); }
| /* a boolean atom */
f = predFormula
;
: { Expr e; }
f = term
(EQUAL e = term
- { f = mkExpr(CVC4::EQUAL, f, e); }
+ { f = mkExpr(CVC4::kind::EQUAL, f, e); }
)?
; // TODO: lt, gt, etc.
LPAREN formulaList[args] RPAREN
// TODO: check arity
- { t = mkExpr(CVC4::APPLY, args); }
+ { t = mkExpr(CVC4::kind::APPLY, args); }
| /* if-then-else */
t = iteTerm
THEN iteThen = formula
iteElse = iteElseTerm
ENDIF
- { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); }
+ { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); }
;
/**
| ELSEIF iteCondition = formula
THEN iteThen = formula
iteElse = iteElseTerm
- { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); }
+ { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); }
;
/**
Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
string filename) {
istream* input = new ifstream(filename.c_str());
+ if(!*input) {
+ throw Exception("file does not exist or is unreadable: " + filename);
+ }
return getNewParser(em, lang, input, filename, true);
}
annotatedFormula returns [CVC4::Expr formula]
{
Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
- Kind kind = UNDEFINED_KIND;
+ Kind kind = CVC4::kind::UNDEFINED_KIND;
vector<Expr> args;
}
: /* a built-in operator application */
{ args.push_back(f); }
annotatedFormulas[args] RPAREN
// TODO: check arity
- { formula = mkExpr(CVC4::APPLY,args); }
+ { formula = mkExpr(CVC4::kind::APPLY,args); }
| /* An ite expression */
LPAREN (ITE | IF_THEN_ELSE)
trueExpr = annotatedFormula
falseExpr = annotatedFormula
RPAREN
- { formula = mkExpr(CVC4::ITE, test, trueExpr, falseExpr); }
+ { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); }
| /* a variable */
{ std::string name; }
{
Debug("parser") << "builtin: " << LT(1)->getText() << endl;
}
- : NOT { kind = CVC4::NOT; }
- | IMPLIES { kind = CVC4::IMPLIES; }
- | AND { kind = CVC4::AND; }
- | OR { kind = CVC4::OR; }
- | XOR { kind = CVC4::XOR; }
- | IFF { kind = CVC4::IFF; }
- | EQUAL { kind = CVC4::EQUAL; }
+ : NOT { kind = CVC4::kind::NOT; }
+ | IMPLIES { kind = CVC4::kind::IMPLIES; }
+ | AND { kind = CVC4::kind::AND; }
+ | OR { kind = CVC4::kind::OR; }
+ | XOR { kind = CVC4::kind::XOR; }
+ | IFF { kind = CVC4::kind::IFF; }
+ | EQUAL { kind = CVC4::kind::EQUAL; }
/* TODO: lt, gt, plus, minus, etc. */
;
#include <queue>
using namespace std;
+using namespace CVC4::kind;
namespace CVC4 {
namespace prop {
delete d_satSolver;
}
-void PropEngine::assertFormula(const Node& node) {
+void PropEngine::assertFormula(TNode node) {
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "assertFormula(" << node << ")" << endl;
// Assert as non-removable
d_cnfStream->convertAndAssert(node);
}
-void PropEngine::assertLemma(const Node& node) {
+void PropEngine::assertLemma(TNode node) {
Debug("prop") << "assertFormula(" << node << ")" << endl;
// Assert as removable
d_cnfStream->convertAndAssert(node);
* The formula is asserted permanently for the current context.
* @param node the formula to assert
*/
- void assertFormula(const Node& node);
+ void assertFormula(TNode node);
/**
* Converts the given formula to CNF and assert the CNF to the sat solver.
* The formula can be removed by the sat solver.
* @param node the formula to assert
*/
- void assertLemma(const Node& node);
+ void assertLemma(TNode node);
/**
* Checks the current context for satisfiability.
#include "prop/prop_engine.h"
using namespace CVC4::prop;
+using CVC4::context::Context;
namespace CVC4 {
SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
+ d_ctxt(new Context),
d_exprManager(em),
d_nodeManager(em->getNodeManager()),
- d_options(opts)
-{
- d_decisionEngine = new DecisionEngine();
- d_theoryEngine = new TheoryEngine(this);
+ d_options(opts) {
+ NodeManagerScope nms(d_nodeManager);
+ d_decisionEngine = new DecisionEngine;
+ d_theoryEngine = new TheoryEngine(this, d_ctxt);
d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine);
}
delete d_propEngine;
delete d_theoryEngine;
delete d_decisionEngine;
+ delete d_ctxt;
}
void SmtEngine::doCommand(Command* c) {
c->invoke(this);
}
-Node SmtEngine::preprocess(const Node& e) {
+Node SmtEngine::preprocess(TNode e) {
return e;
}
return Result(Result::VALIDITY_UNKNOWN);
}
-void SmtEngine::addFormula(const Node& e) {
+void SmtEngine::addFormula(TNode e) {
Debug("smt") << "push_back assertion " << e << std::endl;
d_propEngine->assertFormula(preprocess(e));
}
private:
+ /** Our Context */
+ CVC4::context::Context* d_ctxt;
+
/** Our expression manager */
ExprManager* d_exprManager;
* passes over the Node. TODO: may need to specify a LEVEL of
* preprocessing (certain contexts need more/less ?).
*/
- Node preprocess(const Node& node);
+ Node preprocess(TNode node);
/**
* Adds a formula to the current context.
*/
- void addFormula(const Node& node);
+ void addFormula(TNode node);
/**
* Full check of consistency in current context. Returns true iff
noinst_LTLIBRARIES = libtheory.la
libtheory_la_SOURCES = \
+ @srcdir@/theoryof_table.h \
theory_engine.h \
theory_engine.cpp \
theory.h \
theory.cpp
libtheory_la_LIBADD = \
- @builddir@/bool/libbool.la
- @builddir@/uf/libuf.la
- @builddir@/uf/libarith.la
+ @builddir@/booleans/libbooleans.la \
+ @builddir@/uf/libuf.la \
+ @builddir@/arith/libarith.la
-SUBDIRS = bool uf arith
+EXTRA_DIST = \
+ @srcdir@/theoryof_table.h \
+ theoryof_table_prologue.h \
+ theoryof_table_middle.h \
+ theoryof_table_epilogue.h
+
+@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_prologue.h theoryof_table_middle.h theoryof_table_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+ chmod +x @srcdir@/mktheoryof
+ (@srcdir@/mktheoryof \
+ @srcdir@/theoryof_table_prologue.h \
+ @srcdir@/theoryof_table_middle.h \
+ @srcdir@/theoryof_table_epilogue.h \
+ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+ > @srcdir@/theoryof_table.h) || (rm -f @srcdir@/theoryof_table.h && exit 1)
+
+BUILT_SOURCES = @srcdir@/theoryof_table.h
+dist-hook: @srcdir@/theoryof_table.h
+MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h
+
+SUBDIRS = booleans uf arith
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/arith
+
+include $(topdir)/Makefile.subdir
noinst_LTLIBRARIES = libarith.la
-libarith_la_SOURCES =
+libarith_la_SOURCES = \
+ theory_def.h \
+ theory_arith.h
EXTRA_DIST = kinds
--- /dev/null
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class TheoryArith : public TheoryImpl<TheoryArith> {
+public:
+ TheoryArith(context::Context* c, OutputChannel& out) :
+ TheoryImpl<TheoryArith>(c, out) {
+ }
+
+ void preRegisterTerm(TNode n) { Unimplemented(); }
+ void registerTerm(TNode n) { Unimplemented(); }
+ void check(Effort e) { Unimplemented(); }
+ void propagate(Effort e) { Unimplemented(); }
+ void explain(TNode n, Effort e) { Unimplemented(); }
+};
+
+}
+}
+}
+
--- /dev/null
+#include "theory/arith/theory_arith.h"
+
+namespace CVC4 {
+ namespace theory {
+ namespace arith {
+ typedef TheoryArith TheoryARITH;
+ }
+ }
+}
+++ /dev/null
-AM_CPPFLAGS = \
- -D__BUILDING_CVC4LIB \
- -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
-
-noinst_LTLIBRARIES = libbool.la
-
-libbool_la_SOURCES =
-
-EXTRA_DIST = kinds
+++ /dev/null
-FALSE
-TRUE
-NOT
-AND
-IFF
-IMPLIES
-OR
-XOR
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/bool
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -fvisibility=hidden
+
+noinst_LTLIBRARIES = libbooleans.la
+
+libbooleans_la_SOURCES = \
+ theory_def.h \
+ theory_bool.h
+
+EXTRA_DIST = kinds
--- /dev/null
+FALSE
+TRUE
+NOT
+AND
+IFF
+IMPLIES
+OR
+XOR
--- /dev/null
+#include "theory/theory.h"
+#include "context/context.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+class TheoryBool : public TheoryImpl<TheoryBool> {
+public:
+ TheoryBool(context::Context* c, OutputChannel& out) :
+ TheoryImpl<TheoryBool>(c, out) {
+ }
+
+ void preRegisterTerm(TNode n) { Unimplemented(); }
+ void registerTerm(TNode n) { Unimplemented(); }
+ void check(Effort e) { Unimplemented(); }
+ void propagate(Effort e) { Unimplemented(); }
+ void explain(TNode n, Effort e) { Unimplemented(); }
+};
+
+}
+}
+}
+
--- /dev/null
+#include "theory/booleans/theory_bool.h"
+
+namespace CVC4 {
+ namespace theory {
+ namespace booleans {
+ typedef TheoryBool TheoryBOOLEANS;
+ }
+ }
+}
--- /dev/null
+#!/bin/bash
+#
+# mktheoryof
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010 The CVC4 Project
+#
+# The purpose of this script is to create theoryof_table.h from a
+# prologue, epilogue, and a list of theory kinds.
+#
+# Invocation:
+#
+# mktheoryof prologue-file epilogue-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+cat <<EOF
+/********************* -*- C++ -*- */
+/** theoryof_table.h
+ **
+ ** Copyright 2010 The AcSys Group, New York University, and as below.
+ **
+ ** This header file automatically generated by:
+ **
+ ** $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+EOF
+
+prologue=$1; shift
+middle=$1; shift
+epilogue=$1; shift
+
+registers=
+cat "$prologue"
+while [ $# -gt 0 ]; do
+ b=$(basename $(dirname "$1"))
+ B=$(echo "$b" | tr 'a-z' 'A-Z')
+ echo "#include \"theory/$b/theory_def.h\""
+ registers="$registers
+ /* from $b */
+ void registerTheory(::CVC4::theory::$b::Theory$B* th) {
+"
+ for r in `cat "$1"`; do
+ registers="$registers d_table[::CVC4::kind::$r] = th;
+"
+ done
+ registers="$registers }
+"
+ shift
+done
+echo
+cat "$middle"
+echo "$registers"
+cat "$epilogue"
* Generic "theory output channel" interface.
*/
class OutputChannel {
+ /** Disallow copying: private constructor */
+ OutputChannel(const OutputChannel&);
+
+ /** Disallow assignment: private operator=() */
+ OutputChannel& operator=(const OutputChannel&);
+
public:
+ /**
+ * Construct an OutputChannel.
+ */
+ OutputChannel() {
+ }
+
/**
* Destructs an OutputChannel. This implementation does nothing,
* but we need a virtual destructor for safety in case subclasses
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted.
*/
- virtual void safePoint() throw(Interrupted&) {
+ virtual void safePoint() throw(Interrupted) {
}
/**
* Indicate a theory conflict has arisen.
*
- * @param n - a conflict at the current decision level
+ * @param n - a conflict at the current decision level. This should
+ * be an OR-kinded node of literals that are false in the current
+ * assignment.
+ *
* @param safe - whether it is safe to be interrupted
*/
- virtual void conflict(Node n, bool safe = false) throw(Interrupted&) = 0;
+ virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0;
/**
* Propagate a theory literal.
*
- * @param n - a theory consequence at the current decision level
+ * @param n - a theory consequence at the current decision level.
+ *
* @param safe - whether it is safe to be interrupted
*/
- virtual void propagate(Node n, bool safe = false) throw(Interrupted&) = 0;
+ virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0;
/**
* Tell the core that a valid theory lemma at decision level 0 has
* @param n - a theory lemma valid at decision level 0
* @param safe - whether it is safe to be interrupted
*/
- virtual void lemma(Node n, bool safe = false) throw(Interrupted&) = 0;
-
-};/* class OutputChannel */
-
-/**
- * Generic "theory output channel" interface for explanations.
- */
-class ExplainOutputChannel {
-public:
-
- /**
- * Destructs an ExplainOutputChannel. This implementation does
- * nothing, but we need a virtual destructor for safety in case
- * subclasses have a destructor.
- */
- virtual ~ExplainOutputChannel() {
- }
-
- /**
- * With safePoint(), the theory signals that it is at a safe point
- * and can be interrupted. The default implementation never
- * interrupts.
- */
- virtual void safePoint() throw(Interrupted&) {
- }
+ virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0;
/**
* Provide an explanation in response to an explanation request.
* @param n - an explanation
* @param safe - whether it is safe to be interrupted
*/
- virtual void explanation(Node n, bool safe = false) throw(Interrupted&) = 0;
-};/* class ExplainOutputChannel */
+ virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0;
+
+};/* class OutputChannel */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
**/
#include "theory/theory.h"
+#include "util/Assert.h"
-namespace CVC4 {
-namespace theory {
-
-bool Theory::done() {
- return d_nextAssertion >= d_assertions.size();
-}
+#include <vector>
+using namespace std;
-Node Theory::get() {
- Node n = d_assertions[d_nextAssertion];
- d_nextAssertion = d_nextAssertion + 1;
- return n;
-}
-
-void Theory::assertFact(const Node& n){
- d_assertions.push_back(n);
-}
+namespace CVC4 {
+namespace theory {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#define __CVC4__THEORY__THEORY_H
#include "expr/node.h"
+#include "expr/attribute.h"
#include "theory/output_channel.h"
#include "context/context.h"
+#include <queue>
+#include <vector>
+
+#include <typeinfo>
+
namespace CVC4 {
namespace theory {
+template <class T>
+class TheoryImpl;
+
/**
* Base class for T-solvers. Abstract DPLL(T).
+ *
+ * This is essentially an interface class. The TheoryEngine has
+ * pointers to Theory. But each individual theory implementation T
+ * should inherit from TheoryImpl<T>, which specializes a few things
+ * for that theory.
*/
class Theory {
+private:
+
+ template <class T>
+ friend class TheoryImpl;
+
+ /**
+ * Construct a Theory.
+ */
+ Theory(context::Context* ctxt, OutputChannel& out) throw() :
+ d_context(ctxt),
+ d_out(&out) {
+ }
+
+ /**
+ * Disallow default construction.
+ */
+ Theory();
+
+protected:
+
+ /**
+ * The output channel for the Theory.
+ */
+ context::Context* d_context;
+
+ /**
+ * The output channel for the Theory.
+ */
+ OutputChannel* d_out;
+
+ /**
+ * The assertFact() queue.
+ */
+ // FIXME CD: on backjump we clear the facts IFF the queue gets
+ // emptied on every DL. In general I guess we need a CDQueue<>?
+ // Perhaps one that asserts it's empty at each push?
+ std::queue<Node> d_facts;
/**
* Return whether a node is shared or not. Used by setup().
*/
- bool isShared(const Node& n);
+ bool isShared(TNode n) throw();
+
+ /**
+ * Returns true if the assertFact queue is empty
+ */
+ bool done() throw() {
+ return d_facts.empty();
+ }
public:
+ /**
+ * Destructs a Theory. This implementation does nothing, but we
+ * need a virtual destructor for safety in case subclasses have a
+ * destructor.
+ */
+ virtual ~Theory() {
+ }
+
/**
* Subclasses of Theory may add additional efforts. DO NOT CHECK
* equality with one of these values (e.g. if STANDARD xxx) but
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
/**
- * Construct a Theory.
+ * Set the output channel associated to this theory.
*/
- Theory(context::Context* c) : d_assertions(c), d_nextAssertion(c, 0){}
+ void setOutputChannel(OutputChannel& out) {
+ d_out = &out;
+ }
/**
- * Destructs a Theory. This implementation does nothing, but we
- * need a virtual destructor for safety in case subclasses have a
- * destructor.
+ * Get the output channel associated to this theory.
*/
- virtual ~Theory() {
+ OutputChannel& getOutputChannel() {
+ return *d_out;
+ }
+
+ /**
+ * Get the output channel associated to this theory [const].
+ */
+ const OutputChannel& getOutputChannel() const {
+ return *d_out;
}
/**
- * Prepare for a Node.
+ * Pre-register a term. Done one time for a Node, ever.
+ *
+ */
+ virtual void preRegisterTerm(TNode) = 0;
+
+ /**
+ * Register a term.
*
* When get() is called to get the next thing off the theory queue,
* setup() is called on its subterms (in TheoryEngine). Then setup()
* setup() MUST NOT MODIFY context-dependent objects that it hasn't
* itself just created.
*/
-
- /*virtual void setup(const Node& n) = 0;*/
-
- virtual void registerTerm(TNode n) = 0;
+ virtual void registerTerm(TNode) = 0;
/**
* Assert a fact in the current context.
*/
- void assertFact(const Node& n);
+ void assertFact(TNode n) {
+ d_facts.push(n);
+ }
/**
* Check the current assignment's consistency.
*/
- virtual void check(OutputChannel& out,
- Effort level = FULL_EFFORT) = 0;
+ virtual void check(Effort level = FULL_EFFORT) = 0;
/**
* T-propagate new literal assignments in the current context.
*/
- virtual void propagate(OutputChannel& out,
- Effort level = FULL_EFFORT) = 0;
+ virtual void propagate(Effort level = FULL_EFFORT) = 0;
/**
* Return an explanation for the literal represented by parameter n
* (which was previously propagated by this theory). Report
* explanations to an output channel.
*/
- virtual void explain(OutputChannel& out,
- const Node& n,
- Effort level = FULL_EFFORT) = 0;
-private:
- context::CDList<Node> d_assertions;
- context::CDO<unsigned> d_nextAssertion;
+ virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
+
+ //
+ // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
+ //
-protected:
/**
- * Returns the next atom in the assertFact() queue.
- * Guarentees that registerTerm is called on the theory specific subterms.
- * @return the next atom in the assertFact() queue.
+ * Different states at which invariants are checked.
*/
- Node get();
+ enum ReadyState {
+ ABOUT_TO_PUSH,
+ ABOUT_TO_POP
+ };/* enum ReadyState */
/**
- * Returns true if the assertFactQueue is empty
+ * Public invariant checker. Assert that this theory is in a valid
+ * state for the (external) system state. This implementation
+ * checks base invariants and then calls theoryReady(). This
+ * function may abort in the case of a failed assert, or return
+ * false (the caller should assert that the return value is true).
+ *
+ * @param s the state about which to check invariants
*/
- bool done();
+ bool ready(ReadyState s) {
+ if(s == ABOUT_TO_PUSH) {
+ Assert(d_facts.empty(), "Theory base code invariant broken: "
+ "fact queue is nonempty on context push");
+ }
+
+ return theoryReady(s);
+ }
+
+protected:
+
+ /**
+ * Check any invariants at the ReadyState given. Only called by
+ * Theory class, and then only with CVC4_ASSERTIONS enabled. This
+ * function may abort in the case of a failed assert, or return
+ * false (the caller should assert that the return value is true).
+ *
+ * @param s the state about which to check invariants
+ */
+ virtual bool theoryReady(ReadyState s) {
+ return true;
+ }
};/* class Theory */
+
+/**
+ * Base class for T-solver implementations. Each individual
+ * implementation T of the Theory interface should inherit from
+ * TheoryImpl<T>. This class specializes some things for a particular
+ * theory implementation.
+ *
+ * The problem with this is that Theory implementations cannot be
+ * further subclassed without designing all non-children in the type
+ * DAG to play the same trick as here (be template-polymorphic in their
+ * most-derived child), linearizing the inheritance hierarchy (viewing
+ * each instantiation separately).
+ */
+template <class T>
+class TheoryImpl : public Theory {
+
+protected:
+
+ /**
+ * Construct a Theory.
+ */
+ TheoryImpl(context::Context* ctxt, OutputChannel& out) :
+ Theory(ctxt, out) {
+ /* FIXME: assert here that a TheoryImpl<T> doesn't already exist
+ * for this NodeManager?? If it does, we're hosed because they'll
+ * share per-theory node attributes. */
+ }
+
+ /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
+ struct Registered {};
+ /** The "registerTerm()-has-been-called" flag on Nodes */
+ typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
+
+ /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
+ struct PreRegistered {};
+ /** The "preRegisterTerm()-has-been-called" flag on Nodes */
+ typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
+
+ /**
+ * Returns the next atom in the assertFact() queue. Guarantees that
+ * registerTerm() has been called on the theory specific subterms.
+ *
+ * @return the next atom in the assertFact() queue.
+ */
+ Node get();
+};/* class TheoryImpl<T> */
+
+template <class T>
+Node TheoryImpl<T>::get() {
+ Warning.printf("testing %s == %s\n", typeid(*this).name(), typeid(T).name());
+ /*Assert(typeid(*this) == typeid(T),
+ "Improper Theory inheritance chain detected.");*/
+
+ Assert( !d_facts.empty(),
+ "Theory::get() called with assertion queue empty!" );
+
+ Node fact = d_facts.front();
+ d_facts.pop();
+
+ if(! fact.getAttribute(RegisteredAttr())) {
+ std::vector<TNode> toReg;
+ toReg.push_back(fact);
+
+ /* Essentially this is doing a breadth-first numbering of
+ * non-registered subterms with children. Any non-registered
+ * leaves are immediately registered. */
+ for(std::vector<TNode>::iterator workp = toReg.begin();
+ workp != toReg.end();
+ ++workp) {
+
+ TNode n = *workp;
+
+ for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+ TNode c = *i;
+
+ if(! c.getAttribute(RegisteredAttr())) {
+ if(c.getNumChildren() == 0) {
+ c.setAttribute(RegisteredAttr(), true);
+ registerTerm(c);
+ } else {
+ toReg.push_back(c);
+ }
+ }
+ }
+ }
+
+ /* Now register the list of terms in reverse order. Between this
+ * and the above registration of leaves, this should ensure that
+ * all subterms in the entire tree were registered in
+ * reverse-topological order. */
+ for(std::vector<TNode>::reverse_iterator i = toReg.rend();
+ i != toReg.rbegin();
+ ++i) {
+
+ TNode n = *i;
+
+ /* Note that a shared TNode in the DAG rooted at "fact" could
+ * appear twice on the list, so we have to avoid hitting it
+ * twice. */
+ // FIXME when ExprSets are online, use one of those to avoid
+ // duplicates in the above?
+ if(! n.getAttribute(RegisteredAttr())) {
+ n.setAttribute(RegisteredAttr(), true);
+ registerTerm(n);
+ }
+ }
+ }
+
+ return fact;
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include "expr/node.h"
#include "theory/theory.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/theoryof_table.h"
namespace CVC4 {
*/
class TheoryEngine {
+ /** Associated SMT engine */
SmtEngine* d_smt;
+ /** A table of Kinds to pointers to Theory */
+ theory::TheoryOfTable theoryOfTable;
+
+ /**
+ * An output channel for Theory that passes messages
+ * back to a TheoryEngine.
+ */
+ class EngineOutputChannel : public theory::OutputChannel {
+ TheoryEngine* d_engine;
+ public:
+ void setEngine(TheoryEngine& engine) throw() {
+ d_engine = &engine;
+ }
+
+ void conflict(TNode, bool) throw(theory::Interrupted) {
+ }
+
+ void propagate(TNode, bool) throw(theory::Interrupted) {
+ }
+
+ void lemma(TNode, bool) throw(theory::Interrupted) {
+ }
+
+ void explanation(TNode, bool) throw(theory::Interrupted) {
+ }
+ };
+
+ EngineOutputChannel d_theoryOut;
+ theory::booleans::TheoryBool d_bool;
+ theory::uf::TheoryUF d_uf;
+ theory::arith::TheoryArith d_arith;
+
public:
/**
* Construct a theory engine.
*/
- TheoryEngine(SmtEngine* smt) : d_smt(smt) {
+ TheoryEngine(SmtEngine* smt, context::Context* ctxt) :
+ d_smt(smt),
+ d_theoryOut(),
+ d_bool(ctxt, d_theoryOut),
+ d_uf(ctxt, d_theoryOut),
+ d_arith(ctxt, d_theoryOut) {
+ d_theoryOut.setEngine(*this);
+ theoryOfTable.registerTheory(&d_bool);
+ theoryOfTable.registerTheory(&d_uf);
+ theoryOfTable.registerTheory(&d_arith);
}
/**
* Get the theory associated to a given Node.
+ *
+ * @returns the theory, or NULL if the TNode is
+ * of built-in type.
*/
- CVC4::theory::Theory* theoryOf(const Node& n);
+ theory::Theory* theoryOf(TNode n) {
+ return theoryOfTable[n];
+ }
};/* class TheoryEngine */
--- /dev/null
+/********************* */
+/** theoryof_table_epilogue.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** The theoryOf table.
+ **/
+
+};/* class TheoryOfTable */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__THEORYOF_TABLE_H */
--- /dev/null
+/********************* */
+/** theoryof_table_middle.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** The theoryOf table.
+ **/
+
+namespace CVC4 {
+namespace theory {
+
+class Theory;
+
+class TheoryOfTable {
+
+ Theory** d_table;
+
+public:
+
+ TheoryOfTable() :
+ d_table(new Theory*[::CVC4::kind::LAST_KIND]) {
+ }
+
+ Theory* operator[](TNode n) {
+ Assert(n.getKind() >= 0 && n.getKind() < ::CVC4::kind::LAST_KIND,
+ "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)");
+ return d_table[n.getKind()];
+ }
--- /dev/null
+/********************* */
+/** theoryof_table_prologue.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** The theoryOf table.
+ **/
+
+#ifndef __CVC4__THEORY__THEORYOF_TABLE_H
+#define __CVC4__THEORY__THEORYOF_TABLE_H
+
+#include "expr/kind.h"
+#include "util/Assert.h"
+
noinst_LTLIBRARIES = libuf.la
libuf_la_SOURCES = \
+ theory_def.h \
ecdata.h \
ecdata.cpp \
theory_uf.h \
--- /dev/null
+namespace CVC4 {
+ namespace theory {
+ namespace uf {
+ class TheoryUF;
+ }
+ }
+}
#include "expr/kind.h"
using namespace CVC4;
-using namespace context;
-using namespace theory;
-using namespace uf;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
-TheoryUF::TheoryUF(Context* c) :
- Theory(c),
+TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
+ TheoryImpl<TheoryUF>(c, out),
d_pending(c),
d_currentPendingIdx(c,0),
d_disequality(c),
TheoryUF::~TheoryUF(){}
+void TheoryUF::preRegisterTerm(TNode n){
+}
+
void TheoryUF::registerTerm(TNode n){
d_registered.push_back(n);
ECData* ecN;
- if(n.hasAttribute(ECAttr(),&ecN)){
+ if(n.hasAttribute(ECAttr(), ecN)){
/* registerTerm(n) is only called when a node has not been seen in the
* current context. ECAttr() is not a context-dependent attribute.
* When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
}
}
-void TheoryUF::check(OutputChannel& out, Effort level){
+void TheoryUF::check(Effort level){
while(!done()){
- Node assertion = get();
+ Node assertion;// = get();
switch(assertion.getKind()){
case EQUAL:
TNode left = (*diseqIter)[0];
TNode right = (*diseqIter)[1];
if(sameCongruenceClass(left, right)){
- out.conflict(*diseqIter, true);
+ d_out->conflict(*diseqIter, true);
}
}
}
#include "expr/attribute.h"
#include "theory/theory.h"
-#include "theory/output_channel.h"
#include "context/context.h"
#include "theory/uf/ecdata.h"
namespace theory {
namespace uf {
+class TheoryUF : public TheoryImpl<TheoryUF> {
-
-class TheoryUF : public Theory {
private:
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(context::Context* c);
+ TheoryUF(context::Context* c, OutputChannel& out);
/** Destructor for the TheoryUF object. */
~TheoryUF();
//has pending changes to the contracts
void registerTerm(TNode n);
+ void preRegisterTerm(TNode n);
- void check(OutputChannel& out, Effort level= FULL_EFFORT);
+ void check(Effort level);
- void propagate(OutputChannel& out, Effort level= FULL_EFFORT){}
+ void propagate(Effort level) {}
- void explain(OutputChannel& out,
- const Node& n,
- Effort level = FULL_EFFORT){}
+ void explain(TNode n, Effort level) {}
private:
/**
#include "expr/kind.h"
using namespace CVC4;
+using namespace CVC4::kind;
using namespace std;
class KindBlack : public CxxTest::TestSuite {
#include "expr/node.h"
using namespace CVC4;
+using namespace CVC4::kind;
using namespace std;
class NodeBlack : public CxxTest::TestSuite {
}
void tearDown() {
- delete d_nm;
delete d_scope;
+ delete d_nm;
}
bool imp(bool a, bool b) const {
TS_ASSERT(*(++eq.begin()) == right);
}
- void testPlusNode() {
- /*Node plusNode(const Node& right) const;*/
- TS_WARN( "TODO: No implementation to test." );
- }
-
- void testUMinusNode() {
- /*Node uMinusNode() const;*/
- TS_WARN( "TODO: No implementation to test." );
- }
- void testMultNode() {
- /* Node multNode(const Node& right) const;*/
- TS_WARN( "TODO: No implementation to test." );
- }
-
void testKindSingleton(Kind k) {
Node n = d_nm->mkNode(k);
TS_ASSERT(k == n.getKind());
#include "expr/kind.h"
using namespace CVC4;
+using namespace CVC4::kind;
using namespace std;
class NodeBuilderBlack : public CxxTest::TestSuite {
#include "expr/attribute.h"
using namespace CVC4;
+using namespace CVC4::kind;
using namespace CVC4::expr;
+using namespace CVC4::expr::attr;
using namespace std;
struct Test1;
typedef Attribute<Test1, std::string> TestStringAttr1;
typedef Attribute<Test2, std::string> TestStringAttr2;
+// it would be nice to have CDAttribute<> for context-dependence
+typedef CDAttribute<Test1, bool> TestCDFlag;
+
+struct ecdata;
+struct cleanupfcn {
+ static void cleanup(ecdata* ec) { /* clean up */ }
+};
+
+// ManagedAttribute<> has a cleanup function deleting the value
+typedef ManagedAttribute<Test1, ecdata*, cleanupfcn> TestECDataAttr;
+
typedef Attribute<Test1, bool> TestFlag1;
typedef Attribute<Test2, bool> TestFlag2;
typedef Attribute<Test3, bool> TestFlag3;
typedef Attribute<Test4, bool> TestFlag4;
typedef Attribute<Test5, bool> TestFlag5;
+struct FooBar {};
+struct Test6;
+typedef Attribute<Test6, FooBar> TestFlag6;
+
class NodeWhite : public CxxTest::TestSuite {
NodeManagerScope *d_scope;
}
void tearDown() {
- delete d_nm;
delete d_scope;
+ delete d_nm;
}
void testNull() {
TS_ASSERT(TestFlag3::s_id == 2);
TS_ASSERT(TestFlag4::s_id == 3);
TS_ASSERT(TestFlag5::s_id == 4);
- TS_ASSERT(attr::LastAttributeId<bool>::s_id == 5);
}
void testAttributes() {
// test two-arg version of hasAttribute()
bool bb;
Debug("boolattr", "get flag 1 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag1(), &bb));
+ TS_ASSERT(a.hasAttribute(TestFlag1(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 1 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag1(), &bb));
+ TS_ASSERT(b.hasAttribute(TestFlag1(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 1 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag1(), &bb));
+ TS_ASSERT(c.hasAttribute(TestFlag1(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 1 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag1(), &bb));
+ TS_ASSERT(unnamed.hasAttribute(TestFlag1(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 2 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag2(), &bb));
+ TS_ASSERT(a.hasAttribute(TestFlag2(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 2 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag2(), &bb));
+ TS_ASSERT(b.hasAttribute(TestFlag2(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 2 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag2(), &bb));
+ TS_ASSERT(c.hasAttribute(TestFlag2(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag2(), &bb));
+ TS_ASSERT(unnamed.hasAttribute(TestFlag2(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 3 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag3(), &bb));
+ TS_ASSERT(a.hasAttribute(TestFlag3(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 3 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag3(), &bb));
+ TS_ASSERT(b.hasAttribute(TestFlag3(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 3 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag3(), &bb));
+ TS_ASSERT(c.hasAttribute(TestFlag3(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 3 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag3(), &bb));
+ TS_ASSERT(unnamed.hasAttribute(TestFlag3(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 4 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag4(), &bb));
+ TS_ASSERT(a.hasAttribute(TestFlag4(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 4 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag4(), &bb));
+ TS_ASSERT(b.hasAttribute(TestFlag4(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 4 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag4(), &bb));
+ TS_ASSERT(c.hasAttribute(TestFlag4(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 4 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag4(), &bb));
+ TS_ASSERT(unnamed.hasAttribute(TestFlag4(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 5 on a (should be F)\n");
- TS_ASSERT(a.hasAttribute(TestFlag5(), &bb));
+ TS_ASSERT(a.hasAttribute(TestFlag5(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 5 on b (should be F)\n");
- TS_ASSERT(b.hasAttribute(TestFlag5(), &bb));
+ TS_ASSERT(b.hasAttribute(TestFlag5(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 5 on c (should be F)\n");
- TS_ASSERT(c.hasAttribute(TestFlag5(), &bb));
+ TS_ASSERT(c.hasAttribute(TestFlag5(), bb));
TS_ASSERT(! bb);
Debug("boolattr", "get flag 5 on unnamed (should be F)\n");
- TS_ASSERT(unnamed.hasAttribute(TestFlag5(), &bb));
+ TS_ASSERT(unnamed.hasAttribute(TestFlag5(), bb));
TS_ASSERT(! bb);
// setting boolean flags
projects / cvc5.git / commitdiff