smt.ml 8.36 KB
Newer Older
Francois Bobot's avatar
Francois Bobot committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
19
open Register
Francois Bobot's avatar
Francois Bobot committed
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
open Format
open Pp
open Ident
open Ty
open Term
open Decl
open Task

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"] 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


let rec print_type drv fmt ty = match ty.ty_node with
51
  | Tyvar _ -> unsupported "smt : you must encode the polymorphism"
52
  | Tyapp (ts, tl) -> begin match Driver.query_syntax drv ts.ts_name with 
53 54 55 56 57 58 59 60 61
      | Some s -> Driver.syntax_arguments s (print_type drv) fmt tl
      | None -> fprintf fmt "%a%a" (print_tyapp drv) tl print_ident ts.ts_name
    end

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

62
let print_type drv fmt = catch_unsupportedType (print_type drv fmt)
63

Francois Bobot's avatar
Francois Bobot committed
64
let rec print_term drv fmt t = match t.t_node with
65
  | Tbvar _ -> assert false
Francois Bobot's avatar
Francois Bobot committed
66 67 68
  | Tconst c ->
      Pretty.print_const fmt c
  | Tvar v -> print_var fmt v
69
  | Tapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
70
      | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
71 72
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
73
          | _ -> fprintf fmt "@[(%a@ %a)@]" 
74 75
	      print_ident ls.ls_name (print_list space (print_term drv)) tl
        end end
Francois Bobot's avatar
Francois Bobot committed
76 77
  | Tlet (t1, tb) ->
      let v, t2 = t_open_bound tb in
78
      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
Francois Bobot's avatar
Francois Bobot committed
79 80
        (print_term drv) t1 (print_term drv) t2;
      forget_var v
81
  | Tif (f1,t1,t2) -> 
82
      fprintf fmt "@[(ite %a@ %a@ %a)@]"
83
        (print_fmla drv) f1 (print_term drv) t1 (print_term drv) t2
84
  | Tcase _ -> unsupportedTerm t 
85
      "smtv1 : you must eliminate match"
86
  | Teps _ -> unsupportedTerm t 
87 88 89
      "smtv1 : you must eliminate epsilon"

and print_fmla drv fmt f = match f.f_node with
Francois Bobot's avatar
Francois Bobot committed
90 91
  | Fapp ({ ls_name = id }, []) ->
      print_ident fmt id
92
  | Fapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
93
      | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
94 95
      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
          | [] -> fprintf fmt "%a" print_ident ls.ls_name
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96
          | _ -> fprintf fmt "(%a@ %a)" 
97 98
	      print_ident ls.ls_name (print_list space (print_term drv)) tl 
        end end
Francois Bobot's avatar
Francois Bobot committed
99 100
  | Fquant (q, fq) ->
      let q = match q with Fforall -> "forall" | Fexists -> "exists" in
101
      let vl, _tl, f = f_open_quant fq in
