simplify_formula.ml 8.46 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7
(*    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
          | Ttrue, Paxiom -> [[]]
          | Tfalse, Paxiom -> []
          | Ttrue, Pgoal -> []
34 35
          | _ -> [[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
  ~desc:"Simplify@ the@ formulas@ using@ propositional@ simplifications."
45

Andrei Paskevich's avatar
Andrei Paskevich committed
46
let () = Trans.register_transform_l
47
  "simplify_formula_and_task" simplify_formula_and_task
48 49
  ~desc:"Same as simplify_formula, but also@ \
         removes@ axioms@ and@ goals@ that@ become@ trivial."
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] *)

Andrei Paskevich's avatar
Andrei Paskevich committed
57
(** test if the freevariable of a term
58
    are included in a given set *)
59
let t_boundvars_in fvars t =
60
  try
61 62 63
    t_v_fold (fun () u -> if Svs.mem u fvars then raise Exit) () t;
    false
  with Exit -> true
64 65 66

exception Subst_found of term

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

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

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

(*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
133
let simplify_trivial_quantification =
134
  Trans.rewriteTF (fun t -> t) fmla_remove_quant None
135

Andrei Paskevich's avatar
Andrei Paskevich committed
136
let () = Trans.register_transform
137
  "simplify_trivial_quantification" simplify_trivial_quantification
138 139 140 141
  ~desc:"@[Simplify@ trivial@ quantifications:@]@\n  \
@[\
 - @[transform \\exists x. x == y /\\ F@ into F[y/x],@]@\n\
 - @[transform \\forall x. x <> y \\/ F@ into F[y/x].@]@]"
142

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

Andrei Paskevich's avatar
Andrei Paskevich committed
146 147
let () = Trans.register_transform
  "simplify_trivial_quantification_in_goal"
148
   simplify_trivial_quantification_in_goal
149
  ~desc:"Same@ as@ simplify_trivial_quantification, but@ only@ in@ goals."
150 151 152

(** linearize all the subformulas with the given connector (conj/disj);
    the returned array also contains the sign of each subformula *)
153
let fmla_flatten conj f =
154 155
  let terms = ref [] in
  let rec aux sign f =
156
    match f.t_node with
157 158
    | Tnot f -> aux (not sign) f
    | Tbinop (Tor, f1, f2) when sign <> conj ->
159
        aux sign f2; aux sign f1
160
    | Tbinop (Tand, f1, f2) when sign = conj ->
161
        aux sign f2; aux sign f1
162
    | Tbinop (Timplies, f1, f2) when sign <> conj ->
163 164
        aux sign f2; aux (not sign) f1
    | _ -> terms := (f, sign)::!terms in
165
  aux true f;
166 167 168
  Array.of_list !terms

(** recreate the structure of a given formula with linearized subformulas *)
169
let fmla_unflatten conj f formulas =
170
  let i = ref 0 in
171
  let rec aux sign f = t_label_copy f (match f.t_node with
172 173 174 175 176 177 178
    | 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)
179 180 181 182 183
    | _ ->
        let (t, s) = formulas.(!i) in
        assert (sign = s);
        incr i;
        t) in
184
  aux true f
185 186 187 188

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

189 190 191
    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
192 193 194 195

    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 *)
196
let fmla_cond_subst filter f =
197
  let rec aux f =
198
    match f.t_node with
199
    | Tbinop (o, _, _) when o <> Tiff ->
200
        let conj = match o with
201
          Tand -> true | Tor | Timplies -> false | Tiff -> assert false in
202
        let subf = fmla_flatten conj f in
203 204 205
        let subl = Array.length subf in
        for i = 0 to subl - 1 do
          let (f, s) = subf.(i) in
206
          subf.(i) <- (aux f, s);
207 208 209 210 211 212
        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
213
                subf.(j) <- (t_replace_alpha t1 t2 f, s);
214 215
            done in
          let (f, s) = subf.(i) in
216 217
          match f.t_node with
          | Tapp (ls,[t1;t2]) when ls_equal ls ps_equ && s = conj ->
218 219 220 221
              if filter t1 t2 then do_subst t1 t2 else
              if filter t2 t1 then do_subst t2 t1
          | _ -> ()
        done;
222
        fmla_unflatten conj f subf
223
    | _ -> TermTF.t_map (fun t -> t) aux f in
224
  aux f