Skip to content

GitLab

why3
why3
Commit 00f53d91 authored by Francois Bobot's avatar Francois Bobot
Browse files
Options

ajout d'exception dans printer_utils, utilisation dans alt-ergo et smt

parent 12f1d315
Hide whitespace changes
Inline Side-by-side
Showing with 273 additions and 87 deletions
Makefile.in
View file @ 00f53d91
......@@ -92,7 +92,7 @@ LIBGENERATED = src/util/rc.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_parser.output src/driver/driver_lexer.ml
LIB_UTIL = pp loc prtree util hashcons sysutil hashweak rc
LIB_UTIL = pp loc prtree hashweak util hashcons sysutil rc
LIB_CORE = ident ty term pattern decl theory task pretty trans env
......@@ -107,7 +107,7 @@ LIB_TRANSFORM = simplify_recursive_definition inlining \
compile_match eliminate_algebraic \
eliminate_let eliminate_definition
LIB_PRINTER = print_real alt_ergo why3 smt coq
LIB_PRINTER = print_real printer_utils alt_ergo why3 smt coq
LIBMODULES = src/config \
$(addprefix src/util/, $(LIB_UTIL)) \
......
drivers/z3.drv
View file @ 00f53d91
......@@ -12,7 +12,7 @@ unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"
transformation "eliminate_definition"
transformation "remove_logic_definition"
transformation "encoding_decorate"
(* transformation "encoding_decorate_every_simple" *)
......
src/core/ty.ml
View file @ 00f53d91
......@@ -62,6 +62,7 @@ end)
module Sts = Tsym.S
module Mts = Tsym.M
module Hts = Tsym.H
module Wts = Tsym.W
let mk_ts name args def = {
ts_name = name;
......@@ -96,6 +97,7 @@ end)
module Sty = Ty.S
module Mty = Ty.M
module Hty = Ty.H
module Wty = Ty.W
let mk_ty n = { ty_node = n; ty_tag = -1 }
let ty_var n = Hsty.hashcons (mk_ty (Tyvar n))
......
src/core/ty.mli
View file @ 00f53d91
......@@ -51,10 +51,12 @@ and ty_node = private
module Sts : Set.S with type elt = tysymbol
module Mts : Map.S with type key = tysymbol
module Hts : Hashtbl.S with type key = tysymbol
module Wts : Hashweak.S with type key = tysymbol
module Sty : Set.S with type elt = ty
module Mty : Map.S with type key = ty
module Hty : Hashtbl.S with type key = ty
module Wty : Hashweak.S with type key = ty
exception BadTypeArity of int * int
exception DuplicateTypeVar of tvsymbol
......
src/main.ml
View file @ 00f53d91
......@@ -260,6 +260,8 @@ let rec report fmt = function
Prover.report fmt e
| Trans.Error e ->
Trans.report fmt e
| Printer_utils.Error e ->
Printer_utils.report fmt e
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
let print_th_namespace fmt th =
......
src/printer/alt_ergo.ml
View file @ 00f53d91
......@@ -16,7 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Printer_utils
open Format
open Pp
open Ident
......@@ -70,17 +70,14 @@ let rec print_term drv fmt t = match t.t_node with
| Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
| None -> fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp drv) tl
end
| Tlet (t1, tb) ->
let v, t2 = t_open_bound tb in
fprintf fmt "@[(let %a = %a@ in %a)@]" print_ident v.vs_name
(print_term drv) t1 (print_term drv) t2;
forget_var v
| Tif _ ->
assert false
| Tcase _ ->
assert false
| Teps _ ->
assert false
| Tlet _ -> unsupportedExpression (Term t)
"alt-ergo : you must eliminate let in term"
| Tif _ -> unsupportedExpression (Term t)
"alt-ergo : you must eliminate if_then_else"
| Tcase _ -> unsupportedExpression (Term t)
"alt-ergo : you must eliminate match"
| Teps _ -> unsupportedExpression (Term t)
"alt-ergo : you must eliminate epsilon"
and print_tapp drv fmt = function
| [] -> ()
......@@ -121,10 +118,11 @@ let rec print_fmla drv fmt f = match f.f_node with
fprintf fmt "((%a and %a) or (not %a and %a))"
(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv)
f1 (print_fmla drv) f3
| Flet _ ->
assert false
| Fcase _ ->
assert false
| Flet _ -> unsupportedExpression (Fmla f)
"alt-ergo : you must eliminate let in formula"
| Fcase _ -> unsupportedExpression (Fmla f)
"alt-ergo : you must eliminate match"
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
......@@ -146,7 +144,8 @@ let print_type_decl fmt ts = match ts.ts_args with
let print_type_decl drv fmt = function
| ts, Tabstract when Driver.query_remove drv ts.ts_name -> false
| ts, Tabstract -> print_type_decl fmt ts; true
| _, Talgebraic _ -> assert false
| _, Talgebraic _ -> unsupported
"alt-ergo : algebraic datatype are not supported"
let ac_th = ["algebra";"AC"]
......@@ -187,7 +186,8 @@ let print_decl drv fmt d = match d.d_node with
print_list_opt newline (print_type_decl drv) fmt dl
| Dlogic dl ->
print_list_opt newline (print_logic_decl drv) fmt dl
| Dind _ -> assert false (* TODO *)
| Dind _ -> unsupportedDeclaration d
"alt-ergo : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
......@@ -198,6 +198,8 @@ let print_decl drv fmt d = match d.d_node with
| Dprop (Plemma, _, _) ->
assert false
let print_decl drv fmt = catch_unsupportedDeclaration (print_decl drv fmt)
let print_task drv fmt task =
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls)
......
src/printer/printer_utils.ml 0 → 100644
View file @ 00f53d91
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
open Term
open Decl
open Ty
(** exception to use in a printer *)
type error =
| UnsupportedType of ty * string
| UnsupportedExpression of expr * string
| UnsupportedDeclaration of decl * string
| NotImplemented of string
exception Error of error
let error e = raise (Error e)
let unsupportedType e s = error (UnsupportedType (e,s))
let unsupportedExpression e s = error (UnsupportedExpression (e,s))
let unsupportedDeclaration e s = error (UnsupportedDeclaration (e,s))
let notImplemented s = error (NotImplemented s)
let report fmt = function
| UnsupportedType (e,s) ->
let msg = "The printer doesn't support this type" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_ty e s
| UnsupportedExpression (e,s) ->
let msg = "The printer doesn't support this expression" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_expr e s
| UnsupportedDeclaration (d,s) ->
let msg = "The printer doesn't support this declaration" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_decl d s
| NotImplemented (s) ->
Format.fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]@\n" s
(** function which cath inner error *)
exception Unsupported of string
let unsupported s = raise (Unsupported s)
let catch_unsupportedtype f ty =
try f ty with Unsupported s -> unsupportedType ty s
let catch_unsupportedterm f t =
try f t with Unsupported s -> unsupportedExpression (Term t) s
let catch_unsupportedfmla f t =
try f t with Unsupported s -> unsupportedExpression (Fmla t) s
let catch_unsupportedDeclaration f d =
try f d with Unsupported s -> unsupportedDeclaration d s
src/printer/printer_utils.mli 0 → 100644
View file @ 00f53d91
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
(** Useful functions for printer *)
(** {2 exception to use in a transformation } *)
type error =
| UnsupportedType of Ty.ty * string
| UnsupportedExpression of Term.expr * string
| UnsupportedDeclaration of Decl.decl * string
| NotImplemented of string
exception Error of error
val unsupportedType : Ty.ty -> string -> 'a
val unsupportedExpression : Term.expr -> string -> 'a
val unsupportedDeclaration : Decl.decl -> string -> 'a
(** - [expr] is the problematic formula
- [string] explain the problem and
possibly a way to solve it (such as applying another
transforamtion) *)
val notImplemented : string -> 'a
(** [string] explain what is not implemented *)
val report : Format.formatter -> error -> unit
(** function which cath inner error *)
exception Unsupported of string
val unsupported : string -> 'a
val catch_unsupportedtype : (Ty.ty -> 'a) -> (Ty.ty -> 'a)
val catch_unsupportedterm : (Term.term -> 'a) -> (Term.term -> 'a)
val catch_unsupportedfmla : (Term.fmla -> 'a) -> (Term.fmla -> 'a)
val catch_unsupportedDeclaration : (Decl.decl -> 'a) -> (Decl.decl -> 'a)
src/printer/smt.ml
View file @ 00f53d91
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Printer_utils
open Format
open Pp
open Ident
......@@ -39,8 +40,6 @@ let ident_printer =
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let print_tvsymbols _fmt _id = assert false
let forget_var v = forget_id ident_printer v.vs_name
let print_var fmt {vs_name = id} =
......@@ -50,8 +49,7 @@ let print_var fmt {vs_name = id} =
let rec print_type drv fmt ty = match ty.ty_node with
| Tyvar id ->
print_tvsymbols fmt id
| Tyvar _ -> unsupported "smt : you must encode the polymorphism"
| Tyapp (ts, tl) -> begin match Driver.query_syntax drv ts.ts_name with
| 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
......@@ -62,9 +60,10 @@ 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
let print_type drv fmt = catch_unsupportedtype (print_type drv fmt)
let rec print_term drv fmt t = match t.t_node with
| Tbvar _ ->
assert false
| Tbvar _ -> assert false
| Tconst c ->
Pretty.print_const fmt c
| Tvar v -> print_var fmt v
......@@ -77,17 +76,18 @@ let rec print_term drv fmt t = match t.t_node with
end end
| Tlet (t1, tb) ->
let v, t2 = t_open_bound tb in
fprintf fmt "@[(let %a = %a@ in %a)@]" print_ident v.vs_name
fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
(print_term drv) t1 (print_term drv) t2;
forget_var v
| Tif _ ->
assert false
| Tcase _ ->
assert false
| Teps _ ->
assert false
let rec print_fmla drv fmt f = match f.f_node with
| Tif (f1,t1,t2) ->
fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
(print_fmla drv) f1 (print_term drv) t1 (print_term drv) t2
| Tcase _ -> unsupportedExpression (Term t)
"smtv1 : you must eliminate match"
| Teps _ -> unsupportedExpression (Term t)
"smtv1 : you must eliminate epsilon"
and print_fmla drv fmt f = match f.f_node with
| Fapp ({ ls_name = id }, []) ->
print_ident fmt id
| Fapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
......@@ -125,13 +125,16 @@ let rec print_fmla drv fmt f = match f.f_node with
| Ffalse ->
fprintf fmt "false"
| Fif (f1, f2, f3) ->
fprintf fmt "@[(if_then_else %a %a %a@]" (* TODO Not sure *)
fprintf fmt "@[(if_then_else %a@ %a@ %a@]"
(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv) f3
| Flet _ -> (* TODO *)
assert false
| Fcase _ ->
assert false
| Flet (t1, tb) ->
let v, f2 = f_open_bound tb in
fprintf fmt "@[(flet (%a %a)@ %a)@]" print_var v
(print_term drv) t1 (print_fmla drv) f2;
forget_var v
| Fcase _ -> unsupportedExpression (Fmla f)
"smtv1 : you must eliminate match"
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
......@@ -144,8 +147,8 @@ let print_type_decl drv fmt = function
| ts, Tabstract when Driver.query_remove drv ts.ts_name -> false
| ts, Tabstract when ts.ts_args = [] ->
fprintf fmt ":extrasorts (%a)" print_ident ts.ts_name; true
| _, Tabstract -> assert false
| _, Talgebraic _ -> assert false
| _, Tabstract -> unsupported "smtv1 : type with argument are not supported"
| _, Talgebraic _ -> unsupported "smtv1 : algebraic type are not supported"
let print_logic_decl drv fmt (ls,ld) = match ld with
| None ->
......@@ -160,7 +163,7 @@ let print_logic_decl drv fmt (ls,ld) = match ld with
(print_list space (print_type drv)) ls.ls_args
(print_type drv) value
end
| Some _ -> assert false (* Dealt in Encoding *)
| Some _ -> unsupported "Predicate and function definition aren't supported"
let print_logic_decl drv fmt d =
if Driver.query_remove drv (fst d).ls_name then
......@@ -171,7 +174,8 @@ let print_decl drv fmt d = match d.d_node with
print_list_opt newline (print_type_decl drv) fmt dl
| Dlogic dl ->
print_list_opt newline (print_logic_decl drv) fmt dl
| Dind _ -> assert false (* TODO *)
| Dind _ -> unsupportedDeclaration d
"smt : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name -> false
| Dprop (Paxiom, _pr, f) ->
fprintf fmt "@[<hov 2>:assumption@ %a@]@\n"
......@@ -184,8 +188,9 @@ let print_decl drv fmt d = match d.d_node with
| Some loc -> fprintf fmt " @[;; %a@]@\n"
Loc.gen_report_position loc);
fprintf fmt " @[(not@ %a)@]" (print_fmla drv) f;true
| Dprop (Plemma, _, _) ->
assert false
| Dprop (Plemma, _, _) -> assert false
let print_decl drv fmt = catch_unsupportedDeclaration (print_decl drv fmt)
let print_task drv fmt task =
fprintf fmt "(benchmark toto@\n"
......
src/transform/encoding_decorate.ml
View file @ 00f53d91
......@@ -209,21 +209,36 @@ let conv_res_app tenv tvar p tl ty =
sort_app tenv tvar t ty
end
let conv_vs tenv tvar (vsvar,acc) vs =
let tres,vsres =
let ty_res = conv_ty_pos tenv vs.vs_ty in
if ty_res == vs.vs_ty then
t_var vs,vs
else
let tty = term_of_ty tenv tvar vs.vs_ty in
let vsres = (create_vsymbol (id_clone vs.vs_name) ty_res) in
let t = t_var vsres in
t_app tenv.sort [tty;t] tenv.deco, vsres in
(Mvs.add vs tres vsvar,vsres::acc)
let rec rewrite_term tenv tvar vsvar t =
let fnT = rewrite_term tenv tvar vsvar in
let fnT = rewrite_term tenv tvar in
let fnF = rewrite_fmla tenv tvar vsvar in
match t.t_node with
| Tconst _ -> t
| Tvar x -> Mvs.find x vsvar
| Tapp(p,tl) ->
let tl = List.map fnT tl in
let tl = List.map (fnT vsvar) tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
conv_res_app tenv tvar p tl t.t_ty
| Tif (f, t1, t2) ->
t_if (fnF f) (fnT t1) (fnT t2)
t_if (fnF f) (fnT vsvar t1) (fnT vsvar t2)
| Tlet (t1, b) -> let u,t2 = t_open_bound b in
let t1' = fnT t1 in let t2' = fnT t2 in
let (vsvar,u) = conv_vs tenv tvar (vsvar,[]) u in
let u = List.hd u in
let t1' = fnT vsvar t1 in let t2' = fnT vsvar t2 in
if t1' == t1 && t2' == t2 then t else t_let u t1' t2'
| Tcase _ | Teps _ | Tbvar _ ->
Trans.unsupportedExpression
......@@ -252,24 +267,18 @@ and rewrite_fmla tenv tvar vsvar f =
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
f_app p tl
| Fquant (q, b) -> let vl, _tl, f1 = f_open_quant b in
let conv_vs (vsvar,acc) vs =
let tres,vsres =
let ty_res = conv_ty_pos tenv vs.vs_ty in
if ty_res == vs.vs_ty then
t_var vs,vs
else
let tty = term_of_ty tenv tvar vs.vs_ty in
let vsres = (create_vsymbol (id_clone vs.vs_name) ty_res) in
let t = t_var vsres in
t_app tenv.sort [tty;t] tenv.deco, vsres in
(Mvs.add vs tres vsvar,vsres::acc) in
let (vsvar,vl) = List.fold_left conv_vs (vsvar,[]) vl in
let (vsvar,vl) = List.fold_left (conv_vs tenv tvar) (vsvar,[]) vl in
let f1' = fnF vsvar f1 in
let tl' = [] (* TODO *) in
if f1' == f1 (*&& tr_equal tl' tl*) then f
else
let vl = List.rev vl in
f_quant q vl tl' f1'
| Flet (t1, b) -> let u,f2 = f_open_bound b in
let (vsvar,u) = conv_vs tenv tvar (vsvar,[]) u in
let u = List.hd u in
let t1' = fnT t1 in let f2' = fnF vsvar f2 in
if t1' == t1 && f2' == f2 then f else f_let u t1' f2'
| _ -> f_map fnT (fnF vsvar) f
let decl (tenv:tenv) d =
......@@ -319,7 +328,7 @@ Perhaps you could use eliminate_definition"
(*
let decl tenv d =
Format.eprintf "@[<hov 2>Decl : %a =>@\n" Pretty.print_decl d;
Format.eprintf "@[<hov 2>Decl : %a =>@\n@?" Pretty.print_decl d;
let res = decl tenv d in
Format.eprintf "%a@]@." (Pp.print_list Pp.newline Pretty.print_task_tdecl)
res;
......
src/util/hashweak.ml
View file @ 00f53d91
......@@ -17,7 +17,42 @@
(* *)
(**************************************************************************)
module Make (S : Util.Tagged) = struct
module type S = sig
type key
type 'a t
val create : int -> 'a t
(* create a hashtbl with weak keys *)
val find : 'a t -> key -> 'a
(* find the value bound to a key.
Raises Not_found if there is no binding *)
val mem : 'a t -> key -> bool
(* test if a key is bound *)
val set : 'a t -> key -> 'a -> unit
(* bind the key _once_ with the given value *)
val memoize : int -> (key -> 'a) -> (key -> 'a)
(* create a memoizing function *)
val memoize_option : int -> (key option -> 'a) -> (key option -> 'a)
(* memoizing functions on option types *)
end
module type Tagged =
sig
type t
val tag : t -> int
end
module Make (S : Tagged) = struct
type key = S.t
type 'a t = {
table : (int,'a) Hashtbl.t;
......
src/util/hashweak.mli
View file @ 00f53d91
......@@ -17,27 +17,37 @@
(* *)
(**************************************************************************)
module Make (S : Util.Tagged) : sig
module type S = sig
type key
type 'a t
val create : int -> 'a t
(* create a hashtbl with weak keys *)
val find : 'a t -> S.t -> 'a
val find : 'a t -> key -> 'a
(* find the value bound to a key.
Raises Not_found if there is no binding *)
val mem : 'a t -> S.t -> bool
val mem : 'a t -> key -> bool
(* test if a key is bound *)
val set : 'a t -> S.t -> 'a -> unit
val set : 'a t -> key -> 'a -> unit
(* bind the key _once_ with the given value *)
val memoize : int -> (S.t -> 'a) -> (S.t -> 'a)
val memoize : int -> (key -> 'a) -> (key -> 'a)
(* create a memoizing function *)
val memoize_option : int -> (S.t option -> 'a) -> (S.t option -> 'a)
val memoize_option : int -> (key option -> 'a) -> (key option -> 'a)
(* memoizing functions on option types *)
end
module type Tagged =
sig
type t
val tag : t -> int
end
module Make (S : Tagged) : S with type key = S.t
src/util/util.ml
View file @ 00f53d91
......@@ -69,13 +69,7 @@ module Mstr = Map.Make(String)
(* Set, Map, Hashtbl on structures with a unique tag and physical equality *)
module type Tagged =
sig
type t
val tag : t -> int
end
module OrderedHash (X : Tagged) =
module OrderedHash (X : Hashweak.Tagged) =
struct
type t = X.t
let equal = (==)
......@@ -83,11 +77,12 @@ struct
let compare ts1 ts2 = Pervasives.compare (X.tag ts1) (X.tag ts2)
end
module StructMake (X : Tagged) =
module StructMake (X : Hashweak.Tagged) =
struct
module T = OrderedHash(X)
module S = Set.Make(T)
module M = Map.Make(T)
module H = Hashtbl.Make(T)
module W = Hashweak.Make(X)
end
src/util/util.mli
View file @ 00f53d91
......@@ -58,12 +58,7 @@ module Sstr : Set.S with type elt = string
module Mstr : Map.S with type key = string
(* Set, Map, Hashtbl on structures with a unique tag and physical equality *)
module type Tagged =
sig
type t
val tag : t -> int
end
open Hashweak
module OrderedHash (X : Tagged) :
sig
......@@ -78,5 +73,6 @@ sig
module S : Set.S with type elt = X.t
module M : Map.S with type key = X.t
module H : Hashtbl.S with type key = X.t
module W : Hashweak.S with type key = X.t
end
tests/test-bobot.why
View file @ 00f53d91
......@@ -13,7 +13,7 @@ theory Test_encoding
goal G : (forall x:int.f(x)=f(x)) or
(forall x:int. x=x+1)
goal G2 : forall x:int. let x = 0 + 1 in x = 1
goal G2 : forall x:int. let x = 0 + 1 in x = let y = 0 + 1 + 0 in y
end