Skip to content

Commit c948f66

Browse files
arminbierearminbiere
committed
added gecpu
1 parent b9daaac commit c948f66

24 files changed

+187
-182
lines changed

‎VERSION

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
06l
1+
06m

‎analyze.c

+4-5
Original file line numberDiff line numberDiff line change
@@ -73,16 +73,15 @@ analyze_reason_side_literals (struct ring *ring)
7373
ticks++;
7474
for (all_watcher_literals (other, watcher))
7575
if (other != not_lit &&
76-
analyze_reason_side_literal (ring, other) &&
77-
++pushed > limit)
76+
analyze_reason_side_literal (ring, other) && ++pushed > limit)
7877
break;
7978
}
8079
}
8180
ring->statistics.contexts[ring->context].ticks += ticks;
8281
}
8382

8483
static bool
85-
larger_trail_position (unsigned * pos, unsigned a, unsigned b)
84+
larger_trail_position (unsigned *pos, unsigned a, unsigned b)
8685
{
8786
unsigned i = IDX (a);
8887
unsigned j = IDX (b);
@@ -92,7 +91,7 @@ larger_trail_position (unsigned * pos, unsigned a, unsigned b)
9291
#define LARGER_TRAIL_POS(A,B) larger_trail_position (pos, (A), (B))
9392

9493
static void
95-
sort_deduced_clause (struct ring * ring)
94+
sort_deduced_clause (struct ring *ring)
9695
{
9796
LOGTMP ("clause before sorting");
9897
unsigned *pos = ring->trail.pos;
@@ -121,7 +120,7 @@ clear_analyzed (struct ring *ring)
121120
}
122121

123122
static void
124-
update_decision_rate (struct ring * ring)
123+
update_decision_rate (struct ring *ring)
125124
{
126125
uint64_t current = SEARCH_DECISIONS;
127126
uint64_t previous = ring->last.decisions;

‎average.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@
77
#endif
88

99
void
10-
update_average (struct ring * ring, struct average *average,
11-
const char * name, double alpha, double y)
10+
update_average (struct ring *ring, struct average *average,
11+
const char *name, double alpha, double y)
1212
{
1313
double old_biased = average->biased;
1414
double delta = y - old_biased;

‎backtrack.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -62,8 +62,8 @@ update_best_and_target_phases (struct ring *ring)
6262
if (ring->target < assigned)
6363
{
6464
very_verbose (ring,
65-
"updating target assigned trail height from %u to %u",
66-
ring->target, assigned);
65+
"updating target assigned trail height from %u to %u",
66+
ring->target, assigned);
6767
ring->target = assigned;
6868
signed char *q = ring->values;
6969
for (all_phases (p))
@@ -77,7 +77,7 @@ update_best_and_target_phases (struct ring *ring)
7777
if (ring->best < assigned)
7878
{
7979
very_verbose (ring,
80-
"updating best assigned trail height from %u to %u",
80+
"updating best assigned trail height from %u to %u",
8181
ring->best, assigned);
8282
ring->best = assigned;
8383
signed char *q = ring->values;

‎bump.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -221,16 +221,16 @@ sort_and_bump_analyzed_variables_on_queue (struct ring *ring)
221221
}
222222

223223
static void
224-
bump_analyzed_variables_on_heap (struct ring * ring)
224+
bump_analyzed_variables_on_heap (struct ring *ring)
225225
{
226226
assert (ring->stable);
227227
for (all_elements_on_stack (unsigned, idx, ring->analyzed))
228-
bump_variable_on_heap (ring, idx);
228+
bump_variable_on_heap (ring, idx);
229229
bump_score_increment (ring);
230230
}
231231

232232
void
233-
bump_variables (struct ring * ring)
233+
bump_variables (struct ring *ring)
234234
{
235235
if (ring->stable)
236236
bump_analyzed_variables_on_heap (ring);

‎catch.c

+4-4
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,8 @@ raising_message (int sig)
9696
if (sig == SIGALRM)
9797
name = "SIGALRM";
9898
char buffer[80];
99-
sprintf (buffer, "c\nc raising signal %d (%s) after reporting statistics\n", sig, name);
99+
sprintf (buffer, "c\nc raising signal %d (%s) after reporting statistics\n",
100+
sig, name);
100101
size_t bytes = strlen (buffer);
101102
if (write (1, buffer, bytes) != bytes)
102103
exit (2);
@@ -105,9 +106,8 @@ raising_message (int sig)
105106
static void
106107
exit_message (void)
107108
{
108-
const char * message =
109-
"c calling 'exit (1)' as raising signal returned\n";
110-
size_t bytes = strlen (message);
109+
const char *message = "c calling 'exit (1)' as raising signal returned\n";
110+
size_t bytes = strlen (message);
111111
if (write (1, message, bytes) != bytes)
112112
exit (2);
113113
}

‎eliminate.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
#include <inttypes.h>
1212

1313
static size_t
14-
actual_occurrences (struct ruler * ruler, struct clauses *clauses)
14+
actual_occurrences (struct ruler *ruler, struct clauses *clauses)
1515
{
1616
size_t clause_size_limit = ruler->limits.clause_size_limit;
1717
struct clause **begin = clauses->begin, **q = begin;

‎import.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -247,7 +247,7 @@ subsumed_large_clause (struct ring *ring, struct clause *clause)
247247
if (blocking_value >= 0)
248248
continue;
249249
unsigned blocking_idx = IDX (blocking);
250-
struct variable * v = variables + blocking_idx;
250+
struct variable *v = variables + blocking_idx;
251251
if (v->level)
252252
continue;
253253
}
@@ -257,7 +257,7 @@ subsumed_large_clause (struct ring *ring, struct clause *clause)
257257
LOGWATCH (watch, "subsuming");
258258
break;
259259
}
260-
struct watcher * watcher = get_watcher (ring, watch);
260+
struct watcher *watcher = get_watcher (ring, watch);
261261
res = true;
262262
for (all_watcher_literals (other, watcher))
263263
{
@@ -272,7 +272,7 @@ subsumed_large_clause (struct ring *ring, struct clause *clause)
272272
if (other_value < 0)
273273
{
274274
unsigned other_idx = IDX (other);
275-
struct variable * other_variable = variables + other_idx;
275+
struct variable *other_variable = variables + other_idx;
276276
if (!other_variable->level)
277277
continue;
278278
}

‎message.h

+9-10
Original file line numberDiff line numberDiff line change
@@ -22,24 +22,23 @@ static const int verbosity = -1;
2222
extern int verbosity;
2323
extern const char *prefix_format;
2424

25+
2526
#ifdef LOGGING
2627
#include <stdatomic.h>
27-
// *INDENT-OFF
28-
extern
29-
_Atomic (uint64_t)
30-
clause_ids;
31-
// *INDENT-ON
28+
// *INDENT-OFF*
29+
extern _Atomic (uint64_t) clause_ids;
30+
// *INDENT-ON*
3231
#endif
3332

34-
void acquire_message_lock (void);
35-
void release_message_lock (void);
33+
void acquire_message_lock (void);
34+
void release_message_lock (void);
3635

37-
struct ring;
36+
struct ring;
3837

39-
void print_line_without_acquiring_lock (struct ring *, const char *, ...)
38+
void print_line_without_acquiring_lock (struct ring *, const char *, ...)
4039
__attribute__((format (printf, 2, 3)));
4140

42-
void message (struct ring *ring, const char *, ...)
41+
void message (struct ring *ring, const char *, ...)
4342
__attribute__((format (printf, 2, 3)));
4443

4544
#define PRINTLN(...) \

‎mode.c

+7-8
Original file line numberDiff line numberDiff line change
@@ -9,14 +9,14 @@
99
#include <inttypes.h>
1010

1111
static void
12-
report_mode_duration (struct ring * ring, double t, const char * type)
12+
report_mode_duration (struct ring *ring, double t, const char *type)
1313
{
14-
struct ring_last * l = &ring->last;
14+
struct ring_last *l = &ring->last;
1515
verbose (ring, "%s mode took %.2f seconds "
16-
"(%" PRIu64 " conflicts, %" PRIu64 " ticks)",
17-
type, t - l->mode.time,
18-
SEARCH_CONFLICTS - l->mode.conflicts,
19-
SEARCH_TICKS - l->mode.ticks);
16+
"(%" PRIu64 " conflicts, %" PRIu64 " ticks)",
17+
type, t - l->mode.time,
18+
SEARCH_CONFLICTS - l->mode.conflicts,
19+
SEARCH_TICKS - l->mode.ticks);
2020
l->mode.time = t;
2121
l->mode.conflicts = SEARCH_CONFLICTS;
2222
l->mode.ticks = SEARCH_TICKS;
@@ -89,8 +89,7 @@ switch_mode (struct ring *ring)
8989
uint64_t interval = base * nlog4n (s->switched / 2 + 1);
9090
l->mode = SEARCH_TICKS + interval;
9191
very_verbose (ring, "new mode switching limit at %" PRIu64
92-
" after %" PRIu64 " ticks",
93-
l->mode, interval);
92+
" after %" PRIu64 " ticks", l->mode, interval);
9493
l->import = 0;
9594
ring->last.decisions = SEARCH_DECISIONS;
9695
}

‎probe.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ probe (struct ring *ring)
4343
limits->probe.conflicts = SEARCH_CONFLICTS + scaled;
4444
limits->probe.reductions = statistics->reductions + 1;
4545
very_verbose (ring, "new probe limit at %" PRIu64
46-
" after %" PRIu64 " conflicts",
46+
" after %" PRIu64 " conflicts",
4747
limits->probe.conflicts, scaled);
4848
STOP_AND_START_SEARCH (probe);
4949
return ring->inconsistent ? 20 : 0;

‎rephase.c

+1-2
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,6 @@ rephase (struct ring *ring)
7777
uint64_t interval = base * nlog3n (rephased);
7878
limits->rephase = SEARCH_CONFLICTS + interval;
7979
very_verbose (ring, "new rephase limit of %" PRIu64
80-
" after %" PRIu64 " conflicts",
81-
limits->rephase, interval);
80+
" after %" PRIu64 " conflicts", limits->rephase, interval);
8281
report (ring, type);
8382
}

‎report.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ verbose_report (struct ring *ring, char type, int level)
4040
"conflicts redundant trail glue irredundant variables\nc\n");
4141

4242
PRINTLN ("%c %7.2f %4.0f %5.0f %6" PRIu64 " %9" PRIu64 " %4.0f"
43-
" %11" PRIu64 " %9zu %3.0f%% %6.1f %9zu %9u %3.0f%%", type, t, m,
43+
" %11" PRIu64 " %9zu %3.0f%% %6.1f %9zu %9u %3.0f%%", type, t, m,
4444
a->level.value, s->reductions, s->restarts, a->decisions.value,
4545
conflicts, s->redundant, a->trail.value, a->glue.slow.value,
4646
s->irredundant, active, percent (active, ring->ruler->size));

‎restart.c

+2-4
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,7 @@ restarting (struct ring *ring)
2525
extremely_verbose (ring, "restart glue limit %g = "
2626
"%g * %g (slow glue) %c %g (fast glue)",
2727
margin, RESTART_MARGIN, slow,
28-
margin == fast ? '=' : margin > fast ? '>' : '<',
29-
fast);
28+
margin == fast ? '=' : margin > fast ? '>' : '<', fast);
3029
return margin <= fast;
3130
}
3231

@@ -58,7 +57,6 @@ restart (struct ring *ring)
5857
interval = FOCUSED_RESTART_INTERVAL + logn (statistics->restarts) - 1;
5958
limits->restart = SEARCH_CONFLICTS + interval;
6059
very_verbose (ring, "new restart limit at %" PRIu64
61-
" after %" PRIu64 " conflicts",
62-
limits->restart, interval);
60+
" after %" PRIu64 " conflicts", limits->restart, interval);
6361
verbose_report (ring, 'r', 1);
6462
}

