split_conjunction.ml 5.84 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Ident
Francois Bobot's avatar
   
Francois Bobot committed
21
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
22
open Decl
Francois Bobot's avatar
   
Francois Bobot committed
23

24
25
26
27
28
let list_fold_product f acc l1 l2 =
  List.fold_left 
    (fun acc e1 ->
       List.fold_left 
         (fun acc e2 -> f acc e1 e2) 
29
         acc l2) 
30
    acc l1
Francois Bobot's avatar
   
Francois Bobot committed
31

32
let rec split_pos split_neg acc f =
33
34
  let split_pos acc f = 
    let p = split_pos split_neg acc f in
Francois Bobot's avatar
Francois Bobot committed
35
    (*Format.printf "@[<hov 2>f : %a@\n acc : %a :@\n %a@]@." 
36
37
      Pretty.print_fmla f
      (Pp.print_list Pp.semi Pretty.print_fmla) acc
Francois Bobot's avatar
Francois Bobot committed
38
      (Pp.print_list Pp.semi Pretty.print_fmla) p;*)
39
40
    p in

41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
  match f.f_node with
    | Ftrue -> acc
    | Ffalse -> f::acc
    | Fapp _ -> f::acc
    | Fbinop (Fand,f1,f2) -> split_pos (split_pos acc f2) f1
    | Fbinop (Fimplies,f1,f2) -> 
        list_fold_product 
          (fun acc f1 f2 ->  (f_implies f1 f2)::acc) 
          acc (split_neg [] f1) (split_pos [] f2)
    | Fbinop (Fiff,f1,f2) -> 
        split_pos (split_pos acc (f_implies f1 f2)) (f_implies f2 f1)
    | Fbinop (For,f1,f2) -> 
        list_fold_product 
          (fun acc f1 f2 ->  (f_or f1 f2)::acc) 
          acc (split_pos [] f1) (split_pos [] f2)
56
    | Fnot f -> List.fold_left (fun acc f -> f_not f::acc) acc (split_neg [] f)
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
    | Fif (fif,fthen,felse) -> 
        split_pos 
          (split_pos acc (f_implies fif fthen)) 
          (f_implies (f_not fif) felse)
    | Flet (t,fb) ->
        let vs,f = f_open_bound fb in
        List.fold_left (fun acc f -> (f_let vs t f)::acc) acc (split_pos [] f)
    | Fcase _ -> (* TODO better *) f::acc
    | Fquant (Fforall,fmlaq) ->
        let vsl,trl,fmla = f_open_quant fmlaq in
        List.fold_left (fun acc f -> 
                          (* TODO : Remove unused variable*)
                          (f_forall vsl trl f)::acc) acc (split_pos [] fmla)
    | Fquant (Fexists,_) -> f::acc

let rec split_neg split_pos acc f =
  let split_neg = split_neg split_pos in
  match f.f_node with
    | Ftrue -> f::acc
    | Ffalse -> acc
    | Fapp _ -> f::acc
    | Fbinop (Fand,f1,f2) -> 
        list_fold_product 
          (fun acc f1 f2 ->  (f_and f1 f2)::acc) 
          acc (split_neg [] f1) (split_neg [] f2)
82
    | Fbinop (Fimplies,f1,f2) -> split_pos (split_neg acc f2) (f_not f1)
83
    | Fbinop (Fiff,f1,f2) -> 
84
        split_neg (split_neg acc (f_and (f_not f1) (f_not f2))) (f_and f2 f1)
85
    | Fbinop (For,f1,f2) -> split_neg (split_neg acc f2) f1
86
    | Fnot f -> List.fold_left (fun acc f -> f_not f::acc) acc (split_pos [] f)
87
    | Fif (fif,fthen,felse) -> 
88
89
        split_neg (split_neg acc (f_and fif fthen))
          (f_and (f_not fif) felse)
90
91
92
93
94
95
96
97
98
99
100
    | Flet (t,fb) ->
        let vs,f = f_open_bound fb in
        List.fold_left (fun acc f -> (f_let vs t f)::acc) acc (split_neg [] f)
    | Fcase _ -> (* TODO better *) f::acc
    | Fquant (Fexists,fmlaq) ->
        let vsl,trl,fmla = f_open_quant fmlaq in
        List.fold_left (fun acc f -> 
                          (* TODO : Remove unused variable*)
                          (f_exists vsl trl f)::acc) acc (split_neg [] fmla)
    | Fquant (Fforall,_) -> f::acc

Francois Bobot's avatar
   
Francois Bobot committed
101

102
let elt is_split_kind split_pos d =
Francois Bobot's avatar
   
Francois Bobot committed
103
  match d.d_node with
104
    | Dprop (k,pr,f) when is_split_kind k ->
105
        let l = split_pos [] f in
106
107
108
109
110
111
112
        let l = List.map (fun p -> create_prop_decl k 
                            (create_prsymbol (id_clone pr.pr_name)) p) l in
        begin match k with
          | Pgoal -> List.map (fun p -> [p]) l
          | Paxiom -> [l]
          | _ -> assert false
        end
113
    | _ -> [[d]]
Francois Bobot's avatar
   
Francois Bobot committed
114

115
116
117
118
119
let is_split_goal = function Pgoal -> true | _ -> false
let is_split_axiom = function Paxiom -> true | _ -> false
let is_split_all = function _ -> true

let t isk fsp = Register.store (fun () -> Trans.decl_l (elt isk fsp) None)
Francois Bobot's avatar
   
Francois Bobot committed
120

121
122
123
124
125
let split_pos1 = split_pos (fun acc x -> x::acc)

let rec split_pos2 acc d = split_pos split_neg2 acc d
and split_neg2 acc d = split_neg split_pos2 acc d

126
127
128
129
130
131
let split_pos_goal = t is_split_goal split_pos1
let split_pos_neg_goal = t is_split_goal split_pos2
let split_pos_axiom = t is_split_axiom split_pos1
let split_pos_neg_axiom = t is_split_axiom split_pos2
let split_pos_all = t is_split_all split_pos1
let split_pos_neg_all = t is_split_all split_pos2
132

133
134
135
136
137
138
139
140
141
142
143
144
let () = Driver.register_transform_l 
  "split_goal_pos_goal" split_pos_goal
let () = Driver.register_transform_l 
  "split_goal_pos_neg_goal" split_pos_neg_goal
let () = Driver.register_transform_l 
  "split_goal_pos_axiom" split_pos_axiom
let () = Driver.register_transform_l 
  "split_goal_pos_neg_axiom" split_pos_neg_axiom
let () = Driver.register_transform_l 
  "split_goal_pos_all" split_pos_all
let () = Driver.register_transform_l 
  "split_goal_pos_neg_all" split_pos_neg_all