diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 00fe6baa8..e763a1f10 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -362,6 +362,9 @@ public: /** Create a skolem constant with the given type. */ Node mkSkolem(const TypeNode& type); + /** Create a instantiation constant with the given type. */ + Node mkInstConstant(const TypeNode& type); + /** * Create a constant of type T. It will have the appropriate * CONST_* kind defined for T. @@ -579,6 +582,15 @@ public: /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); + /** Get the bound var list type. */ + inline TypeNode boundVarListType(); + + /** Get the instantiation pattern type. */ + inline TypeNode instPatternType(); + + /** Get the instantiation pattern type. */ + inline TypeNode instPatternListType(); + /** * Get the (singleton) type for builtin operators (that is, the type * of the Node returned from Node::getOperator() when the operator @@ -897,6 +909,21 @@ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE)); } +/** Get the bound var list type. */ +inline TypeNode NodeManager::boundVarListType(){ + return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE)); +} + +/** Get the instantiation pattern type. */ +inline TypeNode NodeManager::instPatternType(){ + return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE)); +} + +/** Get the instantiation pattern type. */ +inline TypeNode NodeManager::instPatternListType(){ + return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE)); +} + /** Get the (singleton) type for builtin operators. */ inline TypeNode NodeManager::builtinOperatorType() { return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE)); @@ -1366,6 +1393,13 @@ inline Node NodeManager::mkSkolem(const TypeNode& type) { return n; } +inline Node NodeManager::mkInstConstant(const TypeNode& type) { + Node n = NodeBuilder<0>(this, kind::INST_CONSTANT); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + template <class T> Node NodeManager::mkConst(const T& val) { return mkConstInternal<Node, T>(val); |