Skip to content

Commit 4e11cbc

Browse files
tautschnigtautschnig
authored
Merge pull request #1378 from diffblue/smv-grammar-basic-expr
SMV grammar: rename `term` -> `basic_expr`
2 parents 43ee451 + a6c12a6 commit 4e11cbc

File tree

1 file changed

+86
-87
lines changed

1 file changed

+86
-87
lines changed

‎src/smvlang/parser.y‎

Lines changed: 86 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -810,100 +810,99 @@ define : assignment_var BECOMES_Token formula ';'
810810
}
811811
;
812812

813-
formula : term
813+
formula : basic_expr
814814
;
815815

816816
constant : NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
817817
| TRUE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
818818
| FALSE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_false); stack_expr($$).type()=typet(ID_bool); }
819819
;
820820

821-
term : constant
821+
basic_expr : constant
822822
| variable_identifier
823-
| '(' formula ')' { $$=$2; }
824-
| NOT_Token term { init($$, ID_not); mto($$, $2); }
825-
| "abs" '(' term ')' { unary($$, ID_smv_abs, $3); }
826-
| "max" '(' term ',' term ')' { binary($$, $3, ID_smv_max, $5); }
827-
| "min" '(' term ',' term ')' { binary($$, $3, ID_smv_min, $5); }
828-
| term AND_Token term { j_binary($$, $1, ID_and, $3); }
829-
| term OR_Token term { j_binary($$, $1, ID_or, $3); }
830-
| term xor_Token term { j_binary($$, $1, ID_xor, $3); }
831-
| term xnor_Token term { binary($$, $1, ID_xnor, $3); }
832-
| term IMPLIES_Token term { binary($$, $1, ID_implies, $3); }
833-
| term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3); }
834-
| term EQUAL_Token term { binary($$, $1, ID_equal, $3); }
835-
| term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
836-
| term LT_Token term { binary($$, $1, ID_lt, $3); }
837-
| term LE_Token term { binary($$, $1, ID_le, $3); }
838-
| term GT_Token term { binary($$, $1, ID_gt, $3); }
839-
| term GE_Token term { binary($$, $1, ID_ge, $3); }
840-
| MINUS_Token term %prec UMINUS
841-
{ init($$, ID_unary_minus); mto($$, $2); }
842-
| term PLUS_Token term { binary($$, $1, ID_plus, $3); }
843-
| term MINUS_Token term { binary($$, $1, ID_minus, $3); }
844-
| term TIMES_Token term { binary($$, $1, ID_mult, $3); }
845-
| term DIVIDE_Token term { binary($$, $1, ID_div, $3); }
846-
| term mod_Token term { binary($$, $1, ID_mod, $3); }
847-
| term GTGT_Token term { binary($$, $1, ID_shr, $3); }
848-
| term LTLT_Token term { binary($$, $1, ID_shl, $3); }
849-
| term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); }
850-
| "word1" '(' term ')' { unary($$, ID_smv_word1, $3); }
851-
| "bool" '(' term ')' { unary($$, ID_smv_bool, $3); }
852-
| "toint" '(' term ')' { unary($$, ID_smv_toint, $3); }
853-
| "count" '(' term_list ')' { $$=$3; stack_expr($$).id(ID_smv_count); }
854-
| swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); }
855-
| uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); }
856-
| signed_Token '(' term ')' { unary($$, ID_smv_signed_cast, $3); }
857-
| unsigned_Token '(' term ')' { unary($$, ID_smv_unsigned_cast, $3); }
858-
| sizeof_Token '(' term ')' { unary($$, ID_smv_sizeof, $3); }
859-
| extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
860-
| resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
861-
| term union_Token term { binary($$, $1, ID_smv_union, $3); }
862-
| '{' set_body_expr '}' { $$=$2; stack_expr($$).id(ID_smv_set); }
863-
| term in_Token term { binary($$, $1, ID_smv_setin, $3); }
864-
| term IF_Token term ':' term %prec IF_Token
865-
{ init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); }
866-
| case_Token cases esac_Token { $$=$2; }
867-
| next_Token '(' term ')' { init($$, ID_smv_next); mto($$, $3); }
823+
| '(' formula ')' { $$=$2; }
824+
| NOT_Token basic_expr { init($$, ID_not); mto($$, $2); }
825+
| "abs" '(' basic_expr ')' { unary($$, ID_smv_abs, $3); }
826+
| "max" '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_max, $5); }
827+
| "min" '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_min, $5); }
828+
| basic_expr AND_Token basic_expr { j_binary($$, $1, ID_and, $3); }
829+
| basic_expr OR_Token basic_expr { j_binary($$, $1, ID_or, $3); }
830+
| basic_expr xor_Token basic_expr { j_binary($$, $1, ID_xor, $3); }
831+
| basic_expr xnor_Token basic_expr { binary($$, $1, ID_xnor, $3); }
832+
| basic_expr IMPLIES_Token basic_expr { binary($$, $1, ID_implies, $3); }
833+
| basic_expr EQUIV_Token basic_expr { binary($$, $1, ID_smv_iff, $3); }
834+
| basic_expr EQUAL_Token basic_expr { binary($$, $1, ID_equal, $3); }
835+
| basic_expr NOTEQUAL_Token basic_expr { binary($$, $1, ID_notequal, $3); }
836+
| basic_expr LT_Token basic_expr { binary($$, $1, ID_lt, $3); }
837+
| basic_expr LE_Token basic_expr { binary($$, $1, ID_le, $3); }
838+
| basic_expr GT_Token basic_expr { binary($$, $1, ID_gt, $3); }
839+
| basic_expr GE_Token basic_expr { binary($$, $1, ID_ge, $3); }
840+
| MINUS_Token basic_expr %prec UMINUS { init($$, ID_unary_minus); mto($$, $2); }
841+
| basic_expr PLUS_Token basic_expr { binary($$, $1, ID_plus, $3); }
842+
| basic_expr MINUS_Token basic_expr { binary($$, $1, ID_minus, $3); }
843+
| basic_expr TIMES_Token basic_expr { binary($$, $1, ID_mult, $3); }
844+
| basic_expr DIVIDE_Token basic_expr { binary($$, $1, ID_div, $3); }
845+
| basic_expr mod_Token basic_expr { binary($$, $1, ID_mod, $3); }
846+
| basic_expr GTGT_Token basic_expr { binary($$, $1, ID_shr, $3); }
847+
| basic_expr LTLT_Token basic_expr { binary($$, $1, ID_shl, $3); }
848+
| basic_expr COLONCOLON_Token basic_expr { binary($$, $1, ID_concatenation, $3); }
849+
| "word1" '(' basic_expr ')' { unary($$, ID_smv_word1, $3); }
850+
| "bool" '(' basic_expr ')' { unary($$, ID_smv_bool, $3); }
851+
| "toint" '(' basic_expr ')' { unary($$, ID_smv_toint, $3); }
852+
| "count" '(' basic_expr_list ')' { $$=$3; stack_expr($$).id(ID_smv_count); }
853+
| swconst_Token '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_swconst, $5); }
854+
| uwconst_Token '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_uwconst, $5); }
855+
| signed_Token '(' basic_expr ')' { unary($$, ID_smv_signed_cast, $3); }
856+
| unsigned_Token '(' basic_expr ')' { unary($$, ID_smv_unsigned_cast, $3); }
857+
| sizeof_Token '(' basic_expr ')' { unary($$, ID_smv_sizeof, $3); }
858+
| extend_Token '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_extend, $5); }
859+
| resize_Token '(' basic_expr ',' basic_expr ')' { binary($$, $3, ID_smv_resize, $5); }
860+
| basic_expr union_Token basic_expr { binary($$, $1, ID_smv_union, $3); }
861+
| '{' set_body_expr '}' { $$=$2; stack_expr($$).id(ID_smv_set); }
862+
| basic_expr in_Token basic_expr { binary($$, $1, ID_smv_setin, $3); }
863+
| basic_expr IF_Token basic_expr ':' basic_expr %prec IF_Token
864+
{ init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); }
865+
| case_Token cases esac_Token { $$=$2; }
866+
| next_Token '(' basic_expr ')' { init($$, ID_smv_next); mto($$, $3); }
868867
/* Not in NuSMV manual */
869-
| INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
870-
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
871-
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
872-
| SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
868+
| INC_Token '(' basic_expr ')' { init($$, "inc"); mto($$, $3); }
869+
| DEC_Token '(' basic_expr ')' { init($$, "dec"); mto($$, $3); }
870+
| ADD_Token '(' basic_expr ',' basic_expr ')' { j_binary($$, $3, ID_plus, $5); }
871+
| SUB_Token '(' basic_expr ',' basic_expr ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
873872
| switch_Token '(' variable_identifier ')' '{' switches '}' { init($$, ID_switch); mto($$, $3); mto($$, $6); }
874873
/* CTL */
875-
| AX_Token term { init($$, ID_AX); mto($$, $2); }
876-
| AF_Token term { init($$, ID_AF); mto($$, $2); }
877-
| AG_Token term { init($$, ID_AG); mto($$, $2); }
878-
| EX_Token term { init($$, ID_EX); mto($$, $2); }
879-
| EF_Token term { init($$, ID_EF); mto($$, $2); }
880-
| EG_Token term { init($$, ID_EG); mto($$, $2); }
881-
| A_Token '[' term U_Token term ']' { binary($$, $3, ID_AU, $5); }
882-
| A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5); }
883-
| E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5); }
884-
| E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5); }
874+
| AX_Token basic_expr { init($$, ID_AX); mto($$, $2); }
875+
| AF_Token basic_expr { init($$, ID_AF); mto($$, $2); }
876+
| AG_Token basic_expr { init($$, ID_AG); mto($$, $2); }
877+
| EX_Token basic_expr { init($$, ID_EX); mto($$, $2); }
878+
| EF_Token basic_expr { init($$, ID_EF); mto($$, $2); }
879+
| EG_Token basic_expr { init($$, ID_EG); mto($$, $2); }
880+
| A_Token '[' basic_expr U_Token basic_expr ']' { binary($$, $3, ID_AU, $5); }
881+
| A_Token '[' basic_expr R_Token basic_expr ']' { binary($$, $3, ID_AR, $5); }
882+
| E_Token '[' basic_expr U_Token basic_expr ']' { binary($$, $3, ID_EU, $5); }
883+
| E_Token '[' basic_expr R_Token basic_expr ']' { binary($$, $3, ID_ER, $5); }
885884
/* LTL */
886-
| F_Token term { init($$, ID_F); mto($$, $2); }
887-
| G_Token term { init($$, ID_G); mto($$, $2); }
888-
| X_Token term { init($$, ID_X); mto($$, $2); }
889-
| term U_Token term { binary($$, $1, ID_U, $3); }
890-
| term R_Token term { binary($$, $1, ID_R, $3); }
891-
| term V_Token term { binary($$, $1, ID_R, $3); }
885+
| F_Token basic_expr { init($$, ID_F); mto($$, $2); }
886+
| G_Token basic_expr { init($$, ID_G); mto($$, $2); }
887+
| X_Token basic_expr { init($$, ID_X); mto($$, $2); }
888+
| basic_expr U_Token basic_expr { binary($$, $1, ID_U, $3); }
889+
| basic_expr R_Token basic_expr { binary($$, $1, ID_R, $3); }
890+
| basic_expr V_Token basic_expr { binary($$, $1, ID_R, $3); }
892891
/* LTL PAST */
893-
| Y_Token term { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); }
894-
| Z_Token term { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); }
895-
| H_Token term { $$ = $1; stack_expr($$).id(ID_smv_H); mto($$, $2); }
896-
| H_Token bound term { $$ = $1; stack_expr($$).id(ID_smv_bounded_H); mto($$, $3); }
897-
| O_Token term { $$ = $1; stack_expr($$).id(ID_smv_O); mto($$, $2); }
898-
| O_Token bound term { $$ = $1; stack_expr($$).id(ID_smv_bounded_O); mto($$, $3); }
899-
| term S_Token term { $$ = $2; stack_expr($$).id(ID_smv_S); mto($$, $1); mto($$, $3); }
900-
| term T_Token term { $$ = $2; stack_expr($$).id(ID_smv_T); mto($$, $1); mto($$, $3); }
892+
| Y_Token basic_expr { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); }
893+
| Z_Token basic_expr { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); }
894+
| H_Token basic_expr { $$ = $1; stack_expr($$).id(ID_smv_H); mto($$, $2); }
895+
| H_Token bound basic_expr { $$ = $1; stack_expr($$).id(ID_smv_bounded_H); mto($$, $3); }
896+
| O_Token basic_expr { $$ = $1; stack_expr($$).id(ID_smv_O); mto($$, $2); }
897+
| O_Token bound basic_expr { $$ = $1; stack_expr($$).id(ID_smv_bounded_O); mto($$, $3); }
898+
| basic_expr S_Token basic_expr { $$ = $2; stack_expr($$).id(ID_smv_S); mto($$, $1); mto($$, $3); }
899+
| basic_expr T_Token basic_expr { $$ = $2; stack_expr($$).id(ID_smv_T); mto($$, $1); mto($$, $3); }
901900
/* Real-time CTL */
902-
| EBF_Token range term { $$ = $1; stack_expr($$).id(ID_smv_EBF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
903-
| ABF_Token range term { $$ = $1; stack_expr($$).id(ID_smv_ABF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
904-
| EBG_Token range term { $$ = $1; stack_expr($$).id(ID_smv_EBG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
905-
| ABG_Token range term { $$ = $1; stack_expr($$).id(ID_smv_ABG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
906-
| A_Token '[' term BU_Token range term ']'
901+
| EBF_Token range basic_expr { $$ = $1; stack_expr($$).id(ID_smv_EBF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
902+
| ABF_Token range basic_expr { $$ = $1; stack_expr($$).id(ID_smv_ABF); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
903+
| EBG_Token range basic_expr { $$ = $1; stack_expr($$).id(ID_smv_EBG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
904+
| ABG_Token range basic_expr { $$ = $1; stack_expr($$).id(ID_smv_ABG); stack_expr($$).operands().swap(stack_expr($2).operands()); mto($$, $3); }
905+
| A_Token '[' basic_expr BU_Token range basic_expr ']'
907906
{
908907
$$ = $1;
909908
stack_expr($$).id(ID_smv_ABU);
@@ -912,7 +911,7 @@ term : constant
912911
stack_expr($$).add_to_operands(stack_expr($5).operands()[1]);
913912
mto($$, $6);
914913
}
915-
| E_Token '[' term BU_Token range term ']'
914+
| E_Token '[' basic_expr BU_Token range basic_expr ']'
916915
{
917916
$$ = $1;
918917
stack_expr($$).id(ID_smv_EBU);
@@ -936,9 +935,9 @@ set_body_expr:
936935
| set_body_expr ',' formula { $$=$1; mto($$, $3); }
937936
;
938937

939-
term_list:
940-
term { init($$); mto($$, $1); }
941-
| term_list ',' term { $$=$1; mto($$, $3); }
938+
basic_expr_list:
939+
basic_expr { init($$); mto($$, $1); }
940+
| basic_expr_list ',' basic_expr { $$=$1; mto($$, $3); }
942941
;
943942

944943
identifier : IDENTIFIER_Token
@@ -985,11 +984,11 @@ complex_identifier:
985984
unary($$, ID_member, $1);
986985
stack_expr($$).set(ID_component_name, stack_expr($3).id());
987986
}
988-
| complex_identifier '[' term ']'
987+
| complex_identifier '[' basic_expr ']'
989988
{
990989
binary($$, $1, ID_index, $3);
991990
}
992-
| complex_identifier '(' term ')'
991+
| complex_identifier '(' basic_expr ')'
993992
{
994993
// Not in the NuSMV grammar.
995994
binary($$, $1, ID_index, $3);
@@ -1012,7 +1011,7 @@ switches :
10121011
{ $$=$1; mto($$, $2); }
10131012
;
10141013

1015-
switch : NUMBER_Token ':' term ';'
1014+
switch : NUMBER_Token ':' basic_expr ';'
10161015
{ init($$, ID_switch); mto($$, $1); mto($$, $3); }
10171016
;
10181017

0 commit comments

Comments
 (0)