From fb51c4e5494ad1dd71d6b343e20df3a5806ffc01 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 10 Jul 2014 13:11:36 -0400 Subject: [PATCH] membership cvc token changed to `IS_IN' to avoid conflict with IN used for let --- src/parser/antlr_input_imports.cpp | 3 +++ src/parser/cvc/Cvc.g | 8 ++++--- src/printer/cvc/cvc_printer.cpp | 2 +- test/regress/regress0/sets/cvc-sample.cvc | 26 +++++++++++------------ 4 files changed, 21 insertions(+), 18 deletions(-) diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 07283f1af..f50dd5879 100644 --- 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 12a3fa6f2..0a440f299 100644 --- 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 41e87b809..9b3e83578 100644 --- 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 c6fb95a77..6740faa8c 100644 --- 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; -- 2.30.2