diff --git a/.gitignore b/.gitignore index 0f3caa3..2846313 100644 --- a/.gitignore +++ b/.gitignore @@ -4,4 +4,9 @@ simplifications.bin .simplifier-*.bin .direnv/ + typescript + +vgcore.* + +*~ diff --git a/main.c b/main.c index 3a11c8f..7c00482 100644 --- a/main.c +++ b/main.c @@ -15,13 +15,22 @@ #define argv0 program_invocation_name -#ifdef ZDEBUG -#define zprintf(fmt, ...) \ - printf(fmt, ## __VA_ARGS__); -#else -#define zprintf(...); +#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; @@ -29,13 +38,13 @@ const char* command = NULL; struct { bool not; - bool or, orn, nor; + bool or, nor; - bool and, andn, nand; + bool and, nand; bool xor, nxor; - bool lt, lte, gt, gte; + bool compares; bool ternary; } use_operators; @@ -50,6 +59,8 @@ 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); @@ -82,15 +93,14 @@ static void parse_args(int argc, char* const* argv) use_operators.or = true; use_operators.and = true; - use_operators.orn = true; use_operators.nor = true; - - use_operators.andn = true; use_operators.nand = true; use_operators. xor = true; use_operators.nxor = true; + use_operators.compares = true; + unset_operators = false; break; } @@ -105,28 +115,18 @@ static void parse_args(int argc, char* const* argv) use_operators.not = true; else if (!strcmp(moving, "or") || !strcmp(moving, "||")) use_operators.or = true; - else if (!strcmp(moving, "orn") || !strcmp(moving, "|!")) - use_operators.orn = 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, "andn") || !strcmp(moving, "&!")) - use_operators.andn = 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, "<")) - use_operators.lt = true; - else if (!strcmp(moving, "<=")) - use_operators.lte = true; - else if (!strcmp(moving, ">")) - use_operators.gt = true; - else if (!strcmp(moving, ">=")) - use_operators.gte = true; + else if (!strcmp(moving, "compares")) + use_operators.compares = true; else if (!strcmp(moving, "ternary") || !strcmp(moving, "?:")) use_operators.ternary = true; else @@ -152,14 +152,14 @@ static void parse_args(int argc, char* const* argv) break; } - + case 'B': { force_rebuild = true; - + break; } - + default: assert(!"TODO"); break; @@ -179,11 +179,13 @@ static void parse_args(int argc, char* const* argv) #define Z 0b0000000011111111 #define M 0b1111111111111111 -#define N (65536) +#define B (16) + +#define N (1 << (B)) enum kind { ek_unreachable, - + ek_0, ek_1, ek_W, @@ -195,10 +197,8 @@ enum kind { ek_or, ek_and, - ek_orn, ek_nor, - ek_andn, ek_nand, ek_xor, @@ -216,7 +216,7 @@ struct expr { enum kind kind; uint16_t cond, left, right; - + int cost; } lookup[N]; @@ -248,7 +248,7 @@ static void print(uint16_t truthtable, int depth) assert(!"NOPE"); break; } - + case ek_0: { printf(print_with_color ? LITERAL_ESCAPE "0" RESET_ESCAPE : "0"); @@ -323,11 +323,9 @@ static void print(uint16_t truthtable, int depth) } 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, " != "); @@ -335,8 +333,9 @@ static void print(uint16_t truthtable, int depth) BINARY_OPERATOR(ek_lt, " < "); BINARY_OPERATOR(ek_lte, " <= "); - BINARY_OPERATOR(ek_gt, " > "); - BINARY_OPERATOR(ek_gte, " >= "); + + BINARY_OPERATOR(ek_gt, " < "); + BINARY_OPERATOR(ek_gte, " <= "); #undef BINARY_OPERATOR @@ -364,248 +363,284 @@ static void print(uint16_t truthtable, int depth) } } +// 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; 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, uint16_t e) +{ + zprintf("%*s" "boolset_add(e = 0b%hb):" "\n", calldepth++, "", e); + + assert(!this->data[0][e]); + + for (int k = 0; k < 16 && !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 < 16 && !--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++) { - for (int i = 0; i < N; i++) - { - lookup[i].kind = ek_unreachable; - - lookup[i].cost = INT_MAX; - } - } - - // heap of truthtables; key = cost - struct { - uint16_t data[N]; - int n; - - // truthtable -> index in 'todo' - int reverse[N]; - } todo; - - // init 'todo': - { - todo.n = 0; - - for (int i = 0; i < N; i++) - { - todo.reverse[i] = -1; - } - } - - uint16_t pop(void) - { - assert(todo.n > 0); + lookup[i].kind = ek_unreachable; - uint16_t retval = todo.data[0]; - - todo.reverse[retval] = -1; - - uint16_t moving = todo.data[todo.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 < todo.n && lookup[todo.data[left]].cost < cost) - smallest = todo.data[left]; - - if (right < todo.n && lookup[todo.data[right]].cost < lookup[smallest].cost) - smallest = todo.data[right]; - - if (smallest == moving) - { - todo.data[index] = moving; - - todo.reverse[moving] = index; - } - else - { - int new = todo.reverse[smallest]; - - todo.data[index] = smallest; - - todo.reverse[smallest] = index; - - index = new; - - goto again; - } - } - - return retval; + lookup[i].cost = INT_MAX; } - void append(uint16_t truthtable, int cost) - { - assert(todo.reverse[truthtable] == -1); + // list of truthtables we're still working on, sorted by cost. + struct heap* todo = new_heap(); - int index = todo.n++, new_index; - - while (index > 0 && lookup[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; - - lookup[truthtable].cost = cost; - } - - void update(uint16_t truthtable, int cost) - { - assert(todo.reverse[truthtable] != -1); - - assert(cost < lookup[truthtable].cost); - - int index = todo.reverse[truthtable], new_index; - - while (index > 0 && lookup[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; - - lookup[truthtable].cost = cost; - } - // create a list truthtables we're done with // and another list of truthtables we're still working on. - struct boollist { - int _128[2], _64[4], _32[8], _16[16], _8[32], _4[64], _2[128], _1[256]; - } done, undone; + struct boolset* done = new_empty_boolset(); + struct boolset* undone = new_full_boolset(); - void init_empty(struct boollist* this) - { - assert(!"TODO"); - #if 0 - this->head = -1; - - for (int i = 0; i < N; i++) - { - this->headtails[i] = -1; - - this->in[i] = false; - } - #endif - } + 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; - void init_full(struct boollist* this) - { - assert(!"TODO"); - } - - assert(!"TODO"); - // init(&done), init(&undone); - - void insert(struct boollist* this, uint16_t element) - { - assert(!"TODO"); - #if 0 - assert(!done.in[index]); - - 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) - done.next[head] = index; - else - done.next[tophalftail] = done.headtails[prevhead - 1]; - } - 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) - done.next[index] = tail; - else - done.next[index] = done.headtails[prevtail + 1]; - } - else - { - done.next[index] = -1; - } - - done.in[index] = true; - #endif - } - - void remove(struct boollist* this, uint16_t element) - { - assert(!"TODO"); - } + heap_push(todo, 0, 1), lookup[0].kind = ek_0; + heap_push(todo, M, 1), lookup[M].kind = ek_1; - append(W, 0), lookup[W].kind = ek_W; - append(X, 0), lookup[X].kind = ek_X; - append(Y, 0), lookup[Y].kind = ek_Y; - append(Z, 0), lookup[Z].kind = ek_Z; - - append(0, 1), lookup[0].kind = ek_0; - append(M, 1), lookup[M].kind = ek_1; - - for (int iterations = 1; todo.n && iterations <= N; iterations++) + for (int iterations = 1; todo->n && iterations <= N; iterations++) { - uint16_t truthtable = pop(); + zprintf("%*s" "iterations = %i" "\n", calldepth, "", iterations); + + uint16_t truthtable = heap_pop(todo); - assert(!"TODO"); - #if 0 - insert(truthtable); + zprintf("%*s" "truthtable = %#hb" "\n", calldepth, "", truthtable); + boolset_add(done, truthtable), boolset_discard(undone, truthtable); + int cost = lookup[truthtable].cost; if (verbose) { - if (print_with_color) + if (!ZDEBUG && print_with_color) { printf("\e[2K"); } - printf("%i of %i (%.2f%%): [%i] ", - iterations, N, (100.0 * iterations / N), cost); + printf("%i of %i (%.2f%%): [%i] ", iterations, N, (100.0 * iterations / N), cost); print(truthtable, 0), puts(""); - if (print_with_color) + if (!ZDEBUG && print_with_color) { printf("\e[1A"); } @@ -620,13 +655,13 @@ void calculate_simplifications(void) if (not_cost < lookup[not_truthtable].cost) { - if (todo.reverse[not_truthtable] == -1) + if (todo->reverse[not_truthtable] == -1) { - append(not_truthtable, not_cost); + heap_push(todo, not_truthtable, not_cost); } else { - update(not_truthtable, not_cost); + heap_update(todo, not_truthtable, not_cost); } lookup[not_truthtable].kind = ek_not; @@ -634,177 +669,994 @@ void calculate_simplifications(void) } } - // this macro will be removed soon... - - assert(!"TODO"); - #if 0 - #define BINARY_OPERATOR(ekind, function) \ + #define CONSIDER(ekind) \ { \ - for (int i = done.head; i != -1; i = done.next[i]) \ + int bin_cost = 1 + cost + lookup[bi].cost; \ + \ + if (bin_cost < lookup[ci].cost) \ { \ + if (todo->reverse[ci] == -1) \ { \ - uint16_t bin_truthtable = function(truthtable, i) & M; \ - \ - int bin_cost = 1 + cost + lookup[i].cost; \ - \ - if (bin_cost < lookup[bin_truthtable].cost) \ - { \ - if (todo.reverse[bin_truthtable] == -1) \ - append(bin_truthtable, bin_cost); \ - else \ - update(bin_truthtable, bin_cost); \ - \ - lookup[bin_truthtable].kind = ekind; \ - lookup[bin_truthtable].left = truthtable; \ - lookup[bin_truthtable].right = i; \ - } \ + heap_push(todo, ci, bin_cost); \ + } \ + else \ + { \ + heap_update(todo, ci, bin_cost); \ } \ \ - { \ - uint16_t bin_truthtable = function(i, truthtable) & M; \ - \ - int bin_cost = 1 + cost + lookup[i].cost; \ - \ - if (bin_cost < lookup[bin_truthtable].cost) \ - { \ - if (todo.reverse[bin_truthtable] == -1) \ - append(bin_truthtable, bin_cost); \ - else \ - update(bin_truthtable, bin_cost); \ - \ - lookup[bin_truthtable].kind = ekind; \ - lookup[bin_truthtable].left = i; \ - lookup[bin_truthtable].right = truthtable; \ - } \ - } \ + lookup[ci].kind = ekind; \ + lookup[ci].left = truthtable; \ + lookup[ci].right = bi; \ } \ } - - #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 (use_operators.or) { - BINARY_OPERATOR(ek_or, OR); - } - - if (use_operators.and) - { - BINARY_OPERATOR(ek_and, AND); - } - - if (use_operators.orn) - { - BINARY_OPERATOR(ek_orn, ORN); + // 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) { - BINARY_OPERATOR(ek_nor, 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.andn) + if (use_operators.and) { - BINARY_OPERATOR(ek_andn, ANDN); + // 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) { - BINARY_OPERATOR(ek_nand, 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) { - BINARY_OPERATOR(ek_xor, 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) { - BINARY_OPERATOR(ek_nxor, 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.lt) + if (use_operators.compares) { - BINARY_OPERATOR(ek_lt, LT); + // < + // 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.lte) - { - BINARY_OPERATOR(ek_lte, LTE); - } - - if (use_operators.gt) - { - BINARY_OPERATOR(ek_gt, GT); - } - - if (use_operators.gte) - { - BINARY_OPERATOR(ek_gte, GTE); - } - + if (use_operators.ternary) { - for (int i = done.head; i != -1; i = done.next[i]) + // 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) { - for (int j = done.head; j != -1; j = done.next[j]) + zprintf("%*s" "search(k = %i):" "\n", calldepth++, "", k); + + if (k >= 0) { - int ternary_cost = 1 + cost + lookup[i].cost + lookup[j].cost; - - #define TERNARY(C, T, F) \ - { \ - uint16_t ternary_truthtable = \ - ((C) & (T)) | (~(C) & (F)); \ - \ - if (ternary_cost < lookup[ternary_truthtable].cost) \ - { \ - if (todo.reverse[ternary_truthtable] == -1) \ - { \ - append(ternary_truthtable, ternary_cost); \ - } \ - else \ - { \ - update(ternary_truthtable, ternary_cost); \ - } \ - \ - lookup[ternary_truthtable].kind = ek_ternary; \ - lookup[ternary_truthtable].cond = (C); \ - lookup[ternary_truthtable].left = (T); \ - lookup[ternary_truthtable].right = (F); \ - } \ - } \ - - TERNARY(truthtable, i, j); - TERNARY(i, truthtable, j); - TERNARY(i, j, truthtable); + 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); } - #endif - #endif } - if (verbose && print_with_color) + 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-2"; + char path[PATH_MAX] = ".simplifier-cache-3"; if (use_operators.not) strcat(path, "-not"); @@ -812,18 +1664,12 @@ void get_simplifications(void) if (use_operators.or) strcat(path, "-or"); - if (use_operators.orn) - strcat(path, "-orn"); - if (use_operators.nor) strcat(path, "-nor"); if (use_operators.and) strcat(path, "-and"); - if (use_operators.andn) - strcat(path, "-andn"); - if (use_operators.nand) strcat(path, "-nand"); @@ -833,17 +1679,8 @@ void get_simplifications(void) if (use_operators.nxor) strcat(path, "-nxor"); - if (use_operators.lt) - strcat(path, "-lt"); - - if (use_operators.lte) - strcat(path, "-lte"); - - if (use_operators.gt) - strcat(path, "-gt"); - - if (use_operators.gte) - strcat(path, "-gte"); + if (use_operators.compares) + strcat(path, "-compares"); if (use_operators.ternary) strcat(path, "-ternary"); @@ -875,9 +1712,9 @@ void get_simplifications(void) "\n" "This may take a while." "\n" ""); - + rebuild: {}; - + if (!verbose) { puts("re-run with '-v' to watch progress"); @@ -1457,11 +2294,11 @@ int main(int argc, char* const* argv) max_cost); puts(""); } - + for (char* line; (line = readline(">>> ")); free(line)) { add_history(line); - + uint16_t truthtable = evaluate(line); // printf("truthtable = 0b%016b\n", truthtable); diff --git a/spikes/boolean-array-or-2.c b/spikes/boolean-array-or-2.c index e69de29..239fa73 100644 --- a/spikes/boolean-array-or-2.c +++ b/spikes/boolean-array-or-2.c @@ -0,0 +1,148 @@ + +#include +#include +#include + +#ifdef ZDEBUG + #define zprintf(fmt, ...) printf(fmt, ## __VA_ARGS__); +#else + #define zprintf(...) ; +#endif + +#define N (256) + +#define M (255) + +struct boolist +{ + int data[8][256]; +}; + +void init(struct boolist* this) +{ + memset(this, 0, sizeof(*this)); +} + +void add(struct boolist* this, int e) +{ + zprintf("insert(e = %i);\n", e); + + if (!this->data[0][e]) + { + for (int k = 0; k < 8 && !this->data[k][e >> k]++; k++); + } +} + +void search( + struct boolist* alist, + struct boolist* blist, + int k, + int ai, int bi, + int findme, + int calldepth) +{ + zprintf("%*s" "search(k = %i, ai = %#b, bi = %#b, findme = %#b):" "\n", calldepth++, "", k, ai, bi, findme); + + if (k >= 0) + { + // x | y | z + //----------- + // 0 | 0 | 0 + // 0 | 1 | 1 + // 1 | 0 | 1 + // 1 | 1 | 1 + + if (findme & (1 << k)) + { + // there are three cases that would make 'z' one: + zprintf("%*s" "one case" "\n", calldepth, ""); + + // x is 0 and y is 1: + if (alist->data[k][(ai >> k) + 0] && blist->data[k][(bi >> k) + 1]) + { + search(alist, blist, k - 1, ai, bi + (1 << k), findme, calldepth); + } + + // x is 1 and y is 0: + if (alist->data[k][(ai >> k) + 1] && blist->data[k][(bi >> k) + 0]) + { + search(alist, blist, k - 1, ai + (1 << k), bi, findme, calldepth); + } + + // x is 1 and y is 1: + if (alist->data[k][(ai >> k) + 1] && blist->data[k][(bi >> k) + 1]) + { + search(alist, blist, k - 1, ai + (1 << k), bi + (1 << k), findme, calldepth); + } + } + else + { + zprintf("%*s" "zero case" "\n", calldepth, ""); + + // there's only one case when 'z' is zero: 'x' and 'y' both + // must be zero. + + // check that both corrasponding quadrants are not empty first. + if (alist->data[k][(ai >> k) + 0] && blist->data[k][(bi >> k) + 0]) + { + search(alist, blist, k - 1, ai, bi, findme, calldepth); + } + } + } + else + { + assert((ai | bi) == findme); + + printf("%2i (0b%05b) | %2i (0b%05b) == %2i (0b%05b)" "\n", + ai, ai, bi, bi, findme, findme); + } +} + +// 0 1 2 3 4 5 6 7 8 9 +int a[10] = { 2, 4, 5, 7, 9, 11, 15, 17, 17, 19}; +int b[10] = {10, 11, 11, 14, 14, 19, 20, 23, 26, 29}; + +// [ 0] [ 1] [ 2] [ 3] [ 4] [ 5] [ 6] [ 7] [ 8] [ 9] +// 2 4 5 7 9 11 15 17 17 19 +// -------------------------------------------------- +// [ 0] 10 | 10 14 15 15 11 11 15 27 27 27 + +// [ 1] 11 | 11 15 15 15 11 11 15 27 27 27 + +// [ 2] 11 | 11 15 15 15 11 11 15 27 27 27 + +// [ 3] 14 | 14 14 15 15 15 15 15 31 31 31 + +// [ 4] 14 | 14 14 15 15 15 15 15 31 31 31 + +// [ 5] 19 | 19 (23) (23) (23) 27 27 31 19 19 19 + +// [ 6] 20 | 22 20 21 (23) 29 31 31 21 21 (23) + +// [ 7](23)|(23) (23) (23) (23) 31 31 31 (23) (23) (23) + +// [ 8] 26 | 26 30 31 31 27 27 31 27 27 27 + +// [ 9] 29 | 31 29 29 31 29 31 31 29 29 31 + +int main() +{ + struct boolist alist, blist; + + init(&alist), init(&blist); + + for (int i = 0; i < 10; i++) + { + add(&alist, a[i]); + } + + for (int i = 0; i < 10; i++) + { + add(&blist, b[i]); + } + + search(&alist, &blist, 7, 0, 0, 23, 0); + + return 0; +} + diff --git a/spikes/boolean-array-reverse-or.c b/spikes/boolean-array-reverse-or.c new file mode 100644 index 0000000..c34c8a4 --- /dev/null +++ b/spikes/boolean-array-reverse-or.c @@ -0,0 +1,189 @@ + +#include +#include +#include +#include + +#ifdef ZDEBUG + #define zprintf(fmt, ...) printf(fmt, ## __VA_ARGS__); +#else + #define zprintf(...) ; +#endif + +#define TODO \ + assert(!"TODO"); + +#define N (256) + +#define M (255) + +struct boolist +{ + int data[8][256]; +}; + +void init(struct boolist* this) +{ + memset(this, 0, sizeof(*this)); +} + +void add(struct boolist* this, int e) +{ + zprintf("insert(e = %i);\n", e); + + if (!this->data[0][e]) + { + for (int k = 0; k < 8 && !this->data[k][e >> k]++; k++); + } +} + +void search( + int a, + struct boolist* blist, + struct boolist* clist, + int k, + int bi, int ci, + int calldepth) +{ + zprintf("%*s" "search(k = %i, bi = %#b, ci = %#b):" "\n", + calldepth++, "", k, bi, ci); + + if (k >= 0) + { + // a | b | c + //----------- + // 0 | 0 | 0 + // 0 | 1 | 1 + // 1 | 0 | 1 + // 1 | 1 | 1 + + if (a & (1 << k)) + { + // there are three cases that would make 'z' one: + zprintf("%*s" "one case" "\n", calldepth, ""); + + // if the left operand is providing the one-ness, then the right + // operand can be whatever it wants, and the resultant must be one + + // b == 0 and c == 1 + if (blist->data[k][(bi >> k) + 0] && clist->data[k][(ci >> k) + 1]) + { + search(a, blist, clist, k - 1, bi, ci + (1 << k), calldepth); + } + + // b == 1 and c == 1 + if (blist->data[k][(bi >> k) + 1] && clist->data[k][(ci >> k) + 1]) + { + search(a, blist, clist, k - 1, bi + (1 << k), ci + (1 << k), calldepth); + } + } + else + { + zprintf("%*s" "zero case" "\n", calldepth, ""); + + // there two cases to consider then. If the left operand + // is not providing the one-ness, then it's up to the right operand + // to provide it if it's needed. + + // b == 0 and c == 0 + if (blist->data[k][(bi >> k) + 0] && clist->data[k][(ci >> k) + 0]) + { + search(a, blist, clist, k - 1, bi, ci, calldepth); + } + + // b == 1 and c == 1 + if (blist->data[k][(bi >> k) + 1] && clist->data[k][(ci >> k) + 1]) + { + search(a, blist, clist, k - 1, bi + (1 << k), ci + (1 << k), calldepth); + } + } + } + else + { + printf("%2i (0b%05b) | %2i (0b%05b) == %2i (0b%05b)" "\n", + a, a, bi, bi, ci, ci); + + assert((a | bi) == ci); + } +} + + +int a = 17; + +// 0 1 2 3 4 5 6 7 8 9 +int b[10] = {10, 11, 11, 14, 14, 19, 20, 23, 26, 29}; + +int c[20] = { +// 0 1 2 3 4 5 6 7 8 9 + 15, 17, 19, 21, 22, 25, 26, 26, 27, 32, + +// 10 11 12 13 14 15 16 17 18 19 + 33, 33, 36, 39, 42, 44, 48, 49, 49, 49 +}; + +// [ 0] [ 1] [ 2] [ 3] [ 4] [ 5] [ 6] [ 7] [ 8] [ 9] +// 10 11 11 14 14 19 20 23 26 29 +// -------------------------------------------------- +// [ 0] 15 | 5 4 4 1 1 12 11 8 5 2 + +// [ 1] 17 | 17 16 16 17 17 0 1 0 1 0 + +// [ 2] 19 | 17 16 16 17 17 (0) 3 0 1 2 + +// [ 3] 21 | 21 20 20 17 17 4 (1) 0 5 0 + +// [ 4] 22 | 20 20 20 16 16 4 2 0 4 2 + +// [ 5] 25 | 17 16 16 17 17 8 9 8 1 0 + +// [ 6] 26 | 16 16 16 16 16 8 10 8 0 2 + +// [ 7] 26 | 16 16 16 16 16 8 10 8 0 2 + +// [ 8] 27 |(17) (16) (16) 17 17 8 11 8 ( 1) 2 + +// [ 9] 32 | 32 32 32 32 32 32 32 32 32 32 + +// [10] 33 | 33 32 32 33 33 32 33 32 33 32 + +// [11] 33 | 33 32 32 33 33 32 33 32 33 32 + +// [12] 36 | 36 36 36 32 32 36 32 32 36 32 + +// [13] 39 | 37 36 36 33 33 36 35 32 37 34 + +// [14] 42 | 32 32 32 32 32 40 42 40 32 34 + +// [15] 44 | 36 36 36 32 32 44 40 40 36 32 + +// [16] 48 | 48 48 48 48 48 32 32 32 32 32 + +// [17] 49 | 49 48 48 49 49 32 33 32 33 32 + +// [18] 49 | 49 48 48 49 49 32 33 32 33 32 + +// [19] 49 | 49 48 48 49 49 32 33 32 33 32 + + + +int main() +{ + struct boolist blist, clist; + + init(&blist), init(&clist); + + for (int i = 0; i < 10; i++) + { + add(&blist, b[i]); + } + + for (int i = 0; i < 20; i++) + { + add(&clist, c[i]); + } + + search(a, &blist, &clist, 7, 0, 0, 0); + + return 0; +} + diff --git a/spikes/boolean-array.c b/spikes/boolean-array.c index 04457c6..b6be01c 100644 --- a/spikes/boolean-array.c +++ b/spikes/boolean-array.c @@ -11,36 +11,36 @@ struct boolist { int data[8][256]; } list = {}; -void insert(int e) +void add(int e) { printf("insert(e = %i);\n", e); - + assert(!list.data[0][e]); - + for (int k = 0; k < 8 && !list.data[k][e >> k]++; k++); } -void delete(int e) +void discard(int e) { - printf("delete(e = %i);\n", e); - + printf("discard(e = %i);\n", e); + assert(list.data[0][e]); - + for (int k = 0; k < 8 && !--list.data[k][e >> k]; k++); } void print() { puts("print():"); - + void walk(int k, int i) { if (k >= 0) { int* a = &list.data[k][i >> k]; - + if (a[0]) walk(k - 1, i); - + if (a[1]) walk(k - 1, i + (1 << k)); } else @@ -48,42 +48,42 @@ void print() printf(" " "%i\n", i); } } - + walk(7, 0); } int main() { print(); - - insert(42); - + + add(42); + print(); - - insert(101); - + + add(101); + print(); - - delete(42); - + + discard(42); + print(); - - insert(34); - + + add(34); + print(); - - insert(35); - + + add(35); + print(); - - insert(36); - + + add(36); + print(); - - delete(35); - + + discard(35); + print(); - + return 0; } diff --git a/spikes/quadrant-or-1.c b/spikes/quadrant-or-1.c index a992d12..21ae38c 100644 --- a/spikes/quadrant-or-1.c +++ b/spikes/quadrant-or-1.c @@ -23,7 +23,7 @@ void search( else { assert((ai | bi) == findme); - + printf("0b%04b | 0b%04b == 0b%04b " "(%2i | %2i == %2i)\n", ai, bi, findme, ai, bi, findme); } @@ -32,6 +32,6 @@ void search( int main() { search(0b1000, 0, 0, 11); - + return 0; } diff --git a/spikes/quadrant-or-2.c b/spikes/quadrant-or-2.c index aa6d69f..913f87f 100644 --- a/spikes/quadrant-or-2.c +++ b/spikes/quadrant-or-2.c @@ -43,13 +43,13 @@ int binary( while (n > 1) { int m = n / 2; - + if (array[i + m] & mask) n = m; else i += m, n = n - m; } - + return (array[i] & mask) ? i : i + 1; } @@ -61,32 +61,32 @@ void search( int calldepth) { zprintf("%*s" "search():" "\n", calldepth++, ""); - + zprintf("%*s" "mask = 0b%05b" "\n", calldepth, "", mask); - + zprintf("%*s" "findme = 0b%05b" "\n", calldepth, "", findme); - + zprintf("%*s" "ai = %i" "\n", calldepth, "", ai); zprintf("%*s" "an = %i" "\n", calldepth, "", an); - + zprintf("%*s" "bi = %i" "\n", calldepth, "", bi); zprintf("%*s" "bn = %i" "\n", calldepth, "", bn); - + if (mask) { int asplit = binary(mask, a + ai, 0, an); int bsplit = binary(mask, b + bi, 0, bn); - + zprintf("%*s" "asplit = %i" "\n", calldepth, "", asplit); zprintf("%*s" "bsplit = %i" "\n", calldepth, "", bsplit); - + assert((asplit == an) || (a[ai + asplit] & mask)); assert((bsplit == bn) || (b[bi + bsplit] & mask)); - + if (mask & findme) { zprintf("%*s" "one path" "\n", calldepth, ""); - + // 0 ... (asplit - 1) | asplit ... (an - 1) // --------------------- ------------------- // 0 | | | @@ -98,12 +98,12 @@ void search( // (bn - 1) | | | // --- | | | // ---------------------- ------------------- - + // second quadrant. if (asplit < an && 0 < bsplit) { zprintf("%*s" "entering second quadrant." "\n", calldepth, ""); - + search( mask >> 1, ai + asplit, an - asplit, @@ -115,12 +115,12 @@ void search( { zprintf("%*s" "empty second quadrant." "\n", calldepth, ""); } - + // third quadrant. if (0 < asplit && bsplit < bn) { zprintf("%*s" "entering third quadrant." "\n", calldepth, ""); - + search( mask >> 1, ai, asplit, @@ -132,12 +132,12 @@ void search( { zprintf("%*s" "empty third quadrant." "\n", calldepth, ""); } - + // fourth quadrant. if (asplit < an && bsplit < bn) { zprintf("%*s" "entering fourth quadrant." "\n", calldepth, ""); - + search( mask >> 1, ai + asplit, an - asplit, @@ -153,12 +153,12 @@ void search( else { zprintf("%*s" "zero path" "\n", calldepth, ""); - + // first quadrant. if (0 < asplit && 0 < bsplit) { zprintf("%*s" "entering first quadrant." "\n", calldepth, ""); - + search( mask >> 1, ai, asplit, @@ -177,7 +177,7 @@ void search( for (int j = 0; j < bn; j++) { assert((a[ai + i] | b[bi + j]) == findme); - + printf("%2i [%2i] (0b%05b) | %2i [%2i] " "(0b%05b) == %2i (0b%05b)" "\n", a[ai + i], ai + i, a[ai + i], @@ -185,7 +185,7 @@ void search( findme, findme); } } - + calldepth--; } @@ -197,7 +197,7 @@ int main() 0, 10, 23, 0); - + return 0; }