summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-06-17 18:38:16 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-06-17 18:38:16 -0500
commitf5ed28fe24f6b887630a48dcf476c462c0c227a1 (patch)
treeedd8b8c35b474ed051ace7c861799d734ab5b99d /src/expr/node_manager.cpp
parent1a2547995acc5a98c8969e628ac5e1c45b0efe94 (diff)
Cleanup from last commit, treat sep.nil as variable kind.
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r--src/expr/node_manager.cpp14
1 files changed, 14 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0809a0331..d2ac7e2a1 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -681,6 +681,20 @@ Node NodeManager::mkInstConstant(const TypeNode& type) {
return n;
}
+Node NodeManager::mkSepNil(const TypeNode& type) {
+ Node n = NodeBuilder<0>(this, kind::SEP_NIL);
+ n.setAttribute(TypeAttr(), type);
+ n.setAttribute(TypeCheckedAttr(), true);
+ return n;
+}
+
+Node* NodeManager::mkSepNilPtr(const TypeNode& type) {
+ Node* n = NodeBuilder<0>(this, kind::SEP_NIL).constructNodePtr();
+ setAttribute(*n, TypeAttr(), type);
+ setAttribute(*n, TypeCheckedAttr(), true);
+ return n;
+}
+
Node NodeManager::mkAbstractValue(const TypeNode& type) {
Node n = mkConst(AbstractValue(++d_abstractValueCount));
n.setAttribute(TypeAttr(), type);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback