simplify_formula.ml 7.63 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
let rec fmla_simpl f = TermTF.t_map_simp (fun t -> t) fmla_simpl f
16 17 18

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

29
let simplify_formula = Trans.rewriteTF (fun t -> t) fmla_simpl None
30

31
let simplify_formula_and_task = Trans.decl_l decl_l None
32

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

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

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

exception Subst_found of term

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

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

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

(*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
121
let simplify_trivial_quantification =
122
  Trans.rewriteTF (fun t -> t) fmla_remove_quant None
123

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

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

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

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

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

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

177 178 179
    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
180 181 182 183

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