eliminate ite and eliminate if_then_else

Makefile.in

@@ -105,7 +105,7 @@ LIB_TRANSFORM = simplify_recursive_definition inlining \
 		split_conjunction encoding_decorate \
 		remove_logic_definition eliminate_inductive \
 		compile_match eliminate_algebraic \
-		eliminate_let eliminate_definition
+		eliminate_constructs eliminate_definition
 
 LIB_PRINTER = print_real printer_utils alt_ergo why3 smt coq
 

drivers/alt_ergo.drv

@@ -17,6 +17,8 @@ transformation "compile_match"
 transformation "eliminate_definition"
 transformation "eliminate_algebraic"
 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" *)

src/core/term.ml

@@ -1318,6 +1318,8 @@ let f_and_simp f1 f2 = match f1.f_node, f2.f_node with
   | _, Ffalse -> f2
   | _, _      -> f_and f1 f2
 
+let f_and_simp_l l = List.fold_left f_and_simp f_true l
+
 let f_or_simp f1 f2 = match f1.f_node, f2.f_node with
   | Ftrue, _  -> f1
   | _, Ftrue  -> f2
@@ -1325,6 +1327,8 @@ let f_or_simp f1 f2 = match f1.f_node, f2.f_node with
   | _, Ffalse -> f1
   | _, _      -> f_or f1 f2
 
+let f_or_simp_l l = List.fold_left f_or_simp f_false l
+
 let f_implies_simp f1 f2 = match f1.f_node, f2.f_node with
   | Ftrue, _  -> f2
   | _, Ftrue  -> f2

src/core/term.mli

@@ -209,7 +209,9 @@ val f_forall_simp : vsymbol list -> trigger list -> fmla -> fmla
 val f_exists_simp : vsymbol list -> trigger list -> fmla -> fmla
 val f_quant_simp : quant -> vsymbol list -> trigger list -> fmla -> fmla
 val f_and_simp : fmla -> fmla -> fmla
+val f_and_simp_l : fmla list -> fmla
 val f_or_simp : fmla -> fmla -> fmla
+val f_or_simp_l : fmla list -> fmla
 val f_implies_simp : fmla -> fmla -> fmla
 val f_iff_simp : fmla -> fmla -> fmla
 val f_binary_simp : binop -> fmla -> fmla -> fmla

src/printer/smt.ml

@@ -80,7 +80,7 @@ let rec print_term drv fmt t = match t.t_node with
         (print_term drv) t1 (print_term drv) t2;
       forget_var v
   | Tif (f1,t1,t2) -> 
-      fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
+      fprintf fmt "@[(ite %a@ %a@ %a)@]"
         (print_fmla drv) f1 (print_term drv) t1 (print_term drv) t2
   | Tcase _ -> unsupportedExpression (Term t) 
       "smtv1 : you must eliminate match"

src/transform/eliminate_constructs.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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 l =
+  (* TODO :
+     Use polarity in order to choose the most efficient translation of ite *)
+  List.fold_left (fun acc (c,f) -> f_and_simp acc (f_implies_simp c f)) 
+    f_true 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 f)]
+and remove_ite_f 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 l
+    | Flet (t,fb) ->
+        let vs,f' = f_open_bound fb in
+        let f'' = remove_ite_f 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 tl
+        end
+    | Fquant (q, b) -> 
+        let vl, tl, f1 = f_open_quant b in
+        let f1' = remove_ite_f 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 f in
+              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 (fun _ -> assert false) remove_ite_f 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 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 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 t
+
+and remove_if_then_else_f f =
+  match f.f_node with
+    | Fif (f1,f2,f3) -> f_and (f_implies f1 f2) (f_implies (f_not f1) f3)
+    | _ -> f_map remove_if_then_else_t remove_if_then_else_f f
+
+let eliminate_if_then_else =
+  Register.store (fun () -> Trans.rewrite remove_if_then_else_t 
+                    remove_if_then_else_f None)
+
+let () = Register.register_transform
+  "eliminate_if_then_else" eliminate_if_then_else

src/transform/eliminate_let.mli → src/transform/eliminate_constructs.mli

@@ -17,8 +17,23 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** 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 : Term.fmla -> Term.fmla
+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 : Term.fmla -> Term.fmla
+
+val eliminate_if_then_else : Task.task Register.trans_reg
+

src/transform/eliminate_definition.ml

@@ -46,7 +46,7 @@ let rec add_fd kn task nm ls hd lm e = match e.t_node with
       let v,e = t_open_bound b in
       add_fd kn task nm ls hd ((v,t)::lm) e
   | Tcase ([t],bl) ->
-      let t = Eliminate_let.remove_let_t (unfold_t lm t) in
+      let t = Eliminate_constructs.remove_let_t (unfold_t lm t) in
       begin match t.t_node with
         | Tvar v ->
             let mk_br (w,m) br =
