diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-14 00:17:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-14 00:17:20 +0000 |
commit | b904efd3a2bad1411099cd2a8696cbda96a37cb0 (patch) | |
tree | 7071d2becf78032d9b3cebbca9c1fcef014af27d /src/expr/node_manager.h | |
parent | 11bb98ba5b1e9e88053a7bd6adc1d48d48a4bb21 (diff) |
reverting node manager change from 1881; also part of parameterized datatypes review
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8b803e696..9974df6ca 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -53,12 +53,10 @@ namespace expr { namespace attr { struct VarNameTag {}; struct SortArityTag {}; - struct DatatypeTag {}; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; -typedef Attribute<attr::SortArityTag, void*> DatatypeAttr; }/* CVC4::expr namespace */ @@ -1190,6 +1188,7 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, return NodeBuilder<>(this, kind).append(children).constructTypeNode(); } + inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { Node n = mkVar(type); n.setAttribute(TypeAttr(), type); |