simplify_formula : simplify the formulas and remove trivial goals and axioms

Makefile.in

@@ -104,7 +104,8 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 LIB_TRANSFORM = simplify_recursive_definition inlining \
 		split_conjunction encoding_decorate \
 		eliminate_definition eliminate_algebraic \
-		eliminate_inductive eliminate_let eliminate_if
+		eliminate_inductive eliminate_let eliminate_if\
+		simplify_formula
 
 LIB_PRINTER = print_real alt_ergo why3 smt coq tptp
 

src/core/term.ml

@@ -923,10 +923,10 @@ let rec pat_equal_alpha p1 p2 =
 
 (* safe opening map *)
 
-let t_branch fn acc b =
+let t_branch' fn acc b =
   let pl,t = t_open_branch b in let t' = fn t in acc && t_equal t' t, (pl,t')
 
-let f_branch fn acc b =
+let f_branch' fn acc b =
   let pl,f = f_open_branch b in let f' = fn f in acc && f_equal f' f, (pl,f')
 
 let t_map fnT fnF t = t_label_copy t (match t.t_node with
@@ -939,7 +939,7 @@ let t_map fnT fnF t = t_label_copy t (match t.t_node with
       if t_equal t1' t1 && t_equal t2' t2 then t else t_let u t1' t2'
   | Tcase (tl, bl) -> let tl' = List.map fnT tl in
       let tltl = List.for_all2 t_equal tl tl' in
-      let blbl,bl' = map_fold_left (t_branch fnT) true bl in
+      let blbl,bl' = map_fold_left (t_branch' fnT) true bl in
       if tltl && blbl then t else t_case tl' bl' t.t_ty
   | Teps b -> let u,f = f_open_bound b in let f' = fnF f in
       if f_equal f' f then t else t_eps u f')
@@ -959,7 +959,7 @@ let f_map fnT fnF f = f_label_copy f (match f.f_node with
       if t_equal t' t && f_equal f1' f1 then f else f_let u t' f1'
   | Fcase (tl, bl) -> let tl' = List.map fnT tl in
       let tltl = List.for_all2 t_equal tl tl' in
-      let blbl,bl' = map_fold_left (f_branch fnF) true bl in
+      let blbl,bl' = map_fold_left (f_branch' fnF) true bl in
       if tltl && blbl then f else f_case tl' bl')
 
 let protect fn t =
@@ -1522,3 +1522,35 @@ let f_let_simp v t f = match f.f_node with
 let f_equ_simp t1 t2 = if t_equal t1 t2 then f_true  else f_equ t1 t2
 let f_neq_simp t1 t2 = if t_equal t1 t2 then f_false else f_neq t1 t2
 
+let is_true_false f = match f.f_node with 
+  | Ftrue | Ffalse -> true | _  -> false
+
+(* Could we add an optional argument which toggle 
+   the simplification to the other map? *)
+let f_map_simp fnT fnF f = 
+  f_label_copy f 
+    (match f.f_node with
+       | Fapp (p, [t1;t2]) when ls_equal p ps_equ -> 
+           f_equ_simp (fnT t1) (fnT t2)
+       | Fapp (p, [t1;t2]) when ls_equal p ps_neq -> 
+           f_neq_simp (fnT t1) (fnT t2)
+       | Fapp (p, tl) -> f_app_unsafe p (List.map fnT tl)
+       | Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in
+         let f1' = fnF f1 in let tl' = tr_map fnT fnF tl in
+         if f_equal f1' f1 && trl_equal tl' tl && not (is_true_false f1) then f
+         else f_quant_simp q vl tl' f1'
+       | Fbinop (op, f1, f2) -> f_binary_simp op (fnF f1) (fnF f2)
+       | Fnot f1 -> f_not_simp (fnF f1)
+       | Ftrue | Ffalse -> f
+       | Fif (f1, f2, f3) -> f_if_simp (fnF f1) (fnF f2) (fnF f3)
+       | Flet (t, b) -> let u,f1 = f_open_bound b in
+         let t' = fnT t in let f1' = fnF f1 in
+         if t_equal t' t && f_equal f1' f1  && not (is_true_false f1) then f
+         else f_let_simp u t' f1'
+       | Fcase (tl, bl) -> let tl' = List.map fnT tl in
+         let tltl = List.for_all2 t_equal tl tl' in
+         let blbl,bl' = map_fold_left (f_branch' fnF) true bl in
+         if tltl && blbl then f else f_case tl' bl')
+  
+  
+let f_map_simp fnT = f_map_simp (protect fnT)

src/core/term.mli

@@ -318,6 +318,10 @@ val f_map_cont : ((term -> 'a) -> term -> 'a) ->
                  ((fmla -> 'a) -> fmla -> 'a) ->
                   (fmla -> 'a) -> fmla -> 'a
 
+(* simplification map *)
+val f_map_simp : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
+
+
 (* map/fold over free variables *)
 
 val t_v_map : (vsymbol -> term) -> term -> term

src/transform/simplify_formula.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
+open Decl
+
+let fmla_simpl f = f_map_simp (fun t -> t) (fun f -> f) f
+
+let decl_l d =
+  match d.d_node with
+    | Dprop (k,pr,f) -> 
+        let f = fmla_simpl f in
+        begin match f.f_node, k with
+          | Ftrue, Paxiom -> [[]]
+          | Ffalse, Paxiom -> []
+          | Ftrue, Pgoal -> []
+          | _ -> [[create_prop_decl k pr f]]
+        end
+    | _ -> [[decl_map (fun t -> t) fmla_simpl d]]
+
+let simplify_formula = Register.store (fun () -> Trans.decl_l decl_l None)
+
+
+let () = Register.register_transform_l "simplify_formula" simplify_formula

src/transform/simplify_formula.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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 simplify_formula :  Task.task list Register.trans_reg