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

13 files changed, 35 insertions, 19 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 267fe303e..fb0304045 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -448,7 +448,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
   default: break;
   }
   Expr e = em->mkExpr(k, lhs, rhs);
-  return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLIMENT : kind::NOT, e) : e;
+  return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLEMENT : kind::NOT, e) : e;
 }/* createPrecedenceTree() recursive variant */
 
 Expr createPrecedenceTree(Parser* parser, ExprManager* em,
@@ -474,7 +474,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
 
 /** Add n NOTs to the front of e and return the result. */
 Expr addNots(ExprManager* em, size_t n, Expr e) {
-  Kind k = e.getType().isSet() ? kind::COMPLIMENT : kind::NOT;
+  Kind k = e.getType().isSet() ? kind::COMPLEMENT : kind::NOT;
   while(n-- > 0) {
     e = em->mkExpr(k, e);
   }
@@ -1689,6 +1689,8 @@ bvNegTerm[CVC4::Expr& f]
     /* BV neg */
   : BVNEG_TOK bvNegTerm[f]
     { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
+  | NOT_TOK bvNegTerm[f]
+    { f = MK_EXPR(CVC4::kind::COMPLEMENT, f); } 
   | TRANSPOSE_TOK bvNegTerm[f]
     { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } 
   | TRANSCLOSURE_TOK bvNegTerm[f]
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 88b2479ea..ebe730e29 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -236,7 +236,7 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::SINGLETON, "singleton");
     addOperator(kind::INSERT, "insert");
     addOperator(kind::CARD, "card");
-    addOperator(kind::COMPLIMENT, "compliment");
+    addOperator(kind::COMPLEMENT, "complement");
     break;
 
   case THEORY_DATATYPES:
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e0c434d5a..981e88a5c 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -90,6 +90,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     string s;
     if(n.getAttribute(expr::VarNameAttr(), s)) {
       out << s;
+    }else if( n.getKind() == kind::UNIVERSE_SET ){
+      out << "UNIVERSE :: " << n.getType();
     } else {
       if(n.getKind() == kind::VARIABLE) {
         out << "var_";
@@ -780,7 +782,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << "IS_IN";
       opType = INFIX;
       break;
-    case kind::COMPLIMENT:
+    case kind::COMPLEMENT:
       op << "NOT";
       opType = PREFIX;
       break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b3fcaf24b..2b7da63f7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -518,7 +518,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::MEMBER:
   case kind::SET_TYPE:
   case kind::SINGLETON: 
-  case kind::COMPLIMENT:out << smtKindString(k) << " "; break;
+  case kind::COMPLEMENT:out << smtKindString(k) << " "; break;
 
     // fp theory
   case kind::FLOATINGPOINT_FP:
@@ -807,7 +807,7 @@ static string smtKindString(Kind k) throw() {
   case kind::SET_TYPE: return "Set";
   case kind::SINGLETON: return "singleton";
   case kind::INSERT: return "insert";
-  case kind::COMPLIMENT: return "compliment";
+  case kind::COMPLEMENT: return "complement";
 
     // fp theory
   case kind::FLOATINGPOINT_FP: return "fp";
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6b4b67a26..d394c8fef 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -137,7 +137,7 @@ Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
 Node TermDb::getMatchOperator( Node n ) {
   Kind k = n.getKind();
   //datatype operators may be parametric, always assume they are
-  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || k==COMPLIMENT ||
+  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
       k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index efd80a83c..1bfc53b41 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -353,7 +353,7 @@ bool Trigger::isAtomicTrigger( Node n ){
 bool Trigger::isAtomicTriggerKind( Kind k ) {
   return k==APPLY_UF || k==SELECT || k==STORE ||
          k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
-         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || k==COMPLIMENT ||
+         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
          k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR;
 }
 
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 */
 
 
 
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 629e8a8a0..06bd6cbf1 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -76,7 +76,8 @@ TESTS =	\
 	abt-te-exh.smt2 \
 	abt-te-exh2.smt2 \
 	univset-simp.smt2 \
-	compliment.cvc
+	complement.cvc \
+	complement2.cvc
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/compliment.cvc b/test/regress/regress0/sets/complement.cvc
index 6181cbee7..6181cbee7 100644
--- a/test/regress/regress0/sets/compliment.cvc
+++ b/test/regress/regress0/sets/complement.cvc
diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc
new file mode 100644
index 000000000..6802065f1
--- /dev/null
+++ b/test/regress/regress0/sets/complement2.cvc
@@ -0,0 +1,11 @@
+% EXPECT: unsat

+OPTION "logic" "ALL_SUPPORTED";

+Atom: TYPE;

+a : SET OF Atom;

+b : SET OF Atom;

+c : Atom;

+

+ASSERT a = NOT(a);

+ASSERT c IS_IN a;

+

+CHECKSAT;

diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2
index 5d10e27cb..ec9750776 100644
--- a/test/regress/regress0/sets/univset-simp.smt2
+++ b/test/regress/regress0/sets/univset-simp.smt2
@@ -15,7 +15,7 @@
 (assert (not (member 1 c)))
 (assert (member 2 d))
 (assert (= e (as univset (Set Int))))
-(assert (= f (compliment d)))
+(assert (= f (complement d)))
 (assert (not (member x (as univset (Set Int)))))
 
 (check-sat)