1 #include "Mace2.h"
2
3 long MACE_Stats[MACE_MAX_STATS];
4 extern struct MACE_clock MACE_Clocks[MACE_MAX_CLOCKS];
5 extern int Internal_flags[MAX_INTERNAL_FLAGS];
6
7 extern int Domain_size; /* owned by mace.c */
8 extern int Init_wall_seconds; /* owned by mace.c */
9
10 /*************
11 *
12 * init_stats()
13 *
14 *************/
15
init_stats()16 void init_stats()
17 {
18 int i;
19
20 init_clocks();
21 for (i = 0; i < MAX_INTERNAL_FLAGS; i++)
22 Internal_flags[i] = 0;
23 for (i = 0; i < MACE_MAX_STATS; i++)
24 MACE_Stats[i] = 0;
25 } /* init_stats */
26
27 /*************
28 *
29 * MACE_print_mem()
30 *
31 *************/
32
MACE_print_mem(FILE * fp)33 void MACE_print_mem(FILE *fp)
34 {
35 fprintf(fp, "\n------------- memory usage ------------\n");
36
37 fprintf(fp, "Memory dynamically allocated (MACE_tp_alloc): %d.\n", MACE_total_mem());
38
39 } /* print_mem */
40
41 /*************
42 *
43 * p_mem
44 *
45 *************/
46
p_mem(void)47 void p_mem(void)
48 {
49 MACE_print_mem(stdout);
50 } /* p_mem */
51
52 /*************
53 *
54 * MACE_print_stats(fp)
55 *
56 *************/
57
MACE_print_stats(FILE * fp)58 void MACE_print_stats(FILE *fp)
59 {
60 fprintf(fp, "\n----- statistics for domain size %d ----\n", Domain_size);
61
62 fprintf(fp, "Input:\n");
63 fprintf(fp, " Clauses input %7ld\n", MACE_Stats[INPUT_CLAUSES]);
64 fprintf(fp, " Literal occurrences input %7ld\n", MACE_Stats[LIT_OCC_INPUT]);
65 fprintf(fp, " Greatest atom %7ld\n", MACE_Stats[GREATEST_ATOM]);
66 fprintf(fp, "Unit preprocess:\n");
67 fprintf(fp, " Preprocess unit assignments %7ld\n", MACE_Stats[PREPROCESS_UNIT_ASSIGNS]);
68 fprintf(fp, " Clauses after subsumption %7ld\n", MACE_Stats[CLAUSES_AFTER_SUB]);
69 fprintf(fp, " Literal occ. after subsump. %7ld\n", MACE_Stats[LIT_OCC_AFTER_SUB]);
70 fprintf(fp, " Selectable clauses %7ld\n", MACE_Stats[SELECTABLE_CLAUSES]);
71 fprintf(fp, "Decide:\n");
72 fprintf(fp, " Splits %7ld\n", MACE_Stats[SPLITS]);
73 fprintf(fp, " Unit assignments %7ld\n", MACE_Stats[UNIT_ASSIGNS]);
74 fprintf(fp, " Failed paths %7ld\n", MACE_Stats[FAILED_PATHS]);
75 fprintf(fp, "Memory:\n");
76 fprintf(fp, " Memory malloced %7ld K\n", MACE_Stats[MEM_MALLOCED] / 1024);
77 fprintf(fp, " Memory MACE_tp_alloced %7d K\n", MACE_total_mem());
78 fprintf(fp, "Time (seconds):\n");
79 fprintf(fp, " Generate ground clauses %10.2f\n", MACE_clock_val(GENERATE_TIME) / 1000.);
80 fprintf(fp, " DPLL %10.2f\n", MACE_clock_val(DECIDE_TIME) / 1000.);
81 } /* MACE_print_stats */
82
83 /*************
84 *
85 * MACE_p_stats()
86 *
87 *************/
88
MACE_p_stats(void)89 void MACE_p_stats(void)
90 {
91 MACE_print_stats(stdout);
92 } /* MACE_p_stats */
93
94 /*************
95 *
96 * MACE_print_times(fp)
97 *
98 *************/
99
MACE_print_times(FILE * fp)100 void MACE_print_times(FILE *fp)
101 {
102 long t, min, hr;
103
104 fprintf(fp, "\n=======================================\n");
105 fprintf(fp, "Total times for run (seconds):\n");
106
107 t = run_time();
108 fprintf(fp, " user CPU time %10.2f ", t / 1000.);
109 t = t / 1000; hr = t / 3600; t = t % 3600; min = t / 60; t = t % 60;
110 fprintf(fp, " (%ld hr, %ld min, %ld sec)\n", hr, min, t);
111
112 t = system_time();
113 fprintf(fp, " system CPU time %10.2f ", t/ 1000.);
114 t = t / 1000; hr = t / 3600; t = t % 3600; min = t / 60; t = t % 60;
115 fprintf(fp, " (%ld hr, %ld min, %ld sec)\n", hr, min, t);
116
117 t = wall_seconds() - Init_wall_seconds;
118 fprintf(fp, " wall-clock time %7ld ", t);
119 hr = t / 3600; t = t % 3600; min = t / 60; t = t % 60;
120 fprintf(fp, " (%ld hr, %ld min, %ld sec)\n", hr, min, t);
121
122 } /* MACE_print_times */
123
124 /*************
125 *
126 * MACE_output_stats
127 *
128 *************/
129
MACE_output_stats(FILE * fp)130 void MACE_output_stats(FILE *fp)
131 {
132 MACE_print_stats(fp);
133 MACE_print_times(fp);
134 } /* MACE_output_stats */
135
136