Source file psmt2_to_alt_ergo.ml
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
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
open AltErgoLib
module Smtlib_error = Psmt2Frontend.Smtlib_error
module Smtlib_options = Psmt2Frontend.Options
module Smtlib_ty = Psmt2Frontend.Smtlib_ty
module Smtlib_typed_env = Psmt2Frontend.Smtlib_typed_env
module Smtlib_typing = Psmt2Frontend.Smtlib_typing
module Smtlib_syntax = Psmt2Frontend.Smtlib_syntax
module Smtlib_parser = Psmt2Frontend.Smtlib_parser
module Smtlib_lexer = Psmt2Frontend.Smtlib_lexer
open Smtlib_syntax
open Parsed_interface
module Translate = struct
let pos x =
match x.p with
| None -> Loc.dummy
| Some p -> p
let must_not_happen loc s =
let s = Format.sprintf
"psmt2-frontend typing should ensure that this case can't happen : %s" s
in
raise (Errors.error (Errors.Syntax_error (loc,s)))
let translate_left_assoc f id params =
match params with
| [] | [_] -> assert false
| t :: l ->
List.fold_left (fun acc t ->
f (pos id) acc t
) t l
let translate_right_assoc f id params =
match List.rev params with
| [] | [_] -> assert false
| t :: l ->
List.fold_left (fun acc t ->
f (pos id) t acc
) t l
let translate_chainable_assoc f id params =
match params with
| [] | [_] -> assert false
| a::b::l ->
let (res,_) = List.fold_left (fun (acc,curr) next ->
mk_and (pos id) acc (f (pos id) curr next), next
) ((f (pos id) a b),b) l
in res
let init n f =
let rec init_aux i n f =
if i >= n then []
else
let r = f i in
r :: init_aux (i+1) n f
in
init_aux 0 n f
let translate_sort sort =
let open Smtlib_ty in
let rec aux ty =
match (shorten ty).desc with
| TDummy -> assert false
| TInt -> int_type
| TReal -> real_type
| TBool -> bool_type
| TString -> assert false
| TArray (t1,t2) -> mk_external_type (pos sort) [aux t1;aux t2] "farray"
| TBitVec _ -> assert false
| TSort (s,t_list) -> mk_external_type (pos sort) (List.map aux t_list) s
| TDatatype (d,t_list) ->
mk_external_type (pos sort) (List.map aux t_list) d
| TVar (s) -> mk_var_type (pos sort) s
| TFun _ -> assert false
| TLink _ -> assert false
| TRoundingMode -> assert false
| TFloatingPoint _ -> assert false
in
aux sort.ty
let translate_constant cst t =
let loc = pos t in
match cst with
| Const_Dec(s) -> mk_real_const loc (Numbers.Q.from_string s)
| Const_Num(s) ->
let open Smtlib_ty in
let ty = shorten t.ty in
begin match ty.desc with
| TInt -> mk_int_const loc s
| TReal -> mk_real_const loc (Numbers.Q.from_string s)
| _ ->
Printer.print_err "%s" (to_string ty);
assert false
end
| Const_Str _ -> assert false
| Const_Hex(s) -> mk_int_const loc s
| Const_Bin(s) -> mk_int_const loc s
let translate_string_identifier name params raw_params =
match name.c with
| "true" -> mk_true_const (pos name)
| "false" -> mk_false_const (pos name)
| "+" -> begin
match params with
| [p] -> p
| _ -> translate_left_assoc mk_add name params
end
| "-" -> begin
match params with
| [t] -> mk_minus (pos name) t
| _ -> translate_left_assoc mk_sub name params
end
| "*" -> translate_left_assoc mk_mul name params
| "/" -> translate_left_assoc mk_div name params
| "div" -> translate_left_assoc mk_div name params
| "mod" -> begin
match params with
| [t1;t2] -> mk_mod (pos name) t1 t2
| _ -> assert false
end
| "abs" -> begin
match params with
| [x] ->
let cond = mk_pred_ge (pos name) x (mk_int_const (pos name) "0") in
mk_ite (pos name) cond x (mk_minus (pos name) x)
| _ -> assert false
end
| "<" -> translate_chainable_assoc mk_pred_lt name params
| "<=" -> translate_chainable_assoc mk_pred_le name params
| ">" -> translate_chainable_assoc mk_pred_gt name params
| ">=" -> translate_chainable_assoc mk_pred_ge name params
| "=" ->
let f = match raw_params with
| [] -> assert false
| par :: _ ->
if Smtlib_ty.is_bool (Smtlib_ty.shorten par.ty) then mk_iff
else mk_pred_eq
in
translate_chainable_assoc f name params
| "=>" -> translate_right_assoc mk_implies name params
| "and" -> begin
match params with
| [p] -> p
| _ -> translate_left_assoc mk_and name params
end
| "or" -> begin
match params with
| [p] -> p
| _ -> translate_left_assoc mk_or name params
end
| "xor" -> translate_left_assoc mk_xor name params
| "ite" ->
begin
match params with
| [b;e1;e2] -> mk_ite (pos name) b e1 e2
| _ -> assert false
end
| "not" -> begin
match params with
| [t] -> mk_not (pos name) t
| _ -> assert false
end
| "distinct" -> mk_distinct (pos name) params
| "select" -> begin
match params with
| [t;i] -> mk_array_get (pos name) t i
| _ -> assert false
end
| "store" -> begin
match params with
| [t;i;j] -> mk_array_set (pos name) t i j
| _ -> assert false
end
| _ ->
if name.is_quantif then
mk_var (pos name) name.c
else
mk_application (pos name) name.c params
let translate_identifier id params raw_params =
let name, l = Smtlib_typed_env.get_identifier id in
match name.c, l, params with
| _, [], _ -> translate_string_identifier name params raw_params
| "is", [constr], [e] ->
mk_algebraic_test (pos name) e constr
| _ ->
Printer.print_err "[TODO] handle other underscored IDs";
assert false
let translate_qual_identifier qid params raw_params=
match qid.c with
| QualIdentifierId(id) -> translate_identifier id params raw_params, None
| QualIdentifierAs(id,sort) ->
translate_identifier id params raw_params, Some sort
let rec translate_key_term pars acc k =
match k.c with
| Pattern(term_list) ->
let tl = List.map (translate_term pars) term_list in
(tl, true) :: acc
| Named _ ->
Printer.print_wrn
~warning:(Options.get_verbose () || Options.get_debug_warnings ())
"(! :named not yet supported)%!";
acc
and translate_quantif f svl pars t =
match t.c with
| TermExclimationPt(term,key_term_list) ->
let triggers = List.fold_left (fun acc key_term ->
translate_key_term pars acc key_term
) [] key_term_list in
f (pos t) svl triggers [] (translate_term pars term)
| _ -> f (pos t) svl [] [] (translate_term pars t)
and translate_term pars term =
match term.c with
| TermSpecConst(cst) -> translate_constant cst term
| TermQualIdentifier(qid) ->
let q,s = translate_qual_identifier qid [] [] in
begin
match s with
| None -> q
| Some s -> mk_type_cast (pos term) q (translate_sort s)
end
| TermQualIdTerm(qid,term_list) ->
let params = List.map (translate_term pars) term_list in
let q,s = translate_qual_identifier qid params term_list in
begin
match s with
| None -> q
| Some s -> mk_type_cast (pos term) q (translate_sort s)
end
| TermLetTerm(varbinding_list,term) ->
let varbind = List.map (fun (s,term) ->
s.c, (translate_term pars term)
) varbinding_list in
mk_let (pos term) varbind (translate_term pars term)
| TermForAllTerm(sorted_var_list,t) ->
let svl = List.map (fun (v,s) ->
v.c, v.c, translate_sort s
) sorted_var_list in
translate_quantif mk_forall svl pars t
| TermExistsTerm(sorted_var_list,t) ->
let svl = List.map (fun (v,s) ->
v.c, "", translate_sort s
) sorted_var_list in
translate_quantif mk_exists svl pars t
| TermExclimationPt(term,_key_term_list) ->
translate_term pars term
| TermMatch(term,pattern_term_list) ->
let t = translate_term pars term in
let cases = List.map (fun (pat,term) ->
translate_pattern pat,
translate_term pars term
) pattern_term_list
in
mk_match (pos term) t cases
and translate_pattern pat =
let p = pos pat in
match pat.c with
| MatchPattern(s,sl) -> mk_pattern p s.c (List.map (fun s -> s.c) sl)
| MatchUnderscore -> mk_pattern p "_" []
let translate_assert_term (pars,term) =
translate_term pars term
let translate_goal pos (pars,term) =
mk_goal pos "g" (translate_assert_term (pars,term))
let name_of_assert term =
match term.c with
| TermExclimationPt(_, [{ c = Named s; _ }]) -> Some s.c
| _ -> None
let translate_assert =
let cpt = ref 0 in
fun pos (pars,term) ->
incr cpt;
let name =
match name_of_assert term with
| Some s -> s
| None -> Format.sprintf "unamed__assert__%d" !cpt
in
mk_generic_axiom pos name (translate_assert_term (pars,term))
let translate_const_dec (_,sort) =
translate_sort sort
let translate_decl_fun f params ret =
let logic_type = mk_logic_type params (Some ret) in
mk_logic (pos f) Symbols.Other [(f.c,f.c)] logic_type
let translate_fun_dec (_,sl,s) =
List.map translate_sort sl, translate_sort s
let translate_fun_def_aux (symb,pars,svl,sort) =
let pars = List.map (fun par -> par.c) pars in
let params = List.map (fun (p,s) -> pos p, p.c,translate_sort s) svl in
symb, params, translate_sort sort, pars
let translate_fun_def fun_def term =
let symb,params,ret,pars = translate_fun_def_aux fun_def in
let t_expr = translate_term pars term in
if Smtlib_ty.is_bool (Smtlib_ty.shorten term.ty) then
mk_non_ground_predicate_def (pos symb) (symb.c,symb.c) params t_expr
else mk_function_def (pos symb) (symb.c,symb.c) params ret t_expr
let translate_datatype_decl (name, _) (params, cases) =
let params = List.map (fun n -> n.c) params in
let cases =
List.map (fun (constr, d_l) ->
constr.c,
List.map (fun (des, sort) -> des.c, translate_sort sort) d_l
)cases
in
pos name, params, name.c, (Parsed.Algebraic cases)
let translate_datatypes sort_dec datatype_dec =
try
mk_rec_type_decl @@
List.map2 translate_datatype_decl sort_dec datatype_dec
with Invalid_argument _ -> assert false
let translate_push_pop fun_push_pop n pos =
try let n = int_of_string n in
if n < 0 then
must_not_happen pos "negative integer n in push n /pop n command";
fun_push_pop pos n
with _ ->
must_not_happen pos "int of string conversion error in push/pop command"
let not_supported s =
Printer.print_wrn
~warning:(Options.get_verbose () || Options.get_debug_warnings ())
"%S : Not yet supported" s
let requires_dolmen s =
Printer.print_wrn
~warning:(Options.get_verbose () || Options.get_debug_warnings ())
"%S : Requires --frontend dolmen" s
let translate_prop_literal x =
match x.c with
| PropLit sy ->
mk_application (pos x) sy.c []
| PropLitNot sy ->
let ps = pos x in
mk_not ps (mk_application ps sy.c [])
let count_goals = ref 0
let translate_check_sat command l =
let loc = pos command in
incr count_goals;
let gname = "g_" ^ (string_of_int !count_goals) in
let l = List.rev_map (fun e -> translate_prop_literal e) (List.rev l) in
let e =
match l with
| [] -> mk_false_const loc
| [e] -> mk_not loc e
| _ -> mk_not loc (translate_left_assoc mk_and command l)
in
mk_goal loc gname e
let translate_command acc command =
match command.c with
| Cmd_Assert(assert_term) ->
(translate_assert (pos command) assert_term) :: acc
| Cmd_CheckEntailment(assert_term) ->
(translate_goal (pos command) assert_term) :: acc
| Cmd_CheckSat ->
(translate_check_sat command []) :: acc
| Cmd_CheckSatAssum l ->
(translate_check_sat command l) :: acc
| Cmd_DeclareConst(symbol,const_dec) ->
(translate_decl_fun symbol [] (translate_const_dec const_dec)) :: acc
| Cmd_DeclareDataType(symbol,datatype_dec) ->
(mk_rec_type_decl
[(translate_datatype_decl (symbol,0) datatype_dec)]) :: acc
| Cmd_DeclareDataTypes(sort_dec_list,datatype_dec_list) ->
(translate_datatypes sort_dec_list datatype_dec_list) :: acc
| Cmd_DeclareFun(symbol,fun_dec) ->
let params,ret = translate_fun_dec fun_dec in
(translate_decl_fun symbol params ret):: acc
| Cmd_DeclareSort(symbol,n) ->
let n = int_of_string n in
let pars = init n (fun i -> Format.sprintf "'a_%d" i) in
(mk_abstract_type_decl (pos command) pars symbol.c) :: acc
| Cmd_DefineFun(fun_def,term)
| Cmd_DefineFunRec(fun_def,term) ->
(translate_fun_def fun_def term) :: acc
| Cmd_DefineFunsRec(fun_def_list,term_list) ->
let l = List.map2 translate_fun_def fun_def_list term_list in
l @ acc
| Cmd_DefineSort _ -> acc
| Cmd_GetModel -> requires_dolmen "get-model"; acc
| Cmd_Echo _ -> not_supported "echo"; acc
| Cmd_GetAssert -> not_supported "get-assertions"; acc
| Cmd_GetProof -> not_supported "get-proof"; acc
| Cmd_GetUnsatCore -> not_supported "get-unsat-core"; acc
| Cmd_GetValue _ -> not_supported "get-value"; acc
| Cmd_GetAssign -> not_supported "get-assign"; acc
| Cmd_GetOption _ -> not_supported "get-option"; acc
| Cmd_GetInfo _ -> not_supported "get-info"; acc
| Cmd_GetUnsatAssumptions -> not_supported "get-unsat-assumptions"; acc
| Cmd_Reset -> not_supported "reset"; assert false
| Cmd_ResetAssert -> not_supported "reset-asserts"; assert false
| Cmd_SetLogic _ -> not_supported "set-logic"; acc
| Cmd_SetOption _ -> not_supported "set-option"; acc
| Cmd_SetInfo _ -> not_supported "set-info"; acc
| Cmd_Push n -> translate_push_pop mk_push n (pos command) :: acc
| Cmd_Pop n -> translate_push_pop mk_pop n (pos command) :: acc
| Cmd_CheckAllSat _ -> not_supported "check-all-sat"; acc
| Cmd_Maximize _ -> not_supported "maximize"; acc
| Cmd_Minimize _ -> not_supported "minimize"; acc
| Cmd_Exit -> acc
let init () =
if Psmt2Frontend.Options.get_is_int_real () then
let dummy_pos = Lexing.dummy_pos,Lexing.dummy_pos in
let logic_type = mk_logic_type [real_type] (Some int_type) in
let to_int =
mk_logic dummy_pos Symbols.Other [("to_int","to_int")] logic_type in
let logic_type = mk_logic_type [int_type] (Some real_type) in
let to_real =
mk_logic dummy_pos Symbols.Other [("to_real","to_real")] logic_type in
let logic_type = mk_logic_type [real_type] (Some bool_type) in
let is_int =
mk_logic dummy_pos Symbols.Other [("is_int","is_int")] logic_type in
[to_int;to_real;is_int]
else []
let file commands =
Smtlib_typing.typing commands;
if Options.get_type_smt2 () then begin
Printer.print_dbg
"%s" (Smtlib_options.status ());
[]
end
else begin
let l = List.fold_left translate_command [] (List.rev commands) in
(init ()) @ l
end
let lexpr l = translate_term [] l
let trigger (tl,b) = List.map (translate_term []) tl,b
end
let aux aux_fun token lexbuf =
try
Smtlib_options.set_filename (Options.get_file ());
Smtlib_options.set_keep_loc true;
let res = aux_fun token lexbuf in
Options.set_status (Smtlib_options.status ());
Parsing.clear_parser ();
res
with
| Parsing.Parse_error
| Smtlib_parser.Error ->
let loc = (Lexing.lexeme_start_p lexbuf, Lexing.lexeme_end_p lexbuf) in
let lex = Lexing.lexeme lexbuf in
Parsing.clear_parser ();
Smtlib_error.print (Options.Output.get_fmt_err ()) (Options.get_file ())
(Syntax_error (lex)) loc;
Errors.error (Errors.Syntax_error (loc,""))
| Smtlib_error.Error (e , p) ->
Parsing.clear_parser ();
let loc =
match p with
Some loc -> loc
| None -> Lexing.dummy_pos,Lexing.dummy_pos
in
Smtlib_error.print (Options.Output.get_fmt_err ())
(Options.get_file ()) e loc;
Errors.error (Errors.Syntax_error (loc,""))
let file_parser token lexbuf =
Translate.file (Smtlib_parser.commands token lexbuf)
let lexpr_parser token lexbuf =
Translate.lexpr (Smtlib_parser.term token lexbuf)
let trigger_parser token lexbuf =
Translate.trigger (Smtlib_parser.term_list token lexbuf)
module Parser : Parsers.PARSER_INTERFACE = struct
let file = aux file_parser Smtlib_lexer.token
let expr = aux lexpr_parser Smtlib_lexer.token
let trigger = aux trigger_parser Smtlib_lexer.token
end
let register_psmt2 () =
let p = (module Parser : Parsers.PARSER_INTERFACE) in
Parsers.register_parser ~lang:".smt2" p;
Parsers.register_parser ~lang:".psmt2" p;