From 82db0d4e034218b12c15210fc60c992c8d653c73 Mon Sep 17 00:00:00 2001 From: Zander Thannhauser Date: Sat, 21 Jun 2025 12:04:53 -0500 Subject: [PATCH] turns out: we cant do 5 variables --- 5.c | 1986 +++++++++++++++++++++++++++++++++++++++++++++++++++++ flake.nix | 1 + main.py | 2 +- makefile | 4 +- 4 files changed, 1990 insertions(+), 3 deletions(-) create mode 100644 5.c diff --git a/5.c b/5.c new file mode 100644 index 0000000..44e8b9a --- /dev/null +++ b/5.c @@ -0,0 +1,1986 @@ + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include + +#define argv0 program_invocation_name + +#ifndef ZDEBUG +#define ZDEBUG 0 +#endif + +#if ZDEBUG + int calldepth = 0; + + #define zprintf(fmt, ...) \ + printf(fmt, ## __VA_ARGS__); +#else + #define zprintf(...); +#endif + +#define TODO \ + assert(!"TODO"); + +bool print_all_and_quit = false; + +const char* command = NULL; + +struct { + bool not; + + bool or, nor; + + bool and, nand; + + bool xor, nxor; + + bool compares; +} use_operators; + +bool assume_yes = false; + +bool verbose = false; + +bool print_with_color = false; + +bool force_rebuild = false; + +static void parse_args(int argc, char* const* argv) +{ + zprintf("%*s" "parse_args():" "\n", calldepth, ""); + + bool unset_operators = true; + + print_with_color = isatty(1); + + for (int opt; (opt = getopt(argc, argv, "pyvc:eo:C:B")) != -1; ) switch (opt) + { + case 'p': + print_all_and_quit = true; + break; + + case 'y': + assume_yes = true; + break; + + case 'v': + verbose = true; + break; + + case 'c': + command = optarg; + break; + + case 'e': + { + use_operators.not = true; + use_operators.or = true; + use_operators.and = true; + + use_operators.nor = true; + use_operators.nand = true; + + use_operators. xor = true; + use_operators.nxor = true; + + use_operators.compares = true; + + unset_operators = false; + break; + } + + case 'o': + { + unset_operators = false; + + for (char* moving; (moving = strtok_r(NULL, ",", &optarg)); ) + { + if (!strcmp(moving, "not") || !strcmp(moving, "!")) + use_operators.not = true; + else if (!strcmp(moving, "or") || !strcmp(moving, "||")) + use_operators.or = true; + else if (!strcmp(moving, "nor") || !strcmp(moving, "!|")) + use_operators.nor = true; + else if (!strcmp(moving, "and") || !strcmp(moving, "&&")) + use_operators.and = true; + else if (!strcmp(moving, "nand") || !strcmp(moving, "!&")) + use_operators.nand = true; + else if (!strcmp(moving, "xor") || !strcmp(moving, "!=")) + use_operators.xor = true; + else if (!strcmp(moving, "nxor") || !strcmp(moving, "==")) + use_operators.nxor = true; + else if (!strcmp(moving, "compares")) + use_operators.compares = true; + else + { + assert(!"TODO"); + } + } + break; + } + + case 'C': + { + if (!strcmp(optarg, "yes") || !strcmp(optarg, "on")) + print_with_color = true; + else if (!strcmp(optarg, "no") || !strcmp(optarg, "off")) + print_with_color = false; + else if (!strcmp(optarg, "auto")) + print_with_color = isatty(1); + else + { + assert(!"TODO"); + } + + break; + } + + case 'B': + { + force_rebuild = true; + + break; + } + + default: + assert(!"TODO"); + break; + } + + if (unset_operators) + { + use_operators.not = true; + use_operators.or = true; + use_operators.and = true; + } +} + +#define V 0b01010101010101010101010101010101 +#define W 0b00110011001100110011001100110011 +#define X 0b00001111000011110000111100001111 +#define Y 0b00000000111111110000000011111111 +#define Z 0b00000000000000001111111111111111 +#define M 0b11111111111111111111111111111111 + +#define B (32) + +#define N ((uint64_t) 1 << (B)) + +enum kind { + ek_unreachable, + + ek_0, + ek_1, + + ek_V, + ek_W, + ek_X, + ek_Y, + ek_Z, + + ek_not, + ek_or, + ek_and, + + ek_nor, + + ek_nand, + + ek_xor, + ek_nxor, + + ek_lt, + ek_lte, + ek_gt, + ek_gte, +}; + +struct expr { + enum kind kind; + + uint32_t cond, left, right; + + int cost; +} lookup[N]; + +static void print(uint32_t truthtable, int depth) +{ + #define LITERAL_ESCAPE "\e[38;2;200;200;100m" + #define VARIABLE_ESCAPE "\e[38;2;100;100;200m" + #define RESET_ESCAPE "\e[0m" + + static const char* const operator_colors[10] = { + "\e[38;2;204;0;0m", + "\e[38;2;204;122;0m", + "\e[38;2;163;204;0m", + "\e[38;2;40;204;0m", + "\e[38;2;0;204;81m", + "\e[38;2;0;204;204m", + "\e[38;2;0;81;204m", + "\e[38;2;40;0;204m", + "\e[38;2;163;0;204m", + "\e[38;2;204;0;122m", + }; + + const struct expr* e = &lookup[truthtable]; + + switch (e->kind) + { + case ek_unreachable: + { + assert(!"NOPE"); + break; + } + + case ek_0: + { + printf(print_with_color ? LITERAL_ESCAPE "0" RESET_ESCAPE : "0"); + break; + } + + case ek_1: + { + printf(print_with_color ? LITERAL_ESCAPE "1" RESET_ESCAPE : "1"); + break; + } + + case ek_V: + { + printf(print_with_color ? VARIABLE_ESCAPE "v" RESET_ESCAPE : "v"); + break; + } + + case ek_W: + { + printf(print_with_color ? VARIABLE_ESCAPE "w" RESET_ESCAPE : "w"); + break; + } + + case ek_X: + { + printf(print_with_color ? VARIABLE_ESCAPE "x" RESET_ESCAPE : "x"); + break; + } + + case ek_Y: + { + printf(print_with_color ? VARIABLE_ESCAPE "y" RESET_ESCAPE : "y"); + break; + } + + case ek_Z: + { + printf(print_with_color ? VARIABLE_ESCAPE "z" RESET_ESCAPE : "z"); + break; + } + + case ek_not: + { + const char* start = print_with_color ? operator_colors[depth % 10] : ""; + const char* end = print_with_color ? RESET_ESCAPE : ""; + + printf("%s(!%s", start, end); + + print(e->left, depth + 1); + + printf("%s)%s", start, end); + break; + } + + #define BINARY_OPERATOR(kind, operatorstring) \ + case kind: \ + { \ + const char *start = "", *end = ""; \ + \ + if (print_with_color) \ + { \ + start = operator_colors[depth % 10]; \ + \ + end = RESET_ESCAPE; \ + } \ + \ + printf("%s(%s", start, end); \ + \ + print(e->left, depth + 1); \ + \ + printf("%s%s%s", start, operatorstring, end); \ + \ + print(e->right, depth + 1); \ + \ + printf("%s)%s", start, end); \ + break; \ + } + + BINARY_OPERATOR(ek_or, " || "); + BINARY_OPERATOR(ek_nor, " !| "); + + BINARY_OPERATOR(ek_and, " && "); + BINARY_OPERATOR(ek_nand, " !& "); + + BINARY_OPERATOR(ek_xor, " != "); + BINARY_OPERATOR(ek_nxor, " == "); + + BINARY_OPERATOR(ek_lt, " < "); + BINARY_OPERATOR(ek_lte, " <= "); + + BINARY_OPERATOR(ek_gt, " < "); + BINARY_OPERATOR(ek_gte, " <= "); + + #undef BINARY_OPERATOR + } +} + +// heap of truthtables; key = cost +struct heap +{ + uint32_t data[N]; + long n; + + // truthtable -> index in 'todo' + long reverse[N]; +}; + +struct heap* new_heap(void) +{ + zprintf("%*s" "new_heap():" "\n", calldepth++, ""); + + struct heap* this = malloc(sizeof(*this)); + + this->n = 0; + + for (int i = 0; i < N; i++) + { + this->reverse[i] = -1; + } + + #if ZDEBUG + calldepth--; + #endif + + return this; +} + +uint32_t heap_pop(struct heap* this) +{ + zprintf("%*s" "heap_pop():" "\n", calldepth++, ""); + + assert(this->n > 0); + + uint32_t retval = this->data[0]; + + this->reverse[retval] = -1; + + uint32_t moving = this->data[this->n-- - 1]; + + int cost = lookup[moving].cost; + + long index = 0; + + again: + { + long left = index * 2 + 1; + long right = index * 2 + 2; + + uint32_t smallest = moving; + + if (left < this->n && lookup[this->data[left]].cost < cost) + smallest = this->data[left]; + + if (right < this->n && lookup[this->data[right]].cost < lookup[smallest].cost) + smallest = this->data[right]; + + if (smallest == moving) + { + this->data[index] = moving; + + this->reverse[moving] = index; + } + else + { + long new = this->reverse[smallest]; + + this->data[index] = smallest; + + this->reverse[smallest] = index; + + index = new; + + goto again; + } + } + + #if ZDEBUG + calldepth--; + #endif + + return retval; +} + +void heap_push(struct heap* this, uint32_t truthtable, int cost) +{ + zprintf("%*s" "heap_push():" "\n", calldepth++, ""); + + assert(this->reverse[truthtable] == -1); + + long index = this->n++, new_index; + + while (index > 0 && lookup[this->data[new_index = (index - 1) / 2]].cost > cost) + { + this->data[index] = this->data[new_index]; + + this->reverse[this->data[new_index]] = index; + + index = new_index; + } + + this->data[index] = truthtable; + + this->reverse[truthtable] = index; + + lookup[truthtable].cost = cost; + + #if ZDEBUG + calldepth--; + #endif +} + +void heap_update(struct heap* this, uint32_t truthtable, int cost) +{ + zprintf("%*s" "heap_update():" "\n", calldepth++, ""); + + assert(this->reverse[truthtable] != -1); + + assert(cost < lookup[truthtable].cost); + + long index = this->reverse[truthtable], new_index; + + while (index > 0 && lookup[this->data[new_index = (index - 1) / 2]].cost > cost) + { + this->data[index] = this->data[new_index]; + + this->reverse[this->data[new_index]] = index; + + index = new_index; + } + + this->data[index] = truthtable; + this->reverse[truthtable] = index; + + lookup[truthtable].cost = cost; + + #if ZDEBUG + calldepth--; + #endif +} + +// create a list truthtables we're done with +// and another list of truthtables we're still working on. +struct boolset +{ + int data[B][N]; +}; + +struct boolset* new_empty_boolset(void) +{ + zprintf("%*s" "new_empty_boolset():" "\n", calldepth++, ""); + + struct boolset* this = malloc(sizeof(*this)); + + for (long i = 0; i < B; i++) + { + for (long j = 0; j < N; j++) + { + this->data[i][j] = 0; + } + } + + #if ZDEBUG + calldepth--; + #endif + + return this; +} + +struct boolset* new_full_boolset(void) +{ + zprintf("%*s" "new_full_boolset():" "\n", calldepth++, ""); + + struct boolset* this = malloc(sizeof(*this)); + + long i, j; + + for (i = 0; i < B - 1; i++) + { + for (j = 0; j < N; j++) + { + this->data[i][j] = 2; + } + } + + for (j = 0; j < N; j++) + { + this->data[i][j] = 1; + } + + #if ZDEBUG + calldepth--; + #endif + + return this; +} + +void boolset_add(struct boolset* this, uint32_t e) +{ + zprintf("%*s" "boolset_add(e = 0b%hb):" "\n", calldepth++, "", e); + + assert(!this->data[0][e]); + + for (int k = 0; k < B && !this->data[k][e >> k]++; k++); + + #if ZDEBUG + calldepth--; + #endif +} + +void boolset_discard(struct boolset* this, uint32_t e) +{ + zprintf("%*s" "boolset_discard(e = 0b%hb):" "\n", calldepth++, "", e); + + assert(this->data[0][e]); + + for (int k = 0; k < B && !--this-> data[k][e >> k]; k++); + + #if ZDEBUG + calldepth--; + #endif +} + + +void calculate_simplifications(void) +{ + zprintf("%*s" "calculate_simplifications():" "\n", calldepth++, ""); + + // init 'lookup': + for (long i = 0; i < N; i++) + { + zprintf("%*s" "init lookup: i = %li" "\n", calldepth, "", i); + + lookup[i].kind = ek_unreachable; + + lookup[i].cost = INT_MAX; + } + + zprintf("%*s" "HERE: line %i" "\n", calldepth, "", __LINE__); + + // list of truthtables we're still working on, sorted by cost. + struct heap* todo = new_heap(); + + zprintf("%*s" "HERE: line %i" "\n", calldepth, "", __LINE__); + + // create a list truthtables we're done with + // and another list of truthtables we're still working on. + struct boolset* done = new_empty_boolset(); + struct boolset* undone = new_full_boolset(); + + zprintf("%*s" "HERE: line %i" "\n", calldepth, "", __LINE__); + + heap_push(todo, V, 0), lookup[V].kind = ek_V; + heap_push(todo, W, 0), lookup[W].kind = ek_W; + heap_push(todo, X, 0), lookup[X].kind = ek_X; + heap_push(todo, Y, 0), lookup[Y].kind = ek_Y; + heap_push(todo, Z, 0), lookup[Z].kind = ek_Z; + + heap_push(todo, 0, 1), lookup[0].kind = ek_0; + heap_push(todo, M, 1), lookup[M].kind = ek_1; + + for (long iterations = 1; todo->n && iterations <= N; iterations++) + { + zprintf("%*s" "iterations = %li" "\n", calldepth, "", iterations); + + uint32_t truthtable = heap_pop(todo); + + zprintf("%*s" "truthtable = %#hb" "\n", calldepth, "", truthtable); + + boolset_add(done, truthtable), boolset_discard(undone, truthtable); + + int cost = lookup[truthtable].cost; + + if (verbose) + { + if (!ZDEBUG && print_with_color) + { + printf("\e[2K"); + } + + printf("%li of %li (%.2f%%): [%i] ", iterations, N, (100.0 * (double) iterations / N), cost); + + print(truthtable, 0), puts(""); + + if (!ZDEBUG && print_with_color) + { + printf("\e[1A"); + } + } + + // consider NOT: + if (use_operators.not) + { + uint32_t not_truthtable = ~truthtable & M; + + int not_cost = cost + 1; + + if (not_cost < lookup[not_truthtable].cost) + { + if (todo->reverse[not_truthtable] == -1) + { + heap_push(todo, not_truthtable, not_cost); + } + else + { + heap_update(todo, not_truthtable, not_cost); + } + + lookup[not_truthtable].kind = ek_not; + lookup[not_truthtable].left = truthtable; + } + } + + #define CONSIDER(ekind) \ + { \ + int bin_cost = 1 + cost + lookup[bi].cost; \ + \ + if (bin_cost < lookup[ci].cost) \ + { \ + if (todo->reverse[ci] == -1) \ + { \ + heap_push(todo, ci, bin_cost); \ + } \ + else \ + { \ + heap_update(todo, ci, bin_cost); \ + } \ + \ + lookup[ci].kind = ekind; \ + lookup[ci].left = truthtable; \ + lookup[ci].right = bi; \ + } \ + } + + if (use_operators.or) + { + // a | b | c + //----------- + // 0 | 0 | 0 + // 0 | 1 | 1 + // 1 | 0 | 1 + // 1 | 1 | 1 + + void search(int k, uint32_t bi, uint32_t ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi, ci + (1 << k)); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + else + { + // done == 0 and undone == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi, ci); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + } + else + { + assert((truthtable | bi) == ci); + + zprintf("%*s" "(0b%016b | 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_or); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search(B - 1, 0, 0); + } + + if (use_operators.nor) + { + // a | b | c + //----------- + // 0 | 0 | 1 + // 0 | 1 | 0 + // 1 | 0 | 0 + // 1 | 1 | 0 + + void search(int k, uint32_t bi, uint32_t ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (0 << k), ci + (0 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + else + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + + (1 << k)]) + { + search(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + } + else + { + assert((~(truthtable | bi) & M) == ci); + + zprintf("%*s" "(0b%016b !| 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_nor); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search(B - 1, 0, 0); + } + + if (use_operators.and) + { + // a | b | c + //----------- + // 0 | 0 | 0 + // 0 | 1 | 0 + // 1 | 0 | 0 + // 1 | 1 | 1 + + void search(int k, uint32_t bi, uint32_t ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi, ci); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + else + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi, ci); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (1 << k), ci); + } + } + } + else + { + assert((truthtable & bi) == ci); + + zprintf("%*s" "(0b%016b & 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_and); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search(B - 1, 0, 0); + } + + #if 0 + if (use_operators.nand) + { + // a | b | c + //----------- + // 0 | 0 | 1 + // 0 | 1 | 1 + // 1 | 0 | 1 + // 1 | 1 | 0 + + void search(int k, int bi, int ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + else + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + } + else + { + assert(((~(truthtable & bi)) & M) == ci); + + zprintf("%*s" "(0b%016b !& 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_nand); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search(B - 1, 0, 0); + } + + if (use_operators.xor) + { + // a | b | c + //----------- + // 0 | 0 | 0 + // 0 | 1 | 1 + // 1 | 0 | 1 + // 1 | 1 | 0 + + void search(int k, int bi, int ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + else + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (0 << k), ci + (0 << k)); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + } + else + { + assert(((truthtable ^ bi) & M) == ci); + + zprintf("%*s" "(0b%016b != 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_xor); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search(B - 1, 0, 0); + } + + if (use_operators.nxor) + { + // a | b | c + //----------- + // 0 | 0 | 1 + // 0 | 1 | 0 + // 1 | 0 | 0 + // 1 | 1 | 1 + + void search(int k, int bi, int ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (0 << k), ci + (0 << k)); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + else + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + } + else + { + assert((~(truthtable ^ bi) & M) == ci); + + zprintf("%*s" "(0b%016b == 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_nxor); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search(B - 1, 0, 0); + } + + if (use_operators.compares) + { + // < + // a | b | c + //----------- + // 0 | 0 | 0 + // 0 | 1 | 1 + // 1 | 0 | 0 + // 1 | 1 | 0 + + void search1(int k, int bi, int ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search1(k - 1, bi + (0 << k), ci + (0 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search1(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + else + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search1(k - 1, bi + (0 << k), ci + (0 << k)); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search1(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + } + else + { + assert(((~truthtable & bi) & M) == ci); + + zprintf("%*s" "(0b%016b < 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_lt); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search1(B - 1, 0, 0); + + // <= + // a | b | c + //----------- + // 0 | 0 | 1 + // 0 | 1 | 1 + // 1 | 0 | 0 + // 1 | 1 | 1 + + void search2(int k, int bi, int ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search2(k - 1, bi + (0 << k), ci + (0 << k)); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search2(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + else + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search2(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search2(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + } + else + { + assert(((~truthtable | bi) & M) == ci); + + zprintf("%*s" "(0b%016b <= 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_lte); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search2(B - 1, 0, 0); + + + // > + // a | b | c + //----------- + // 0 | 0 | 0 + // 0 | 1 | 0 + // 1 | 0 | 1 + // 1 | 1 | 0 + + void search3(int k, int bi, int ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search3(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search3(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + else + { + // b == 0 and c == 0 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 0]) + { + search3(k - 1, bi + (0 << k), ci + (0 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search3(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + } + else + { + assert(((truthtable & ~bi) & M) == ci); + + zprintf("%*s" "(0b%016b > 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_gt); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search3(B - 1, 0, 0); + + // >= + // a | b | c + //----------- + // 0 | 0 | 1 + // 0 | 1 | 0 + // 1 | 0 | 1 + // 1 | 1 | 1 + + void search4(int k, int bi, int ci) + { + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) + { + if (truthtable & (1 << k)) + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search4(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 1 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 1]) + { + search4(k - 1, bi + (1 << k), ci + (1 << k)); + } + } + else + { + // b == 0 and c == 1 + if (done->data[k][(bi >> k) + 0] && undone->data[k][(ci >> k) + 1]) + { + search4(k - 1, bi + (0 << k), ci + (1 << k)); + } + + // b == 1 and c == 0 + if (done->data[k][(bi >> k) + 1] && undone->data[k][(ci >> k) + 0]) + { + search4(k - 1, bi + (1 << k), ci + (0 << k)); + } + } + } + else + { + assert(((truthtable | ~bi) & M) == ci); + + zprintf("%*s" "(0b%016b >= 0b%016b) == 0b%016b" "\n", calldepth, "", truthtable, bi, ci); + + CONSIDER(ek_gte); + } + + #if ZDEBUG + calldepth--; + #endif + } + + search4(B - 1, 0, 0); + } + #endif + } + + if (verbose && !ZDEBUG && print_with_color) + { + printf("\e[2K"); + } + + free(todo), free(done), free(undone); + + #if ZDEBUG + calldepth--; + #endif +} + +void get_simplifications(void) +{ + char path[PATH_MAX] = ".simplifier-5-cache-3"; + + if (use_operators.not) + strcat(path, "-not"); + + if (use_operators.or) + strcat(path, "-or"); + + if (use_operators.nor) + strcat(path, "-nor"); + + if (use_operators.and) + strcat(path, "-and"); + + if (use_operators.nand) + strcat(path, "-nand"); + + if (use_operators.xor) + strcat(path, "-xor"); + + if (use_operators.nxor) + strcat(path, "-nxor"); + + if (use_operators.compares) + strcat(path, "-compares"); + + strcat(path, ".bin"); + + int fd = -1; + + if (force_rebuild) + { + goto rebuild; + } + else if ((fd = open(path, O_RDONLY)) > 0) + { + // great, just read it into memory + + if (read(fd, lookup, sizeof(lookup)) < (ssize_t) sizeof(lookup)) + { + printf("%s: read() to cache failed: %m\n", argv0); + exit(1); + } + } + else if (fd < 0 && errno == ENOENT) + { + puts("" + "Oh! looks like you're running this for the first time" "\n" + "I'll have to build up my cache of simplifications" "\n" + "I'll only have to do this once." "\n" + "\n" + "This may take a while." "\n" + ""); + + rebuild: {}; + + if (!verbose) + { + puts("re-run with '-v' to watch progress"); + } + + if (!assume_yes) + { + puts(""); + puts("any input to start:"), getchar(); + puts(""); + } + + calculate_simplifications(); + + fd = open(path, O_WRONLY | O_TRUNC | O_CREAT, 0664); + + if (write(fd, lookup, sizeof(lookup)) < (ssize_t) sizeof(lookup)) + { + printf("%s: write() to cache failed: %m\n", argv0); + exit(1); + } + } + else + { + // something else + assert(!"TODO"); + } + + if (fd > 0) + { + close(fd); + } +} + +uint32_t evaluate(const char* text) +{ + enum { + tk_uninitialized, + + tk_0, + tk_1, + + tk_w, + tk_x, + tk_y, + tk_z, + + tk_oparen, + tk_cparen, + + tk_emark, + tk_emarkequals, + tk_emarkvbar, + tk_emarkampersand, + + tk_equalsequals, + + tk_vbarvbar, + tk_vbaremark, + + tk_qmark, + + tk_less_than, + tk_less_than_eq, + + tk_greater_than, + tk_greater_than_eq, + + tk_ampersandemark, + tk_ampersandampersand, + + tk_colon, + + tk_EOF, + } tokenkind = tk_uninitialized; + + const char* moving = text; + + void next_token(void) + { + while (*moving && *moving == ' ') + moving++; + + switch (*moving) + { + case 0: + tokenkind = tk_EOF; + break; + + case '0': + tokenkind = tk_0, moving++; + break; + + case '1': + tokenkind = tk_1, moving++; + break; + + case 'w': + tokenkind = tk_w, moving++; + break; + + case 'x': + tokenkind = tk_x, moving++; + break; + + case 'y': + tokenkind = tk_y, moving++; + break; + + case 'z': + tokenkind = tk_z, moving++; + break; + + case '(': + tokenkind = tk_oparen, moving++; + break; + + case ')': + tokenkind = tk_cparen, moving++; + break; + + case '?': + tokenkind = tk_qmark, moving++; + break; + + case ':': + tokenkind = tk_colon, moving++; + break; + + // either '||' or '|!': + case '|': + { + moving++; + + switch (*moving) + { + case '|': + tokenkind = tk_vbarvbar, moving++; + break; + + case '!': + tokenkind = tk_vbaremark, moving++; + break; + + default: + { + puts("syntax error"); + exit(1); + break; + } + } + + break; + } + + // either '&&' or '&!': + case '&': + { + moving++; + + switch (*moving) + { + case '&': + tokenkind = tk_ampersandampersand, moving++; + break; + + case '!': + tokenkind = tk_ampersandemark, moving++; + break; + + default: + { + puts("syntax error"); + exit(1); + break; + } + } + + break; + } + + // either '!' or '!=' or '!&' or '!|' + case '!': + { + moving++; + + switch (*moving) + { + case '=': + tokenkind = tk_emarkequals, moving++; + break; + + case '|': + tokenkind = tk_emarkvbar, moving++; + break; + + case '&': + tokenkind = tk_emarkampersand, moving++; + break; + + default: + tokenkind = tk_emark; + break; + } + + break; + } + + case '<': + { + moving++; + + switch (*moving) + { + case '=': + tokenkind = tk_less_than_eq, moving++; + break; + + default: + { + tokenkind = tk_less_than; + break; + } + } + + break; + } + + case '>': + { + moving++; + + switch (*moving) + { + case '=': + tokenkind = tk_greater_than_eq, moving++; + break; + + default: + { + tokenkind = tk_greater_than; + break; + } + } + + break; + } + + // could only be '==': + case '=': + { + moving++; + + switch (*moving) + { + case '=': + tokenkind = tk_equalsequals, moving++; + break; + + default: + { + puts("syntax error"); + exit(1); + break; + } + } + + break; + } + + default: + assert(!"TODO"); + break; + } + } + + next_token(); + + uint32_t parse_root(void) + { + uint32_t parse_ternary(void) + { + uint32_t parse_ors(void) + { + uint32_t parse_ands(void) + { + uint32_t parse_equals(void) + { + uint32_t parse_compares(void) + { + uint32_t parse_prefix(void) + { + uint32_t parse_primary(void) + { + uint32_t retval; + + switch (tokenkind) + { + case tk_0: + retval = 0, next_token(); + break; + + case tk_1: + retval = M, next_token(); + break; + + case tk_w: + retval = W, next_token(); + break; + + case tk_x: + retval = X, next_token(); + break; + + case tk_y: + retval = Y, next_token(); + break; + + case tk_z: + retval = Z, next_token(); + break; + + case tk_oparen: + { + next_token(); + + retval = parse_root(); + + if (tokenkind != tk_cparen) + { + assert(!"NOPE"); + } + + next_token(); + break; + } + + default: + assert(!"TODO"); + break; + } + + return retval; + } + + if (tokenkind == tk_emark) + { + next_token(); + + return ~parse_prefix(); + } + else + { + return parse_primary(); + } + } + + uint32_t left = parse_prefix(); + + again: switch (tokenkind) + { + case tk_less_than: + { + next_token(); + left = (~left & parse_equals()) & M; + goto again; + } + + case tk_less_than_eq: + { + next_token(); + left = (~left | parse_equals()) & M; + goto again; + } + + case tk_greater_than_eq: + { + next_token(); + left = ( left | ~parse_equals()) & M; + goto again; + } + + case tk_greater_than: + { + next_token(); + left = ( left & ~parse_equals()) & M; + goto again; + } + + default: + break; + } + + return left; + } + + uint32_t left = parse_compares(); + + again: switch (tokenkind) + { + case tk_equalsequals: + { + next_token(); + left = ~(left ^ parse_equals()) & M; + goto again; + } + + case tk_emarkequals: + { + next_token(); + left = left ^ parse_equals(); + goto again; + } + + default: + break; + } + + return left; + } + + uint32_t left = parse_equals(); + + again: switch (tokenkind) + { + case tk_ampersandampersand: + { + next_token(); + left = left & parse_equals(); + goto again; + } + + case tk_ampersandemark: + { + next_token(); + left = ~left & parse_equals(); + goto again; + } + + case tk_emarkampersand: + { + next_token(); + left = ~(left & parse_equals()); + goto again; + } + + default: + break; + } + + return left; + } + + uint32_t left = parse_ands(); + + again: switch (tokenkind) + { + case tk_vbarvbar: + { + next_token(); + left = left | parse_ands(); + goto again; + } + + case tk_vbaremark: + { + next_token(); + left = (~left | parse_ands()) & M; + goto again; + } + + case tk_emarkvbar: + { + next_token(); + left = ~(left | parse_ands()) & M; + goto again; + } + + default: + break; + } + + return left; + } + + uint32_t cond = parse_ors(); + + if (tokenkind == tk_qmark) + { + next_token(); + + uint32_t left = parse_ors(); + + if (tokenkind != tk_colon) + { + puts("syntax error!"); + exit(1); + } + + next_token(); + + uint32_t right = parse_ternary(); + + return (cond & left) | (~cond & right); + } + else + { + return cond; + } + } + + return parse_ternary(); + } + + uint32_t truthtable = parse_root(); + + if (tokenkind != tk_EOF) + { + puts("syntax error!"); + exit(1); + } + + return truthtable; +} + +int main(int argc, char* const* argv) +{ + parse_args(argc, argv); + + get_simplifications(); + + if (print_all_and_quit) + { + for (long i = 0; i < N; i++) + { + int cost = lookup[i].cost; + + if (cost != INT_MAX) + { + printf("0b%032lb: [%2i]: ", i, cost), print((uint32_t) i, 0), puts(""); + } + } + } + else if (command) + { + uint32_t truthtable = evaluate(command); + + // printf("truthtable = 0b%016b\n", truthtable); + + if (lookup[truthtable].kind == ek_unreachable) + { + puts("unreachable"); + } + else + { + printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts(""); + } + } + else + { + // Let's humble-brag just a little. + { + int max_cost = 0; + + for (int i = 0; i < N; i++) + { + 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(""); + } + + for (char* line; (line = readline(">>> ")); free(line)) + { + add_history(line); + + uint32_t truthtable = evaluate(line); + + // printf("truthtable = 0b%016b\n", truthtable); + + if (lookup[truthtable].kind == ek_unreachable) + { + puts("unreachable"); + } + else + { + printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts(""); + } + } + } + + return 0; +} + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/flake.nix b/flake.nix index f1fab72..d3dc913 100644 --- a/flake.nix +++ b/flake.nix @@ -25,6 +25,7 @@ pkgs.mkShell { buildInputs = with pkgs; [ gcc + gcc.man gnumake readline.dev python3 diff --git a/main.py b/main.py index 050824f..1e47fb0 100755 --- a/main.py +++ b/main.py @@ -369,7 +369,7 @@ def calculate_simplifications(args, available_operators): return costs, lookup -pathname = "simplifications.bin" +pathname = ".simplifications.bin" def get_simplifications(args, available_operators): available_operators = tuple(sorted(available_operators)); diff --git a/makefile b/makefile index b19cc63..4201975 100644 --- a/makefile +++ b/makefile @@ -10,9 +10,9 @@ cppflags += -D _GNU_SOURCE cflags = -Werror -Wall -Wextra -Wstrict-prototypes -Wfatal-errors -cflags += -O3 +cflags += -O4 -cflags += -Wno-unused +# cflags += -Wno-unused ldflags += -lreadline