637 lines
16 KiB
C
637 lines
16 KiB
C
|
|
#include <unistd.h>
|
|
#include <stdio.h>
|
|
#include <limits.h>
|
|
#include <assert.h>
|
|
#include <stdbool.h>
|
|
|
|
#include <debug.h>
|
|
|
|
#include <cmdln.h>
|
|
|
|
#include <print.h>
|
|
|
|
#ifdef MULTITHREADED_BUILD
|
|
#include <pthread.h>
|
|
#endif
|
|
|
|
#include "calculate_simplifications.h"
|
|
|
|
void helper(
|
|
const struct cmdln_flags* flags,
|
|
struct simplifications* simps,
|
|
bool have_extra_variable,
|
|
uint16_t A)
|
|
{
|
|
ENTER;
|
|
|
|
struct row* row = have_extra_variable ? &simps->with_vars[A] : &simps->main;
|
|
|
|
// init 'row->data':
|
|
{
|
|
for (int i = 0; i < N; i++)
|
|
{
|
|
row->data[i].kind = ek_unreachable;
|
|
|
|
row->data[i].cost = INT_MAX;
|
|
}
|
|
}
|
|
|
|
// heap of truthtables; key = cost
|
|
struct {
|
|
uint16_t data[N];
|
|
int n;
|
|
|
|
// truthtable -> index in 'todo'
|
|
int reverse[N];
|
|
} todo;
|
|
|
|
// init 'todo':
|
|
{
|
|
todo.n = 0;
|
|
|
|
for (int i = 0; i < N; i++)
|
|
{
|
|
todo.reverse[i] = -1;
|
|
}
|
|
}
|
|
|
|
uint16_t pop(void)
|
|
{
|
|
assert(todo.n > 0);
|
|
|
|
uint16_t retval = todo.data[0];
|
|
|
|
todo.reverse[retval] = -1;
|
|
|
|
uint16_t moving = todo.data[todo.n-- - 1];
|
|
|
|
int cost = row->data[moving].cost;
|
|
|
|
int index = 0;
|
|
|
|
again:
|
|
{
|
|
int left = index * 2 + 1;
|
|
int right = index * 2 + 2;
|
|
|
|
uint16_t smallest = moving;
|
|
|
|
if (left < todo.n && row->data[todo.data[left]].cost < cost)
|
|
smallest = todo.data[left];
|
|
|
|
if (right < todo.n && row->data[todo.data[right]].cost < row->data[smallest].cost)
|
|
smallest = todo.data[right];
|
|
|
|
if (smallest == moving)
|
|
{
|
|
todo.data[index] = moving;
|
|
|
|
todo.reverse[moving] = index;
|
|
}
|
|
else
|
|
{
|
|
int new = todo.reverse[smallest];
|
|
|
|
todo.data[index] = smallest;
|
|
|
|
todo.reverse[smallest] = index;
|
|
|
|
index = new;
|
|
|
|
goto again;
|
|
}
|
|
}
|
|
|
|
return retval;
|
|
}
|
|
|
|
void append(uint16_t truthtable, int cost)
|
|
{
|
|
assert(todo.reverse[truthtable] == -1);
|
|
|
|
int index = todo.n++, new_index;
|
|
|
|
while (index > 0 && row->data[todo.data[new_index = (index - 1) / 2]].cost > cost)
|
|
{
|
|
todo.data[index] = todo.data[new_index];
|
|
|
|
todo.reverse[todo.data[new_index]] = index;
|
|
|
|
index = new_index;
|
|
}
|
|
|
|
todo.data[index] = truthtable;
|
|
|
|
todo.reverse[truthtable] = index;
|
|
|
|
row->data[truthtable].cost = cost;
|
|
}
|
|
|
|
void update(uint16_t truthtable, int cost)
|
|
{
|
|
assert(todo.reverse[truthtable] != -1);
|
|
|
|
assert(cost < row->data[truthtable].cost);
|
|
|
|
int index =todo. reverse[truthtable], new_index;
|
|
|
|
while (index > 0 && row->data[todo.data[new_index = (index - 1) / 2]].cost > cost)
|
|
{
|
|
todo.data[index] = todo.data[new_index];
|
|
|
|
todo.reverse[todo.data[new_index]] = index;
|
|
|
|
index = new_index;
|
|
}
|
|
|
|
todo.data[index] = truthtable;
|
|
todo.reverse[truthtable] = index;
|
|
|
|
row->data[truthtable].cost = cost;
|
|
}
|
|
|
|
// create a list of the "done" truthtables
|
|
struct {
|
|
int headtails[N], next[N], head;
|
|
|
|
// for debugging:
|
|
#if ZDEBUG
|
|
bool in[N];
|
|
#endif
|
|
} done = {};
|
|
|
|
// init 'done':
|
|
{
|
|
done.head = -1;
|
|
|
|
for (int i = 0; i < N; i++)
|
|
{
|
|
done.headtails[i] = -1;
|
|
|
|
#if ZDEBUG
|
|
done.in[i] = false;
|
|
#endif
|
|
}
|
|
}
|
|
|
|
void insert(int index)
|
|
{
|
|
#if ZDEBUG
|
|
assert(!done.in[index]);
|
|
#endif
|
|
|
|
int head = index & 1 ? index & ~(index & -index) : index, prevhead = -1;
|
|
|
|
while (done.headtails[head] == -1 || index < done.headtails[head])
|
|
{
|
|
done.headtails[head] = index;
|
|
|
|
prevhead = head, head = head & ~(head & -head);
|
|
}
|
|
|
|
if (done.headtails[head] < index)
|
|
{
|
|
if (prevhead == -1)
|
|
{
|
|
assert(done.headtails[head] == head);
|
|
|
|
done.next[head] = index;
|
|
}
|
|
else
|
|
{
|
|
int tophalftail = done.headtails[prevhead - 1];
|
|
|
|
assert(tophalftail != -1);
|
|
|
|
done.next[tophalftail] = index;
|
|
}
|
|
}
|
|
else
|
|
{
|
|
done.head = index;
|
|
}
|
|
|
|
int n = ~index & M;
|
|
int tail = index & 1 ? index : index | (n & -n), prevtail = -1;
|
|
|
|
while (done.headtails[tail] == -1 || done.headtails[tail] < index)
|
|
{
|
|
done.headtails[tail] = index;
|
|
|
|
prevtail = tail, tail = tail | (n = ~tail & M, n & -n);
|
|
}
|
|
|
|
if (index < done.headtails[tail])
|
|
{
|
|
if (prevtail == -1)
|
|
{
|
|
assert(done.headtails[tail] == tail);
|
|
|
|
#if ZDEBUG
|
|
assert(done.in[tail]);
|
|
#endif
|
|
|
|
done.next[index] = tail;
|
|
}
|
|
else
|
|
{
|
|
int bottomhalfhead = done.headtails[prevtail + 1];
|
|
|
|
assert(bottomhalfhead != -1);
|
|
|
|
done.next[index] = bottomhalfhead;
|
|
}
|
|
}
|
|
else
|
|
{
|
|
done.next[index] = -1;
|
|
}
|
|
|
|
#if ZDEBUG
|
|
done.in[index] = true;
|
|
#endif
|
|
}
|
|
|
|
append(W, 0), row->data[W].kind = ek_W;
|
|
append(X, 0), row->data[X].kind = ek_X;
|
|
append(Y, 0), row->data[Y].kind = ek_Y;
|
|
append(Z, 0), row->data[Z].kind = ek_Z;
|
|
|
|
append(0, 1), row->data[0].kind = ek_0;
|
|
append(M, 1), row->data[M].kind = ek_1;
|
|
|
|
if (have_extra_variable && todo.reverse[A] == -1)
|
|
{
|
|
append(A, 0), row->data[A].kind = ek_A;
|
|
}
|
|
|
|
// disable terminal autowrap:
|
|
if (!ZDEBUG && flags->verbose && flags->print_with_color)
|
|
{
|
|
printf("\e[?7l");
|
|
}
|
|
|
|
for (int iterations = 1; todo.n && iterations <= N; iterations++)
|
|
{
|
|
uint16_t truthtable = pop();
|
|
|
|
insert(truthtable);
|
|
|
|
int cost = row->data[truthtable].cost;
|
|
|
|
if (flags->verbose)
|
|
{
|
|
if (!ZDEBUG && flags->print_with_color)
|
|
{
|
|
printf("\e[2K");
|
|
}
|
|
|
|
printf("%i of %i (%.2f%%): [%i] ",
|
|
iterations, N, (100.0 * iterations / N), cost);
|
|
|
|
if (have_extra_variable)
|
|
{
|
|
printf("a = 0b%016b, ", A);
|
|
}
|
|
|
|
print(flags, simps, row, truthtable);
|
|
|
|
puts("");
|
|
|
|
if (!ZDEBUG && flags->print_with_color)
|
|
{
|
|
printf("\e[1A");
|
|
}
|
|
}
|
|
|
|
// consider NOT:
|
|
if (flags->use_operators.not)
|
|
{
|
|
uint16_t not_truthtable = ~truthtable & M;
|
|
|
|
int not_cost = cost + 1;
|
|
|
|
if (not_cost < row->data[not_truthtable].cost)
|
|
{
|
|
if (todo.reverse[not_truthtable] == -1)
|
|
{
|
|
append(not_truthtable, not_cost);
|
|
}
|
|
else
|
|
{
|
|
update(not_truthtable, not_cost);
|
|
}
|
|
|
|
row->data[not_truthtable].kind = ek_not;
|
|
row->data[not_truthtable].left = truthtable;
|
|
}
|
|
}
|
|
|
|
#define BINARY_OPERATOR(ekind, function) \
|
|
{ \
|
|
for (int i = done.head; i != -1; i = done.next[i]) \
|
|
{ \
|
|
{ \
|
|
uint16_t bin_truthtable = function(truthtable, i) & M; \
|
|
\
|
|
int bin_cost = 1 + cost + row->data[i].cost; \
|
|
\
|
|
if (bin_cost < row->data[bin_truthtable].cost) \
|
|
{ \
|
|
if (todo.reverse[bin_truthtable] == -1) \
|
|
append(bin_truthtable, bin_cost); \
|
|
else \
|
|
update(bin_truthtable, bin_cost); \
|
|
\
|
|
row->data[bin_truthtable].kind = ekind; \
|
|
row->data[bin_truthtable].left = truthtable; \
|
|
row->data[bin_truthtable].right = i; \
|
|
} \
|
|
} \
|
|
\
|
|
{ \
|
|
uint16_t bin_truthtable = function(i, truthtable) & M; \
|
|
\
|
|
int bin_cost = 1 + cost + row->data[i].cost; \
|
|
\
|
|
if (bin_cost < row->data[bin_truthtable].cost) \
|
|
{ \
|
|
if (todo.reverse[bin_truthtable] == -1) \
|
|
append(bin_truthtable, bin_cost); \
|
|
else \
|
|
update(bin_truthtable, bin_cost); \
|
|
\
|
|
row->data[bin_truthtable].kind = ekind; \
|
|
row->data[bin_truthtable].left = i; \
|
|
row->data[bin_truthtable].right = truthtable; \
|
|
} \
|
|
} \
|
|
} \
|
|
}
|
|
|
|
#define OR(a, b) ((a) | (b))
|
|
#define AND(a, b) ((a) & (b))
|
|
|
|
#define ORN(a, b) (~(a) | (b))
|
|
#define NOR(a, b) ~( (a) | (b))
|
|
#define ANDN(a, b) (~(a) & (b))
|
|
#define NAND(a, b) ~( (a) & (b))
|
|
#define XOR(a, b) (( a) ^ (b))
|
|
#define NXOR(a, b) ~( (a) ^ (b))
|
|
|
|
#define LT(a, b) ((~a) & (b))
|
|
#define LTE(a, b) ((~a) | (b))
|
|
#define GT(a, b) (( a) & ~(b))
|
|
#define GTE(a, b) (( a) | ~(b))
|
|
|
|
if (flags->use_operators.or)
|
|
{
|
|
BINARY_OPERATOR(ek_or, OR);
|
|
}
|
|
|
|
if (flags->use_operators.and)
|
|
{
|
|
BINARY_OPERATOR(ek_and, AND);
|
|
}
|
|
|
|
if (flags->use_operators.orn)
|
|
{
|
|
BINARY_OPERATOR(ek_orn, ORN);
|
|
}
|
|
|
|
if (flags->use_operators.nor)
|
|
{
|
|
BINARY_OPERATOR(ek_nor, NOR);
|
|
}
|
|
|
|
if (flags->use_operators.andn)
|
|
{
|
|
BINARY_OPERATOR(ek_andn, ANDN);
|
|
}
|
|
|
|
if (flags->use_operators.nand)
|
|
{
|
|
BINARY_OPERATOR(ek_nand, NAND);
|
|
}
|
|
|
|
if (flags->use_operators.xor)
|
|
{
|
|
BINARY_OPERATOR(ek_xor, XOR);
|
|
}
|
|
|
|
if (flags->use_operators.nxor)
|
|
{
|
|
BINARY_OPERATOR(ek_nxor, NXOR);
|
|
}
|
|
|
|
if (flags->use_operators.lt)
|
|
{
|
|
BINARY_OPERATOR(ek_lt, LT);
|
|
}
|
|
|
|
if (flags->use_operators.lte)
|
|
{
|
|
BINARY_OPERATOR(ek_lte, LTE);
|
|
}
|
|
|
|
if (flags->use_operators.gt)
|
|
{
|
|
BINARY_OPERATOR(ek_gt, GT);
|
|
}
|
|
|
|
if (flags->use_operators.gte)
|
|
{
|
|
BINARY_OPERATOR(ek_gte, GTE);
|
|
}
|
|
|
|
if (flags->use_operators.ternary)
|
|
{
|
|
for (int i = done.head; i != -1; i = done.next[i])
|
|
{
|
|
for (int j = done.head; j != -1; j = done.next[j])
|
|
{
|
|
int ternary_cost = 1 + cost + row->data[i].cost + row->data[j].cost;
|
|
|
|
#define TERNARY(C, T, F) \
|
|
{ \
|
|
uint16_t ternary_truthtable = \
|
|
((C) & (T)) | (~(C) & (F)); \
|
|
\
|
|
if (ternary_cost < row->data[ternary_truthtable].cost) \
|
|
{ \
|
|
if (todo.reverse[ternary_truthtable] == -1) \
|
|
{ \
|
|
append(ternary_truthtable, ternary_cost); \
|
|
} \
|
|
else \
|
|
{ \
|
|
update(ternary_truthtable, ternary_cost); \
|
|
} \
|
|
\
|
|
row->data[ternary_truthtable].kind = ek_ternary; \
|
|
row->data[ternary_truthtable].cond = (C); \
|
|
row->data[ternary_truthtable].left = (T); \
|
|
row->data[ternary_truthtable].right = (F); \
|
|
} \
|
|
} \
|
|
|
|
TERNARY(truthtable, i, j);
|
|
TERNARY(i, truthtable, j);
|
|
TERNARY(i, j, truthtable);
|
|
}
|
|
}
|
|
}
|
|
|
|
if (flags->use_operators.assignment)
|
|
{
|
|
assert(row == &simps->main);
|
|
|
|
for (int t = 0; t < N; t++)
|
|
{
|
|
int using_me_cost = simps->with_vars[truthtable].data[t].cost;
|
|
|
|
if (using_me_cost < INT_MAX)
|
|
{
|
|
int assign_cost = cost + 1 + using_me_cost;
|
|
|
|
if (assign_cost < simps->main.data[t].cost)
|
|
{
|
|
if (todo.reverse[t] == -1)
|
|
{
|
|
append(t, assign_cost);
|
|
}
|
|
else
|
|
{
|
|
update(t, assign_cost);
|
|
}
|
|
|
|
row->data[t].kind = ek_assignment;
|
|
row->data[t].left = truthtable;
|
|
row->data[t].right = t;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
// clear progress line, enable terminal autowrap:
|
|
if (!ZDEBUG && flags->verbose && flags->print_with_color)
|
|
{
|
|
printf("\e[2K"), printf("\e[?7h");
|
|
}
|
|
|
|
EXIT;
|
|
}
|
|
|
|
void calculate_simplifications(
|
|
const struct cmdln_flags* flags,
|
|
struct simplifications* simps)
|
|
{
|
|
ENTER;
|
|
|
|
if (flags->use_operators.assignment)
|
|
{
|
|
struct cmdln_flags flag_no_assign = *flags;
|
|
|
|
flag_no_assign.use_operators.assignment = false;
|
|
|
|
#ifdef MULTITHREADED_BUILD
|
|
{
|
|
int num_cores = sysconf(_SC_NPROCESSORS_ONLN);
|
|
|
|
zprintf("num_cores = %i" "\n", num_cores);
|
|
|
|
assert(0 < num_cores && num_cores < 100);
|
|
|
|
struct cmdln_flags flag_no_verbose = flag_no_assign;
|
|
|
|
if (!flags->quiet && flags->verbose)
|
|
{
|
|
printf(""
|
|
"note: the usual verbosity is disabled in the "
|
|
"multithreaded section" "\n"
|
|
"");
|
|
|
|
flag_no_verbose.verbose = false;
|
|
}
|
|
|
|
int starts[num_cores];
|
|
|
|
void* runner(void* _start)
|
|
{
|
|
const int* start = _start;
|
|
|
|
for (int a = *start; a < N; a += num_cores)
|
|
{
|
|
if (flags->verbose)
|
|
{
|
|
printf("a = 0b%016b" "\n", a);
|
|
}
|
|
|
|
helper(
|
|
/* cmdln flags: */ &flag_no_verbose,
|
|
/* simplifications */ simps,
|
|
/* have extra variable? */ true,
|
|
/* extra variable value: */ a);
|
|
}
|
|
|
|
return NULL;
|
|
}
|
|
|
|
pthread_t handles[num_cores];
|
|
|
|
for (int i = 0; i < num_cores; i++)
|
|
{
|
|
starts[i] = i;
|
|
|
|
pthread_create(
|
|
/* handle */ &handles[i],
|
|
/* attributes: */ NULL,
|
|
/* start_routine: */ runner,
|
|
/* arg: */ &starts[i]);
|
|
}
|
|
|
|
for (int i = 0; i < num_cores; i++)
|
|
{
|
|
pthread_join(
|
|
/* handle: */ handles[i],
|
|
/* return value: */ (void*[1]){});
|
|
}
|
|
}
|
|
#else
|
|
{
|
|
for (int a = 0; a < N; a++)
|
|
{
|
|
helper(
|
|
/* cmdln flags: */ &flag_no_assign,
|
|
/* simplifications */ simps,
|
|
/* have extra variable? */ true,
|
|
/* extra variable value: */ a);
|
|
}
|
|
}
|
|
#endif
|
|
}
|
|
|
|
helper(
|
|
/* cmdln flags: */ flags,
|
|
/* simplifications */ simps,
|
|
/* have extra variable? */ false,
|
|
/* extra variable value: */ 0);
|
|
|
|
EXIT;
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|