diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-15 16:56:11 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-15 16:56:11 +0000 |
commit | 74eb1c4f0f3932dcb9aeb0d8d9ac24b32fb69cec (patch) | |
tree | 4e4228705cc082e832181bd876e47443343c016b /src/expr/node_manager.h | |
parent | 80c2545bedb3ed8e64a3035d326b110dc9332bd9 (diff) |
Enhancements to NodeManager tests, taking advantage of new Type implementation
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 3a6b6e15a..138a87493 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -473,6 +473,9 @@ public: */ inline Type mkPredicateType(const std::vector<Type>& sorts); + /** Make a new sort. */ + inline Type mkSort(); + /** Make a new sort with the given name. */ inline Type mkSort(const std::string& name); @@ -630,6 +633,10 @@ NodeManager::mkPredicateType(const std::vector<Type>& sorts) { return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes)); } +inline Type NodeManager::mkSort() { + return Type(this, mkVarPtr(kindType())); +} + inline Type NodeManager::mkSort(const std::string& name) { return Type(this, mkVarPtr(name, kindType())); } |