smtv1.ml 9.57 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   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.                           *)
(*                                                                  *)
(********************************************************************)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
11

Francois Bobot's avatar
Francois Bobot committed
12
13
(** SMT v1 printer with some extensions *)

Francois Bobot's avatar
Francois Bobot committed
14
15
16
17
18
19
open Format
open Pp
open Ident
open Ty
open Term
open Decl
20
open Printer
Francois Bobot's avatar
Francois Bobot committed
21

22
let ident_printer =
23
  let bls = ["and";"benchmark";"distinct";"exists";"false";"flet";"forall";
Francois Bobot's avatar
Francois Bobot committed
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
     "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"] 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)

let forget_var v = forget_id ident_printer v.vs_name

let print_var fmt {vs_name = id} =
  let sanitize n = "?" ^ n in
  let n = id_unique ident_printer ~sanitizer:sanitize id in
  fprintf fmt "%s" n

43
type info = {
44
45
  info_syn     : syntax_map;
  complex_type : ty Mty.t ref;
46
  urg_output   : string list ref;
47
}
Francois Bobot's avatar
Francois Bobot committed
48

49
50
51
52
let complex_type = Wty.memoize 3 (fun ty ->
  let s = Pp.string_of_wnl Pretty.print_ty ty in
  create_tysymbol (id_fresh s) [] None)

53
54
let rec print_type info fmt ty = match ty.ty_node with
  | Tyvar _ -> unsupported "smtv1: you must encode the polymorphism"
55
  | Tyapp (ts, l) ->
56
      begin match query_syntax info.info_syn ts.ts_name, l with
57
      | Some s, _ -> syntax_arguments s (print_type info) fmt l
58
59
60
61
62
63
      | None, [] -> fprintf fmt "%a" print_ident ts.ts_name
      | None, _ ->
          begin match Mty.find_opt ty !(info.complex_type) with
          | Some ty -> print_type info fmt ty
          | None ->
              let ts = complex_type ty in let cty = ty_app ts [] in
64
              let us = Pp.sprintf
65
66
67
68
69
                ":extrasorts (%a)@\n@\n" print_ident ts.ts_name in
              info.complex_type := Mty.add ty cty !(info.complex_type);
              info.urg_output := us :: !(info.urg_output);
              print_type info fmt cty
          end
70
71
      end

72
let print_type info fmt ty = try print_type info fmt ty
73
74
  with Unsupported s -> raise (UnsupportedType (ty,s))

75
let rec print_term info fmt t = match t.t_node with
76
77
  | Tconst c ->
      let number_format = {
78
          Number.long_int_support = true;
79
          Number.extra_leading_zeros_support = false;
80
81
82
83
84
85
86
87
88
89
          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;
90
        } in
91
      Number.print number_format fmt c
Francois Bobot's avatar
Francois Bobot committed
92
  | Tvar v -> print_var fmt v
93
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
94
      | Some s -> syntax_arguments s (print_term info) fmt tl
95
96
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
97
          | _ -> fprintf fmt "@[(%a@ %a)@]"
98
              print_ident ls.ls_name (print_list space (print_term info)) tl
99
        end end
Francois Bobot's avatar
Francois Bobot committed
100
101
  | Tlet (t1, tb) ->
      let v, t2 = t_open_bound tb in
102
      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
103
        (print_term info) t1 (print_term info) t2;
Francois Bobot's avatar
Francois Bobot committed
104
      forget_var v
105
  | Tif (f1,t1,t2) ->
106
      fprintf fmt "@[(ite %a@ %a@ %a)@]"
107
        (print_fmla info) f1 (print_term info) t1 (print_term info) t2
108
  | Tcase _ -> unsupportedTerm t
109
      "smtv1 : you must eliminate match"
110
  | Teps _ -> unsupportedTerm t
111
      "smtv1 : you must eliminate epsilon"
112
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
113

114
115
and print_fmla info fmt f = match f.t_node with
  | Tapp ({ ls_name = id }, []) ->
Francois Bobot's avatar
Francois Bobot committed
116
      print_ident fmt id
117
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
118
      | Some s -> syntax_arguments s (print_term info) fmt tl
119
120
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "%a" print_ident ls.ls_name
121
          | _ -> fprintf fmt "(%a@ %a)"
122
              print_ident ls.ls_name (print_list space (print_term info)) tl
123
        end end
124
125
126
  | Tquant (q, fq) ->
      let q = match q with Tforall -> "forall" | Texists -> "exists" in
      let vl, _tl, f = t_open_quant fq in
127
128
      (* TODO trigger dépend des capacités du prover : 2 printers?
      smtwithtriggers/smtstrict *)
Francois Bobot's avatar
Francois Bobot committed
129
      let rec forall fmt = function
130
        | [] -> print_fmla info fmt f
131
        | v::l ->
132
            fprintf fmt "@[(%s (%a %a)@ %a)@]" q print_var v
133
              (print_type info) v.vs_ty forall l
Francois Bobot's avatar
Francois Bobot committed
134
135
136
      in
      forall fmt vl;
      List.iter forget_var vl
137
  | Tbinop (Tand, f1, f2) ->
138
      fprintf fmt "@[(and@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
