From 8152650e06bdd2dc6cf902546371684a4a6e6d6a Mon Sep 17 00:00:00 2001 From: Zander Thannhauser Date: Thu, 26 Jun 2025 22:41:11 -0500 Subject: [PATCH] broke main into many source files, added spike about assignment support that actually works pretty well --- .gitignore | 2 + buildtypes/debug.txt | 13 + buildtypes/release.txt | 11 + calculate_simplifications.c | 486 ++++++ calculate_simplifications.h | 8 + cmdln.c | 210 +++ cmdln.h | 40 + debug.h | 18 + defines.h | 9 + evaluate.c | 500 ++++++ evaluate.h | 5 + expr.h | 53 + flake.nix | 23 +- get_cached_simplifications.c | 172 ++ get_cached_simplifications.h | 8 + main.c | 2315 +------------------------ makefile | 72 +- nix-make.sh | 6 + print.c | 199 +++ print.h | 12 + simplifications.h | 14 + 5.c => spikes/5.c | 0 spikes/assignment.py | 199 +++ main.py => spikes/proof-of-concept.py | 0 24 files changed, 2092 insertions(+), 2283 deletions(-) create mode 100644 buildtypes/debug.txt create mode 100644 buildtypes/release.txt create mode 100644 calculate_simplifications.c create mode 100644 calculate_simplifications.h create mode 100644 cmdln.c create mode 100644 cmdln.h create mode 100644 debug.h create mode 100644 defines.h create mode 100644 evaluate.c create mode 100644 evaluate.h create mode 100644 expr.h create mode 100644 get_cached_simplifications.c create mode 100644 get_cached_simplifications.h create mode 100755 nix-make.sh create mode 100644 print.c create mode 100644 print.h create mode 100644 simplifications.h rename 5.c => spikes/5.c (100%) create mode 100644 spikes/assignment.py rename main.py => spikes/proof-of-concept.py (100%) diff --git a/.gitignore b/.gitignore index 22220a4..dcedce7 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,6 @@ +bin + .simplifications.bin .~lock.stats.ods# stats.ods diff --git a/buildtypes/debug.txt b/buildtypes/debug.txt new file mode 100644 index 0000000..b6139ee --- /dev/null +++ b/buildtypes/debug.txt @@ -0,0 +1,13 @@ + +-D _GNU_SOURCE + +-D ZDEBUG=1 + +-I . + +-Werror -Wall -Wextra -Wstrict-prototypes -Wfatal-errors + +-Wno-unused + +-lreadline + diff --git a/buildtypes/release.txt b/buildtypes/release.txt new file mode 100644 index 0000000..68d42ed --- /dev/null +++ b/buildtypes/release.txt @@ -0,0 +1,11 @@ + +-D _GNU_SOURCE + +-D ZDEBUG=0 + +-I . + +-Werror -Wall -Wextra -Wstrict-prototypes -Wfatal-errors + +-lreadline + diff --git a/calculate_simplifications.c b/calculate_simplifications.c new file mode 100644 index 0000000..b0b86c6 --- /dev/null +++ b/calculate_simplifications.c @@ -0,0 +1,486 @@ + +#include +#include +#include + +#include + +#include + +#include + +#include "calculate_simplifications.h" + +struct simplifications calculate_simplifications( + const struct cmdln_flags* flags) +{ + struct simplifications simps = {}; + + // init 'simps.data': + { + 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; + + // 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); + + 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.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; + } + + void update(uint16_t truthtable, int cost) + { + assert(todo.reverse[truthtable] != -1); + + assert(cost < simps.data[truthtable].cost); + + int index =todo. reverse[truthtable], 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; + } + + // 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), 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; + + append(0, 1), simps.data[0].kind = ek_0; + append(M, 1), simps.data[M].kind = ek_1; + + // disable terminal autowrap: + if (flags->verbose && flags->print_with_color) + { + printf("\e[?7l"); + } + + for (int iterations = 1; todo.n && iterations <= N; iterations++) + { + uint16_t truthtable = pop(); + + insert(truthtable); + + int cost = simps.data[truthtable].cost; + + if (flags->verbose) + { + if (flags->print_with_color) + { + printf("\e[2K"); + } + + printf("%i of %i (%.2f%%): [%i] ", + iterations, N, (100.0 * iterations / N), cost); + + print(flags, &simps, truthtable), puts(""); + + if (flags->print_with_color) + { + printf("\e[1A"); + } + } + + // consider NOT: + if (flags->use_operators.not) + { + uint16_t not_truthtable = ~truthtable & M; + + int not_cost = cost + 1; + + if (not_cost < simps.data[not_truthtable].cost) + { + if (todo.reverse[not_truthtable] == -1) + { + append(not_truthtable, not_cost); + } + else + { + update(not_truthtable, not_cost); + } + + simps.data[not_truthtable].kind = ek_not; + simps.data[not_truthtable].left = truthtable; + } + } + + #define BINARY_OPERATOR(ekind, function) \ + { \ + for (int i = done.head; i != -1; i = done.next[i]) \ + { \ + { \ + uint16_t bin_truthtable = function(truthtable, i) & M; \ + \ + int bin_cost = 1 + cost + simps.data[i].cost; \ + \ + if (bin_cost < simps.data[bin_truthtable].cost) \ + { \ + if (todo.reverse[bin_truthtable] == -1) \ + append(bin_truthtable, bin_cost); \ + else \ + update(bin_truthtable, bin_cost); \ + \ + simps.data[bin_truthtable].kind = ekind; \ + simps.data[bin_truthtable].left = truthtable; \ + simps.data[bin_truthtable].right = i; \ + } \ + } \ + \ + { \ + uint16_t bin_truthtable = function(i, truthtable) & M; \ + \ + int bin_cost = 1 + cost + simps.data[i].cost; \ + \ + if (bin_cost < simps.data[bin_truthtable].cost) \ + { \ + if (todo.reverse[bin_truthtable] == -1) \ + append(bin_truthtable, bin_cost); \ + else \ + update(bin_truthtable, bin_cost); \ + \ + simps.data[bin_truthtable].kind = ekind; \ + simps.data[bin_truthtable].left = i; \ + simps.data[bin_truthtable].right = truthtable; \ + } \ + } \ + } \ + } + + #define OR(a, b) ((a) | (b)) + #define AND(a, b) ((a) & (b)) + + #define ORN(a, b) (~(a) | (b)) + #define NOR(a, b) ~( (a) | (b)) + #define ANDN(a, b) (~(a) & (b)) + #define NAND(a, b) ~( (a) & (b)) + #define XOR(a, b) (( a) ^ (b)) + #define NXOR(a, b) ~( (a) ^ (b)) + + #define LT(a, b) ((~a) & (b)) + #define LTE(a, b) ((~a) | (b)) + #define GT(a, b) (( a) & ~(b)) + #define GTE(a, b) (( a) | ~(b)) + + if (flags->use_operators.or) + { + BINARY_OPERATOR(ek_or, OR); + } + + if (flags->use_operators.and) + { + BINARY_OPERATOR(ek_and, AND); + } + + if (flags->use_operators.orn) + { + BINARY_OPERATOR(ek_orn, ORN); + } + + if (flags->use_operators.nor) + { + BINARY_OPERATOR(ek_nor, NOR); + } + + if (flags->use_operators.andn) + { + BINARY_OPERATOR(ek_andn, ANDN); + } + + if (flags->use_operators.nand) + { + BINARY_OPERATOR(ek_nand, NAND); + } + + if (flags->use_operators.xor) + { + BINARY_OPERATOR(ek_xor, XOR); + } + + if (flags->use_operators.nxor) + { + BINARY_OPERATOR(ek_nxor, NXOR); + } + + if (flags->use_operators.lt) + { + BINARY_OPERATOR(ek_lt, LT); + } + + if (flags->use_operators.lte) + { + BINARY_OPERATOR(ek_lte, LTE); + } + + if (flags->use_operators.gt) + { + BINARY_OPERATOR(ek_gt, GT); + } + + if (flags->use_operators.gte) + { + BINARY_OPERATOR(ek_gte, GTE); + } + + if (flags->use_operators.ternary) + { + for (int i = done.head; i != -1; i = done.next[i]) + { + for (int j = done.head; j != -1; j = done.next[j]) + { + int ternary_cost = 1 + cost + simps.data[i].cost + simps.data[j].cost; + + #define TERNARY(C, T, F) \ + { \ + uint16_t ternary_truthtable = \ + ((C) & (T)) | (~(C) & (F)); \ + \ + if (ternary_cost < simps.data[ternary_truthtable].cost) \ + { \ + if (todo.reverse[ternary_truthtable] == -1) \ + { \ + append(ternary_truthtable, ternary_cost); \ + } \ + else \ + { \ + update(ternary_truthtable, ternary_cost); \ + } \ + \ + simps.data[ternary_truthtable].kind = ek_ternary; \ + simps.data[ternary_truthtable].cond = (C); \ + simps.data[ternary_truthtable].left = (T); \ + simps.data[ternary_truthtable].right = (F); \ + } \ + } \ + + TERNARY(truthtable, i, j); + TERNARY(i, truthtable, j); + TERNARY(i, j, truthtable); + } + } + } + } + + // clear progress line, enable terminal autowrap: + if (flags->verbose && flags->print_with_color) + { + printf("\e[2K"), printf("\e[?7h"); + } + + return simps; +} + + + + + + + + + + + + + + + diff --git a/calculate_simplifications.h b/calculate_simplifications.h new file mode 100644 index 0000000..72dfd98 --- /dev/null +++ b/calculate_simplifications.h @@ -0,0 +1,8 @@ + +#include "simplifications.h" + +struct cmdln_flags; + +struct simplifications calculate_simplifications( + const struct cmdln_flags* flags); + diff --git a/cmdln.c b/cmdln.c new file mode 100644 index 0000000..9ba8ad5 --- /dev/null +++ b/cmdln.c @@ -0,0 +1,210 @@ + +#include +#include +#include +#include + +#include "cmdln.h" + +#include "debug.h" + +struct cmdln_flags parse_args(int argc, char* const* argv) +{ + struct cmdln_flags flags = {}; + + flags.argv0 = argv[0]; + + bool unset_operators = true; + + bool unset_print_with_color = true; + + for (int opt; (opt = getopt(argc, argv, "pyqmvc:eEo:C:B")) != -1; ) + { + switch (opt) + { + case 'p': + { + flags.print_all_and_quit = true; + break; + } + + case 'y': + { + flags.assume_yes = true; + break; + } + + case 'q': + { + flags.quiet = true; + break; + } + + case 'm': + { + flags.print_max_operators_needed_and_quit = true; + break; + } + + case 'v': + { + flags.verbose = true; + break; + } + + case 'c': + { + flags.command = optarg; + break; + } + + case 'E': + { + flags.use_operators.ternary = true; + } + // fallthrough + + case 'e': + { + flags.use_operators.not = true; + flags.use_operators.or = true; + flags.use_operators.and = true; + + flags.use_operators.orn = true; + flags.use_operators.nor = true; + + flags.use_operators.andn = true; + flags.use_operators.nand = true; + + flags.use_operators. xor = true; + flags.use_operators.nxor = true; + + unset_operators = false; + break; + } + + case 'o': + { + unset_operators = false; + + for (char* moving; (moving = strtok_r(NULL, ",", &optarg)); ) + { + if (!strcmp(moving, "not") || !strcmp(moving, "!")) + { + flags.use_operators.not = true; + } + else if (!strcmp(moving, "or") || !strcmp(moving, "||")) + { + flags.use_operators.or = true; + } + else if (!strcmp(moving, "orn") || !strcmp(moving, "|!")) + { + flags.use_operators.orn = true; + } + else if (!strcmp(moving, "nor") || !strcmp(moving, "!|")) + { + flags.use_operators.nor = true; + } + else if (!strcmp(moving, "and") || !strcmp(moving, "&&")) + { + flags.use_operators.and = true; + } + else if (!strcmp(moving, "andn") || !strcmp(moving, "&!")) + { + flags.use_operators.andn = true; + } + else if (!strcmp(moving, "nand") || !strcmp(moving, "!&")) + { + flags.use_operators.nand = true; + } + else if (!strcmp(moving, "xor") || !strcmp(moving, "!=")) + { + flags.use_operators.xor = true; + } + else if (!strcmp(moving, "nxor") || !strcmp(moving, "==")) + { + flags.use_operators.nxor = true; + } + else if (!strcmp(moving, "lt") || !strcmp(moving, "<")) + { + flags.use_operators.lt = true; + } + else if (!strcmp(moving, "lte") || !strcmp(moving, "<=")) + { + flags.use_operators.lte = true; + } + else if (!strcmp(moving, "gt") || !strcmp(moving, ">")) + { + flags.use_operators.gt = true; + } + else if (!strcmp(moving, "gte") || !strcmp(moving, ">=")) + { + flags.use_operators.gte = true; + } + else if (!strcmp(moving, "ternary") || !strcmp(moving, "?:")) + { + flags.use_operators.ternary = true; + } + else + { + assert(!"TODO"); + } + } + break; + } + + case 'C': + { + unset_print_with_color = false; + + if (!strcmp(optarg, "yes") || !strcmp(optarg, "on")) + { + flags.print_with_color = true; + } + else if (!strcmp(optarg, "no") || !strcmp(optarg, "off")) + { + flags.print_with_color = false; + } + else if (!strcmp(optarg, "auto")) + { + flags.print_with_color = isatty(1); + } + else + { + assert(!"TODO"); + } + + break; + } + + case 'B': + { + flags.force_rebuild = true; + + break; + } + + default: + { + assert(!"TODO"); + break; + } + } + } + + if (unset_operators) + { + flags.use_operators.not = true; + flags.use_operators.or = true; + flags.use_operators.and = true; + } + + if (unset_print_with_color) + { + flags.print_with_color = isatty(1); + } + + return flags; +} + + diff --git a/cmdln.h b/cmdln.h new file mode 100644 index 0000000..da50cad --- /dev/null +++ b/cmdln.h @@ -0,0 +1,40 @@ + +#include + +struct cmdln_flags +{ + const char* argv0; + + const char* command; + + struct use_operators { + bool not; + + bool or, orn, nor; + + bool and, andn, nand; + + bool xor, nxor; + + bool lt, lte, gt, gte; + + bool ternary; + } use_operators; + + bool print_all_and_quit; + + bool print_max_operators_needed_and_quit; + + bool assume_yes; + + bool verbose; + + bool print_with_color; + + bool force_rebuild; + + bool quiet; +}; + +struct cmdln_flags parse_args(int argc, char* const* argv); + diff --git a/debug.h b/debug.h new file mode 100644 index 0000000..e1e92fc --- /dev/null +++ b/debug.h @@ -0,0 +1,18 @@ + +#ifndef ZDEBUG + #define ZDEBUG 1 +#endif + +#if ZDEBUG + #define zprintf(fmt, ...) \ + printf(fmt, ## __VA_ARGS__); +#else + #define zprintf(...); +#endif + +#define TODO \ + assert(!"TODO"); + +#define CHECK \ + assert(!"CHECK"); + diff --git a/defines.h b/defines.h new file mode 100644 index 0000000..5be9237 --- /dev/null +++ b/defines.h @@ -0,0 +1,9 @@ + +#define W 0b0101010101010101 +#define X 0b0011001100110011 +#define Y 0b0000111100001111 +#define Z 0b0000000011111111 +#define M 0b1111111111111111 + +#define N (65536) + diff --git a/evaluate.c b/evaluate.c new file mode 100644 index 0000000..2cb8d93 --- /dev/null +++ b/evaluate.c @@ -0,0 +1,500 @@ + +#include +#include +#include + +#include + +#include "evaluate.h" + +uint16_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(); + + uint16_t parse_root(void) + { + uint16_t parse_ternary(void) + { + uint16_t parse_ors(void) + { + uint16_t parse_ands(void) + { + uint16_t parse_equals(void) + { + uint16_t parse_compares(void) + { + uint16_t parse_prefix(void) + { + uint16_t parse_primary(void) + { + uint16_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(); + } + } + + uint16_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; + } + + uint16_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; + } + + uint16_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; + } + + uint16_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; + } + + uint16_t cond = parse_ors(); + + if (tokenkind == tk_qmark) + { + next_token(); + + uint16_t left = parse_ors(); + + if (tokenkind != tk_colon) + { + puts("syntax error!"); + exit(1); + } + + next_token(); + + uint16_t right = parse_ternary(); + + return (cond & left) | (~cond & right); + } + else + { + return cond; + } + } + + return parse_ternary(); + } + + uint16_t truthtable = parse_root(); + + if (tokenkind != tk_EOF) + { + puts("syntax error!"); + exit(1); + } + + return truthtable; +} + diff --git a/evaluate.h b/evaluate.h new file mode 100644 index 0000000..46668f6 --- /dev/null +++ b/evaluate.h @@ -0,0 +1,5 @@ + +#include + +uint16_t evaluate(const char* text); + diff --git a/expr.h b/expr.h new file mode 100644 index 0000000..daba83b --- /dev/null +++ b/expr.h @@ -0,0 +1,53 @@ + +#ifndef STRUCT_EXPR +#define STRUCT_EXPR + +#include + +enum ekind +{ + ek_unreachable, + + ek_0, + ek_1, + ek_W, + ek_X, + ek_Y, + ek_Z, + + ek_not, + ek_or, + ek_and, + + ek_orn, + ek_nor, + + ek_andn, + ek_nand, + + ek_xor, + ek_nxor, + + ek_lt, + ek_lte, + ek_gt, + ek_gte, + + ek_ternary, +}; + +struct expr +{ + enum ekind kind; + + uint16_t cond, left, right; + + int cost; +}; + + + + + + +#endif diff --git a/flake.nix b/flake.nix index d3dc913..b1c8355 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ # vim: set sw=2 ts=2 et: # { - description = "An example project using flutter"; + description = "description"; inputs.nixpkgs = { url = "github:NixOS/nixpkgs"; }; @@ -29,8 +29,29 @@ gnumake readline.dev python3 + valgrind + + # for my sake: + gedit ]; }; }); } + + + + + + + + + + + + + + + + + diff --git a/get_cached_simplifications.c b/get_cached_simplifications.c new file mode 100644 index 0000000..f09eb0f --- /dev/null +++ b/get_cached_simplifications.c @@ -0,0 +1,172 @@ + +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#include + +#include + +#include "get_cached_simplifications.h" +#include "calculate_simplifications.h" + +static struct path { char data[PATH_MAX]; } get_path( + const struct cmdln_flags* flags) +{ + struct path path = {}; + + strcat(path.data, ".simplifier-cache-1"); + + if (flags->use_operators.not) + strcat(path.data, "-not"); + + if (flags->use_operators.or) + strcat(path.data, "-or"); + + if (flags->use_operators.orn) + strcat(path.data, "-orn"); + + if (flags->use_operators.nor) + strcat(path.data, "-nor"); + + if (flags->use_operators.and) + strcat(path.data, "-and"); + + if (flags->use_operators.andn) + strcat(path.data, "-andn"); + + if (flags->use_operators.nand) + strcat(path.data, "-nand"); + + if (flags->use_operators.xor) + strcat(path.data, "-xor"); + + if (flags->use_operators.nxor) + strcat(path.data, "-nxor"); + + if (flags->use_operators.lt) + strcat(path.data, "-lt"); + + if (flags->use_operators.lte) + strcat(path.data, "-lte"); + + if (flags->use_operators.gt) + strcat(path.data, "-gt"); + + if (flags->use_operators.gte) + strcat(path.data, "-gte"); + + if (flags->use_operators.ternary) + strcat(path.data, "-ternary"); + + strcat(path.data, ".bin"); + + return path; +} + +struct simplifications get_cached_simplifications( + const struct cmdln_flags* flags) +{ + struct path path = get_path(flags); + + int fd = -1; + + bool rebuild = flags->force_rebuild; + + struct simplifications simps = {}; + + if (!rebuild) + { + fd = open(path.data, O_RDONLY); + + if (fd > 0) + { + // great, just read it into memory + + if (read(fd, &simps, sizeof(simps)) < (ssize_t) sizeof(simps)) + { + printf("%s: read() to cache failed: %m\n", flags->argv0); + exit(1); + } + } + else if (errno == ENOENT) + { + rebuild = true; + } + else + { + TODO; + exit(1); + } + } + + if (rebuild) + { + if (!flags->quiet) + { + puts("" + "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" + ""); + } + + if (!flags->quiet && !flags->verbose) + { + puts("Re-run with '-v' to watch progress"); + } + + if (!flags->quiet && !flags->assume_yes) + { + puts(""); + puts("Any input to start:"), getchar(); + puts("Started."); + } + + simps = calculate_simplifications(flags); + + fd = open(path.data, O_WRONLY | O_TRUNC | O_CREAT, 0664); + + if (fd < 0) + { + TODO; + exit(1); + } + + if (write(fd, &simps, sizeof(simps)) < (ssize_t) sizeof(simps)) + { + printf("%s: write() to cache failed: %m\n", flags->argv0); + exit(1); + } + } + + if (fd > 0) + { + close(fd); + } + + return simps; +} + + + + + + + + + + + + + + + diff --git a/get_cached_simplifications.h b/get_cached_simplifications.h new file mode 100644 index 0000000..f6e91af --- /dev/null +++ b/get_cached_simplifications.h @@ -0,0 +1,8 @@ + +#include "simplifications.h" + +struct cmdln_flags; + +struct simplifications get_cached_simplifications( + const struct cmdln_flags* flags); + diff --git a/main.c b/main.c index 9bd0071..774f014 100644 --- a/main.c +++ b/main.c @@ -1,2319 +1,108 @@ -#include -#include -#include -#include -#include -#include #include -#include -#include +#include #include #include #include -#define argv0 program_invocation_name +#include +#include -#ifndef ZDEBUG -#define ZDEBUG 0 -#endif +#include -#if ZDEBUG - int calldepth = 0; - - #define zprintf(fmt, ...) \ - printf(fmt, ## __VA_ARGS__); -#else - #define zprintf(...); -#endif +#include -#define TODO \ - assert(!"TODO"); +#include -bool print_all_and_quit = false; - -const char* command = NULL; - -struct { - bool not; - - bool or, nor; - - bool and, nand; - - bool xor, nxor; - - bool compares; - - bool ternary; -} 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:eEo: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.ternary = true; - // fallthrough - - 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 if (!strcmp(moving, "ternary") || !strcmp(moving, "?:")) - use_operators.ternary = 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 W 0b0101010101010101 -#define X 0b0011001100110011 -#define Y 0b0000111100001111 -#define Z 0b0000000011111111 -#define M 0b1111111111111111 - -#define B (16) - -#define N (1 << (B)) - -enum kind { - ek_unreachable, - - ek_0, - ek_1, - 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, - - ek_ternary, -}; - -struct expr { - enum kind kind; - - uint16_t cond, left, right; - - int cost; -} lookup[N]; - -static void print(uint16_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_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 - - case ek_ternary: - { - const char *start = "", *end = ""; - - if (print_with_color) - { - start = operator_colors[depth % 10]; - - end = RESET_ESCAPE; - } - - printf("%s(%s", start, end); - print(e->cond, depth + 1); - printf("%s ? %s", start, end); - print(e->left, depth + 1); - printf("%s : %s", start, end); - print(e->right, depth + 1); - printf("%s)%s", start, end); - - break; - } - } -} - -// heap of truthtables; key = cost -struct heap -{ - uint16_t data[N]; - int n; - - // truthtable -> index in 'todo' - int 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; -} - -uint16_t heap_pop(struct heap* this) -{ - zprintf("%*s" "heap_pop():" "\n", calldepth++, ""); - - assert(this->n > 0); - - uint16_t retval = this->data[0]; - - this->reverse[retval] = -1; - - uint16_t moving = this->data[this->n-- - 1]; - - int cost = lookup[moving].cost; - - int index = 0; - - again: - { - int left = index * 2 + 1; - int right = index * 2 + 2; - - uint16_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 - { - int 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, uint16_t truthtable, int cost) -{ - zprintf("%*s" "heap_push():" "\n", calldepth++, ""); - - assert(this->reverse[truthtable] == -1); - - int 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, uint16_t truthtable, int cost) -{ - zprintf("%*s" "heap_update():" "\n", calldepth++, ""); - - assert(this->reverse[truthtable] != -1); - - assert(cost < lookup[truthtable].cost); - - int 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 (int i = 0; i < B; i++) - { - for (int 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)); - - int i, j; - - for (i = 0, j = 0; j < N; j++) - { - this->data[i][j] = 1; - } - - for (i = 1; i < B; i++) - { - for (j = 0; j < N; j++) - { - this->data[i][j] = 2; - } - } - - #if ZDEBUG - calldepth--; - #endif - - return this; -} - -void boolset_add(struct boolset* this, uint16_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, uint16_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 (int i = 0; i < N; i++) - { - lookup[i].kind = ek_unreachable; - - lookup[i].cost = INT_MAX; - } - - // list of truthtables we're still working on, sorted by cost. - struct heap* todo = new_heap(); - - // 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(); - - 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 (int iterations = 1; todo->n && iterations <= N; iterations++) - { - zprintf("%*s" "iterations = %i" "\n", calldepth, "", iterations); - - uint16_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("%i of %i (%.2f%%): [%i] ", iterations, N, (100.0 * iterations / N), cost); - - print(truthtable, 0), puts(""); - - if (!ZDEBUG && print_with_color) - { - printf("\e[1A"); - } - } - - // consider NOT: - if (use_operators.not) - { - uint16_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, 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, 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, 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 == 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, 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, 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 (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); - } - - if (use_operators.ternary) - { - // a ? b : c = d - //--------------- - // 0 | 0 | 0 | 0 - // 0 | 0 | 1 | 1 - // 0 | 1 | 0 | 0 - // 0 | 1 | 1 | 1 - // 1 | 0 | 0 | 0 - // 1 | 1 | 0 | 1 - // 1 | 0 | 1 | 0 - // 1 | 1 | 1 | 1 - - void search1(int k, int bi, int ci, int di) - { - zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); - - if (k >= 0) - { - if (truthtable & (1 << k)) - { - // 1 | 0 | 0 | 0 - // 1 | 1 | 0 | 1 - // 1 | 0 | 1 | 0 - // 1 | 1 | 1 | 1 - - // a == 1 and b == 0 and c == 0 and d == 0 - if (done->data[k][(bi >> k) + 0] && done->data[k][(ci >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search1(k - 1, bi + (0 << k), ci + (0 << k), di + (0 << k)); - } - - // a == 1 and b == 0 and c == 1 and d == 0 - if (done->data[k][(bi >> k) + 0] && done->data[k][(ci >> k) + 1] && undone->data[k][(di >> k) + 0]) - { - search1(k - 1, bi + (0 << k), ci + (1 << k), di + (0 << k)); - } - - // a == 1 and b == 1 and c == 0 and d == 1 - if (done->data[k][(bi >> k) + 1] && done->data[k][(ci >> k) + 0] && undone->data[k][(di >> k) + 1]) - { - search1(k - 1, bi + (1 << k), ci + (0 << k), di + (1 << k)); - } - - // a == 1 and b == 1 and c == 1 and d == 1 - if (done->data[k][(bi >> k) + 1] && done->data[k][(ci >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search1(k - 1, bi + (1 << k), ci + (1 << k), di + (1 << k)); - } - } - else - { - // 0 | 0 | 0 | 0 - // 0 | 0 | 1 | 1 - // 0 | 1 | 0 | 0 - // 0 | 1 | 1 | 1 - - // a == 0 and b == 0 and c == 0 and d == 0 - if (done->data[k][(bi >> k) + 0] && done->data[k][(ci >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search1(k - 1, bi + (0 << k), ci + (0 << k), di + (0 << k)); - } - - // a == 0 and b == 0 and c == 1 and d == 1 - if (done->data[k][(bi >> k) + 0] && done->data[k][(ci >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search1(k - 1, bi + (0 << k), ci + (1 << k), di + (1 << k)); - } - - // a == 0 and b == 1 and c == 0 and d == 0 - if (done->data[k][(bi >> k) + 1] && done->data[k][(ci >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search1(k - 1, bi + (1 << k), ci + (0 << k), di + (0 << k)); - } - - // a == 0 and b == 1 and c == 1 and d == 1 - if (done->data[k][(bi >> k) + 1] && done->data[k][(ci >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search1(k - 1, bi + (1 << k), ci + (1 << k), di + (1 << k)); - } - } - } - else - { - zprintf("%*s" "(0b%016b ? 0b%016b : 0b%016b) == 0b%016b" "\n", - calldepth, "", truthtable, bi, ci, di); - - assert(((((truthtable & bi) | (~truthtable & ci)))) == di); - - int ternary_cost = 1 + cost + lookup[bi].cost + lookup[ci].cost; - - if (ternary_cost < lookup[di].cost) - { - if (todo->reverse[di] == -1) - { - heap_push(todo, di, ternary_cost); - } - else - { - heap_update(todo, di, ternary_cost); - } - - lookup[di].kind = ek_ternary; - lookup[di].cond = (truthtable); - lookup[di].left = (bi); - lookup[di].right = (ci); - } - } - - #if ZDEBUG - calldepth--; - #endif - } - - search1(B - 1, 0, 0, 0); - - // a ? b : c = d - //--------------- - // 0 | 0 | 0 | 0 - // 0 | 0 | 1 | 1 - // 0 | 1 | 0 | 0 - // 0 | 1 | 1 | 1 - // 1 | 0 | 0 | 0 - // 1 | 1 | 0 | 1 - // 1 | 0 | 1 | 0 - // 1 | 1 | 1 | 1 - - void search2(int k, int ai, int ci, int di) - { - zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); - - if (k >= 0) - { - if (truthtable & (1 << k)) - { - // 0 | 1 | 0 | 0 - // 0 | 1 | 1 | 1 - // 1 | 1 | 0 | 1 - // 1 | 1 | 1 | 1 - - // a == 0 and b == 1 and c == 0 and d == 0 - if (done->data[k][(ai >> k) + 0] && done->data[k][(ci >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search2(k - 1, ai + (0 << k), ci + (0 << k), di + (0 << k)); - } - - // a == 0 and b == 1 and c == 1 and d == 0 - if (done->data[k][(ai >> k) + 0] && done->data[k][(ci >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search2(k - 1, ai + (0 << k), ci + (1 << k), di + (1 << k)); - } - - // a == 1 and b == 1 and c == 0 and d == 1 - if (done->data[k][(ai >> k) + 1] && done->data[k][(ci >> k) + 0] && undone->data[k][(di >> k) + 1]) - { - search2(k - 1, ai + (1 << k), ci + (0 << k), di + (1 << k)); - } - - // a == 1 and b == 1 and c == 1 and d == 1 - if (done->data[k][(ai >> k) + 1] && done->data[k][(ci >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search2(k - 1, ai + (1 << k), ci + (1 << k), di + (1 << k)); - } - } - else - { - // 0 | 0 | 0 | 0 - // 0 | 0 | 1 | 1 - // 1 | 0 | 0 | 0 - // 1 | 0 | 1 | 0 - - // a == 0 and b == 0 and c == 0 and d == 0 - if (done->data[k][(ai >> k) + 0] && done->data[k][(ci >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search2(k - 1, ai + (0 << k), ci + (0 << k), di + (0 << k)); - } - - // a == 0 and b == 0 and c == 1 and d == 1 - if (done->data[k][(ai >> k) + 0] && done->data[k][(ci >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search2(k - 1, ai + (0 << k), ci + (1 << k), di + (1 << k)); - } - - // a == 1 and b == 0 and c == 0 and d == 0 - if (done->data[k][(ai >> k) + 1] && done->data[k][(ci >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search2(k - 1, ai + (1 << k), ci + (0 << k), di + (0 << k)); - } - - // a == 1 and b == 0 and c == 1 and d == 1 - if (done->data[k][(ai >> k) + 1] && done->data[k][(ci >> k) + 1] && undone->data[k][(di >> k) + 0]) - { - search2(k - 1, ai + (1 << k), ci + (1 << k), di + (0 << k)); - } - } - } - else - { - zprintf("%*s" "(0b%016b ? 0b%016b : 0b%016b) == 0b%016b" "\n", - calldepth, "", ai, truthtable, ci, di); - - assert(((((ai & truthtable) | (~ai & ci)))) == di); - - int ternary_cost = 1 + lookup[ai].cost + cost + lookup[ci].cost; - - if (ternary_cost < lookup[di].cost) - { - if (todo->reverse[di] == -1) - { - heap_push(todo, di, ternary_cost); - } - else - { - heap_update(todo, di, ternary_cost); - } - - lookup[di].kind = ek_ternary; - lookup[di].cond = (ai); - lookup[di].left = (truthtable); - lookup[di].right = (ci); - } - } - - #if ZDEBUG - calldepth--; - #endif - } - - search2(B - 1, 0, 0, 0); - - // a ? b : c = d - //--------------- - // 0 | 0 | 0 | 0 - // 0 | 0 | 1 | 1 - // 0 | 1 | 0 | 0 - // 0 | 1 | 1 | 1 - // 1 | 0 | 0 | 0 - // 1 | 1 | 0 | 1 - // 1 | 0 | 1 | 0 - // 1 | 1 | 1 | 1 - - void search3(int k, int ai, int bi, int di) - { - zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); - - if (k >= 0) - { - if (truthtable & (1 << k)) - { - // 0 | 0 | 1 | 1 - // 0 | 1 | 1 | 1 - // 1 | 0 | 1 | 0 - // 1 | 1 | 1 | 1 - - // a == 0 and b == 0 and c == 1 and d == 0 - if (done->data[k][(ai >> k) + 0] && done->data[k][(bi >> k) + 0] && undone->data[k][(di >> k) + 1]) - { - search3(k - 1, ai + (0 << k), bi + (0 << k), di + (1 << k)); - } - - // a == 0 and b == 1 and c == 1 and d == 0 - if (done->data[k][(ai >> k) + 0] && done->data[k][(bi >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search3(k - 1, ai + (0 << k), bi + (1 << k), di + (1 << k)); - } - - // a == 1 and b == 0 and c == 1 and d == 1 - if (done->data[k][(ai >> k) + 1] && done->data[k][(bi >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search3(k - 1, ai + (1 << k), bi + (0 << k), di + (0 << k)); - } - - // a == 1 and b == 1 and c == 1 and d == 1 - if (done->data[k][(ai >> k) + 1] && done->data[k][(bi >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search3(k - 1, ai + (1 << k), bi + (1 << k), di + (1 << k)); - } - } - else - { - // 0 | 0 | 0 | 0 - // 0 | 1 | 0 | 0 - // 1 | 0 | 0 | 0 - // 1 | 1 | 0 | 1 - - // a == 0 and b == 0 and c == 0 and d == 0 - if (done->data[k][(ai >> k) + 0] && done->data[k][(bi >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search3(k - 1, ai + (0 << k), bi + (0 << k), di + (0 << k)); - } - - // a == 0 and b == 1 and c == 0 and d == 1 - if (done->data[k][(ai >> k) + 0] && done->data[k][(bi >> k) + 1] && undone->data[k][(di >> k) + 0]) - { - search3(k - 1, ai + (0 << k), bi + (1 << k), di + (0 << k)); - } - - // a == 1 and b == 0 and c == 0 and d == 0 - if (done->data[k][(ai >> k) + 1] && done->data[k][(bi >> k) + 0] && undone->data[k][(di >> k) + 0]) - { - search3(k - 1, ai + (1 << k), bi + (0 << k), di + (0 << k)); - } - - // a == 1 and b == 1 and c == 0 and d == 1 - if (done->data[k][(ai >> k) + 1] && done->data[k][(bi >> k) + 1] && undone->data[k][(di >> k) + 1]) - { - search3(k - 1, ai + (1 << k), bi + (1 << k), di + (1 << k)); - } - } - } - else - { - zprintf("%*s" "(0b%016b ? 0b%016b : 0b%016b) == 0b%016b" "\n", - calldepth, "", ai, bi, truthtable, di); - - assert(((((ai & bi) | (~ai & truthtable)))) == di); - - int ternary_cost = 1 + lookup[ai].cost + lookup[bi].cost + cost; - - if (ternary_cost < lookup[di].cost) - { - if (todo->reverse[di] == -1) - { - heap_push(todo, di, ternary_cost); - } - else - { - heap_update(todo, di, ternary_cost); - } - - lookup[di].kind = ek_ternary; - lookup[di].cond = (ai); - lookup[di].left = (bi); - lookup[di].right = (truthtable); - } - } - - #if ZDEBUG - calldepth--; - #endif - } - - search3(B - 1, 0, 0, 0); - } - } - - 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-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"); - - if (use_operators.ternary) - strcat(path, "-ternary"); - - 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); - } -} - -uint16_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(); - - uint16_t parse_root(void) - { - uint16_t parse_ternary(void) - { - uint16_t parse_ors(void) - { - uint16_t parse_ands(void) - { - uint16_t parse_equals(void) - { - uint16_t parse_compares(void) - { - uint16_t parse_prefix(void) - { - uint16_t parse_primary(void) - { - uint16_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(); - } - } - - uint16_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; - } - - uint16_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; - } - - uint16_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; - } - - uint16_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; - } - - uint16_t cond = parse_ors(); - - if (tokenkind == tk_qmark) - { - next_token(); - - uint16_t left = parse_ors(); - - if (tokenkind != tk_colon) - { - puts("syntax error!"); - exit(1); - } - - next_token(); - - uint16_t right = parse_ternary(); - - return (cond & left) | (~cond & right); - } - else - { - return cond; - } - } - - return parse_ternary(); - } - - uint16_t truthtable = parse_root(); - - if (tokenkind != tk_EOF) - { - puts("syntax error!"); - exit(1); - } - - return truthtable; -} +#include int main(int argc, char* const* argv) { - parse_args(argc, argv); + struct cmdln_flags flags = parse_args(argc, argv); - get_simplifications(); - - if (print_all_and_quit) + struct simplifications simps = get_cached_simplifications(&flags); + + if (flags.print_all_and_quit) { for (int i = 0; i < N; i++) { - int cost = lookup[i].cost; + int cost = simps.data[i].cost; if (cost != INT_MAX) { - printf("0b%016b: [%2i]: ", i, cost), print(i, 0), puts(""); + printf("0b%016b: [%2i]: ", i, cost); + print(&flags, &simps, i); + puts(""); } } } - else if (command) + else if (flags.print_max_operators_needed_and_quit) { - uint16_t truthtable = evaluate(command); + int max_cost = 0; + + for (int i = 0; i < N; i++) + { + int cost = simps.data[i].cost; + + if (cost != INT_MAX && max_cost < cost) + { + max_cost = cost; + } + } + + printf("I can simplify any tree down to %i operators or less.\n", max_cost); + } + else if (flags.command) + { + uint16_t truthtable = evaluate(flags.command); // printf("truthtable = 0b%016b\n", truthtable); - if (lookup[truthtable].kind == ek_unreachable) + if (simps.data[truthtable].kind == ek_unreachable) { - puts("unreachable"); + puts("Unreachable"); } else { - printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts(""); + printf("%2i: ", simps.data[truthtable].cost); + print(&flags, &simps, truthtable); + puts(""); } } else { - // Let's humble-brag just a little. + if (!flags.quiet) { - 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(""); + puts("Use C-style syntax for boolean operators and expressions."); + puts("Available variables: 'w', 'x', 'y' and 'z'."); + puts("Extended operators: nor is '!|', orn is '|!', nand is '!&', andn is '&!'."); + puts("Comparison operators are also suppported."); } - + for (char* line; (line = readline(">>> ")); free(line)) { + if (!*line) continue; + add_history(line); - + uint16_t truthtable = evaluate(line); // printf("truthtable = 0b%016b\n", truthtable); - if (lookup[truthtable].kind == ek_unreachable) + if (simps.data[truthtable].kind == ek_unreachable) { puts("unreachable"); } else { - printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts(""); + printf("%2i: ", simps.data[truthtable].cost); + print(&flags, &simps, truthtable); + puts(""); } } } - + return 0; } diff --git a/makefile b/makefile index 4201975..74d286b 100644 --- a/makefile +++ b/makefile @@ -1,28 +1,62 @@ # vim: noexpandtab tabstop=4 : +buildtype ?= release + +optionset = buildtypes/${buildtype}.txt + +prefix = bin/${buildtype} + +default: ${prefix}/bsimp + +.PRECIOUS: %/ + +%/: + @mkdir -p $@ + +srcs += calculate_simplifications.c cmdln.c evaluate.c +srcs += get_cached_simplifications.c main.c print.c + +${prefix}/%.o ${prefix}/%.d: %.c ${optionset} | ${prefix}/%/ + @echo "compiling (${buildtype}) ${*}.c ..." + @gcc -c @${optionset} $< -MD -MF ${prefix}/${*}.d -o ${prefix}/${*}.o + +objs = $(patsubst %.c,${prefix}/%.o,${srcs}) + +${prefix}/bsimp: ${optionset} ${objs} | bin/ + @echo "linking (${buildtype})" + @gcc @${optionset} ${objs} -o $@ + args = -cc = gcc - -cppflags += -D _GNU_SOURCE -#cppflags += -D ZDEBUG - -cflags = -Werror -Wall -Wextra -Wstrict-prototypes -Wfatal-errors - -cflags += -O4 - -# cflags += -Wno-unused - -ldflags += -lreadline - -/tmp/4-variable-simplifier: main.c - $(cc) $(cppflags) $(cflags) $< -o $@ $(ldflags) - -run: /tmp/4-variable-simplifier +run: ${prefix}/bsimp $< $(args) +valrun: ${prefix}/bsimp + valgrind --exit-on-first-error=yes --error-exitcode=1 -- $< ${args} + +PREFIX ?= ${HOME} + +install: ${PREFIX}/bin/bsimp + +${PREFIX}/bin/bsimp: bin/release/bsimp | ${PREFIX}/bin/ + cp -vau $< $@ + +include $(patsubst %.c,${prefix}/%.d,${srcs}) + + + + + + + + + + + + + + + -# nix --extra-experimental-features nix-command \ -# --extra-experimental-features flakes develop --command 'make' diff --git a/nix-make.sh b/nix-make.sh new file mode 100755 index 0000000..3fba410 --- /dev/null +++ b/nix-make.sh @@ -0,0 +1,6 @@ +#!/bin/sh +set -ev +nix --extra-experimental-features nix-command \ + --extra-experimental-features flakes \ + develop \ + --command "make" "$@" diff --git a/print.c b/print.c new file mode 100644 index 0000000..e0d53e7 --- /dev/null +++ b/print.c @@ -0,0 +1,199 @@ + +#include +#include + +#include + +#include + +#include + +#include "simplifications.h" + +#include "print.h" + +static void helper( + const struct simplifications *simps, + uint16_t truthtable, + bool print_with_color, + 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 = &simps->data[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_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); + + helper(simps, e->left, print_with_color, 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); \ + \ + helper(simps, e->left, print_with_color, depth + 1); \ + \ + printf("%s%s%s", start, operatorstring, end); \ + \ + helper(simps, e->right, print_with_color, depth + 1); \ + \ + printf("%s)%s", start, end); \ + break; \ + } + + BINARY_OPERATOR(ek_or, " || "); + BINARY_OPERATOR(ek_orn, " |! "); + BINARY_OPERATOR(ek_nor, " !| "); + + BINARY_OPERATOR(ek_and, " && "); + BINARY_OPERATOR(ek_andn, " &! "); + 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 + + case ek_ternary: + { + const char *start = "", *end = ""; + + if (print_with_color) + { + start = operator_colors[depth % 10]; + + end = RESET_ESCAPE; + } + + printf("%s(%s", start, end); + helper(simps, e->cond, print_with_color, depth + 1); + printf(" %s?%s ", start, end); + helper(simps, e->left, print_with_color, depth + 1); + printf(" %s:%s ", start, end); + helper(simps, e->right, print_with_color, depth + 1); + printf("%s)%s", start, end); + + break; + } + } +} + +void print( + const struct cmdln_flags* flags, + const struct simplifications *simps, + uint16_t truthtable) +{ + helper(simps, truthtable, flags->print_with_color, 0); +} + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/print.h b/print.h new file mode 100644 index 0000000..a299aa6 --- /dev/null +++ b/print.h @@ -0,0 +1,12 @@ + +#include + +struct cmdln_flags; +struct simplifications; + +void print( + const struct cmdln_flags* flags, + const struct simplifications *simps, + uint16_t truthtable); + + diff --git a/simplifications.h b/simplifications.h new file mode 100644 index 0000000..7262269 --- /dev/null +++ b/simplifications.h @@ -0,0 +1,14 @@ + +#ifndef STRUCT_SIMPLIFICATIONS +#define STRUCT_SIMPLIFICATIONS + +#include "defines.h" + +#include "expr.h" + +struct simplifications +{ + struct expr data[N]; +}; + +#endif diff --git a/5.c b/spikes/5.c similarity index 100% rename from 5.c rename to spikes/5.c diff --git a/spikes/assignment.py b/spikes/assignment.py new file mode 100644 index 0000000..e451a4d --- /dev/null +++ b/spikes/assignment.py @@ -0,0 +1,199 @@ +#!/usr/bin/env python3 + +from heapq import heappush, heappop + +X = 0b01010101 +Y = 0b00110011 +Z = 0b00001111 +M = 0b11111111 + +B = 1 << 3 +N = 1 << B + +def calc_simps(A = None): + # truthtable -> ('var', name) + # truthtable -> ('not', inner truthtable) + # truthtable -> (binary op, left truthtable, right truthtable) + lookup = dict(); + + # truthtable -> cost + costs = dict(); + + todo = set(); + + def initial(exp, truthtable): + lookup[truthtable] = exp; + costs[truthtable] = 0; + todo.add(truthtable); + + initial(('var', 'x'), X); + initial(('var', 'y'), Y); + initial(('var', 'z'), Z); + initial(('lit', '0'), 0); + initial(('lit', '1'), M); + + if (A is not None): + initial(('var', 'a'), A); + + done = list(); + + for iteration in range(1, N + 1): + mytruthtable = min(todo, key = lambda x: (costs[x], x)); + + mycost = costs[mytruthtable]; + + todo.remove(mytruthtable); + + # consider NOT: + not_cost = mycost + 1 + not_truthtable = ~mytruthtable & M; + if (not_truthtable not in costs) or (not_cost < costs[not_truthtable]): + todo.add(not_truthtable); + + lookup[not_truthtable] = ("not", mytruthtable); + + costs[not_truthtable] = not_cost; + + # consider OR: + for othertruthtable in done: + or_cost = 1 + mycost + costs[othertruthtable]; + + or_truthtable = mytruthtable | othertruthtable; + + if (or_truthtable not in costs) or (or_cost < costs[or_truthtable]): + todo.add(or_truthtable); + + lookup[or_truthtable] = ("or", mytruthtable, othertruthtable); + + costs[or_truthtable] = or_cost; + + # consider AND: + for othertruthtable in done: + and_cost = 1 + mycost + costs[othertruthtable]; + + and_truthtable = mytruthtable & othertruthtable; + + if (and_truthtable not in costs) or (and_cost < costs[and_truthtable]): + todo.add(and_truthtable); + + lookup[and_truthtable] = ("and", mytruthtable, othertruthtable); + + costs[and_truthtable] = and_cost; + + # consider XOR: + if 0: + for othertruthtable in done: + xor_cost = 1 + mycost + costs[othertruthtable]; + + xor_truthtable = mytruthtable ^ othertruthtable; + + if (xor_truthtable not in costs) or (xor_cost < costs[xor_truthtable]): + todo.add(xor_truthtable); + + lookup[xor_truthtable] = ("xor", mytruthtable, othertruthtable); + + costs[xor_truthtable] = xor_cost; + + done.append(mytruthtable); + + assert(sorted(done) == sorted(costs)); + + return costs, lookup; + +def etostr(lookup, expr): + match expr: + case ('lit', x): + return x; + case ('var', x): + return x; + case ('not', inner): + return "(!" + tostr(lookup, inner) + ")"; + case ('or', left, right): + return "(" + tostr(lookup, left) + " || " + tostr(lookup, right) + ")"; + case ('and', left, right): + return "(" + tostr(lookup, left) + " && " + tostr(lookup, right) + ")"; + case ('xor', left, right): + return "(" + tostr(lookup, left) + " != " + tostr(lookup, right) + ")"; + case _: + assert(not "TODO"); + +def tostr(lookup, truthtable): + return etostr(lookup, lookup[truthtable]); + +zdcosts, zdlookup = calc_simps(); + +# now that we've figured out the zero-depth trees, we need to figure out which +# trees could be done faster with a variable. We need to go through every +# possible truthtable, considering them the new variable, building up a new +# table of what expressions are the cheapiest with that variable. +# Then, if that figured out for all of them, we could read down the columns +# figuring out the best answers for anything the user gives. + +# truthtable -> cost +costs = zdcosts; + +# truthtable -> variable truthtable +varlookup = {x: None for x in range(1 << B)}; + +all_costs = dict(); # variable truthtable -> truthtable -> cost +all_lookups = dict(); # variable truthtable -> truthtable -> expr + +for A in range(0, 1 << B): + print(f"what if the variable was 0b{A:08b}?"); + + var_costs, var_lookup = calc_simps(A); + + for t in range(0, 1 << B): + mycost = var_costs[t] + 1 + zdcosts[A]; + + if mycost < costs[t]: + varlookup[t] = A; + + costs[t] = mycost; + + all_costs[A] = var_costs; + + all_lookups[A] = var_lookup; + +for t in range(0, 1 << B): + line = f"0b{t:08b}: "; + + line += f"[{costs[t]}] "; + + if varlookup[t] is None: + line += tostr(zdlookup, t); + else: + line += "(" + + a = varlookup[t]; + + line += "a = " + tostr(zdlookup, a); + + line += ", " + + line += tostr(all_lookups[a], t); + + line += ")" + + line += " [before: " + tostr(zdlookup, t) + "]"; + + print(line); + +print(); +print(f"we can do anything in {max(costs.values())} operations"); + + + + + + + + + + + + + + + + diff --git a/main.py b/spikes/proof-of-concept.py similarity index 100% rename from main.py rename to spikes/proof-of-concept.py