diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
| commit | 8d54316e7ff784a8d66da9ecc2d289ab463761c2 (patch) | |
| tree | c7b5351b372cb360780ce62935fb2cfb5792299a /src/expr/node_manager.h | |
| parent | 69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66 (diff) | |
added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 9974df6ca..8b803e696 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -53,10 +53,12 @@ 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 */ @@ -1188,7 +1190,6 @@ 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); |