simplify_trivial_quantifier va moins sous les triggers (il peut encore...

simplify_trivial_quantifier va moins sous les triggers (il peut encore remplacer dessous mais pas y trouver d'égalité)

Makefile.in

@@ -101,11 +101,10 @@ LIB_PARSER = ptree parser lexer denv typing
 LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 	     register prover whyconf
 
-LIB_TRANSFORM = simplify_recursive_definition inlining \
+LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
 		split_conjunction encoding_decorate \
 		eliminate_definition eliminate_algebraic \
-		eliminate_inductive eliminate_let eliminate_if\
-		simplify_formula
+		eliminate_inductive eliminate_let eliminate_if
 
 LIB_PRINTER = print_real alt_ergo why3 smt coq tptp
 

drivers/alt_ergo.drv

@@ -23,8 +23,10 @@ transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
 transformation "eliminate_if"
 transformation "eliminate_let"
+transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
+
 theory BuiltIn
   syntax type int "int"
   syntax type real "real"

drivers/cvc3.drv

@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
+transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 transformation "encoding_decorate"

drivers/why3_total_elimination.drv

@@ -7,6 +7,7 @@ transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
 transformation "eliminate_if"
 transformation "eliminate_let"
+transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 theory BuiltIn

drivers/z3.drv

@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
+transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 transformation "encoding_decorate"

src/driver/prover.ml

@@ -64,8 +64,7 @@ let print_task ?(debug=false) drv fmt task =
     try
       Register.apply_driver tr drv task 
     with e when not debug ->
-      Format.eprintf "failure in transformation %s: %s@." 
-	s (Printexc.to_string e);
+      Format.eprintf "failure in transformation %s@." s;
       raise e
   in
   let task = List.fold_left apply task transl in

src/main.ml

@@ -250,6 +250,9 @@ let rec report fmt = function
       Typing.report fmt e
   | Decl.UnknownIdent i ->
       fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
+  | Decl.UnboundVars vs ->
+      fprintf fmt "anomaly: unknown vars  [%a]" 
+        (Pp.print_iter1 Term.Svs.iter Pp.semi Pretty.print_vs) vs
   | Driver.Error e ->
       Driver.report fmt e
   | Config.Dynlink.Error e ->

src/transform/eliminate_inductive.ml

@@ -45,7 +45,8 @@ let inv acc (ps,al) =
   let tl = List.map t_var vl in
   let hd = f_app ps tl in
   let dj = Util.map_join_left (exi tl) f_or al in
-  let ax = f_forall vl [[Fmla hd]] (f_implies hd dj) in
+  let hsdj = Simplify_formula.fmla_remove_quant (f_implies hd dj) in 
+  let ax = f_forall vl [[Fmla hd]] hsdj in
   let nm = id_derive (ps.ls_name.id_string ^ "_inversion") ps.ls_name in
   create_prop_decl Paxiom (create_prsymbol nm) ax :: acc
 

src/transform/simplify_formula.ml

@@ -34,10 +34,17 @@ let decl_l d =
         end
     | _ -> [[decl_map (fun t -> t) fmla_simpl d]]
 
-let simplify_formula = Register.store (fun () -> Trans.decl_l decl_l None)
+let simplify_formula = Register.store 
+  (fun () -> Trans.rewrite (fun t -> t) fmla_simpl None)
 
+let simplify_formula_and_task = 
+  Register.store (fun () -> Trans.decl_l decl_l None)
 
-let () = Register.register_transform_l "simplify_formula" simplify_formula
+let () = Register.register_transform 
+  "simplify_formula" simplify_formula
+
+let () = Register.register_transform_l 
+  "simplify_formula_and_task" simplify_formula_and_task
 
 (** remove_trivial_quantification
     Original version in the alt-ergo prover by Sylvain Conchon *)
@@ -47,72 +54,82 @@ let () = Register.register_transform_l "simplify_formula" simplify_formula
 
 (** test if the freevariable of a term 
     are included in a given set *)
-let t_freevars_in fvars t =
+let t_boundvars_in fvars t =
   try
-    t_v_fold (fun () u -> if not (Svs.mem u fvars) then raise Exit) () t;
-    true
-  with Exit -> false
+    t_v_fold (fun () u -> if Svs.mem u fvars then raise Exit) () t;
+    false
+  with Exit -> true
 
 exception Subst_found of term
 
-let rec fmla_find_subst freevars var sign f =
-  let fnF = fmla_find_subst freevars var in
+let rec fmla_find_subst boundvars var sign f =
+  let fnF = fmla_find_subst boundvars var in
   match f.f_node with
-    | Fapp (ls,[{t_node=Tvar vs};t])
+    | Fapp (ls,[{t_node=Tvar vs} as tv;t])
         when sign && ls_equal ls ps_equ && vs_equal vs var 
-          && t_freevars_in freevars t ->
+          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
         raise (Subst_found t)
-    | Fapp (ls,[t;{t_node=Tvar vs}])         
+    | Fapp (ls,[t;{t_node=Tvar vs} as tv])         
         when sign && ls_equal ls ps_equ && vs_equal vs var 
-          && t_freevars_in freevars t ->
+          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
         raise (Subst_found t)
-    | Fapp (ls,[{t_node=Tvar vs};t])
+    | Fapp (ls,[{t_node=Tvar vs} as tv;t])
         when not sign && ls_equal ls ps_neq && vs_equal vs var 
-          && t_freevars_in freevars t ->
+          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
         raise (Subst_found t)
-    | Fapp (ls,[t;{t_node=Tvar vs}]) 
+    | Fapp (ls,[t;{t_node=Tvar vs} as tv]) 
         when not sign && ls_equal ls ps_neq && vs_equal vs var 
-          && t_freevars_in freevars t ->
+          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
         raise (Subst_found t)
     | Fbinop (For, f1, f2)  when not sign -> (fnF sign f1); (fnF sign f2) 
     | Fbinop (Fand, f1, f2) when sign ->  (fnF sign f1); (fnF sign f2)
     | Fbinop (Fimplies, f1, f2) when not sign -> 
         (fnF (not sign) f1); (fnF sign f2)
     | Fnot f1 -> fnF (not sign) f1
-    | Fbinop (Fiff, _, _) | Fif ( _, _, _) -> ()
-    | _ -> f_fold (fun () _ -> ()) (fun () -> fnF sign) () f
-
-let rec fmla_quant freevars sign f = function
-  | [] -> freevars, [], f
+    | Fquant (_,fb) ->
+        let vsl,trl,f' = f_open_quant fb in
+        if trl = [] 
+        then 
+          let boundvars = 
+            List.fold_left (fun s v -> Svs.add v s) boundvars vsl in
+          fmla_find_subst boundvars var sign f'
+    | Flet (_,fb) ->
+        let vs,f' = f_open_bound fb in
+        let boundvars = Svs.add vs boundvars in
+        fmla_find_subst boundvars var sign f'
+    | Fcase (_,fbs) ->
+        let iter_fb fb =
+          let patl,f = f_open_branch fb in
+          let boundvars = 
+            List.fold_left (fun s p -> pat_freevars s p) boundvars patl in
+          fmla_find_subst boundvars var sign f in
+        List.iter iter_fb fbs
+    | Fbinop (_, _, _) | Fif ( _, _, _) | Fapp _ | Ffalse | Ftrue-> ()
+
+let rec fmla_quant sign f = function
+  | [] -> [], f
   | vs::l -> 
-      let freevars, vsl, f = fmla_quant (Svs.add vs freevars) sign f l in
-      let freevars' = Svs.remove vs freevars in
+      let vsl, f = fmla_quant sign f l in
       try
-        fmla_find_subst freevars' vs sign f;
-        freevars, vs::vsl, f
+        fmla_find_subst Svs.empty vs sign f;
+        vs::vsl, f
       with Subst_found t ->
         let f = f_subst_single vs t f in
-        freevars', vsl, fmla_simpl f
+        vsl, fmla_simpl f
 
-let rec fmla_remove_quant freevars f =
+let rec fmla_remove_quant f =
   match f.f_node with
     | Fquant (k,fb) ->
-        let vsl,trl,f = f_open_quant fb in
-        let freevars, vsl, f = 
+        let vsl,trl,f' = f_open_quant fb in
           if trl <> [] 
-          then
-            let freevars = List.fold_left 
-              (fun acc vs -> Svs.add vs acc) freevars vsl in
-            freevars, vsl, f
+          then f
           else
             let sign = match k with
               | Fforall -> false | Fexists -> true in
-            fmla_quant freevars sign f vsl in
-        let f = fmla_remove_quant freevars f in
-        f_quant k vsl trl f
-    | _ -> f_map (fun t -> t) (fmla_remove_quant freevars) f
-
-let fmla_remove_quant = (fmla_remove_quant Svs.empty)
+            let vsl, f' = fmla_quant sign f' vsl in
+            let f' = fmla_remove_quant f' in
+            f_quant k vsl [] f'
+    | _ -> f_map (fun t -> t) fmla_remove_quant f
 
 (*let fmla_remove_quant f =
   Format.eprintf "@[<hov>%a =>|@\n" Pretty.print_fmla f;

src/transform/simplify_formula.mli

@@ -17,4 +17,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val simplify_formula :  Task.task list Register.trans_reg
+val fmla_simpl : Term.fmla -> Term.fmla
+
+val simplify_formula :  Task.task Register.trans_reg
+val simplify_formula_and_task :  Task.task list Register.trans_reg
+
+val fmla_remove_quant : Term.fmla -> Term.fmla