smtv1.ml 9.43 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
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
     "if then else";"iff";"implies";"ite";"let";"logic";"not";"or";
     "sat";"theory";"true";"unknown";"unsat";"xor";
Ralf Treinen's avatar
Ralf Treinen committed
26
     "assumption";"axioms";"definition";"extensions";"formula";
Francois Bobot's avatar
Francois Bobot committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
     "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
let complex_type = Wty.memoize 3 (fun ty ->
  let s = Pp.string_of_wnl Pretty.print_ty ty in
Clément Fumex's avatar
Clément Fumex committed
51
  create_tysymbol (id_fresh s) [] NoDef)
52

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 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
let number_format = {
    Number.long_int_support = `Default;
    Number.negative_int_support = `Default;
    Number.dec_int_support = `Default;
    Number.hex_int_support = `Unsupported;
    Number.oct_int_support = `Unsupported;
    Number.bin_int_support = `Unsupported;
    Number.negative_real_support = `Default;
    Number.dec_real_support = `Unsupported;
    Number.hex_real_support = `Unsupported;
    Number.frac_real_support =
      `Custom
        ((fun fmt i -> fprintf fmt "%s.0" i),
         (fun fmt i n -> fprintf fmt "(* %s.0 %s.0)" i n),
         (fun fmt i n -> fprintf fmt "(/ %s.0 %s.0)" i n));
  }

92
let rec print_term info fmt t = match t.t_node with
93
  | Tconst c ->
94
      Number.print number_format fmt c
Francois Bobot's avatar
Francois Bobot committed
95
  | Tvar v -> print_var fmt v
96
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
97
      | Some s -> syntax_arguments s (print_term info) fmt tl
98 99
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
100
          | _ -> fprintf fmt "@[(%a@ %a)@]"
101
              print_ident ls.ls_name (print_list space (print_term info)) tl
102
        end end
Francois Bobot's avatar
Francois Bobot committed
103 104
  | Tlet (t1, tb) ->
      let v, t2 = t_open_bound tb in
105
      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
106
        (print_term info) t1 (print_term info) t2;
Francois Bobot's avatar
Francois Bobot committed
107
      forget_var v
108
  | Tif (f1,t1,t2) ->
109
      fprintf fmt "@[(ite %a@ %a@ %a)@]"
110
        (print_fmla info) f1 (print_term info) t1 (print_term info) t2
111
  | Tcase _ -> unsupportedTerm t
Andrei Paskevich's avatar
Andrei Paskevich committed
112
      "smtv1: you must eliminate match"
113
  | Teps _ -> unsupportedTerm t
Andrei Paskevich's avatar
Andrei Paskevich committed
114
      "smtv1: you must eliminate epsilon"
115
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
116

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

167
(*
MARCHE Claude's avatar
MARCHE Claude committed
168
and _print_expr info fmt =
169
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
Francois Bobot's avatar
Francois Bobot committed
170

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

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

177
let print_type_decl info fmt ts =
Clément Fumex's avatar
Clément Fumex committed
178
  if ts.ts_args = [] && not (is_alias_type_def ts.ts_def) then
179 180
  if not (Mid.mem ts.ts_name info.info_syn) then
  fprintf fmt ":extrasorts (%a)@\n@\n" print_ident ts.ts_name
181

182
let print_param_decl info fmt ls = match ls.ls_value with
183
  | None ->
184
      fprintf fmt "@[<hov 2>:extrapreds ((%a %a))@]@\n@\n"
185 186 187
        print_ident ls.ls_name
        (print_list space (print_type info)) ls.ls_args
  | Some value ->
188
      fprintf fmt "@[<hov 2>:extrafuns ((%a %a %a))@]@\n@\n"
189 190 191 192 193
        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 =
194 195
  if not (Mid.mem ls.ls_name info.info_syn) then
  print_param_decl info fmt ls
196

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

221 222
let print_decls =
  let print_decl (sm,ct) fmt d =
223 224
    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)
225 226 227 228 229 230
    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),[]))

231
let print_task args ?old:_ fmt task =
232 233 234
  (* 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
235
  fprintf fmt "  :status unknown@\n";
236 237
  print_prelude fmt args.prelude;
  print_th_prelude task fmt args.th_prelude;
238 239 240 241 242 243 244
  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
245
  ~desc:"Printer@ for@ the@ SMTlib@ version@ 1@ format."