@@ -90,7 +90,7 @@ let rec add_pd kn task nm ls hd lm e = match e.f_node with
       let v,e = f_open_bound b in
       add_pd kn task nm ls hd ((v,t)::lm) e
   | Fcase ([t],bl) ->
-      let t = Eliminate_let.remove_let_t (unfold_t lm t) in
+      let t = Eliminate_constructs.remove_let_t (unfold_t lm t) in
       begin match t.t_node with
         | Tvar v ->
             let mk_br (w,m) br =

src/transform/eliminate_let.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  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
-
-let rec rewrite_t map t =
-  match t.t_node with
-    | Tlet (t1,tb) ->
-        let t1 = rewrite_t map t1 in
-        let vs,t2 = t_open_bound tb in
-        rewrite_t (Mvs.add vs t1 map) t2
-    | Tvar vs ->
-        begin try
-          Mvs.find vs map
-        with Not_found -> t end
-    | _ -> t_map (rewrite_t map) (rewrite_f map) t
-
-and rewrite_f map f =
-  match f.f_node with
-    | Flet (t1,fb) ->
-        let t1 = rewrite_t map t1 in
-        let vs,f2 = f_open_bound fb in
-        rewrite_f (Mvs.add vs t1 map) f2
-    | _ -> f_map (rewrite_t map) (rewrite_f map) f
-
-let remove_let_t = rewrite_t Mvs.empty
-let remove_let_f = rewrite_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
-

src/transform/split_conjunction.ml

@@ -20,14 +20,7 @@
 open Ident
 open Term
 open Decl
-
-let list_fold_product f acc l1 l2 =
-  List.fold_left 
-    (fun acc e1 ->
-       List.fold_left 
-         (fun acc e2 -> f acc e1 e2) 
-         acc l2) 
-    acc l1
+open Util
 
 let rec split_pos split_neg acc f =
   let split_pos acc f = 

src/util/util.ml

@@ -34,14 +34,19 @@ let option_eq eq a b = match a,b with
 
 (* useful list combinators *)
 
-let map_fold_left f acc l =
+let rev_map_fold_left f acc l =
   let acc, rev =
     List.fold_left
       (fun (acc, rev) e -> let acc, e = f acc e in acc, e :: rev)
       (acc, []) l
   in
+  acc, rev
+
+let map_fold_left f acc l =
+  let acc, rev = rev_map_fold_left f acc l in
   acc, List.rev rev
 
+
 let list_all2 pr l1 l2 =
   try List.for_all2 pr l1 l2 with Invalid_argument _ -> false
 
@@ -51,6 +56,22 @@ let map_join_left map join = function
 
 let list_apply f = List.fold_left (fun acc x -> List.rev_append (f x) acc) []
 
+
+let list_fold_product f acc l1 l2 =
+  List.fold_left 
+    (fun acc e1 ->
+       List.fold_left 
+         (fun acc e2 -> f acc e1 e2) 
+         acc l2) 
+    acc l1
+
+let list_fold_product_l f acc ll =
+  let ll = List.rev ll in
+  let rec aux acc le = function
+    | [] -> f acc le
+    | l::ll -> List.fold_left (fun acc e -> aux acc (e::le) ll) acc l in
+  aux acc [] ll
+
 (* boolean fold accumulators *)
 
 exception FoldSkip

src/util/util.mli

@@ -31,6 +31,9 @@ val option_eq : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool
 
 (* useful list combinators *)
 
+val rev_map_fold_left :
+  ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
+
 val map_fold_left :
   ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
 
@@ -40,7 +43,20 @@ val map_join_left : ('a -> 'b) -> ('b -> 'b -> 'b) -> 'a list -> 'b
 
 val list_apply : ('a -> 'b list) -> 'a list -> 'b list
 
-(* boolean fold accumulators *)
+val list_fold_product : 
+  ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
+  (** [list_fold_product f acc l1 l2] apply the function [f] with the
+      accumulator [acc] on all the pair of elements of [l1] and [l2]
+      tail-reccursive
+  *)
+
+val list_fold_product_l : 
+  ('a -> 'b list -> 'a) -> 'a -> 'b list list -> 'a
+  (** generalisation of {! list_fold_product} 
+      not tail-reccursive
+  *)
+  
+  (* boolean fold accumulators *)
 
 exception FoldSkip
 

tests/test-bobot.why

@@ -61,11 +61,14 @@ theory TestEnco
   logic h (int) : toto mytype
   axiom A1 : forall x : 'a mytype. p(p2(x)) = x
   goal G2 : forall x:int. f(g(p(x))) = h(x)
-
-
 end
 
-
+theory TestIte
+  use import int.Int
+  logic abs(x:int) : int = if x >= 0 then x else -x 
+  goal G : forall x:int. abs(x) >= 0
+  goal G2 : forall x:int. if x>=0 then x >= 0 else -x>=0 
+end
 
 (*
 Local Variables: