simplify_formula.ml 7.82 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12
open Ident
13 14 15
open Term
open Decl

16 17 18 19 20 21
let labset = Slab.of_list [keep_on_simp_label;asym_label]

let rec fmla_simpl f =
  let f = if Slab.disjoint f.t_label labset then f else
    t_label ?loc:f.t_loc (Slab.diff f.t_label labset) f in
  TermTF.t_map_simp t_fmla_simpl fmla_simpl f
22 23

and t_fmla_simpl t = TermTF.t_map t_fmla_simpl fmla_simpl t
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 t_fmla_simpl fmla_simpl d]]
36

37
let simplify_formula = Trans.rewriteTF t_fmla_simpl 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
  ~desc:"Simplify@ the@ formulas@ using@ propositional@ simplifications."
44

Andrei Paskevich's avatar
Andrei Paskevich committed
45
let () = Trans.register_transform_l
46
  "simplify_formula_and_task" simplify_formula_and_task
47
  ~desc:"Same as simplify_formula, but also@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
48
         remove@ axioms@ and@ goals@ that@ become@ trivial."
49 50 51 52 53 54 55

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

exception Subst_found of term

66 67
let rec fmla_find_subst boundvars var sign f =
  let fnF = fmla_find_subst boundvars var in
68 69 70
  let test ls vs t tv =
    sign && ls_equal ls ps_equ && vs_equal vs var &&
      not (t_equal t tv) && not (t_boundvars_in boundvars t) in
71 72
  match f.t_node with
    | Tapp (ls,[{t_node=Tvar vs} as tv;t])
73
        when test ls vs t tv -> raise (Subst_found t)
74
    | Tapp (ls,[t;{t_node=Tvar vs} as tv])
75
        when test ls vs t tv -> raise (Subst_found t)
76 77 78
    | 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 ->
79
        (fnF (not sign) f1); (fnF sign f2)
80 81 82
    | Tnot f1 -> fnF (not sign) f1
    | Tquant (_,fb) ->
        let vsl,trl,f' = t_open_quant fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
83 84 85
        if trl = []
        then
          let boundvars =
86 87
            List.fold_left (fun s v -> Svs.add v s) boundvars vsl in
          fmla_find_subst boundvars var sign f'
88
    | Tlet (_,fb) ->
89
        let vs,f' = t_open_bound fb in
90 91
        let boundvars = Svs.add vs boundvars in
        fmla_find_subst boundvars var sign f'
92 93
    | Tbinop (_, _, _) | Tif ( _, _, _)  | Tcase (_, _)
    | 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
    | _ -> Term.t_map 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.rewrite 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
  ~desc:"@[Simplify@ trivial@ quantifications:@]@\n  \
Andrei Paskevich's avatar
Andrei Paskevich committed
135 136 137
    @[\
     - @[transform \\exists x. x == y /\\ F@ into F[y/x],@]@\n\
     - @[transform \\forall x. x <> y \\/ F@ into F[y/x].@]@]"
138

139
let simplify_trivial_quantification_in_goal =
140
  Trans.goal (fun pr f -> [create_prop_decl Pgoal pr (fmla_remove_quant f)])
141

Andrei Paskevich's avatar
Andrei Paskevich committed
142 143
let () = Trans.register_transform
  "simplify_trivial_quantification_in_goal"
144
   simplify_trivial_quantification_in_goal
145
  ~desc:"Same@ as@ simplify_trivial_quantification, but@ only@ in@ goals."
146 147 148

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

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

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

185 186 187
    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
188 189 190 191

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