diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
commit | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (patch) | |
tree | 4ff6643e38469ceb84cd6791c5cbc295f625a735 /src/expr/node_manager.h | |
parent | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (diff) |
declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 58 |
1 files changed, 53 insertions, 5 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index ca93473db..c0f489d7a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -48,9 +48,11 @@ namespace expr { // TODO: hide this attribute behind a NodeManager interface. namespace attr { struct VarNameTag {}; + struct SortArityTag {}; }/* CVC4::expr::attr namespace */ typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr; +typedef expr::Attribute<attr::SortArityTag, uint64_t> SortArityAttr; }/* CVC4::expr namespace */ @@ -508,7 +510,14 @@ public: inline TypeNode mkSort(); /** Make a new sort with the given name and arity. */ - inline TypeNode mkSort(const std::string& name, size_t arity = 0); + inline TypeNode mkSort(const std::string& name); + + /** Make a new sort with the given name and arity. */ + inline TypeNode mkSort(TypeNode constructor, + const std::vector<TypeNode>& children); + + /** Make a new sort with the given name and arity. */ + inline TypeNode mkSortConstructor(const std::string& name, size_t arity); /** * Get the type for the given node and optionally do type checking. @@ -762,16 +771,55 @@ inline bool NodeManager::hasOperator(Kind k) { } inline TypeNode NodeManager::mkSort() { - return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode(); + NodeBuilder<1> nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + nb << sortTag; + return nb.constructTypeNode(); } -inline TypeNode NodeManager::mkSort(const std::string& name, size_t arity) { - Assert(arity == 0, "parameterized sorts not yet supported."); +inline TypeNode NodeManager::mkSort(const std::string& name) { TypeNode type = mkSort(); type.setAttribute(expr::VarNameAttr(), name); return type; } +inline TypeNode NodeManager::mkSort(TypeNode constructor, + const std::vector<TypeNode>& children) { + Assert(constructor.getKind() == kind::SORT_TYPE && + constructor.getNumChildren() == 0, + "expected a sort constructor"); + Assert(children.size() > 0, "expected non-zero # of children"); + uint64_t arity; + std::string name; + bool hasArityAttribute = + getAttribute(constructor.d_nv, expr::SortArityAttr(), arity); + Assert(hasArityAttribute, "expected a sort constructor"); + bool hasNameAttribute = + getAttribute(constructor.d_nv, expr::VarNameAttr(), name); + Assert(hasNameAttribute, "expected a sort constructor"); + Assert(arity == children.size(), + "arity mismatch in application of sort constructor"); + NodeBuilder<> nb(this, kind::SORT_TYPE); + Node sortTag = Node(constructor.d_nv->d_children[0]); + nb << sortTag; + nb.append(children); + TypeNode type = nb.constructTypeNode(); + type.setAttribute(expr::VarNameAttr(), name); + return type; +} + +inline TypeNode NodeManager::mkSortConstructor(const std::string& name, + size_t arity) { + Assert(arity > 0); + NodeBuilder<> nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + nb << sortTag; + TypeNode type = nb.constructTypeNode(); + type.setAttribute(expr::VarNameAttr(), name); + type.setAttribute(expr::SortArityAttr(), arity); + return type; +} + inline Node NodeManager::mkNode(Kind kind, TNode child1) { NodeBuilder<1> nb(this, kind); nb << child1; @@ -832,7 +880,7 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, - TNode child3, TNode child4, TNode child5) { + TNode child3, TNode child4, TNode child5) { NodeBuilder<5> nb(this, kind); nb << child1 << child2 << child3 << child4 << child5; return nb.constructNodePtr(); |