diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-16 20:26:14 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-16 20:26:14 +0000 |
commit | c237443e1fad0ab948f2acb97651dec4f0c34dae (patch) | |
tree | 83ccbb9b08fcfbacbacbdc3e717a7e8c3adede7c /src/expr | |
parent | 22685d657c483ab53c645bb9228bd5d4dd708cf5 (diff) |
This commit just contains miscellaneous arithmetic cleanup.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 2d96ac57a..7e0cfd0cf 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -313,6 +313,8 @@ public: Node mkVar(const TypeNode& type); Node* mkVarPtr(const TypeNode& type); + /** Create a skolem constant with the given type. */ + Node mkSkolem(const TypeNode& type); /** * Create a constant of type T. It will have the appropriate @@ -864,6 +866,12 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type) { return n; } +inline Node NodeManager::mkSkolem(const TypeNode& type) { + Node n = NodeBuilder<0>(this, kind::SKOLEM); + n.setAttribute(TypeAttr(), type); + return n; +} + template <class T> Node NodeManager::mkConst(const T& val) { return mkConstInternal<Node, T>(val); |