2346 lines
68 KiB
C
2346 lines
68 KiB
C
|
|
#include <string.h>
|
|
#include <stdint.h>
|
|
#include <errno.h>
|
|
#include <fcntl.h>
|
|
#include <stdio.h>
|
|
#include <stdbool.h>
|
|
#include <stdlib.h>
|
|
#include <unistd.h>
|
|
#include <assert.h>
|
|
#include <limits.h>
|
|
|
|
#include <readline/readline.h>
|
|
#include <readline/history.h>
|
|
|
|
#define argv0 program_invocation_name
|
|
|
|
#ifndef ZDEBUG
|
|
#define ZDEBUG 0
|
|
#endif
|
|
|
|
#if ZDEBUG
|
|
int calldepth = 0;
|
|
|
|
#define zprintf(fmt, ...) \
|
|
printf(fmt, ## __VA_ARGS__);
|
|
#else
|
|
#define zprintf(...);
|
|
#endif
|
|
|
|
#define TODO \
|
|
assert(!"TODO");
|
|
|
|
bool print_all_and_quit = false;
|
|
|
|
const char* command = NULL;
|
|
|
|
struct {
|
|
bool not;
|
|
|
|
bool or, nor;
|
|
|
|
bool and, nand;
|
|
|
|
bool xor, nxor;
|
|
|
|
bool compares;
|
|
|
|
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;
|
|
}
|
|
|
|
int main(int argc, char* const* argv)
|
|
{
|
|
parse_args(argc, argv);
|
|
|
|
get_simplifications();
|
|
|
|
if (print_all_and_quit)
|
|
{
|
|
for (int i = 0; i < N; i++)
|
|
{
|
|
int cost = lookup[i].cost;
|
|
|
|
if (cost != INT_MAX)
|
|
{
|
|
printf("0b%016b: [%2i]: ", i, cost), print(i, 0), puts("");
|
|
}
|
|
}
|
|
}
|
|
else if (command)
|
|
{
|
|
uint16_t truthtable = evaluate(command);
|
|
|
|
// printf("truthtable = 0b%016b\n", truthtable);
|
|
|
|
if (lookup[truthtable].kind == ek_unreachable)
|
|
{
|
|
puts("unreachable");
|
|
}
|
|
else
|
|
{
|
|
printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts("");
|
|
}
|
|
}
|
|
else
|
|
{
|
|
// Let's humble-brag just a little.
|
|
{
|
|
int max_cost = 0;
|
|
|
|
for (int i = 0; i < N; i++)
|
|
{
|
|
int cost = lookup[i].cost;
|
|
|
|
if (cost != INT_MAX && max_cost < cost)
|
|
{
|
|
max_cost = cost;
|
|
}
|
|
}
|
|
|
|
puts("");
|
|
printf("I can simplify any tree down to %i operators or less.\n",
|
|
max_cost);
|
|
puts("");
|
|
}
|
|
|
|
for (char* line; (line = readline(">>> ")); free(line))
|
|
{
|
|
add_history(line);
|
|
|
|
uint16_t truthtable = evaluate(line);
|
|
|
|
// printf("truthtable = 0b%016b\n", truthtable);
|
|
|
|
if (lookup[truthtable].kind == ek_unreachable)
|
|
{
|
|
puts("unreachable");
|
|
}
|
|
else
|
|
{
|
|
printf("%2i: ", lookup[truthtable].cost), print(truthtable, 0), puts("");
|
|
}
|
|
}
|
|
}
|
|
|
|
return 0;
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|