1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
(**************************************************************************)
(* *)
(* The Why platform for program certification *)
(* Copyright (C) 2002-2008 *)
(* Romain BARDOU *)
(* Jean-Franois COUCHOT *)
(* Mehdi DOGGUY *)
(* Jean-Christophe FILLITRE *)
(* Thierry HUBERT *)
(* Claude MARCH *)
(* Yannick MOY *)
(* Christine PAULIN *)
(* Yann RGIS-GIANAS *)
(* Nicolas ROUSSET *)
(* Xavier URBAIN *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU General Public *)
(* License version 2, as published by the Free Software Foundation. *)
(* *)
(* 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. *)
(* *)
(* See the GNU General Public License version 2 for more details *)
(* (enclosed in the file GPL). *)
(* *)
(**************************************************************************)
open Options
open Marshal
open Digest
open Logic
open Cc
let flags = []
let max_size = ref 5000 (* maximum cache size *)
let cache = ref (Hashtbl.create 97)
let source_file = ref "/tmp/gwhy.cache"
let active = ref true
let obligs = ref true
let ok = ref true
let enable () = active := true
let disable () = active := false
let set_active v = active := v
let swap_active () = active := not !active
let is_enabled () = !active
let swap_hard_proof () = obligs := not !obligs
let set_hard_proof v = obligs := v
let hard_proof () = !obligs
let exists p o =
try
Queue.iter
(fun pr -> if p = pr then raise Exit)
(Hashtbl.find !cache o);
false
with Exit -> true
let read_cache () =
try
let in_channel = open_in !source_file in
cache := from_channel in_channel
with
| Sys_error s ->
print_endline (" [...] Sys_error : "^s);
flush stdout
| End_of_file ->
print_endline (" [...] cache empty !");
flush stdout
| _ ->
print_endline (" [...] error while loading cache !");
flush stdout
let clean seq =
let (ctx, p) = seq.Env.scheme_type in
let rec clean0 = function
| Pvar _ | Papp (_, _, _) | Pfpi (_,_,_) | Ptrue | Pfalse as p -> p
| Pimplies (i, p1, p2) ->
Pimplies (i, clean0 p1, clean0 p2)
| Pif (t, p1, p2) ->
Pif (t, clean0 p1, clean0 p2)
| Pand (wp, sym, p1, p2) ->
Pand (wp, sym, clean0 p1, clean0 p2)
| Por (p1, p2) ->
Por (clean0 p1, clean0 p2)
| Piff (p1, p2) ->
Piff (clean0 p1, clean0 p2)
| Pnot p ->
Pnot (clean0 p)
| Forall (wp, id1, id2, pt, tl, p) ->
Forall (wp, id1, id2, pt, tl, clean0 p)
| Forallb (wp, p1, p2) ->
Forallb (wp, clean0 p1, clean0 p2)
| Exists (id1, id2, pt, p) ->
Exists (id1, id2, pt, clean0 p)
| Pnamed (_, p) ->
clean0 p
and clean1 = function
| Svar _ as c -> c
| Spred (id, p) -> Spred (id, clean0 p)
in
(List.map clean1 ctx, clean0 p)
let fool () = Hashtbl.length !cache > !max_size
(* i mean fool ... cache doesn't want to do his job *)
let is_full = ref false
let load_cache source =
source_file := source;
if not (Sys.file_exists !source_file) then
begin
let xc = Sys.command ("touch " ^ source) in
if xc <> 0 then
begin
ok := false;
print_endline (" [...] Error : cannot create cache file "^source^" !");
flush stdout;
end
end;
if !ok then read_cache ();
is_full := fool ()
let save () =
let out_channel = open_out_bin !source_file in
to_channel out_channel !cache flags;
close_out out_channel
let clear () =
Hashtbl.clear !cache;
save ()
let remove x = Hashtbl.remove !cache x
let in_cache x = Hashtbl.mem !cache x
let find x = Hashtbl.find !cache x
let is_empty () = Hashtbl.length !cache = 0
let o_in_cache o = let (_,_,seq) = o in in_cache seq
let add (seq:Cc.sequent Env.scheme) (prover:string) =
let o = clean seq in
if not !is_full then begin
if in_cache o then
begin
if not (exists prover o) then
Queue.add prover (Hashtbl.find !cache o)
end
else
begin
let q = Queue.create () in
let _ = Queue.add prover q in
Hashtbl.add !cache o q;
is_full := fool ()
end
end;
save () (* actually, must be done when exiting gui *)
|
