diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a9be51418..ebf78f541 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -780,6 +780,13 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } +Node NodeManager::mkBooleanTermVariable() { + Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE); + n.setAttribute(TypeAttr(), booleanType()); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) { std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); if( it==d_unique_vars[k].end() ){ |