@@ -675,53 +675,57 @@ define : assignment_var BECOMES_Token formula ';'
675
675
formula : term
676
676
;
677
677
678
- term : variable_identifier
679
- | next_Token ' (' term ' )' { init ($$, ID_smv_next); mto ($$, $3 ); }
680
- | ' (' formula ' )' { $$=$2 ; }
681
- | ' {' set_body_expr ' }' { $$=$2 ; stack_expr ($$).id (ID_smv_set); }
682
- | INC_Token ' (' term ' )' { init ($$, " inc" ); mto ($$, $3 ); }
683
- | DEC_Token ' (' term ' )' { init ($$, " dec" ); mto ($$, $3 ); }
684
- | ADD_Token ' (' term ' ,' term ' )' { j_binary ($$, $3 , ID_plus, $5 ); }
685
- | SUB_Token ' (' term ' ,' term ' )' { init ($$, ID_minus); mto ($$, $3 ); mto ($$, $5 ); }
686
- | NUMBER_Token { init ($$, ID_constant); stack_expr ($$).set (ID_value, stack_expr ($1 ).id ()); stack_expr ($$).type ()=integer_typet (); }
678
+ constant : NUMBER_Token { init ($$, ID_constant); stack_expr ($$).set (ID_value, stack_expr ($1 ).id ()); stack_expr ($$).type ()=integer_typet (); }
687
679
| TRUE_Token { init ($$, ID_constant); stack_expr ($$).set (ID_value, ID_true); stack_expr ($$).type ()=typet (ID_bool); }
688
680
| FALSE_Token { init ($$, ID_constant); stack_expr ($$).set (ID_value, ID_false); stack_expr ($$).type ()=typet (ID_bool); }
689
- | case_Token cases esac_Token { $$=$2 ; }
690
- | term IF_Token term ' :' term %prec IF_Token
691
- { init ($$, ID_if); mto ($$, $1 ); mto ($$, $3 ); mto ($$, $5 ); }
692
- | switch_Token ' (' variable_identifier ' )' ' {' switches ' }' { init ($$, ID_switch); mto ($$, $3 ); mto ($$, $6 ); }
693
- | MINUS_Token term %prec UMINUS
694
- { init ($$, ID_unary_minus); mto ($$, $2 ); }
695
- | term mod_Token term { binary ($$, $1 , ID_mod, $3 ); }
696
- | term GTGT_Token term { binary ($$, $1 , ID_shr, $3 ); }
697
- | term LTLT_Token term { binary ($$, $1 , ID_shl, $3 ); }
698
- | term COLONCOLON_Token term { binary ($$, $1 , ID_concatenation, $3 ); }
699
- | term TIMES_Token term { binary ($$, $1 , ID_mult, $3 ); }
700
- | term DIVIDE_Token term { binary ($$, $1 , ID_div, $3 ); }
701
- | term PLUS_Token term { binary ($$, $1 , ID_plus, $3 ); }
702
- | term MINUS_Token term { binary ($$, $1 , ID_minus, $3 ); }
703
- | term EQUIV_Token term { binary ($$, $1 , ID_smv_iff, $3 ); }
704
- | term IMPLIES_Token term { binary ($$, $1 , ID_implies, $3 ); }
681
+ ;
682
+
683
+ term : constant
684
+ | variable_identifier
685
+ | ' (' formula ' )' { $$=$2 ; }
686
+ | NOT_Token term { init ($$, ID_not); mto ($$, $2 ); }
687
+ | term AND_Token term { j_binary ($$, $1 , ID_and, $3 ); }
688
+ | term OR_Token term { j_binary ($$, $1 , ID_or, $3 ); }
705
689
| term xor_Token term { j_binary ($$, $1 , ID_xor, $3 ); }
706
690
| term xnor_Token term { binary ($$, $1 , ID_xnor, $3 ); }
707
- | term OR_Token term { j_binary ($$, $1 , ID_or, $3 ); }
708
- | term AND_Token term { j_binary ($$, $1 , ID_and, $3 ); }
709
- | NOT_Token term { init ($$, ID_not); mto ($$, $2 ); }
691
+ | term IMPLIES_Token term { binary ($$, $1 , ID_implies, $3 ); }
692
+ | term EQUIV_Token term { binary ($$, $1 , ID_smv_iff, $3 ); }
710
693
| term EQUAL_Token term { binary ($$, $1 , ID_equal, $3 ); }
711
694
| term NOTEQUAL_Token term { binary ($$, $1 , ID_notequal, $3 ); }
712
695
| term LT_Token term { binary ($$, $1 , ID_lt, $3 ); }
713
696
| term LE_Token term { binary ($$, $1 , ID_le, $3 ); }
714
697
| term GT_Token term { binary ($$, $1 , ID_gt, $3 ); }
715
698
| term GE_Token term { binary ($$, $1 , ID_ge, $3 ); }
716
- | term union_Token term { binary ($$, $1 , ID_smv_union, $3 ); }
717
- | term in_Token term { binary ($$, $1 , ID_smv_setin, $3 ); }
718
- | extend_Token ' (' term ' ,' term ' )' { binary ($$, $3 , ID_smv_extend, $5 ); }
719
- | resize_Token ' (' term ' ,' term ' )' { binary ($$, $3 , ID_smv_resize, $5 ); }
720
- | signed_Token ' (' term ' )' { init ($$, ID_smv_signed_cast); mto ($$, $3 ); }
721
- | sizeof_Token ' (' term ' )' { init ($$, ID_smv_sizeof); mto ($$, $3 ); }
699
+ | MINUS_Token term %prec UMINUS
700
+ { init ($$, ID_unary_minus); mto ($$, $2 ); }
701
+ | term PLUS_Token term { binary ($$, $1 , ID_plus, $3 ); }
702
+ | term MINUS_Token term { binary ($$, $1 , ID_minus, $3 ); }
703
+ | term TIMES_Token term { binary ($$, $1 , ID_mult, $3 ); }
704
+ | term DIVIDE_Token term { binary ($$, $1 , ID_div, $3 ); }
705
+ | term mod_Token term { binary ($$, $1 , ID_mod, $3 ); }
706
+ | term GTGT_Token term { binary ($$, $1 , ID_shr, $3 ); }
707
+ | term LTLT_Token term { binary ($$, $1 , ID_shl, $3 ); }
708
+ | term COLONCOLON_Token term { binary ($$, $1 , ID_concatenation, $3 ); }
722
709
| swconst_Token ' (' term ' ,' term ' )' { binary ($$, $3 , ID_smv_swconst, $5 ); }
723
- | unsigned_Token ' (' term ' )' { init ($$, ID_smv_unsigned_cast); mto ($$, $3 ); }
724
710
| uwconst_Token ' (' term ' ,' term ' )' { binary ($$, $3 , ID_smv_uwconst, $5 ); }
711
+ | signed_Token ' (' term ' )' { init ($$, ID_smv_signed_cast); mto ($$, $3 ); }
712
+ | unsigned_Token ' (' term ' )' { init ($$, ID_smv_unsigned_cast); mto ($$, $3 ); }
713
+ | sizeof_Token ' (' term ' )' { init ($$, ID_smv_sizeof); mto ($$, $3 ); }
714
+ | extend_Token ' (' term ' ,' term ' )' { binary ($$, $3 , ID_smv_extend, $5 ); }
715
+ | resize_Token ' (' term ' ,' term ' )' { binary ($$, $3 , ID_smv_resize, $5 ); }
716
+ | term union_Token term { binary ($$, $1 , ID_smv_union, $3 ); }
717
+ | ' {' set_body_expr ' }' { $$=$2 ; stack_expr ($$).id (ID_smv_set); }
718
+ | term in_Token term { binary ($$, $1 , ID_smv_setin, $3 ); }
719
+ | term IF_Token term ' :' term %prec IF_Token
720
+ { init ($$, ID_if); mto ($$, $1 ); mto ($$, $3 ); mto ($$, $5 ); }
721
+ | case_Token cases esac_Token { $$=$2 ; }
722
+ | next_Token ' (' term ' )' { init ($$, ID_smv_next); mto ($$, $3 ); }
723
+ /* Not in NuSMV manual */
724
+ | INC_Token ' (' term ' )' { init ($$, " inc" ); mto ($$, $3 ); }
725
+ | DEC_Token ' (' term ' )' { init ($$, " dec" ); mto ($$, $3 ); }
726
+ | ADD_Token ' (' term ' ,' term ' )' { j_binary ($$, $3 , ID_plus, $5 ); }
727
+ | SUB_Token ' (' term ' ,' term ' )' { init ($$, ID_minus); mto ($$, $3 ); mto ($$, $5 ); }
728
+ | switch_Token ' (' variable_identifier ' )' ' {' switches ' }' { init ($$, ID_switch); mto ($$, $3 ); mto ($$, $6 ); }
725
729
/* CTL */
726
730
| AX_Token term { init ($$, ID_AX); mto ($$, $2 ); }
727
731
| AF_Token term { init ($$, ID_AF); mto ($$, $2 ); }
0 commit comments