Skip to content

Commit b2e2656

Browse files
committed
SMV: split up constant production rule
This splits up the constant production rule in the SMV grammar, to match the NuSMV manual.
1 parent 8a43f94 commit b2e2656

File tree

1 file changed

+26
-3
lines changed

1 file changed

+26
-3
lines changed

src/smvlang/parser.y

Lines changed: 26 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -813,9 +813,32 @@ define : assignment_var BECOMES_Token formula ';'
813813
formula : basic_expr
814814
;
815815

816-
constant : NUMBER_Token { init($$, ID_constant); stack_expr($$).set(ID_value, stack_expr($1).id()); stack_expr($$).type()=integer_typet(); }
817-
| TRUE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_true); stack_expr($$).type()=typet(ID_bool); }
818-
| FALSE_Token { init($$, ID_constant); stack_expr($$).set(ID_value, ID_false); stack_expr($$).type()=typet(ID_bool); }
816+
constant : boolean_constant
817+
| integer_constant
818+
;
819+
820+
boolean_constant:
821+
TRUE_Token
822+
{
823+
init($$, ID_constant);
824+
stack_expr($$).set(ID_value, ID_true);
825+
stack_expr($$).type()=typet{ID_bool};
826+
}
827+
| FALSE_Token
828+
{
829+
init($$, ID_constant);
830+
stack_expr($$).set(ID_value, ID_false);
831+
stack_expr($$).type()=typet{ID_bool};
832+
}
833+
;
834+
835+
integer_constant:
836+
NUMBER_Token
837+
{
838+
init($$, ID_constant);
839+
stack_expr($$).set(ID_value, stack_expr($1).id());
840+
stack_expr($$).type()=integer_typet{};
841+
}
819842
;
820843

821844
basic_expr : constant

0 commit comments

Comments
 (0)