From 1b9fe3b44a5d532a2c21bdf0c83196f7b92f80ba Mon Sep 17 00:00:00 2001 From: Zander Thannhauser Date: Fri, 27 Jun 2025 14:54:26 -0500 Subject: [PATCH] . --- calculate_simplifications.c | 488 +++++++++++++++-------------------- debug.h | 15 +- get_cached_simplifications.c | 42 ++- get_cached_simplifications.h | 2 +- main.c | 2 + makefile | 2 +- simplifications.h | 4 +- 7 files changed, 259 insertions(+), 296 deletions(-) diff --git a/calculate_simplifications.c b/calculate_simplifications.c index 6e780b0..b0b86c6 100644 --- a/calculate_simplifications.c +++ b/calculate_simplifications.c @@ -11,120 +11,112 @@ #include "calculate_simplifications.h" - -static void init_simplifications( - struct simplifications* simps) +struct simplifications calculate_simplifications( + const struct cmdln_flags* flags) { - for (int i = 0; i < N; i++) + struct simplifications simps = {}; + + // init 'simps.data': { - simps->data[i].kind = ek_unreachable; + for (int i = 0; i < N; i++) + { + simps.data[i].kind = ek_unreachable; + + simps.data[i].cost = INT_MAX; + } + } + + // heap of truthtables; key = cost + struct { + uint16_t data[N]; + int n; - simps->data[i].cost = INT_MAX; - } -} - -struct heap -{ - uint16_t data[N]; - int n; + // truthtable -> index in 'todo' + int reverse[N]; + } todo; - // truthtable -> index in 'todo' - int reverse[N]; -}; - -static struct heap new_heap(void) -{ - zprintf("new_heap" "\n"); - - struct heap todo = {}; - - todo.n = 0; - - for (int i = 0; i < N; i++) + // init 'todo': { - todo.reverse[i] = -1; - } - - return todo; -} - - -uint16_t heap_pop(struct heap* todo, struct simplifications *simps) -{ - assert(todo->n > 0); - - uint16_t retval = todo->data[0]; - - todo->reverse[retval] = -1; - - uint16_t moving = todo->data[todo->n-- - 1]; - - int cost = simps->data[moving].cost; - - int index = 0; - - again: - { - int left = index * 2 + 1; - int right = index * 2 + 2; - - uint16_t smallest = moving; - - if (left < todo->n && simps->data[todo->data[left]].cost < cost) - smallest = todo->data[left]; - - if (right < todo->n && simps->data[todo->data[right]].cost < simps->data[smallest].cost) - smallest = todo->data[right]; - - if (smallest == moving) + todo.n = 0; + + for (int i = 0; i < N; i++) { - todo->data[index] = moving; - - todo->reverse[moving] = index; - } - else - { - int new = todo->reverse[smallest]; - - todo->data[index] = smallest; - - todo->reverse[smallest] = index; - - index = new; - - goto again; + todo.reverse[i] = -1; } } - - return retval; -} - - -void heap_append(struct heap* todo, struct simplifications* simps, uint16_t truthtable, int cost) -{ - zprintf("heap_append()" "\n"); - assert(todo->reverse[truthtable] == -1); - - int index = todo->n++, new_index; - - while (index > 0 && simps->data[todo->data[new_index = (index - 1) / 2]].cost > cost) + uint16_t pop(void) { - todo->data[index] = todo->data[new_index]; + assert(todo.n > 0); - todo->reverse[todo->data[new_index]] = index; + uint16_t retval = todo.data[0]; - index = new_index; + todo.reverse[retval] = -1; + + uint16_t moving = todo.data[todo.n-- - 1]; + + int cost = simps.data[moving].cost; + + int index = 0; + + again: + { + int left = index * 2 + 1; + int right = index * 2 + 2; + + uint16_t smallest = moving; + + if (left < todo.n && simps.data[todo.data[left]].cost < cost) + smallest = todo.data[left]; + + if (right < todo.n && simps.data[todo.data[right]].cost < simps.data[smallest].cost) + smallest = todo.data[right]; + + if (smallest == moving) + { + todo.data[index] = moving; + + todo.reverse[moving] = index; + } + else + { + int new = todo.reverse[smallest]; + + todo.data[index] = smallest; + + todo.reverse[smallest] = index; + + index = new; + + goto again; + } + } + + return retval; + } + + void append(uint16_t truthtable, int cost) + { + assert(todo.reverse[truthtable] == -1); + + int index = todo.n++, new_index; + + while (index > 0 && simps.data[todo.data[new_index = (index - 1) / 2]].cost > cost) + { + todo.data[index] = todo.data[new_index]; + + todo.reverse[todo.data[new_index]] = index; + + index = new_index; + } + + todo.data[index] = truthtable; + + todo.reverse[truthtable] = index; + + simps.data[truthtable].cost = cost; } - - todo->data[index] = truthtable; - - todo->reverse[truthtable] = index; - - simps->data[truthtable].cost = cost; -} -#if 0 void update(uint16_t truthtable, int cost) { assert(todo.reverse[truthtable] != -1); @@ -147,147 +139,134 @@ void heap_append(struct heap* todo, struct simplifications* simps, uint16_t trut simps.data[truthtable].cost = cost; } -#endif - - // create a list of the "done" truthtables -struct sparselist -{ - int headtails[N], next[N], head; - // for debugging: - #if ZDEBUG - bool in[N]; - #endif -}; - -struct sparselist new_sparselist(void) -{ - struct sparselist done = {}; + // create a list of the "done" truthtables + struct { + int headtails[N], next[N], head; + + // for debugging: + #if ZDEBUG + bool in[N]; + #endif + } done = {}; - done.head = -1; - - for (int i = 0; i < N; i++) + // init 'done': { - done.headtails[i] = -1; + 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[i] = false; + done.in[index] = true; #endif } - return done; -} - -void sparselist_insert(struct sparselist* this, int index) -{ - TODO; - #if 0 - #if ZDEBUG - assert(!done.in[index]); - #endif + append(W, 0), simps.data[W].kind = ek_W; + append(X, 0), simps.data[X].kind = ek_X; + append(Y, 0), simps.data[Y].kind = ek_Y; + append(Z, 0), simps.data[Z].kind = ek_Z; - 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 - #endif -} - - -static void loop( - const struct cmdln_flags* flags, - struct simplifications* simps, - struct heap* todo, - struct sparselist* done) -{ - zprintf("loop()" "\n"); + append(0, 1), simps.data[0].kind = ek_0; + append(M, 1), simps.data[M].kind = ek_1; // disable terminal autowrap: - if (!ZDEBUG && flags->verbose && flags->print_with_color) + if (flags->verbose && flags->print_with_color) { printf("\e[?7l"); } - for (int iterations = 1; todo->n && iterations <= N; iterations++) + for (int iterations = 1; todo.n && iterations <= N; iterations++) { - uint16_t truthtable = heap_pop(todo, simps); + uint16_t truthtable = pop(); - if (!done) - { - sparselist_insert(done, truthtable); - } + insert(truthtable); - int cost = simps->data[truthtable].cost; + int cost = simps.data[truthtable].cost; if (flags->verbose) { - if (!ZDEBUG && flags->print_with_color) + if (flags->print_with_color) { printf("\e[2K"); } @@ -295,16 +274,14 @@ static void loop( printf("%i of %i (%.2f%%): [%i] ", iterations, N, (100.0 * iterations / N), cost); - print(flags, &simps->data, truthtable), puts(""); + print(flags, &simps, truthtable), puts(""); - if (!ZDEBUG && flags->print_with_color) + if (flags->print_with_color) { printf("\e[1A"); } } - TODO - #if 0 // consider NOT: if (flags->use_operators.not) { @@ -482,72 +459,17 @@ static void loop( } } } - #endif } // clear progress line, enable terminal autowrap: - if (!ZDEBUG && flags->verbose && flags->print_with_color) + if (flags->verbose && flags->print_with_color) { printf("\e[2K"), printf("\e[?7h"); } + + return simps; } -struct simplifications calculate_simplifications( - const struct cmdln_flags* flags) -{ - zprintf("calculate_simplifications()" "\n"); - - struct simplifications simps = {}; - - init_simplifications(&simps); - - struct heap todo = new_heap(); - - struct sparselist done = new_sparselist(); - - heap_append(&todo, &simps, W, 0), simps.data[W].kind = ek_W; - heap_append(&todo, &simps, X, 0), simps.data[X].kind = ek_X; - heap_append(&todo, &simps, Y, 0), simps.data[Y].kind = ek_Y; - heap_append(&todo, &simps, Z, 0), simps.data[Z].kind = ek_Z; - - heap_append(&todo, &simps, 0, 1), simps.data[0].kind = ek_0; - heap_append(&todo, &simps, M, 1), simps.data[M].kind = ek_1; - - loop(flags, &simps, &todo, &done); - - TODO; -} - -struct simplifications calculate_simplifications_with_extra_variable( - const struct cmdln_flags* flags, - uint16_t A) -{ - zprintf("calculate_simplifications_with_extra_variable()" "\n"); - - #if 0 - - if (have_extra_variable && todo.reverse[A] == -1) - { - append(A, 0), simps.data[A].kind = ek_A; - } - - #endif - - TODO; -} - -void update_simplifications( - struct simplifications* simps, - const struct cmdln_flags* flags, - uint16_t starting_with) -{ - zprintf("update_simplifications()" "\n"); - - TODO; -} - -#if 0 - @@ -562,5 +484,3 @@ void update_simplifications( - -#endif diff --git a/debug.h b/debug.h index e1e92fc..dd62324 100644 --- a/debug.h +++ b/debug.h @@ -1,15 +1,20 @@ -#ifndef ZDEBUG - #define ZDEBUG 1 +#ifdef DEBUG_BUILD +extern int debug_depth; #endif -#if ZDEBUG - #define zprintf(fmt, ...) \ - printf(fmt, ## __VA_ARGS__); +#ifdef DEBUG_BUILD + #define zprintf(fmt, ...) printf("%*s" fmt, debug_depth, "", ## __VA_ARGS__); #else #define zprintf(...); #endif +#define ENTER \ + { zprintf("%s():" "\n", __PRETTY_FUNCTION__); debug_depth++; } + +#define EXIT \ + { zprintf("return" "\n"); debug_depth--; } + #define TODO \ assert(!"TODO"); diff --git a/get_cached_simplifications.c b/get_cached_simplifications.c index 266fc7f..1f0c998 100644 --- a/get_cached_simplifications.c +++ b/get_cached_simplifications.c @@ -83,16 +83,20 @@ static struct path { char data[PATH_MAX]; } get_path( return path; } -void get_cached_simplifications(const struct cmdln_flags* flags) +struct simplifications* get_cached_simplifications(const struct cmdln_flags* flags) { - zprintf("get_cached_simplifications()" "\n"); + ENTER; struct path path = get_path(flags); + zprintf("path.data = %s\n", path.data); + int fd = -1; bool rebuild = flags->force_rebuild; + struct simplifications* simps; + if (!rebuild) { fd = open(path.data, O_RDONLY); @@ -131,6 +135,7 @@ void get_cached_simplifications(const struct cmdln_flags* flags) if (rebuild) { + #ifndef DEBUG_BUILD if (!flags->quiet) { puts("" @@ -152,8 +157,9 @@ void get_cached_simplifications(const struct cmdln_flags* flags) puts("Any input to start:"), getchar(); puts("Started."); } + #endif - fd = open("/tmp/", O_RDWR | O_TMPFILE, 0664); + fd = open(".simplifier-cache-temp.bin", O_TRUNC | O_CREAT | O_RDWR, 0664); if (fd < 0) { @@ -161,8 +167,30 @@ void get_cached_simplifications(const struct cmdln_flags* flags) exit(1); } - struct simplifications simps = calculate_simplifications(flags); + if (ftruncate(fd, sizeof(*simps)) < 0) + { + TODO; + } + void* ptr = mmap( + /* addr: */ NULL, + /* len: */ sizeof(*simps), + /* prot: */ PROT_WRITE | PROT_READ, + /* flags: */ MAP_PRIVATE, + /* fd: */ fd, + /* offset: */ 0); + + if (ptr == MAP_FAILED) + { + TODO; + } + + simps = ptr; + + simps->initial = calculate_simplifications(flags); + + TODO; + #if 0 TODO; #if 0 if (flags->use_operators.assignment) @@ -228,8 +256,11 @@ void get_cached_simplifications(const struct cmdln_flags* flags) } #endif + #endif } + TODO; + #if 0 TODO; #if 0 assert(fd > 0); @@ -238,6 +269,9 @@ void get_cached_simplifications(const struct cmdln_flags* flags) return retval; #endif + #endif + + return simps; } diff --git a/get_cached_simplifications.h b/get_cached_simplifications.h index b55b084..6922f39 100644 --- a/get_cached_simplifications.h +++ b/get_cached_simplifications.h @@ -3,5 +3,5 @@ struct cmdln_flags; -void get_cached_simplifications(const struct cmdln_flags* flags); +struct simplifications* get_cached_simplifications(const struct cmdln_flags* flags); diff --git a/main.c b/main.c index b11c766..57e24ba 100644 --- a/main.c +++ b/main.c @@ -19,6 +19,8 @@ int main(int argc, char* const* argv) { + ENTER; + struct cmdln_flags flags = parse_args(argc, argv); get_cached_simplifications(&flags); diff --git a/makefile b/makefile index 2e98edc..192ebb5 100644 --- a/makefile +++ b/makefile @@ -14,7 +14,7 @@ default: ${prefix}/bsimp %/: @mkdir -p $@ -srcs += calculate_simplifications.c cmdln.c evaluate.c +srcs += calculate_simplifications.c cmdln.c evaluate.c debug.c srcs += get_cached_simplifications.c main.c print.c ${prefix}/%.o ${prefix}/%.d: %.c ${optionset} | ${prefix}/%/ diff --git a/simplifications.h b/simplifications.h index 73cd07d..4f9739b 100644 --- a/simplifications.h +++ b/simplifications.h @@ -8,7 +8,9 @@ struct simplifications { - struct expr data[N]; + struct row { + struct expr data[N]; + } initial, with_variables[N]; }; #endif