.
This commit is contained in:
parent
d3ae35ceb5
commit
9183961738
3 changed files with 269 additions and 161 deletions
8
.gitignore
vendored
8
.gitignore
vendored
|
|
@ -3,3 +3,11 @@ simplifications.bin
|
|||
|
||||
.simplifier-*.bin
|
||||
|
||||
vgcore.*
|
||||
|
||||
.direnv/
|
||||
.simplifications.bin
|
||||
.~lock.stats.ods#
|
||||
*~
|
||||
stats.ods
|
||||
|
||||
|
|
|
|||
420
main.c
420
main.c
|
|
@ -182,7 +182,8 @@ static void parse_args(int argc, char* const* argv)
|
|||
#define N (65536)
|
||||
|
||||
enum kind {
|
||||
ek_undef,
|
||||
ek_unreachable,
|
||||
|
||||
ek_0,
|
||||
ek_1,
|
||||
ek_W,
|
||||
|
|
@ -215,11 +216,10 @@ struct expr {
|
|||
enum kind kind;
|
||||
|
||||
uint16_t cond, left, right;
|
||||
|
||||
int cost;
|
||||
} lookup[N];
|
||||
|
||||
// truthtable -> cost
|
||||
int costs[N] = {};
|
||||
|
||||
static void print(uint16_t truthtable, int depth)
|
||||
{
|
||||
#define LITERAL_ESCAPE "\e[38;2;200;200;100m"
|
||||
|
|
@ -243,10 +243,12 @@ static void print(uint16_t truthtable, int depth)
|
|||
|
||||
switch (e->kind)
|
||||
{
|
||||
case ek_undef:
|
||||
case ek_unreachable:
|
||||
{
|
||||
assert(!"NOPE");
|
||||
break;
|
||||
|
||||
}
|
||||
|
||||
case ek_0:
|
||||
{
|
||||
printf(print_with_color ? LITERAL_ESCAPE "0" RESET_ESCAPE : "0");
|
||||
|
|
@ -364,34 +366,46 @@ static void print(uint16_t truthtable, int depth)
|
|||
|
||||
void calculate_simplifications(void)
|
||||
{
|
||||
// heap of truthtables; key = cost
|
||||
uint16_t todo[N];
|
||||
int todo_n = 0;
|
||||
|
||||
// truthtable -> index in 'todo'
|
||||
int reverse[N];
|
||||
|
||||
// init:
|
||||
for (int i = 0; i < N; i++)
|
||||
// init 'lookup':
|
||||
{
|
||||
lookup[i].kind = ek_undef;
|
||||
|
||||
reverse[i] = -1;
|
||||
|
||||
costs[i] = INT_MAX;
|
||||
for (int i = 0; i < N; i++)
|
||||
{
|
||||
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;
|
||||
|
||||
for (int i = 0; i < N; i++)
|
||||
{
|
||||
todo.reverse[i] = -1;
|
||||
}
|
||||
}
|
||||
|
||||
uint16_t pop(void)
|
||||
{
|
||||
assert(todo_n > 0);
|
||||
assert(todo.n > 0);
|
||||
|
||||
uint16_t retval = todo[0];
|
||||
uint16_t retval = todo.data[0];
|
||||
|
||||
reverse[retval] = -1;
|
||||
todo.reverse[retval] = -1;
|
||||
|
||||
uint16_t moving = todo[todo_n-- - 1];
|
||||
uint16_t moving = todo.data[todo.n-- - 1];
|
||||
|
||||
int cost = costs[moving];
|
||||
int cost = lookup[moving].cost;
|
||||
|
||||
int index = 0;
|
||||
|
||||
|
|
@ -402,25 +416,25 @@ void calculate_simplifications(void)
|
|||
|
||||
uint16_t smallest = moving;
|
||||
|
||||
if (left < todo_n && costs[todo[left]] < cost)
|
||||
smallest = todo[left];
|
||||
if (left < todo.n && lookup[todo.data[left]].cost < cost)
|
||||
smallest = todo.data[left];
|
||||
|
||||
if (right < todo_n && costs[todo[right]] < costs[smallest])
|
||||
smallest = todo[right];
|
||||
if (right < todo.n && lookup[todo.data[right]].cost < lookup[smallest].cost)
|
||||
smallest = todo.data[right];
|
||||
|
||||
if (smallest == moving)
|
||||
{
|
||||
todo[index] = moving;
|
||||
todo.data[index] = moving;
|
||||
|
||||
reverse[moving] = index;
|
||||
todo.reverse[moving] = index;
|
||||
}
|
||||
else
|
||||
{
|
||||
int new = reverse[smallest];
|
||||
int new = todo.reverse[smallest];
|
||||
|
||||
todo[index] = smallest;
|
||||
todo.data[index] = smallest;
|
||||
|
||||
reverse[smallest] = index;
|
||||
todo.reverse[smallest] = index;
|
||||
|
||||
index = new;
|
||||
|
||||
|
|
@ -433,73 +447,176 @@ void calculate_simplifications(void)
|
|||
|
||||
void append(uint16_t truthtable, int cost)
|
||||
{
|
||||
assert(reverse[truthtable] == -1);
|
||||
assert(todo.reverse[truthtable] == -1);
|
||||
|
||||
int index = todo_n++, new_index;
|
||||
int index = todo.n++, new_index;
|
||||
|
||||
while (index > 0 && costs[todo[new_index = (index - 1) / 2]] > cost)
|
||||
while (index > 0 && lookup[todo.data[new_index = (index - 1) / 2]].cost > cost)
|
||||
{
|
||||
todo[index] = todo[new_index];
|
||||
todo.data[index] = todo.data[new_index];
|
||||
|
||||
reverse[todo[new_index]] = index;
|
||||
todo.reverse[todo.data[new_index]] = index;
|
||||
|
||||
index = new_index;
|
||||
}
|
||||
|
||||
todo[index] = truthtable;
|
||||
|
||||
reverse[truthtable] = index;
|
||||
|
||||
costs[truthtable] = cost;
|
||||
|
||||
todo.data[index] = truthtable;
|
||||
|
||||
todo.reverse[truthtable] = index;
|
||||
|
||||
lookup[truthtable].cost = cost;
|
||||
}
|
||||
|
||||
void update(uint16_t truthtable, int cost)
|
||||
{
|
||||
assert(reverse[truthtable] != -1);
|
||||
assert(todo.reverse[truthtable] != -1);
|
||||
|
||||
assert(cost < costs[truthtable]);
|
||||
assert(cost < lookup[truthtable].cost);
|
||||
|
||||
int index = reverse[truthtable], new_index;
|
||||
int index =todo. reverse[truthtable], new_index;
|
||||
|
||||
while (index > 0 && costs[todo[new_index = (index - 1) / 2]] > cost)
|
||||
while (index > 0 && lookup[todo.data[new_index = (index - 1) / 2]].cost > cost)
|
||||
{
|
||||
todo[index] = todo[new_index];
|
||||
todo.data[index] = todo.data[new_index];
|
||||
|
||||
reverse[todo[new_index]] = index;
|
||||
todo.reverse[todo.data[new_index]] = index;
|
||||
|
||||
index = new_index;
|
||||
}
|
||||
|
||||
todo[index] = truthtable;
|
||||
reverse[truthtable] = index;
|
||||
todo.data[index] = truthtable;
|
||||
todo.reverse[truthtable] = index;
|
||||
|
||||
costs[truthtable] = cost;
|
||||
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;
|
||||
|
||||
for (int i = 0; i < N; i++)
|
||||
{
|
||||
done.headtails[i] = -1;
|
||||
|
||||
#if ZDEBUG
|
||||
done.in[i] = false;
|
||||
#endif
|
||||
}
|
||||
}
|
||||
|
||||
void insert(int index)
|
||||
{
|
||||
#if ZDEBUG
|
||||
assert(!done.in[index]);
|
||||
#endif
|
||||
|
||||
int head = index & 1 ? index & ~(index & -index) : index, prevhead = -1;
|
||||
|
||||
while (done.headtails[head] == -1 || index < done.headtails[head])
|
||||
{
|
||||
done.headtails[head] = index;
|
||||
|
||||
prevhead = head, head = head & ~(head & -head);
|
||||
}
|
||||
|
||||
if (done.headtails[head] < index)
|
||||
{
|
||||
if (prevhead == -1)
|
||||
{
|
||||
assert(done.headtails[head] == head);
|
||||
|
||||
done.next[head] = index;
|
||||
}
|
||||
else
|
||||
{
|
||||
int tophalftail = done.headtails[prevhead - 1];
|
||||
|
||||
assert(tophalftail != -1);
|
||||
|
||||
done.next[tophalftail] = index;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
done.head = index;
|
||||
}
|
||||
|
||||
int n = ~index & M;
|
||||
int tail = index & 1 ? index : index | (n & -n), prevtail = -1;
|
||||
|
||||
while (done.headtails[tail] == -1 || done.headtails[tail] < index)
|
||||
{
|
||||
done.headtails[tail] = index;
|
||||
|
||||
prevtail = tail, tail = tail | (n = ~tail & M, n & -n);
|
||||
}
|
||||
|
||||
if (index < done.headtails[tail])
|
||||
{
|
||||
if (prevtail == -1)
|
||||
{
|
||||
assert(done.headtails[tail] == tail);
|
||||
|
||||
#if ZDEBUG
|
||||
assert(done.in[tail]);
|
||||
#endif
|
||||
|
||||
done.next[index] = tail;
|
||||
}
|
||||
else
|
||||
{
|
||||
int bottomhalfhead = done.headtails[prevtail + 1];
|
||||
|
||||
assert(bottomhalfhead != -1);
|
||||
|
||||
done.next[index] = bottomhalfhead;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
done.next[index] = -1;
|
||||
}
|
||||
|
||||
#if ZDEBUG
|
||||
done.in[index] = true;
|
||||
#endif
|
||||
}
|
||||
|
||||
append(W, 0), lookup[W].kind = ek_W;
|
||||
append(X, 0), lookup[X].kind = ek_X;
|
||||
append(Y, 0), lookup[Y].kind = ek_Y;
|
||||
append(Z, 0), lookup[Z].kind = ek_Z;
|
||||
|
||||
|
||||
append(0, 1), lookup[0].kind = ek_0;
|
||||
append(M, 1), lookup[M].kind = ek_1;
|
||||
|
||||
while (todo_n)
|
||||
|
||||
for (int iterations = 1; todo.n && iterations <= N; iterations++)
|
||||
{
|
||||
uint16_t truthtable = pop();
|
||||
|
||||
int cost = costs[truthtable];
|
||||
|
||||
insert(truthtable);
|
||||
|
||||
int cost = lookup[truthtable].cost;
|
||||
|
||||
if (verbose)
|
||||
{
|
||||
int left = N - todo_n;
|
||||
|
||||
if (print_with_color)
|
||||
{
|
||||
printf("\e[2K");
|
||||
}
|
||||
|
||||
printf("%i of %i (%.2f%%): [%i] ", left, N, (100.0 * left / N), cost);
|
||||
printf("%i of %i (%.2f%%): [%i] ",
|
||||
iterations, N, (100.0 * iterations / N), cost);
|
||||
|
||||
print(truthtable, 0), puts("");
|
||||
|
||||
|
|
@ -516,9 +633,9 @@ void calculate_simplifications(void)
|
|||
|
||||
int not_cost = cost + 1;
|
||||
|
||||
if (not_cost < costs[not_truthtable])
|
||||
if (not_cost < lookup[not_truthtable].cost)
|
||||
{
|
||||
if (reverse[not_truthtable] == -1)
|
||||
if (todo.reverse[not_truthtable] == -1)
|
||||
{
|
||||
append(not_truthtable, not_cost);
|
||||
}
|
||||
|
|
@ -534,44 +651,41 @@ void calculate_simplifications(void)
|
|||
|
||||
#define BINARY_OPERATOR(ekind, function) \
|
||||
{ \
|
||||
for (int i = 0; i < N; i++) \
|
||||
for (int i = done.head; i != -1; i = done.next[i]) \
|
||||
{ \
|
||||
if (costs[i] != INT_MAX) \
|
||||
{ \
|
||||
uint16_t bin_truthtable = function(truthtable, i) & M; \
|
||||
\
|
||||
int bin_cost = 1 + cost + lookup[i].cost; \
|
||||
\
|
||||
if (bin_cost < lookup[bin_truthtable].cost) \
|
||||
{ \
|
||||
uint16_t bin_truthtable = function(truthtable, i) & M; \
|
||||
if (todo.reverse[bin_truthtable] == -1) \
|
||||
append(bin_truthtable, bin_cost); \
|
||||
else \
|
||||
update(bin_truthtable, bin_cost); \
|
||||
\
|
||||
int bin_cost = 1 + cost + costs[i]; \
|
||||
\
|
||||
if (bin_cost < costs[bin_truthtable]) \
|
||||
{ \
|
||||
if (reverse[bin_truthtable] == -1) \
|
||||
append(bin_truthtable, bin_cost); \
|
||||
else \
|
||||
update(bin_truthtable, bin_cost); \
|
||||
\
|
||||
lookup[bin_truthtable].kind = ekind; \
|
||||
lookup[bin_truthtable].left = truthtable; \
|
||||
lookup[bin_truthtable].right = i; \
|
||||
} \
|
||||
lookup[bin_truthtable].kind = ekind; \
|
||||
lookup[bin_truthtable].left = truthtable; \
|
||||
lookup[bin_truthtable].right = i; \
|
||||
} \
|
||||
\
|
||||
} \
|
||||
\
|
||||
{ \
|
||||
uint16_t bin_truthtable = function(i, truthtable) & M; \
|
||||
\
|
||||
int bin_cost = 1 + cost + lookup[i].cost; \
|
||||
\
|
||||
if (bin_cost < lookup[bin_truthtable].cost) \
|
||||
{ \
|
||||
uint16_t bin_truthtable = function(i, truthtable) & M; \
|
||||
if (todo.reverse[bin_truthtable] == -1) \
|
||||
append(bin_truthtable, bin_cost); \
|
||||
else \
|
||||
update(bin_truthtable, bin_cost); \
|
||||
\
|
||||
int bin_cost = 1 + cost + costs[i]; \
|
||||
\
|
||||
if (bin_cost < costs[bin_truthtable]) \
|
||||
{ \
|
||||
if (reverse[bin_truthtable] == -1) \
|
||||
append(bin_truthtable, bin_cost); \
|
||||
else \
|
||||
update(bin_truthtable, bin_cost); \
|
||||
\
|
||||
lookup[bin_truthtable].kind = ekind; \
|
||||
lookup[bin_truthtable].left = i; \
|
||||
lookup[bin_truthtable].right = truthtable; \
|
||||
} \
|
||||
lookup[bin_truthtable].kind = ekind; \
|
||||
lookup[bin_truthtable].left = i; \
|
||||
lookup[bin_truthtable].right = truthtable; \
|
||||
} \
|
||||
} \
|
||||
} \
|
||||
|
|
@ -654,44 +768,38 @@ void calculate_simplifications(void)
|
|||
|
||||
if (use_operators.ternary)
|
||||
{
|
||||
for (int i = 0; i < N; i++)
|
||||
for (int i = done.head; i != -1; i = done.next[i])
|
||||
{
|
||||
if (costs[i] != INT_MAX)
|
||||
for (int j = done.head; j != -1; j = done.next[j])
|
||||
{
|
||||
for (int j = 0; j < N; j++)
|
||||
{
|
||||
if (costs[j] != INT_MAX)
|
||||
{
|
||||
int ternary_cost = 1 + cost + costs[i] + costs[j];
|
||||
int ternary_cost = 1 + cost + lookup[i].cost + lookup[j].cost;
|
||||
|
||||
#define TERNARY(C, T, F) \
|
||||
#define TERNARY(C, T, F) \
|
||||
{ \
|
||||
uint16_t ternary_truthtable = \
|
||||
((C) & (T)) | (~(C) & (F)); \
|
||||
\
|
||||
if (ternary_cost < lookup[ternary_truthtable].cost) \
|
||||
{ \
|
||||
if (todo.reverse[ternary_truthtable] == -1) \
|
||||
{ \
|
||||
uint16_t ternary_truthtable = \
|
||||
((C) & (T)) | (~(C) & (F)); \
|
||||
\
|
||||
if (ternary_cost < costs[ternary_truthtable]) \
|
||||
{ \
|
||||
if (reverse[ternary_truthtable] == -1) \
|
||||
{ \
|
||||
append(ternary_truthtable, ternary_cost); \
|
||||
} \
|
||||
else \
|
||||
{ \
|
||||
update(ternary_truthtable, ternary_cost); \
|
||||
} \
|
||||
\
|
||||
lookup[ternary_truthtable].kind = ek_ternary; \
|
||||
lookup[ternary_truthtable].cond = (C); \
|
||||
lookup[ternary_truthtable].left = (T); \
|
||||
lookup[ternary_truthtable].right = (F); \
|
||||
} \
|
||||
append(ternary_truthtable, ternary_cost); \
|
||||
} \
|
||||
else \
|
||||
{ \
|
||||
update(ternary_truthtable, ternary_cost); \
|
||||
} \
|
||||
\
|
||||
lookup[ternary_truthtable].kind = ek_ternary; \
|
||||
lookup[ternary_truthtable].cond = (C); \
|
||||
lookup[ternary_truthtable].left = (T); \
|
||||
lookup[ternary_truthtable].right = (F); \
|
||||
} \
|
||||
} \
|
||||
|
||||
TERNARY(truthtable, i, j);
|
||||
TERNARY(i, truthtable, j);
|
||||
TERNARY(i, j, truthtable);
|
||||
}
|
||||
}
|
||||
TERNARY(truthtable, i, j);
|
||||
TERNARY(i, truthtable, j);
|
||||
TERNARY(i, j, truthtable);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -705,7 +813,7 @@ void calculate_simplifications(void)
|
|||
|
||||
void get_simplifications(void)
|
||||
{
|
||||
char path[PATH_MAX] = ".simplifier-cache";
|
||||
char path[PATH_MAX] = ".simplifier-cache-2";
|
||||
|
||||
if (use_operators.not)
|
||||
strcat(path, "-not");
|
||||
|
|
@ -766,12 +874,6 @@ void get_simplifications(void)
|
|||
printf("%s: read() to cache failed: %m\n", argv0);
|
||||
exit(1);
|
||||
}
|
||||
|
||||
if (read(fd, costs, sizeof(costs)) < (ssize_t) sizeof(costs))
|
||||
{
|
||||
printf("%s: read() to cache failed: %m\n", argv0);
|
||||
exit(1);
|
||||
}
|
||||
}
|
||||
else if (fd < 0 && errno == ENOENT)
|
||||
{
|
||||
|
|
@ -806,12 +908,6 @@ void get_simplifications(void)
|
|||
printf("%s: write() to cache failed: %m\n", argv0);
|
||||
exit(1);
|
||||
}
|
||||
|
||||
if (write(fd, costs, sizeof(costs)) < (ssize_t) sizeof(costs))
|
||||
{
|
||||
printf("%s: write() to cache failed: %m\n", argv0);
|
||||
exit(1);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -1326,7 +1422,7 @@ int main(int argc, char* const* argv)
|
|||
{
|
||||
for (int i = 0; i < N; i++)
|
||||
{
|
||||
int cost = costs[i];
|
||||
int cost = lookup[i].cost;
|
||||
|
||||
if (cost != INT_MAX)
|
||||
{
|
||||
|
|
@ -1340,48 +1436,52 @@ int main(int argc, char* const* argv)
|
|||
|
||||
// printf("truthtable = 0b%016b\n", truthtable);
|
||||
|
||||
if (costs[truthtable] == INT_MAX)
|
||||
if (lookup[truthtable].kind == ek_unreachable)
|
||||
{
|
||||
puts("unreachable");
|
||||
}
|
||||
else
|
||||
{
|
||||
printf("%2i: ", costs[truthtable]), print(truthtable, 0), puts("");
|
||||
printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts("");
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
int max_cost = 0;
|
||||
|
||||
for (int i = 0; i < N; i++)
|
||||
// Let's humble-brag just a little.
|
||||
{
|
||||
int cost = costs[i];
|
||||
int max_cost = 0;
|
||||
|
||||
if (cost != INT_MAX && max_cost < cost)
|
||||
for (int i = 0; i < N; i++)
|
||||
{
|
||||
max_cost = cost;
|
||||
int cost = lookup[i].cost;
|
||||
|
||||
if (cost != INT_MAX && max_cost < cost)
|
||||
{
|
||||
max_cost = cost;
|
||||
}
|
||||
}
|
||||
|
||||
puts("");
|
||||
printf("I can simplify any tree down to %i operators or less.\n",
|
||||
max_cost);
|
||||
puts("");
|
||||
}
|
||||
|
||||
// we subtract 4 from the cost because
|
||||
puts("");
|
||||
printf("I can simplify any tree down to %i operators or less.\n",
|
||||
max_cost);
|
||||
puts("");
|
||||
|
||||
|
||||
for (char* line; (line = readline(">>> ")); free(line))
|
||||
{
|
||||
add_history(line);
|
||||
|
||||
uint16_t truthtable = evaluate(line);
|
||||
|
||||
// printf("truthtable = 0b%016b\n", truthtable);
|
||||
|
||||
if (costs[truthtable] == INT_MAX)
|
||||
if (lookup[truthtable].kind == ek_unreachable)
|
||||
{
|
||||
puts("unreachable");
|
||||
}
|
||||
else
|
||||
{
|
||||
printf("%2i: ", costs[truthtable]), print(truthtable, 0), puts("");
|
||||
printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts("");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
2
makefile
2
makefile
|
|
@ -6,7 +6,7 @@ args =
|
|||
cc = gcc
|
||||
|
||||
cppflags += -D _GNU_SOURCE
|
||||
#cppflags += -D ZDEBUG
|
||||
#cppflags += -D ZDEBUG=1
|
||||
|
||||
cflags = -Werror -Wall -Wextra -Wstrict-prototypes -Wfatal-errors
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue