Zander/4-variable-simplifier
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

...

Browse source
This commit is contained in:
Zander Thannhauser 2025-06-27 14:37:09 -05:00
parent 6f326a9bcb
commit 7f012a32c8
13 changed files with 476 additions and 261 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
buildtypes/debug.txt
View file

@ -1,8 +1,12 @@
-g
-D _GNU_SOURCE
-D ZDEBUG=1
-D DEBUG_BUILD
-I .
-Werror -Wall -Wextra -Wstrict-prototypes -Wfatal-errors
@ -10,4 +14,5 @@
-Wno-unused
-lreadline
-lexplain

2
buildtypes/release.txt
View file

@ -5,6 +5,8 @@
-I .
-O3
-Werror -Wall -Wextra -Wstrict-prototypes -Wfatal-errors
-lreadline

488
calculate_simplifications.c
View file

@ -11,112 +11,120 @@
#include "calculate_simplifications.h"
struct simplifications calculate_simplifications(
const struct cmdln_flags* flags)
static void init_simplifications(
struct simplifications* simps)
{
struct simplifications simps = {};
// init 'simps.data':
for (int i = 0; i < N; i++)
{
for (int i = 0; i < N; i++)
{
simps.data[i].kind = ek_unreachable;
simps.data[i].cost = INT_MAX;
}
simps->data[i].kind = ek_unreachable;
simps->data[i].cost = INT_MAX;
}
}
struct heap
{
uint16_t data[N];
int n;
// 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++)
{
todo.reverse[i] = -1;
}
// heap of truthtables; key = cost
struct {
uint16_t data[N];
int n;
// truthtable -> index in 'todo'
int reverse[N];
} todo;
// init 'todo':
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:
{
todo.n = 0;
for (int i = 0; i < N; i++)
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.reverse[i] = -1;
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 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)
{
todo->data[index] = todo->data[new_index];
todo->reverse[todo->data[new_index]] = index;
index = new_index;
}
uint16_t pop(void)
{
assert(todo.n > 0);
uint16_t retval = todo.data[0];
todo.reverse[retval] = -1;
uint16_t moving = todo.data[todo.n-- - 1];
int cost = simps.data[moving].cost;
int index = 0;
again:
{
int left = index * 2 + 1;
int right = index * 2 + 2;
uint16_t smallest = moving;
if (left < todo.n && simps.data[todo.data[left]].cost < cost)
smallest = todo.data[left];
if (right < todo.n && simps.data[todo.data[right]].cost < simps.data[smallest].cost)
smallest = todo.data[right];
if (smallest == moving)
{
todo.data[index] = moving;
todo.reverse[moving] = index;
}
else
{
int new = todo.reverse[smallest];
todo.data[index] = smallest;
todo.reverse[smallest] = index;
index = new;
goto again;
}
}
return retval;
}
void append(uint16_t truthtable, int cost)
{
assert(todo.reverse[truthtable] == -1);
int index = todo.n++, new_index;
while (index > 0 && simps.data[todo.data[new_index = (index - 1) / 2]].cost > cost)
{
todo.data[index] = todo.data[new_index];
todo.reverse[todo.data[new_index]] = index;
index = new_index;
}
todo.data[index] = truthtable;
todo.reverse[truthtable] = index;
simps.data[truthtable].cost = cost;
}
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);
@ -139,134 +147,147 @@ struct simplifications calculate_simplifications(
simps.data[truthtable].cost = cost;
}
#endif
// create a list of the "done" truthtables
struct sparselist
{
int headtails[N], next[N], head;
// create a list of the "done" truthtables
struct {
int headtails[N], next[N], head;
// for debugging:
#if ZDEBUG
bool in[N];
#endif
} done = {};
// for debugging:
#if ZDEBUG
bool in[N];
#endif
};
struct sparselist new_sparselist(void)
{
struct sparselist done = {};
// init 'done':
done.head = -1;
for (int i = 0; i < N; i++)
{
done.head = -1;
done.headtails[i] = -1;
for (int i = 0; i < N; i++)
#if ZDEBUG
done.in[i] = false;
#endif
}
return done;
}
void sparselist_insert(struct sparselist* this, int index)
{
TODO;
#if 0
#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)
{
done.headtails[i] = -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
done.in[i] = false;
assert(done.in[tail]);
#endif
done.next[index] = tail;
}
else
{
int bottomhalfhead = done.headtails[prevtail + 1];
assert(bottomhalfhead != -1);
done.next[index] = bottomhalfhead;
}
}
void insert(int index)
else
{
#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
done.next[index] = -1;
}
append(W, 0), simps.data[W].kind = ek_W;
append(X, 0), simps.data[X].kind = ek_X;
append(Y, 0), simps.data[Y].kind = ek_Y;
append(Z, 0), simps.data[Z].kind = ek_Z;
append(0, 1), simps.data[0].kind = ek_0;
append(M, 1), simps.data[M].kind = ek_1;
#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");
// disable terminal autowrap:
if (flags->verbose && flags->print_with_color)
if (!ZDEBUG && 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 = pop();
uint16_t truthtable = heap_pop(todo, simps);
insert(truthtable);
if (!done)
{
sparselist_insert(done, truthtable);
}
int cost = simps.data[truthtable].cost;
int cost = simps->data[truthtable].cost;
if (flags->verbose)
{
if (flags->print_with_color)
if (!ZDEBUG && flags->print_with_color)
{
printf("\e[2K");
}
@ -274,14 +295,16 @@ struct simplifications calculate_simplifications(
printf("%i of %i (%.2f%%): [%i] ",
iterations, N, (100.0 * iterations / N), cost);
print(flags, &simps.data, truthtable), puts("");
print(flags, &simps->data, truthtable), puts("");
if (flags->print_with_color)
if (!ZDEBUG && flags->print_with_color)
{
printf("\e[1A");
}
}
TODO
#if 0
// consider NOT:
if (flags->use_operators.not)
{
@ -459,17 +482,72 @@ struct simplifications calculate_simplifications(
}
}
}
#endif
}
// clear progress line, enable terminal autowrap:
if (flags->verbose && flags->print_with_color)
if (!ZDEBUG && 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
@ -484,3 +562,5 @@ struct simplifications calculate_simplifications(
#endif

13
calculate_simplifications.h
View file

@ -1,8 +1,19 @@
#include "simplifications.h"
#include <expr.h>
#include <simplifications.h>
struct cmdln_flags;
struct simplifications calculate_simplifications(
const struct cmdln_flags* flags);
struct simplifications calculate_simplifications_with_extra_variable(
const struct cmdln_flags* flags,
uint16_t A);
void update_simplifications(
struct simplifications* simps,
const struct cmdln_flags* flags,
uint16_t starting_with);

9
expr.h
View file

@ -14,6 +14,9 @@ enum ekind
ek_X,
ek_Y,
ek_Z,
// very special:
ek_A,
ek_not,
ek_or,
@ -34,6 +37,12 @@ enum ekind
ek_gte,
ek_ternary,
// also very special.
// 'left' is the variable's truthtable
// to print the requested truthtable
// look a the relavent lookup.
ek_assignment,
};
struct expr

26
flake.lock
View file

@ -36,15 +36,32 @@
},
"nixpkgs": {
"locked": {
"lastModified": 1749664469,
"narHash": "sha256-Ar3r6cmQVKVoEy/TWAKq8WuGqZibRjMt5oZRvkn+2Bk=",
"lastModified": 1750838302,
"narHash": "sha256-aVkL3/yu50oQzi2YuKo0ceiCypVZpZXYd2P2p1FMJM4=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "3fa008da69980bd61324ad9e3a825022f0b736f1",
"rev": "7284e2decc982b81a296ab35aa46e804baaa1cfe",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-25.05",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-libexplain": {
"locked": {
"lastModified": 1750646418,
"narHash": "sha256-4UAN+W0Lp4xnUiHYXUXAPX18t+bn6c4Btry2RqM9JHY=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "1f426f65ac4e6bf808923eb6f8b8c2bfba3d18c5",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-24.11",
"repo": "nixpkgs",
"type": "github"
}
@ -53,7 +70,8 @@
"inputs": {
"flake-compat": "flake-compat",
"flake-utils": "flake-utils",
"nixpkgs": "nixpkgs"
"nixpkgs": "nixpkgs",
"nixpkgs-libexplain": "nixpkgs-libexplain"
}
},
"systems": {

16
flake.nix
View file

@ -4,7 +4,9 @@
{
description = "description";
inputs.nixpkgs = { url = "github:NixOS/nixpkgs"; };
inputs.nixpkgs = { url = "github:NixOS/nixpkgs?ref=nixos-25.05"; };
inputs.nixpkgs-libexplain = { url = "github:NixOS/nixpkgs?ref=nixos-24.11"; };
inputs.flake-utils.url = "github:numtide/flake-utils";
@ -13,14 +15,17 @@
flake = false;
};
outputs = { self, nixpkgs, flake-utils, ... }:
outputs = { self, nixpkgs, nixpkgs-libexplain, flake-utils, ... }:
flake-utils.lib.eachDefaultSystem (system:
let pkgs = import nixpkgs {
inherit system;
config.allowUnfree = true;
};
in {
}; pkgs-libexplain = import nixpkgs-libexplain {
inherit system;
config.allowUnfree = true;
}; in {
devShells.default =
pkgs.mkShell {
buildInputs = with pkgs; [
@ -34,6 +39,9 @@
man-pages
man-pages-posix
# let's try this:
pkgs-libexplain.explain.dev
# for my sake:
gedit
];

143
get_cached_simplifications.c
View file

@ -10,6 +10,13 @@
#include <limits.h>
#include <assert.h>
#include <libexplain/gcc_attributes.h>
#include <libexplain/large_file_support.h>
#include <libexplain/mmap.h>
#include <sys/mman.h>
#include <defines.h>
#include <debug.h>
@ -76,31 +83,49 @@ static struct path { char data[PATH_MAX]; } get_path(
return path;
}
struct expr (*get_cached_simplifications(const struct cmdln_flags* flags))[N]
void get_cached_simplifications(const struct cmdln_flags* flags)
{
zprintf("get_cached_simplifications()" "\n");
struct path path = get_path(flags);
int fd = -1;
bool rebuild = flags->force_rebuild;
struct expr (*retval)[N];
if (!rebuild)
{
fd = open(path.data, O_RDONLY);
if (fd < 0)
if (fd > 0)
{
if (errno == ENOENT)
{
rebuild = true;
}
else
TODO;
#if 0
retval = malloc(length);
if (!retval)
{
TODO;
exit(1);
}
ssize_t rretval = read(fd, retval, length);
if (rretval < 0 || (size_t) rretval < length)
{
printf("rretval = %li" "\n", rretval);
TODO;
}
#endif
}
else if (errno == ENOENT)
{
rebuild = true;
}
else
{
TODO;
exit(1);
}
}
@ -128,14 +153,7 @@ struct expr (*get_cached_simplifications(const struct cmdln_flags* flags))[N]
puts("Started.");
}
struct simplifications simps0 = calculate_simplifications(flags);
if (flags->use_operators.assignment)
{
TODO;
}
fd = open(path.data, O_RDWR | O_TRUNC | O_CREAT, 0664);
fd = open("/tmp/", O_RDWR | O_TMPFILE, 0664);
if (fd < 0)
{
@ -143,39 +161,83 @@ struct expr (*get_cached_simplifications(const struct cmdln_flags* flags))[N]
exit(1);
}
if (write(fd, &simps0, sizeof(simps0)) < (ssize_t) sizeof(simps0))
{
printf("%s: write() to cache failed: %m\n", flags->argv0);
exit(1);
}
struct simplifications simps = calculate_simplifications(flags);
TODO;
#if 0
if (flags->use_operators.assignment)
{
for (int a = 0; a < N; a++)
{
if (simps0.data[a].cost < INT_MAX)
{
zprintf("what if a = 0b%016b?" "\n", a);
TODO;
#if 0
struct simplifications vsimps = \
calculate_simplifications(flags,
/* have extra variable? */ true,
/* extra variable value: */ a);
for (int t = 0; t < N; t++)
{
if (vsimps.data[t].cost < INT_MAX)
{
int total_cost =
simps.data[a].cost + 1 + vsimps.data[t].cost;
if (total_cost < simps.data[t].cost)
{
simps.data[t].kind = ek_assignment;
simps.data[t].left = a;
simps.data[t].right = t;
simps.data[t].cost = total_cost;
TODO;
}
}
}
if (pwrite(
/* fd: */ fd,
/* addr: */ &vsimps,
/* len: */ sizeof(vsimps),
/* offset: */ (1 + a) * sizeof(struct simplifications))
< (ssize_t) sizeof(vsimps))
{
printf("%s: write() to cache failed: %m\n", flags->argv0);
exit(1);
}
#endif
}
}
// since we've lowered costs of simplifications, other expressions
// will want to update their expressions and costs.
TODO;
if (write(fd, &simps0, sizeof(simps0)) < (ssize_t) sizeof(simps0))
{
printf("%s: write() to cache failed: %m\n", flags->argv0);
exit(1);
}
}
#endif
}
TODO;
#if 0
assert(fd > 0);
void* ptr = mmap(
/* addr: */ NULL,
/* len: */ flags->use_operators.assignment
? sizeof(struct simplifications) * ((1 << 16) + 1)
: sizeof(struct simplifications),
/* prot: */ PROT_READ,
/* flags: */ MAP_PRIVATE,
/* fildes: */ fd,
/* off: */ 0);
if (ptr == (void*) -1)
{
TODO;
}
close(fd);
return ptr;
return retval;
#endif
}
@ -192,3 +254,4 @@ struct expr (*get_cached_simplifications(const struct cmdln_flags* flags))[N]

4
get_cached_simplifications.h
View file

@ -1,7 +1,7 @@
#include "simplifications.h"
// #include <expr.h>
struct cmdln_flags;
struct expr (*get_cached_simplifications(const struct cmdln_flags* flags))[N];
void get_cached_simplifications(const struct cmdln_flags* flags);

14
main.c
View file

@ -21,24 +21,26 @@ int main(int argc, char* const* argv)
{
struct cmdln_flags flags = parse_args(argc, argv);
get_cached_simplifications(&flags);
TODO;
#if 0
struct expr (*simps)[N] = get_cached_simplifications(&flags);
if (flags.print_all_and_quit)
{
TODO;
#if 0
for (int i = 0; i < N; i++)
{
int cost = simps.data[i].cost;
int cost = simps[0][i].cost;
if (cost != INT_MAX)
{
printf("0b%016b: [%2i]: ", i, cost);
print(&flags, &simps, i);
print(&flags, simps, i);
puts("");
}
}
#endif
}
else if (flags.print_max_operators_needed_and_quit)
{
@ -110,6 +112,8 @@ int main(int argc, char* const* argv)
#endif
}
#endif
return 0;
}

3
makefile
View file

@ -33,7 +33,8 @@ run: ${prefix}/bsimp
$< $(args)
valrun: ${prefix}/bsimp
valgrind --exit-on-first-error=yes --error-exitcode=1 -- $< ${args}
valgrind --max-stackframe=2031768 \
--exit-on-first-error=yes --error-exitcode=1 -- $< ${args}
PREFIX ?= ${HOME}

13
print.c
View file

@ -81,6 +81,12 @@ static void helper(
break;
}
case ek_A:
{
printf(print_with_color ? VARIABLE_ESCAPE "a" RESET_ESCAPE : "a");
break;
}
case ek_not:
{
const char* start = print_with_color ? operator_colors[depth % 10] : "";
@ -157,6 +163,13 @@ static void helper(
break;
}
case ek_assignment:
{
TODO;
break;
};
}
}

1
simplifications.h
View file

@ -12,3 +12,4 @@ struct simplifications
};
#endif