needs more ram
This commit is contained in:
parent
c44f737a0e
commit
19a36e120f
2 changed files with 184 additions and 146 deletions
|
|
@ -28,6 +28,7 @@
|
|||
gnumake
|
||||
readline.dev
|
||||
python3
|
||||
valgrind
|
||||
];
|
||||
};
|
||||
packages.default = pkgs.stdenv.mkDerivation rec {
|
||||
|
|
|
|||
329
main.c
329
main.c
|
|
@ -189,19 +189,24 @@ static void parse_args(int argc, char* const* argv)
|
|||
}
|
||||
}
|
||||
|
||||
#define W 0b0101010101010101
|
||||
#define X 0b0011001100110011
|
||||
#define Y 0b0000111100001111
|
||||
#define Z 0b0000000011111111
|
||||
#define M 0b1111111111111111
|
||||
#define V 0b01010101010101010101010101010101
|
||||
#define W 0b00110011001100110011001100110011
|
||||
#define X 0b00001111000011110000111100001111
|
||||
#define Y 0b00000000111111110000000011111111
|
||||
#define Z 0b00000000000000001111111111111111
|
||||
#define M 0b11111111111111111111111111111111
|
||||
|
||||
#define N (65536)
|
||||
#define N (1UL << (1UL << 5UL))
|
||||
|
||||
#define NN (65536)
|
||||
|
||||
enum kind {
|
||||
ek_unreachable,
|
||||
|
||||
ek_0,
|
||||
ek_1,
|
||||
|
||||
ek_V,
|
||||
ek_W,
|
||||
ek_X,
|
||||
ek_Y,
|
||||
|
|
@ -231,13 +236,15 @@ enum kind {
|
|||
struct expr {
|
||||
enum kind kind;
|
||||
|
||||
uint16_t cond, left, right;
|
||||
uint32_t cond, left, right;
|
||||
|
||||
int cost;
|
||||
} lookup[N];
|
||||
|
||||
static void print(uint16_t truthtable, int depth)
|
||||
static void print(uint32_t truthtable, int depth)
|
||||
{
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
#define LITERAL_ESCAPE "\e[38;2;200;200;100m"
|
||||
#define VARIABLE_ESCAPE "\e[38;2;100;100;200m"
|
||||
#define RESET_ESCAPE "\e[0m"
|
||||
|
|
@ -378,79 +385,102 @@ static void print(uint16_t truthtable, int depth)
|
|||
break;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
|
||||
// heap of truthtables; key = cost
|
||||
struct todo {
|
||||
uint32_t data[N];
|
||||
uint32_t n;
|
||||
|
||||
// truthtable -> index in 'todo'
|
||||
uint32_t reverse[N];
|
||||
} *todo;
|
||||
|
||||
// create a list of the "done" truthtables
|
||||
struct done {
|
||||
uint64_t headtails[N], next[N], head;
|
||||
} *done;
|
||||
|
||||
void calculate_simplifications(void)
|
||||
{
|
||||
// init 'lookup':
|
||||
for (uint64_t i = 0; i < N; i++)
|
||||
{
|
||||
for (int i = 0; i < N; i++)
|
||||
if (i % 42949672 == 0)
|
||||
{
|
||||
lookup[i].kind = ek_unreachable;
|
||||
|
||||
lookup[i].cost = INT_MAX;
|
||||
printf("init lookup: %.2f%%\n", (double) i * 100 / N);
|
||||
}
|
||||
|
||||
lookup[i].kind = ek_unreachable;
|
||||
|
||||
lookup[i].cost = INT_MAX;
|
||||
}
|
||||
|
||||
// heap of truthtables; key = cost
|
||||
struct {
|
||||
uint16_t data[N];
|
||||
int n;
|
||||
|
||||
// truthtable -> index in 'todo'
|
||||
int reverse[N];
|
||||
} todo;
|
||||
|
||||
// init 'todo':
|
||||
{
|
||||
todo.n = 0;
|
||||
todo->n = 0;
|
||||
|
||||
for (int i = 0; i < N; i++)
|
||||
for (uint64_t i = 0; i < N; i++)
|
||||
{
|
||||
todo.reverse[i] = -1;
|
||||
if (i % 42949672 == 0)
|
||||
{
|
||||
printf("init todo: %.2f%%\n", (double) i * 100 / N);
|
||||
}
|
||||
|
||||
todo->reverse[i] = (uint32_t) -1;
|
||||
}
|
||||
}
|
||||
|
||||
uint16_t pop(void)
|
||||
uint32_t pop(void)
|
||||
{
|
||||
assert(todo.n > 0);
|
||||
printf(" pop()\n");
|
||||
|
||||
uint16_t retval = todo.data[0];
|
||||
assert(todo->n > 0);
|
||||
|
||||
todo.reverse[retval] = -1;
|
||||
uint32_t retval = todo->data[0];
|
||||
|
||||
uint16_t moving = todo.data[todo.n-- - 1];
|
||||
todo->reverse[retval] = (uint32_t) -1;
|
||||
|
||||
uint32_t moving = todo->data[todo->n-- - 1];
|
||||
|
||||
int cost = lookup[moving].cost;
|
||||
|
||||
int index = 0;
|
||||
uint64_t index = 0;
|
||||
|
||||
again:
|
||||
{
|
||||
int left = index * 2 + 1;
|
||||
int right = index * 2 + 2;
|
||||
printf(" index = %lu\n", index);
|
||||
|
||||
uint16_t smallest = moving;
|
||||
uint64_t left = index * 2 + 1;
|
||||
uint64_t right = index * 2 + 2;
|
||||
|
||||
if (left < todo.n && lookup[todo.data[left]].cost < cost)
|
||||
smallest = todo.data[left];
|
||||
uint32_t smallest = moving;
|
||||
|
||||
if (right < todo.n && lookup[todo.data[right]].cost < lookup[smallest].cost)
|
||||
smallest = todo.data[right];
|
||||
if (left < todo->n && lookup[todo->data[left]].cost < cost)
|
||||
smallest = todo->data[left];
|
||||
|
||||
if (right < todo->n && lookup[todo->data[right]].cost < lookup[smallest].cost)
|
||||
smallest = todo->data[right];
|
||||
|
||||
if (smallest == moving)
|
||||
{
|
||||
todo.data[index] = moving;
|
||||
todo->data[index] = moving;
|
||||
|
||||
todo.reverse[moving] = index;
|
||||
assert(index < 4294967296);
|
||||
|
||||
todo->reverse[moving] = (uint32_t) index;
|
||||
}
|
||||
else
|
||||
{
|
||||
int new = todo.reverse[smallest];
|
||||
uint32_t new = todo->reverse[smallest];
|
||||
|
||||
todo.data[index] = smallest;
|
||||
todo->data[index] = smallest;
|
||||
|
||||
todo.reverse[smallest] = index;
|
||||
assert(index < 4294967296);
|
||||
|
||||
todo->reverse[smallest] = (uint32_t) index;
|
||||
|
||||
index = new;
|
||||
|
||||
|
|
@ -458,156 +488,163 @@ void calculate_simplifications(void)
|
|||
}
|
||||
}
|
||||
|
||||
printf(" return 0b%032b\n", retval);
|
||||
|
||||
return retval;
|
||||
}
|
||||
|
||||
void append(uint16_t truthtable, int cost)
|
||||
void append(uint32_t truthtable, int cost)
|
||||
{
|
||||
assert(todo.reverse[truthtable] == -1);
|
||||
printf("append(truthtable = 0b%032b, cost = %i)\n", truthtable, cost);
|
||||
|
||||
int index = todo.n++, new_index;
|
||||
assert(todo->reverse[truthtable] == (uint32_t) -1);
|
||||
|
||||
while (index > 0 && lookup[todo.data[new_index = (index - 1) / 2]].cost > cost)
|
||||
assert(todo->n < N);
|
||||
|
||||
uint32_t index = (uint32_t) todo->n++, new_index;
|
||||
printf(" index = %i\n", index);
|
||||
|
||||
while (index > 0 && lookup[todo->data[new_index = (index - 1) / 2]].cost > cost)
|
||||
{
|
||||
todo.data[index] = todo.data[new_index];
|
||||
todo->data[index] = todo->data[new_index];
|
||||
|
||||
todo.reverse[todo.data[new_index]] = index;
|
||||
todo->reverse[todo->data[new_index]] = index;
|
||||
|
||||
index = new_index;
|
||||
printf(" index = %i\n", index);
|
||||
}
|
||||
|
||||
todo.data[index] = truthtable;
|
||||
todo->data[index] = truthtable;
|
||||
|
||||
todo.reverse[truthtable] = index;
|
||||
todo->reverse[truthtable] = index;
|
||||
|
||||
lookup[truthtable].cost = cost;
|
||||
}
|
||||
|
||||
void update(uint16_t truthtable, int cost)
|
||||
{
|
||||
assert(todo.reverse[truthtable] != -1);
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
assert(todo->reverse[truthtable] != -1);
|
||||
|
||||
assert(cost < lookup[truthtable].cost);
|
||||
|
||||
int index =todo. reverse[truthtable], new_index;
|
||||
int index =todo-> reverse[truthtable], new_index;
|
||||
|
||||
while (index > 0 && lookup[todo.data[new_index = (index - 1) / 2]].cost > cost)
|
||||
while (index > 0 && lookup[todo->data[new_index = (index - 1) / 2]].cost > cost)
|
||||
{
|
||||
todo.data[index] = todo.data[new_index];
|
||||
todo->data[index] = todo->data[new_index];
|
||||
|
||||
todo.reverse[todo.data[new_index]] = index;
|
||||
todo->reverse[todo->data[new_index]] = index;
|
||||
|
||||
index = new_index;
|
||||
}
|
||||
|
||||
todo.data[index] = truthtable;
|
||||
todo.reverse[truthtable] = index;
|
||||
todo->data[index] = truthtable;
|
||||
todo->reverse[truthtable] = index;
|
||||
|
||||
lookup[truthtable].cost = cost;
|
||||
}
|
||||
|
||||
// create a list of the "done" truthtables
|
||||
struct {
|
||||
int headtails[N], next[N], head;
|
||||
|
||||
// for debugging:
|
||||
#if ZDEBUG
|
||||
bool in[N];
|
||||
#endif
|
||||
} done = {};
|
||||
}
|
||||
|
||||
// init 'done':
|
||||
{
|
||||
done.head = -1;
|
||||
done->head = (uint64_t) -1;
|
||||
|
||||
for (int i = 0; i < N; i++)
|
||||
for (uint64_t i = 0; i < N; i++)
|
||||
{
|
||||
done.headtails[i] = -1;
|
||||
done->headtails[i] = (uint64_t) -1;
|
||||
|
||||
#if ZDEBUG
|
||||
done.in[i] = false;
|
||||
#endif
|
||||
if (i % 42949672 == 0)
|
||||
{
|
||||
printf("init done: %.2f%%\n", (double) i * 100 / N);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void insert(int index)
|
||||
void insert(uint32_t index)
|
||||
{
|
||||
#if ZDEBUG
|
||||
assert(!done.in[index]);
|
||||
#endif
|
||||
printf(" insert(0b%032b)\n", index);
|
||||
|
||||
int head = index & 1 ? index & ~(index & -index) : index, prevhead = -1;
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
uint32_t head = index & 1 ? index & ~(index & -index) : index;
|
||||
|
||||
while (done.headtails[head] == -1 || index < done.headtails[head])
|
||||
uint32_t prevhead = (uint32_t) -1;
|
||||
|
||||
while (false
|
||||
|| done->headtails[head] == (uint32_t) -1
|
||||
|| index < done->headtails[head])
|
||||
{
|
||||
done.headtails[head] = index;
|
||||
done->headtails[head] = index;
|
||||
|
||||
prevhead = head, head = head & ~(head & -head);
|
||||
}
|
||||
|
||||
if (done.headtails[head] < index)
|
||||
{
|
||||
if (prevhead == -1)
|
||||
{
|
||||
assert(done.headtails[head] == head);
|
||||
printf(" head = %lu\n", head);
|
||||
|
||||
done.next[head] = index;
|
||||
if (done->headtails[head] < index)
|
||||
{
|
||||
if (prevhead == (uint32_t) -1)
|
||||
{
|
||||
assert(done->headtails[head] == head);
|
||||
|
||||
done->next[head] = index;
|
||||
}
|
||||
else
|
||||
{
|
||||
int tophalftail = done.headtails[prevhead - 1];
|
||||
uint32_t tophalftail = done->headtails[prevhead - 1];
|
||||
|
||||
assert(tophalftail != -1);
|
||||
assert(tophalftail != (uint32_t) -1);
|
||||
|
||||
done.next[tophalftail] = index;
|
||||
done->next[tophalftail] = index;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
done.head = index;
|
||||
done->head = index;
|
||||
}
|
||||
|
||||
int n = ~index & M;
|
||||
int tail = index & 1 ? index : index | (n & -n), prevtail = -1;
|
||||
uint32_t n = ~index & M;
|
||||
uint32_t tail = index & 1 ? index : index | (n & -n);
|
||||
uint32_t prevtail = (uint32_t) -1;
|
||||
|
||||
while (done.headtails[tail] == -1 || done.headtails[tail] < index)
|
||||
while (false
|
||||
|| done->headtails[tail] == (uint32_t) -1
|
||||
|| done->headtails[tail] < index)
|
||||
{
|
||||
done.headtails[tail] = index;
|
||||
done->headtails[tail] = index;
|
||||
|
||||
prevtail = tail, tail = tail | (n = ~tail & M, n & -n);
|
||||
}
|
||||
|
||||
if (index < done.headtails[tail])
|
||||
printf(" tail = %lu\n", tail);
|
||||
|
||||
if (index < done->headtails[tail])
|
||||
{
|
||||
if (prevtail == -1)
|
||||
if (prevtail == (uint32_t) -1)
|
||||
{
|
||||
assert(done.headtails[tail] == tail);
|
||||
assert(done->headtails[tail] == tail);
|
||||
|
||||
#if ZDEBUG
|
||||
assert(done.in[tail]);
|
||||
#endif
|
||||
|
||||
done.next[index] = tail;
|
||||
done->next[index] = tail;
|
||||
}
|
||||
else
|
||||
{
|
||||
int bottomhalfhead = done.headtails[prevtail + 1];
|
||||
int bottomhalfhead = done->headtails[prevtail + 1];
|
||||
|
||||
assert(bottomhalfhead != -1);
|
||||
assert(bottomhalfhead != (uint32_t) -1);
|
||||
|
||||
done.next[index] = bottomhalfhead;
|
||||
done->next[index] = bottomhalfhead;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
done.next[index] = -1;
|
||||
done->next[index] = (uint32_t) -1;
|
||||
}
|
||||
|
||||
#if ZDEBUG
|
||||
done.in[index] = true;
|
||||
#endif
|
||||
}
|
||||
|
||||
append(V, 0), lookup[V].kind = ek_V;
|
||||
append(W, 0), lookup[W].kind = ek_W;
|
||||
append(X, 0), lookup[X].kind = ek_X;
|
||||
append(Y, 0), lookup[Y].kind = ek_Y;
|
||||
|
|
@ -616,38 +653,24 @@ void calculate_simplifications(void)
|
|||
append(0, 1), lookup[0].kind = ek_0;
|
||||
append(M, 1), lookup[M].kind = ek_1;
|
||||
|
||||
// disable terminal autowrap:
|
||||
if (verbose && print_with_color)
|
||||
for (uint64_t iterations = 1; iterations <= N; iterations++)
|
||||
{
|
||||
printf("\e[?7l");
|
||||
}
|
||||
printf("iterations = %lu\n", iterations);
|
||||
|
||||
for (int iterations = 1; todo.n && iterations <= N; iterations++)
|
||||
{
|
||||
uint16_t truthtable = pop();
|
||||
assert(todo->n);
|
||||
|
||||
uint32_t truthtable = pop();
|
||||
|
||||
insert(truthtable);
|
||||
|
||||
int cost = lookup[truthtable].cost;
|
||||
printf("%lu of %lu (%.2f%%): [%i] ",
|
||||
iterations, N, (100.0 * (double) iterations / N), cost);
|
||||
|
||||
if (verbose)
|
||||
{
|
||||
if (print_with_color)
|
||||
{
|
||||
printf("\e[2K");
|
||||
}
|
||||
|
||||
printf("%i of %i (%.2f%%): [%i] ",
|
||||
iterations, N, (100.0 * iterations / N), cost);
|
||||
|
||||
print(truthtable, 0), puts("");
|
||||
|
||||
if (print_with_color)
|
||||
{
|
||||
printf("\e[1A");
|
||||
}
|
||||
}
|
||||
print(truthtable, 0), puts("");
|
||||
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
// consider NOT:
|
||||
if (use_operators.not)
|
||||
{
|
||||
|
|
@ -657,7 +680,7 @@ void calculate_simplifications(void)
|
|||
|
||||
if (not_cost < lookup[not_truthtable].cost)
|
||||
{
|
||||
if (todo.reverse[not_truthtable] == -1)
|
||||
if (todo->reverse[not_truthtable] == -1)
|
||||
{
|
||||
append(not_truthtable, not_cost);
|
||||
}
|
||||
|
|
@ -673,7 +696,7 @@ void calculate_simplifications(void)
|
|||
|
||||
#define BINARY_OPERATOR(ekind, function) \
|
||||
{ \
|
||||
for (int i = done.head; i != -1; i = done.next[i]) \
|
||||
for (int i = done->head; i != -1; i = done->next[i]) \
|
||||
{ \
|
||||
{ \
|
||||
uint16_t bin_truthtable = function(truthtable, i) & M; \
|
||||
|
|
@ -682,7 +705,7 @@ void calculate_simplifications(void)
|
|||
\
|
||||
if (bin_cost < lookup[bin_truthtable].cost) \
|
||||
{ \
|
||||
if (todo.reverse[bin_truthtable] == -1) \
|
||||
if (todo->reverse[bin_truthtable] == -1) \
|
||||
append(bin_truthtable, bin_cost); \
|
||||
else \
|
||||
update(bin_truthtable, bin_cost); \
|
||||
|
|
@ -700,7 +723,7 @@ void calculate_simplifications(void)
|
|||
\
|
||||
if (bin_cost < lookup[bin_truthtable].cost) \
|
||||
{ \
|
||||
if (todo.reverse[bin_truthtable] == -1) \
|
||||
if (todo->reverse[bin_truthtable] == -1) \
|
||||
append(bin_truthtable, bin_cost); \
|
||||
else \
|
||||
update(bin_truthtable, bin_cost); \
|
||||
|
|
@ -790,9 +813,9 @@ void calculate_simplifications(void)
|
|||
|
||||
if (use_operators.ternary)
|
||||
{
|
||||
for (int i = done.head; i != -1; i = done.next[i])
|
||||
for (int i = done->head; i != -1; i = done->next[i])
|
||||
{
|
||||
for (int j = done.head; j != -1; j = done.next[j])
|
||||
for (int j = done->head; j != -1; j = done->next[j])
|
||||
{
|
||||
int ternary_cost = 1 + cost + lookup[i].cost + lookup[j].cost;
|
||||
|
||||
|
|
@ -803,7 +826,7 @@ void calculate_simplifications(void)
|
|||
\
|
||||
if (ternary_cost < lookup[ternary_truthtable].cost) \
|
||||
{ \
|
||||
if (todo.reverse[ternary_truthtable] == -1) \
|
||||
if (todo->reverse[ternary_truthtable] == -1) \
|
||||
{ \
|
||||
append(ternary_truthtable, ternary_cost); \
|
||||
} \
|
||||
|
|
@ -825,17 +848,13 @@ void calculate_simplifications(void)
|
|||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (verbose && print_with_color)
|
||||
{
|
||||
printf("\e[2K" "\e[?7h");
|
||||
#endif
|
||||
}
|
||||
}
|
||||
|
||||
void get_simplifications(void)
|
||||
{
|
||||
char path[PATH_MAX] = ".simplifier-cache-2";
|
||||
char path[PATH_MAX] = ".simplifier-cache-5-var";
|
||||
|
||||
if (use_operators.not)
|
||||
strcat(path, "-not");
|
||||
|
|
@ -948,6 +967,8 @@ void get_simplifications(void)
|
|||
|
||||
uint16_t evaluate(const char* text)
|
||||
{
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
enum {
|
||||
tk_uninitialized,
|
||||
|
||||
|
|
@ -1435,16 +1456,22 @@ uint16_t evaluate(const char* text)
|
|||
}
|
||||
|
||||
return truthtable;
|
||||
#endif
|
||||
}
|
||||
|
||||
int main(int argc, char* const* argv)
|
||||
{
|
||||
parse_args(argc, argv);
|
||||
|
||||
todo = malloc(sizeof(*todo));
|
||||
done = malloc(sizeof(*done));
|
||||
|
||||
get_simplifications();
|
||||
|
||||
if (print_all_and_quit)
|
||||
{
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
for (int i = 0; i < N; i++)
|
||||
{
|
||||
int cost = lookup[i].cost;
|
||||
|
|
@ -1454,9 +1481,12 @@ int main(int argc, char* const* argv)
|
|||
printf("0b%016b: [%2i]: ", i, cost), print(i, 0), puts("");
|
||||
}
|
||||
}
|
||||
#endif
|
||||
}
|
||||
else if (print_stats)
|
||||
{
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
printf("statistics:" "\n");
|
||||
|
||||
uintmax_t total_cost = 0;
|
||||
|
|
@ -1509,9 +1539,12 @@ int main(int argc, char* const* argv)
|
|||
{
|
||||
puts("everything unreachable: no statistics to give");
|
||||
}
|
||||
#endif
|
||||
}
|
||||
else if (command)
|
||||
{
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
uint16_t truthtable = evaluate(command);
|
||||
|
||||
// printf("truthtable = 0b%016b\n", truthtable);
|
||||
|
|
@ -1524,9 +1557,12 @@ int main(int argc, char* const* argv)
|
|||
{
|
||||
printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts("");
|
||||
}
|
||||
#endif
|
||||
}
|
||||
else
|
||||
{
|
||||
assert(!"TODO");
|
||||
#if 0
|
||||
if (!quiet)
|
||||
{
|
||||
puts("Use C-style syntax for boolean operators and expressions.");
|
||||
|
|
@ -1556,6 +1592,7 @@ int main(int argc, char* const* argv)
|
|||
print(truthtable, 0), puts("");
|
||||
}
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
return 0;
|
||||
|
|
|
|||
Loading…
Reference in a new issue