simplify_formula.ml 5.7 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(**************************************************************************)
(*                                                                        *)
(*  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

23
let rec fmla_simpl f = f_map_simp (fun t -> t) fmla_simpl f
24 25 26 27 28 29 30 31 32 33 34 35 36

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]]

37
let simplify_formula = Trans.rewrite (fun t -> t) fmla_simpl None
38

39
let simplify_formula_and_task = Trans.decl_l decl_l None
40

41
let () = Trans.register_transform 
42
  "simplify_formula" simplify_formula
43

44
let () = Trans.register_transform_l 
45
  "simplify_formula_and_task" simplify_formula_and_task
46 47 48 49 50 51 52 53 54

(** remove_trivial_quantification
    Original version in the alt-ergo prover by Sylvain Conchon *)

(** transform \exists x. x == y /\ F into F[y/x] *)
(** transform \forall x. x <> y \/ F into F[y/x] *)

(** test if the freevariable of a term 
    are included in a given set *)
55
let t_boundvars_in fvars t =
56
  try
57 58 59
    t_v_fold (fun () u -> if Svs.mem u fvars then raise Exit) () t;
    false
  with Exit -> true
60 61 62

exception Subst_found of term

63 64
let rec fmla_find_subst boundvars var sign f =
  let fnF = fmla_find_subst boundvars var in
65
  match f.f_node with
66
    | Fapp (ls,[{t_node=Tvar vs} as tv;t])
67
        when sign && ls_equal ls ps_equ && vs_equal vs var 
68
          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
69
        raise (Subst_found t)
70
    | Fapp (ls,[t;{t_node=Tvar vs} as tv])         
71
        when sign && ls_equal ls ps_equ && vs_equal vs var 
72
          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
73
        raise (Subst_found t)
74
    | Fapp (ls,[{t_node=Tvar vs} as tv;t])
75
        when not sign && ls_equal ls ps_neq && vs_equal vs var 
76
          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
77
        raise (Subst_found t)
78
    | Fapp (ls,[t;{t_node=Tvar vs} as tv]) 
79
        when not sign && ls_equal ls ps_neq && vs_equal vs var 
80
          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
81 82 83 84 85 86
        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
87 88 89 90 91 92 93 94 95 96 97 98 99 100
    | 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
Andrei Paskevich's avatar
Andrei Paskevich committed
101
          let boundvars = patl.pat_vars in 
102 103 104 105 106 107
          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
108
  | vs::l -> 
109
      let vsl, f = fmla_quant sign f l in
110
      try
111
        fmla_find_subst (Svs.singleton vs) vs sign f;
112
        vs::vsl, f
113 114
      with Subst_found t ->
        let f = f_subst_single vs t f in
115
        vsl, fmla_simpl f
116

117
let rec fmla_remove_quant f =
118 119
  match f.f_node with
    | Fquant (k,fb) ->
120
        let vsl,trl,f' = f_open_quant fb in
121
          if trl <> [] 
122
          then f
123 124 125
          else
            let sign = match k with
              | Fforall -> false | Fexists -> true in
126 127 128 129
            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
130 131 132 133 134 135 136 137 138 139

(*let fmla_remove_quant f =
  Format.eprintf "@[<hov>%a =>|@\n" Pretty.print_fmla f;
  let f = fmla_remove_quant f in
  Format.eprintf "|=>%a@]@.@." Pretty.print_fmla f;
  Pretty.forget_all ();
  f
*)

let simplify_trivial_quantification = 
140 141 142
  Trans.rewrite (fun t -> t) fmla_remove_quant None

let () = Trans.register_transform 
143
  "simplify_trivial_quantification" simplify_trivial_quantification
144

145
let simplify_trivial_quantification_in_goal =
146
  Trans.goal (fun pr f -> [create_prop_decl Pgoal pr (fmla_remove_quant f)])
147

148
let () = Trans.register_transform 
149
  "simplify_trivial_quantification_in_goal" 
150
   simplify_trivial_quantification_in_goal