simplify_formula.ml 7.87 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(*    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

23
let rec fmla_simpl f = f_map_simp (fun t -> t) fmla_simpl f
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 29 30 31 32 33 34 35 36
        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]]

37
let simplify_formula = Trans.rewrite (fun t -> t) 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

Andrei Paskevich's avatar
Andrei Paskevich committed
44
let () = Trans.register_transform_l
45
  "simplify_formula_and_task" simplify_formula_and_task
46 47 48 49 50 51 52

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

exception Subst_found of term

63 64
let rec fmla_find_subst boundvars var sign f =
  let fnF = fmla_find_subst boundvars var in
65
  match f.f_node with
66
    | Fapp (ls,[{t_node=Tvar vs} as tv;t])
Andrei Paskevich's avatar
Andrei Paskevich committed
67 68
    | Fapp (ls,[t;{t_node=Tvar vs} as tv])
        when sign && ls_equal ls ps_equ && vs_equal vs var
69
          && not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
70
        raise (Subst_found t)
Andrei Paskevich's avatar
Andrei Paskevich committed
71
    | Fbinop (For, f1, f2)  when not sign -> (fnF sign f1); (fnF sign f2)
72
    | Fbinop (Fand, f1, f2) when sign ->  (fnF sign f1); (fnF sign f2)
Andrei Paskevich's avatar
Andrei Paskevich committed
73
    | Fbinop (Fimplies, f1, f2) when not sign ->
74 75
        (fnF (not sign) f1); (fnF sign f2)
    | Fnot f1 -> fnF (not sign) f1
76 77
    | Fquant (_,fb) ->
        let vsl,trl,f' = f_open_quant fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
78 79 80
        if trl = []
        then
          let boundvars =
81 82 83 84 85 86 87 88 89
            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
90
          let boundvars = patl.pat_vars in
91 92 93 94 95 96
          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
97
  | vs::l ->
98
      let vsl, f = fmla_quant sign f l in
99
      try
100
        fmla_find_subst (Svs.singleton vs) vs sign f;
101
        vs::vsl, f
102 103
      with Subst_found t ->
        let f = f_subst_single vs t f in
104
        vsl, fmla_simpl f
105

106
let rec fmla_remove_quant f =
107 108
  match f.f_node with
    | Fquant (k,fb) ->
109
        let vsl,trl,f',close = f_open_quant_cb fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
110
          if trl <> []
111
          then f
112 113 114
          else
            let sign = match k with
              | Fforall -> false | Fexists -> true in
115 116
            let vsl, f' = fmla_quant sign f' vsl in
            let f' = fmla_remove_quant f' in
117
            f_quant k (close vsl [] f')
118
    | _ -> f_map (fun t -> t) fmla_remove_quant f
119 120 121 122 123 124 125 126 127

(*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
128
let simplify_trivial_quantification =
129 130
  Trans.rewrite (fun t -> t) fmla_remove_quant None

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
137 138
let () = Trans.register_transform
  "simplify_trivial_quantification_in_goal"
139
   simplify_trivial_quantification_in_goal
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 146 147 148 149 150 151 152 153 154
  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
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 161 162 163 164 165 166 167 168 169 170 171 172 173
  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
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 187
let rec fmla_cond_subst filter f =
  let rec aux f =
188 189 190 191
    match f.f_node with
    | Fbinop (o, _, _) when o <> Fiff ->
        let conj = match o with
          Fand -> true | For | Fimplies -> false | Fiff -> 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 203 204 205 206
        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
207
          | Fapp (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 213 214
        fmla_unflatten conj f subf
    | _ -> f_map (fun t -> t) aux f in
  aux f