139
  | Tbinop (Tor, f1, f2) ->
140
      fprintf fmt "@[(or@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
141
  | Tbinop (Timplies, f1, f2) ->
142
      fprintf fmt "@[(implies@ %a@ %a)@]"
143
        (print_fmla info) f1 (print_fmla info) f2
144
  | Tbinop (Tiff, f1, f2) ->
145
      fprintf fmt "@[(iff@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
146
  | Tnot f ->
147
      fprintf fmt "@[(not@ %a)@]" (print_fmla info) f
148
  | Ttrue ->
Francois Bobot's avatar
Francois Bobot committed
149
      fprintf fmt "true"
150
  | Tfalse ->
Francois Bobot's avatar
Francois Bobot committed
151
      fprintf fmt "false"
152
  | Tif (f1, f2, f3) ->
153
      fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
154
        (print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
155
  | Tlet (t1, tb) ->
156
      let v, f2 = t_open_bound tb in
157
      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
158
        (print_term info) t1 (print_fmla info) f2;
159
      forget_var v
160
  | Tcase _ -> unsupportedTerm f
161
      "smtv1 : you must eliminate match"
162
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
163

164
(*
MARCHE Claude's avatar
MARCHE Claude committed
165
and _print_expr info fmt =
166
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
Francois Bobot's avatar
Francois Bobot committed
167

MARCHE Claude's avatar
MARCHE Claude committed
168
and _print_triggers info fmt tl = print_list comma (_print_expr info) fmt tl
Francois Bobot's avatar
Francois Bobot committed
169

170
let _print_logic_binder info fmt v =
171
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
172
*)
Francois Bobot's avatar
Francois Bobot committed
173

174
let print_type_decl info fmt ts =
175
176
177
  if ts.ts_args = [] && ts.ts_def = None then
  if not (Mid.mem ts.ts_name info.info_syn) then
  fprintf fmt ":extrasorts (%a)@\n@\n" print_ident ts.ts_name
178

179
let print_param_decl info fmt ls = match ls.ls_value with
180
  | None ->
181
      fprintf fmt "@[<hov 2>:extrapreds ((%a %a))@]@\n@\n"
182
183
184
        print_ident ls.ls_name
        (print_list space (print_type info)) ls.ls_args
  | Some value ->
185
      fprintf fmt "@[<hov 2>:extrafuns ((%a %a %a))@]@\n@\n"
186
187
188
189
190
        print_ident ls.ls_name
        (print_list space (print_type info)) ls.ls_args
        (print_type info) value

let print_param_decl info fmt ls =
191
192
  if not (Mid.mem ls.ls_name info.info_syn) then
  print_param_decl info fmt ls
193

194
let print_decl info fmt d = match d.d_node with
195
196
  | Dtype ts ->
      print_type_decl info fmt ts
197
198
  | Ddata _ -> unsupportedDecl d
      "smtv1 : algebraic types are not supported"
199
200
  | Dparam ls ->
      print_param_decl info fmt ls
201
202
  | Dlogic _ -> unsupportedDecl d
      "smtv1 : predicate and function definitions are not supported"
203
  | Dind _ -> unsupportedDecl d
204
205
      "smtv1 : inductive definitions are not supported"
  | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
206
  | Dprop (Paxiom, pr, f) ->
207
208
      fprintf fmt "@[<hov 2>;; %s@\n:assumption@ %a@]@\n@\n"
        pr.pr_name.id_string (print_fmla info) f
Francois Bobot's avatar
Francois Bobot committed
209
210
211
  | Dprop (Pgoal, pr, f) ->
      fprintf fmt "@[:formula@\n";
      fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
212
      (match pr.pr_name.id_loc with
213
214
215
        | Some loc -> fprintf fmt " @[;; %a@]@\n" Loc.gen_report_position loc
        | None -> ());
      fprintf fmt "  @[(not@ %a)@]@\n" (print_fmla info) f
216
  | Dprop ((Plemma|Pskip), _, _) -> assert false
217

218
219
let print_decls =
  let print_decl (sm,ct) fmt d =
220
221
    let info = {info_syn = sm; complex_type = ref ct; urg_output = ref []} in
    try print_decl info fmt d; (sm, !(info.complex_type)), !(info.urg_output)
222
223
224
225
226
227
    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
  Discriminate.on_syntax_map (fun sm ->
    Trans.fold print_decl ((sm,Mty.empty),[]))

228
let print_task args ?old:_ fmt task =
229
230
231
  (* In trans-based p-printing [forget_all] is a no-no *)
  (* forget_all ident_printer; *)
  fprintf fmt "(benchmark why3@\n";
Francois Bobot's avatar
Francois Bobot committed
232
  fprintf fmt "  :status unknown@\n";
233
234
  print_prelude fmt args.prelude;
  print_th_prelude task fmt args.th_prelude;
235
236
237
238
239
240
241
  let rec print = function
    | x :: r -> print r; Pp.string fmt x
    | [] -> () in
  print (snd (Trans.apply print_decls task));
  fprintf fmt ")@."

let () = register_printer "smtv1" print_task
Andrei Paskevich's avatar
Andrei Paskevich committed
242
  ~desc:"Printer@ for@ the@ SMTlib@ version@ 1@ format."