simplify_formula.ml 7.96 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(*    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 = TermTF.t_map_simp (fun t -> t) fmla_simpl f
24 25 26

let decl_l d =
  match d.d_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
27
    | Dprop (k,pr,f) ->
28
        let f = fmla_simpl f in
29
        begin match f.t_node, k with
30 31 32
          | Ttrue, Paxiom -> [[]]
          | Tfalse, Paxiom -> []
          | Ttrue, Pgoal -> []
33 34
          | _ -> [[create_prop_decl k pr f]]
        end
35
    | _ -> [[DeclTF.decl_map (fun t -> t) fmla_simpl d]]
36

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

39
let simplify_formula_and_task = Trans.decl_l decl_l None
40

Andrei Paskevich's avatar
Andrei Paskevich committed
41
let () = Trans.register_transform
42
  "simplify_formula" simplify_formula
43

Andrei Paskevich's avatar
Andrei Paskevich committed
44
let () = Trans.register_transform_l
45
  "simplify_formula_and_task" simplify_formula_and_task
46 47 48 49 50 51 52

(** 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] *)

Andrei Paskevich's avatar
Andrei Paskevich committed
53
(** test if the freevariable of a term
54
    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 66 67
  match f.t_node with
    | Tapp (ls,[{t_node=Tvar vs} as tv;t])
    | Tapp (ls,[t;{t_node=Tvar vs} as tv])
Andrei Paskevich's avatar
Andrei Paskevich committed
68
        when sign && ls_equal ls ps_equ && vs_equal vs var
69
          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
70
        raise (Subst_found t)
71 72 73
    | Tbinop (Tor, f1, f2)  when not sign -> (fnF sign f1); (fnF sign f2)
    | Tbinop (Tand, f1, f2) when sign ->  (fnF sign f1); (fnF sign f2)
    | Tbinop (Timplies, f1, f2) when not sign ->
74
        (fnF (not sign) f1); (fnF sign f2)
75 76 77
    | Tnot f1 -> fnF (not sign) f1
    | Tquant (_,fb) ->
        let vsl,trl,f' = t_open_quant fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
78 79 80
        if trl = []
        then
          let boundvars =
81 82
            List.fold_left (fun s v -> Svs.add v s) boundvars vsl in
          fmla_find_subst boundvars var sign f'
83
    | Tlet (_,fb) ->
84
        let vs,f' = t_open_bound fb in
85 86
        let boundvars = Svs.add vs boundvars in
        fmla_find_subst boundvars var sign f'
87
    | Tcase (_,fbs) ->
88
        let iter_fb fb =
89
          let patl,f = t_open_branch fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
90
          let boundvars = patl.pat_vars in
91 92
          fmla_find_subst boundvars var sign f in
        List.iter iter_fb fbs
93
    | Tbinop (_, _, _) | Tif ( _, _, _) | Tapp _ | Tfalse | Ttrue-> ()
94
    | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
95 96 97

let rec fmla_quant sign f = function
  | [] -> [], f
Andrei Paskevich's avatar
Andrei Paskevich committed
98
  | vs::l ->
99
      let vsl, f = fmla_quant sign f l in
100
      try
101
        fmla_find_subst (Svs.singleton vs) vs sign f;
102
        vs::vsl, f
103
      with Subst_found t ->
104
        let f = t_subst_single vs t f in
105
        vsl, fmla_simpl f
106

107
let rec fmla_remove_quant f =
108
  match f.t_node with
109 110
    | Tquant (k,fb) ->
        let vsl,trl,f',close = t_open_quant_cb fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
111
          if trl <> []
112
          then f
113 114
          else
            let sign = match k with
115
              | Tforall -> false | Texists -> true in
116 117
            let vsl, f' = fmla_quant sign f' vsl in
            let f' = fmla_remove_quant f' in
118
            t_quant k (close vsl [] f')
119
    | _ -> TermTF.t_map (fun t -> t) fmla_remove_quant f
120 121 122 123 124 125 126 127 128

(*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
*)

Andrei Paskevich's avatar
Andrei Paskevich committed
129
let simplify_trivial_quantification =
130
  Trans.rewriteTF (fun t -> t) fmla_remove_quant None
131

Andrei Paskevich's avatar
Andrei Paskevich committed
132
let () = Trans.register_transform
133
  "simplify_trivial_quantification" simplify_trivial_quantification
134

135
let simplify_trivial_quantification_in_goal =
136
  Trans.goal (fun pr f -> [create_prop_decl Pgoal pr (fmla_remove_quant f)])
137

Andrei Paskevich's avatar
Andrei Paskevich committed
138 139
let () = Trans.register_transform
  "simplify_trivial_quantification_in_goal"
140
   simplify_trivial_quantification_in_goal
141 142 143

(** linearize all the subformulas with the given connector (conj/disj);
    the returned array also contains the sign of each subformula *)
144
let fmla_flatten conj f =
145 146
  let terms = ref [] in
  let rec aux sign f =
147
    match f.t_node with
148 149
    | Tnot f -> aux (not sign) f
    | Tbinop (Tor, f1, f2) when sign <> conj ->
150
        aux sign f2; aux sign f1
151
    | Tbinop (Tand, f1, f2) when sign = conj ->
152
        aux sign f2; aux sign f1
153
    | Tbinop (Timplies, f1, f2) when sign <> conj ->
154 155
        aux sign f2; aux (not sign) f1
    | _ -> terms := (f, sign)::!terms in
156
  aux true f;
157 158 159
  Array.of_list !terms

(** recreate the structure of a given formula with linearized subformulas *)
160
let fmla_unflatten conj f formulas =
161
  let i = ref 0 in
162
  let rec aux sign f = t_label_copy f (match f.t_node with
163 164 165 166 167 168 169
    | Tnot f -> t_not (aux (not sign) f)
    | Tbinop (Tor, f1, f2) when sign <> conj ->
        let f1' = aux sign f1 in t_or f1' (aux sign f2)
    | Tbinop (Tand, f1, f2) when sign = conj ->
        let f1' = aux sign f1 in t_and f1' (aux sign f2)
    | Tbinop (Timplies, f1, f2) when sign <> conj ->
        let f1' = aux (not sign) f1 in t_implies f1' (aux sign f2)
170 171 172 173 174
    | _ ->
        let (t, s) = formulas.(!i) in
        assert (sign = s);
        incr i;
        t) in
175
  aux true f
176 177 178 179

(** substitute all the terms that appear as a side of an equality/disequality
    and that match the given filter

180 181 182
    equal terms can be substituted in all the terms of surrounding
    conjunctions, while disequal terms can be substituted in all the terms
    of surrounding disjunctions
183 184 185 186

    substitutions are not exported outside quantifiers (even if their free
    variables are untouched), so the transformation is possibly incomplete
    (but still correct) on formulas that have inner quantifiers *)
187 188
let rec fmla_cond_subst filter f =
  let rec aux f =
189
    match f.t_node with
190
    | Tbinop (o, _, _) when o <> Tiff ->
191
        let conj = match o with
192
          Tand -> true | Tor | Timplies -> false | Tiff -> assert false in
193
        let subf = fmla_flatten conj f in
194 195 196
        let subl = Array.length subf in
        for i = 0 to subl - 1 do
          let (f, s) = subf.(i) in
197
          subf.(i) <- (aux f, s);
198 199 200 201 202 203
        done;
        for i = 0 to subl - 1 do
          let do_subst t1 t2 =
            for j = 0 to subl - 1 do
              if j <> i then
                let (f, s) = subf.(j) in
204
                subf.(j) <- (t_replace t1 t2 f, s);
205 206
            done in
          let (f, s) = subf.(i) in
207 208
          match f.t_node with
          | Tapp (ls,[t1;t2]) when ls_equal ls ps_equ && s = conj ->
209 210 211 212
              if filter t1 t2 then do_subst t1 t2 else
              if filter t2 t1 then do_subst t2 t1
          | _ -> ()
        done;
213
        fmla_unflatten conj f subf
214
    | _ -> TermTF.t_map (fun t -> t) aux f in
215
  aux f