Add nullary operator metakind.

12 files changed, 46 insertions, 21 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 470a6eeca..82cabbd3e 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -946,9 +946,9 @@ Expr ExprManager::mkBoundVar(Type type) {
   return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
 }
 
-Expr ExprManager::mkUniqueVar(Type type, Kind k){
+Expr ExprManager::mkNullaryOperator(Type type, Kind k){
   NodeManagerScope nms(d_nodeManager);
-  Node n = d_nodeManager->mkUniqueVar(*type.d_typeNode, k); 
+  Node n = d_nodeManager->mkNullaryOperator(*type.d_typeNode, k); 
   return n.toExpr();
 }
 
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index ed9247e5e..9e962d970 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -549,7 +549,7 @@ public:
   /**
    * Create unique variable of type 
    */
-  Expr mkUniqueVar( Type type, Kind k);
+  Expr mkNullaryOperator( Type type, Kind k);
 
   /** Get a reference to the statistics registry for this ExprManager */
   Statistics getStatistics() const throw();
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 1c03cf407..2dcf24b09 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -98,7 +98,8 @@ enum MetaKind_t {
   VARIABLE, /**< special node kinds: no operator */
   OPERATOR, /**< operators that get "inlined" */
   PARAMETERIZED, /**< parameterized ops (like APPLYs) that carry extra data */
-  CONSTANT /**< constants */
+  CONSTANT, /**< constants */
+  NULLARY_OPERATOR /**< nullary operator */
 };/* enum MetaKind_t */
 
 }/* CVC4::kind::metakind namespace */
@@ -338,7 +339,7 @@ ${metakind_operatorKinds}
 
 }/* CVC4::kind namespace */
 
-#line 342 "${template}"
+#line 343 "${template}"
 
 namespace theory {
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 963e297b4..60ee758d8 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -248,6 +248,12 @@ template <> $2 const & Expr::getConst() const {
   case $1: return to->mkConst(n.getConst< $2 >());"
 }
 
+function nullaryoperator {
+  # nullaryoperator K ["comment"]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function check_theory_seen {
   if $seen_endtheory; then
     echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 271c8bc7a..2b1901f5d 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -239,6 +239,15 @@ function constant {
   register_kind "$1" 0 "$5"
 }
 
+function nullaryoperator {
+  # nullaryoperator K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_kind "$1" 0 "$2"
+}
+
 function register_sort {
   id=$1
   cardinality=$2
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 3e06a88a5..19e6e2244 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -302,6 +302,15 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 "
 }
 
+function nullaryoperator {
+  # nullaryoperator K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_metakind NULLARY_OPERATOR "$1" 0
+}
+
 function registerOperatorToKind {
   operatorKind=$1
   applyKind=$2
diff --git a/src/expr/node.h b/src/expr/node.h
index 31721b2ef..6d98b940b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -464,12 +464,6 @@ public:
     assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::VARIABLE;
   }
-  inline bool isUninterpretedVar() const {
-    assertTNodeNotExpired();
-    return getMetaKind() == kind::metakind::VARIABLE &&
-           getKind() != kind::UNIVERSE_SET && 
-           getKind() != kind::SEP_NIL;
-  }
 
   inline bool isClosure() const {
     assertTNodeNotExpired();
@@ -1259,6 +1253,9 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
   case kind::metakind::CONSTANT:
     IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind");
 
+  case kind::metakind::NULLARY_OPERATOR:
+    IllegalArgument(*this, "getOperator() called on Node with NULLARY_OPERATOR-kinded kind");
+
   default:
     Unhandled(mk);
   }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index d92524a19..7cb14ed5a 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -933,7 +933,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   // file comments at the top of this file.
 
   // Case 0: If a VARIABLE
-  if(getMetaKind() == kind::metakind::VARIABLE) {
+  if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) {
     /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
      * there are no children (no reference counts to reason about),
      * and we don't keep VARIABLE-kinded Nodes in the NodeManager
@@ -1123,7 +1123,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
   // file comments at the top of this file.
 
   // Case 0: If a VARIABLE
-  if(getMetaKind() == kind::metakind::VARIABLE) {
+  if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) {
     /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
      * there are no children (no reference counts to reason about),
      * and we don't keep VARIABLE-kinded Nodes in the NodeManager
@@ -1336,6 +1336,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
   if( d_nm->getOptions()[options::earlyTypeChecking] ) {
     kind::MetaKind mk = n.getMetaKind();
     if( mk != kind::metakind::VARIABLE
+        && mk != kind::metakind::NULLARY_OPERATOR
         && mk != kind::metakind::CONSTANT ) {
       d_nm->getType(n, true);
     }
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index ebf78f541..2a819935d 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -315,7 +315,7 @@ void NodeManager::reclaimZombies() {
 
       // remove from the pool
       kind::MetaKind mk = nv->getMetaKind();
-      if(mk != kind::metakind::VARIABLE) {
+      if(mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR) {
         poolRemove(nv);
       }
 
@@ -787,14 +787,15 @@ Node NodeManager::mkBooleanTermVariable() {
   return n;
 }
 
-Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) {
+Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
   std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
   if( it==d_unique_vars[k].end() ){
     Node n = NodeBuilder<0>(this, k);
     n.setAttribute(TypeAttr(), type);
-    n.setAttribute(TypeCheckedAttr(), true);
+    //should type check it
+    //n.setAttribute(TypeCheckedAttr(), true);
     d_unique_vars[k][type] = n;
-    Assert( n.getMetaKind() == kind::metakind::VARIABLE );
+    Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR );
     return n;
   }else{
     return it->second;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d2b45a636..3aa826b49 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -536,7 +536,7 @@ public:
   Node mkAbstractValue(const TypeNode& type);
   
   /** make unique (per Type,Kind) variable. */
-  Node mkUniqueVar(const TypeNode& type, Kind k);
+  Node mkNullaryOperator(const TypeNode& type, Kind k);
 
   /**
    * Create a constant of type T.  It will have the appropriate
@@ -1240,6 +1240,7 @@ inline bool NodeManager::hasOperator(Kind k) {
 
   case kind::metakind::INVALID:
   case kind::metakind::VARIABLE:
+  case kind::metakind::NULLARY_OPERATOR:
     return false;
 
   case kind::metakind::OPERATOR:
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 40649ef2c..f8de8c0c8 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -60,7 +60,7 @@ void NodeValue::printAst(std::ostream& out, int ind) const {
   indent(out, ind);
   out << '(';
   out << getKind();
-  if (getMetaKind() == kind::metakind::VARIABLE) {
+  if (getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR ) {
     out << ' ' << getId();
   } else if (getMetaKind() == kind::metakind::CONSTANT) {
     out << ' ';
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 8ed894a22..757a32529 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -61,7 +61,7 @@ ${typerules}
 bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
   throw (AssertionException) {
 
-  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
 
   switch(n.getKind()) {
 ${construles}
@@ -78,7 +78,7 @@ ${construles}
 bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
   throw (AssertionException) {
 
-  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
 
   switch(n.getKind()) {
 ${neverconstrules}