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

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 267fe303ec47fb6ef3533865bb06686a5b8de5c2..fb0304045618dc7658827fd6b484c7dc77156ac3 100644 (file)
--- 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 88b2479eab0926571baf124611acf33af55ec128..ebe730e299980c8ee2fc10d52aa831fc5d1c9da1 100644 (file)
--- 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 e0c434d5a7de5027c8ee7b058b89d8a06dc990b9..981e88a5cc78ff90872bb36d7c57f5ca975574d2 100644 (file)
--- 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 b3fcaf24bd6f8ee2ab1fbd147f9ba07cfbec3ade..2b7da63f7165ee203379a8d11b7d3d7eec5d5a1b 100644 (file)
--- 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 6b4b67a2647a1dd48a48f3be1c903b75ec1a6430..d394c8fef3732995634b24bdd1f9ae6cae0d1c74 100644 (file)
--- 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 efd80a83c883fa5653f4fb3e291cee62d369823c..1bfc53b41f5d84b87e7d08af3c72b5f6b2ac1403 100644 (file)
--- 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 53905e47f7e12860998b79f9d3d8bb80e1590211..ab0ca3428b7d7c3583436532c0e4786d294f4bc6 100644 (file)
--- 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 da4f8fb7a45bf372a8ecd9bcf70c8ab5846af9fe..9669561a6c6c952a414e50cb1f4b0bcad5fedd98 100644 (file)
--- 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 66e06b038e79b9ee522abfec2bea65db120134b2..11f375d5bcc941712e9665e6260a3a98370075ff 100644 (file)
--- 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 629e8a8a07ab23414f937bbd2b2349bd8de2046b..06bd6cbf11205bb6d040eedfd51e337befb9b1a8 100644 (file)
--- 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/complement.cvc b/test/regress/regress0/sets/complement.cvc
new file mode 100644 (file)
index 0000000..6181cbe
--- /dev/null
+++ b/test/regress/regress0/sets/complement.cvc
@@ -0,0 +1,9 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+a : SET OF [Atom];
+b : SET OF [Atom];
+
+ASSERT a = (NOT b);
+
+CHECKSAT;

diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc
new file mode 100644 (file)
index 0000000..6802065
--- /dev/null
+++ b/test/regress/regress0/sets/complement2.cvc
@@ -0,0 +1,11 @@
+% EXPECT: unsat\r
+OPTION "logic" "ALL_SUPPORTED";\r
+Atom: TYPE;\r
+a : SET OF Atom;\r
+b : SET OF Atom;\r
+c : Atom;\r
+\r
+ASSERT a = NOT(a);\r
+ASSERT c IS_IN a;\r
+\r
+CHECKSAT;\r

diff --git a/test/regress/regress0/sets/compliment.cvc b/test/regress/regress0/sets/compliment.cvc
deleted file mode 100644 (file)
index 6181cbe..0000000
--- a/test/regress/regress0/sets/compliment.cvc
+++ /dev/null
@@ -1,9 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-Atom: TYPE;
-a : SET OF [Atom];
-b : SET OF [Atom];
-
-ASSERT a = (NOT b);
-
-CHECKSAT;

diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2
index 5d10e27cbf7af0c7d34bd50d831ec5249a9b28c7..ec975077632074453043ef7181cfb4b91545eb6c 100644 (file)
--- 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)