.
This commit is contained in:
parent
ff78073433
commit
1b9fe3b44a
7 changed files with 259 additions and 296 deletions
|
|
@ -11,120 +11,112 @@
|
|||
|
||||
#include "calculate_simplifications.h"
|
||||
|
||||
|
||||
static void init_simplifications(
|
||||
struct simplifications* simps)
|
||||
struct simplifications calculate_simplifications(
|
||||
const struct cmdln_flags* flags)
|
||||
{
|
||||
for (int i = 0; i < N; i++)
|
||||
struct simplifications simps = {};
|
||||
|
||||
// init 'simps.data':
|
||||
{
|
||||
simps->data[i].kind = ek_unreachable;
|
||||
for (int i = 0; i < N; i++)
|
||||
{
|
||||
simps.data[i].kind = ek_unreachable;
|
||||
|
||||
simps.data[i].cost = INT_MAX;
|
||||
}
|
||||
}
|
||||
|
||||
// heap of truthtables; key = cost
|
||||
struct {
|
||||
uint16_t data[N];
|
||||
int n;
|
||||
|
||||
simps->data[i].cost = INT_MAX;
|
||||
}
|
||||
}
|
||||
|
||||
struct heap
|
||||
{
|
||||
uint16_t data[N];
|
||||
int n;
|
||||
// truthtable -> index in 'todo'
|
||||
int reverse[N];
|
||||
} todo;
|
||||
|
||||
// truthtable -> index in 'todo'
|
||||
int reverse[N];
|
||||
};
|
||||
|
||||
static struct heap new_heap(void)
|
||||
{
|
||||
zprintf("new_heap" "\n");
|
||||
|
||||
struct heap todo = {};
|
||||
|
||||
todo.n = 0;
|
||||
|
||||
for (int i = 0; i < N; i++)
|
||||
// init 'todo':
|
||||
{
|
||||
todo.reverse[i] = -1;
|
||||
}
|
||||
|
||||
return todo;
|
||||
}
|
||||
|
||||
|
||||
uint16_t heap_pop(struct heap* todo, struct simplifications *simps)
|
||||
{
|
||||
assert(todo->n > 0);
|
||||
|
||||
uint16_t retval = todo->data[0];
|
||||
|
||||
todo->reverse[retval] = -1;
|
||||
|
||||
uint16_t moving = todo->data[todo->n-- - 1];
|
||||
|
||||
int cost = simps->data[moving].cost;
|
||||
|
||||
int index = 0;
|
||||
|
||||
again:
|
||||
{
|
||||
int left = index * 2 + 1;
|
||||
int right = index * 2 + 2;
|
||||
|
||||
uint16_t smallest = moving;
|
||||
|
||||
if (left < todo->n && simps->data[todo->data[left]].cost < cost)
|
||||
smallest = todo->data[left];
|
||||
|
||||
if (right < todo->n && simps->data[todo->data[right]].cost < simps->data[smallest].cost)
|
||||
smallest = todo->data[right];
|
||||
|
||||
if (smallest == moving)
|
||||
todo.n = 0;
|
||||
|
||||
for (int i = 0; i < N; i++)
|
||||
{
|
||||
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;
|
||||
todo.reverse[i] = -1;
|
||||
}
|
||||
}
|
||||
|
||||
return retval;
|
||||
}
|
||||
|
||||
|
||||
void heap_append(struct heap* todo, struct simplifications* simps, uint16_t truthtable, int cost)
|
||||
{
|
||||
zprintf("heap_append()" "\n");
|
||||
|
||||
assert(todo->reverse[truthtable] == -1);
|
||||
|
||||
int index = todo->n++, new_index;
|
||||
|
||||
while (index > 0 && simps->data[todo->data[new_index = (index - 1) / 2]].cost > cost)
|
||||
uint16_t pop(void)
|
||||
{
|
||||
todo->data[index] = todo->data[new_index];
|
||||
assert(todo.n > 0);
|
||||
|
||||
todo->reverse[todo->data[new_index]] = index;
|
||||
uint16_t retval = todo.data[0];
|
||||
|
||||
index = new_index;
|
||||
todo.reverse[retval] = -1;
|
||||
|
||||
uint16_t moving = todo.data[todo.n-- - 1];
|
||||
|
||||
int cost = simps.data[moving].cost;
|
||||
|
||||
int index = 0;
|
||||
|
||||
again:
|
||||
{
|
||||
int left = index * 2 + 1;
|
||||
int right = index * 2 + 2;
|
||||
|
||||
uint16_t smallest = moving;
|
||||
|
||||
if (left < todo.n && simps.data[todo.data[left]].cost < cost)
|
||||
smallest = todo.data[left];
|
||||
|
||||
if (right < todo.n && simps.data[todo.data[right]].cost < simps.data[smallest].cost)
|
||||
smallest = todo.data[right];
|
||||
|
||||
if (smallest == moving)
|
||||
{
|
||||
todo.data[index] = moving;
|
||||
|
||||
todo.reverse[moving] = index;
|
||||
}
|
||||
else
|
||||
{
|
||||
int new = todo.reverse[smallest];
|
||||
|
||||
todo.data[index] = smallest;
|
||||
|
||||
todo.reverse[smallest] = index;
|
||||
|
||||
index = new;
|
||||
|
||||
goto again;
|
||||
}
|
||||
}
|
||||
|
||||
return retval;
|
||||
}
|
||||
|
||||
void append(uint16_t truthtable, int cost)
|
||||
{
|
||||
assert(todo.reverse[truthtable] == -1);
|
||||
|
||||
int index = todo.n++, new_index;
|
||||
|
||||
while (index > 0 && simps.data[todo.data[new_index = (index - 1) / 2]].cost > cost)
|
||||
{
|
||||
todo.data[index] = todo.data[new_index];
|
||||
|
||||
todo.reverse[todo.data[new_index]] = index;
|
||||
|
||||
index = new_index;
|
||||
}
|
||||
|
||||
todo.data[index] = truthtable;
|
||||
|
||||
todo.reverse[truthtable] = index;
|
||||
|
||||
simps.data[truthtable].cost = cost;
|
||||
}
|
||||
|
||||
todo->data[index] = truthtable;
|
||||
|
||||
todo->reverse[truthtable] = index;
|
||||
|
||||
simps->data[truthtable].cost = cost;
|
||||
}
|
||||
|
||||
#if 0
|
||||
void update(uint16_t truthtable, int cost)
|
||||
{
|
||||
assert(todo.reverse[truthtable] != -1);
|
||||
|
|
@ -147,147 +139,134 @@ void heap_append(struct heap* todo, struct simplifications* simps, uint16_t trut
|
|||
|
||||
simps.data[truthtable].cost = cost;
|
||||
}
|
||||
#endif
|
||||
|
||||
// create a list of the "done" truthtables
|
||||
struct sparselist
|
||||
{
|
||||
int headtails[N], next[N], head;
|
||||
|
||||
// for debugging:
|
||||
#if ZDEBUG
|
||||
bool in[N];
|
||||
#endif
|
||||
};
|
||||
|
||||
struct sparselist new_sparselist(void)
|
||||
{
|
||||
struct sparselist done = {};
|
||||
// create a list of the "done" truthtables
|
||||
struct {
|
||||
int headtails[N], next[N], head;
|
||||
|
||||
// for debugging:
|
||||
#if ZDEBUG
|
||||
bool in[N];
|
||||
#endif
|
||||
} done = {};
|
||||
|
||||
done.head = -1;
|
||||
|
||||
for (int i = 0; i < N; i++)
|
||||
// init 'done':
|
||||
{
|
||||
done.headtails[i] = -1;
|
||||
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[i] = false;
|
||||
done.in[index] = true;
|
||||
#endif
|
||||
}
|
||||
|
||||
return done;
|
||||
}
|
||||
|
||||
void sparselist_insert(struct sparselist* this, int index)
|
||||
{
|
||||
TODO;
|
||||
#if 0
|
||||
#if ZDEBUG
|
||||
assert(!done.in[index]);
|
||||
#endif
|
||||
append(W, 0), simps.data[W].kind = ek_W;
|
||||
append(X, 0), simps.data[X].kind = ek_X;
|
||||
append(Y, 0), simps.data[Y].kind = ek_Y;
|
||||
append(Z, 0), simps.data[Z].kind = ek_Z;
|
||||
|
||||
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
|
||||
#endif
|
||||
}
|
||||
|
||||
|
||||
static void loop(
|
||||
const struct cmdln_flags* flags,
|
||||
struct simplifications* simps,
|
||||
struct heap* todo,
|
||||
struct sparselist* done)
|
||||
{
|
||||
zprintf("loop()" "\n");
|
||||
append(0, 1), simps.data[0].kind = ek_0;
|
||||
append(M, 1), simps.data[M].kind = ek_1;
|
||||
|
||||
// disable terminal autowrap:
|
||||
if (!ZDEBUG && flags->verbose && flags->print_with_color)
|
||||
if (flags->verbose && flags->print_with_color)
|
||||
{
|
||||
printf("\e[?7l");
|
||||
}
|
||||
|
||||
for (int iterations = 1; todo->n && iterations <= N; iterations++)
|
||||
for (int iterations = 1; todo.n && iterations <= N; iterations++)
|
||||
{
|
||||
uint16_t truthtable = heap_pop(todo, simps);
|
||||
uint16_t truthtable = pop();
|
||||
|
||||
if (!done)
|
||||
{
|
||||
sparselist_insert(done, truthtable);
|
||||
}
|
||||
insert(truthtable);
|
||||
|
||||
int cost = simps->data[truthtable].cost;
|
||||
int cost = simps.data[truthtable].cost;
|
||||
|
||||
if (flags->verbose)
|
||||
{
|
||||
if (!ZDEBUG && flags->print_with_color)
|
||||
if (flags->print_with_color)
|
||||
{
|
||||
printf("\e[2K");
|
||||
}
|
||||
|
|
@ -295,16 +274,14 @@ static void loop(
|
|||
printf("%i of %i (%.2f%%): [%i] ",
|
||||
iterations, N, (100.0 * iterations / N), cost);
|
||||
|
||||
print(flags, &simps->data, truthtable), puts("");
|
||||
print(flags, &simps, truthtable), puts("");
|
||||
|
||||
if (!ZDEBUG && flags->print_with_color)
|
||||
if (flags->print_with_color)
|
||||
{
|
||||
printf("\e[1A");
|
||||
}
|
||||
}
|
||||
|
||||
TODO
|
||||
#if 0
|
||||
// consider NOT:
|
||||
if (flags->use_operators.not)
|
||||
{
|
||||
|
|
@ -482,72 +459,17 @@ static void loop(
|
|||
}
|
||||
}
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
// clear progress line, enable terminal autowrap:
|
||||
if (!ZDEBUG && flags->verbose && flags->print_with_color)
|
||||
if (flags->verbose && flags->print_with_color)
|
||||
{
|
||||
printf("\e[2K"), printf("\e[?7h");
|
||||
}
|
||||
|
||||
return simps;
|
||||
}
|
||||
|
||||
struct simplifications calculate_simplifications(
|
||||
const struct cmdln_flags* flags)
|
||||
{
|
||||
zprintf("calculate_simplifications()" "\n");
|
||||
|
||||
struct simplifications simps = {};
|
||||
|
||||
init_simplifications(&simps);
|
||||
|
||||
struct heap todo = new_heap();
|
||||
|
||||
struct sparselist done = new_sparselist();
|
||||
|
||||
heap_append(&todo, &simps, W, 0), simps.data[W].kind = ek_W;
|
||||
heap_append(&todo, &simps, X, 0), simps.data[X].kind = ek_X;
|
||||
heap_append(&todo, &simps, Y, 0), simps.data[Y].kind = ek_Y;
|
||||
heap_append(&todo, &simps, Z, 0), simps.data[Z].kind = ek_Z;
|
||||
|
||||
heap_append(&todo, &simps, 0, 1), simps.data[0].kind = ek_0;
|
||||
heap_append(&todo, &simps, M, 1), simps.data[M].kind = ek_1;
|
||||
|
||||
loop(flags, &simps, &todo, &done);
|
||||
|
||||
TODO;
|
||||
}
|
||||
|
||||
struct simplifications calculate_simplifications_with_extra_variable(
|
||||
const struct cmdln_flags* flags,
|
||||
uint16_t A)
|
||||
{
|
||||
zprintf("calculate_simplifications_with_extra_variable()" "\n");
|
||||
|
||||
#if 0
|
||||
|
||||
if (have_extra_variable && todo.reverse[A] == -1)
|
||||
{
|
||||
append(A, 0), simps.data[A].kind = ek_A;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
TODO;
|
||||
}
|
||||
|
||||
void update_simplifications(
|
||||
struct simplifications* simps,
|
||||
const struct cmdln_flags* flags,
|
||||
uint16_t starting_with)
|
||||
{
|
||||
zprintf("update_simplifications()" "\n");
|
||||
|
||||
TODO;
|
||||
}
|
||||
|
||||
#if 0
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
@ -562,5 +484,3 @@ void update_simplifications(
|
|||
|
||||
|
||||
|
||||
|
||||
#endif
|
||||
|
|
|
|||
15
debug.h
15
debug.h
|
|
@ -1,15 +1,20 @@
|
|||
|
||||
#ifndef ZDEBUG
|
||||
#define ZDEBUG 1
|
||||
#ifdef DEBUG_BUILD
|
||||
extern int debug_depth;
|
||||
#endif
|
||||
|
||||
#if ZDEBUG
|
||||
#define zprintf(fmt, ...) \
|
||||
printf(fmt, ## __VA_ARGS__);
|
||||
#ifdef DEBUG_BUILD
|
||||
#define zprintf(fmt, ...) printf("%*s" fmt, debug_depth, "", ## __VA_ARGS__);
|
||||
#else
|
||||
#define zprintf(...);
|
||||
#endif
|
||||
|
||||
#define ENTER \
|
||||
{ zprintf("%s():" "\n", __PRETTY_FUNCTION__); debug_depth++; }
|
||||
|
||||
#define EXIT \
|
||||
{ zprintf("return" "\n"); debug_depth--; }
|
||||
|
||||
#define TODO \
|
||||
assert(!"TODO");
|
||||
|
||||
|
|
|
|||
|
|
@ -83,16 +83,20 @@ static struct path { char data[PATH_MAX]; } get_path(
|
|||
return path;
|
||||
}
|
||||
|
||||
void get_cached_simplifications(const struct cmdln_flags* flags)
|
||||
struct simplifications* get_cached_simplifications(const struct cmdln_flags* flags)
|
||||
{
|
||||
zprintf("get_cached_simplifications()" "\n");
|
||||
ENTER;
|
||||
|
||||
struct path path = get_path(flags);
|
||||
|
||||
zprintf("path.data = %s\n", path.data);
|
||||
|
||||
int fd = -1;
|
||||
|
||||
bool rebuild = flags->force_rebuild;
|
||||
|
||||
struct simplifications* simps;
|
||||
|
||||
if (!rebuild)
|
||||
{
|
||||
fd = open(path.data, O_RDONLY);
|
||||
|
|
@ -131,6 +135,7 @@ void get_cached_simplifications(const struct cmdln_flags* flags)
|
|||
|
||||
if (rebuild)
|
||||
{
|
||||
#ifndef DEBUG_BUILD
|
||||
if (!flags->quiet)
|
||||
{
|
||||
puts(""
|
||||
|
|
@ -152,8 +157,9 @@ void get_cached_simplifications(const struct cmdln_flags* flags)
|
|||
puts("Any input to start:"), getchar();
|
||||
puts("Started.");
|
||||
}
|
||||
#endif
|
||||
|
||||
fd = open("/tmp/", O_RDWR | O_TMPFILE, 0664);
|
||||
fd = open(".simplifier-cache-temp.bin", O_TRUNC | O_CREAT | O_RDWR, 0664);
|
||||
|
||||
if (fd < 0)
|
||||
{
|
||||
|
|
@ -161,8 +167,30 @@ void get_cached_simplifications(const struct cmdln_flags* flags)
|
|||
exit(1);
|
||||
}
|
||||
|
||||
struct simplifications simps = calculate_simplifications(flags);
|
||||
if (ftruncate(fd, sizeof(*simps)) < 0)
|
||||
{
|
||||
TODO;
|
||||
}
|
||||
|
||||
void* ptr = mmap(
|
||||
/* addr: */ NULL,
|
||||
/* len: */ sizeof(*simps),
|
||||
/* prot: */ PROT_WRITE | PROT_READ,
|
||||
/* flags: */ MAP_PRIVATE,
|
||||
/* fd: */ fd,
|
||||
/* offset: */ 0);
|
||||
|
||||
if (ptr == MAP_FAILED)
|
||||
{
|
||||
TODO;
|
||||
}
|
||||
|
||||
simps = ptr;
|
||||
|
||||
simps->initial = calculate_simplifications(flags);
|
||||
|
||||
TODO;
|
||||
#if 0
|
||||
TODO;
|
||||
#if 0
|
||||
if (flags->use_operators.assignment)
|
||||
|
|
@ -228,8 +256,11 @@ void get_cached_simplifications(const struct cmdln_flags* flags)
|
|||
|
||||
}
|
||||
#endif
|
||||
#endif
|
||||
}
|
||||
|
||||
TODO;
|
||||
#if 0
|
||||
TODO;
|
||||
#if 0
|
||||
assert(fd > 0);
|
||||
|
|
@ -238,6 +269,9 @@ void get_cached_simplifications(const struct cmdln_flags* flags)
|
|||
|
||||
return retval;
|
||||
#endif
|
||||
#endif
|
||||
|
||||
return simps;
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -3,5 +3,5 @@
|
|||
|
||||
struct cmdln_flags;
|
||||
|
||||
void get_cached_simplifications(const struct cmdln_flags* flags);
|
||||
struct simplifications* get_cached_simplifications(const struct cmdln_flags* flags);
|
||||
|
||||
|
|
|
|||
2
main.c
2
main.c
|
|
@ -19,6 +19,8 @@
|
|||
|
||||
int main(int argc, char* const* argv)
|
||||
{
|
||||
ENTER;
|
||||
|
||||
struct cmdln_flags flags = parse_args(argc, argv);
|
||||
|
||||
get_cached_simplifications(&flags);
|
||||
|
|
|
|||
2
makefile
2
makefile
|
|
@ -14,7 +14,7 @@ default: ${prefix}/bsimp
|
|||
%/:
|
||||
@mkdir -p $@
|
||||
|
||||
srcs += calculate_simplifications.c cmdln.c evaluate.c
|
||||
srcs += calculate_simplifications.c cmdln.c evaluate.c debug.c
|
||||
srcs += get_cached_simplifications.c main.c print.c
|
||||
|
||||
${prefix}/%.o ${prefix}/%.d: %.c ${optionset} | ${prefix}/%/
|
||||
|
|
|
|||
|
|
@ -8,7 +8,9 @@
|
|||
|
||||
struct simplifications
|
||||
{
|
||||
struct expr data[N];
|
||||
struct row {
|
||||
struct expr data[N];
|
||||
} initial, with_variables[N];
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Reference in a new issue