Cleanup from last commit, treat sep.nil as variable kind.

4 files changed, 29 insertions, 1 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 84f674d2b..ef74575f3 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -941,6 +941,11 @@ Expr ExprManager::mkBoundVar(Type type) {
   return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
 }
 
+Expr ExprManager::mkSepNil(Type type) {
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode));
+}
+
 Expr ExprManager::mkAssociative(Kind kind,
                                 const std::vector<Expr>& children) {
   PrettyCheckArgument(
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 04f2f4289..31c911736 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -545,6 +545,11 @@ public:
    * @param type the type for the new bound variable
    */
   Expr mkBoundVar(Type type);
+  
+  /**
+   * Create a (nameless) new nil reference for separation logic of type
+   */
+  Expr mkSepNil(Type type);
 
   /** Get a reference to the statistics registry for this ExprManager */
   Statistics getStatistics() const throw();
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);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7d2b13e4c..dcd7005f8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -332,7 +332,7 @@ class NodeManager {
   /** Create a variable with the given type. */
   Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
   Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
+  
 public:
 
   explicit NodeManager(ExprManager* exprManager);
@@ -486,6 +486,10 @@ public:
 
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
+  
+  /** Create nil reference for separation logic with the given type. */
+  Node mkSepNil(const TypeNode& type);
+  Node* mkSepNilPtr(const TypeNode& type);
 
   /** Make a new abstract value with the given type. */
   Node mkAbstractValue(const TypeNode& type);