smtv1.ml 9.3 KB
Newer Older
Francois Bobot's avatar
Francois Bobot committed
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
Francois Bobot's avatar
Francois Bobot committed
7 8 9 10 11 12 13 14 15 16 17 18
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
19

Francois Bobot's avatar
Francois Bobot committed
20 21
(** SMT v1 printer with some extensions *)

Francois Bobot's avatar
Francois Bobot committed
22 23 24 25 26 27
open Format
open Pp
open Ident
open Ty
open Term
open Decl
28
open Theory
Francois Bobot's avatar
Francois Bobot committed
29
open Task
30
open Printer
Francois Bobot's avatar
Francois Bobot committed
31

32 33 34 35 36 37 38
(** Options of this printer *)
let use_trigger = Theory.register_meta_excl "Smt : trigger" []
let use_builtin_array = Theory.register_meta_excl "Smt : builtin array" []

(** *)

let ident_printer =
39
  let bls = ["and";"benchmark";"distinct";"exists";"false";"flet";"forall";
Francois Bobot's avatar
Francois Bobot committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
     "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

59
type info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
60
  info_syn : string Mid.t;
61
  info_rem : Sid.t;
62
  use_trigger : bool;
63
}
Francois Bobot's avatar
Francois Bobot committed
64

65
let rec print_type info fmt ty = match ty.ty_node with
66
  | Tyvar _ -> unsupported "smt : you must encode the polymorphism"
François Bobot's avatar
François Bobot committed
67 68 69 70 71
  | 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
  | Tyapp (_, _) -> unsupported "smt : you must encode the complexe type"
72

François Bobot's avatar
François Bobot committed
73 74 75 76
(* 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 *)
77

78
let print_type info fmt = catch_unsupportedType (print_type info fmt)
79

80
let rec print_term info fmt t = match t.t_node with
81 82
  | Tconst (ConstInt n) -> fprintf fmt "%s" n
  | Tconst (ConstReal c) ->
83
      Print_real.print_with_integers
84
        "%s.0" "(* %s.0 %s.0)" "(/ %s.0 %s.0)" fmt c
Francois Bobot's avatar
Francois Bobot committed
85
  | Tvar v -> print_var fmt v
86
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
87
      | Some s -> syntax_arguments s (print_term info) fmt tl
88 89
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
90
          | _ -> fprintf fmt "@[(%a@ %a)@]"
91
              print_ident ls.ls_name (print_list space (print_term info)) tl
92
        end end
Francois Bobot's avatar
Francois Bobot committed
93 94
  | Tlet (t1, tb) ->
      let v, t2 = t_open_bound tb in
95
      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
96
        (print_term info) t1 (print_term info) t2;
Francois Bobot's avatar
Francois Bobot committed
97
      forget_var v
98
  | Tif (f1,t1,t2) ->
99
      fprintf fmt "@[(ite %a@ %a@ %a)@]"
100
        (print_fmla info) f1 (print_term info) t1 (print_term info) t2
101
  | Tcase _ -> unsupportedTerm t
102
      "smtv1 : you must eliminate match"
103
  | Teps _ -> unsupportedTerm t
104
      "smtv1 : you must eliminate epsilon"
105
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
106

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

157 158
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
Francois Bobot's avatar
Francois Bobot committed
159

160
and print_triggers info fmt tl = print_list comma (print_expr info) fmt tl
Francois Bobot's avatar
Francois Bobot committed
161 162


163 164
let print_logic_binder info fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
Francois Bobot's avatar
Francois Bobot committed
165

166 167
let print_type_decl info fmt = function
  | ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
168
  | ts, Tabstract when ts.ts_args = [] ->
169
      fprintf fmt ":extrasorts (%a)" print_ident ts.ts_name; true
170
  | _, Tabstract -> unsupported
171
          "smtv1 : type with argument are not supported"
172
  | _, Talgebraic _ -> unsupported
173
          "smtv1 : algebraic type are not supported"
174

175
let print_logic_decl info fmt (ls,ld) = match ld with
176 177 178 179 180
  | None ->
      begin match ls.ls_value with
        | None ->
            fprintf fmt "@[<hov 2>:extrapreds ((%a %a))@]@\n"
              print_ident ls.ls_name
181
              (print_list space (print_type info)) ls.ls_args
182 183 184
        | Some value ->
            fprintf fmt "@[<hov 2>:extrafuns ((%a %a %a))@]@\n"
              print_ident ls.ls_name
185
              (print_list space (print_type info)) ls.ls_args
186
              (print_type info) value
Francois Bobot's avatar
Francois Bobot committed
187
      end
188
  | Some _ -> unsupported
189
      "Predicate and function definition aren't supported"
Francois Bobot's avatar
Francois Bobot committed
190

191
let print_logic_decl info fmt d =
192 193
  if Sid.mem (fst d).ls_name info.info_rem then
    false else (print_logic_decl info fmt d; true)
194

195
let print_decl info fmt d = match d.d_node with
Francois Bobot's avatar
Francois Bobot committed
196
  | Dtype dl ->
197
      print_list_opt newline (print_type_decl info) fmt dl
Francois Bobot's avatar
Francois Bobot committed
198
  | Dlogic dl ->
199
      print_list_opt newline (print_logic_decl info) fmt dl
200
  | Dind _ -> unsupportedDecl d
201
      "smt : inductive definition are not supported"
202
  | Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
203 204 205
  | Dprop (Paxiom, pr, f) ->
      fprintf fmt "@[<hov 2>;; %s@\n:assumption@ %a@]@\n"
        pr.pr_name.id_string
206
        (print_fmla info) f; true
Francois Bobot's avatar
Francois Bobot committed
207 208 209
  | Dprop (Pgoal, pr, f) ->
      fprintf fmt "@[:formula@\n";
      fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
210
      (match pr.pr_name.id_loc with
Francois Bobot's avatar
Francois Bobot committed
211
        | None -> ()
212
        | Some loc -> fprintf fmt " @[;; %a@]@\n"
Francois Bobot's avatar
Francois Bobot committed
213
            Loc.gen_report_position loc);
214
      fprintf fmt "  @[(not@ %a)@]" (print_fmla info) f;true
215
  | Dprop ((Plemma|Pskip), _, _) -> assert false
216

217
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
Francois Bobot's avatar
Francois Bobot committed
218

Andrei Paskevich's avatar
Andrei Paskevich committed
219
let print_task pr thpr fmt task =
220
  fprintf fmt "(benchmark why3@\n"
Francois Bobot's avatar
Francois Bobot committed
221 222
    (*print_ident (Task.task_goal task).pr_name*);
  fprintf fmt "  :status unknown@\n";
223 224 225
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
  let info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
226
    info_syn = get_syntax_map task;
227 228 229
    info_rem = get_remove_set task;
    use_trigger = false;
  }
230
  in
Francois Bobot's avatar
Francois Bobot committed
231
  let decls = Task.task_decls task in
232
  ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls);
Francois Bobot's avatar
Francois Bobot committed
233 234
  fprintf fmt "@\n)@."

235
let () = register_printer "smtv1"
MARCHE Claude's avatar
MARCHE Claude committed
236
  (fun _env pr thpr ?old:_ fmt task ->
Francois Bobot's avatar
Francois Bobot committed
237
     forget_all ident_printer;
Andrei Paskevich's avatar
Andrei Paskevich committed
238
     print_task pr thpr fmt task)