parse_smtv2_model_lexer.mll 4.24 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
{
13
  open Parse_smtv2_model_parser
14
  exception SyntaxError
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

  let interp_float b eb sb =
    try
      let is_neg = match b with
        | "#b0" -> false
        | "#b1" -> true
        | _ -> raise Exit
      in
      if String.sub eb 0 2 = "#b" && String.length eb = 13 &&
         String.sub sb 0 2 = "#x" && String.length sb = 15 then
         (* binary 64 *)
         let exp_base2 = String.sub eb 2 11 in
         let exp = int_of_string ("0b" ^ exp_base2) - 1023 in
         let mant_base16 = String.sub sb 2 13 in
         Model_parser.Float_hexa((if is_neg then "-" else "")^
         "0x1."^mant_base16^"p"^(string_of_int exp))
      else
      if String.sub eb 0 2 = "#x" && String.length eb = 4 &&
         String.sub sb 0 2 = "#b" && String.length eb = 25 then
         (* binary 32 *)
         let exp_base16 = String.sub eb 2 2 in
         let mant_base2 = String.sub sb 2 23 in
           raise Exit (* TODO *)
         else raise Exit
   with Exit -> Model_parser.Float_value (b, eb, sb)
40 41 42
}

let atom = [^'('')'' ''\t''\n']
43
let space = [' ''\t''\n''\r']
David Hauzar's avatar
David Hauzar committed
44
let num = ['0'-'9']+
45
let opt_num = ['0'-'9']*
46
let hexa_num = ( num | ['a' - 'f'] | ['A' - 'F'])+
47
let dec_num = num"."num
48
let name = (['a'-'z']*'_'*['0'-'9']*)*
49
let dummy = ('_''_''_')?
50
let float_num = '#'('b' | 'x') hexa_num
51

52 53 54 55

rule token = parse
  | '\n'
    { token lexbuf }
56 57
  | space+
      { token lexbuf }
58 59
  | "store" { STORE }
  | "const" { CONST }
60
  | "model" {MODEL}
61 62 63 64 65
  | "as" { AS }
  | '('
      { LPAREN }
  | ')'
      { RPAREN }
66 67 68 69
  | ';' { read_string (Buffer.create 17) lexbuf }
  | ";;" { read_string (Buffer.create 17) lexbuf }
  | '=' { EQUAL }
  | '_' { UNDERSCORE }
70
  | '/' { DIV }
71 72 73 74 75 76
  | "as-array" { AS_ARRAY }
  | "ite" { ITE }
  | "define-fun" { DEFINE_FUN }
  | "declare-fun" { DECLARE_FUN }
  | "declare-sort" { DECLARE_SORT } (* z3 declare functions *)
  | "forall" { FORALL } (* z3 cardinality *)
77 78 79 80
  | "not" { NOT } (* Z3 specific *)
  | "and" { AND } (* z3 specific in ite  *)
  | "<=" { LE } (* z3 specific *)
  | ">=" { GE } (* z3 specific *)
81 82 83 84 85 86
  | "declare-datatypes" { DECLARE_DATATYPES }
  | "let" { LET }
  | "true" { TRUE }
  | "false" { FALSE }
  | "LAMBDA" { LAMBDA }
  | "ARRAY_LAMBDA" { ARRAY_LAMBDA }
87 88
  | "(_" space+ "bv"(num as bv_value) space+ num")" { BITVECTOR_VALUE bv_value }
  | "(_" space+ "BitVec" space+ num")" { BITVECTOR_TYPE }
89
  | "(_" space+ "extract" space+ num space+ num ")" as s { BITVECTOR_EXTRACT s }
90

91 92 93 94 95
  | "(_" space+ "+zero" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Plus_zero }
  | "(_" space+ "-zero" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Minus_zero }
  | "(_"  space+ "+oo" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Plus_infinity }
  | "(_" space+ "-oo" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Minus_infinity }
  | "(_" space+ "NaN" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Not_a_number }
96
  | "(fp" space+ (float_num as b) space+ (float_num as eb) space+ (float_num as sb) ")"
97
      { FLOAT_VALUE (interp_float b eb sb) }
98

David Hauzar's avatar
David Hauzar committed
99
  | num as integer
100
      { INT_STR (integer) }
101 102 103 104 105
  | '-'space*(num as integer) { MINUS_INT_STR ("-"^integer) }
  | (num as int_part)"."(num as fract_part)
      { DEC_STR (int_part, fract_part)  }
  | '-'space*(num as int_part)"."(num as fract_part)
      {MINUS_DEC_STR (("-"^int_part), fract_part)}
106 107 108 109
  | atom+ as at { ATOM (at) }
  | eof
      { EOF }
  | _
110
      { raise SyntaxError }
111 112 113 114 115 116 117

and read_string buf =
  parse
  | '\n'      { COMMENT (Buffer.contents buf) }
  | '\r'      { COMMENT (Buffer.contents buf) }
  | eof       { COMMENT (Buffer.contents buf) }
  | _ as a    { Buffer.add_char buf a; read_string buf lexbuf }