smtv2.ml 15.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
9
10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

12
(** SMT v2 printer with some extensions *)
13
14
15
16
17
18
19
20
21

open Format
open Pp
open Ident
open Ty
open Term
open Decl
open Printer

22
23
24
25
let debug = Debug.register_info_flag "smtv2_printer"
  ~desc:"Print@ debugging@ messages@ about@ printing@ \
         the@ input@ of@ smtv2."

26
(** SMTLIB tokens taken from CVC4: src/parser/smt2/Smt2.g *)
27
28
29
30
31
32
33
34
35
let ident_printer =
  let bls = (*["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
     "if then else";"iff";"implies";"ite";"let";"logic";"not";"or";
     "sat";"theory";"true";"unknown";"unsat";"xor";
     "assumption";"axioms";"defintion";"extensions";"formula";
     "funs";"extrafuns";"extrasorts";"extrapreds";"language";
     "notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
     "Array";"U";"select";"store"]*)
    (** smtlib2 V2 p71 *)
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
    [(** Base SMT-LIB tokens *)
      "assert"; "check-sat"; "declare-fun"; "declare-sort"; "define-fun";
      "define-sort"; "get-value"; "get-assignment"; "get-assertions";
      "get-proof"; "get-unsat-core"; "exit"; "ite"; "let"; "!"; "_";
      "set-logic"; "set-info"; "get-info"; "set-option"; "get-option";
      "push"; "pop"; "as";

      (** extended commands *)
      "declare-datatypes"; "get-model"; "echo"; "assert-rewrite";
      "assert-reduction"; "assert-propagation"; "declare-sorts";
      "declare-funs"; "declare-preds"; "define"; "declare-const";
      "simplify";

      (** attributes *)

      (** operators, including theory symbols *)
      "and"; "distinct"; "exists"; "forall"; "is_int"; "not"; "or"; "select";
      "store"; "to_int"; "to_real"; "xor";

      "div"; "mod";

      "concat"; "bvnot"; "bvand"; "bvor"; "bvneg"; "bvadd"; "bvmul"; "bvudiv";
      "bvurem"; "bvshl"; "bvlshr"; "bvult"; "bvnand"; "bvnor"; "bvxor";
      "bvcomp"; "bvsub"; "bvsdiv"; "bvsrem"; "bvsmod"; "bvashr"; "bvule";
60
      "bvugt"; "bvuge"; "bvslt"; "bvsle"; "bvsgt"; "bvsge"; "rotate_left"; "rotate_right";
61

62
63
      "cos"; "sin"; "tan"; "atan"; "pi";

64
65
      (** Other stuff that Why3 seems to need *)
      "DECIMAL"; "NUMERAL"; "par"; "STRING";
66
      "unsat";"sat";
67
68
69
      "Bool"; "true"; "false";
      "Array";"const";
      "abs";
Clément Fumex's avatar
Clément Fumex committed
70
71
72
      "BitVec"; "extract"; "bv2nat"; "nat2bv";

      (** From Z3 *)
73
      "map"; "bv"; "subset"; "union"
Andrei Paskevich's avatar
Andrei Paskevich committed
74
      ]
75
76
77
78
79
80
81
82
  in
  let san = sanitizer char_to_alpha char_to_alnumus in
  create_ident_printer bls ~sanitizer:san

let print_ident fmt id =
  fprintf fmt "%s" (id_unique ident_printer id)

type info = {
Clément Fumex's avatar
Clément Fumex committed
83
84
  info_syn        : syntax_map;
  info_converters : converter_map;
85
  mutable info_model : term list;
86
87
}

88
89
90
91
92
93
94
95
96
let debug_print_term message t =
  let form = Debug.get_debug_formatter () in
  begin
    Debug.dprintf debug message;
    if Debug.test_flag debug then 
      Pretty.print_term form t;
    Debug.dprintf debug "@.";
  end

97
(** type *)
98
99
let rec print_type info fmt ty = match ty.ty_node with
  | Tyvar _ -> unsupported "smt : you must encode the polymorphism"
100
  | Tyapp (ts, l) ->
101
102
103
104
105
     begin match query_syntax info.info_syn ts.ts_name, l with
      | Some s, _ -> syntax_arguments s (print_type info) fmt l
      | None, [] -> fprintf fmt "%a" print_ident ts.ts_name
      | None, _ -> fprintf fmt "(%a %a)" print_ident ts.ts_name
          (print_list space (print_type info)) l
106
107
     end

108
109
let print_type info fmt ty = try print_type info fmt ty
  with Unsupported s -> raise (UnsupportedType (ty,s))
110
111
112
113
114
115
116
117
118
119
120
121
122

let print_type_value info fmt = function
  | None -> fprintf fmt "Bool"
  | Some ty -> print_type info fmt ty

(** var *)
let forget_var v = forget_id ident_printer v.vs_name

let print_var fmt {vs_name = id} =
  let n = id_unique ident_printer id in
  fprintf fmt "%s" n

let print_typed_var info fmt vs =
123
124
  fprintf fmt "(%a %a)" print_var vs
    (print_type info) vs.vs_ty
125
126
127
128

let print_var_list info fmt vsl =
  print_list space (print_typed_var info) fmt vsl

129
130
let model_label = Ident.create_label "model"

131
132
133
134
135
let collect_model_ls info ls =
  if ls.ls_args = [] &&
    Slab.mem model_label ls.ls_name.id_label then 
    begin
      let t = t_app ls [] ls.ls_value in
136
      info.info_model <- (t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) :: info.info_model
137
138
    end

139
(** expr *)
140
let rec print_term info fmt t = 
141
142
  debug_print_term "Printing term: " t; 

143
144
  if Slab.mem model_label t.t_label then
    info.info_model <- (t) :: info.info_model;
145

146
  match t.t_node with
147
148
  | Tconst c ->
      let number_format = {
149
          Number.long_int_support = true;
150
          Number.extra_leading_zeros_support = false;
151
152
153
154
155
156
157
158
159
160
          Number.dec_int_support = Number.Number_default;
          Number.hex_int_support = Number.Number_unsupported;
          Number.oct_int_support = Number.Number_unsupported;
          Number.bin_int_support = Number.Number_unsupported;
          Number.def_int_support = Number.Number_unsupported;
          Number.dec_real_support = Number.Number_unsupported;
          Number.hex_real_support = Number.Number_unsupported;
          Number.frac_real_support = Number.Number_custom
            (Number.PrintFracReal ("%s.0", "(* %s.0 %s.0)", "(/ %s.0 %s.0)"));
          Number.def_real_support = Number.Number_unsupported;
161
        } in
162
      Number.print number_format fmt c
163
  | Tvar v -> print_var fmt v
Clément Fumex's avatar
Clément Fumex committed
164
165
166
167
168
169
170
171
172
173
174
175
176
  | Tapp (ls, tl) ->
    (* let's check if a converter applies *)
    begin try
      match tl with
      | [ { t_node = Tconst _} ] ->
        begin match query_converter info.info_converters ls with
        | None -> raise Exit
        | Some s -> syntax_arguments s (print_term info) fmt tl
        end
      | _ -> raise Exit
    with Exit ->
    (* non converter applies, then ... *)
    match query_syntax info.info_syn ls.ls_name with
177
      | Some s -> syntax_arguments_typed s (print_term info)
178
        (print_type info) t fmt tl
179
180
181
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
          | _ -> fprintf fmt "@[(%a@ %a)@]"
182
              print_ident ls.ls_name (print_list space (print_term info)) tl
183
184
185
        end end
  | Tlet (t1, tb) ->
      let v, t2 = t_open_bound tb in
186
      fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
187
188
189
190
191
        (print_term info) t1 (print_term info) t2;
      forget_var v
  | Tif (f1,t1,t2) ->
      fprintf fmt "@[(ite %a@ %a@ %a)@]"
        (print_fmla info) f1 (print_term info) t1 (print_term info) t2
192
193
194
195
196
197
198
199
  | Tcase({t_node = Tvar v}, bl) ->
      print_branches info v print_term fmt bl
  | Tcase(t, bl) ->
      let subject = create_vsymbol (id_fresh "subject") (t_type t) in
      fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
        print_var subject (print_term info) t
        (print_branches info subject print_term) bl;
      forget_var subject
200
  | Teps _ -> unsupportedTerm t
201
      "smtv2: you must eliminate epsilon"
202
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
203

204
and print_fmla info fmt f = 
205
  debug_print_term "Printing formula: " f;  
206
207
  if Slab.mem model_label f.t_label then
    info.info_model <- (f) :: info.info_model;
208
  
209
  match f.t_node with
210
  | Tapp ({ ls_name = id }, []) ->
211
      print_ident fmt id
212
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
213
      | Some s -> syntax_arguments_typed s (print_term info)
214
        (print_type info) f fmt tl
215
216
217
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "%a" print_ident ls.ls_name
          | _ -> fprintf fmt "(%a@ %a)"
218
              print_ident ls.ls_name (print_list space (print_term info)) tl
219
        end end
220
221
222
  | Tquant (q, fq) ->
      let q = match q with Tforall -> "forall" | Texists -> "exists" in
      let vl, tl, f = t_open_quant fq in
223
224
225
      (* TODO trigger dépend des capacités du prover : 2 printers?
      smtwithtriggers/smtstrict *)
      if tl = [] then
226
        fprintf fmt "@[(%s@ (%a)@ %a)@]"
227
228
229
230
          q
          (print_var_list info) vl
          (print_fmla info) f
      else
231
        fprintf fmt "@[(%s@ (%a)@ (! %a %a))@]"
232
233
234
235
236
          q
          (print_var_list info) vl
          (print_fmla info) f
          (print_triggers info) tl;
      List.iter forget_var vl
237
  | Tbinop (Tand, f1, f2) ->
238
      fprintf fmt "@[(and@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
239
  | Tbinop (Tor, f1, f2) ->
240
      fprintf fmt "@[(or@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
241
  | Tbinop (Timplies, f1, f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
242
      fprintf fmt "@[(=>@ %a@ %a)@]"
243
        (print_fmla info) f1 (print_fmla info) f2
244
  | Tbinop (Tiff, f1, f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
245
      fprintf fmt "@[(=@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
246
  | Tnot f ->
247
      fprintf fmt "@[(not@ %a)@]" (print_fmla info) f
248
  | Ttrue ->
249
      fprintf fmt "true"
250
  | Tfalse ->
251
      fprintf fmt "false"
252
  | Tif (f1, f2, f3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
253
      fprintf fmt "@[(ite %a@ %a@ %a)@]"
254
        (print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
255
  | Tlet (t1, tb) ->
256
      let v, f2 = t_open_bound tb in
257
258
259
      fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
        (print_term info) t1 (print_fmla info) f2;
      forget_var v
260
261
262
263
264
265
266
267
  | Tcase({t_node = Tvar v}, bl) ->
      print_branches info v print_fmla fmt bl
  | Tcase(t, bl) ->
      let subject = create_vsymbol (id_fresh "subject") (t_type t) in
      fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
        print_var subject (print_term info) t
        (print_branches info subject print_fmla) bl;
      forget_var subject
268
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
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
and print_branches info subject pr fmt bl = match bl with
  | [] -> assert false
  | br::bl ->
      let (p,t) = t_open_branch br in
      let error () = unsupportedPattern p
        "smtv2: you must compile nested pattern matching" in
      match p.pat_node with
      | Pwild -> pr info fmt t
      | Papp (cs,args) ->
          let args = List.map (function
            | {pat_node = Pvar v} -> v | _ -> error ()) args in
          if bl = [] then print_branch info subject pr fmt (cs,args,t)
          else fprintf fmt "@[(ite (is-%a %a) %a %a)@]"
            print_ident cs.ls_name print_var subject
            (print_branch info subject pr) (cs,args,t)
            (print_branches info subject pr) bl
      | _ -> error ()

and print_branch info subject pr fmt (cs,vars,t) =
  if vars = [] then pr info fmt t else
  let tvs = t_freevars Mvs.empty t in
  if List.for_all (fun v -> not (Mvs.mem v tvs)) vars then pr info fmt t else
  let i = ref 0 in
  let pr_proj fmt v = incr i;
    if Mvs.mem v tvs then fprintf fmt "(%a (%a_proj_%d %a))"
      print_var v print_ident cs.ls_name !i print_var subject in
  fprintf fmt "@[(let (%a) %a)@]" (print_list space pr_proj) vars (pr info) t

298
299
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
300

Andrei Paskevich's avatar
Andrei Paskevich committed
301
and print_trigger info fmt e = fprintf fmt "%a" (print_expr info) e
302
303
304
305
306
307
308

and print_triggers info fmt = function
  | [] -> ()
  | a::l -> fprintf fmt ":pattern (%a) %a"
    (print_list space (print_trigger info)) a
    (print_triggers info) l

309
310
let print_type_decl info fmt ts =
  if ts.ts_def <> None then () else
311
  if Mid.mem ts.ts_name info.info_syn then () else
312
313
  fprintf fmt "(declare-sort %a %i)@\n@\n"
    print_ident ts.ts_name (List.length ts.ts_args)
314

315
316
317
318
319
320
let print_param_decl info fmt ls =
  if Mid.mem ls.ls_name info.info_syn then () else
  fprintf fmt "@[<hov 2>(declare-fun %a (%a) %a)@]@\n@\n"
    print_ident ls.ls_name
    (print_list space (print_type info)) ls.ls_args
    (print_type_value info) ls.ls_value
321

322
let print_logic_decl info fmt (ls,def) =
323
  if Mid.mem ls.ls_name info.info_syn then () else
324
  collect_model_ls info ls;
325
  let vsl,expr = Decl.open_ls_defn def in
326
  fprintf fmt "@[<hov 2>(define-fun %a (%a) %a %a)@]@\n@\n"
327
328
329
330
331
    print_ident ls.ls_name
    (print_var_list info) vsl
    (print_type_value info) ls.ls_value
    (print_expr info) expr;
  List.iter forget_var vsl
332

333
let print_prop_decl args info fmt k pr f = match k with
334
335
336
337
338
  | Paxiom ->
      fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a)@]@\n@\n"
        pr.pr_name.id_string (* FIXME? collisions *)
        (print_fmla info) f
  | Pgoal ->
339
340
      fprintf fmt "@[(assert@\n";
      fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
341
      (match pr.pr_name.id_loc with
342
343
344
        | None -> ()
        | Some loc -> fprintf fmt " @[;; %a@]@\n"
            Loc.gen_report_position loc);
345
      fprintf fmt "  @[(not@ %a))@]@\n" (print_fmla info) f;
346
      fprintf fmt "@[(check-sat)@]@\n";
347
348
349
350
351
352
353
354
      if info.info_model != [] then 
	begin
	  let model_list = info.info_model in
	  (*
          fprintf fmt "@[(get-value (%a))@]@\n"
            (Pp.print_list Pp.space (print_fmla info)) model_list;*)
	  fprintf fmt "@[(get-value (";
	  List.iter (fun f -> 
355
	    fprintf str_formatter "%a" (print_fmla info) f;
356
          let s = flush_str_formatter () in
357
          fprintf fmt "%s" s;
358
359
          ) model_list;
	  fprintf fmt "))@]@\n";
360
361
362
363
	end;
      args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
			       queried_terms = info.info_model; }
	  
364
365
  | Plemma| Pskip -> assert false

366

367
368
let print_constructor_decl info fmt (ls,args) =
  match args with
369
  | [] -> fprintf fmt "(%a)" print_ident ls.ls_name
370
  | _ ->
371
     fprintf fmt "@[(%a@ " print_ident ls.ls_name;
372
     let _ =
373
374
375
376
377
378
379
380
381
382
       List.fold_left2
         (fun i ty pr ->
          begin match pr with
                | Some pr -> fprintf fmt "(%a" print_ident pr.ls_name
                | None -> fprintf fmt "(%a_proj_%d" print_ident ls.ls_name i
          end;
          fprintf fmt " %a)" (print_type info) ty;
          succ i) 1 ls.ls_args args
     in
     fprintf fmt ")@]"
383
384
385
386
387
388

let print_data_decl info fmt (ts,cl) =
  fprintf fmt "@[(%a@ %a)@]"
    print_ident ts.ts_name
    (print_list space (print_constructor_decl info)) cl

389
let print_decl args info fmt d = match d.d_node with
390
391
  | Dtype ts ->
      print_type_decl info fmt ts
392
393
394
395
396
  | Ddata dl ->
    (*unsupportedDecl d
      "smtv2 : algebraic type are not supported" *)
    fprintf fmt "@[(declare-datatypes ()@ (%a))@]@\n"
      (print_list space (print_data_decl info)) dl
397
  | Dparam ls ->
398
      collect_model_ls info ls;
399
      print_param_decl info fmt ls
400
401
402
  | Dlogic dl ->
      print_list nothing (print_logic_decl info) fmt dl
  | Dind _ -> unsupportedDecl d
403
      "smtv2 : inductive definition are not supported"
404
405
  | Dprop (k,pr,f) ->
      if Mid.mem pr.pr_name info.info_syn then () else
406
      print_prop_decl args info fmt k pr f
407

408
let print_decls args =
409
410
  let print_decl (sm, cm, model) fmt d =
    try let info = {info_syn = sm; info_converters = cm; info_model = model} in
411
        print_decl args info fmt d; (sm, cm, info.info_model), []
412
413
414
    with Unsupported s -> raise (UnsupportedDecl (d,s)) in
  let print_decl = Printer.sprint_decl print_decl in
  let print_decl task acc = print_decl task.Task.task_decl acc in
Clément Fumex's avatar
Clément Fumex committed
415
416
  Discriminate.on_syntax_map (fun sm ->
  Printer.on_converter_map (fun cm ->
417
      Trans.fold print_decl ((sm, cm, []),[])))
418

419
let print_task args ?old:_ fmt task =
420
  (* In trans-based p-printing [forget_all] is a no-no *)
421
  (* forget_all ident_printer; *)
422
423
  print_prelude fmt args.prelude;
  print_th_prelude task fmt args.th_prelude;
424
425
426
  let rec print = function
    | x :: r -> print r; Pp.string fmt x
    | [] -> () in
427
  print (snd (Trans.apply (print_decls args) task));
428
429
430
431
  pp_print_flush fmt ()

let () = register_printer "smtv2" print_task
  ~desc:"Printer@ for@ the@ SMTlib@ version@ 2@ format."