diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
commit | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (patch) | |
tree | 8db12e260b24978bbbed3363846f6daf7c0da04f /src/expr/node_manager.h | |
parent | 5e2f381b26d683691d9a040589536dc39c5831e0 (diff) |
parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 77f00ab33..ca93473db 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -395,7 +395,7 @@ public: * <code>AttrKind::value_type</code> if not. */ template <class AttrKind> - inline typename AttrKind::value_type + inline typename AttrKind::value_type getAttribute(TNode n, const AttrKind& attr) const; /** @@ -504,11 +504,11 @@ public: /** Make the type of arrays with the given parameterization */ inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); - /** Make a new sort. */ + /** Make a new (anonymous) sort of arity 0. */ inline TypeNode mkSort(); - /** Make a new sort with the given name. */ - inline TypeNode mkSort(const std::string& name); + /** Make a new sort with the given name and arity. */ + inline TypeNode mkSort(const std::string& name, size_t arity = 0); /** * Get the type for the given node and optionally do type checking. @@ -532,7 +532,7 @@ public: * amount of checking required to return a valid result. * * @param n the Node for which we want a type - * @param check whether we should check the type as we compute it + * @param check whether we should check the type as we compute it * (default: false) */ TypeNode getType(TNode n, bool check = false) @@ -765,7 +765,8 @@ inline TypeNode NodeManager::mkSort() { return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode(); } -inline TypeNode NodeManager::mkSort(const std::string& name) { +inline TypeNode NodeManager::mkSort(const std::string& name, size_t arity) { + Assert(arity == 0, "parameterized sorts not yet supported."); TypeNode type = mkSort(); type.setAttribute(expr::VarNameAttr(), name); return type; |