parse_smtv2_model_parser.mly 2.41 KB
Newer Older
David Hauzar's avatar
David Hauzar committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
%{
%}

%start <Model_parser.model_element list> output

%token <string> SPACE
%token <string> ATOM
%token STORE
%token CONST
%token AS
%token <string> INT_STR
%token <string> MINUS_INT_STR
%token LPAREN RPAREN
%token EOF
%%

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

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

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

term:
| text { $1 }
35
| LPAREN term_list RPAREN
David Hauzar's avatar
David Hauzar committed
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
    { "(" ^ $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 }
55
| other_val_str { Model_parser.Unparsed $1 }
David Hauzar's avatar
David Hauzar committed
56 57 58 59
| array { Model_parser.Array $1 }

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

(* Everything that cannot be integer (positive and negative) and array. *)
other_val_str:
| text_without_int { $1 }
| LPAREN possible_space RPAREN { "(" ^ $2 ^ ")" }
67
| LPAREN possible_space paren_other_val_str RPAREN
David Hauzar's avatar
David Hauzar committed
68 69 70 71 72
    { "(" ^ $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 }
73
| LPAREN possible_space other_than_const_array possible_space RPAREN
74
    { "(" ^ $3 ^ ")" }
David Hauzar's avatar
David Hauzar committed
75 76 77 78 79 80 81 82 83 84 85 86 87

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"  }

(* Example:
88 89
   (store (store ((as const (Array Int Int)) 0) 1 2) 3 4)
   (store (store ((as const (Array Int Int)) false) 1 true) 3 true) *)
David Hauzar's avatar
David Hauzar committed
90
array:
91 92 93 94
| LPAREN possible_space
    LPAREN possible_space
      AS SPACE CONST possible_space array_skipped_part possible_space
    RPAREN possible_space
95
    value possible_space
96
  RPAREN
David Hauzar's avatar
David Hauzar committed
97
    { Model_parser.array_create_constant ~value:$13 }
98
| LPAREN possible_space
99
    STORE possible_space array possible_space value SPACE integer
100 101
    possible_space
  RPAREN
102
    { Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
David Hauzar's avatar
David Hauzar committed
103 104 105

array_skipped_part:
| LPAREN term_list RPAREN {}