# ------------
# 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
noinst_LTLIBRARIES = libexpr.la
libexpr_la_SOURCES = \
- attr_type.h \
- attr_var_name.h \
node.h \
node_builder.h \
expr.h \
node_value.h \
node_manager.h \
expr_manager.h \
- node_attribute.h \
+ attribute.h \
+ attribute.cpp \
@srcdir@/kind.h \
node.cpp \
node_builder.cpp \
+++ /dev/null
-/********************* */
-/** 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 */
+++ /dev/null
-/********************* */
-/** 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 */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
namespace CVC4 {
-ExprManager::ExprManager()
- : d_nm(new NodeManager()) {
+ExprManager::ExprManager() :
+ d_nm(new NodeManager()) {
}
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())));
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();
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 {
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:
#include "util/Assert.h"
namespace CVC4 {
- class Node;
-}/* CVC4 namespace */
-namespace CVC4 {
+class Node;
inline std::ostream& operator<<(std::ostream&, const Node&);
class Node {
friend class NodeValue;
+ friend class SoftNode;
/** A convenient null-valued encapsulated pointer */
static Node s_null;
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.
}/* 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 {
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 */
+++ /dev/null
-/********************* */
-/** 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 */
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;
}
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) {
#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()) {
}
// 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);
}
#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;
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);
public:
- NodeManager();
+ NodeManager() : d_am(this) {
+ poolInsert( &NodeValue::s_null );
+ }
static NodeManager* currentNM() { return s_current; }
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 */
** reference count on NodeValue instances and
**/
-#include "node_value.h"
+#include "expr/node_value.h"
+#include "expr/node.h"
#include <sstream>
using namespace std;
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() {
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()) {
* 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) */
unsigned d_rc : 8;
/** Kind of the expression */
- unsigned d_kind : 8;
+ unsigned d_kind : KINDBITS;
/** Number of children */
unsigned d_nchildren : 16;
}
};
-
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 */
--- /dev/null
+/********************* -*- 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 */
* Class encapsulating CVC4 expression types.
*/
class Type {
- public:
+public:
/** Comparision for equality */
bool operator==(const Type& t) const;
* @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 */
}
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*
}
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 {
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());
}
}
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) ) ;
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;
}
#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 {
}
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();
}
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();
}
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 */
$(TEST_DEPS_DIST) \
$(TEST_DEPS_NODIST)
-@mk_include@ @srcdir@/Makefile.tests
-
if HAVE_CXXTESTGEN
AM_CPPFLAGS = \
AM_LDFLAGS_PUBLIC = \
@abs_top_builddir@/src/libcvc4.la
-TESTS = $(UNIT_TESTS)
-
EXTRA_DIST = \
no_cxxtest \
$(TEST_DEPS_DIST)
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
$(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
-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)
d_scope = new NodeManagerScope(d_nm);
}
- void tearDown(){
+ void tearDown() {
delete d_nm;
delete d_scope;
}
Node::null();
}
- void testIsNull(){
+ void testIsNull() {
/* bool isNull() const; */
Node a = Node::null();
Node e(Node::null());
}
- void testDestructor(){
+ void testDestructor() {
/* No access to internals ?
* Makes sense to only test that this is crash free.
*/
}
/*tests: bool operator==(const Node& e) const */
- void testOperatorEquals(){
+ void testOperatorEquals() {
Node a, b, c;
b = d_nm->mkVar();
}
/* operator!= */
- void testOperatorNotEquals(){
+ void testOperatorNotEquals() {
Node a, b, c;
}
- void testOperatorSquare(){
+ void testOperatorSquare() {
/*Node operator[](int i) const */
//Basic bounds check on a node w/out children
}
/*tests: Node& operator=(const Node&); */
- void testOperatorAssign(){
+ void testOperatorAssign() {
Node a, b;
Node c = d_nm->mkNode(NOT);
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.
*/
std::vector<Node> chain;
int N = 500;
Node curr = d_nm->mkNode(NULL_EXPR);
- for(int i=0;i<N;i++){
+ for(int i=0;i<N;i++) {
chain.push_back(curr);
curr = d_nm->mkNode(AND,curr);
}
- for(int i=0;i<N;i++){
- for(int j=i+1;j<N;j++){
+ for(int i=0;i<N;i++) {
+ for(int j=i+1;j<N;j++) {
Node chain_i = chain[i];
Node chain_j = chain[j];
TS_ASSERT(chain_i<chain_j);
}
- void testHash(){
+ void testHash() {
/* Not sure how to test this except survial... */
Node a = d_nm->mkNode(ITE);
Node b = d_nm->mkNode(ITE);
- void testEqExpr(){
+ void testEqExpr() {
/*Node eqExpr(const Node& right) const;*/
Node left = d_nm->mkNode(TRUE);
TS_ASSERT(eq[1] == right);
}
- void testNotExpr(){
+ void testNotExpr() {
/* Node notExpr() const;*/
Node child = d_nm->mkNode(TRUE);
TS_ASSERT(parent[0] == child);
}
- void testAndExpr(){
+ void testAndExpr() {
/*Node andExpr(const Node& right) const;*/
Node left = d_nm->mkNode(TRUE);
}
- void testOrExpr(){
+ void testOrExpr() {
/*Node orExpr(const Node& right) const;*/
Node left = d_nm->mkNode(TRUE);
}
- void testIteExpr(){
+ void testIteExpr() {
/*Node iteExpr(const Node& thenpart, const Node& elsepart) const;*/
Node cnd = d_nm->mkNode(PLUS);
TS_ASSERT(*(++(++ite.begin())) == elseBranch);
}
- void testIffExpr(){
+ void testIffExpr() {
/* Node iffExpr(const Node& right) const; */
Node left = d_nm->mkNode(TRUE);
}
- 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)));
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)));
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);
#include <cxxtest/TestSuite.h>
+#include <string>
+
+#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<Test1, std::string> TestStringAttr1;
+typedef Attribute<Test2, std::string> TestStringAttr2;
+
+typedef Attribute<Test3, bool> TestFlag1;
+typedef Attribute<Test4, bool> 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;
}
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<string>::s_id == 3);
+
+ TS_ASSERT(TypeAttr::s_id == 0);
+ TS_ASSERT(attr::LastAttributeId<void*>::s_id == 1);
+
+ TS_ASSERT(TestFlag1::s_id == 0);
+ TS_ASSERT(TestFlag2::s_id == 1);
+ TS_ASSERT(attr::LastAttributeId<bool>::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()));
+
+ }
};
projects / cvc5.git / commitdiff