File: smtlib2_lex.mll

package info (click to toggle)
alt-ergo 0.95.2-3
  • links: PTS, VCS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 1,528 kB
  • ctags: 3,449
  • sloc: ml: 19,645; makefile: 354
file content (89 lines) | stat: -rw-r--r-- 3,540 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
(******************************************************************************)
(*     The Alt-Ergo theorem prover                                            *)
(*     Copyright (C) 2006-2013                                                *)
(*     CNRS - INRIA - Universite Paris Sud                                    *)
(*                                                                            *)
(*     Sylvain Conchon                                                        *)
(*     Evelyne Contejean                                                      *)
(*                                                                            *)
(*     Francois Bobot                                                         *)
(*     Mohamed Iguernelala                                                    *)
(*     Stephane Lescuyer                                                      *)
(*     Alain Mebsout                                                          *)
(*                                                                            *)
(*   This file is distributed under the terms of the CeCILL-C licence         *)
(******************************************************************************)

{ 
open Lexing
open Smtlib2_parse

let smtlib2_util_line = ref 1

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 }
| "declare-const"  { DECLARECONST }
| "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))}{}