Files
psat/subtree.h

89 lines
2.6 KiB
C

#pragma once
#include "types.h"
#include <stdlib.h>
/*
void sortstrings(char** list, u32 len, u32 cnt) {
bool v = false;
u32* d = malloc(sizeof(u32) * c->litcnt);
u32* d2 = malloc(sizeof(u32) * c->litcnt);
u8* d3 = malloc(sizeof(u8) * c->litcnt);
u64 qb[RLVLS * RSIZE];
u64 qe[RLVLS * RSIZE];
memset(qb, 0, sizeof(u64) * RLVLS * RSIZE);
memset(qe, 0, sizeof(u64) * RLVLS * RSIZE);
for (u64 pass = 0; pass < RLVLS; ++pass) {
u64 shift = pass * RBITS;
for (u64 i = 0; i < N; ++i) {
// U32MAX - because we want to sort highest to lowest, not lowest to highest
u32 val = UINT32_MAX - c->lastvars[c->clauses[i]];
u64 ind = (val >> shift) & RMASK;
qe[pass * RSIZE + ind]++;
}
u64 uc = 0;
for (u64 i = 0; i < RSIZE; ++i) if (qe[pass * RSIZE + i]) uc++;
if (uc == 1) continue;
qb[pass * RSIZE] = 0;
for (u64 i = 1; i < RSIZE; ++i) {
qb[pass * RSIZE + i] = qb[pass * RSIZE + i - 1] + qe[pass * RSIZE + i - 1];
}
for (u64 i = 0; i < N; ++i) {
u32 val = UINT32_MAX - c->lastvars[c->clauses[i]];
u64 ind = (val >> shift) & RMASK;
d[qb[pass * RSIZE + ind]] = c->variables[i];
d2[qb[pass * RSIZE + ind]] = c->clauses[i];
d3[qb[pass * RSIZE + ind]] = c->pars[i];
qb[pass * RSIZE + ind]++;
__builtin_prefetch(d + qb[pass * RSIZE + ind] + 1);
__builtin_prefetch(d2 + qb[pass * RSIZE + ind] + 1);
__builtin_prefetch(d3 + qb[pass * RSIZE + ind] + 1);
}
// Every iteration we swap pointers to avoid doing a memcpy
u32* tptr = c->variables;
c->variables = d;
d = tptr;
tptr = c->clauses;
c->clauses = d2;
d2 = tptr;
u8* tptr2 = c->pars;
c->pars = d3;
d3 = tptr2;
v = !v;
}
// If the pointers are still swapped at the end, we swap them to their original locations and
// copy over the result
if (v) {
u32* tptr = c->variables;
c->variables = d;
d = tptr;
tptr = c->clauses;
c->clauses = d2;
d2 = tptr;
u8* tptr2 = c->pars;
c->pars = d3;
d3 = tptr2;
memcpy(c->variables, d, N * sizeof(u32));
memcpy(c->clauses, d2, N * sizeof(u32));
memcpy(c->pars, d3, N * sizeof(u8));
}
free(d);
free(d2);
free(d3);
// Initialize an array with all the clause indices in their current order
u32* swaparr = malloc(sizeof(u32) * c->clausecnt);
for (u32 i = 0; i < c->clausecnt; ++i) {
swaparr[i] = i;
}
}
*/