File: smt_parser.mly

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 (288 lines) | stat: -rw-r--r-- 7,329 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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
/******************************************************************************/
/*     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 Smt_ast

  let loc () = symbol_start_pos (), symbol_end_pos ()

  let mk_term t = { term = t; tloc = loc () }

  let mk_form f = { formula = f; floc = loc () }

  let status = ref Unknown

%}

%token BENCHMARK
%token LOGIC
%token THEORY

/* attributes */
%token ASSUMPTION_ATRB 
%token AXIOMS_ATRB 
%token DEFINITION_ATRB 
%token EXTENSIONS_ATRB 
%token FORMULA_ATRB
%token FUNS_ATRB 
%token EXTRAFUNS_ATRB 
%token EXTRASORTS_ATRB
%token EXTRAPREDS_ATRB 
%token LANGUAGE_ATRB
%token LOGIC_ATRB
%token NOTES_ATRB
%token PREDS_ATRB
%token REWRITING_ATRB 
%token SORTS_ATRB 
%token STATUS_ATRB 
%token THEORY_ATRB 
%token <string> ATTRIBUTE

/* status */
%token SAT UNSAT UNKNOWN

/* symbols */
%token <string> NUMERAL
%token <string> RATIONAL
%token <string> ID
%token <string> ARSYMB
%token <string> USER_VALUE
%token <string> VAR
%token <string> FVAR
%token <string> STRING

/* predicates */
%token EQUALS
%token DISTINCT

/* connectives */
%token ITE
%token NOT
%token IMPLIES
%token IFTHENELSE
%token AND OR XOR
%token IFF

/* formulas */
%token TRUE FALSE
%token EXISTS FORALL
%token LET FLET

/* misc */
%token LP RP
%token EOF


%start benchmark logic theory
%type <Smt_ast.pbench> benchmark
%type <Smt_ast.plogic> logic
%type <Smt_ast.ptheory> theory

%%

theory:
| LP THEORY ID theory_attributes RP { $3 , List.rev $4 }
;

theory_attributes:
| theory_attribute { [$1] }
| theory_attributes theory_attribute { $2::$1 }
;

theory_attribute:
| SORTS_ATRB LP ids RP { Tsorts $3 }
| FUNS_ATRB LP fun_decls RP { Funs $3 }
| PREDS_ATRB LP pred_decls RP { Preds $3 }
| DEFINITION_ATRB STRING { Definition $2 }
| AXIOMS_ATRB LP formulas RP { Axioms $3 }
| NOTES_ATRB STRING { Tcomment }
| annot { Tcomment }
;

logic:
| LP LOGIC ID logic_attributes RP { $3 , List.rev $4 }
;

logic_attributes:
| logic_attribute { [$1] }
| logic_attributes logic_attribute { $2::$1 }
;

logic_attribute:
| THEORY_ATRB ID { Ltheory $2 }
| LANGUAGE_ATRB STRING { Lcomment }
| EXTENSIONS_ATRB STRING { Lcomment }
| NOTES_ATRB STRING { Lcomment }
| annot { Lcomment }
;

benchmark:
| LP BENCHMARK ID bench_attributes RP { $3 , List.rev $4 , !status}
;

bench_attributes:
| bench_attribute { [$1] }
| bench_attributes NOTES_ATRB STRING {$1}
| bench_attributes bench_attribute  { $2::$1 }
;

bench_attribute:
| LOGIC_ATRB ID                    { Pblogic $2 } 
| ASSUMPTION_ATRB formula          { Pbassumption (loc (), $2) }
| FORMULA_ATRB formula             { Pbformula (loc (), $2) }
| STATUS_ATRB status               { status:=$2;Pbstatus $2 }
| EXTRASORTS_ATRB LP ids RP        { Pbextr_sorts (List.rev $3) }
| EXTRAFUNS_ATRB LP fun_decls RP   { Pbextr_funs (List.rev $3) }
| EXTRAPREDS_ATRB LP pred_decls RP { Pbextr_preds (List.rev $3) }
| REWRITING_ATRB formulas          { Pbrewriting (loc (), $2) }
| annot                            { Pannotation }
;  