Francois Bobot's avatar
Francois Bobot committed
102 103 104 105 106 107 108 109 110 111
      (* TODO trigger *)
      let rec forall fmt = function
        | [] -> print_fmla drv fmt f
        | v::l -> 
	    fprintf fmt "@[(%s (%a %a)@ %a)@]" q print_var v 
              (print_type drv) v.vs_ty forall l
      in
      forall fmt vl;
      List.iter forget_var vl
  | Fbinop (Fand, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
112
      fprintf fmt "@[(and@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
Francois Bobot's avatar
Francois Bobot committed
113
  | Fbinop (For, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114
      fprintf fmt "@[(or@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
Francois Bobot's avatar
Francois Bobot committed
115
  | Fbinop (Fimplies, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116
      fprintf fmt "@[(implies@ %a@ %a)@]" 
Francois Bobot's avatar
Francois Bobot committed
117 118
        (print_fmla drv) f1 (print_fmla drv) f2
  | Fbinop (Fiff, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
119
      fprintf fmt "@[(iff@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
Francois Bobot's avatar
Francois Bobot committed
120 121 122 123 124 125 126
  | Fnot f ->
      fprintf fmt "@[(not@ %a)@]" (print_fmla drv) f
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fif (f1, f2, f3) ->
127
      fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
Francois Bobot's avatar
Francois Bobot committed
128
	(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv) f3
129 130
  | Flet (t1, tb) ->
      let v, f2 = f_open_bound tb in
131
      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
132 133
        (print_term drv) t1 (print_fmla drv) f2;
      forget_var v
134
  | Fcase _ -> unsupportedFmla f 
135 136
      "smtv1 : you must eliminate match"
      
Francois Bobot's avatar
Francois Bobot committed
137 138 139 140 141 142 143 144 145
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)

and print_triggers drv fmt tl = print_list comma (print_expr drv) fmt tl


let print_logic_binder drv fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type drv) v.vs_ty

let print_type_decl drv fmt = function
146
  | ts, Tabstract when Driver.query_remove drv ts.ts_name -> false
147 148
  | ts, Tabstract when ts.ts_args = [] ->
      fprintf fmt ":extrasorts (%a)" print_ident ts.ts_name; true
149 150
  | _, Tabstract -> unsupported "smtv1 : type with argument are not supported"
  | _, Talgebraic _ -> unsupported "smtv1 : algebraic type are not supported"
151 152 153 154 155 156 157 158 159 160 161 162 163

let print_logic_decl drv fmt (ls,ld) = match ld with
  | None ->
      begin match ls.ls_value with
        | None ->
            fprintf fmt "@[<hov 2>:extrapreds ((%a %a))@]@\n"
              print_ident ls.ls_name
              (print_list space (print_type drv)) ls.ls_args
        | Some value ->
            fprintf fmt "@[<hov 2>:extrafuns ((%a %a %a))@]@\n"
              print_ident ls.ls_name
              (print_list space (print_type drv)) ls.ls_args 
              (print_type drv) value
Francois Bobot's avatar
Francois Bobot committed
164
      end
165
  | Some _ -> unsupported "Predicate and function definition aren't supported"
Francois Bobot's avatar
Francois Bobot committed
166

167
let print_logic_decl drv fmt d = 
168 169
  if Driver.query_remove drv (fst d).ls_name then
    false else (print_logic_decl drv fmt d; true)
Francois Bobot's avatar
Francois Bobot committed
170
  
171
let print_decl drv fmt d = match d.d_node with
Francois Bobot's avatar
Francois Bobot committed
172 173 174
  | Dtype dl ->
      print_list_opt newline (print_type_decl drv) fmt dl
  | Dlogic dl ->
175
      print_list_opt newline (print_logic_decl drv) fmt dl
176
  | Dind _ -> unsupportedDecl d 
177
      "smt : inductive definition are not supported"
178
  | Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name -> false
179
  | Dprop (Paxiom, _pr, f) ->
Francois Bobot's avatar
Francois Bobot committed
180 181 182 183 184 185 186 187 188 189
      fprintf fmt "@[<hov 2>:assumption@ %a@]@\n" 
        (print_fmla drv) f; true
  | Dprop (Pgoal, pr, f) ->
      fprintf fmt "@[:formula@\n";
      fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
      (match id_from_user pr.pr_name with
        | None -> ()
        | Some loc -> fprintf fmt " @[;; %a@]@\n" 
            Loc.gen_report_position loc);
      fprintf fmt "  @[(not@ %a)@]" (print_fmla drv) f;true
190 191
  | Dprop (Plemma, _, _) -> assert false

192
let print_decl drv fmt = catch_unsupportedDecl (print_decl drv fmt)
Francois Bobot's avatar
Francois Bobot committed
193

194
let print_task drv fmt task = 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
195
  fprintf fmt "(benchmark why3@\n" 
Francois Bobot's avatar
Francois Bobot committed
196 197
    (*print_ident (Task.task_goal task).pr_name*);
  fprintf fmt "  :status unknown@\n";
198
  Driver.print_full_prelude drv task fmt;
Francois Bobot's avatar
Francois Bobot committed
199
  let decls = Task.task_decls task in
200
  ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls);
Francois Bobot's avatar
Francois Bobot committed
201 202
  fprintf fmt "@\n)@."

203
let () = register_printer "smtv1" 
Francois Bobot's avatar
Francois Bobot committed
204 205
  (fun drv fmt task -> 
     forget_all ident_printer;
206
     print_task drv fmt task)