simplify_formula.ml 7.95 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 = f_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 30 31 32 33 34 35 36 37
        let f = fmla_simpl f in
        begin match f.f_node, k with
          | Ftrue, Paxiom -> [[]]
          | Ffalse, Paxiom -> []
          | Ftrue, Pgoal -> []
          | _ -> [[create_prop_decl k pr f]]
        end
    | _ -> [[decl_map (fun t -> t) fmla_simpl d]]

38
let simplify_formula = Trans.rewrite (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
  match f.f_node with
67
    | Fapp (ls,[{t_node=Tvar vs} as tv;t])
Andrei Paskevich's avatar
Andrei Paskevich committed
68 69
    | Fapp (ls,[t;{t_node=Tvar vs} as tv])
        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 84 85 86 87 88 89 90
            List.fold_left (fun s v -> Svs.add v s) boundvars vsl in
          fmla_find_subst boundvars var sign f'
    | Flet (_,fb) ->
        let vs,f' = f_open_bound fb in
        let boundvars = Svs.add vs boundvars in
        fmla_find_subst boundvars var sign f'
    | Fcase (_,fbs) ->
        let iter_fb fb =
          let patl,f = f_open_branch fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
91
          let boundvars = patl.pat_vars in
92 93 94 95 96 97
          fmla_find_subst boundvars var sign f in
        List.iter iter_fb fbs
    | Fbinop (_, _, _) | Fif ( _, _, _) | Fapp _ | Ffalse | Ftrue-> ()

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 104
      with Subst_found t ->
        let f = f_subst_single vs t f in
105
        vsl, fmla_simpl f
106

107
let rec fmla_remove_quant f =
108 109
  match f.f_node with
    | Fquant (k,fb) ->
110
        let vsl,trl,f',close = f_open_quant_cb fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
111
          if trl <> []
112
          then f
113 114 115
          else
            let sign = match k with
              | Fforall -> false | Fexists -> true in
116 117
            let vsl, f' = fmla_quant sign f' vsl in
            let f' = fmla_remove_quant f' in
118
            f_quant k (close vsl [] f')
119
    | _ -> f_map (fun t -> t) 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 131
  Trans.rewrite (fun t -> t) fmla_remove_quant None

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

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

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

(** linearize all the subformulas with the given connector (conj/disj);
    the returned array also contains the sign of each subformula *)
144
let fmla_flatten conj f =
145 146 147 148 149 150 151 152 153 154 155
  let terms = ref [] in
  let rec aux sign f =
    match f.f_node with
    | 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
156
  aux true f;
157 158 159
  Array.of_list !terms

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

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

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

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