membership cvc token changed to `IS_IN' to avoid conflict with IN used for let

diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index 07283f1afc1daccd679aa9d670dcc98f7182f013..f50dd5879931ebddeddef270762ad3686f0ec8b9 100644 (file)
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -143,6 +143,9 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
         ss << "Missing end of file marker.";
       } else if( ex->expecting == 0 ) {
         ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
+        if( std::string(tokenText((pANTLR3_COMMON_TOKEN)ex->token)) == std::string("IN") ) {
+          ss << " Did you mean: `IS_IN'?";
+        }
       } else {
         ss << "Missing " << tokenNames[ex->expecting] << ".";
       }

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 12a3fa6f2ec03aaee3acd1b1f9dca5a3fd9c218c..0a440f2990ea92b0a0093a0c3f3e896a9cdcf32e 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -91,6 +91,7 @@ tokens {
   IN_TOK = 'IN';
   INT_TOK = 'INT';
   LET_TOK = 'LET';
+  MEMBER_TOK = 'IS_IN';
   NOT_TOK = 'NOT';
   OR_TOK = 'OR';
   REAL_TOK = 'REAL';
@@ -288,7 +289,8 @@ int getOperatorPrecedence(int type) {
   case LEQ_TOK:
   case LT_TOK:
   case GEQ_TOK:
-  case GT_TOK: return 25;
+  case GT_TOK:
+  case MEMBER_TOK: return 25;
   case EQUAL_TOK:
   case DISEQUAL_TOK: return 26;
   case NOT_TOK: return 27;
@@ -327,7 +329,7 @@ Kind getOperatorKind(int type, bool& negate) {
   case GEQ_TOK: return kind::GEQ;
   case LT_TOK: return kind::LT;
   case LEQ_TOK: return kind::LEQ;
-  case IN_TOK: return kind::MEMBER;
+  case MEMBER_TOK: return kind::MEMBER;
 
     // arithmeticBinop
   case PLUS_TOK: return kind::PLUS;
@@ -1442,7 +1444,7 @@ comparisonBinop[unsigned& op]
   | GEQ_TOK
   | LT_TOK
   | LEQ_TOK
-  | IN_TOK
+  | MEMBER_TOK
   ;
 
 term[CVC4::Expr& f]

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 41e87b80988100f742464daa72c092fa2d8c7879..9b3e83578a34468ec4a4aaa0bf9aa0b52b82d9ca 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -725,7 +725,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       opType = INFIX;
       break;
     case kind::MEMBER:
-      op << "IN";
+      op << "IS_IN";
       opType = INFIX;
       break;
     case kind::SINGLETON:

diff --git a/test/regress/regress0/sets/cvc-sample.cvc b/test/regress/regress0/sets/cvc-sample.cvc
index c6fb95a77d60831f2467fb1d8da4d2daeb44828d..6740faa8cf349630c28f6067faecc146a07e0f12 100644 (file)
--- a/test/regress/regress0/sets/cvc-sample.cvc
+++ b/test/regress/regress0/sets/cvc-sample.cvc
@@ -1,9 +1,10 @@
+% COMMAND-LINE: --incremental
 % EXPECT: unsat
 % EXPECT: unsat
 % EXPECT: unsat
 % EXPECT: unsat
 % EXPECT: unsat
-% EXPECT: valid
+% EXPECT: invalid
 OPTION "incremental" true;
 OPTION "logic" "ALL_SUPPORTED";
 SetInt : TYPE = SET OF INT;
@@ -22,9 +23,9 @@ ASSERT c = (a | b);
 ASSERT NOT(c = (a & b));
 ASSERT c = (a - b);
 ASSERT a <= b;
-ASSERT e IN c;
-ASSERT e IN a;
-ASSERT e IN (a & b);
+ASSERT e IS_IN c;
+ASSERT e IS_IN a;
+ASSERT e IS_IN (a & b);
 CHECKSAT TRUE;
 POP;
 PUSH;
@@ -35,23 +36,20 @@ POP;
 PUSH;
 ASSERT x = y;
 ASSERT e1 = e2;
-ASSERT e1 IN x;
-ASSERT NOT(e2 IN y);
+ASSERT e1 IS_IN x;
+ASSERT NOT(e2 IS_IN y);
 CHECKSAT TRUE;
 POP;
 PUSH;
 ASSERT x = y;
 ASSERT e1 = e2;
-ASSERT e1 IN (x | z);
-ASSERT NOT(e2 IN (y | z));
+ASSERT e1 IS_IN (x | z);
+ASSERT NOT(e2 IS_IN (y | z));
 CHECKSAT TRUE;
 POP;
 PUSH;
-ASSERT 5 IN ({1, 2, 3, 4} | {5});
-ASSERT 5 IN ({1, 2, 3, 4} | {} :: SET OF INT);
+ASSERT 5 IS_IN ({1, 2, 3, 4} | {5});
+ASSERT 5 IS_IN ({1, 2, 3, 4} | {} :: SET OF INT);
 CHECKSAT TRUE;
 POP;
-PUSH;
-QUERY LET v_0 = e1 IN z
-IN NOT (v_0 AND NOT v_0);
-POP;
+QUERY LET v_0 = e1 IS_IN z IN v_0 AND NOT v_0;