diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-19 20:29:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-19 20:29:58 +0000 |
commit | ce0e796ad92f040fb75435bd7880bc28a60b0374 (patch) | |
tree | 00a390f0347a30978b482cbbb6e074c6dc5a99d2 /src | |
parent | 34b455b1d74fdc06dd2f874fa2bc8d73127fbedf (diff) |
* 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
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/Makefile.am | 5 | ||||
-rw-r--r-- | src/expr/attr_type.h | 43 | ||||
-rw-r--r-- | src/expr/attr_var_name.h | 40 | ||||
-rw-r--r-- | src/expr/attribute.cpp | 30 | ||||
-rw-r--r-- | src/expr/attribute.h | 573 | ||||
-rw-r--r-- | src/expr/expr_manager.cpp | 32 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 1 | ||||
-rw-r--r-- | src/expr/node.h | 50 | ||||
-rw-r--r-- | src/expr/node_attribute.h | 102 | ||||
-rw-r--r-- | src/expr/node_builder.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 23 | ||||
-rw-r--r-- | src/expr/node_manager.h | 58 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 21 | ||||
-rw-r--r-- | src/expr/node_value.h | 18 | ||||
-rw-r--r-- | src/expr/soft_node.h | 36 | ||||
-rw-r--r-- | src/expr/type.h | 7 | ||||
-rw-r--r-- | src/parser/antlr_parser.cpp | 27 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 10 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 17 |
19 files changed, 849 insertions, 248 deletions
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_attr> 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_attr> 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 <string> + +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 <stdint.h> + +#include <string> +#include <ext/hash_map> + +#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<unsigned, SoftNode>& 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 T> +class AttrTable; + +template <> +class AttrTable<bool> { +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<uint64_t>* s_hash; + + //typedef AttrHash<SoftNode, uint64_t>::iterator iterator; + //typedef AttrHash<SoftNode, uint64_t>::const_iterator const_iterator; + + template <class Attr> + BitAccessor& find(Node e, const Attr&); + + template <class Attr> + bool find(Node e, const Attr&) const; +}; + +template <> +class AttrTable<uint64_t> { +public: + // int(egral) specialization + //static AttrHash<uint64_t>* s_hash; + typedef AttrHash<uint64_t>::iterator iterator; + typedef AttrHash<uint64_t>::const_iterator const_iterator; + uint64_t& find(TNode); +}; + +template <class T> +class AttrTable<T*> { +public: + // pointer specialization + //static AttrHash<void*>* s_hash; + typedef AttrHash<void*>::iterator iterator; + typedef AttrHash<void*>::const_iterator const_iterator; +}; + +template <> +class AttrTable<Node> { +public: + // Node specialization + //static AttrHash<SoftNode>* s_hash; + typedef AttrHash<SoftNode>::iterator iterator; + typedef AttrHash<SoftNode>::const_iterator const_iterator; + Node find(TNode); +}; + +template <> +class AttrTable<std::string> { +public: + // string specialization + //static AttrHash<std::string>* s_hash; + typedef AttrHash<std::string>::iterator iterator; + typedef AttrHash<std::string>::const_iterator const_iterator; + Node find(TNode); +}; + +*/ + +/* +template <class T> +AttrHash<void*>* AttrTable<T*>::s_hash = &g_hash_ptr; +*/ + +template <class T> +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<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; } +}; + +template <class T> +struct KindValueToTableValueMapping<T*> { + typedef void* table_value_type; + inline static void* convert(const T*& t) { + return reinterpret_cast<void*>(t); + } + inline static T* convertBack(void*& t) { + return reinterpret_cast<T*>(t); + } +}; + +template <class T> +struct KindValueToTableValueMapping<const T*> { + typedef void* table_value_type; + inline static void* convert(const T* const& t) { + return reinterpret_cast<void*>(const_cast<T*>(t)); + } + inline static const T* convertBack(const void*& 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; +}; + +// use a TAG to indicate which table it should be in +template <class value_type> +struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {}; + +/* +template <> +class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> { + + typedef __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> 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<SoftNode, uint64_t>& d_word; + + int d_bit; + + public: + + BitIterator() : + d_word((uint64_t&) d_bit), + d_bit(-1) { + } + + BitIterator(std::pair<SoftNode, uint64_t>& 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<unsigned, SoftNode> key_type; + typedef bool data_type; + typedef std::pair<const key_type, data_type> value_type; + + typedef BitIterator iterator; + typedef ConstBitIterator const_iterator; + + BitIterator find(const std::pair<unsigned, SoftNode>& k) { + super::iterator i = super::find(k.second); + if(i == super::end()) { + return BitIterator(); + } + return BitIterator(*i, k.first); + } + + ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const { + super::const_iterator i = super::find(k.second); + return ConstBitIterator(*i, k.first); + } + + BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) { + uint64_t& word = super::operator[](k.second); + return BitAccessor(word, k.first); + } +}; +*/ + +/** + * An "attribute type" structure. + */ +template <class T, class value_t> +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 <class T> +struct Attribute<T, bool> { + + /** 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 <class T> + struct LastAttributeId { + static unsigned s_id; + }; + + template <class T> + unsigned LastAttributeId<T>::s_id = 0; + + struct BitAssignment { + static unsigned s_bit; + }; +}/* CVC4::expr::attr namespace */ + +typedef Attribute<attr::VarName, std::string> VarNameAttr; +typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr; + +/* +template <class Attr> +class AttributeTable { + typedef typename Attr::value_type value_type; + + AttrTable<value_type>& d_table; + +}; +*/ + +/* +template <class T> +struct AttrTables { + +}; +*/ + +template <class T, class value_t> +unsigned Attribute<T, value_t>::s_id = + attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++; +template <class T, class value_t> +unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id; + +template <class T> +unsigned Attribute<T, bool>::s_id = + attr::LastAttributeId<bool>::s_id++; +template <class T> +unsigned Attribute<T, bool>::s_bit = + attr::BitAssignment::s_bit++; +template <class T> +unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id; + +class AttributeManager; + +template <class T> +struct getTable { + //inline AttrHash<KindTableValueMapping<T> >& get(AttributeManager& am); +}; + +class AttributeManager { + NodeManager* d_nm; + + AttrHash<uint64_t> d_bools; + AttrHash<uint64_t> d_ints; + AttrHash<SoftNode> d_exprs; + AttrHash<std::string> d_strings; + AttrHash<void*> d_ptrs; + + template <class T> + friend struct getTable; + +public: + AttributeManager(NodeManager* nm) : d_nm(nm) {} + + template <class AttrKind> + typename AttrKind::value_type getAttribute(const Node& n, + const AttrKind&); + + template <class AttrKind> + bool hasAttribute(const Node& n, + const AttrKind&, + typename AttrKind::value_type* = NULL); + + template <class AttrKind> + void setAttribute(const Node& n, + const AttrKind&, + const typename AttrKind::value_type& value); +}; + +template <> +struct getTable<bool> { + typedef AttrHash<uint64_t> table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_bools; + } +}; + +template <> +struct getTable<uint64_t> { + typedef AttrHash<uint64_t> table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_ints; + } +}; + +template <> +struct getTable<Node> { + typedef AttrHash<SoftNode> table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_exprs; + } +}; + +template <> +struct getTable<std::string> { + typedef AttrHash<std::string> table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_strings; + } +}; + +template <class T> +struct getTable<T*> { + typedef AttrHash<void*> table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_ptrs; + } +}; + +template <class AttrKind> +typename AttrKind::value_type AttributeManager::getAttribute(const Node& n, + const AttrKind& marker) { + + typedef typename AttrKind::value_type value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + typedef typename getTable<value_type>::table_type table_type; + + table_type& ah = getTable<value_type>::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 <class AttrKind> +bool AttributeManager::hasAttribute(const Node& n, + const AttrKind&, + 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; + + table_type& ah = getTable<value_type>::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 <class AttrKind> +inline void AttributeManager::setAttribute(const Node& n, + const AttrKind&, + const typename AttrKind::value_type& value) { + + typedef typename AttrKind::value_type value_type; + typedef KindValueToTableValueMapping<value_type> mapping; + typedef typename getTable<value_type>::table_type table_type; + + table_type& ah = getTable<value_type>::get(*this); + ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value); +} + +/* + +template <class attr> +struct last_attribute_id { + static unsigned value; +}; + +template <class attr> +unsigned last_attribute_id<attr>::value = 0; + +template <class attr> +unsigned register_attribute_kind() { + return last_attribute_id<attr>::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<Expr>& children) { + NodeManagerScope nms(d_nm); + vector<Node> nodes; vector<Expr>::const_iterator it = children.begin(); vector<Expr>::const_iterator it_end = children.end(); @@ -95,24 +105,32 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& 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<const Type*>& 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 <class AttrKind> + inline typename AttrKind::value_type getAttribute(const AttrKind&); + + template <class AttrKind> + inline bool hasAttribute(const AttrKind&, + typename AttrKind::value_type* = NULL); + + template <class AttrKind> + 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 <ext/hash_map> + +// for hashtables +namespace __gnu_cxx { + template <> + struct hash<CVC4::Node> { + 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 <class AttrKind> +inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) { + return NodeManager::currentNM()->getAttribute(*this, AttrKind()); +} + +template <class AttrKind> +inline bool Node::hasAttribute(const AttrKind&, + typename AttrKind::value_type* ret) { + return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); +} + +template <class AttrKind> +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 <stdint.h> -#include "config.h" -#include "context/context.h" -#include "expr/node.h" - -namespace CVC4 { -namespace expr { - -template <class value_type> -class AttrTables; - -// global (or TSS) -extern CDMap<uint64_t> g_hash_bool; -extern CDMap<uint64_t> g_hash_int; -extern CDMap<Node> g_hash_expr; -extern CDMap<void*> g_hash_ptr; - -template <class T> -class AttrTable; - -template <> -class AttrTable<bool> { -public: - class BitAccessor { - uint64_t& d_word; - unsigned d_bit; - public: - BitAccessor& operator=(bool b); - // continue... - }; - - // bool specialization - static CDMap<uint64_t> *s_hash; - - template <class Attr> - BitAccessor& find(Node e, const Attr&); - - template <class Attr> - bool find(Node e, const Attr&) const; -}; - -template <> -class AttrTable<uint64_t> { -public: - // int(egral) specialization - static CDMap<uint64_t> *s_hash; - uint64_t& find(Node); - uint64_t& find(Node) const; -}; - -template <class T> -class AttrTable<T*> { - // pointer specialization - static CDMap<void*> *s_hash; -public: -}; - -template <> -class AttrTable<Node> { -public: - // Node specialization - static CDMap<Node> *s_hash; - Node find(Node); -}; - -CDMap<uint64_t>* AttrTable<bool>::s_hash = &g_hash_bool; -CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int; -CDMap<Node>* AttrTable<Node>::s_hash = &g_hash_expr; - -template <class T> -CDMap<void*>* AttrTable<T*>::s_hash = &g_hash_ptr; - -template <class Attr> -class AttributeTable { - typedef typename Attr::value_type value_type; - - AttrTable<value_type>& 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<nchild_thresh>::dealloc() { template <unsigned nchild_thresh> NodeBuilder<nchild_thresh>::operator Node() {// not const Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Assert(d_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<Node>& children) { +Node NodeManager::mkNode(Kind kind, const vector<Node>& 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 <vector> +#include <string> #include <ext/hash_set> -#include "node.h" -#include "kind.h" +#include "expr/node.h" +#include "expr/kind.h" namespace __gnu_cxx { -template<> + template<> struct hash<CVC4::NodeValue*> { 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*, __gnu_cxx::hash<NodeValue*>, 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<Node>& children); // variables are special, because duplicates are permitted + Node mkVar(const Type* type, std::string name); + Node mkVar(const Type* type); Node mkVar(); -}; + template <class AttrKind> + inline typename AttrKind::value_type getAttribute(const Node& n, + const AttrKind&); + + template <class AttrKind> + inline bool hasAttribute(const Node& n, + const AttrKind&, + typename AttrKind::value_type* = NULL); + + template <class AttrKind> + 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 <class AttrKind> +inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n, + const AttrKind&) { + return d_am.getAttribute(n, AttrKind()); +} + +template <class AttrKind> +inline bool NodeManager::hasAttribute(const Node& n, + const AttrKind&, + typename AttrKind::value_type* ret) { + return d_am.hasAttribute(n, AttrKind(), ret); +} + +template <class AttrKind> +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 <sstream> 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<const Type*>& 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<std::string> 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 <ext/hash_map> -namespace __gnu_cxx { -template<> - struct hash<CVC4::Node> { - 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 */ |