simplify_formula.ml 7.64 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   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 13 14

open Term
open Decl

15 16 17
let rec fmla_simpl f = TermTF.t_map_simp t_fmla_simpl fmla_simpl f

and t_fmla_simpl t = TermTF.t_map t_fmla_simpl fmla_simpl t
18 19 20

let decl_l d =
  match d.d_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
21
    | Dprop (k,pr,f) ->
22
        let f = fmla_simpl f in
23
        begin match f.t_node, k with
24 25 26
          | Ttrue, Paxiom -> [[]]
          | Tfalse, Paxiom -> []
          | Ttrue, Pgoal -> []
27 28
          | _ -> [[create_prop_decl k pr f]]
        end
29
    | _ -> [[DeclTF.decl_map t_fmla_simpl fmla_simpl d]]
30

31
let simplify_formula = Trans.rewriteTF t_fmla_simpl fmla_simpl None
32

33
let simplify_formula_and_task = Trans.decl_l decl_l None
34

Andrei Paskevich's avatar
Andrei Paskevich committed
35
let () = Trans.register_transform
36
  "simplify_formula" simplify_formula
37
  ~desc:"Simplify@ the@ formulas@ using@ propositional@ simplifications."
38

Andrei Paskevich's avatar
Andrei Paskevich committed
39
let () = Trans.register_transform_l
40
  "simplify_formula_and_task" simplify_formula_and_task
41
  ~desc:"Same as simplify_formula, but also@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
42
         remove@ axioms@ and@ goals@ that@ become@ trivial."
43 44 45 46 47 48 49

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

exception Subst_found of term

60 61
let rec fmla_find_subst boundvars var sign f =
  let fnF = fmla_find_subst boundvars var in
62 63 64
  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
65 66
  match f.t_node with
    | Tapp (ls,[{t_node=Tvar vs} as tv;t])
67
        when test ls vs t tv -> raise (Subst_found t)
68
    | Tapp (ls,[t;{t_node=Tvar vs} as tv])
69
        when test ls vs t tv -> raise (Subst_found t)
70 71 72
    | 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 ->
73
        (fnF (not sign) f1); (fnF sign f2)
74 75 76
    | Tnot f1 -> fnF (not sign) f1
    | Tquant (_,fb) ->
        let vsl,trl,f' = t_open_quant fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
77 78 79
        if trl = []
        then
          let boundvars =
80 81
            List.fold_left (fun s v -> Svs.add v s) boundvars vsl in
          fmla_find_subst boundvars var sign f'
82
    | Tlet (_,fb) ->
83
        let vs,f' = t_open_bound fb in
84 85
        let boundvars = Svs.add vs boundvars in
        fmla_find_subst boundvars var sign f'
86 87
    | Tbinop (_, _, _) | Tif ( _, _, _)  | Tcase (_, _)
    | Tapp _ | Tfalse | Ttrue -> ()
88
    | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
89 90 91

let rec fmla_quant sign f = function
  | [] -> [], f
Andrei Paskevich's avatar
Andrei Paskevich committed
92
  | vs::l ->
93
      let vsl, f = fmla_quant sign f l in
94
      try
95
        fmla_find_subst (Svs.singleton vs) vs sign f;
96
        vs::vsl, f
97
      with Subst_found t ->
98
        let f = t_subst_single vs t f in
99
        vsl, fmla_simpl f
100

101
let rec fmla_remove_quant f =
102
  match f.t_node with
103 104
    | Tquant (k,fb) ->
        let vsl,trl,f',close = t_open_quant_cb fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
105
          if trl <> []
106
          then f
107 108
          else
            let sign = match k with
109
              | Tforall -> false | Texists -> true in
110 111
            let vsl, f' = fmla_quant sign f' vsl in
            let f' = fmla_remove_quant f' in
112
            t_quant k (close vsl [] f')
113
    | _ -> Term.t_map fmla_remove_quant f
114 115 116 117 118 119 120 121 122

(*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
123
let simplify_trivial_quantification =
124
  Trans.rewrite fmla_remove_quant None
125

Andrei Paskevich's avatar
Andrei Paskevich committed
126
let () = Trans.register_transform
127
  "simplify_trivial_quantification" simplify_trivial_quantification
128
  ~desc:"@[Simplify@ trivial@ quantifications:@]@\n  \
Andrei Paskevich's avatar
Andrei Paskevich committed
129 130 131
    @[\
     - @[transform \\exists x. x == y /\\ F@ into F[y/x],@]@\n\
     - @[transform \\forall x. x <> y \\/ F@ into F[y/x].@]@]"
132

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

Andrei Paskevich's avatar
Andrei Paskevich committed
136 137
let () = Trans.register_transform
  "simplify_trivial_quantification_in_goal"
138
   simplify_trivial_quantification_in_goal
139
  ~desc:"Same@ as@ simplify_trivial_quantification, but@ only@ in@ goals."
140 141 142

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

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

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

179 180 181
    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
182 183 184 185

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