‎ring.c

+20-18
Original file line numberDiff line numberDiff line change
@@ -141,7 +141,7 @@ release_ring (struct ring *ring, bool keep_values)
141141
}
142142

143143
static void
144-
activate_variables (struct ring * ring, unsigned size)
144+
activate_variables (struct ring *ring, unsigned size)
145145
{
146146
if (!size)
147147
return;
@@ -169,28 +169,30 @@ activate_variables (struct ring * ring, unsigned size)
169169

170170
struct heap *heap = &ring->heap;
171171
struct queue *queue = &ring->queue;
172-
struct node * nodes = heap->nodes;
173-
struct link * links = queue->links;
172+
struct node *nodes = heap->nodes;
173+
struct link *links = queue->links;
174174

175175
unsigned idx = start;
176176
unsigned activated = 0;
177-
do {
178-
assert (idx < size);
177+
do
178+
{
179+
assert (idx < size);
179180

180-
struct node * node = nodes + idx;
181-
node->score = 1.0 - 1.0 / ++activated;
182-
push_heap (heap, node);
183-
LOG ("activating %s on heap", LOGVAR (idx));
181+
struct node *node = nodes + idx;
182+
node->score = 1.0 - 1.0 / ++activated;
183+
push_heap (heap, node);
184+
LOG ("activating %s on heap", LOGVAR (idx));
184185

185-
struct link * link = links + idx;
186-
enqueue (queue, link, true);
187-
LOG ("activating %s on queue", LOGVAR (idx));
186+
struct link *link = links + idx;
187+
enqueue (queue, link, true);
188+
LOG ("activating %s on queue", LOGVAR (idx));
188189

189-
idx += delta;
190-
if (idx >= size)
191-
idx -= size;
190+
idx += delta;
191+
if (idx >= size)
192+
idx -= size;
192193

193-
} while (idx != start);
194+
}
195+
while (idx != start);
194196
LOG ("activated %u variables", activated);
195197
}
196198

