1 files changed, 88 insertions, 0 deletions
diff --git a/src/verit/smtlib2_lex.mll b/src/verit/smtlib2_lex.mll
new file mode 100644
index 0000000..f235403
--- /dev/null
+++ b/src/verit/smtlib2_lex.mll
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq, originally belong to The Alt-ergo theorem prover           *)
+(*     Copyright (C) 2006-2010                                            *)
+(*                                                                        *)
+(*     Sylvain Conchon                                                    *)
+(*     Evelyne Contejean                                                  *)
+(*     Stephane Lescuyer                                                  *)
+(*     Mohamed Iguernelala                                                *)
+(*     Alain Mebsout                                                      *)
+(*                                                                        *)
+(*     CNRS - INRIA - Universite Paris Sud                                *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+{
+open Lexing
+open Smtlib2_parse
+
+
+let newline lexbuf =
+    let pos = lexbuf.lex_curr_p in
+    lexbuf.lex_curr_p <-
+      { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum;
+        pos_cnum=0 }
+
+}
+
+rule token = parse
+| ['\t' ' ' ]+
+    { token lexbuf }
+| ';'  (_ # '\n')*
+     { token lexbuf }
+| ['\n']+ as str
+     { newline lexbuf;
+       Smtlib2_util.line := (!Smtlib2_util.line + (String.length str));
+       token lexbuf }
+| "_"              { UNDERSCORE }
+| "("              { LPAREN }
+| ")"              { RPAREN }
+| "as"             { AS }
+| "let"            { LET }
+| "forall"         { FORALL }
+| "exists"         { EXISTS }
+| "!"              { EXCLIMATIONPT }
+| "set-logic"      { SETLOGIC }
+| "set-option"     { SETOPTION }
+| "set-info"       { SETINFO }
+| "declare-sort"   { DECLARESORT }
+| "define-sort"    { DEFINESORT }
+| "declare-fun"    { DECLAREFUN }
+| "define-fun"     { DEFINEFUN }
+| "push"           { PUSH }
+| "pop"            { POP }
+| "assert"         { ASSERT }
+| "check-sat"      { CHECKSAT }
+| "get-assertions" { GETASSERT }
+| "get-proof"      { GETPROOF }
+| "get-unsat-core" { GETUNSATCORE }
+| "get-value"      { GETVALUE }
+| "get-assignment" { GETASSIGN }
+| "get-option"     { GETOPTION }
+| "get-info"       { GETINFO }
+| "exit"           { EXIT }
+|  '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+  as str
+    { HEXADECIMAL(str) }
+|  '#' 'b' ['0'-'1']+  as str
+    { BINARY(str) }
+|  '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|'  as str
+    { ASCIIWOR(str) }
+|  ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']+  as str
+    { KEYWORD(str) }
+|  ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']*  as str
+    { SYMBOL(str) }
+|  '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\' ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"' as str
+    { STRINGLIT(str) }
+|  ( '0' | ['1'-'9'] ['0'-'9']* )  as str
+    { NUMERAL(str) }
+|  ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str
+    { DECIMAL(str) }
+| eof
+    { EOF }
+| _
+    {failwith(
+      (Lexing.lexeme lexbuf) ^
+	": lexing error on line "^(string_of_int !Smtlib2_util.line))}{}