diff options
Diffstat (limited to 'src/verit/veritLexer.mll')
| -rw-r--r-- | src/verit/veritLexer.mll | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/verit/veritLexer.mll b/src/verit/veritLexer.mll index 2a51a02..80fcc39 100644 --- a/src/verit/veritLexer.mll +++ b/src/verit/veritLexer.mll @@ -55,6 +55,7 @@ "dl_disequality", DLDE; "la_disequality", LADE; "forall_inst", FINS; + "forall", FORALL; "exists_inst", EINS; "skolem_ex_ax", SKEA; "skolem_all_ax", SKAA; @@ -105,6 +106,7 @@ let alpha = [ 'a'-'z' 'A' - 'Z' ] let blank = [' ' '\t'] let newline = ['\n' '\r'] let var = alpha (alpha|digit|'_')* +let atvar = '@' var let bindvar = '?' var+ let int = '-'? digit+ @@ -136,7 +138,9 @@ rule token = parse | "distinct" { DIST } | "Formula is Satisfiable" { SAT } - + | "Tindex_" (int as i) { TINDEX (int_of_string i) } + | "Int" { TINT } + | "Bool" { TBOOL } | int { try INT (int_of_string (Lexing.lexeme lexbuf)) with _ -> BIGINT @@ -147,4 +151,6 @@ rule token = parse | Not_found -> VAR v } | bindvar { BINDVAR (Lexing.lexeme lexbuf) } + | atvar { ATVAR (Lexing.lexeme lexbuf) } + | eof { raise Eof } |