From: Morgan Deters Date: Fri, 19 Feb 2010 20:29:58 +0000 (+0000) Subject: * Attribute infrastructure -- static design. Documentation is coming. X-Git-Tag: cvc5-1.0.0~9242 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce0e796ad92f040fb75435bd7880bc28a60b0374;p=cvc5.git * Attribute infrastructure -- static design. Documentation is coming. See test/unit/expr/node_white.h for use examples, including how to define new attribute kinds. Also: * fixes to test infrastructure * minor changes to code formatting throughout * attribute tests in test/unit/expr/node_white.h * fixes to NodeManagerScope ordering * use NodeValue::getKind() to properly deal with UNDEFINED_KIND (removing compiler warning) * ExprManager: add proper NodeManagerScope to public-facing member functions * store variable names and types in attributes * SoftNode is a placeholder, not a real implementation --- diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 661631b4d..42dfaead5 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -2,6 +2,7 @@ # ------------ # Do early initialization/diversion of autoconf things for CVC4 build process. AC_DEFUN([CVC4_AC_INIT], +dnl _AS_ME_PREPARE [CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE ])# CVC4_AC_INIT diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index dd5b2a2f6..7393f27a5 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -6,8 +6,6 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ - attr_type.h \ - attr_var_name.h \ node.h \ node_builder.h \ expr.h \ @@ -15,7 +13,8 @@ libexpr_la_SOURCES = \ node_value.h \ node_manager.h \ expr_manager.h \ - node_attribute.h \ + attribute.h \ + attribute.cpp \ @srcdir@/kind.h \ node.cpp \ node_builder.cpp \ diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h deleted file mode 100644 index f19491b70..000000000 --- a/src/expr/attr_type.h +++ /dev/null @@ -1,43 +0,0 @@ -/********************* */ -/** attr_type.h - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan, taking - ** 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 attribute describing the type of a node. - **/ - -#ifndef __CVC4__EXPR__ATTR_TYPE_H -#define __CVC4__EXPR__ATTR_TYPE_H - -#include "expr_attribute.h" - -namespace CVC4 { -namespace expr { - -class Type; - -// an "attribute type" for types -// this is essentially a traits structure -class Type_attr { -public: - - // could use typeid but then different on different machines/compiles - enum { hash_value = 11 }; - - typedef Type value_type;//Node? - static const Type_attr marker; -}; - -extern AttrTable type_table; - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR__ATTR_TYPE_H */ diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h deleted file mode 100644 index b3267c7dc..000000000 --- a/src/expr/attr_var_name.h +++ /dev/null @@ -1,40 +0,0 @@ -/********************* */ -/** attr_var_name.h - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan - ** 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 node attribute describing variable names. - **/ - -#ifndef __CVC4__EXPR__ATTR_VAR_NAME_H -#define __CVC4__EXPR__ATTR_VAR_NAME_H - -#include "expr_attribute.h" - -namespace CVC4 { -namespace expr { - -class VarName; - -// an "attribute type" for types -// this is essentially a traits structure -class VarName_attr { -public: - enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles - typedef Type value_type;//Node? - static const Type_attr marker; -}; - -extern AttrTable type_table; - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR__ATTR_TYPE_H */ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp new file mode 100644 index 000000000..ea672b514 --- /dev/null +++ b/src/expr/attribute.cpp @@ -0,0 +1,30 @@ +/********************* -*- C++ -*- */ +/** attribute.cpp + ** 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. + **/ + +#include "expr/attribute.h" + +#include + +using std::string; + +namespace CVC4 { +namespace expr { +namespace attr { + +unsigned BitAssignment::s_bit = 0; + +}/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/attribute.h b/src/expr/attribute.h new file mode 100644 index 000000000..b8cddacbf --- /dev/null +++ b/src/expr/attribute.h @@ -0,0 +1,573 @@ +/********************* -*- C++ -*- */ +/** attribute.h + ** Original author: mdeters + ** Major contributors: dejan + ** 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. + ** + ** Attribute structures: + ** + ** An attribute structure looks like the following: + ** + ** struct VarName_attr { + ** + ** // 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 }; + ** + ** // whether inclusion in the table keeps the (key) Node live or not + ** static const bool hard_key = false; + ** + ** // cleanup routine when the Node goes away + ** static inline void cleanup(const std::string&) { + ** } + ** } + **/ + +/* There are strong constraints on ordering of declarations of + * attributes and nodes due to template use */ +#include "expr/node.h" + +#ifndef __CVC4__EXPR__ATTRIBUTE_H +#define __CVC4__EXPR__ATTRIBUTE_H + +#include + +#include +#include + +#include "config.h" +#include "context/context.h" +#include "expr/soft_node.h" +#include "expr/type.h" + +#include "util/output.h" + +namespace CVC4 { +namespace expr { + +struct AttrHashFcn { + enum { LARGE_PRIME = 1 }; + std::size_t operator()(const std::pair& p) const { + return p.first * LARGE_PRIME + p.second.hash(); + } +}; + +struct AttrHashBoolFcn { + std::size_t operator()(const SoftNode& n) const { + return n.hash(); + } +}; + +/* +template +class AttrTable; + +template <> +class AttrTable { +public: + 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; + } + }; + + // bool specialization + //static AttrHash* s_hash; + + //typedef AttrHash::iterator iterator; + //typedef AttrHash::const_iterator const_iterator; + + template + BitAccessor& find(Node e, const Attr&); + + template + bool find(Node e, const Attr&) const; +}; + +template <> +class AttrTable { +public: + // int(egral) specialization + //static AttrHash* s_hash; + typedef AttrHash::iterator iterator; + typedef AttrHash::const_iterator const_iterator; + uint64_t& find(TNode); +}; + +template +class AttrTable { +public: + // pointer specialization + //static AttrHash* s_hash; + typedef AttrHash::iterator iterator; + typedef AttrHash::const_iterator const_iterator; +}; + +template <> +class AttrTable { +public: + // Node specialization + //static AttrHash* s_hash; + typedef AttrHash::iterator iterator; + typedef AttrHash::const_iterator const_iterator; + Node find(TNode); +}; + +template <> +class AttrTable { +public: + // string specialization + //static AttrHash* s_hash; + typedef AttrHash::iterator iterator; + typedef AttrHash::const_iterator const_iterator; + Node find(TNode); +}; + +*/ + +/* +template +AttrHash* AttrTable::s_hash = &g_hash_ptr; +*/ + +template +struct KindValueToTableValueMapping { + typedef T table_value_type; + inline static T convert(const T& t) { return t; } + inline static T convertBack(const T& t) { return t; } +}; + +template <> +struct KindValueToTableValueMapping { + 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; } +}; + +template +struct KindValueToTableValueMapping { + typedef void* table_value_type; + inline static void* convert(const T*& t) { + return reinterpret_cast(t); + } + inline static T* convertBack(void*& t) { + return reinterpret_cast(t); + } +}; + +template +struct KindValueToTableValueMapping { + typedef void* table_value_type; + inline static void* convert(const T* const& t) { + return reinterpret_cast(const_cast(t)); + } + inline static const T* convertBack(const void*& t) { + return reinterpret_cast(t); + } +}; + +template +struct OwnTable; + +template +struct KindValueToTableValueMapping > { + typedef typename KindValueToTableValueMapping::table_value_type table_value_type; +}; + +template +struct KindTableMapping { + typedef typename AttrKind::value_type table_identifier; +}; + +// use a TAG to indicate which table it should be in +template +struct AttrHash : public __gnu_cxx::hash_map, value_type, AttrHashFcn> {}; + +/* +template <> +class AttrHash : protected __gnu_cxx::hash_map { + + typedef __gnu_cxx::hash_map super; + + 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; + } + }; + + class BitIterator { + + std::pair& d_word; + + int d_bit; + + public: + + BitIterator() : + d_word((uint64_t&) d_bit), + d_bit(-1) { + } + + BitIterator(std::pair& entry, unsigned bit) : + d_entry(entry), + d_bit(bit) { + } + + BitAccessor operator*() { + return BitAccessor(d_word, d_bit); + } + }; + + class ConstBitIterator { + + uint64_t& d_word; + + unsigned d_bit; + + public: + + ConstBitIterator(uint64_t& word, unsigned bit) : + d_word(word), + d_bit(bit) { + } + + bool operator*() { + return (d_word & (1 << d_bit)) ? true : false; + } + }; + +public: + + typedef std::pair key_type; + typedef bool data_type; + typedef std::pair value_type; + + typedef BitIterator iterator; + typedef ConstBitIterator const_iterator; + + BitIterator find(const std::pair& k) { + super::iterator i = super::find(k.second); + if(i == super::end()) { + return BitIterator(); + } + return BitIterator(*i, k.first); + } + + ConstBitIterator find(const std::pair& k) const { + super::const_iterator i = super::find(k.second); + return ConstBitIterator(*i, k.first); + } + + BitAccessor operator[](const std::pair& k) { + uint64_t& word = super::operator[](k.second); + return BitAccessor(word, k.first); + } +}; +*/ + +/** + * An "attribute type" structure. + */ +template +struct 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&) {} + + static inline unsigned getId() { return s_id; } + static inline unsigned getHashValue() { return s_hashValue; } + +private: + + /** an id */ + static unsigned s_id; + + /** an extra hash value (to avoid same-value-type collisions) */ + static unsigned s_hashValue; +}; + +/** + * An "attribute type" structure for boolean flags (special). + */ +template +struct Attribute { + + /** the value type for this attribute */ + typedef bool value_type; + + /** cleanup routine when the Node goes away */ + static inline void cleanup(const bool&) {} + + static inline unsigned getId() { return s_id; } + static inline unsigned getBit() { return s_bit; } + static inline unsigned getHashValue() { return s_hashValue; } + +private: + + /** an id */ + static unsigned s_id; + + /** a bit assignment */ + static unsigned s_bit; + + /** an extra hash value (to avoid same-value-type collisions) */ + static unsigned s_hashValue; +}; + +namespace attr { + struct VarName {}; + struct Type {}; + + template + struct LastAttributeId { + static unsigned s_id; + }; + + template + unsigned LastAttributeId::s_id = 0; + + struct BitAssignment { + static unsigned s_bit; + }; +}/* CVC4::expr::attr namespace */ + +typedef Attribute VarNameAttr; +typedef Attribute TypeAttr; + +/* +template +class AttributeTable { + typedef typename Attr::value_type value_type; + + AttrTable& d_table; + +}; +*/ + +/* +template +struct AttrTables { + +}; +*/ + +template +unsigned Attribute::s_id = + attr::LastAttributeId::table_value_type>::s_id++; +template +unsigned Attribute::s_hashValue = Attribute::s_id; + +template +unsigned Attribute::s_id = + attr::LastAttributeId::s_id++; +template +unsigned Attribute::s_bit = + attr::BitAssignment::s_bit++; +template +unsigned Attribute::s_hashValue = Attribute::s_id; + +class AttributeManager; + +template +struct getTable { + //inline AttrHash >& get(AttributeManager& am); +}; + +class AttributeManager { + NodeManager* d_nm; + + AttrHash d_bools; + AttrHash d_ints; + AttrHash d_exprs; + AttrHash d_strings; + AttrHash d_ptrs; + + template + friend struct getTable; + +public: + AttributeManager(NodeManager* nm) : d_nm(nm) {} + + template + typename AttrKind::value_type getAttribute(const Node& n, + const AttrKind&); + + template + bool hasAttribute(const Node& n, + const AttrKind&, + typename AttrKind::value_type* = NULL); + + template + void setAttribute(const Node& n, + const AttrKind&, + const typename AttrKind::value_type& value); +}; + +template <> +struct getTable { + typedef AttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_bools; + } +}; + +template <> +struct getTable { + typedef AttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_ints; + } +}; + +template <> +struct getTable { + typedef AttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_exprs; + } +}; + +template <> +struct getTable { + typedef AttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_strings; + } +}; + +template +struct getTable { + typedef AttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_ptrs; + } +}; + +template +typename AttrKind::value_type AttributeManager::getAttribute(const Node& n, + const AttrKind& marker) { + + typedef typename AttrKind::value_type value_type; + typedef KindValueToTableValueMapping mapping; + typedef typename getTable::table_type table_type; + + table_type& ah = getTable::get(*this); + typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + + if(i == ah.end()) { + return typename AttrKind::value_type(); + } + + return mapping::convertBack(i->second); +} + +template +bool AttributeManager::hasAttribute(const Node& n, + const AttrKind&, + typename AttrKind::value_type* ret) { + + typedef typename AttrKind::value_type value_type; + typedef KindValueToTableValueMapping mapping; + typedef typename getTable::table_type table_type; + + table_type& ah = getTable::get(*this); + typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n)); + + if(i == ah.end()) { + return false; + } + + if(ret != NULL) { + *ret = mapping::convertBack(i->second); + } + + return true; +} + +template +inline void AttributeManager::setAttribute(const Node& n, + const AttrKind&, + const typename AttrKind::value_type& value) { + + typedef typename AttrKind::value_type value_type; + typedef KindValueToTableValueMapping mapping; + typedef typename getTable::table_type table_type; + + table_type& ah = getTable::get(*this); + ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value); +} + +/* + +template +struct last_attribute_id { + static unsigned value; +}; + +template +unsigned last_attribute_id::value = 0; + +template +unsigned register_attribute_kind() { + return last_attribute_id::value++; +} + +*/ + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR__ATTRIBUTE_H */ diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 8bd9b21f6..506c118bc 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -30,8 +30,8 @@ using namespace std; namespace CVC4 { -ExprManager::ExprManager() - : d_nm(new NodeManager()) { +ExprManager::ExprManager() : + d_nm(new NodeManager()) { } ExprManager::~ExprManager() { @@ -39,34 +39,41 @@ ExprManager::~ExprManager() { } const BooleanType* ExprManager::booleanType() { + NodeManagerScope nms(d_nm); return BooleanType::getInstance(); } const KindType* ExprManager::kindType() { + NodeManagerScope nms(d_nm); return KindType::getInstance(); } Expr ExprManager::mkExpr(Kind kind) { + NodeManagerScope nms(d_nm); return Expr(this, new Node(d_nm->mkNode(kind))); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { + NodeManagerScope nms(d_nm); return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode()))); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { + NodeManagerScope nms(d_nm); return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(), child2.getNode()))); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3) { + NodeManagerScope nms(d_nm); return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(), child2.getNode(), child3.getNode()))); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4) { + NodeManagerScope nms(d_nm); return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(), child2.getNode(), child3.getNode(), child4.getNode()))); @@ -75,12 +82,15 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5) { + NodeManagerScope nms(d_nm); return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(), child2.getNode(), child3.getNode(), child5.getNode()))); } Expr ExprManager::mkExpr(Kind kind, const vector& children) { + NodeManagerScope nms(d_nm); + vector nodes; vector::const_iterator it = children.begin(); vector::const_iterator it_end = children.end(); @@ -95,24 +105,32 @@ Expr ExprManager::mkExpr(Kind kind, const vector& children) { const FunctionType* ExprManager::mkFunctionType(const Type* domain, const Type* range) { - return FunctionType::getInstance(this,domain,range); + NodeManagerScope nms(d_nm); + return FunctionType::getInstance(this, domain, range); } /** Make a function type with input types from argTypes. */ const FunctionType* ExprManager::mkFunctionType(const std::vector& argTypes, const Type* range) { - return FunctionType::getInstance(this,argTypes,range); + NodeManagerScope nms(d_nm); + return FunctionType::getInstance(this, argTypes, range); } const Type* ExprManager::mkSort(std::string name) { // FIXME: Sorts should be unique per-ExprManager - return new SortType(this,name); + NodeManagerScope nms(d_nm); + return new SortType(this, name); +} + +Expr ExprManager::mkVar(const Type* type, string name) { + NodeManagerScope nms(d_nm); + return Expr(this, new Node(d_nm->mkVar(type, name))); } Expr ExprManager::mkVar(const Type* type) { - // FIXME: put the type into an attribute table - return Expr(this, new Node(d_nm->mkVar())); + NodeManagerScope nms(d_nm); + return Expr(this, new Node(d_nm->mkVar(type))); } NodeManager* ExprManager::getNodeManager() const { diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 1ca707fae..5bfef2aa7 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -103,6 +103,7 @@ public: const Type* mkSort(std::string name); // variables are special, because duplicates are permitted + Expr mkVar(const Type* type, std::string name); Expr mkVar(const Type* type); private: diff --git a/src/expr/node.h b/src/expr/node.h index 39eb3bcd7..463ff8144 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -28,10 +28,8 @@ #include "util/Assert.h" namespace CVC4 { - class Node; -}/* CVC4 namespace */ -namespace CVC4 { +class Node; inline std::ostream& operator<<(std::ostream&, const Node&); @@ -50,6 +48,7 @@ using CVC4::expr::NodeValue; class Node { friend class NodeValue; + friend class SoftNode; /** A convenient null-valued encapsulated pointer */ static Node s_null; @@ -155,7 +154,18 @@ public: bool isNull() const; bool isAtomic() const; - /** + template + inline typename AttrKind::value_type getAttribute(const AttrKind&); + + template + inline bool hasAttribute(const AttrKind&, + typename AttrKind::value_type* = NULL); + + template + inline void setAttribute(const AttrKind&, + const typename AttrKind::value_type& value); + + /** * Very basic pretty printer for Node. * @param o output stream to print to. * @param indent number of spaces to indent the formula by. @@ -176,7 +186,20 @@ private: }/* CVC4 namespace */ -#include "expr/node_value.h" +#include + +// for hashtables +namespace __gnu_cxx { + template <> + struct hash { + size_t operator()(const CVC4::Node& node) const { + return (size_t)node.hash(); + } + }; +}/* __gnu_cxx namespace */ + +#include "expr/attribute.h" +#include "expr/node_manager.h" namespace CVC4 { @@ -237,6 +260,23 @@ inline size_t Node::getNumChildren() const { return d_ev->d_nchildren; } +template +inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) { + return NodeManager::currentNM()->getAttribute(*this, AttrKind()); +} + +template +inline bool Node::hasAttribute(const AttrKind&, + typename AttrKind::value_type* ret) { + return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); +} + +template +inline void Node::setAttribute(const AttrKind&, + const typename AttrKind::value_type& value) { + NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); +} + }/* CVC4 namespace */ #endif /* __CVC4__NODE_H */ diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h deleted file mode 100644 index f43013a27..000000000 --- a/src/expr/node_attribute.h +++ /dev/null @@ -1,102 +0,0 @@ -/********************* */ -/** node_attribute.h - ** Original author: mdeters - ** Major contributors: dejan - ** 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. - **/ - -#ifndef __CVC4__EXPR__NODE_ATTRIBUTE_H -#define __CVC4__EXPR__NODE_ATTRIBUTE_H - -#include -#include "config.h" -#include "context/context.h" -#include "expr/node.h" - -namespace CVC4 { -namespace expr { - -template -class AttrTables; - -// global (or TSS) -extern CDMap g_hash_bool; -extern CDMap g_hash_int; -extern CDMap g_hash_expr; -extern CDMap g_hash_ptr; - -template -class AttrTable; - -template <> -class AttrTable { -public: - class BitAccessor { - uint64_t& d_word; - unsigned d_bit; - public: - BitAccessor& operator=(bool b); - // continue... - }; - - // bool specialization - static CDMap *s_hash; - - template - BitAccessor& find(Node e, const Attr&); - - template - bool find(Node e, const Attr&) const; -}; - -template <> -class AttrTable { -public: - // int(egral) specialization - static CDMap *s_hash; - uint64_t& find(Node); - uint64_t& find(Node) const; -}; - -template -class AttrTable { - // pointer specialization - static CDMap *s_hash; -public: -}; - -template <> -class AttrTable { -public: - // Node specialization - static CDMap *s_hash; - Node find(Node); -}; - -CDMap* AttrTable::s_hash = &g_hash_bool; -CDMap* AttrTable::s_hash = &g_hash_int; -CDMap* AttrTable::s_hash = &g_hash_expr; - -template -CDMap* AttrTable::s_hash = &g_hash_ptr; - -template -class AttributeTable { - typedef typename Attr::value_type value_type; - - AttrTable& d_table; - -}; - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 08a879600..093f09a79 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -171,7 +171,7 @@ public: NodeBuilder& operator<<(const Kind& k) { Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Assert(d_ev->d_kind == UNDEFINED_KIND); + Assert(d_ev->getKind() == UNDEFINED_KIND); d_ev->d_kind = k; return *this; } @@ -563,7 +563,7 @@ inline void NodeBuilder::dealloc() { template NodeBuilder::operator Node() {// not const Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Assert(d_ev->d_kind != UNDEFINED_KIND, + Assert(d_ev->getKind() != UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); if(d_ev->d_kind == VARIABLE) { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 3561f2119..12a6d1732 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -16,16 +16,16 @@ #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; + namespace CVC4 { __thread NodeManager* NodeManager::s_current = 0; -NodeManager::NodeManager() { - poolInsert(&NodeValue::s_null); -} - NodeValue* NodeManager::poolLookup(NodeValue* nv) const { NodeValueSet::const_iterator find = d_nodeValueSet.find(nv); if (find == d_nodeValueSet.end()) { @@ -68,10 +68,23 @@ Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, cons } // N-ary version -Node NodeManager::mkNode(Kind kind, const std::vector& children) { +Node NodeManager::mkNode(Kind kind, const vector& children) { return NodeBuilder<>(this, kind).append(children); } +Node NodeManager::mkVar(const Type* type, string name) { + Node n = NodeBuilder<>(this, VARIABLE); + n.setAttribute(TypeAttr(), 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); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0abd86130..2862203db 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -17,23 +17,26 @@ #define __CVC4__NODE_MANAGER_H #include +#include #include -#include "node.h" -#include "kind.h" +#include "expr/node.h" +#include "expr/kind.h" namespace __gnu_cxx { -template<> + template<> struct hash { size_t operator()(const CVC4::NodeValue* nv) const { return (size_t)nv->hash(); } }; -} /* __gnu_cxx namespace */ +}/* __gnu_cxx namespace */ namespace CVC4 { +class Type; + class NodeManager { static __thread NodeManager* s_current; @@ -42,6 +45,8 @@ class NodeManager { typedef __gnu_cxx::hash_set, NodeValue::NodeValueEq> NodeValueSet; NodeValueSet d_nodeValueSet; + expr::AttributeManager d_am; + NodeValue* poolLookup(NodeValue* nv) const; void poolInsert(NodeValue* nv); @@ -49,7 +54,9 @@ class NodeManager { public: - NodeManager(); + NodeManager() : d_am(this) { + poolInsert( &NodeValue::s_null ); + } static NodeManager* currentNM() { return s_current; } @@ -64,22 +71,61 @@ public: Node mkNode(Kind kind, const std::vector& children); // variables are special, because duplicates are permitted + Node mkVar(const Type* type, std::string name); + Node mkVar(const Type* type); Node mkVar(); -}; + template + inline typename AttrKind::value_type getAttribute(const Node& n, + const AttrKind&); + + template + inline bool hasAttribute(const Node& n, + const AttrKind&, + typename AttrKind::value_type* = NULL); + + template + inline void setAttribute(const Node& n, + const AttrKind&, + const typename AttrKind::value_type& value); +}; class NodeManagerScope { NodeManager *d_oldNodeManager; public: + NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) { NodeManager::s_current = nm; + Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } + ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; + Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n"; } }; +template +inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n, + const AttrKind&) { + return d_am.getAttribute(n, AttrKind()); +} + +template +inline bool NodeManager::hasAttribute(const Node& n, + const AttrKind&, + typename AttrKind::value_type* ret) { + return d_am.hasAttribute(n, AttrKind(), ret); +} + +template +inline void NodeManager::setAttribute(const Node& n, + const AttrKind&, + const typename AttrKind::value_type& value) { + d_am.setAttribute(n, AttrKind(), value); +} + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index f8bf33b5c..36d634b8b 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -17,7 +17,8 @@ ** reference count on NodeValue instances and **/ -#include "node_value.h" +#include "expr/node_value.h" +#include "expr/node.h" #include using namespace std; @@ -27,11 +28,17 @@ namespace CVC4 { size_t NodeValue::next_id = 1; NodeValue::NodeValue() : - d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) { + 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(unsigned(UNDEFINED_KIND)), d_nchildren(0) { + d_id(0), + d_rc(0), + d_kind(kindToDKind(UNDEFINED_KIND)), + d_nchildren(0) { } NodeValue::~NodeValue() { @@ -98,7 +105,13 @@ string NodeValue::toString() const { void NodeValue::toStream(std::ostream& out) const { out << "(" << Kind(d_kind); if(d_kind == VARIABLE) { - out << ":" << this; + Node n(this); + string s; + if(n.hasAttribute(VarNameAttr(), &s)) { + out << ":" << s; + } else { + out << ":" << this; + } } else { for(const_ev_iterator i = ev_begin(); i != ev_end(); ++i) { if(i != ev_end()) { diff --git a/src/expr/node_value.h b/src/expr/node_value.h index d86822b8d..2d84967c6 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -51,6 +51,12 @@ class NodeValue { * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ static const unsigned MAX_RC = 255; + /** Number of bits assigned to the kind in the NodeValue header */ + static const unsigned KINDBITS = 8; + + /** A mask for d_kind */ + static const unsigned kindMask = (1u << KINDBITS) - 1; + // this header fits into one 64-bit word /** The ID (0 is reserved for the null value) */ @@ -60,7 +66,7 @@ class NodeValue { unsigned d_rc : 8; /** Kind of the expression */ - unsigned d_kind : 8; + unsigned d_kind : KINDBITS; /** Number of children */ unsigned d_nchildren : 16; @@ -178,13 +184,19 @@ public: } }; - unsigned getId() const { return d_id; } - Kind getKind() const { return (Kind) d_kind; } + Kind getKind() const { return dKindToKind(d_kind); } unsigned getNumChildren() const { return d_nchildren; } std::string toString() const; void toStream(std::ostream& out) const; + + static inline unsigned kindToDKind(Kind k) { + return ((unsigned) k) & kindMask; + } + static inline Kind dKindToKind(unsigned d) { + return (d == kindMask) ? UNDEFINED_KIND : Kind(d); + } }; }/* CVC4::expr namespace */ diff --git a/src/expr/soft_node.h b/src/expr/soft_node.h new file mode 100644 index 000000000..fe71a4d1a --- /dev/null +++ b/src/expr/soft_node.h @@ -0,0 +1,36 @@ +/********************* -*- C++ -*- */ +/** soft_node.h + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): taking + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Encapsulation of a pointer to node information that is explicitly + ** NOT reference-counted. These "smart pointers" do NOT keep live + ** the NodeValue object to which they refer. + **/ + +#ifndef __CVC4__SOFT_NODE_H +#define __CVC4__SOFT_NODE_H + +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +/** + * For now, treat SoftNodes as regular Nodes. We'll address this + * later. + */ +typedef CVC4::Node SoftNode; +typedef CVC4::Node TNode; + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__SOFT_NODE_H */ diff --git a/src/expr/type.h b/src/expr/type.h index e5fda779e..19d0c831e 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -29,7 +29,7 @@ class ExprManager; * Class encapsulating CVC4 expression types. */ class Type { - public: +public: /** Comparision for equality */ bool operator==(const Type& t) const; @@ -229,7 +229,8 @@ public: * @param e the type to output * @return the stream */ -std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC ; +std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; + } -#endif // __CVC4__TYPE_H +#endif /* __CVC4__TYPE_H */ diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 533e2cb2d..30fb33a32 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -49,23 +49,26 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : } Expr AntlrParser::getSymbol(std::string name, SymbolType type) { - Assert( isDeclared(name,type) ); + Assert( isDeclared(name, type) ); + switch( type ) { + case SYM_VARIABLE: // Functions share var namespace case SYM_FUNCTION: return d_varSymbolTable.getObject(name); + default: Unhandled("Unhandled symbol type!"); } } Expr AntlrParser::getVariable(std::string name) { - return getSymbol(name,SYM_VARIABLE); + return getSymbol(name, SYM_VARIABLE); } Expr AntlrParser::getFunction(std::string name) { - return getSymbol(name,SYM_FUNCTION); + return getSymbol(name, SYM_FUNCTION); } const Type* @@ -77,24 +80,24 @@ AntlrParser::getType(std::string var_name, } const Type* AntlrParser::getSort(std::string name) { - Assert( isDeclared(name,SYM_SORT) ); + Assert( isDeclared(name, SYM_SORT) ); const Type* t = d_sortTable.getObject(name); return t; } /* Returns true if name is bound to a boolean variable. */ bool AntlrParser::isBoolean(std::string name) { - return isDeclared(name,SYM_VARIABLE) && getType(name)->isBoolean(); + return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean(); } /* Returns true if name is bound to a function. */ bool AntlrParser::isFunction(std::string name) { - return isDeclared(name,SYM_FUNCTION) && getType(name)->isFunction(); + return isDeclared(name, SYM_FUNCTION) && getType(name)->isFunction(); } /* Returns true if name is bound to a function returning boolean. */ bool AntlrParser::isPredicate(std::string name) { - return isDeclared(name,SYM_FUNCTION) && getType(name)->isPredicate(); + return isDeclared(name, SYM_FUNCTION) && getType(name)->isPredicate(); } Expr AntlrParser::getTrueExpr() const { @@ -160,7 +163,7 @@ const Type* AntlrParser::predicateType(const std::vector& sorts) { if(sorts.size() == 0) { return d_exprManager->booleanType(); } else { - return d_exprManager->mkFunctionType(sorts,d_exprManager->booleanType()); + return d_exprManager->mkFunctionType(sorts, d_exprManager->booleanType()); } } @@ -168,7 +171,7 @@ Expr AntlrParser::mkVar(const std::string name, const Type* type) { Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; Assert( !isDeclared(name) ) ; - Expr expr = d_exprManager->mkVar(type); + Expr expr = d_exprManager->mkVar(type, name); d_varSymbolTable.bindName(name, expr); d_varTypeTable.bindName(name,type); Assert( isDeclared(name) ) ; @@ -189,10 +192,10 @@ AntlrParser::mkVars(const std::vector names, const Type* AntlrParser::newSort(std::string name) { Debug("parser") << "newSort(" << name << ")" << std::endl; - Assert( !isDeclared(name,SYM_SORT) ) ; + Assert( !isDeclared(name, SYM_SORT) ) ; const Type* type = d_exprManager->mkSort(name); - d_sortTable.bindName(name,type); - Assert( isDeclared(name,SYM_SORT) ) ; + d_sortTable.bindName(name, type); + Assert( isDeclared(name, SYM_SORT) ) ; return type; } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9fb5858b3..1bb71860c 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -22,20 +22,12 @@ #ifndef __CVC4__CNF_STREAM_H #define __CVC4__CNF_STREAM_H + #include "expr/node.h" #include "prop/sat.h" #include -namespace __gnu_cxx { -template<> - struct hash { - size_t operator()(const CVC4::Node& node) const { - return (size_t)node.hash(); - } - }; -} /* __gnu_cxx namespace */ - namespace CVC4 { namespace prop { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8bca39df4..24795111f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -75,8 +75,8 @@ void SmtEngine::addFormula(const Node& e) { } Result SmtEngine::checkSat(const BoolExpr& e) { - Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; NodeManagerScope nms(d_nodeManager); + Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; Node node_e = preprocess(e.getNode()); addFormula(node_e); Result r = check().asSatisfiabilityResult(); @@ -85,8 +85,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) { } Result SmtEngine::query(const BoolExpr& e) { - Debug("smt") << "SMT query(" << e << ")" << std::endl; NodeManagerScope nms(d_nodeManager); + Debug("smt") << "SMT query(" << e << ")" << std::endl; Node node_e = preprocess(d_nodeManager->mkNode(NOT, e.getNode())); addFormula(node_e); Result r = check().asValidityResult(); @@ -95,25 +95,34 @@ Result SmtEngine::query(const BoolExpr& e) { } Result SmtEngine::assertFormula(const BoolExpr& e) { - Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; NodeManagerScope nms(d_nodeManager); + Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; Node node_e = preprocess(e.getNode()); addFormula(node_e); return quickCheck().asValidityResult(); } Expr SmtEngine::simplify(const Expr& e) { + NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT simplify(" << e << ")" << std::endl; - Expr simplify(const Expr& e); + Unimplemented(); +} + +Model SmtEngine::getModel() { + NodeManagerScope nms(d_nodeManager); Unimplemented(); } void SmtEngine::push() { + NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT push()" << std::endl; + Unimplemented(); } void SmtEngine::pop() { + NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT pop()" << std::endl; + Unimplemented(); } }/* CVC4 namespace */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 7a1b75cbc..84465127b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -24,8 +24,6 @@ TEST_DEPS = \ $(TEST_DEPS_DIST) \ $(TEST_DEPS_NODIST) -@mk_include@ @srcdir@/Makefile.tests - if HAVE_CXXTESTGEN AM_CPPFLAGS = \ @@ -46,8 +44,6 @@ AM_LDFLAGS_BLACK = \ AM_LDFLAGS_PUBLIC = \ @abs_top_builddir@/src/libcvc4.la -TESTS = $(UNIT_TESTS) - EXTRA_DIST = \ no_cxxtest \ $(TEST_DEPS_DIST) @@ -57,9 +53,17 @@ noinst_LTLIBRARIES = libdummy.la libdummy_la_SOURCES = expr/node_black.cpp libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la -$(TESTS:%=%.cpp): %.cpp: %.h +MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp) + +@mk_include@ @srcdir@/Makefile.tests + +# We leave "TESTS" empty here; it's handled in Makefile.tests (see +# that file for comment) +# TESTS = + +$(UNIT_TESTS:%=%.cpp): %.cpp: %.h mkdir -p `dirname "$@"` - @CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<" + $(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<" $(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS) $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $< $(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo @@ -70,15 +74,13 @@ $(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS) $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $< $(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo -MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp) - else # force a user-visible failure for "make check" TESTS = no_cxxtest EXTRA_DIST = \ - $(UNIT_TESTS) \ + $(UNIT_TESTS:%=%.cpp) \ $(TEST_DEPS_DIST) endif diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests index c542259b1..4f2f3dd5f 100644 --- a/test/unit/Makefile.tests +++ b/test/unit/Makefile.tests @@ -1,5 +1,20 @@ -TESTS := $(filter $(TEST_PREFIX)%,$(TESTS)) +# This makefile is separated because it's not under automake control. +# This gets confusing, because we want: +# +# 1. to (re)build only the tests in the "filtered" set of tests +# (those that we're going to run) +# 2. run only the tests in the "filtered" set of tests. +# +# It's a pain to make automake happy. -WHITE_TESTS = $(filter %_white,$(TESTS)) -BLACK_TESTS = $(filter %_black,$(TESTS)) -PUBLIC_TESTS = $(filter %_public,$(TESTS)) +# Add "filtered" tests to the set of TESTS +TESTS = $(filter $(TEST_PREFIX)%,$(UNIT_TESTS)) + +# subsets of the tests, based on name +WHITE_TESTS = $(filter %_white,$(UNIT_TESTS)) +BLACK_TESTS = $(filter %_black,$(UNIT_TESTS)) +PUBLIC_TESTS = $(filter %_public,$(UNIT_TESTS)) + +# This rule forces automake to correctly build our filtered +# set of tests +check-TESTS: $(TESTS) diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index fd2cf3332..0693b48db 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -39,7 +39,7 @@ public: d_scope = new NodeManagerScope(d_nm); } - void tearDown(){ + void tearDown() { delete d_nm; delete d_scope; } @@ -55,7 +55,7 @@ public: Node::null(); } - void testIsNull(){ + void testIsNull() { /* bool isNull() const; */ Node a = Node::null(); @@ -73,7 +73,7 @@ public: Node e(Node::null()); } - void testDestructor(){ + void testDestructor() { /* No access to internals ? * Makes sense to only test that this is crash free. */ @@ -84,7 +84,7 @@ public: } /*tests: bool operator==(const Node& e) const */ - void testOperatorEquals(){ + void testOperatorEquals() { Node a, b, c; b = d_nm->mkVar(); @@ -122,7 +122,7 @@ public: } /* operator!= */ - void testOperatorNotEquals(){ + void testOperatorNotEquals() { Node a, b, c; @@ -157,7 +157,7 @@ public: } - void testOperatorSquare(){ + void testOperatorSquare() { /*Node operator[](int i) const */ //Basic bounds check on a node w/out children @@ -183,7 +183,7 @@ public: } /*tests: Node& operator=(const Node&); */ - void testOperatorAssign(){ + void testOperatorAssign() { Node a, b; Node c = d_nm->mkNode(NOT); @@ -197,7 +197,7 @@ public: TS_ASSERT(a==c); } - void testOperatorLessThan(){ + void testOperatorLessThan() { /* We don't have access to the ids so we can't test the implementation * in the black box tests. */ @@ -232,13 +232,13 @@ public: std::vector chain; int N = 500; Node curr = d_nm->mkNode(NULL_EXPR); - for(int i=0;imkNode(AND,curr); } - for(int i=0;imkNode(ITE); Node b = d_nm->mkNode(ITE); @@ -257,7 +257,7 @@ public: - void testEqExpr(){ + void testEqExpr() { /*Node eqExpr(const Node& right) const;*/ Node left = d_nm->mkNode(TRUE); @@ -272,7 +272,7 @@ public: TS_ASSERT(eq[1] == right); } - void testNotExpr(){ + void testNotExpr() { /* Node notExpr() const;*/ Node child = d_nm->mkNode(TRUE); @@ -284,7 +284,7 @@ public: TS_ASSERT(parent[0] == child); } - void testAndExpr(){ + void testAndExpr() { /*Node andExpr(const Node& right) const;*/ Node left = d_nm->mkNode(TRUE); @@ -300,7 +300,7 @@ public: } - void testOrExpr(){ + void testOrExpr() { /*Node orExpr(const Node& right) const;*/ Node left = d_nm->mkNode(TRUE); @@ -316,7 +316,7 @@ public: } - void testIteExpr(){ + void testIteExpr() { /*Node iteExpr(const Node& thenpart, const Node& elsepart) const;*/ Node cnd = d_nm->mkNode(PLUS); @@ -333,7 +333,7 @@ public: TS_ASSERT(*(++(++ite.begin())) == elseBranch); } - void testIffExpr(){ + void testIffExpr() { /* Node iffExpr(const Node& right) const; */ Node left = d_nm->mkNode(TRUE); @@ -349,7 +349,7 @@ public: } - void testImpExpr(){ + void testImpExpr() { /* Node impExpr(const Node& right) const; */ Node left = d_nm->mkNode(TRUE); Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); @@ -363,7 +363,7 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - void testXorExpr(){ + void testXorExpr() { /*Node xorExpr(const Node& right) const;*/ Node left = d_nm->mkNode(TRUE); Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); @@ -377,26 +377,26 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - void testPlusExpr(){ + void testPlusExpr() { /*Node plusExpr(const Node& right) const;*/ TS_WARN( "TODO: No implementation to test." ); } - void testUMinusExpr(){ + void testUMinusExpr() { /*Node uMinusExpr() const;*/ TS_WARN( "TODO: No implementation to test." ); } - void testMultExpr(){ + void testMultExpr() { /* Node multExpr(const Node& right) const;*/ TS_WARN( "TODO: No implementation to test." ); } - void testKindSingleton(Kind k){ + void testKindSingleton(Kind k) { Node n = d_nm->mkNode(k); TS_ASSERT(k == n.getKind()); } - void testGetKind(){ + void testGetKind() { /*inline Kind getKind() const; */ testKindSingleton(NOT); diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index c097f2758..73a7b1a54 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -15,13 +15,46 @@ #include +#include + +#include "expr/node_value.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" #include "expr/node.h" +#include "expr/attribute.h" using namespace CVC4; +using namespace CVC4::expr; +using namespace std; + +struct Test1; +struct Test2; +struct Test3; +struct Test4; + +typedef Attribute TestStringAttr1; +typedef Attribute TestStringAttr2; + +typedef Attribute TestFlag1; +typedef Attribute TestFlag2; class NodeWhite : public CxxTest::TestSuite { + + NodeManagerScope *d_scope; + NodeManager *d_nm; + public: + void setUp() { + d_nm = new NodeManager(); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown() { + delete d_nm; + delete d_scope; + } + void testNull() { Node::s_null; } @@ -29,4 +62,157 @@ public: void testCopyCtor() { Node e(Node::s_null); } + + void testBuilder() { + NodeBuilder<> b; + TS_ASSERT(b.d_ev->getId() == 0); + TS_ASSERT(b.d_ev->getKind() == UNDEFINED_KIND); + TS_ASSERT(b.d_ev->getNumChildren() == 0); + /* etc. */ + } + + void testAttributeIds() { + TS_ASSERT(VarNameAttr::s_id == 0); + TS_ASSERT(TestStringAttr1::s_id == 1); + TS_ASSERT(TestStringAttr2::s_id == 2); + TS_ASSERT(attr::LastAttributeId::s_id == 3); + + TS_ASSERT(TypeAttr::s_id == 0); + TS_ASSERT(attr::LastAttributeId::s_id == 1); + + TS_ASSERT(TestFlag1::s_id == 0); + TS_ASSERT(TestFlag2::s_id == 1); + TS_ASSERT(attr::LastAttributeId::s_id == 2); + TS_ASSERT(TestFlag1::s_bit == 0); + TS_ASSERT(TestFlag2::s_bit == 1); + TS_ASSERT(attr::BitAssignment::s_bit == 2); + } + + void testAttributes() { + AttributeManager& am = d_nm->d_am; + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + Node unnamed = d_nm->mkVar(); + + a.setAttribute(VarNameAttr(), "a"); + b.setAttribute(VarNameAttr(), "b"); + c.setAttribute(VarNameAttr(), "c"); + + a.setAttribute(TestFlag1(), true); + b.setAttribute(TestFlag1(), false); + c.setAttribute(TestFlag1(), false); + unnamed.setAttribute(TestFlag1(), true); + + a.setAttribute(TestFlag2(), false); + b.setAttribute(TestFlag2(), true); + c.setAttribute(TestFlag2(), true); + unnamed.setAttribute(TestFlag2(), false); + + TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr1())); + TS_ASSERT(! b.hasAttribute(TestStringAttr1())); + TS_ASSERT(! c.hasAttribute(TestStringAttr1())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr2())); + TS_ASSERT(! b.hasAttribute(TestStringAttr2())); + TS_ASSERT(! c.hasAttribute(TestStringAttr2())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); + + TS_ASSERT(a.getAttribute(TestFlag1())); + TS_ASSERT(! b.getAttribute(TestFlag1())); + TS_ASSERT(! c.getAttribute(TestFlag1())); + TS_ASSERT(unnamed.getAttribute(TestFlag1())); + + TS_ASSERT(! a.getAttribute(TestFlag2())); + TS_ASSERT(b.getAttribute(TestFlag2())); + TS_ASSERT(c.getAttribute(TestFlag2())); + TS_ASSERT(! unnamed.getAttribute(TestFlag2())); + + a.setAttribute(TestStringAttr1(), "foo"); + b.setAttribute(TestStringAttr1(), "bar"); + c.setAttribute(TestStringAttr1(), "baz"); + + TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + + TS_ASSERT(a.hasAttribute(TestStringAttr1())); + TS_ASSERT(b.hasAttribute(TestStringAttr1())); + TS_ASSERT(c.hasAttribute(TestStringAttr1())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr2())); + TS_ASSERT(! b.hasAttribute(TestStringAttr2())); + TS_ASSERT(! c.hasAttribute(TestStringAttr2())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); + + a.setAttribute(VarNameAttr(), "b"); + b.setAttribute(VarNameAttr(), "c"); + c.setAttribute(VarNameAttr(), "a"); + + TS_ASSERT(c.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(a.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + + } };