smtv2.ml 13.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   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
13
14
15
16
17
18
19
20
21

(** SMT v1 printer with some extensions *)

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

22
(** SMTLIB tokens taken from CVC4: src/parser/smt2/Smt2.g *)
23
24
25
26
27
28
29
30
31
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 *)
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
    [(** 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";
56
      "bvugt"; "bvuge"; "bvslt"; "bvsle"; "bvsgt"; "bvsge"; "rotate_left"; "rotate_right";
57

58
59
      "cos"; "sin"; "tan"; "atan"; "pi";

60
61
      (** Other stuff that Why3 seems to need *)
      "DECIMAL"; "NUMERAL"; "par"; "STRING";
62
      "unsat";"sat";
63
64
65
66
      "Bool"; "true"; "false";
      "Array";"const";
      "abs";
      "BitVec"; "extract"; "bv2nat"; "nat2bv"
Andrei Paskevich's avatar
Andrei Paskevich committed
67
      ]
68
69
70
71
72
73
74
75
  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
76
77
  info_syn        : syntax_map;
  info_converters : converter_map;
78
79
}

80
(** type *)
81
82
let rec print_type info fmt ty = match ty.ty_node with
  | Tyvar _ -> unsupported "smt : you must encode the polymorphism"
83
  | Tyapp (ts, l) ->
84
85
86
87
88
     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
89
90
     end

91
92
let print_type info fmt ty = try print_type info fmt ty
  with Unsupported s -> raise (UnsupportedType (ty,s))
93
94
95
96
97
98
99
100
101
102
103
104
105

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 =
106
107
  fprintf fmt "(%a %a)" print_var vs
    (print_type info) vs.vs_ty
108
109
110
111
112
113

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

(** expr *)
let rec print_term info fmt t = match t.t_node with
114
115
  | Tconst c ->
      let number_format = {
116
          Number.long_int_support = true;
117
          Number.extra_leading_zeros_support = false;
118
119
120
121
122
123
124
125
126
127
          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;
128
        } in
129
      Number.print number_format fmt c
130
  | Tvar v -> print_var fmt v
Clément Fumex's avatar
Clément Fumex committed
131
132
133
134
135
136
137
138
139
140
141
142
143
  | 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
144
      | Some s -> syntax_arguments_typed s (print_term info)
145
        (print_type info) t fmt tl
146
147
148
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
          | _ -> fprintf fmt "@[(%a@ %a)@]"
149
              print_ident ls.ls_name (print_list space (print_term info)) tl
150
151
152
        end end
  | Tlet (t1, tb) ->
      let v, t2 = t_open_bound tb in
153
      fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
154
155
156
157
158
        (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
159
(*
160
  | Tcase _ -> unsupportedTerm t
161
162
163
164
165
166
167
168
      "smtv2: you must eliminate match"
*)
  | 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) bl;
     forget_var subject
169
  | Teps _ -> unsupportedTerm t
170
      "smtv2: you must eliminate epsilon"
171
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
172

173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
and print_branches info subject fmt bl =
  match bl with
  | [] -> assert false
  | br::bl ->
     let (p,t) = t_open_branch br in
     let constr,args =
       match p.pat_node with
       | Papp(cs,args) -> cs,args
       | _ -> unsupportedPattern p
                "smtv2: you must compile nested pattern-matching"
     in
     match bl with
     | [] -> print_branch info fmt (args,t)
     | _ ->
        fprintf fmt "@[(ite (is-%a %a) %a %a)@]"
                print_ident constr.ls_name print_var subject
                (print_branch info) (args,t) (print_branches info subject) bl

and print_branch info fmt (vars,t) =
  fprintf fmt "<branch>"

194
195
and print_fmla info fmt f = match f.t_node with
  | Tapp ({ ls_name = id }, []) ->
196
      print_ident fmt id
197
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
198
      | Some s -> syntax_arguments_typed s (print_term info)
199
        (print_type info) f fmt tl
200
201
202
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "%a" print_ident ls.ls_name
          | _ -> fprintf fmt "(%a@ %a)"
203
              print_ident ls.ls_name (print_list space (print_term info)) tl
204
        end end
205
206
207
  | Tquant (q, fq) ->
      let q = match q with Tforall -> "forall" | Texists -> "exists" in
      let vl, tl, f = t_open_quant fq in
208
209
210
      (* TODO trigger dépend des capacités du prover : 2 printers?
      smtwithtriggers/smtstrict *)
      if tl = [] then
211
        fprintf fmt "@[(%s@ (%a)@ %a)@]"
212
213
214
215
          q
          (print_var_list info) vl
          (print_fmla info) f
      else
216
        fprintf fmt "@[(%s@ (%a)@ (! %a %a))@]"
217
218
219
220
221
          q
          (print_var_list info) vl
          (print_fmla info) f
          (print_triggers info) tl;
      List.iter forget_var vl
222
  | Tbinop (Tand, f1, f2) ->
223
      fprintf fmt "@[(and@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
224
  | Tbinop (Tor, f1, f2) ->
225
      fprintf fmt "@[(or@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
226
  | Tbinop (Timplies, f1, f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
227
      fprintf fmt "@[(=>@ %a@ %a)@]"
228
        (print_fmla info) f1 (print_fmla info) f2
229
  | Tbinop (Tiff, f1, f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
230
      fprintf fmt "@[(=@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
231
  | Tnot f ->
232
      fprintf fmt "@[(not@ %a)@]" (print_fmla info) f
233
  | Ttrue ->
234
      fprintf fmt "true"
235
  | Tfalse ->
236
      fprintf fmt "false"
237
  | Tif (f1, f2, f3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
238
      fprintf fmt "@[(ite %a@ %a@ %a)@]"
239
        (print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
240
  | Tlet (t1, tb) ->
241
      let v, f2 = t_open_bound tb in
242
243
244
      fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
        (print_term info) t1 (print_fmla info) f2;
      forget_var v
245
  | Tcase _ -> unsupportedTerm f
246
      "smtv2 : you must eliminate match"
247
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
248

249
250
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
251

Andrei Paskevich's avatar
Andrei Paskevich committed
252
and print_trigger info fmt e = fprintf fmt "%a" (print_expr info) e
253
254
255
256
257
258
259

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

260
261
let print_type_decl info fmt ts =
  if ts.ts_def <> None then () else
262
  if Mid.mem ts.ts_name info.info_syn then () else
263
264
  fprintf fmt "(declare-sort %a %i)@\n@\n"
    print_ident ts.ts_name (List.length ts.ts_args)
265

266
267
268
269
270
271
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
272

273
let print_logic_decl info fmt (ls,def) =
274
  if Mid.mem ls.ls_name info.info_syn then () else
275
  let vsl,expr = Decl.open_ls_defn def in
276
  fprintf fmt "@[<hov 2>(define-fun %a (%a) %a %a)@]@\n@\n"
277
278
279
280
281
    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
282
283
284
285
286
287
288

let print_prop_decl info fmt k pr f = match k with
  | Paxiom ->
      fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a)@]@\n@\n"
        pr.pr_name.id_string (* FIXME? collisions *)
        (print_fmla info) f
  | Pgoal ->
289
290
      fprintf fmt "@[(assert@\n";
      fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
291
      (match pr.pr_name.id_loc with
292
293
294
        | None -> ()
        | Some loc -> fprintf fmt " @[;; %a@]@\n"
            Loc.gen_report_position loc);
295
296
297
298
      fprintf fmt "  @[(not@ %a))@]@\n" (print_fmla info) f;
      fprintf fmt "@[(check-sat)@]@\n"
  | Plemma| Pskip -> assert false

299
300
let print_constructor_decl info fmt (ls,args) =
  match args with
301
  | [] -> fprintf fmt "(%a)" print_ident ls.ls_name
302
  | _ ->
303
304
305
306
307
308
309
310
311
312
313
314
     fprintf fmt "@[(%a@ " print_ident ls.ls_name;
     let _ = 
       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 ")@]"
315
316
317
318
319
320

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

321
let print_decl info fmt d = match d.d_node with
322
323
  | Dtype ts ->
      print_type_decl info fmt ts
324
325
326
327
328
  | Ddata dl ->
    (*unsupportedDecl d
      "smtv2 : algebraic type are not supported" *)
    fprintf fmt "@[(declare-datatypes ()@ (%a))@]@\n"
      (print_list space (print_data_decl info)) dl
329
330
  | Dparam ls ->
      print_param_decl info fmt ls
331
332
333
  | Dlogic dl ->
      print_list nothing (print_logic_decl info) fmt dl
  | Dind _ -> unsupportedDecl d
334
      "smtv2 : inductive definition are not supported"
335
336
337
  | Dprop (k,pr,f) ->
      if Mid.mem pr.pr_name info.info_syn then () else
      print_prop_decl info fmt k pr f
338

339
let print_decls =
Clément Fumex's avatar
Clément Fumex committed
340
341
  let print_decl (sm, cm) fmt d =
    try print_decl {info_syn = sm; info_converters = cm} fmt d; (sm, cm), []
342
343
344
    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
345
346
347
  Discriminate.on_syntax_map (fun sm ->
  Printer.on_converter_map (fun cm ->
      Trans.fold print_decl ((sm, cm),[])))
348

349
let print_task args ?old:_ fmt task =
350
  (* In trans-based p-printing [forget_all] is a no-no *)
351
  (* forget_all ident_printer; *)
352
353
  print_prelude fmt args.prelude;
  print_th_prelude task fmt args.th_prelude;
354
355
356
357
358
359
360
361
  let rec print = function
    | x :: r -> print r; Pp.string fmt x
    | [] -> () in
  print (snd (Trans.apply print_decls task));
  pp_print_flush fmt ()

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