Add nullary operator metakind.

4 files changed, 17 insertions, 5 deletions

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index ab0ca3428..cfe7eb632 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -44,6 +44,7 @@ operator SINGLETON     1  "the set of the single element given as a parameter"
 operator INSERT        2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
 operator CARD          1  "set cardinality operator"
 operator COMPLEMENT    1  "set COMPLEMENT (with respect to finite universe)"
+nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it."
 
 operator JOIN 		   2  "set join"
 operator PRODUCT 	   2  "set cartesian product"
@@ -60,14 +61,13 @@ typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule
 typerule INSERT         ::CVC4::theory::sets::InsertTypeRule
 typerule CARD           ::CVC4::theory::sets::CardTypeRule
 typerule COMPLEMENT     ::CVC4::theory::sets::ComplementTypeRule
+typerule UNIVERSE_SET   ::CVC4::theory::sets::UniverseSetTypeRule
 
 typerule JOIN 			::CVC4::theory::sets::RelBinaryOperatorTypeRule
 typerule PRODUCT 		::CVC4::theory::sets::RelBinaryOperatorTypeRule
 typerule TRANSPOSE 		::CVC4::theory::sets::RelTransposeTypeRule
 typerule TCLOSURE 	    ::CVC4::theory::sets::RelTransClosureTypeRule
 
-variable UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it."
-
 construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle INTERSECTION  ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle SETMINUS      ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 5b9f4bf03..57ab8c0cf 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1531,7 +1531,7 @@ Node TheorySetsPrivate::getEmptySet( TypeNode tn ) {
 Node TheorySetsPrivate::getUnivSet( TypeNode tn ) {
   std::map< TypeNode, Node >::iterator it = d_univset.find( tn );
   if( it==d_univset.end() ){
-    Node n = NodeManager::currentNM()->mkUniqueVar(tn, kind::UNIVERSE_SET);
+    Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET);
     d_univset[tn] = n;
     return n;
   }else{
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 9669561a6..8facf1f48 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -306,7 +306,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     break;
   }//kind::UNION
   case kind::COMPLEMENT: {
-    Node univ = NodeManager::currentNM()->mkUniqueVar( node[0].getType(), kind::UNIVERSE_SET );
+    Node univ = NodeManager::currentNM()->mkNullaryOperator( node[0].getType(), kind::UNIVERSE_SET );
     return RewriteResponse( REWRITE_AGAIN, NodeManager::currentNM()->mkNode( kind::SETMINUS, univ, node[0] ) );
   }
     break;
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 11f375d5b..541835980 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -174,7 +174,19 @@ struct ComplementTypeRule {
   }
 };/* struct ComplementTypeRule */
 
-
+struct UniverseSetTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::UNIVERSE_SET);
+    // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation
+    Assert(check);
+    TypeNode setType = n.getType(false);
+    if(!setType.isSet()) {
+      throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found");
+    }
+    return setType;
+  }
+};/* struct ComplementTypeRule */
 
 struct InsertTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)