summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/Makefile.am6
-rw-r--r--src/expr/attribute.cpp2
-rw-r--r--src/expr/attribute.h17
-rw-r--r--src/expr/expr_manager_template.cpp32
-rw-r--r--src/expr/node.h20
-rw-r--r--src/expr/node_builder.h44
-rw-r--r--src/expr/node_manager.h150
-rw-r--r--src/expr/node_value.h33
-rw-r--r--src/expr/type.cpp36
-rw-r--r--src/expr/type.h16
-rw-r--r--src/expr/type_node.cpp62
-rw-r--r--src/expr/type_node.h437
-rw-r--r--test/unit/expr/attribute_black.h14
-rw-r--r--test/unit/expr/attribute_white.h6
-rw-r--r--test/unit/expr/node_black.h14
-rw-r--r--test/unit/expr/node_builder_black.h4
-rw-r--r--test/unit/expr/node_manager_black.h72
-rw-r--r--test/unit/theory/theory_black.h4
-rw-r--r--test/unit/theory/theory_uf_white.h4
19 files changed, 791 insertions, 182 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 0abeebb9e..404334199 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -8,9 +8,12 @@ noinst_LTLIBRARIES = libexpr.la
libexpr_la_SOURCES = \
node.h \
node.cpp \
+ type_node.h \
+ type_node.cpp \
node_builder.h \
@srcdir@/expr.h \
type.h \
+ type.cpp \
node_value.h \
node_manager.h \
@srcdir@/expr_manager.h \
@@ -22,7 +25,6 @@ libexpr_la_SOURCES = \
@srcdir@/expr_manager.cpp \
node_value.cpp \
@srcdir@/expr.cpp \
- type.cpp \
command.h \
command.cpp \
declaration_scope.h \
@@ -36,6 +38,8 @@ EXTRA_DIST = \
@srcdir@/expr.h \
@srcdir@/expr_manager.cpp \
@srcdir@/expr.cpp \
+ @srcdir@/type.h \
+ @srcdir@/type.cpp \
kind_template.h \
metakind_template.h \
expr_manager_template.h \
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index e5a50591f..bc724cdd1 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -30,6 +30,7 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
deleteFromTable(d_ints, nv);
deleteFromTable(d_tnodes, nv);
deleteFromTable(d_nodes, nv);
+ deleteFromTable(d_types, nv);
deleteFromTable(d_strings, nv);
deleteFromTable(d_ptrs, nv);
@@ -59,6 +60,7 @@ void AttributeManager::deleteAllAttributes() {
deleteAllFromTable(d_ints);
deleteAllFromTable(d_tnodes);
deleteAllFromTable(d_nodes);
+ deleteAllFromTable(d_types);
deleteAllFromTable(d_strings);
deleteAllFromTable(d_ptrs);
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 4250bb3ef..f231b701c 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -18,6 +18,7 @@
/* There are strong constraints on ordering of declarations of
* attributes and nodes due to template use */
#include "expr/node.h"
+#include "expr/type_node.h"
#ifndef __CVC4__EXPR__ATTRIBUTE_H
#define __CVC4__EXPR__ATTRIBUTE_H
@@ -59,6 +60,8 @@ class AttributeManager {
AttrHash<TNode> d_tnodes;
/** Underlying hash table for node-valued attributes */
AttrHash<Node> d_nodes;
+ /** Underlying hash table for types attributes */
+ AttrHash<TypeNode> d_types;
/** Underlying hash table for string-valued attributes */
AttrHash<std::string> d_strings;
/** Underlying hash table for pointer-valued attributes */
@@ -241,6 +244,18 @@ struct getTable<Node, false> {
}
};
+/** Access the "d_types" member of AttributeManager. */
+template <>
+struct getTable<TypeNode, false> {
+ typedef AttrHash<TypeNode> table_type;
+ static inline table_type& get(AttributeManager& am) {
+ return am.d_types;
+ }
+ static inline const table_type& get(const AttributeManager& am) {
+ return am.d_types;
+ }
+};
+
/** Access the "d_strings" member of AttributeManager. */
template <>
struct getTable<std::string, false> {
@@ -313,7 +328,7 @@ struct getTable<TNode, true> {
}
};
-/** Access the "d_nodes" member of AttributeManager. */
+/** Access the "d_cdnodes" member of AttributeManager. */
template <>
struct getTable<Node, true> {
typedef CDAttrHash<Node> table_type;
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 7407043d2..5d50dd100 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -48,12 +48,12 @@ ExprManager::~ExprManager() {
BooleanType ExprManager::booleanType() const {
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->booleanType();
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()));
}
KindType ExprManager::kindType() const {
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->kindType();
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()));
}
Expr ExprManager::mkExpr(Kind kind) {
@@ -154,46 +154,58 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
/** Make a function type from domain to range. */
FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) {
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkFunctionType(domain, range);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)));
}
/** Make a function type with input types from argTypes. */
FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
Assert( argTypes.size() >= 1 );
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkFunctionType(argTypes, range);
+ std::vector<TypeNode> argTypeNodes;
+ for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
+ argTypeNodes.push_back(*argTypes[i].d_typeNode);
+ }
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode)));
}
FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
Assert( sorts.size() >= 2 );
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkFunctionType(sorts);
+ std::vector<TypeNode> sortNodes;
+ for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
+ sortNodes.push_back(*sorts[i].d_typeNode);
+ }
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes)));
}
FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
Assert( sorts.size() >= 1 );
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkPredicateType(sorts);
+ std::vector<TypeNode> sortNodes;
+ for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
+ sortNodes.push_back(*sorts[i].d_typeNode);
+ }
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)));
}
SortType ExprManager::mkSort(const std::string& name) {
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkSort(name);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
}
Type ExprManager::getType(const Expr& e) {
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->getType(e.getNode());
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode())));
}
Expr ExprManager::mkVar(const std::string& name, const Type& type) {
NodeManagerScope nms(d_nodeManager);
- return Expr(this, d_nodeManager->mkVarPtr(name, type));
+ return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode));
}
Expr ExprManager::mkVar(const Type& type) {
NodeManagerScope nms(d_nodeManager);
- return Expr(this, d_nodeManager->mkVarPtr(type));
+ return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
}
unsigned ExprManager::minArity(Kind kind) {
diff --git a/src/expr/node.h b/src/expr/node.h
index 27756da5b..f8d9117c7 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -33,7 +33,7 @@
namespace CVC4 {
-class Type;
+class TypeNode;
class NodeManager;
template <bool ref_count>
@@ -229,7 +229,7 @@ public:
* Returns the unique id of this node
* @return the ud
*/
- uint64_t getId() const {
+ unsigned getId() const {
return d_nv->getId();
}
@@ -247,7 +247,7 @@ public:
* Returns the type of this node.
* @return the type
*/
- Type getType() const;
+ TypeNode getType() const;
/**
* Returns the kind of this node.
@@ -322,16 +322,16 @@ public:
const typename AttrKind::value_type& value);
/** Iterator allowing for scanning through the children. */
- typedef typename expr::NodeValue::iterator<ref_count> iterator;
+ typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > iterator;
/** Constant iterator allowing for scanning through the children. */
- typedef typename expr::NodeValue::iterator<ref_count> const_iterator;
+ typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > const_iterator;
/**
* Returns the iterator pointing to the first child.
* @return the iterator
*/
inline iterator begin() {
- return d_nv->begin<ref_count>();
+ return d_nv->begin< NodeTemplate<ref_count> >();
}
/**
@@ -340,7 +340,7 @@ public:
* @return the end of the children iterator.
*/
inline iterator end() {
- return d_nv->end<ref_count>();
+ return d_nv->end< NodeTemplate<ref_count> >();
}
/**
@@ -348,7 +348,7 @@ public:
* @return the const_iterator
*/
inline const_iterator begin() const {
- return d_nv->begin<ref_count>();
+ return d_nv->begin< NodeTemplate<ref_count> >();
}
/**
@@ -357,7 +357,7 @@ public:
* @return the end of the children const_iterator.
*/
inline const_iterator end() const {
- return d_nv->end<ref_count>();
+ return d_nv->end< NodeTemplate<ref_count> >();
}
/**
@@ -814,7 +814,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const {
}
template <bool ref_count>
-Type NodeTemplate<ref_count>::getType() const {
+TypeNode NodeTemplate<ref_count>::getType() const {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
"Perhaps a public-facing function is missing a NodeManagerScope ?" );
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 09e72660e..cefeb2fe2 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -173,6 +173,7 @@
/* strong dependency; make sure node is included first */
#include "node.h"
+#include "type_node.h"
#ifndef __CVC4__NODE_BUILDER_H
#define __CVC4__NODE_BUILDER_H
@@ -410,21 +411,21 @@ public:
// override this in a derived class.
inline ~NodeBuilderBase();
- typedef expr::NodeValue::iterator<true> iterator;
- typedef expr::NodeValue::iterator<true> const_iterator;
+ typedef expr::NodeValue::iterator< NodeTemplate<true> > iterator;
+ typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator;
/** Get the begin-const-iterator of this Node-under-construction. */
inline const_iterator begin() const {
Assert(!isUsed(), "NodeBuilder is one-shot only; "
"attempt to access it after conversion");
- return d_nv->begin<true>();
+ return d_nv->begin< NodeTemplate<true> >();
}
/** Get the end-const-iterator of this Node-under-construction. */
inline const_iterator end() const {
Assert(!isUsed(), "NodeBuilder is one-shot only; "
"attempt to access it after conversion");
- return d_nv->end<true>();
+ return d_nv->end< NodeTemplate<true> >();
}
/** Get the kind of this Node-under-construction. */
@@ -505,6 +506,14 @@ public:
return append(n);
}
+ /** Append a sequence of children to this TypeNode-under-construction. */
+ inline Builder&
+ append(const std::vector<TypeNode>& children) {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; "
+ "attempt to access it after conversion");
+ return append(children.begin(), children.end());
+ }
+
/** Append a sequence of children to this Node-under-construction. */
template <bool ref_count>
inline Builder&
@@ -537,6 +546,18 @@ public:
return static_cast<Builder&>(*this);
}
+ /** Append a child to this Node-under-construction. */
+ Builder& append(const TypeNode& typeNode) {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; "
+ "attempt to access it after conversion");
+ Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node");
+ allocateNvIfNecessaryForAppend();
+ expr::NodeValue* nv = typeNode.d_nv;
+ nv->inc();
+ d_nv->d_children[d_nv->d_nchildren++] = nv;
+ return static_cast<Builder&>(*this);
+ }
+
private:
/** Construct the node value out of the node builder */
@@ -553,6 +574,10 @@ public:
Node* constructNodePtr();
Node* constructNodePtr() const;
+ /** Construction of the TypeNode out of the node builder */
+ TypeNode constructTypeNode();
+ TypeNode constructTypeNode() const;
+
// two versions, so we can support extraction from (const)
// NodeBuilders which are temporaries appearing as rvalues
operator Node();
@@ -1245,6 +1270,17 @@ void NodeBuilderBase<Builder>::decrRefCounts() {
d_inlineNv.d_nchildren = 0;
}
+
+template <class Builder>
+TypeNode NodeBuilderBase<Builder>::constructTypeNode() {
+ return TypeNode(constructNV());
+}
+
+template <class Builder>
+TypeNode NodeBuilderBase<Builder>::constructTypeNode() const {
+ return TypeNode(constructNV());
+}
+
template <class Builder>
Node NodeBuilderBase<Builder>::constructNode() {
return Node(constructNV());
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 138a87493..cbfcdd110 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -20,6 +20,7 @@
/* circular dependency; force node.h first */
#include "expr/attribute.h"
#include "expr/node.h"
+#include "expr/type_node.h"
#ifndef __CVC4__NODE_MANAGER_H
#define __CVC4__NODE_MANAGER_H
@@ -32,7 +33,6 @@
#include "expr/metakind.h"
#include "expr/node_value.h"
#include "context/context.h"
-#include "expr/type.h"
namespace CVC4 {
@@ -206,7 +206,7 @@ class NodeManager {
// NodeManager's attributes. These aren't exposed outside of this
// class; use the getters.
- typedef expr::Attribute<TypeTag, Node> TypeAttr;
+ typedef expr::Attribute<TypeTag, TypeNode> TypeAttr;
typedef expr::Attribute<AtomicTag, bool> AtomicAttr;
/**
@@ -290,12 +290,13 @@ public:
* lookup is done on the name. If you mkVar("a", type) and then
* mkVar("a", type) again, you have two variables.
*/
- Node mkVar(const std::string& name, const Type& type);
- Node* mkVarPtr(const std::string& name, const Type& type);
+ Node mkVar(const std::string& name, const TypeNode& type);
+ Node* mkVarPtr(const std::string& name, const TypeNode& type);
/** Create a variable with the given type. */
- Node mkVar(const Type& type);
- Node* mkVarPtr(const Type& type);
+ Node mkVar(const TypeNode& type);
+ Node* mkVarPtr(const TypeNode& type);
+
/**
* Create a constant of type T. It will have the appropriate
@@ -304,6 +305,19 @@ public:
template <class T>
Node mkConst(const T&);
+ template <class T>
+ TypeNode mkTypeConst(const T&);
+
+ template <class NodeClass, class T>
+ NodeClass mkConstInternal(const T&);
+
+ /** Create a type-variable */
+ TypeNode mkTypeVar();
+ TypeNode mkTypeVar(const std::string& name);
+
+ /** Create a node with no children. */
+ TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
+
/**
* Determine whether Nodes of a particular Kind have operators.
* @returns true if Nodes of Kind k have operators.
@@ -433,10 +447,10 @@ public:
const typename AttrKind::value_type& value);
/** Get the (singleton) type for booleans. */
- inline BooleanType booleanType();
+ inline TypeNode booleanType();
/** Get the (singleton) type for sorts. */
- inline KindType kindType();
+ inline TypeNode kindType();
/**
* Make a function type from domain to range.
@@ -445,7 +459,7 @@ public:
* @param range the range type
* @returns the functional type domain -> range
*/
- inline Type mkFunctionType(const Type& domain, const Type& range);
+ inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
/**
* Make a function type with input types from
@@ -455,7 +469,7 @@ public:
* @param range the range type
* @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
*/
- inline Type mkFunctionType(const std::vector<Type>& argTypes, const Type& range);
+ inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range);
/**
* Make a function type with input types from
@@ -463,7 +477,7 @@ public:
* <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
* at least 2 elements.
*/
- inline Type mkFunctionType(const std::vector<Type>& sorts);
+ inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
/**
* Make a predicate type with input types from
@@ -471,18 +485,18 @@ public:
* <code>BOOLEAN</code>. <code>sorts</code> must have at least one
* element.
*/
- inline Type mkPredicateType(const std::vector<Type>& sorts);
+ inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
/** Make a new sort. */
- inline Type mkSort();
+ inline TypeNode mkSort();
/** Make a new sort with the given name. */
- inline Type mkSort(const std::string& name);
+ inline TypeNode mkSort(const std::string& name);
/**
* Get the type for the given node.
*/
- inline Type getType(TNode n);
+ inline TypeNode getType(TNode n);
/**
* Returns true if this node is atomic (has no more Boolean structure)
@@ -589,63 +603,64 @@ NodeManager::setAttribute(TNode n, const AttrKind&,
/** Get the (singleton) type for booleans. */
-inline BooleanType NodeManager::booleanType() {
- return Type(this, new Node(mkConst<TypeConstant>(BOOLEAN_TYPE)));
+inline TypeNode NodeManager::booleanType() {
+ return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
}
/** Get the (singleton) type for sorts. */
-inline KindType NodeManager::kindType() {
- return Type(this, new Node(mkConst<TypeConstant>(KIND_TYPE)));
+inline TypeNode NodeManager::kindType() {
+ return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
}
-/** Make a function type from domain to range.
- * TODO: Function types should be unique for this manager. */
-inline Type NodeManager::mkFunctionType(const Type& domain, const Type& range) {
- return Type(this, mkNodePtr(kind::FUNCTION_TYPE, *domain.d_typeNode, *range.d_typeNode));
+/** Make a function type from domain to range. */
+inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
+ std::vector<TypeNode> sorts;
+ sorts.push_back(domain);
+ sorts.push_back(range);
+ return mkFunctionType(sorts);
}
-inline Type NodeManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
+inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
Assert(argTypes.size() >= 1);
- std::vector<Type> sorts(argTypes);
+ std::vector<TypeNode> sorts(argTypes);
sorts.push_back(range);
return mkFunctionType(sorts);
}
-
-inline Type
-NodeManager::mkFunctionType(const std::vector<Type>& sorts) {
+inline TypeNode
+NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
Assert(sorts.size() >= 2);
- std::vector<Node> sortNodes;
+ std::vector<TypeNode> sortNodes;
for (unsigned i = 0; i < sorts.size(); ++ i) {
- sortNodes.push_back(*(sorts[i].d_typeNode));
+ sortNodes.push_back(sorts[i]);
}
- return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes));
+ return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
}
-inline Type
-NodeManager::mkPredicateType(const std::vector<Type>& sorts) {
+inline TypeNode
+NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
Assert(sorts.size() >= 1);
- std::vector<Node> sortNodes;
+ std::vector<TypeNode> sortNodes;
for (unsigned i = 0; i < sorts.size(); ++ i) {
- sortNodes.push_back(*(sorts[i].d_typeNode));
+ sortNodes.push_back(sorts[i]);
}
- sortNodes.push_back(*(booleanType().d_typeNode));
- return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes));
+ sortNodes.push_back(booleanType());
+ return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
}
-inline Type NodeManager::mkSort() {
- return Type(this, mkVarPtr(kindType()));
+inline TypeNode NodeManager::mkSort() {
+ return mkTypeVar();
}
-inline Type NodeManager::mkSort(const std::string& name) {
- return Type(this, mkVarPtr(name, kindType()));
+inline TypeNode NodeManager::mkSort(const std::string& name) {
+ return mkTypeVar(name);
}
-inline Type NodeManager::getType(TNode n) {
- Node* typeNode = new Node;
- getAttribute(n, TypeAttr(), *typeNode);
+inline TypeNode NodeManager::getType(TNode n) {
+ TypeNode typeNode;
+ getAttribute(n, TypeAttr(), typeNode);
// TODO: Type computation
- return Type(this, typeNode);
+ return typeNode;
}
inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
@@ -815,34 +830,61 @@ inline Node* NodeManager::mkNodePtr(Kind kind,
return NodeBuilder<>(this, kind).append(children).constructNodePtr();
}
-inline Node NodeManager::mkVar(const std::string& name, const Type& type) {
+// N-ary version for types
+inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector<TypeNode>& children) {
+ return NodeBuilder<>(this, kind).append(children).constructTypeNode();
+}
+
+
+inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
Node n = mkVar(type);
n.setAttribute(expr::VarNameAttr(), name);
return n;
}
-inline Node* NodeManager::mkVarPtr(const std::string& name, const Type& type) {
+inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) {
Node* n = mkVarPtr(type);
n->setAttribute(expr::VarNameAttr(), name);
return n;
}
-inline Node NodeManager::mkVar(const Type& type) {
+inline Node NodeManager::mkVar(const TypeNode& type) {
Node n = NodeBuilder<0>(this, kind::VARIABLE);
- n.setAttribute(TypeAttr(), *type.d_typeNode);
+ n.setAttribute(TypeAttr(), type);
return n;
}
-inline Node* NodeManager::mkVarPtr(const Type& type) {
+inline TypeNode NodeManager::mkTypeVar(const std::string& name) {
+ TypeNode type = mkTypeVar();
+ type.setAttribute(expr::VarNameAttr(), name);
+ return type;
+}
+
+inline TypeNode NodeManager::mkTypeVar() {
+ TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
+ return type;
+}
+
+inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
- n->setAttribute(TypeAttr(), *type.d_typeNode);
+ n->setAttribute(TypeAttr(), type);
return n;
}
template <class T>
Node NodeManager::mkConst(const T& val) {
- // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
+ return mkConstInternal<Node, T>(val);
+}
+
+template <class T>
+TypeNode NodeManager::mkTypeConst(const T& val) {
+ return mkConstInternal<TypeNode, T>(val);
+}
+
+template <class NodeClass, class T>
+NodeClass NodeManager::mkConstInternal(const T& val) {
+ // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
NVStorage<1> nvStorage;
expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
@@ -855,7 +897,7 @@ Node NodeManager::mkConst(const T& val) {
expr::NodeValue* nv = poolLookup(&nvStack);
if(nv != NULL) {
- return Node(nv);
+ return NodeClass(nv);
}
nv = (expr::NodeValue*)
@@ -876,7 +918,7 @@ Node NodeManager::mkConst(const T& val) {
Debug("gc") << "creating node value " << nv
<< " [" << nv->d_id << "]: " << *nv << "\n";
- return Node(nv);
+ return NodeClass(nv);
}
}/* CVC4 namespace */
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index a998dd8e4..260a9daae 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -34,6 +34,7 @@
namespace CVC4 {
template <bool ref_count> class NodeTemplate;
+class TypeNode;
template <class Builder> class NodeBuilderBase;
template <unsigned N> class NodeBuilder;
class AndNodeBuilder;
@@ -101,6 +102,7 @@ class NodeValue {
// todo add exprMgr ref in debug case
template <bool> friend class ::CVC4::NodeTemplate;
+ friend class ::CVC4::TypeNode;
template <class Builder> friend class ::CVC4::NodeBuilderBase;
template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder;
friend class ::CVC4::NodeManager;
@@ -137,13 +139,13 @@ private:
const_nv_iterator nv_begin() const;
const_nv_iterator nv_end() const;
- template <bool ref_count>
+ template <typename T>
class iterator {
const_nv_iterator d_i;
public:
explicit iterator(const_nv_iterator i) : d_i(i) {}
- inline CVC4::NodeTemplate<ref_count> operator*();
+ inline T operator*();
bool operator==(const iterator& i) {
return d_i == i.d_i;
@@ -172,11 +174,11 @@ private:
public:
- template <bool ref_count>
- inline iterator<ref_count> begin() const;
+ template <typename T>
+ inline iterator<T> begin() const;
- template <bool ref_count>
- inline iterator<ref_count> end() const;
+ template <typename T>
+ inline iterator<T> end() const;
/**
* Hash this NodeValue. For hash_maps, hash_sets, etc.. but this is
@@ -317,18 +319,18 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
return d_children + d_nchildren;
}
-template <bool ref_count>
-inline NodeValue::iterator<ref_count> NodeValue::begin() const {
+template <typename T>
+inline NodeValue::iterator<T> NodeValue::begin() const {
NodeValue* const* firstChild = d_children;
if(getMetaKind() == kind::metakind::PARAMETERIZED) {
++firstChild;
}
- return iterator<ref_count>(firstChild);
+ return iterator<T>(firstChild);
}
-template <bool ref_count>
-inline NodeValue::iterator<ref_count> NodeValue::end() const {
- return iterator<ref_count>(d_children + d_nchildren);
+template <typename T>
+inline NodeValue::iterator<T> NodeValue::end() const {
+ return iterator<T>(d_children + d_nchildren);
}
inline bool NodeValue::isBeingDeleted() const {
@@ -349,13 +351,14 @@ inline NodeValue* NodeValue::getChild(int i) const {
}/* CVC4 namespace */
#include "expr/node.h"
+#include "expr/type_node.h"
namespace CVC4 {
namespace expr {
-template <bool ref_count>
-inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*() {
- return NodeTemplate<ref_count>(*d_i);
+template <typename T>
+inline T NodeValue::iterator<T>::operator*() {
+ return T(*d_i);
}
inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 63d270ac1..98a7e88e7 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -15,6 +15,7 @@
#include "expr/node_manager.h"
#include "expr/type.h"
+#include "expr/type_node.h"
#include "expr/type_constant.h"
#include "util/Assert.h"
#include <string>
@@ -26,12 +27,12 @@ std::ostream& operator<<(std::ostream& out, const Type& e) {
return out;
}
-Type Type::makeType(NodeTemplate<false> typeNode) const
+Type Type::makeType(const TypeNode& typeNode) const
{
- return Type(d_nodeManager, new Node(typeNode));
+ return Type(d_nodeManager, new TypeNode(typeNode));
}
-Type::Type(NodeManager* nm, NodeTemplate<true>* node)
+Type::Type(NodeManager* nm, TypeNode* node)
: d_typeNode(node),
d_nodeManager(nm)
{
@@ -43,19 +44,19 @@ Type::~Type() {
}
Type::Type()
-: d_typeNode(new Node()),
+: d_typeNode(new TypeNode()),
d_nodeManager(NULL)
{
}
Type::Type(uintptr_t n)
-: d_typeNode(new Node()),
+: d_typeNode(new TypeNode()),
d_nodeManager(NULL) {
AlwaysAssert(n == 0);
}
Type::Type(const Type& t)
-: d_typeNode(new Node(*t.d_typeNode)),
+: d_typeNode(new TypeNode(*t.d_typeNode)),
d_nodeManager(t.d_nodeManager)
{
}
@@ -95,8 +96,7 @@ void Type::toStream(std::ostream& out) const {
/** Is this the Boolean type? */
bool Type::isBoolean() const {
NodeManagerScope nms(d_nodeManager);
- return d_typeNode->getKind() == kind::TYPE_CONSTANT
- && d_typeNode->getConst<TypeConstant>() == BOOLEAN_TYPE;
+ return d_typeNode->isBoolean();
}
/** Cast to a Boolean type */
@@ -109,14 +109,14 @@ Type::operator BooleanType() const {
/** Is this a function type? */
bool Type::isFunction() const {
NodeManagerScope nms(d_nodeManager);
- return d_typeNode->getKind() == kind::FUNCTION_TYPE;
+ return d_typeNode->isFunction();
}
/** Is this a predicate type? NOTE: all predicate types are also
function types. */
bool Type::isPredicate() const {
NodeManagerScope nms(d_nodeManager);
- return isFunction() && ((FunctionType)*this).getRangeType().isBoolean();
+ return d_typeNode->isPredicate();
}
/** Cast to a function type */
@@ -129,8 +129,7 @@ Type::operator FunctionType() const {
/** Is this a sort kind */
bool Type::isSort() const {
NodeManagerScope nms(d_nodeManager);
- return d_typeNode->getKind() == kind::VARIABLE &&
- d_typeNode->getType().isKind();
+ return d_typeNode->isSort();
}
/** Cast to a sort type */
@@ -143,8 +142,7 @@ Type::operator SortType() const {
/** Is this a kind type (i.e., the type of a type)? */
bool Type::isKind() const {
NodeManagerScope nms(d_nodeManager);
- return d_typeNode->getKind() == kind::TYPE_CONSTANT
- && d_typeNode->getConst<TypeConstant>() == KIND_TYPE;
+ return d_typeNode->isKind();
}
/** Cast to a kind type */
@@ -157,15 +155,19 @@ Type::operator KindType() const {
std::vector<Type> FunctionType::getArgTypes() const {
NodeManagerScope nms(d_nodeManager);
std::vector<Type> args;
- for (unsigned i = 0, i_end = d_typeNode->getNumChildren() - 1; i < i_end; ++ i) {
- args.push_back(makeType((*d_typeNode)[i]));
+ std::vector<TypeNode> argNodes = d_typeNode->getArgTypes();
+ std::vector<TypeNode>::iterator it = argNodes.begin();
+ std::vector<TypeNode>::iterator it_end = argNodes.end();
+ for(; it != it_end; ++ it) {
+ args.push_back(makeType(*it));
}
return args;
}
Type FunctionType::getRangeType() const {
NodeManagerScope nms(d_nodeManager);
- return makeType((*d_typeNode)[d_typeNode->getNumChildren()-1]);
+ Assert(isFunction());
+ return makeType(d_typeNode->getRangeType());
}
void BooleanType::toStream(std::ostream& out) const {
diff --git a/src/expr/type.h b/src/expr/type.h
index 4f9142698..5cbe0613a 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -29,7 +29,7 @@
namespace CVC4 {
class NodeManager;
-template <bool ref_count> class NodeTemplate;
+class TypeNode;
class BooleanType;
class FunctionType;
@@ -41,12 +41,12 @@ class SortType;
*/
class CVC4_PUBLIC Type {
- friend class NodeManager;
+ friend class ExprManager;
protected:
/** The internal expression representation */
- NodeTemplate<true>* d_typeNode;
+ TypeNode* d_typeNode;
/** The responsible expression manager */
NodeManager* d_nodeManager;
@@ -54,14 +54,14 @@ protected:
/**
* Construct a new type given the typeNode;
*/
- Type makeType(NodeTemplate<false> typeNode) const;
+ Type makeType(const TypeNode& typeNode) const;
/**
* Constructor for internal purposes.
* @param em the expression manager that handles this expression
* @param node the actual expression node pointer for this type
*/
- Type(NodeManager* em, NodeTemplate<true>* typeNode);
+ Type(NodeManager* em, TypeNode* typeNode);
public:
@@ -160,12 +160,6 @@ public:
/** Get the range type (i.e., the type of the result). */
Type getRangeType() const;
- /** Is this as function type? (Returns true.) */
- bool isFunction() const;
-
- /** Is this as predicate type? (Returns true if range is Boolean.) */
- bool isPredicate() const;
-
/**
* Outputs a string representation of this type to the stream,
* in the format "D -> R" or "(A, B, C) -> R".
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
new file mode 100644
index 000000000..87b6ed58a
--- /dev/null
+++ b/src/expr/type_node.cpp
@@ -0,0 +1,62 @@
+/********************* */
+/** node.cpp
+ ** Original author: dejan
+ ** 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.
+ **
+ ** Reference-counted encapsulation of a pointer to node information.
+ **/
+
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+TypeNode TypeNode::s_null(&expr::NodeValue::s_null);
+
+bool TypeNode::isBoolean() const {
+ return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE;
+}
+
+/** Is this a function type? */
+bool TypeNode::isFunction() const {
+ return getKind() == kind::FUNCTION_TYPE;
+}
+
+/** Is this a predicate type? NOTE: all predicate types are also
+ function types. */
+bool TypeNode::isPredicate() const {
+ return isFunction() && getRangeType().isBoolean();
+}
+
+std::vector<TypeNode> TypeNode::getArgTypes() const {
+ Assert(isFunction());
+ std::vector<TypeNode> args;
+ for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++ i) {
+ args.push_back((*this)[i]);
+ }
+ return args;
+}
+
+TypeNode TypeNode::getRangeType() const {
+ Assert(isFunction());
+ return (*this)[getNumChildren()-1];
+}
+
+
+/** Is this a sort kind */
+bool TypeNode::isSort() const {
+ return getKind() == kind::VARIABLE;
+}
+
+/** Is this a kind type (i.e., the type of a type)? */
+bool TypeNode::isKind() const {
+ return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == KIND_TYPE;
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
new file mode 100644
index 000000000..7747b93e1
--- /dev/null
+++ b/src/expr/type_node.h
@@ -0,0 +1,437 @@
+/********************* */
+/** type_node.h
+ ** Original author: 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.
+ **
+ ** Reference-counted encapsulation of a pointer to node information.
+ **/
+
+#include "cvc4_private.h"
+
+// circular dependency
+#include "expr/node_value.h"
+
+#ifndef __CVC4__TYPE_NODE_H
+#define __CVC4__TYPE_NODE_H
+
+#include <vector>
+#include <string>
+#include <iostream>
+#include <stdint.h>
+
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "util/Assert.h"
+#include "util/output.h"
+
+namespace CVC4 {
+
+class NodeManager;
+
+namespace expr {
+class NodeValue;
+}/* CVC4::expr namespace */
+
+/**
+ * Encapsulation of an NodeValue pointer. The reference count is
+ * maintained in the NodeValue if ref_count is true.
+ */
+class TypeNode {
+
+ /**
+ * The NodeValue has access to the private constructors, so that the
+ * iterators can can create new nodes.
+ */
+ friend class expr::NodeValue;
+
+ /** A convenient null-valued encapsulated pointer */
+ static TypeNode s_null;
+
+ /** The referenced NodeValue */
+ expr::NodeValue* d_nv;
+
+ /**
+ * This constructor is reserved for use by the TypeNode package.
+ */
+ explicit TypeNode(const expr::NodeValue*);
+
+ friend class NodeManager;
+
+ template <class Builder>
+ friend class NodeBuilderBase;
+
+ /**
+ * Assigns the expression value and does reference counting. No assumptions
+ * are made on the expression, and should only be used if we know what we
+ * are doing.
+ *
+ * @param ev the expression value to assign
+ */
+ void assignNodeValue(expr::NodeValue* ev);
+
+public:
+
+ /** Default constructor, makes a null expression. */
+ TypeNode() : d_nv(&expr::NodeValue::s_null) { }
+
+ /** Copy constructor */
+ TypeNode(const TypeNode& node);
+
+ /**
+ * Assignment operator for nodes, copies the relevant information from node
+ * to this node.
+ * @param node the node to copy
+ * @return reference to this node
+ */
+ TypeNode& operator=(const TypeNode& typeNode);
+
+ /**
+ * Destructor. If ref_count is true it will decrement the reference count
+ * and, if zero, collect the NodeValue.
+ */
+ ~TypeNode() throw(AssertionException);
+
+ /**
+ * Return the null node.
+ * @return the null node
+ */
+ static TypeNode null() {
+ return s_null;
+ }
+
+ /**
+ * Returns true if this type is a null type.
+ * @return true if null
+ */
+ bool isNull() const {
+ return d_nv == &expr::NodeValue::s_null;
+ }
+
+ /**
+ * Structural comparison operator for expressions.
+ * @param typeNode the type node to compare to
+ * @return true if expressions are equal, false otherwise
+ */
+ bool operator==(const TypeNode& typeNode) const {
+ return d_nv == typeNode.d_nv;
+ }
+
+ /**
+ * Structural comparison operator for expressions.
+ * @param typeNode the type node to compare to
+ * @return true if expressions are equal, false otherwise
+ */
+ bool operator!=(const TypeNode& typeNode) const {
+ return d_nv != typeNode.d_nv;
+ }
+
+ /**
+ * We compare by expression ids so, keeping things deterministic and having
+ * that subexpressions have to be smaller than the enclosing expressions.
+ * @param node the node to compare to
+ * @return true if this expression is smaller
+ */
+ inline bool operator<(const TypeNode& typeNode) const {
+ return d_nv->d_id < typeNode.d_nv->d_id;
+ }
+
+ /**
+ * Returns the i-th child of this node.
+ * @param i the index of the child
+ * @return the node representing the i-th child
+ */
+ TypeNode operator[](int i) const {
+ return TypeNode(d_nv->getChild(i));
+ }
+
+ /**
+ * Returns the unique id of this node
+ * @return the id
+ */
+ unsigned getId() const {
+ return d_nv->getId();
+ }
+
+ /**
+ * Returns the kind of this type node.
+ * @return the kind
+ */
+ inline Kind getKind() const {
+ return Kind(d_nv->d_kind);
+ }
+
+ /**
+ * Returns the metakind of this type node.
+ * @return the metakind
+ */
+ inline kind::MetaKind getMetaKind() const {
+ return kind::metaKindOf(getKind());
+ }
+
+ /**
+ * Returns the number of children this node has.
+ * @return the number of children
+ */
+ inline size_t getNumChildren() const;
+
+ /**
+ * If this is a CONST_* TypeNode, extract the constant from it.
+ */
+ template <class T>
+ inline const T& getConst() const;
+
+ /**
+ * Returns the value of the given attribute that this has been attached.
+ * @param attKind the kind of the attribute
+ * @return the value of the attribute
+ */
+ template <class AttrKind>
+ inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
+
+ // Note that there are two, distinct hasAttribute() declarations for
+ // a reason (rather than using a pointer-valued argument with a
+ // default value): they permit more optimized code in the underlying
+ // hasAttribute() implementations.
+
+ /**
+ * Returns true if this node has been associated an attribute of given kind.
+ * Additionaly, if a pointer to the value_kind is give, and the attribute
+ * value has been set for this node, it will be returned.
+ * @param attKind the kind of the attribute
+ * @return true if this node has the requested attribute
+ */
+ template <class AttrKind>
+ inline bool hasAttribute(const AttrKind& attKind) const;
+
+ /**
+ * Returns true if this node has been associated an attribute of given kind.
+ * Additionaly, if a pointer to the value_kind is give, and the attribute
+ * value has been set for this node, it will be returned.
+ * @param attKind the kind of the attribute
+ * @param value where to store the value if it exists
+ * @return true if this node has the requested attribute
+ */
+ template <class AttrKind>
+ inline bool getAttribute(const AttrKind& attKind,
+ typename AttrKind::value_type& value) const;
+
+ /**
+ * Sets the given attribute of this node to the given value.
+ * @param attKind the kind of the atribute
+ * @param value the value to set the attribute to
+ */
+ template <class AttrKind>
+ inline void setAttribute(const AttrKind& attKind,
+ const typename AttrKind::value_type& value);
+
+ /** Iterator allowing for scanning through the children. */
+ typedef expr::NodeValue::iterator<TypeNode> iterator;
+ /** Constant iterator allowing for scanning through the children. */
+ typedef expr::NodeValue::iterator<TypeNode> const_iterator;
+
+ /**
+ * Returns the iterator pointing to the first child.
+ * @return the iterator
+ */
+ inline iterator begin() {
+ return d_nv->begin<TypeNode>();
+ }
+
+ /**
+ * Returns the iterator pointing to the end of the children (one beyond the
+ * last one.
+ * @return the end of the children iterator.
+ */
+ inline iterator end() {
+ return d_nv->end<TypeNode>();
+ }
+
+ /**
+ * Returns the const_iterator pointing to the first child.
+ * @return the const_iterator
+ */
+ inline const_iterator begin() const {
+ return d_nv->begin<TypeNode>();
+ }
+
+ /**
+ * Returns the const_iterator pointing to the end of the children (one
+ * beyond the last one.
+ * @return the end of the children const_iterator.
+ */
+ inline const_iterator end() const {
+ return d_nv->end<TypeNode>();
+ }
+
+ /**
+ * Converts this node into a string representation.
+ * @return the string representation of this node.
+ */
+ inline std::string toString() const {
+ return d_nv->toString();
+ }
+
+ /**
+ * Converst this node into a string representation and sends it to the
+ * given stream
+ * @param out the sream to serialise this node to
+ */
+ inline void toStream(std::ostream& out, int toDepth = -1) const {
+ d_nv->toStream(out, toDepth);
+ }
+
+ /**
+ * Very basic pretty printer for Node.
+ * @param o output stream to print to.
+ * @param indent number of spaces to indent the formula by.
+ */
+ void printAst(std::ostream & o, int indent = 0) const;
+
+ /** Is this the Boolean type? */
+ bool isBoolean() const;
+
+ /** Is this a function type? */
+ bool isFunction() const;
+
+ /** Get the argument types */
+ std::vector<TypeNode> getArgTypes() const;
+
+ /** Get the range type (i.e., the type of the result). */
+ TypeNode getRangeType() const;
+
+ /** Is this a predicate type? NOTE: all predicate types are also
+ function types. */
+ bool isPredicate() const;
+
+ /** Is this a sort kind */
+ bool isSort() const;
+
+ /** Is this a kind type (i.e., the type of a type)? */
+ bool isKind() const;
+
+private:
+
+ /**
+ * Indents the given stream a given amount of spaces.
+ * @param out the stream to indent
+ * @param indent the numer of spaces
+ */
+ static void indent(std::ostream& out, int indent) {
+ for(int i = 0; i < indent; i++) {
+ out << ' ';
+ }
+ }
+
+};/* class TypeNode */
+
+/**
+ * Serializes a given node to the given stream.
+ * @param out the output stream to use
+ * @param node the node to output to the stream
+ * @return the changed stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
+ n.toStream(out, Node::setdepth::getDepth(out));
+ return out;
+}
+
+}/* CVC4 namespace */
+
+#include <ext/hash_map>
+
+#include "expr/node_manager.h"
+
+namespace CVC4 {
+
+// for hash_maps, hash_sets..
+struct TypeNodeHashFunction {
+ size_t operator()(const CVC4::TypeNode& node) const {
+ return (size_t) node.getId();
+ }
+};
+
+inline size_t TypeNode::getNumChildren() const {
+ return d_nv->getNumChildren();
+}
+
+template <class T>
+inline const T& TypeNode::getConst() const {
+ return d_nv->getConst<T>();
+}
+
+inline TypeNode::TypeNode(const expr::NodeValue* ev) :
+ d_nv(const_cast<expr::NodeValue*> (ev)) {
+ Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+ d_nv->inc();
+}
+
+inline TypeNode::TypeNode(const TypeNode& typeNode) {
+ Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value!");
+ d_nv = typeNode.d_nv;
+ d_nv->inc();
+}
+
+inline TypeNode::~TypeNode() throw(AssertionException) {
+ Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+ d_nv->dec();
+}
+
+inline void TypeNode::assignNodeValue(expr::NodeValue* ev) {
+ d_nv = ev;
+ d_nv->inc();
+}
+
+inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
+ Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+ Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+ if(EXPECT_TRUE( d_nv != typeNode.d_nv )) {
+ d_nv->dec();
+ d_nv = typeNode.d_nv;
+ d_nv->inc();
+ }
+ return *this;
+}
+
+template <class AttrKind>
+inline typename AttrKind::value_type TypeNode::
+getAttribute(const AttrKind&) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ return NodeManager::currentNM()->getAttribute(d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool TypeNode::
+hasAttribute(const AttrKind&) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void TypeNode::
+setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+ NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__NODE_H */
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index d0be9a351..7894743d6 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -70,7 +70,7 @@ public:
typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute;
void testDeallocation() {
- Type booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkVar(booleanType));
MyData* data;
MyData* data1;
@@ -88,7 +88,7 @@ public:
typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute;
typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute;
void testInts(){
- BooleanType booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkVar(booleanType));
const uint64_t val = 63489;
uint64_t data0 = 0;
@@ -116,7 +116,7 @@ public:
typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute;
typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute;
void testTNodes(){
- BooleanType booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkVar(booleanType));
Node val(d_nodeManager->mkVar(booleanType));
@@ -151,7 +151,7 @@ public:
typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute;
typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute;
void testPtrs(){
- BooleanType booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkVar(booleanType));
Foo* val = new Foo(63489);
@@ -182,7 +182,7 @@ public:
typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute;
typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute;
void testConstPtrs(){
- BooleanType booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkVar(booleanType));
const Foo* val = new Foo(63489);
@@ -212,7 +212,7 @@ public:
typedef expr::Attribute<StringAttributeId, std::string> StringAttribute;
typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute;
void testStrings(){
- BooleanType booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkVar(booleanType));
std::string val("63489");
@@ -241,7 +241,7 @@ public:
typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute;
typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute;
void testBools(){
- BooleanType booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkVar(booleanType));
bool val = true;
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index bfe0ef3cf..43bcc7fe3 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -60,7 +60,7 @@ class AttributeWhite : public CxxTest::TestSuite {
Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
- Type* d_booleanType;
+ TypeNode* d_booleanType;
public:
@@ -69,7 +69,7 @@ public:
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
- d_booleanType = new Type(d_nm->booleanType());
+ d_booleanType = new TypeNode(d_nm->booleanType());
}
void tearDown() {
@@ -146,7 +146,7 @@ public:
lastId = attr::LastAttributeId<TNode, false>::s_id;
TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId);
- lastId = attr::LastAttributeId<Node, false>::s_id;
+ lastId = attr::LastAttributeId<TypeNode, false>::s_id;
TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
}
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 6469806d6..7e034036a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -36,7 +36,7 @@ private:
Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
- Type *d_booleanType;
+ TypeNode *d_booleanType;
public:
@@ -44,7 +44,7 @@ public:
d_ctxt = new Context;
d_nodeManager = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nodeManager);
- d_booleanType = new Type(d_nodeManager->booleanType());
+ d_booleanType = new TypeNode(d_nodeManager->booleanType());
}
void tearDown() {
@@ -400,9 +400,9 @@ public:
}
void testGetOperator() {
- Type sort = d_nodeManager->mkSort("T");
- Type booleanType = d_nodeManager->booleanType();
- Type predType = d_nodeManager->mkFunctionType(sort, booleanType);
+ TypeNode sort = d_nodeManager->mkSort("T");
+ TypeNode booleanType = d_nodeManager->booleanType();
+ TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
Node f = d_nodeManager->mkVar(predType);
Node a = d_nodeManager->mkVar(booleanType);
@@ -490,7 +490,7 @@ public:
}
void testToString() {
- Type booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node w = d_nodeManager->mkVar("w",booleanType);
Node x = d_nodeManager->mkVar("x",booleanType);
@@ -503,7 +503,7 @@ public:
}
void testToStream() {
- Type booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node w = d_nodeManager->mkVar("w",booleanType);
Node x = d_nodeManager->mkVar("x",booleanType);
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 17e1d6f18..a1887118c 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -37,7 +37,7 @@ private:
Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
- Type* d_booleanType;
+ TypeNode* d_booleanType;
public:
@@ -47,7 +47,7 @@ public:
d_scope = new NodeManagerScope(d_nm);
specKind = PLUS;
- d_booleanType = new Type(d_nm->booleanType());
+ d_booleanType = new TypeNode(d_nm->booleanType());
}
void tearDown() {
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 118ba8173..0e1e09178 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -142,7 +142,7 @@ public:
}
void testMkVarWithNoName() {
- Type booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node x = d_nodeManager->mkVar(booleanType);
TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
TS_ASSERT_EQUALS(x.getNumChildren(),0u);
@@ -150,7 +150,7 @@ public:
}
void testMkVarWithName() {
- Type booleanType = d_nodeManager->booleanType();
+ TypeNode booleanType = d_nodeManager->booleanType();
Node x = d_nodeManager->mkVar("x", booleanType);
TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
TS_ASSERT_EQUALS(x.getNumChildren(),0u);
@@ -187,9 +187,9 @@ public:
}
void testBooleanType() {
- Type t = d_nodeManager->booleanType();
- Type t2 = d_nodeManager->booleanType();
- Type t3 = d_nodeManager->mkSort("T");
+ TypeNode t = d_nodeManager->booleanType();
+ TypeNode t2 = d_nodeManager->booleanType();
+ TypeNode t3 = d_nodeManager->mkSort("T");
TS_ASSERT( t.isBoolean() );
TS_ASSERT( !t.isFunction() );
TS_ASSERT( !t.isKind() );
@@ -199,14 +199,14 @@ public:
TS_ASSERT_EQUALS(t, t2);
TS_ASSERT( t != t3 );
- BooleanType bt = t;
+ TypeNode bt = t;
TS_ASSERT_EQUALS( bt, t);
}
void testKindType() {
- Type t = d_nodeManager->kindType();
- Type t2 = d_nodeManager->kindType();
- Type t3 = d_nodeManager->mkSort("T");
+ TypeNode t = d_nodeManager->kindType();
+ TypeNode t2 = d_nodeManager->kindType();
+ TypeNode t3 = d_nodeManager->mkSort("T");
TS_ASSERT( !t.isBoolean() );
TS_ASSERT( !t.isFunction() );
@@ -218,15 +218,15 @@ public:
TS_ASSERT_EQUALS(t, t2);
TS_ASSERT( t != t3);
- KindType kt = t;
+ TypeNode kt = t;
TS_ASSERT_EQUALS( kt, t );
// TODO: Is there a way to get the type of otherType (it should == t)?
}
void testMkFunctionTypeBoolToBool() {
- Type booleanType = d_nodeManager->booleanType();
- Type t = d_nodeManager->mkFunctionType(booleanType,booleanType);
- Type t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
+ TypeNode booleanType = d_nodeManager->booleanType();
+ TypeNode t = d_nodeManager->mkFunctionType(booleanType,booleanType);
+ TypeNode t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
TS_ASSERT( !t.isBoolean() );
TS_ASSERT( t.isFunction() );
@@ -237,7 +237,7 @@ public:
TS_ASSERT_EQUALS( t, t2 );
- FunctionType ft = t;
+ TypeNode ft = t;
TS_ASSERT_EQUALS( ft, t );
TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u);
TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType);
@@ -246,16 +246,16 @@ public:
}
void testMkFunctionTypeVectorOfArgsWithReturnType() {
- Type a = d_nodeManager->mkSort();
- Type b = d_nodeManager->mkSort();
- Type c = d_nodeManager->mkSort();
+ TypeNode a = d_nodeManager->mkSort();
+ TypeNode b = d_nodeManager->mkSort();
+ TypeNode c = d_nodeManager->mkSort();
- std::vector<Type> argTypes;
+ std::vector<TypeNode> argTypes;
argTypes.push_back(a);
argTypes.push_back(b);
- Type t = d_nodeManager->mkFunctionType(argTypes,c);
- Type t2 = d_nodeManager->mkFunctionType(argTypes,c);
+ TypeNode t = d_nodeManager->mkFunctionType(argTypes,c);
+ TypeNode t2 = d_nodeManager->mkFunctionType(argTypes,c);
TS_ASSERT( !t.isBoolean() );
TS_ASSERT( t.isFunction() );
@@ -266,7 +266,7 @@ public:
TS_ASSERT_EQUALS( t, t2 );
- FunctionType ft = t;
+ TypeNode ft = t;
TS_ASSERT_EQUALS( ft, t );
TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
@@ -276,17 +276,17 @@ public:
}
void testMkFunctionTypeVectorOfArguments() {
- Type a = d_nodeManager->mkSort();
- Type b = d_nodeManager->mkSort();
- Type c = d_nodeManager->mkSort();
+ TypeNode a = d_nodeManager->mkSort();
+ TypeNode b = d_nodeManager->mkSort();
+ TypeNode c = d_nodeManager->mkSort();
- std::vector<Type> types;
+ std::vector<TypeNode> types;
types.push_back(a);
types.push_back(b);
types.push_back(c);
- Type t = d_nodeManager->mkFunctionType(types);
- Type t2 = d_nodeManager->mkFunctionType(types);
+ TypeNode t = d_nodeManager->mkFunctionType(types);
+ TypeNode t2 = d_nodeManager->mkFunctionType(types);
TS_ASSERT( !t.isBoolean() );
TS_ASSERT( t.isFunction() );
@@ -297,7 +297,7 @@ public:
TS_ASSERT_EQUALS( t, t2 );
- FunctionType ft = t;
+ TypeNode ft = t;
TS_ASSERT_EQUALS( ft, t );
TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1);
TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
@@ -306,18 +306,18 @@ public:
}
void testMkPredicateType() {
- Type a = d_nodeManager->mkSort("a");
- Type b = d_nodeManager->mkSort("b");
- Type c = d_nodeManager->mkSort("c");
- Type booleanType = d_nodeManager->booleanType();
+ TypeNode a = d_nodeManager->mkSort("a");
+ TypeNode b = d_nodeManager->mkSort("b");
+ TypeNode c = d_nodeManager->mkSort("c");
+ TypeNode booleanType = d_nodeManager->booleanType();
- std::vector<Type> argTypes;
+ std::vector<TypeNode> argTypes;
argTypes.push_back(a);
argTypes.push_back(b);
argTypes.push_back(c);
- Type t = d_nodeManager->mkPredicateType(argTypes);
- Type t2 = d_nodeManager->mkPredicateType(argTypes);
+ TypeNode t = d_nodeManager->mkPredicateType(argTypes);
+ TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
TS_ASSERT( !t.isBoolean() );
TS_ASSERT( t.isFunction() );
@@ -328,7 +328,7 @@ public:
TS_ASSERT_EQUALS( t, t2 );
- FunctionType ft = t;
+ TypeNode ft = t;
TS_ASSERT_EQUALS( ft, t );
TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 25c22f196..e0dfd7aa8 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -211,8 +211,8 @@ public:
void testRegisterTerm() {
TS_ASSERT(d_dummy->doneWrapper());
- Type typeX = d_nm->booleanType();
- Type typeF = d_nm->mkFunctionType(typeX, typeX);
+ TypeNode typeX = d_nm->booleanType();
+ TypeNode typeF = d_nm->mkFunctionType(typeX, typeX);
Node x = d_nm->mkVar("x",typeX);
Node f = d_nm->mkVar("f",typeF);
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index 44b13c87c..6b14a38d5 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -94,7 +94,7 @@ class TheoryUFWhite : public CxxTest::TestSuite {
TheoryUF* d_euf;
- Type* d_booleanType;
+ TypeNode* d_booleanType;
public:
@@ -107,7 +107,7 @@ public:
d_outputChannel.clear();
d_euf = new TheoryUF(d_ctxt, d_outputChannel);
- d_booleanType = new Type(d_nm->booleanType());
+ d_booleanType = new TypeNode(d_nm->booleanType());
}
void tearDown() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback