]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/TEMPI
Main code clean-up.
[helm.git] / helm / interface / TEMPI
1 prima di UriManager.ml:
2
3  [ABCI]* (terza passata, uguale alla seconda):
4
5    real 0m50.266s
6    user 0m44.160s
7    sys  0m0.700s
8
9 dopo UriManager.ml, ma prima di passare da = a ==:
10
11  [ABCI]* (terza passata, uguale alla seconda):
12
13    real 0m51.388s
14    user 0m45.430s
15    sys  0m0.530s
16
17 dopo UriManager.ml e popo il passaggio (parziale?) da = a ==:
18
19  [ABCI]* (terza passata, uguale alla seconda):
20
21    real 0m50.767s
22    user 0m44.750s
23    sys  0m0.510s
24
25 dopo il passaggio alla cache che usa ancora =:
26
27  [ABCI]* (terza passata, uguale alla seconda):
28
29    real 0m50.646s
30    user 0m44.680s
31    sys  0m0.530s
32
33 dopo il passaggio alla cache con utilizzo di ==:
34
35  [ABCI]* (terza passata, uguale alla seconda):
36
37    real 0m50.861s
38    user 0m45.030s
39    sys  0m0.500s
40
41 con funzione di hashing costante ;-(
42
43  [ABCI]* (terza passata, uguale alla seconda):
44
45    real 0m51.442s
46    user 0m45.440s
47    sys  0m0.530s
48
49 con implementazione isomorfa all'albero delle uri:
50
51  [ABCI]* (terza passata, uguale alla seconda):
52
53    real 0m54.081s
54    user 0m47.590s
55    sys  0m0.780s
56
57 con implementazione con doppio RB-albero:
58
59  [ABCI]* (terza passata, uguale alla seconda):
60
61    real 0m52.504s
62    user 0m46.120s
63    sys  0m0.720s
64
65 con implementazione semplice, gestite anche le uri delle var:
66
67  [ABCI]* (terza passata, uguale alla seconda):
68
69    real 0m51.850s
70    user 0m46.060s
71    sys  0m0.530s
72
73 con implementazione con doppio RB-albero, gestite anche le uri delle var:
74
75  [ABCI]* (terza passata, uguale alla seconda):
76
77    real 0m51.495s
78    user 0m45.660s
79    sys  0m0.540s
80
81 =========================================================
82
83 con implementazione con doppio RB-albero, gestite anche le uri delle var
84 e spostata nell'uri-manager is_prefix:
85
86  [ABCI]* (terza passata, uguale alla seconda):
87
88    real 0m50.465s
89    user 0m45.710s
90    sys  0m0.590s
91
92 con implementazione semplice (e tutto il resto):
93
94  [ABCI]* (terza passata, uguale alla seconda):
95
96    real 0m49.710s
97    user 0m43.850s
98    sys  0m0.500s
99
100 con implementazione banale (e tutto il resto):
101
102  [ABCI]* (terza passata, uguale alla seconda):
103
104    real 0m49.289s
105    user 0m44.840s
106    sys  0m0.570s
107
108 con implementazione banale SOLO PARSING ;-)
109
110  [ABCI]* (terza passata, uguale alla seconda):
111
112    real 0m48.395s
113    user 0m42.830s
114    sys  0m0.850s
115
116 =========================================================
117
118 con implementazione con doppio RB-albero, gestite anche le uri delle var
119 e spostata nell'uri-manager is_prefix:
120
121  REAL (prima passata, dopo un sync):
122
123    real 10m58.033s
124    user 10m37.690s
125    sys  0m2.570s
126
127 con implementazione semplice (e tutto il resto):
128
129  REAL (prima passata, dopo un sync):
130
131    real 10m31.035s
132    user 10m9.350s
133    sys  0m3.230s
134
135 con implementazione banale (e tutto il resto):
136
137  REAL (prima passata, dopo un sync):
138
139    real 11m4.026s
140    user 10m43.930s
141    sys  0m3.070s
142
143 =================================================
144
145 con implementazione banale, SOLO PARSING di tutto:
146
147    real 6m54.336s
148    user 6m13.850s
149    sys  0m6.580s
150
151 con implementazione banale, anche typechecking di tutto:
152
153    real 20m17.739s
154    user 19m14.740s
155    sys  0m8.550s
156
157 con implementazione semplice, anche typechecking di tutto:
158
159    real 19m36.079s
160    user 18m36.480s
161    sys  0m7.760s
162
163 con implementazione con doppio RB-albero, anche typechecking di tutto:
164
165    real 17m30.423s
166    user 16m30.840s
167    sys  0m6.170s
168
169 ***************************************************************************
170                          APPLICATA EURISTICA
171 ***************************************************************************
172
173 con implementazione con doppio RB-albero, anche typechecking di tutto
174 (universita') ????????:
175
176 real    5m37.805s
177 user    5m1.640s
178 sys     0m5.010s
179
180 tutto (ma a casa):
181
182 real    7m36.663s
183 user    6m52.220s
184 sys     0m5.860s
185
186
187 solo REAL:
188
189 real    2m52.860s
190 user    2m41.050s
191 sys     0m2.820s
192
193 ==========================================================================
194
195 tutto (ma a casa) dopo eliminazione buri:
196
197 real    7m52.773s
198 user    6m52.110s
199 sys     0m7.130s
200
201 "solo parsing" di tutto dopo eliminazione buri:
202
203 real    7m8.379s
204 user    6m15.250s
205 sys     0m6.700s
206
207 ===========================================================================
208
209 TUTTO ALL'UNIVERSITA' CON EURISTICA MA SENZA UNIVERSI:
210
211 real    5m47.920s
212 user    5m14.600s
213 sys     0m5.010s
214