diff options
Diffstat (limited to 'src/verit/veritLexer.mll')
| -rw-r--r-- | src/verit/veritLexer.mll | 86 |
1 files changed, 66 insertions, 20 deletions
diff --git a/src/verit/veritLexer.mll b/src/verit/veritLexer.mll index 80fcc39..f5b88bf 100644 --- a/src/verit/veritLexer.mll +++ b/src/verit/veritLexer.mll @@ -1,20 +1,16 @@ +{ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2016 *) -(* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) +(* Copyright (C) 2011 - 2019 *) (* *) -(* Inria - École Polytechnique - Université Paris-Sud *) +(* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) (**************************************************************************) -{ open VeritParser exception Eof @@ -62,6 +58,7 @@ "qnt_simplify_ax", QNTS; "qnt_merge_ax", QNTM; "resolution", RESO; + "weaken", WEAK; "and", AND; "not_or", NOR; "or", OR; @@ -97,11 +94,62 @@ "tmp_qnt_simplify", TPQS; "tmp_skolemize", TPSK; "subproof", SUBP; - "hole", HOLE ] + "flatten", FLAT; + "hole", HOLE; + "bbvar", BBVA; + "bbconst", BBCONST; + "bbeq", BBEQ; + "bv_const_neq", BBDIS; + "bbop", BBOP; + "bbnot", BBNOT; + "bbneg", BBNEG; + "bbadd", BBADD; + "bbmul", BBMUL; + "bbult", BBULT; + "bbslt", BBSLT; + "bbconcat", BBCONC; + "bbextract", BBEXTR; + "bbzextend", BBZEXT; + "bbsextend", BBSEXT; + "bbshl", BBSHL; + "bbshr", BBSHR; + "bvand", BVAND; + "bvor", BVOR; + "bvxor", BVXOR; + "bvadd", BVADD; + "bvmul", BVMUL; + "bvult", BVULT; + "bvslt", BVSLT; + "bvule", BVULE; + "bvsle", BVSLE; + "bvshl", BVSHL; + "bvlshr", BVSHR; + "not", NOT; + "xor", XOR; + "ite", ITE; + "let", LET; + "distinct", DIST; + "bbT", BBT; + "bitof", BITOF; + "bvnot", BVNOT; + "bvneg", BVNEG; + "concat", BVCONC; + "extract", BVEXTR; + "zero_extend", BVZEXT; + "sign_extend", BVSEXT; + "select", SELECT; + "diff", DIFF; + "store", STORE; + "row1", ROW1; + "row2", ROW2; + "ext", EXTE; + ] } let digit = [ '0'-'9' ] +let bit = [ '0'-'1' ] +let bitvector = '#' 'b' bit+ let alpha = [ 'a'-'z' 'A' - 'Z' ] let blank = [' ' '\t'] let newline = ['\n' '\r'] @@ -116,14 +164,14 @@ rule token = parse | newline + { EOL } | ":" { COLON } - | "#" { SHARP } + | "#" (int as i) { SHARPINT (int_of_string i) } | "(" { LPAR } | ")" { RPAR } - | "not" { NOT } - | "xor" { XOR } - | "ite" { ITE } + | "[" { LBRACKET } + | "]" { RBRACKET } + | "=" { EQ } | "<" { LT } | "<=" { LEQ } @@ -134,22 +182,20 @@ rule token = parse | "~" { OPP } | "*" { MULT } | "=>" { IMP } - | "let" { LET } - | "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 - (Big_int.big_int_of_string - (Lexing.lexeme lexbuf)) } + | (int as i) { try INT (int_of_string i) + with _ -> + BIGINT (Big_int.big_int_of_string i) } + | bitvector as bv { BITV bv } | var { let v = Lexing.lexeme lexbuf in try Hashtbl.find typ_table v with | Not_found -> VAR v } - | bindvar { BINDVAR (Lexing.lexeme lexbuf) } + | bindvar as v { BINDVAR v } | atvar { ATVAR (Lexing.lexeme lexbuf) } |