parse_smtv2_model_parser.mly 3.23 KB
Newer Older
David Hauzar's avatar
David Hauzar committed
1 2 3 4 5 6 7 8 9
%{
%}

%start <Model_parser.model_element list> output
%token <string> SPACE
%token <string> ATOM
%token STORE
%token CONST
%token AS
10
%token <string> BITVECTOR_VALUE
11
%token <string> INT_STR
David Hauzar's avatar
David Hauzar committed
12
%token <string> MINUS_INT_STR
13 14
%token <string * string> DEC_STR
%token <string * string> MINUS_DEC_STR
David Hauzar's avatar
David Hauzar committed
15 16 17 18 19 20
%token LPAREN RPAREN
%token EOF
%%

output:
| EOF { [] }
21
| possible_space text { [] }
22 23
| possible_space LPAREN text { [] }
    (* Error of the prover while getting counter-example *)
24
| possible_space LPAREN pairs RPAREN { $3 }
David Hauzar's avatar
David Hauzar committed
25 26 27

pairs:
| possible_space { [] }
28
| possible_space LPAREN term SPACE value RPAREN pairs
29
    { (Model_parser.create_model_element ~name:$3 ~value:$5 ())::$7 }
30

David Hauzar's avatar
David Hauzar committed
31 32 33 34 35 36
possible_space:
| { "" }
| SPACE { $1 }

term:
| text { $1 }
37
| LPAREN term_list RPAREN
David Hauzar's avatar
David Hauzar committed
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
    { "(" ^ $2 ^ ")" }

term_list:
| possible_space { $1 }
| possible_space term term_list { $1 ^ $2 ^ $3 }

text:
| MINUS_INT_STR { $1 }
| INT_STR { $1 }
| text_without_int { $1 }

text_without_int:
| ATOM { $1 }
| STORE { "store" }
| CONST { "const"  }
| AS { "as" }

value:
| integer { $1 }
57
| decimal { $1 }
58
| other_val_str { Model_parser.Unparsed $1 }
David Hauzar's avatar
David Hauzar committed
59
| array { Model_parser.Array $1 }
David Hauzar's avatar
David Hauzar committed
60
| bitvector { Model_parser.Bitvector $1 }
David Hauzar's avatar
David Hauzar committed
61 62 63

integer:
| INT_STR { Model_parser.Integer $1 }
64
| LPAREN possible_space MINUS_INT_STR possible_space RPAREN
David Hauzar's avatar
David Hauzar committed
65 66
    { Model_parser.Integer $3 }

67 68 69 70 71
decimal:
| DEC_STR { Model_parser.Decimal $1 }
| LPAREN possible_space MINUS_DEC_STR possible_space RPAREN
    { Model_parser.Decimal ($3) }

David Hauzar's avatar
David Hauzar committed
72 73 74 75
(* Everything that cannot be integer (positive and negative) and array. *)
other_val_str:
| text_without_int { $1 }
| LPAREN possible_space RPAREN { "(" ^ $2 ^ ")" }
76
| LPAREN possible_space paren_other_val_str RPAREN
David Hauzar's avatar
David Hauzar committed
77 78 79 80 81
    { "(" ^ $3 ^ ")" }

(* Everything that cannot be negative integer and start of an array  *)
paren_other_val_str:
| other_than_neg_int_and_array_store term_list { $1 ^ $2 }
82
| LPAREN possible_space other_than_const_array possible_space RPAREN
83
    { "(" ^ $3 ^ ")" }
David Hauzar's avatar
David Hauzar committed
84 85 86 87 88 89 90 91 92 93 94 95

other_than_neg_int_and_array_store:
| INT_STR { $1 }
| ATOM { $1 }
| CONST { "const"  }
| AS { "as" }

other_than_const_array:
| MINUS_INT_STR { $1 }
| INT_STR { $1 }
| CONST { "const"  }

96 97 98 99 100 101 102 103 104 105
(* Examples:
   (1) Map from int to int:
     (store (store ((as const (Array Int Int)) 0) 1 2) 3 4)
   (2) Map from int to bool:
     (store (store ((as const (Array Int Int)) false) 1 true) 3 true)
   (3) Map from int to map from int to int (all elemets are 0):
     ((as const (Array Int (Array Int Int))) ((as const (Array Int Int)) 0))
   (4) Map from int to map from int to int (element [1][1] is 3, all others are 0)
     (store (store ((as const (Array Int (Array Int Int))) ((as const (Array Int Int)) 0)) 0 (store ((as const (Array Int Int)) 0) 0 3)) 1 (store ((as const (Array Int Int)) 0) 1 3))
*)
David Hauzar's avatar
David Hauzar committed
106
array:
107 108 109 110
| LPAREN possible_space
    LPAREN possible_space
      AS SPACE CONST possible_space array_skipped_part possible_space
    RPAREN possible_space
111
    value possible_space
112
  RPAREN
David Hauzar's avatar
David Hauzar committed
113
    { Model_parser.array_create_constant ~value:$13 }
114
| LPAREN possible_space
115
    STORE possible_space array possible_space value SPACE value
116 117
    possible_space
  RPAREN
118
    { Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
David Hauzar's avatar
David Hauzar committed
119

120 121 122
array_skipped_part:
| LPAREN term_list RPAREN {}

David Hauzar's avatar
David Hauzar committed
123 124 125 126 127
(* Example:
   (_ bv2048 16) *)
bitvector:
| BITVECTOR_VALUE
    { $1 }