smtv2.ml 13.2 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
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
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(** SMT v1 printer with some extensions *)

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

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 *)
    [(** General: *)
      "!";"_"; "as"; "DECIMAL"; "exists"; "forall"; "let"; "NUMERAL";
      "par"; "STRING";
       (**Command names:*)
      "assert";"check-sat"; "declare-sort";"declare-fun";"define-sort";
      "define-fun";"exit";"get-assertions";"get-assignment"; "get-info";
      "get-option"; "get-proof"; "get-unsat-core"; "get-value"; "pop"; "push";
      "set-logic"; "set-info"; "set-option";
       (** for security *)
Andrei Paskevich's avatar
Andrei Paskevich committed
51
52
53
      "Bool";"unsat";"sat";"true";"false";"select";"store";
       (** arrays -- this really belongs to the driver! (esp. const) *)
      "Array";"select";"store";"const";
54
55
       (** div and mod are builtin *)
      "div";"mod";
Andrei Paskevich's avatar
Andrei Paskevich committed
56
      ]
57
58
59
60
61
62
63
64
65
  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 *)
type info = {
66
  info_syn : syntax_map;
67
(*  complex_type : ty Hty.t; *)
68
69
70
71
72
73
74
75
}

let rec print_type info fmt ty = match ty.ty_node with
  | Tyvar _ -> unsupported "smt : you must encode the polymorphism"
  | Tyapp (ts, []) -> begin match query_syntax info.info_syn ts.ts_name with
      | Some s -> syntax_arguments s (print_type info) fmt []
      | None -> fprintf fmt "%a" print_ident ts.ts_name
  end
76
77
78
79
80
81
82
  | Tyapp (ts, l) ->
     begin match query_syntax info.info_syn ts.ts_name with
      | Some s -> syntax_arguments s (print_type info) fmt l
      | None -> fprintf fmt "(%a %a)" print_ident ts.ts_name
        (print_list space (print_type info)) l
     end

83
(*
84
let iter_complex_type info fmt () ty =
85
86
87
88
89
    match ty.ty_node with
      | Tyapp (_,_::_) when not (Hty.mem info.complex_type ty) ->
        let id = id_fresh (Pp.string_of_wnl Pretty.print_ty ty) in
        let ts = create_tysymbol id [] None in
        let cty = ty_app ts [] in
Andrei Paskevich's avatar
Andrei Paskevich committed
90
        fprintf fmt "(define-sorts ((%a %a)))@\n"
91
92
93
94
          print_ident ts.ts_name
          (print_type info) ty;
        Hty.add info.complex_type ty cty
      | _ -> ()
95
96

let find_complex_type info fmt f =
97
  t_ty_fold (iter_complex_type info fmt) () f
98

99
100
101
102
103
let print_type info fmt ty =
  print_type info fmt
    (try
       Hty.find info.complex_type ty
     with Not_found -> ty)
104
*)
105
106
107
108
109
110

(* and print_tyapp info fmt = function *)
(*   | [] -> () *)
(*   | [ty] -> fprintf fmt "%a " (print_type info) ty *)
(*   | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl *)

111
112
let print_type info fmt =
  catch_unsupportedType (print_type info fmt)
113
114
115
116
117
118
119
120
121
122
123
124
125

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 =
126
127
  fprintf fmt "(%a %a)" print_var vs
    (print_type info) vs.vs_ty
128
129
130
131
132
133

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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
  | Tconst c ->
      let number_format = {
          Print_number.long_int_support = true;
          Print_number.dec_int_support = Print_number.Number_default;
          Print_number.hex_int_support = Print_number.Number_unsupported;
          Print_number.oct_int_support = Print_number.Number_unsupported;
          Print_number.bin_int_support = Print_number.Number_unsupported;
          Print_number.def_int_support = Print_number.Number_unsupported;
          Print_number.dec_real_support = Print_number.Number_unsupported;
          Print_number.hex_real_support = Print_number.Number_unsupported;
          Print_number.frac_real_support = Print_number.Number_custom
            (Print_number.PrintFracReal ("%s.0", "(* %s.0 %s.0)", "(/ %s.0 %s.0)"));
          Print_number.def_real_support = Print_number.Number_unsupported;
        } in
      Print_number.print number_format fmt c
