simplify_formula.ml 5.6 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 38
let simplify_formula = Register.store 
  (fun () -> Trans.rewrite (fun t -> t) fmla_simpl None)
39

40 41
let simplify_formula_and_task = 
  Register.store (fun () -> Trans.decl_l decl_l None)
42

43 44 45 46 47
let () = Register.register_transform 
  "simplify_formula" simplify_formula

let () = Register.register_transform_l 
  "simplify_formula_and_task" simplify_formula_and_task
48 49 50 51 52 53 54 55 56

(** 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 *)
57
let t_boundvars_in fvars t =
58
  try
59 60 61
    t_v_fold (fun () u -> if Svs.mem u fvars then raise Exit) () t;
    false
  with Exit -> true
62 63 64

exception Subst_found of term

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

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

(*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 = 
  Register.store 
    (fun () -> Trans.rewrite (fun t -> t) fmla_remove_quant None)

let () = Register.register_transform 
  "simplify_trivial_quantification" simplify_trivial_quantification