-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathstats.c
252 lines (208 loc) · 8.42 KB
/
stats.c
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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
/* File inherited from EQP0.9c and adapted for the */
/* MODIFIED CLAUSE DIFFUSION distributed prover Peers_mcd */
#include "Header.h"
#include "Stats.h"
/* following are for memory stats */
#include "Term.h"
#include "Symbols.h"
#include "List.h"
#include "Unify.h"
#include "Clause.h"
#include "Discrim.h"
#include "Fpa.h"
#include "Ac.h"
#include "Paramod.h"
#include "Heuristic.h"
long Stats[MAX_STATS];
struct clock Clocks[MAX_CLOCKS];
int Internal_flags[MAX_INTERNAL_FLAGS];
/*************
*
* init_stats()
*
*************/
void init_stats()
{
int i;
init_clocks();
for (i = 0; i < MAX_INTERNAL_FLAGS; i++)
Internal_flags[i] = 0;
for (i = 0; i < MAX_STATS; i++)
Stats[i] = 0;
Stats[INIT_WALL_SECONDS] = wall_seconds();
} /* init_stats */
/*************
*
* print_mem()
*
*************/
void print_mem(FILE *fp)
{
fprintf(fp, "\n------------- memory usage ------------\n");
fprintf(fp, "Memory dynamically allocated (tp_alloc): %d.\n", total_mem());
print_symbols_mem(fp, 1);
print_term_mem(fp, 0);
print_list_mem(fp, 0);
print_unify_mem(fp, 0);
print_ac_mem(fp, 0);
print_discrim_mem(fp, 0);
print_fpa_mem(fp, 0);
print_clause_mem(fp, 0);
print_clause_pair_mem(fp, 0);
} /* print_mem */
/*************
*
* p_mem
*
*************/
void p_mem(void)
{
print_mem(stdout);
} /* p_mem */
/*************
*
* print_stats(fp)
*
*************/
void print_stats(FILE *fp)
{
fprintf(fp, "\n-------------- statistics -------------\n");
#if 0
fprintf(fp, "Input errors %7ld\n", Stats[INPUT_ERRORS]);
fprintf(fp, "BT occur checks %7ld\n", Stats[BT_OCCUR_CHECKS]);
fprintf(fp, "AC initiations %7ld\n", Stats[AC_INITIATIONS]);
fprintf(fp, "AC continuations %7ld\n", Stats[AC_CONTINUATIONS]);
fprintf(fp, "\n");
#endif
fprintf(fp, "Clauses input %7ld\n", Stats[CLAUSES_INPUT]);
fprintf(fp, " Usable input %7ld\n", Stats[USABLE_INPUT]);
fprintf(fp, " Sos input %7ld\n", Stats[SOS_INPUT]);
fprintf(fp, " Demodulators input %7ld\n", Stats[DEMODULATORS_INPUT]);
fprintf(fp, " Passive input %7ld\n", Stats[PASSIVE_INPUT]);
fprintf(fp, "\n");
fprintf(fp, "Processed BS (before search)%4ld\n", Stats[CLAUSES_GENERATED_INPUT]);
fprintf(fp, "Forward subsumed BS %7ld\n", Stats[CLAUSES_FORWARD_SUBSUMED_INPUT]);
fprintf(fp, "Kept BS %7ld\n", Stats[CLAUSES_KEPT_INPUT]);
fprintf(fp, "New demodulators BS %7ld\n", Stats[NEW_DEMODULATORS_INPUT]);
fprintf(fp, "Back demodulated BS %7ld\n", Stats[CLAUSES_BACK_DEMODULATED_INPUT]);
fprintf(fp, "\n");
fprintf(fp, "Clauses or pairs given %7ld\n", Stats[GIVEN]);
fprintf(fp, "Clauses generated %7ld\n", Stats[CLAUSES_GENERATED]);
fprintf(fp, "Forward subsumed %7ld\n", Stats[CLAUSES_FORWARD_SUBSUMED]);
fprintf(fp, "Deleted by weight %7ld\n", Stats[CLAUSES_WT_DELETE]);
fprintf(fp, "Deleted by variable count%7ld\n", Stats[CLAUSES_VAR_DELETE]);
fprintf(fp, "Kept %7ld\n", Stats[CLAUSES_KEPT]);
fprintf(fp, "New demodulators %7ld\n", Stats[NEW_DEMODULATORS]);
fprintf(fp, "Back demodulated %7ld\n", Stats[CLAUSES_BACK_DEMODULATED]);
fprintf(fp, "Ordered paramod prunes %7ld\n", Stats[ORDERED_PARAMOD_PRUNES]);
fprintf(fp, "Basic paramod prunes %7ld\n", Stats[BASIC_PARAMOD_PRUNES]);
fprintf(fp, "Prime paramod prunes %7ld\n", Stats[PRIME_PARAMOD_PRUNES]);
fprintf(fp, "Semantic prunes %7ld\n", Stats[SEMANTIC_PARAMOD_PRUNES]);
fprintf(fp, "\n");
fprintf(fp, "Rewrite attempts %7ld\n", Stats[REWRITE_ATTEMPTS]);
fprintf(fp, "Rewrites %7ld\n", Stats[REWRITES]);
fprintf(fp, "\n");
fprintf(fp, "FPA overloads %7ld\n", Stats[FPA_OVERLOADS]);
fprintf(fp, "FPA underloads %7ld\n", Stats[FPA_UNDERLOADS]);
fprintf(fp, "\n");
fprintf(fp, "Usable size %7ld\n", Stats[USABLE_SIZE]);
fprintf(fp, "Sos size %7ld\n", Stats[SOS_SIZE]);
fprintf(fp, "Demodulators size %7ld\n", Stats[DEMODULATORS_SIZE]);
fprintf(fp, "Passive size %7ld\n", Stats[PASSIVE_SIZE]);
fprintf(fp, "Disabled size %7ld\n", Stats[DISABLED_SIZE]);
fprintf(fp, "\n");
fprintf(fp, "Proofs found %7ld\n", Stats[PROOFS]);
fprintf(fp, "\n");
/* Peers_mcd -- October 1996 */
fprintf(fp, "Residents %7ld\n", Stats[RESIDENTS]);
fprintf(fp, "Visitors %7ld\n", Stats[VISITORS]);
fprintf(fp, "Residents in SOS %7ld\n", Stats[RESIDENTS_IN_SOS]);
fprintf(fp, "Visitors in SOS %7ld\n", Stats[VISITORS_IN_SOS]);
fprintf(fp, "Generated by expansion %7ld\n", Stats[EXP_GENERATED]);
fprintf(fp, "Inference msgs broadcast %7ld\n", Stats[IM_BROADCAST]);
fprintf(fp, "Inference msgs received %7ld\n", Stats[IM_RECEIVED]);
fprintf(fp, "Residents back demod %7ld\n", Stats[BD_RESIDENTS]);
fprintf(fp, "Visitors back demod %7ld\n", Stats[BD_VISITORS]);
if (Stats[PROOFS] > 0)
fprintf(fp, "PROOF LENGTH %7ld\n", Stats[PROOF_LENGTH]);
else
fprintf(fp, "Proof length %7ld\n", Stats[PROOF_LENGTH]);
/* Peers-mcd, November 1996: to use grep LENGTH to extract the proof */
/* length from the file of the process which found the proof. */
} /* print_stats */
/*************
*
* p_stats()
*
*************/
void p_stats(void)
{
print_stats(stdout);
} /* p_stats */
/*************
*
* print_times(fp)
*
*************/
void print_times(FILE *fp)
{
long t, min, hr;
fprintf(fp, "\n----------- times (seconds) ----------- %s\n", get_time());
t = run_time();
fprintf(fp, "user CPU time %10.2f ", t / 1000.);
t = t / 1000; hr = t / 3600; t = t % 3600; min = t / 60; t = t % 60;
fprintf(fp, " (%ld hr, %ld min, %ld sec)\n", hr, min, t);
t = system_time();
fprintf(fp, "system CPU time %10.2f ", t/ 1000.);
t = t / 1000; hr = t / 3600; t = t % 3600; min = t / 60; t = t % 60;
fprintf(fp, " (%ld hr, %ld min, %ld sec)\n", hr, min, t);
t = wall_seconds() - Stats[INIT_WALL_SECONDS];
if (Stats[PROOFS] > 0)
fprintf(fp, "WALL-CLOCK TIME %7ld ", t);
else
fprintf(fp, "wall-clock time %7ld ", t);
/* Peers-mcd, November 1996: to use grep WALL to extract the wall-clock */
/* time from the file of the process which found the proof. */
hr = t / 3600; t = t % 3600; min = t / 60; t = t % 60;
fprintf(fp, " (%ld hr, %ld min, %ld sec)\n", hr, min, t);
fprintf(fp, "input time %10.2f\n", clock_val(INPUT_TIME) / 1000.);
fprintf(fp, "paramodulation time %10.2f\n", clock_val(PARAMOD_TIME) / 1000.);
fprintf(fp, "demodulation time %10.2f\n", clock_val(DEMOD_TIME) / 1000.);
fprintf(fp, "orient time %10.2f\n", clock_val(ORIENT_EQ_TIME) / 1000.);
fprintf(fp, "weigh time %10.2f\n", clock_val(WEIGH_TIME) / 1000.);
fprintf(fp, "forward subsume time%10.2f\n", clock_val(FOR_SUB_TIME) / 1000.);
fprintf(fp, "back demod find time%10.2f\n", clock_val(BD_FIND_TIME) / 1000.);
fprintf(fp, "conflict time %10.2f\n", clock_val(CONFLICT_TIME) / 1000.);
fprintf(fp, "LRPO time %10.2f\n", clock_val(LRPO_TIME) / 1000.);
fprintf(fp, "store clause time %10.2f\n", clock_val(STORE_TIME) / 1000.);
fprintf(fp, "disable clause time %10.2f\n", clock_val(DISABLE_TIME) / 1000.);
fprintf(fp, "prime paramod time %10.2f\n", clock_val(PRIME_PARAMOD_TIME) / 1000.);
fprintf(fp, "semantics time %10.2f\n", clock_val(SEMANTICS_TIME) / 1000.);
/* Peers_mcd -- October 1996 */
fprintf(fp, "inference msg time %10.2f\n", clock_val(INF_MSG_TIME) / 1000.);
fprintf(fp, "inference work time %10.2f\n", clock_val(INFERENCE_TIME) / 1000.);
/* Peers_mcd -- April 2000 */
if(Flags[HEURISTIC_SEARCH].val)
fprintf(fp, "heuristic compute time %10.2f\n", clock_val(HEURISTIC_TIME) / 1000.);
fprintf(fp, "\n");
} /* print_times */
/*************
*
* p_times()
*
*************/
void p_times(void)
{
print_times(stdout);
} /* p_times */
/*************
*
* output_stats
*
*************/
void output_stats(FILE *fp)
{
print_mem(fp);
print_stats(fp);
print_times(fp);
} /* output_stats */