149
150
  | Tvar v -> print_var fmt v
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
151
152
      | Some s -> syntax_arguments_typed s (print_term info)
        (print_type info) (Some t) fmt tl
153
154
155
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
          | _ -> fprintf fmt "@[(%a@ %a)@]"
156
              print_ident ls.ls_name (print_list space (print_term info)) tl
157
158
159
        end end
  | Tlet (t1, tb) ->
      let v, t2 = t_open_bound tb in
160
      fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
161
162
163
164
165
166
167
168
169
        (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
  | Tcase _ -> unsupportedTerm t
      "smtv2 : you must eliminate match"
  | Teps _ -> unsupportedTerm t
      "smtv2 : you must eliminate epsilon"
170
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
171

172
173
and print_fmla info fmt f = match f.t_node with
  | Tapp ({ ls_name = id }, []) ->
174
      print_ident fmt id
175
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
176
177
      | Some s -> syntax_arguments_typed s (print_term info)
        (print_type info) None fmt tl
178
179
180
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "%a" print_ident ls.ls_name
          | _ -> fprintf fmt "(%a@ %a)"
181
              print_ident ls.ls_name (print_list space (print_term info)) tl
182
        end end
183
184
185
  | Tquant (q, fq) ->
      let q = match q with Tforall -> "forall" | Texists -> "exists" in
      let vl, tl, f = t_open_quant fq in
186
187
188
      (* TODO trigger dépend des capacités du prover : 2 printers?
      smtwithtriggers/smtstrict *)
      if tl = [] then
189
        fprintf fmt "@[(%s@ (%a)@ %a)@]"
190
191
192
193
          q
          (print_var_list info) vl
          (print_fmla info) f
      else
194
        fprintf fmt "@[(%s@ (%a)@ (! %a %a))@]"
195
196
197
198
199
          q
          (print_var_list info) vl
          (print_fmla info) f
          (print_triggers info) tl;
      List.iter forget_var vl
200
  | Tbinop (Tand, f1, f2) ->
201
      fprintf fmt "@[(and@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
202
  | Tbinop (Tor, f1, f2) ->
203
      fprintf fmt "@[(or@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
204
  | Tbinop (Timplies, f1, f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
205
      fprintf fmt "@[(=>@ %a@ %a)@]"
206
        (print_fmla info) f1 (print_fmla info) f2
207
  | Tbinop (Tiff, f1, f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
208
      fprintf fmt "@[(=@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
209
  | Tnot f ->
210
      fprintf fmt "@[(not@ %a)@]" (print_fmla info) f
211
  | Ttrue ->
212
      fprintf fmt "true"
213
  | Tfalse ->
214
      fprintf fmt "false"
215
  | Tif (f1, f2, f3) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
216
      fprintf fmt "@[(ite %a@ %a@ %a)@]"
217
        (print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
218
  | Tlet (t1, tb) ->
219
      let v, f2 = t_open_bound tb in
220
221
222
      fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
        (print_term info) t1 (print_fmla info) f2;
      forget_var v
223
  | Tcase _ -> unsupportedTerm f
224
      "smtv2 : you must eliminate match"
225
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
226

227
228
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
229

Andrei Paskevich's avatar
Andrei Paskevich committed
230
and print_trigger info fmt e = fprintf fmt "%a" (print_expr info) e
231
232
233
234
235
236
237
238

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

let print_logic_binder info fmt v =
239
240
  fprintf fmt "%a: %a" print_ident v.vs_name
    (print_type info) v.vs_ty
241

242
243
let print_type_decl info fmt ts =
  if ts.ts_def <> None then () else
244
  if Mid.mem ts.ts_name info.info_syn then () else
245
246
  fprintf fmt "(declare-sort %a %i)@\n@\n"
    print_ident ts.ts_name (List.length ts.ts_args)
247

248
249
250
251
252
253
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
254

255
let print_logic_decl info fmt (ls,def) =
256
  if Mid.mem ls.ls_name info.info_syn then () else
257
258
259
260
261
262
263
  let vsl,expr = Decl.open_ls_defn def in
  fprintf fmt "@[<hov 2>(declare-fun %a (%a) %a %a)@]@\n@\n"
    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
264
265
266
267
268
269
270

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 ->
271
272
      fprintf fmt "@[(assert@\n";
      fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
273
      (match pr.pr_name.id_loc with
274
275
276
        | None -> ()
        | Some loc -> fprintf fmt " @[;; %a@]@\n"
            Loc.gen_report_position loc);
277
278
279
280
281
      fprintf fmt "  @[(not@ %a))@]@\n" (print_fmla info) f;
      fprintf fmt "@[(check-sat)@]@\n"
  | Plemma| Pskip -> assert false

let print_decl info fmt d = match d.d_node with
282
283
284
285
286
287
  | Dtype ts ->
      print_type_decl info fmt ts
  | Ddata _ -> unsupportedDecl d
      "smtv2 : algebraic type are not supported"
  | Dparam ls ->
      print_param_decl info fmt ls
288
289
290
  | Dlogic dl ->
      print_list nothing (print_logic_decl info) fmt dl
  | Dind _ -> unsupportedDecl d
291
      "smtv2 : inductive definition are not supported"
292
293
294
  | Dprop (k,pr,f) ->
      if Mid.mem pr.pr_name info.info_syn then () else
      print_prop_decl info fmt k pr f
295
296
297

let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)

298
299
300
301
302
303
304
305
306
307
let distingued =
  let dist_syntax mls = function
    | [MAls ls;MAstr s] -> Mls.add ls s mls
    | _ -> assert false in
  let dist_dist syntax mls = function
    | [MAls ls;MAls lsdis] ->
      begin try
              Mid.add lsdis.ls_name (Mls.find ls syntax) mls
        with Not_found -> mls end
    | _ -> assert false in
308
  Trans.on_meta meta_syntax_logic (fun syntax ->
309
    let syntax = List.fold_left dist_syntax Mls.empty syntax in
310
    Trans.on_meta Discriminate.meta_lsinst (fun dis ->
311
312
313
      let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
      Trans.return dis2))

314
let print_task_old pr thpr fmt task =
315
316
317
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
  let info = {
318
319
    info_syn = Mid.union (fun _ _ s -> Some s)
      (get_syntax_map task) (Trans.apply distingued task);
320
    (* complex_type = Hty.create 5; *)
321
322
323
  }
  in
  let decls = Task.task_decls task in
324
  fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
325
326

let () = register_printer "smtv2"
327
  (fun _env pr thpr ?old:_ fmt task ->
328
     forget_all ident_printer;
329
330
331
332
333
334
335
336
337
338
339
340
     print_task_old pr thpr fmt task)

let print_decls =
  let add_ls sm acc = function
    | [MAls ls; MAls lsdis] ->
        begin try
          Mid.add lsdis.ls_name (Mid.find ls.ls_name sm) acc
        with Not_found -> acc end
    | _ -> assert false in
  let print dls sm fmt d =
    let info = {
      info_syn = List.fold_left (add_ls sm) sm dls;
Andrei Paskevich's avatar
Andrei Paskevich committed
341
    } in
342
343
344
345
    print_decl info fmt d in
  Trans.on_meta Discriminate.meta_lsinst (fun dls ->
    Printer.sprint_decls (print dls))

346
let print_task _env pr thpr ?old:_ fmt task =
347
348
349
350
351
352
353
354
  (* In trans-based p-printing [forget_all] is taboo *)
  (* forget_all ident_printer; *)
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
  fprintf fmt "%a@." (print_list nothing string)
    (List.rev (Trans.apply print_decls task))

let () = register_printer "smtv2new" print_task