More fixes for printing/parsing sets, fix kind name.

3 files changed, 9 insertions, 9 deletions

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 53905e47f..ab0ca3428 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -43,7 +43,7 @@ operator MEMBER        2  "set membership predicate; first parameter a member of
 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 COMPLIMENT    1  "set compliment (with respect to finite universe)"
+operator COMPLEMENT    1  "set COMPLEMENT (with respect to finite universe)"
 
 operator JOIN 		   2  "set join"
 operator PRODUCT 	   2  "set cartesian product"
@@ -59,7 +59,7 @@ typerule SINGLETON      ::CVC4::theory::sets::SingletonTypeRule
 typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule
 typerule INSERT         ::CVC4::theory::sets::InsertTypeRule
 typerule CARD           ::CVC4::theory::sets::CardTypeRule
-typerule COMPLIMENT     ::CVC4::theory::sets::ComplimentTypeRule
+typerule COMPLEMENT     ::CVC4::theory::sets::ComplementTypeRule
 
 typerule JOIN 			::CVC4::theory::sets::RelBinaryOperatorTypeRule
 typerule PRODUCT 		::CVC4::theory::sets::RelBinaryOperatorTypeRule
@@ -74,7 +74,7 @@ construle SETMINUS      ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle SINGLETON     ::CVC4::theory::sets::SingletonTypeRule
 construle INSERT        ::CVC4::theory::sets::InsertTypeRule
 construle CARD          ::CVC4::theory::sets::CardTypeRule
-construle COMPLIMENT    ::CVC4::theory::sets::ComplimentTypeRule
+construle COMPLEMENT    ::CVC4::theory::sets::ComplementTypeRule
 
 construle JOIN 			::CVC4::theory::sets::RelBinaryOperatorTypeRule
 construle PRODUCT 		::CVC4::theory::sets::RelBinaryOperatorTypeRule
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index da4f8fb7a..9669561a6 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -305,7 +305,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     }
     break;
   }//kind::UNION
-  case kind::COMPLIMENT: {
+  case kind::COMPLEMENT: {
     Node univ = NodeManager::currentNM()->mkUniqueVar( node[0].getType(), kind::UNIVERSE_SET );
     return RewriteResponse( REWRITE_AGAIN, NodeManager::currentNM()->mkNode( kind::SETMINUS, univ, node[0] ) );
   }
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 66e06b038..11f375d5b 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -155,24 +155,24 @@ struct CardTypeRule {
   }
 };/* struct CardTypeRule */
 
-struct ComplimentTypeRule {
+struct ComplementTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
-    Assert(n.getKind() == kind::COMPLIMENT);
+    Assert(n.getKind() == kind::COMPLEMENT);
     TypeNode setType = n[0].getType(check);
     if( check ) {
       if(!setType.isSet()) {
-        throw TypeCheckingExceptionPrivate(n, "compliment operates on a set, non-set object found");
+        throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found");
       }
     }
     return setType;
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    Assert(n.getKind() == kind::COMPLIMENT);
+    Assert(n.getKind() == kind::COMPLEMENT);
     return false;
   }
-};/* struct ComplimentTypeRule */
+};/* struct ComplementTypeRule */