status:
| SAT     { Sat }
| UNSAT   { Unsat }
| UNKNOWN { Unknown }
;

symb:
| ID      { $1 }
| ARSYMB  { $1 }

fun_decls:
| fun_decls fun_decl { $2::$1 }
| fun_decl { [$1] }
;

fun_decl:
| LP symb ids opt_annots RP 
    { match $3 with 
	  r::l -> (loc (), {fname=$2; fargs=List.rev l; fres=r } )
	| [] -> assert false }
| LP NUMERAL ID opt_annots RP { (loc (), {fname=$2; fargs=[]; fres=(loc (), $3) } ) }
;  

pred_decls:
| pred_decls pred_decl { $2::$1 }
| pred_decl { [$1] }
;

pred_decl:
| LP symb opt_ids opt_annots RP  { (loc (), {pname=$2; pargs=List.rev $3}) }
;  

opt_ids:
| /* epsilon */ { [] }
| ids           { $1 }
;

ids:
| ID        { [(loc (),$1)] }
| ids ID { (loc (),$2)::$1 }
;

formulas:
| formula { [$1] }
| formula formulas { $1::$2 }
;

formula:
| TRUE                                                
   { mk_form True }
| LP TRUE annots RP                                   
   { mk_form True }
| FALSE                                               
   { mk_form False }
| LP FALSE annots RP                                  
   { mk_form False }
| FVAR                                                
   { mk_form (Fvar $1) }
| LP FVAR annots RP                                   
   { mk_form (Fvar $2) }
| ID                                                  
   { mk_form (Pred($1,[]) )}
| LP symb terms opt_annots RP                         
   { mk_form (Pred($2,List.rev $3)) }
| LP DISTINCT terms opt_annots RP                     
   { mk_form (Distinct (List.rev $3))}
| LP EQUALS terms opt_annots RP                       
   { mk_form (Equals (List.rev $3))}
| LP NOT formula opt_annots RP                        
   { mk_form (Not $3) }
| LP IMPLIES formula formula opt_annots RP            
   { mk_form (Implies($3,$4)) }
| LP IFTHENELSE formula formula formula opt_annots RP 
   { mk_form (Fite($3,$4,$5)) }
| LP AND formulas opt_annots RP                       
   { mk_form (And $3) }
| LP OR  formulas opt_annots RP                       
   { mk_form (Or $3) }
| LP XOR formulas opt_annots RP                       
   { mk_form (Xor $3) }
| LP IFF formulas opt_annots RP                       
   { mk_form (Iff $3) }
| LP FORALL binders formula opt_annots RP          
   { mk_form (Forall(List.rev $3,$4)) }
| LP EXISTS binders formula opt_annots RP          
   { mk_form (Exists(List.rev $3,$4)) }
| LP LET LP VAR term RP formula opt_annots RP      
   { mk_form (Let($4,mk_term $5,$7)) }
| LP FLET LP FVAR formula RP formula opt_annots RP 
   { mk_form (Flet($4,$5,$7)) }
;

opt_annots:
| /* epsilon */ {  }
| annots   {  }
;

annots:
| annot {}
| annots annot {}
;

annot:
| ATTRIBUTE            { }
| ATTRIBUTE USER_VALUE { }
;

binders:
| binder         { [$1] }
| binders binder { $2::$1 }
;

binder:
| LP VAR ID RP   { { var=$2 ; sort=$3 } }
;

terms:
| term       { [mk_term $1] }
| terms term { (mk_term $2)::$1 }

term:
| baseterm  { $1 }
| LP baseterm annots RP { $2 }
| LP ID terms opt_annots RP { Fun($2,List.rev $3) }
| LP VAR terms opt_annots RP { Fun($2,List.rev $3) }
| LP ARSYMB terms opt_annots RP { Fun($2,List.rev $3) }
| LP ITE formula term term opt_annots RP { Ite($3,mk_term $4,mk_term $5) }
;

baseterm:
| VAR { Var $1 }
| ID  { Fun($1,[]) }
| NUMERAL { Num $1 }
| RATIONAL { Rat $1 }
;