Skip to content

GitLab

why3
why3
Commit c38aafa7 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

rearrange the transformations

parent 0d0a403d
Hide whitespace changes
Inline Side-by-side
Showing with 144 additions and 268 deletions
Makefile.in
View file @ c38aafa7
......@@ -103,10 +103,9 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
LIB_TRANSFORM = simplify_recursive_definition inlining \
split_conjunction encoding_decorate \
remove_logic_definition eliminate_inductive \
eliminate_definition \
compile_match eliminate_algebraic \
eliminate_constructs eliminate_if \
eliminate_definition
eliminate_inductive eliminate_let eliminate_if
LIB_PRINTER = print_real alt_ergo why3 smt coq
......
drivers/alt_ergo.drv
View file @ c38aafa7
......@@ -13,15 +13,14 @@ fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "compile_match"
transformation "inline_trivial"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "compile_match"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "eliminate_ite"
transformation "eliminate_if_then_else"
transformation "inline_trivial"
(* transformation "split_goal_pos_neg_goal" *)
(* transformation "split_goal_pos_neg_all" *)
theory BuiltIn
syntax type int "int"
......
drivers/cvc3.drv
View file @ c38aafa7
......@@ -11,9 +11,13 @@ unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
(* À discuter *)
transformation "simplify_recursive_definition"
(* transformation (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"*)
transformation "inline_trivial"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "compile_match"
transformation "eliminate_algebraic"
transformation "encoding_decorate"
theory BuiltIn
......
drivers/why3_encoding_decorate.drv
View file @ c38aafa7
printer "why3"
filename "%f-%t-%g.why"
transformation "remove_logic_definition"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "compile_match"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "encoding_decorate"
theory BuiltIn
......
drivers/why3_split_conjunction.drv deleted 100644 → 0
View file @ 0d0a403d
printer "why3"
filename "%f-%t-%g.why"
(* À discuter *)
(* transformation "split_goal_pos_neg_all" *)
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
end
drivers/why3_total_elimination.drv
View file @ c38aafa7
......@@ -5,8 +5,7 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "compile_match"
transformation "eliminate_algebraic"
transformation "eliminate_if_term"
transformation "eliminate_if_fmla"
transformation "eliminate_if"
transformation "eliminate_let"
theory BuiltIn
......
drivers/z3.drv
View file @ c38aafa7
......@@ -12,7 +12,12 @@ unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"
transformation "remove_logic_definition"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "compile_match"
transformation "eliminate_algebraic"
transformation "encoding_decorate"
(* transformation "encoding_decorate_every_simple" *)
......
src/transform/eliminate_constructs.ml deleted 100644 → 0
View file @ 0d0a403d
(**************************************************************************)
(* *)
(* 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 Util
open Ident
open Term
open Decl
(* eliminate let *)
let rec remove_let_t map t =
match t.t_node with
| Tlet (t1,tb) ->
let t1 = remove_let_t map t1 in
let vs,t2 = t_open_bound tb in
remove_let_t (Mvs.add vs t1 map) t2
| Tvar vs ->
begin try
Mvs.find vs map
with Not_found -> t end
| _ -> t_map (remove_let_t map) (remove_let_f map) t
and remove_let_f map f =
match f.f_node with
| Flet (t1,fb) ->
let t1 = remove_let_t map t1 in
let vs,f2 = f_open_bound fb in
remove_let_f (Mvs.add vs t1 map) f2
| _ -> f_map (remove_let_t map) (remove_let_f map) f
let remove_let_t = remove_let_t Mvs.empty
let remove_let_f = remove_let_f Mvs.empty
let eliminate_let =
Register.store (fun () -> Trans.rewrite remove_let_t remove_let_f None)
let () = Register.register_transform "eliminate_let" eliminate_let
(* eliminate if then else *)
let merge f l1 l2 =
let f acc (c1,t1) (c2,t2) =
(f_and_simp c1 c2, f t1 t2)::acc in
list_fold_product f [] l1 l2
let merge_l f tl =
let f acc tl =
let cond,l = List.split tl in
(f_and_simp_l cond, f l)::acc in
list_fold_product_l f [] tl
let and_impl_f sign l =
if sign
then List.fold_left (fun acc (c,f) -> f_and_simp acc (f_implies_simp c f))
f_true l
else List.fold_left (fun acc (c,f) -> f_or_simp acc (f_and_simp c f))
f_false l
let rec remove_ite_t t =
match t.t_node with
| Tif (f,t1,t2) ->
let g f t =
List.map (fun (e,t) -> f_and_simp f e,t) (remove_ite_t t)in
List.rev_append (g f t1) (g (f_not f) t2)
| Tbvar _ | Tvar _ | Tconst _ -> [f_true,t]
| Tapp (ls,tl) ->
merge_l (fun tl -> t_app ls tl t.t_ty) (List.map remove_ite_t tl)
| Tlet (t1,tb) ->
let vs,t2 = t_open_bound tb in
merge (t_let vs) (remove_ite_t t1) (remove_ite_t t2)
| Tcase (tl,tbl) ->
let tl = merge_l (fun x -> x) (List.map remove_ite_t tl) in
let tbl = List.map
(fun e ->
let pl,t = t_open_branch e in
List.map (fun (c,t) -> (c,(pl,t))) (remove_ite_t t)) tbl in
let tbl = merge_l (fun x -> x) tbl in
merge (fun tl tbl -> t_case tl tbl t.t_ty) tl tbl
| Teps fb ->
let vs,f = f_open_bound fb in [f_true,t_eps vs (remove_ite_f true f)]
and remove_ite_f sign f =
match f.f_node with
| Fapp (ls,tl) ->
let l = merge_l (f_app ls) (List.map remove_ite_t tl) in
and_impl_f sign l
| Flet (t,fb) ->
let vs,f' = f_open_bound fb in
let f'' = remove_ite_f sign f' in
let tl = remove_ite_t t in
begin match tl with
| [c,_] when f' == f'' -> assert (c == f_true); f
| _ ->
let tl = List.map (fun (c,t) -> c,f_let vs t f) tl in
and_impl_f sign tl
end
| Fquant (q, b) ->
let vl, tl, f1 = f_open_quant b in
let f1' = remove_ite_f sign f1 in
let tr_map (changed,acc) = function
| Term t as e ->
let tl = remove_ite_t t in
begin match tl with
| [c,_] -> assert (c == f_true); changed,(e::acc)
| _ -> true,
(* can we do better? *)
List.fold_left (fun acc (_,t) -> Term t::acc) acc tl
end
| Fmla f as e ->
let f' = remove_ite_f true f in (*TODO trigger sign *)
if f == f' then changed,e::acc else true,(Fmla f'::acc) in
let changed,tl' = rev_map_fold_left
(fun acc -> List.fold_left tr_map (acc,[])) false tl in
if f1' == f1 && (not changed) then f
else f_quant q vl tl' f1'
| _ -> f_map_sign (fun _ -> assert false) remove_ite_f sign f
let remove_ite_decl d =
match d.d_node with
| Dlogic l ->
let fn acc = function
| ls, Some ld ->
let vl,e = open_ls_defn ld in
begin match e with
| Term t ->
begin let tl = remove_ite_t t in
match tl with
| [] -> assert false
| [c,t] ->
assert (c == f_true);
acc,make_ls_defn ls vl (Term t)
| _ ->
let d = ls,None in
let h = t_app ls (List.map t_var vl) t.t_ty in
let fax acc (c,t) =
let f = f_forall vl [] (f_implies c (f_equ h t)) in
let pr = create_prsymbol (id_clone ls.ls_name) in
(create_prop_decl Paxiom pr f)::acc in
List.fold_left fax acc tl,d
end
| Fmla f -> acc,make_ls_defn ls vl (Fmla (remove_ite_f true f))
end
| ld -> acc,ld
in
let axs,l = (map_fold_left fn [] l) in
(create_logic_decl l)::axs
| _ -> [decl_map (fun _ -> assert false) (remove_ite_f true) d]
let eliminate_ite = Register.store (fun () -> Trans.decl remove_ite_decl None)
let () = Register.register_transform "eliminate_ite" eliminate_ite
(* eliminate if_then_else *)
let rec remove_if_then_else_t t =
t_map remove_if_then_else_t (remove_if_then_else_f true) t
and remove_if_then_else_f sign f =
match f.f_node with
| Fif (f1,f2,f3) ->
if sign
then f_and (f_implies f1 f2) (f_implies (f_not f1) f3)
else f_or (f_and f1 f2) (f_and (f_not f1) f3)
| _ -> f_map_sign remove_if_then_else_t remove_if_then_else_f sign f
let eliminate_if_then_else =
Register.store (fun () -> Trans.rewrite remove_if_then_else_t
(remove_if_then_else_f true) None)
let () = Register.register_transform
"eliminate_if_then_else" eliminate_if_then_else
src/transform/eliminate_constructs.mli deleted 100644 → 0
View file @ 0d0a403d
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
(** eliminate let *)
val remove_let_t : Term.term -> Term.term
val remove_let_f : Term.fmla -> Term.fmla
val eliminate_let : Task.task Register.trans_reg
(** eliminate ite, ie if then else in term *)
val remove_ite_t : Term.term -> (Term.fmla * Term.term) list
val remove_ite_f : bool -> Term.fmla -> Term.fmla
(* [remove_ite_f sign f] *)
val remove_ite_decl : Decl.decl -> Decl.decl list
val eliminate_ite : Task.task Register.trans_reg
(** eliminate ite, ie if then else in term *)
val remove_if_then_else_t : Term.term -> Term.term
val remove_if_then_else_f : bool -> Term.fmla -> Term.fmla
(* [remove_if_then_else_f sign f] *)
val eliminate_if_then_else : Task.task Register.trans_reg
src/transform/eliminate_if.ml
View file @ c38aafa7
......@@ -48,13 +48,11 @@ and elim_f contF f = match f.f_node with
contF (f_map_cont (elim_t []) elim_f (fun f -> f) f)
| _ -> f_map_cont elim_tr elim_f contF f
(* the only terms we can still meet in a formula are the terms
* in triggers. Since we cannot eliminate 'if' in a trigger term
* (and we shouldn't have one in the first place), we will simply
* replace it with a fresh variable and let the prover sort it out. *)
(* the only terms we can still meet are the terms in triggers *)
and elim_tr contT t = match t.t_node with
| Tif _ -> contT (t_var (create_vsymbol (id_fresh "if") t.t_ty))
| Tif _ ->
Register.unsupportedExpression (Term t)
"cannot eliminate 'if-then-else' in trigger terms"
| _ -> t_map_cont elim_tr elim_f contT t
let elim_f f = elim_f (fun f -> f) f
......@@ -79,7 +77,7 @@ let add_ld axl d = match d with
axl, make_ls_defn ls vl (e_map elim_t elim_f e)
end
let elim d = match d.d_node with
let elim_d d = match d.d_node with
| Dlogic l ->
let axl, l = map_fold_left add_ld [] l in
let d = create_logic_decl l in
......@@ -87,11 +85,6 @@ let elim d = match d.d_node with
| _ ->
[decl_map (fun _ -> assert false) elim_f d]
let eliminate_if_term =
Register.store (fun () -> Trans.decl elim None)
let () = Register.register_transform "eliminate_if_term" eliminate_if_term
(* eliminate if-then-else in formulas *)
let rec elim_t t = t_map elim_t (elim_f true) t
......@@ -107,8 +100,19 @@ and elim_f sign f = match f.f_node with
| _ ->
f_map_sign elim_t elim_f sign f
(* registration *)
let eliminate_if_term =
Register.store (fun () -> Trans.decl elim_d None)
let eliminate_if_fmla =
Register.store (fun () -> Trans.rewrite elim_t (elim_f true) None)
let () = Register.register_transform "eliminate_if_fmla" eliminate_if_fmla
let eliminate_if =
Register.compose eliminate_if_term eliminate_if_fmla
let () =
Register.register_transform "eliminate_if_term" eliminate_if_term;
Register.register_transform "eliminate_if_fmla" eliminate_if_fmla;
Register.register_transform "eliminate_if" eliminate_if
src/transform/eliminate_if.mli
View file @ c38aafa7
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
val eliminate_if_term : Task.task Register.trans_reg
val eliminate_if_fmla : Task.task Register.trans_reg
val eliminate_if : Task.task Register.trans_reg
src/transform/remove_logic_definition.ml → src/transform/eliminate_let.ml
View file @ c38aafa7
......@@ -17,29 +17,54 @@
(* *)
(**************************************************************************)
open Util
open Ident
open Term
open Decl
let decl d =
match d.d_node with
| Dtype _ -> [d]
| Dlogic l ->
let f (accls,accdef) (ls,def) =
let accls =(create_logic_decl [ls,None])::accls in
match def with
| None -> accls,accdef
| Some ls_defn ->
let fmla = ls_defn_axiom ls_defn in
let prsymbol = create_prsymbol (id_clone ls.ls_name) in
accls,(create_prop_decl Paxiom prsymbol fmla)::accdef in
let accls,accdef = (List.fold_left f ([],[]) l) in
(List.rev_append accls) accdef
| Dind _ -> [d]
| Dprop _ -> [d]
let t = Register.store (fun () -> Trans.decl decl None)
let () = Register.register_transform "remove_logic_definition" t
(* eliminate let *)
let rec remove_let_t fnF map t = match t.t_node with
| Tvar vs ->
(try Mvs.find vs map with Not_found -> t)
| Tlet (t1,tb) ->
let t1 = remove_let_t fnF map t1 in
let vs,t2 = t_open_bound tb in
remove_let_t fnF (Mvs.add vs t1 map) t2
| _ ->
t_map (remove_let_t fnF map) (fnF map) t
and remove_let_f fnT map f = match f.f_node with
| Flet (t1,fb) ->
let t1 = fnT map t1 in
let vs,f2 = f_open_bound fb in
remove_let_f fnT (Mvs.add vs t1 map) f2
| _ ->
f_map (fnT map) (remove_let_f fnT map) f
let rec elim_let_t map t = remove_let_t elim_let_f map t
and elim_let_f map f = remove_let_f elim_let_t map f
let elim_let_t = elim_let_t Mvs.empty
let elim_let_f = elim_let_f Mvs.empty
let rec skip_t map t = t_map (skip_t map) (remove_let_f skip_t map) t
let rec skip_f map f = f_map (remove_let_t skip_f map) (skip_f map) f
let skip_t = skip_t Mvs.empty
let skip_f = skip_f Mvs.empty
let eliminate_let_term =
Register.store (fun () -> Trans.rewrite elim_let_t skip_f None)
let eliminate_let_fmla =
Register.store (fun () -> Trans.rewrite skip_t elim_let_f None)
let eliminate_let =
Register.store (fun () -> Trans.rewrite elim_let_t elim_let_f None)
let () =
Register.register_transform "eliminate_let_term" eliminate_let_term;
Register.register_transform "eliminate_let_fmla" eliminate_let_fmla;
Register.register_transform "eliminate_let" eliminate_let
src/transform/remove_logic_definition.mli → src/transform/eliminate_let.mli
View file @ c38aafa7
......@@ -17,6 +17,12 @@
(* *)
(**************************************************************************)
val decl : Decl.decl -> Decl.decl list
(** eliminate let *)
val elim_let_t : Term.term -> Term.term
val elim_let_f : Term.fmla -> Term.fmla
val eliminate_let_term : Task.task Register.trans_reg
val eliminate_let_fmla : Task.task Register.trans_reg
val eliminate_let : Task.task Register.trans_reg
val t : Task.task Register.trans_reg
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment