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

24
let rec fmla_simpl f = TermTF.t_map_simp (fun t -> t) fmla_simpl f
25 26 27

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

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

40
let simplify_formula_and_task = Trans.decl_l decl_l None
41

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

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

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

exception Subst_found of term

64 65
let rec fmla_find_subst boundvars var sign f =
  let fnF = fmla_find_subst boundvars var in
66 67 68
  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
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)
Andrei Paskevich's avatar
Andrei Paskevich committed
72
    | Fbinop (For, f1, f2)  when not sign -> (fnF sign f1); (fnF sign f2)
73
    | Fbinop (Fand, f1, f2) when sign ->  (fnF sign f1); (fnF sign f2)
Andrei Paskevich's avatar
Andrei Paskevich committed
74
    | Fbinop (Fimplies, f1, f2) when not sign ->
75 76
        (fnF (not sign) f1); (fnF sign f2)
    | Fnot f1 -> fnF (not sign) f1
77 78
    | Fquant (_,fb) ->
        let vsl,trl,f' = f_open_quant fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
79 80 81
        if trl = []
        then
          let boundvars =
82 83
            List.fold_left (fun s v -> Svs.add v s) boundvars vsl in
          fmla_find_subst boundvars var sign f'
84
    | Tlet (_,fb) ->
85
        let vs,f' = t_open_bound fb in
86 87
        let boundvars = Svs.add vs boundvars in
        fmla_find_subst boundvars var sign f'
88
    | Tcase (_,fbs) ->
89
        let iter_fb fb =
90
          let patl,f = t_open_branch fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
91
          let boundvars = patl.pat_vars in
92 93
          fmla_find_subst boundvars var sign f in
        List.iter iter_fb fbs
94 95
    | Fbinop (_, _, _) | Tif ( _, _, _) | Tapp _ | Ffalse | Ftrue-> ()
    | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
96 97 98

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

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

(*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
130
let simplify_trivial_quantification =
131
  Trans.rewriteTF (fun t -> t) fmla_remove_quant None
132

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

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

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

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

(** recreate the structure of a given formula with linearized subformulas *)
161
let fmla_unflatten conj f formulas =
162
  let i = ref 0 in
163
  let rec aux sign f = t_label_copy f (match f.t_node with
164 165 166 167 168 169 170 171 172 173 174 175
    | Fnot f -> f_not (aux (not sign) f)
    | Fbinop (For, f1, f2) when sign <> conj ->
        let f1' = aux sign f1 in f_or f1' (aux sign f2)
    | Fbinop (Fand, f1, f2) when sign = conj ->
        let f1' = aux sign f1 in f_and f1' (aux sign f2)
    | Fbinop (Fimplies, f1, f2) when sign <> conj ->
        let f1' = aux (not sign) f1 in f_implies f1' (aux sign f2)
    | _ ->
        let (t, s) = formulas.(!i) in
        assert (sign = s);
        incr i;
        t) in
176
  aux true f
177 178 179 180

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

181 182 183
    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
184 185 186 187

    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 *)
188 189
let rec fmla_cond_subst filter f =
  let rec aux f =
190
    match f.t_node with
191 192 193
    | Fbinop (o, _, _) when o <> Fiff ->
        let conj = match o with
          Fand -> true | For | Fimplies -> false | Fiff -> assert false in
194
        let subf = fmla_flatten conj f in
195 196 197
        let subl = Array.length subf in
        for i = 0 to subl - 1 do
          let (f, s) = subf.(i) in
198
          subf.(i) <- (aux f, s);
199 200 201 202 203 204
        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
205
                subf.(j) <- (t_subst_term t1 t2 f, s);
206 207
            done in
          let (f, s) = subf.(i) in
208 209
          match f.t_node with
          | Tapp (ls,[t1;t2]) when ls_equal ls ps_equ && s = conj ->
210 211 212 213
              if filter t1 t2 then do_subst t1 t2 else
              if filter t2 t1 then do_subst t2 t1
          | _ -> ()
        done;
214
        fmla_unflatten conj f subf
215
    | _ -> TermTF.t_map (fun t -> t) aux f in
216
  aux f