@@ -415,9 +417,9 @@ mark_satisfied_watchers_as_garbage (struct ring *ring)
415417
}
416418

417419
unsigned *
418-
sorter_block (struct ring * ring, size_t size)
420+
sorter_block (struct ring *ring, size_t size)
419421
{
420-
assert (size <= 1u<<31);
422+
assert (size <= 1u << 31);
421423
assert (EMPTY (ring->sorter));
422424
while (CAPACITY (ring->sorter) < size)
423425
ENLARGE (ring->sorter);

‎ring.h

+3-2
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,8 @@ struct ring_limits
3636
uint64_t restart;
3737
uint64_t simplify;
3838
long long conflicts;
39-
struct {
39+
struct
40+
{
4041
uint64_t conflicts;
4142
uint64_t reductions;
4243
} probe;
@@ -217,7 +218,7 @@ void set_satisfied (struct ring *);
217218

218219
void print_ring_profiles (struct ring *);
219220

220-
unsigned * sorter_block (struct ring *, size_t size);
221+
unsigned *sorter_block (struct ring *, size_t size);
221222

222223
/*------------------------------------------------------------------------*/
223224

‎scale.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
#include <inttypes.h>
88

99
uint64_t
10-
scale_interval (struct ring * ring, const char * name, uint64_t interval)
10+
scale_interval (struct ring *ring, const char *name, uint64_t interval)
1111
{
1212
uint64_t reference = ring->statistics.irredundant + 1;
1313
double f = logn (reference);

‎scale.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@
55

66
struct ring;
77

8-
uint64_t scale_interval (struct ring*, const char *, uint64_t);
8+
uint64_t scale_interval (struct ring *, const char *, uint64_t);
99

1010
#endif

‎simplify.c

+1-2
Original file line numberDiff line numberDiff line change
@@ -898,8 +898,7 @@ finish_ring_simplification (struct ring *ring)
898898
limits->simplify = SEARCH_CONFLICTS + scaled;
899899
ruler->last.search = statistics->contexts[SEARCH_CONTEXT].ticks;
900900
very_verbose (ring, "new simplify limit at %" PRIu64
901-
" after %" PRIu64 " conflicts",
902-
limits->simplify, scaled);
901+
" after %" PRIu64 " conflicts", limits->simplify, scaled);
903902
}
904903

905904
#ifndef NDEBUG

‎solve.c

+8-1
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,9 @@ start_running_ring (struct ring *ring)
2525
pthread_t *thread = ruler->threads + ring->id;
2626
if (pthread_create (thread, 0, solve_routine, ring))
2727
fatal_error ("failed to create solving thread %u", ring->id);
28+
unsigned cpu, node;
29+
if (!getcpu (&cpu, &node, 0))
30+
message (ring, "getcpu: cpu=%08x node=%08x", cpu, node);
2831
}
2932

3033
static void
@@ -162,11 +165,15 @@ solve_rings (struct ruler *ruler)
162165
init_barrier (&ruler->barriers.NAME, #NAME, threads);
163166
BARRIERS
164167
#undef BARRIER
165-
for (all_rings (ring))
168+
// *INDENT-OFF*
169+
170+
for (all_rings (ring))
166171
start_running_ring (ring);
167172

168173
for (all_rings (ring))
169174
stop_running_ring (ring);
175+
176+
// *INDENT-ON*
170177
}
171178
else
172179
{

0 commit comments

Comments
 (0)