commit 2add7a474e84b6c4f79fff589460e99ac2a1332e Author: Zander Thannhauser Date: Fri Mar 7 09:45:00 2025 -0600 first commit diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e69de29 diff --git a/automata.cpp b/automata.cpp new file mode 100644 index 0000000..e09a264 --- /dev/null +++ b/automata.cpp @@ -0,0 +1,555 @@ + +#include +#include +#include + +#include +#include +#include +#include +#include +#include +#include + +struct automata* automata::new_variable( + int depth, + bool verbose, + unsigned variable_index, + bool value, + unsigned number_of_variables) +{ + assert(variable_index < number_of_variables); + + if (verbose) + { + printf("%*s" "variable(index = %u, value = %s):\n", + depth++, "", variable_index, value ? "true" : "false"); + } + + size_t total_number_of_states = 0; + + struct automata* start = new automata(); + struct automata* moving = start; + + total_number_of_states++; + + for (unsigned i = 0; i < number_of_variables; i++) + { + struct automata* newmoving = new automata(); + + total_number_of_states++; + + if (i == variable_index) + { + moving->on[value] = newmoving; + } + else + { + moving->on[0] = newmoving; + moving->on[1] = newmoving; + } + + moving = newmoving; + } + + moving->is_accepting = true; + + if (verbose) + { + printf("%*s" "returned automata with %lu states.\n", + depth, "", total_number_of_states); + } + + return start; +} + +void automata::dump(struct automata* start, const char* fmt, ...) +{ + char path[PATH_MAX]; + + static size_t dump_id = 0; + + snprintf(path, PATH_MAX, "/tmp/%05lu.dot", dump_id++); + + FILE* stream = fopen(path, "w"); + + fprintf(stream, "" + "digraph {" "\n" + "\t" "rankdir = LR;" "\n" + "\t" + "\t" "node [" "\n" + "\t" "\t" "shape = circle" "\n" + "\t" "\t" "label = \"\"" "\n" + "\t" "];" "\n" + "\t" "\n" + ""); + + va_list va; + va_start(va, fmt); + + vfprintf(stream, fmt, va); + + va_end(va); + + quack todo; + + set queued; + + if (queued.add(start)) + { + todo.append(start); + } + + while (todo.n) + { + automata* state = todo.pop(); + + if (state->is_accepting) + { + fprintf(stream, "\"%p\" [ shape = doublecircle ];\n", state); + } + + for (int on = 0; on < 2; on++) + { + automata* to = state->on[on]; + + if (to) + { + fprintf(stream, "\"%p\" -> \"%p\" [label = \"%i\"];\n", state, to, on); + + if (queued.add(to)) + { + todo.append(to); + } + } + } + } + + fprintf(stream, "" + "}" "\n" + ""); + + fclose(stream); +} + +struct automata* automata::complement( + const struct automata* original_start) +{ + dict mapping; + + struct automata* start = new automata(); + + struct automata* phi = NULL; + + quack todo; + + todo.append(mapping.add(original_start, start)); + + while (todo.n) + { + auto [original, state] = *todo.pop(); + + state->is_accepting = !original->is_accepting; + + for (int value = 0; value < 2; value++) + { + if (const automata* to = original->on[value]) + { + if (mapping.has(to)) + { + state->on[value] = mapping[to]; + } + else + { + automata* state_to = new automata(); + + state->on[value] = state_to; + + todo.append(mapping.add(to, state_to)); + } + } + else + { + if (!phi) + { + phi = new automata(); + + phi->is_accepting = true; + + phi->on[0] = phi; + phi->on[1] = phi; + } + + state->on[value] = phi; + } + } + } + + return start; +} + +struct automata* automata::union_( + int depth, + bool verbose, + const struct automata* left_start, + const struct automata* right_start) +{ + if (verbose) + { + printf("%*s" "union():\n", depth++, ""); + } + + dict, automata*> mapping; + + size_t total_number_of_states = 0; + + struct automata* start = new automata(); + + total_number_of_states++; + + quack todo; + + // initial state: + todo.append(mapping.add(tuple(left_start, right_start), start)); + + while (todo.n) + { + auto keyvalue = todo.pop(); + + auto [left, right] = keyvalue->key; + + automata* state = keyvalue->value; + + state->is_accepting = false + || (left && left->is_accepting) + || (right && right->is_accepting); + + for (int value = 0; value < 2; value++) + { + const automata* left_to = left ? left->on[value] : NULL; + const automata* right_to = right ? right->on[value] : NULL; + + if (left_to || right_to) + { + if (mapping.has(tuple(left_to, right_to))) + { + state->on[value] = mapping[tuple(left_to, right_to)]; + } + else + { + automata* state_to = new automata(); + + total_number_of_states++; + + state->on[value] = state_to; + + todo.append(mapping.add(tuple(left_to, right_to), state_to)); + } + } + } + } + + if (verbose) + { + printf("%*s" "returned automata with %lu states" "\n", + depth, "", total_number_of_states); + } + + return start; +} + +struct automata* automata::intersect( + int depth, + bool verbose, + const struct automata* left_start, + const struct automata* right_start) +{ + if (verbose) + { + printf("%*s" "intersect():\n", depth++, ""); + } + + dict, automata*> mapping; + + size_t total_number_of_states = 0; + + struct automata* start = new automata(); + + total_number_of_states++; + + quack todo; + + // initial state: + todo.append(mapping.add(tuple(left_start, right_start), start)); + + while (todo.n) + { + auto keyvalue = todo.pop(); + + auto [left, right] = keyvalue->key; + + automata* state = keyvalue->value; + + state->is_accepting = left->is_accepting && right->is_accepting; + + for (int value = 0; value < 2; value++) + { + const automata* left_to = left->on[value]; + const automata* right_to = right->on[value]; + + if (left_to && right_to) + { + if (mapping.has(tuple(left_to, right_to))) + { + state->on[value] = mapping[tuple(left_to, right_to)]; + } + else + { + automata* state_to = new automata(); + + total_number_of_states++; + + state->on[value] = state_to; + + todo.append(mapping.add(tuple(left_to, right_to), state_to)); + } + } + } + } + + if (verbose) + { + printf("%*s" "returned automata with %lu states" "\n", + depth, "", total_number_of_states); + } + + return start; +} + +struct automata* automata::simplify( + int depth, + bool verbose, + const struct automata* original_start) +{ + if (verbose) + { + printf("%*s" "simplify():\n", depth++, ""); + } + + set universe; + { + quack todo; + + universe.add(original_start); + + todo.append(original_start); + + while (todo.n) + { + const automata* state = todo.pop(); + + for (int val = 0; val < 2; val++) + { + auto to = state->on[val]; + + if (to && universe.add(to)) + { + todo.append(to); + } + } + } + } + + typedef tuple pair_t; + + dict> dependent_of; + + heap> todo; + + for (const automata* a: universe) + { + for (const automata* b: universe) + { + if (a < b) + { + bool are_different = false; + + if (a->is_accepting != b->is_accepting) + { + are_different = true; + } + else for (int val = 0; !are_different && val < 2; val++) + { + const automata* a_to = a->on[val]; + const automata* b_to = b->on[val]; + + if (!a_to != !b_to) + { + are_different = true; + } + else if (a_to && b_to) + { + if (a_to > b_to) + { + const automata* swap = b_to; + b_to = a_to, a_to = swap; + } + + if (!dependent_of.has(tuple(a_to, b_to))) + { + dependent_of.add(tuple(a_to, b_to), set()); + } + + dependent_of[tuple(a_to, b_to)].add(tuple(a, b)); + } + } + + if (are_different) + { + todo.push(tuple(0U, tuple(a, b))); + } + } + } + } + + dict> same_as; + + for (const automata* state: universe) + { + same_as.add(state, set(universe)); + } + + while (todo.n) + { + auto [hopcount, pair] = todo.pop(); + + auto [a, b] = pair; + + if (same_as[a].discard(b) && same_as[b].discard(a)) + { + if (dependent_of.has(pair)) + { + for (pair_t dep_on: dependent_of[pair]) + { + todo.push(tuple(hopcount + 1, dep_on)); + } + } + } + } + + size_t total_number_of_states = 1; + + struct automata* new_start = new automata(); + { + dict mapping; + + quack todo; + + // initial state: + { + const automata* cloneme = same_as[original_start].min(); + + todo.append(mapping.add(cloneme, new_start)); + } + + while (todo.n) + { + auto [old, state] = *todo.pop(); + + state->is_accepting = old->is_accepting; + + for (int val = 0; val < 2; val++) + { + if (const automata* to = old->on[val]) + { + const automata* cloneme = same_as[to].min(); + + if (mapping.has(cloneme)) + { + state->on[val] = mapping[cloneme]; + } + else + { + automata* substate = new automata(); + + total_number_of_states++; + + state->on[val] = substate; + + todo.append(mapping.add(cloneme, substate)); + } + } + } + } + } + + if (verbose) + { + printf("%*s" "returned automata with %lu states" "\n", + depth, "", total_number_of_states); + } + + return new_start; +} + +void automata::free(struct automata* start) +{ + set queued; + + quack todo; + + queued.add(start); + + todo.append(start); + + while (todo.n) + { + struct automata* state = todo.pop(); + + for (int val = 0; val < 2; val++) + { + if (struct automata* to = state->on[val]) + { + if (queued.add(to)) + { + todo.append(to); + } + } + } + + delete state; + } +} + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/automata.hpp b/automata.hpp new file mode 100644 index 0000000..fcc0390 --- /dev/null +++ b/automata.hpp @@ -0,0 +1,49 @@ + +#ifndef STRUCT_AUTOMATA +#define STRUCT_AUTOMATA + +#include + +struct automata +{ + public: + bool is_accepting = false; + + struct automata *on[2] = {NULL, NULL}; + + public: + static struct automata* new_variable( + int depth, + bool verbose, + unsigned variable_index, + bool value, + unsigned number_of_variables); + + static struct automata* complement( + const struct automata* original); + + static struct automata* union_( + int depth, + bool verbose, + const struct automata* left, + const struct automata* right); + + static struct automata* intersect( + int depth, + bool verbose, + const struct automata* left, + const struct automata* right); + + static struct automata* simplify( + int depth, + bool verbose, + const struct automata* original); + + static void dump(struct automata*, const char* fmt, ...); + + static void free(struct automata*); +}; + +#endif + + diff --git a/avl.hpp b/avl.hpp new file mode 100644 index 0000000..92d6bfb --- /dev/null +++ b/avl.hpp @@ -0,0 +1,625 @@ + +#ifndef CLASS_AVL_TREE_T +#define CLASS_AVL_TREE_T + +#include +#include + +/* We need either depths, counts or both (the latter being the default) */ +#if !defined(AVL_DEPTH) && !defined(AVL_COUNT) +#define AVL_DEPTH +#define AVL_COUNT +#endif + +#ifdef AVL_COUNT +#define NODE_COUNT(n) ((n) ? (n)->count : 0) +#define L_COUNT(n) (NODE_COUNT((n)->left)) +#define R_COUNT(n) (NODE_COUNT((n)->right)) +#define CALC_COUNT(n) (L_COUNT(n) + R_COUNT(n) + 1) +#endif + +#ifdef AVL_DEPTH +#define NODE_DEPTH(n) ((n) ? (n)->depth : 0) +#define L_DEPTH(n) (NODE_DEPTH((n)->left)) +#define R_DEPTH(n) (NODE_DEPTH((n)->right)) +#define CALC_DEPTH(n) ((L_DEPTH(n) > R_DEPTH(n) ? L_DEPTH(n) : R_DEPTH(n)) + 1) +#endif + +template < + typename I> class avl_tree_t +{ + struct avl_node_t + { + struct avl_node_t *next; + struct avl_node_t *prev; + struct avl_node_t *parent; + struct avl_node_t *left; + struct avl_node_t *right; + + I item; + + #ifdef AVL_COUNT + unsigned int count; + #endif + + #ifdef AVL_DEPTH + int depth; + #endif + + avl_node_t(I _item): item(_item) + { + ; + } + + void clear() + { + this->left = this->right = NULL; + + #ifdef AVL_COUNT + this->count = 1; + #endif + + #ifdef AVL_DEPTH + this->depth = 1; + #endif + } + }; + + public: + struct avl_node_t *top = NULL; + struct avl_node_t *head = NULL; + struct avl_node_t *tail = NULL; + + private: + #ifndef AVL_DEPTH + /* Also known as ffs() (from BSD) */ + static int lg(unsigned int u) + { + int r = 1; + if (!u) return 0; + if (u & 0xffff0000) { u >>= 16; r += 16; } + if (u & 0x0000ff00) { u >>= 8; r += 8; } + if (u & 0x000000f0) { u >>= 4; r += 4; } + if (u & 0x0000000c) { u >>= 2; r += 2; } + if (u & 0x00000002) r++; + return r; + } + #endif + + static int check_balance(avl_node_t *avlnode) + { + #ifdef AVL_DEPTH + int d = R_DEPTH(avlnode) - L_DEPTH(avlnode); + return d < -1 ? -1 : d > 1 ? 1 : 0; + #else + /* int d; + * d = lg(R_COUNT(avlnode)) - lg(L_COUNT(avlnode)); + * d = d<-1?-1:d>1?1:0; + */ + #ifdef AVL_COUNT + int pl, r; + + pl = lg(L_COUNT(avlnode)); + r = R_COUNT(avlnode); + + if(r>>pl+1) + return 1; + if(pl<2 || r>>pl-2) + return 0; + return -1; + #else + #error No balancing possible. + #endif + #endif + } + + int search_closest( + const I& item, + avl_node_t **avlnode) const + { + avl_node_t *node; + + if (!avlnode) + { + avlnode = &node; + } + + node = this->top; + + if (!node) + { + return *avlnode = NULL, 0; + } + + for (;;) + { + auto c = (item <=> node->item); + + if (c < 0) { + if (node->left) + node = node->left; + else + return *avlnode = node, -1; + } else if (c > 0) { + if (node->right) + node = node->right; + else + return *avlnode = node, 1; + } else { + return *avlnode = node, 0; + } + } + } + + struct avl_node_t *insert_top(avl_node_t *newnode) + { + newnode->clear(); + + newnode->prev = newnode->next = newnode->parent = NULL; + + this->head = this->tail = this->top = newnode; + + return newnode; + } + + struct avl_node_t *insert_before(avl_node_t *node, avl_node_t *newnode) + { + if (!node) + { + return this->tail + ? insert_after(this->tail, newnode) + : insert_top(newnode); + } + + if (node->left) + { + return insert_after(node->prev, newnode); + } + + newnode->clear(); + + newnode->next = node; + newnode->parent = node; + + newnode->prev = node->prev; + if (node->prev) + node->prev->next = newnode; + else + this->head = newnode; + node->prev = newnode; + + node->left = newnode; + rebalance(node); + return newnode; + } + + struct avl_node_t *insert_after(avl_node_t *node, avl_node_t *newnode) + { + if (!node) + return this->head + ? insert_before(this->head, newnode) + : insert_top(newnode); + + if (node->right) + return insert_before(node->next, newnode); + + newnode->clear(); + + newnode->prev = node; + newnode->parent = node; + + newnode->next = node->next; + if (node->next) + node->next->prev = newnode; + else + this->tail = newnode; + node->next = newnode; + + node->right = newnode; + + rebalance(node); + + return newnode; + } + + avl_node_t *insert_node(avl_node_t *newnode) + { + avl_node_t *node; + + if (!this->top) + return insert_top(newnode); + + switch (search_closest(newnode->item, &node)) + { + case -1: + return insert_before(node, newnode); + + case 1: + return insert_after(node, newnode); + } + + return NULL; + } + + void rebalance(avl_node_t *avlnode) + { + avl_node_t *child; + avl_node_t *gchild; + avl_node_t *parent; + avl_node_t **superparent; + + parent = avlnode; + + while (avlnode) + { + parent = avlnode->parent; + + superparent = parent + ? avlnode == parent->left + ? &parent->left + : &parent->right + : &this->top; + + switch (check_balance(avlnode)) + { + case -1: + { + child = avlnode->left; + + #ifdef AVL_DEPTH + if (L_DEPTH(child) >= R_DEPTH(child)) { + #else + #ifdef AVL_COUNT + if (L_COUNT(child) >= R_COUNT(child)) { + #else + #error No balancing possible. + #endif + #endif + avlnode->left = child->right; + if (avlnode->left) + avlnode->left->parent = avlnode; + child->right = avlnode; + avlnode->parent = child; + *superparent = child; + child->parent = parent; + #ifdef AVL_COUNT + avlnode->count = CALC_COUNT(avlnode); + child->count = CALC_COUNT(child); + #endif + #ifdef AVL_DEPTH + avlnode->depth = CALC_DEPTH(avlnode); + child->depth = CALC_DEPTH(child); + #endif + } else { + gchild = child->right; + avlnode->left = gchild->right; + if (avlnode->left) + avlnode->left->parent = avlnode; + child->right = gchild->left; + if (child->right) + child->right->parent = child; + gchild->right = avlnode; + if (gchild->right) + gchild->right->parent = gchild; + gchild->left = child; + if (gchild->left) + gchild->left->parent = gchild; + *superparent = gchild; + gchild->parent = parent; + + #ifdef AVL_COUNT + avlnode->count = CALC_COUNT(avlnode); + child->count = CALC_COUNT(child); + gchild->count = CALC_COUNT(gchild); + #endif + + #ifdef AVL_DEPTH + avlnode->depth = CALC_DEPTH(avlnode); + child->depth = CALC_DEPTH(child); + gchild->depth = CALC_DEPTH(gchild); + #endif + } + break; + } + + case 1: + { + child = avlnode->right; + + #ifdef AVL_DEPTH + if (R_DEPTH(child) >= L_DEPTH(child)) { + #else + #ifdef AVL_COUNT + if (R_COUNT(child) >= L_COUNT(child)) { + #else + #error No balancing possible. + #endif + #endif + avlnode->right = child->left; + if (avlnode->right) + avlnode->right->parent = avlnode; + child->left = avlnode; + avlnode->parent = child; + *superparent = child; + child->parent = parent; + #ifdef AVL_COUNT + avlnode->count = CALC_COUNT(avlnode); + child->count = CALC_COUNT(child); + #endif + #ifdef AVL_DEPTH + avlnode->depth = CALC_DEPTH(avlnode); + child->depth = CALC_DEPTH(child); + #endif + } else { + gchild = child->left; + avlnode->right = gchild->left; + if (avlnode->right) + avlnode->right->parent = avlnode; + + child->left = gchild->right; + if (child->left) + child->left->parent = child; + + gchild->left = avlnode; + if (gchild->left) + gchild->left->parent = gchild; + + gchild->right = child; + if (gchild->right) + gchild->right->parent = gchild; + + *superparent = gchild; + gchild->parent = parent; + + #ifdef AVL_COUNT + avlnode->count = CALC_COUNT(avlnode); + child->count = CALC_COUNT(child); + gchild->count = CALC_COUNT(gchild); + #endif + + #ifdef AVL_DEPTH + avlnode->depth = CALC_DEPTH(avlnode); + child->depth = CALC_DEPTH(child); + gchild->depth = CALC_DEPTH(gchild); + #endif + } + + break; + } + + default: + { + #ifdef AVL_COUNT + avlnode->count = CALC_COUNT(avlnode); + #endif + + #ifdef AVL_DEPTH + avlnode->depth = CALC_DEPTH(avlnode); + #endif + + break; + } + } + + avlnode = parent; + } + } + + void unlink_node(avl_node_t *avlnode) + { + avl_node_t *parent; + avl_node_t **superparent; + avl_node_t *subst, *left, *right; + avl_node_t *balnode; + + if (avlnode->prev) + avlnode->prev->next = avlnode->next; + else + this->head = avlnode->next; + + if (avlnode->next) + avlnode->next->prev = avlnode->prev; + else + this->tail = avlnode->prev; + + parent = avlnode->parent; + + superparent = parent + ? avlnode == parent->left + ? &parent->left + : &parent->right + : &this->top; + + left = avlnode->left; + right = avlnode->right; + + if (!left) + { + *superparent = right; + + if (right) + right->parent = parent; + + balnode = parent; + } + else if (!right) + { + *superparent = left; + + left->parent = parent; + + balnode = parent; + } + else + { + subst = avlnode->prev; + + if (subst == left) + { + balnode = subst; + } + else + { + balnode = subst->parent; + + balnode->right = subst->left; + + if (balnode->right) + balnode->right->parent = balnode; + + subst->left = left; + + left->parent = subst; + } + + subst->right = right; + subst->parent = parent; + right->parent = subst; + *superparent = subst; + } + + rebalance(balnode); + } + + void delete_node( + avl_node_t *avlnode) + { + assert(avlnode); + + unlink_node(avlnode); + + delete avlnode; + } + + void free_nodes() + { + for (avl_node_t *node = head, *next; node; node = next) + { + next = node->next; + + delete node; + } + + clear_tree(); + } + + void clear_tree() + { + this->top = this->head = this->tail = NULL; + } + + public: + class iterable + { + private: + struct avl_node_t* node; + + public: + iterable( + struct avl_node_t* _node): + node(_node) + { + ; + } + + I& operator *() + { + assert(node); + + return node->item; + } + + void operator ++() + { + node = node->next; + } + + bool operator != (const iterable& other) + { + return node != other.node; + } + }; + + iterable begin() const + { + return iterable(head); + } + + iterable end() const + { + return iterable(NULL); + } + + public: + avl_tree_t() + { + ; + } + + struct avl_node_t* search(I& item) const + { + avl_node_t *node; + + return search_closest(item, &node) ? NULL : node; + } + + struct avl_node_t* insert(I item) + { + avl_node_t *newnode = new avl_node_t(item); + + if (newnode) + { + if (insert_node(newnode)) + { + return newnode; + } + else + { + delete newnode; + + errno = EEXIST; + } + } + + return NULL; + } + + bool delete_item(I item) + { + auto node = search(item); + + if (node) + return delete_node(node), true; + + return false; + } + + ~avl_tree_t() + { + free_nodes(); + } +}; + + + + + + + + + + + + + + + + + + + + + + + +#endif diff --git a/build-all.py b/build-all.py new file mode 100755 index 0000000..9193288 --- /dev/null +++ b/build-all.py @@ -0,0 +1,59 @@ +#!/usr/bin/env python3 + +import subprocess; +import time; +import atexit; +import os; +import pickle; + +PICKLEFILE = ".build-all.db" + +try: + with open(PICKLEFILE, "rb") as stream: + ftimes = pickle.load(stream); +except: + ftimes = dict(); + +def dumpftimes(): + with open(PICKLEFILE, "wb") as stream: + pickle.dump(ftimes, stream); + +atexit.register(dumpftimes); + +buildtypes = set(); + +for x in os.listdir("buildtypes"): + buildtype = x[:-4]; + + if buildtype not in ftimes: + ftimes[buildtype] = time.time(); + + buildtypes.add(buildtype); + +for buildtype in sorted(buildtypes, key = lambda x: -ftimes[x]): + print("\033[32m" f"$ make buildtype={buildtype}" "\033[0m"); + + result = subprocess.run(["make", f"buildtype={buildtype}"]); + + if result.returncode: + ftimes[buildtype] = time.time(); + print("subcommand failed!"); + exit(1); + + + + + + + + + + + + + + + + + + diff --git a/build_automata.cpp b/build_automata.cpp new file mode 100644 index 0000000..ffc084b --- /dev/null +++ b/build_automata.cpp @@ -0,0 +1,136 @@ + +#include + +#include + +#include + +automata* build_automata( + cmdln_flags& flags, + refcounted p) +{ + struct automata* automata_start = NULL; + + int depth = 0; + + for (const auto& clause: p->clauses) + { + struct automata* clause_start = NULL; + + depth++; + + for (const auto& bundle: clause->bundles) + { + depth++; + + unsigned index = bundle.variable - 1; + + struct automata* variable_start = automata::new_variable( + depth, flags.verbose, + index, bundle.value, + p->number_of_variables); + + if (flags.dump_automata) + { + automata::dump(variable_start, + "label = \"%i (%u) = %s\"", + bundle.variable, index, + bundle.value ? "true" : "false"); + } + + if (clause_start) + { + struct automata* old = clause_start; + + struct automata* unioned = automata::union_( + depth, flags.verbose, old, variable_start); + + if (flags.dump_automata) + { + automata::dump(unioned, "label = \"union\""); + } + + struct automata* simped = automata::simplify( + depth, flags.verbose, unioned); + + if (flags.dump_automata) + { + automata::dump(simped, "label = \"simped\""); + } + + clause_start = simped; + + automata::free(unioned); + + automata::free(variable_start); + + automata::free(old); + } + else + { + clause_start = variable_start; + } + + depth--; + } + + if (automata_start) + { + struct automata* old = automata_start; + + struct automata* intersected = automata::intersect( + depth, flags.verbose, old, clause_start); + + if (flags.dump_automata) + { + automata::dump(intersected, "label = \"intersect\""); + } + + struct automata* simped = automata::simplify( + depth, flags.verbose, intersected); + + if (flags.dump_automata) + { + automata::dump(simped, "label = \"simped\""); + } + + automata_start = simped; + + automata::free(intersected); + + automata::free(clause_start); + + automata::free(old); + } + else + { + automata_start = clause_start; + } + + // if the solution space is empty, no further intersections are going + // to fix it. + if (!automata_start) + { + break; + } + + depth--; + } + + return automata_start; +} + + + + + + + + + + + + + + + diff --git a/build_automata.hpp b/build_automata.hpp new file mode 100644 index 0000000..e6d36aa --- /dev/null +++ b/build_automata.hpp @@ -0,0 +1,11 @@ + +#include + +#include + +#include + +automata* build_automata( + cmdln_flags& flags, + refcounted p); + diff --git a/buildtypes/debug.txt b/buildtypes/debug.txt new file mode 100644 index 0000000..933bfe7 --- /dev/null +++ b/buildtypes/debug.txt @@ -0,0 +1,13 @@ + +-fsanitize=undefined +-fsanitize=address + +-std=c++20 + +-I . + +-D DEBUG_BUILD + +-g + +-Wall -Werror -Wextra -Wfatal-errors diff --git a/buildtypes/release.txt b/buildtypes/release.txt new file mode 100644 index 0000000..8be488c --- /dev/null +++ b/buildtypes/release.txt @@ -0,0 +1,12 @@ + +-O3 + +-std=c++20 + +-I . + +-D TEST_BUILD + +-g + +-Wall -Werror -Wextra -Wfatal-errors diff --git a/buildtypes/test.txt b/buildtypes/test.txt new file mode 100644 index 0000000..a8df973 --- /dev/null +++ b/buildtypes/test.txt @@ -0,0 +1,10 @@ + +-std=c++20 + +-I . + +-D TEST_BUILD + +-g + +-Wall -Werror -Wextra -Wfatal-errors diff --git a/cmdln_flags.cpp b/cmdln_flags.cpp new file mode 100644 index 0000000..bed2e13 --- /dev/null +++ b/cmdln_flags.cpp @@ -0,0 +1,57 @@ + +#include +#include +#include +#include + +#include "cmdln_flags.hpp" + +cmdln_flags::cmdln_flags(int argc, char* const* argv) +{ + static const struct option long_options[] = { + {"input-file", required_argument, 0, 'i'}, + {"dump-automata", no_argument, 0, 'd'}, + {"verbose", no_argument, 0, 'v'}, + {0, 0, 0, 0} + }; + + for (int c; (c = getopt_long(argc, argv, "i:dv", long_options, NULL)) >= 0; ) + { + switch (c) + { + case 'i': + input_path = optarg; + break; + + case 'd': + dump_automata = true; + break; + + case 'v': + verbose = true; + break; + + default: + exit(1); + break; + } + } + + if (!input_path) + { + puts("usage: sat-solver [-v] [-d] -i ./input/file.txt"); + + exit(1); + } +} + + + + + + + + + + + diff --git a/cmdln_flags.hpp b/cmdln_flags.hpp new file mode 100644 index 0000000..ff6be61 --- /dev/null +++ b/cmdln_flags.hpp @@ -0,0 +1,20 @@ + +#ifndef CLASS_CMDLN_FLAGS +#define CLASS_CMDLN_FLAGS + +#include + +class cmdln_flags +{ + public: + const char* input_path = NULL; + + bool dump_automata = false; + + bool verbose = false; + + public: + cmdln_flags(int argc, char* const* argv); +}; + +#endif diff --git a/dict.hpp b/dict.hpp new file mode 100644 index 0000000..715e697 --- /dev/null +++ b/dict.hpp @@ -0,0 +1,145 @@ + +#ifndef CLASS_DICT +#define CLASS_DICT + +#include +#include + +#include "avl.hpp" + +template < + typename K, + typename V> class dict +{ + public: + struct keyvalue_pair + { + K key; + V value; + + keyvalue_pair(K _key): + key(_key), value() + { + ; + } + + keyvalue_pair(K _key, V _value): + key(_key), value(_value) + { + ; + } + + auto operator <=> (const struct keyvalue_pair& other) const + { + return (key <=> other.key); + } + }; + + private: + avl_tree_t tree; + + public: + avl_tree_t::iterable begin() + { + return tree.begin(); + } + + avl_tree_t::iterable end() + { + return tree.end(); + } + + avl_tree_t::iterable begin() const + { + return tree.begin(); + } + + avl_tree_t::iterable end() const + { + return tree.end(); + } + + public: + dict() + { + ; + } + + struct keyvalue_pair* add(K key, V value) + { + struct keyvalue_pair* retval = NULL; + + struct keyvalue_pair pair(key, value); + + auto node = tree.insert(pair); + + if (node) + { + retval = &node->item; + } + else + { + abort(); + } + + return retval; + } + + bool has(K key) const + { + // ENTER; + + struct keyvalue_pair pair(key); + + auto node = tree.search(pair); + + bool retval = !!node; + + // dpvb(retval); + + // EXIT; + return retval; + } + + V& operator[](K key) const + { + struct keyvalue_pair pair(key); + + auto node = tree.search(pair); + + if (!node) + { + puts("dict.hpp: key loop failed"); + abort(); + } + + return node->item.value; + } + + ~dict() + { + ; + } +}; + + + + + + + + + + + + + + + + + + + + + +#endif diff --git a/find_solutions.cpp b/find_solutions.cpp new file mode 100644 index 0000000..5980b12 --- /dev/null +++ b/find_solutions.cpp @@ -0,0 +1,106 @@ + +#include +#include + +#include + +#include "find_solutions.hpp" + +static bool is_empty_solution_space( + unsigned number_of_variables, + const struct automata* start) +{ + const struct automata* moving = start; + + while (moving && number_of_variables--) + { + moving = moving->on[0] ?: moving->on[1]; + } + + return !moving || !moving->is_accepting; +} + +void find_solutions( + unsigned number_of_variables, + const struct automata* start) +{ + bool found_solution = false; + + // there are three cases: + // 1. solutions for no inputs + // 2. solutions for all inputs + // 3. solutions for some inputs + + // consider case 1: (solutions for no inputs) + if (!found_solution) + { + if (is_empty_solution_space(number_of_variables, start)) + { + puts("no solutions."); + + found_solution = true; + } + } + + // consider case 2: (solutions for all inputs) + if (!found_solution) + { + // to do this, we'll dis-prove the opposite: that the complement of the + // solution space is empty. + + struct automata* complement = automata::complement(start); + + if (is_empty_solution_space(number_of_variables, complement)) + { + puts("all solutions."); + + found_solution = true; + } + + automata::free(complement); + } + + // consider case 3: (solutions for some inputs) + if (!found_solution) + { + int solution[number_of_variables]; + + const struct automata* moving = start; + + for (unsigned i = 0; i < number_of_variables; i++) + { + if (moving->on[0]) + { + solution[i] = 0, moving = moving->on[0]; + } + else + { + solution[i] = 1, moving = moving->on[1]; + } + } + + assert(moving && moving->is_accepting); + + for (unsigned i = 0; i < number_of_variables; i++) + { + printf("variable %u = %i\n", i + 1, solution[i]); + } + + found_solution = true; + } +} + + + + + + + + + + + + + + + diff --git a/find_solutions.hpp b/find_solutions.hpp new file mode 100644 index 0000000..14dfdf4 --- /dev/null +++ b/find_solutions.hpp @@ -0,0 +1,7 @@ + +struct automata; + +void find_solutions( + unsigned number_of_variables, + const struct automata* start); + diff --git a/heap.hpp b/heap.hpp new file mode 100644 index 0000000..5807b32 --- /dev/null +++ b/heap.hpp @@ -0,0 +1,127 @@ + +template class heap +{ + public: + T* data = NULL; + size_t n = 0, cap = 0; + + public: + heap() + { + ; + } + + T pop() + { + // ENTER; + + assert(this->n); + + T retval = this->data[0], swap; + + if (--n) + { + size_t l, r, smallest, i = 0; + + data[0] = data[this->n]; + + again: l = 2 * i + 1, r = 2 * i + 2, smallest = i; + + if (l < this->n && data[l] < data[i]) + smallest = l; + + if (r < this->n && data[r] < data[smallest]) + smallest = r; + + if (smallest != i) + { + swap = data[i]; + data[i] = data[smallest]; + data[smallest] = swap; + + i = smallest; + + goto again; // forgive my father for I have sinned. + } + } + + // EXIT; + return retval; + } + + void push(T pushme) + { + // ENTER; + + if (n == cap) + { + cap = cap << 1 ?: 1; + + if constexpr (std::is_trivially_copyable_v) + { + data = realloc(data, sizeof(*data) * cap); + } + else + { + T* new_data = new T[cap](); + + for (size_t i = 0; i < n; i++) + { + new_data[i] = std::move(data[i]); + } + + delete[] data; + + data = new_data; + } + } + + size_t i = n++, j; + + T swap; + + data[i] = pushme; + + for (; i > 0 && data[j = (i - 1) / 2] > data[i]; i = j) + { + swap = data[i]; + data[i] = data[j]; + data[j] = swap; + } + + // EXIT; + } + + ~heap() + { + if constexpr (std::is_trivially_copyable_v) + { + free(data); + } + else + { + delete[] data; + } + } +}; + + + + + + + + + + + + + + + + + + + + + diff --git a/inputs/0.txt b/inputs/0.txt new file mode 100644 index 0000000..dca516e --- /dev/null +++ b/inputs/0.txt @@ -0,0 +1,15 @@ + +c 'c' means comment + +c I think it was f"p {number-of-variables} {number-of-clauses}"? +c then each line is a seperate clause, which is a list of variable indexes +c possibly negative, meaning complement, ending in 0? +c '0' is the "sentinel", so "1" is the first variable index. +c like this: + +p 3 3 + +1 +2 + -1 +3 + +2 +3 + +c a correct solution is: 0 1 0 diff --git a/inputs/1.txt b/inputs/1.txt new file mode 100644 index 0000000..864031e --- /dev/null +++ b/inputs/1.txt @@ -0,0 +1,12 @@ + +p 5 8 + +1 +5 + -1 +5 + +2 +5 + -2 +5 + +3 +5 + -3 +5 + +4 +5 + -4 +5 + +c the only correct solution is: 0 0 0 0 1 diff --git a/inputs/2.txt b/inputs/2.txt new file mode 100644 index 0000000..877a7c5 --- /dev/null +++ b/inputs/2.txt @@ -0,0 +1,9 @@ + +p 6 2 + +1 +2 +3 +4 +5 +6 + -1 -2 -3 -4 -5 -6 + + +c a correct solution is: 0 0 0 0 0 1 + + diff --git a/inputs/3.txt b/inputs/3.txt new file mode 100644 index 0000000..d308ff8 --- /dev/null +++ b/inputs/3.txt @@ -0,0 +1,13 @@ + +p 20 7 + 1 3 5 7 9 11 13 15 17 19 + 1 4 7 10 13 16 19 + 1 6 11 16 + 1 8 15 + 1 12 + 1 14 + 1 18 + +c a correct solution is: 0 0 0 0 0 0 0 0 0 0 0 1 0 1 1 1 0 1 0 0 + + diff --git a/inputs/all.txt b/inputs/all.txt new file mode 100644 index 0000000..8f67ab0 --- /dev/null +++ b/inputs/all.txt @@ -0,0 +1,11 @@ + +c 'c' means comment + +p 3 3 + +1 -1 + +2 -2 + +3 -3 + +c all inputs satisfy the constraints. + + diff --git a/inputs/none.txt b/inputs/none.txt new file mode 100644 index 0000000..def1b03 --- /dev/null +++ b/inputs/none.txt @@ -0,0 +1,13 @@ + +c 'c' means comment + +p 3 6 + +1 + +2 + +3 + -1 + -2 + -3 + +c no inputs satisfy the constraints. + diff --git a/list.hpp b/list.hpp new file mode 100644 index 0000000..0f2fe42 --- /dev/null +++ b/list.hpp @@ -0,0 +1,210 @@ + +#ifndef CLASS_LIST +#define CLASS_LIST + +#include +#include +#include + +#include + +#include +#include +#include + +template class list +{ + public: + class iterable + { + private: + list* owner; + size_t index; + + public: + iterable( + list* _owner, size_t _index): + owner(_owner), index(_index) + { + ; + } + + T operator *() + { + assert(index <= owner->n); + + VALGRIND_CHECK_VALUE_IS_DEFINED(owner->data[index]); + + T retval = owner->data[index]; + + return retval; + } + + void operator ++() + { + index++; + } + + bool operator != (const iterable& other) + { + bool retval = false + || this->owner != other.owner + || this->index != other.index; + + return retval; + } + }; + + class const_iterable + { + private: + const list* owner; + size_t index; + + public: + const_iterable( + const list* _owner, size_t _index): + owner(_owner), index(_index) + { + ; + } + + const T operator *() + { + assert(index <= owner->n); + + VALGRIND_CHECK_VALUE_IS_DEFINED(owner->data[index]); + + const T retval = owner->data[index]; + + return retval; + } + + void operator ++() + { + index++; + } + + bool operator != (const const_iterable& other) + { + bool retval = false + || this->owner != other.owner + || this->index != other.index; + + return retval; + } + }; + + public: + T* data; + size_t n, cap; + + public: + list(): data(NULL), n(0), cap(0) + { + ; + } + + iterable begin() + { + return iterable(this, 0); + } + + iterable end() + { + return iterable(this, n); + } + + const_iterable begin() const + { + return const_iterable(this, 0); + } + + const_iterable end() const + { + return const_iterable(this, n); + } + + void append(T appendme) + { + if constexpr (std::is_trivially_copyable_v) + { + if (n == cap) + { + cap = cap << 1 ?: 1; + + data = (T*) realloc((void*) data, sizeof(*data) * cap); + } + + data[n++] = appendme; + } + else + { + if (n == cap) + { + cap = cap << 1 ?: 1; + + T* new_data = new T[cap](); + + for (size_t i = 0; i < n; i++) + { + new_data[i] = std::move(data[i]); + } + + delete[] data; + + data = new_data; + } + + new (&data[n]) T(appendme); + + VALGRIND_CHECK_VALUE_IS_DEFINED(data[n]); + + n++; + } + } + + ~list() + { + if constexpr (std::is_trivially_copyable_v) + { + free(data); + } + else + { + delete[] data; + } + } +}; + +#endif + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/main.c b/main.c new file mode 100644 index 0000000..056e86f --- /dev/null +++ b/main.c @@ -0,0 +1,1642 @@ + +#if 0 +#define _GNU_SOURCE + +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#define argv0 \ + program_invocation_name + +#define TODO \ + assert(!"TODO"); + +#define CHECK \ + assert(!"CHECK"); + +#ifdef DEBUG +unsigned debug_depth = 0; + +#define ENTER \ + printf("%*s" "<%s>\n", debug_depth++, "", __PRETTY_FUNCTION__); + +#define EXIT \ + printf("%*s" "\n", --debug_depth, "", __PRETTY_FUNCTION__); + +#define dpvs(x) \ + printf("%*s" "%s = \"%s\"\n", debug_depth, "", #x, x); + +#define dpvu(x) \ + printf("%*s" "%s = %u\n", debug_depth, "", #x, x); + +#define dpvlu(x) \ + printf("%*s" "%s = %lu\n", debug_depth, "", #x, x); + +#define dpvi(x) \ + printf("%*s" "%s = %i\n", debug_depth, "", #x, x); + +#define dpvb(x) \ + printf("%*s" "%s = %s\n", debug_depth, "", #x, (x) ? "true" : "false"); + +#define ddprintf(fmt, ...) \ + printf("%*s" fmt, debug_depth, "", ## __VA_ARGS__); +#else +#define ENTER ; + +#define EXIT ; + +#define dpvs(x) ; + +#define dpvu(x) ; + +#define dpvlu(x) ; + +#define dpvi(x) ; + +#define dpvb(x) ; + +#define ddprintf(fmt, ...) ; +#endif + +void* smalloc(size_t size) +{ + void* ptr = malloc(size); + + if (!ptr) + { + TODO; + } + + return ptr; +} + +void* srealloc(void* oldptr, size_t newsize) +{ + void* newptr = realloc(oldptr, newsize); + + if (!newptr) + { + TODO; + } + + return newptr; +} + +struct cmdln_flags +{ + const char* input_file; + + bool dump_automata, verbose; +}; + +struct cmdln_flags* parse_args( + int argc, char* const* argv) +{ + ENTER; + + const char* input_file = NULL; + + bool dump_automata = false; + + bool verbose = false; + + int i = 1; + + while (i < argc) + { + const char* arg = argv[i]; + + dpvs(arg); + + if (arg[0] == '-') + { + if (!strcmp(arg, "-d")) + { + dump_automata = true, i++; + } + else if (!strcmp(arg, "-v")) + { + verbose = true, i++; + } + else + { + TODO; + } + } + else if (input_file) + { + TODO; + } + else + { + input_file = arg, i++; + } + } + + if (!input_file) + { + printf("%s: missing input file!\n", argv0); + + exit(1); + } + + struct cmdln_flags* flags = smalloc(sizeof(*flags)); + + flags->input_file = input_file; + + flags->dump_automata = dump_automata; + + flags->verbose = verbose; + + EXIT; + return flags; +} + +void free_cmdln_flags( + struct cmdln_flags* this) +{ + TODO; +} + +struct quack +{ + void** data; + size_t i, n, cap; +}; + +struct quack* new_quack(void) +{ + ENTER; + + struct quack* this = smalloc(sizeof(*this)); + + this->data = NULL; + + this->i = 0; + this->n = 0; + this->cap = 0; + + EXIT; + return this; +} + +void quack_append( + struct quack* this, + void* element) +{ + ENTER; + + dpvlu(this->i); + dpvlu(this->n); + dpvlu(this->cap); + + if (this->n == this->cap) + { + size_t oldcap = this->cap; + size_t newcap = oldcap << 1 ?: 1; + + this->data = srealloc(this->data, sizeof(*this->data) * newcap); + + if (this->i) + { + TODO; + } + + this->cap = newcap; + + dpvlu(this->cap); + } + + size_t index = ((this->i + this->n++) % this->cap); + + // ddprintf("wrote to index %lu\n", index); + + this->data[index] = element; + + dpvlu(this->i); + dpvlu(this->n); + dpvlu(this->cap); + + EXIT; +} + +void* quack_pop( + struct quack* this) +{ + ENTER; + + assert(this->n); + + dpvlu(this->i); + dpvlu(this->n); + dpvlu(this->cap); + +/* ddprintf("reading from index %lu\n", this->i);*/ + + void* retval = this->data[this->i]; + + this->i = (this->i + 1) % this->cap, this->n--; + + dpvlu(this->i); + dpvlu(this->n); + dpvlu(this->cap); + + EXIT; + return retval; +} + +void free_quack( + struct quack* this) +{ + ENTER; + + free(this); + + EXIT; +} + +struct automata; + +struct automataset +{ + struct avl_tree_t* tree; + + size_t refcount; +}; + +int ptrcmp(const void* a, const void* b) +{ + if (a > b) + return +1; + + if (a < b) + return -1; + + return +0; +} + +struct automataset* new_automataset(void) +{ + ENTER; + + struct automataset* this = smalloc(sizeof(*this)); + + this->tree = avl_alloc_tree(ptrcmp, NULL); + + this->refcount = 1; + + EXIT; + return this; +} + +bool automataset_is_nonempty( + struct automataset* this) +{ + return !!this->tree->head; +} + +bool automataset_add( + struct automataset* this, + struct automata* automata) +{ + bool retval; + ENTER; + + errno = 0; + + struct avl_node_t* node = avl_insert(this->tree, automata); + + if (node) + { + retval = true; + } + else if (errno == EEXIST) + { + retval = false; + } + else + { + TODO; + } + + EXIT; + return retval; +} + +void automataset_foreach( + struct automataset* this, + void (*callback)( + struct automata*)) +{ + ENTER; + + for (struct avl_node_t* node = this->tree->head; node; node = node->next) + { + callback(node->item); + } + + EXIT; +} + +struct automata* automataset_pop( + struct automataset* this) +{ + ENTER; + + assert(this->tree->head); + + struct automata* retval = this->tree->head->item; + + avl_delete_node(this->tree, this->tree->head); + + EXIT; + return retval; +} + +void free_automataset( + struct automataset* this) +{ + ENTER; + + if (!--this->refcount) + { + avl_free_tree(this->tree); + + free(this); + } + + EXIT; +} + +struct automata +{ + bool is_accepting; + + struct automata *on[2]; +}; + +struct automata* new_automata(void) +{ + ENTER; + + struct automata* this = malloc(sizeof(*this)); + + this->is_accepting = false; + + this->on[0] = NULL; + this->on[1] = NULL; + + EXIT; + return this; +} + +void dump_automata( + struct automata* start, + const char* fmt, ...) +{ + ENTER; + + char path[PATH_MAX]; + + static size_t dump_id = 0; + + snprintf(path, PATH_MAX, "/tmp/%05lu.dot", dump_id++); + + FILE* stream = fopen(path, "w"); + + fprintf(stream, "" + "digraph {" "\n" + "\t" "rankdir = LR;" "\n" + "\t" + "\t" "node [" "\n" + "\t" "\t" "shape = circle" "\n" + "\t" "\t" "label = \"\"" "\n" + "\t" "];" "\n" + "\t" "\n" + ""); + + va_list va; + va_start(va, fmt); + + vfprintf(stream, fmt, va); + + va_end(va); + + struct quack* todo = new_quack(); + + struct automataset* queued = new_automataset(); + + if (automataset_add(queued, start)) + { + quack_append(todo, start); + } + + while (todo->n) + { + struct automata* state = quack_pop(todo); + + if (state->is_accepting) + { + fprintf(stream, "\"%p\" [ shape = doublecircle ];\n", state); + } + + for (int on = 0; on < 2; on++) + { + struct automata* to = state->on[on]; + + if (to) + { + fprintf(stream, "\"%p\" -> \"%p\" [label = \"%i\"];\n", state, to, on); + + if (automataset_add(queued, to)) + { + quack_append(todo, to); + } + } + } + } + + fprintf(stream, "" + "}" "\n" + ""); + + free_quack(todo); + + free_automataset(queued); + + fclose(stream); + + EXIT; +} + +struct automata* create_variable_automata( + int depth, + const struct cmdln_flags* flags, + unsigned variable_index, + bool value, + unsigned number_of_variables) +{ + ENTER; + + assert(variable_index < number_of_variables); + + if (flags->verbose) + { + printf("%*s" "variable(index = %u, value = %s):\n", + depth++, "", variable_index, value ? "true" : "false"); + } + + size_t total_number_of_states = 0; + + struct automata* start = new_automata(); + struct automata* moving = start; + + total_number_of_states++; + + for (unsigned i = 0; i < number_of_variables; i++) + { + struct automata* new = new_automata(); + total_number_of_states++; + + if (i == variable_index) + { + moving->on[value] = new; + } + else + { + moving->on[0] = new; + moving->on[1] = new; + } + + moving = new; + } + + moving->is_accepting = true; + + if (flags->verbose) + { + printf("%*s" "returned automata with %lu states.\n", + depth, "", total_number_of_states); + } + + EXIT; + return start; +} + +struct automata* automata_union( + int depth, + const struct cmdln_flags* flags, + const struct automata* left, + const struct automata* right) +{ + ENTER; + + if (flags->verbose) + { + printf("%*s" "union():\n", depth++, ""); + } + + struct bundle + { + const struct automata *left, *right; // key + + struct automata* new; + }; + + struct bundle* new_bundle( + const struct automata *left, + const struct automata* right, + struct automata* new) + { + ENTER; + + struct bundle* this = smalloc(sizeof(*this)); + + this->left = left; + this->right = right; + + this->new = new; + + EXIT; + return this; + } + + int compare(const void* a, const void* b) + { + const struct bundle *A = a, *B = b; + + return ptrcmp(A->left, B->left) ?: ptrcmp(A->right, B->right); + } + + void append(struct bundle* bundle) + { + ENTER; + + EXIT; + } + + size_t total_number_of_states = 0; + + struct avl_tree_t* mapping = avl_alloc_tree(compare, free); + + struct automata* start = new_automata(); + + total_number_of_states++; + + struct quack* todo = new_quack(); + + // initial state: + { + struct bundle* new = new_bundle(left, right, start); + + quack_append(todo, new); + + avl_insert(mapping, new); + } + + while (todo->n) + { + struct bundle* bundle = quack_pop(todo); + + const struct automata *const left = bundle->left; + const struct automata *const right = bundle->right; + + struct automata* const new = bundle->new; + + new->is_accepting = false + || (left && left->is_accepting) + || (right && right->is_accepting); + + for (int value = 0; value < 2; value++) + { + struct automata* left_to = left ? left->on[value] : NULL; + struct automata* right_to = right ? right->on[value] : NULL; + + if (left_to || right_to) + { + struct avl_node_t* node = avl_search(mapping, + &(struct bundle) {left_to, right_to, NULL}); + + if (node) + { + struct bundle* bundle_to = node->item; + + new->on[value] = bundle_to->new; + } + else + { + struct automata* new_to = new_automata(); + + total_number_of_states++; + + new->on[value] = new_to; + + struct bundle* bundle_to = new_bundle( + left_to, right_to, new_to); + + avl_insert(mapping, bundle_to); + + quack_append(todo, bundle_to); + } + } + } + + if (flags->dump_automata) + { + dump_automata(start, "label = \"automata_union\""); + } + } + + if (flags->verbose) + { + printf("%*s" "returned automata with %lu states" "\n", + depth, "", total_number_of_states); + } + + avl_free_tree(mapping); + + free_quack(todo); + + EXIT; + return start; +} + +struct automata* automata_intersection( + const struct cmdln_flags* flags, + const struct automata* left, + const struct automata* right) +{ + TODO; +} + +struct automata* automata_simplify( + int depth, + const struct cmdln_flags* flags, + struct automata* original) +{ + ENTER; + + if (flags->verbose) + { + printf("%*s" "simplify():\n", depth++, ""); + } + + struct pair + { + struct automata *a, *b; + }; + + struct pair* new_pair(struct automata* a, struct automata* b) + { + ENTER; + + struct pair* this = smalloc(sizeof(*this)); + + assert(a < b); + + this->a = a; + this->b = b; + + EXIT; + return this; + } + + struct dependent_of_node + { + struct pair pair; + + struct avl_tree_t* dependent_of; // tree of pairs + }; + + struct dependent_of_node* new_dependent_of_node( + struct automata* a, struct automata* b) + { + ENTER; + + TODO; + #if 0 + struct dependent_of_node* this = smalloc(sizeof(*this)); + + this->pair.a = a; + this->pair.b = b; + + this->dependent_of = avl_alloc_tree(compare_pairs, free); + + EXIT; + return this; + #endif + } + + int compare_dependent_of_nodes(const void* a, const void* b) + { + TODO; + #if 0 + int cmp = 0; + const struct dependent_of_node *A = a, *B = b; + ENTER; + + cmp = compare_pairs(&A->pair, &B->pair); + + EXIT; + return cmp; + #endif + } + + void free_dependent_of_node(void* ptr) + { + TODO; + #if 0 + struct dependent_of_node* this = ptr; + ENTER; + + avl_free_tree(this->dependent_of); + + free(this); + + EXIT; + #endif + } + + struct task + { + struct pair pair; + + unsigned hopcount; + }; + + struct task* new_task( + struct automata* a, struct automata* b, + unsigned hopcount) + { + ENTER; + + struct task* this = smalloc(sizeof(*this)); + + this->pair.a = a; + this->pair.b = b; + + this->hopcount = hopcount; + + EXIT; + return this; + } + + int compare_tasks(const void* a, const void* b) + { + const struct task* A = a, *B = b; + int cmp; + ENTER; + + if (A->hopcount > B->hopcount) + cmp = +1; + else if (A->hopcount < B->hopcount) + cmp = -1; + else + cmp = +0; + + EXIT; + return cmp; + } + + struct heap + { + void** data; + + unsigned n, cap; + + int (*cmp)(const void*, const void*); + }; + + struct heap* new_heap( + int (*cmp)(const void*, const void*)) + { + ENTER; + + struct heap* this = malloc(sizeof(*this)); + + this->cmp = cmp; + + this->data = NULL; + this->n = 0; + this->cap = 0; + + EXIT; + return this; + } + + void* heap_pop(struct heap* this) + { + ENTER; + + assert(this->n); + + void* retval = this->data[0], *swap; + + if (--this->n) + { + unsigned l, r, smallest, i = 0; + void** const data = this->data; + + data[0] = data[this->n]; + + again: l = 2 * i + 1, r = 2 * i + 2, smallest = i; + + if (l < this->n && this->cmp(data[l], data[i]) < 0) + smallest = l; + + if (r < this->n && this->cmp(data[r], data[smallest]) < 0) + smallest = r; + + if (smallest != i) + { + swap = data[i]; + data[i] = data[smallest]; + data[smallest] = swap; + + i = smallest; + + goto again; // forgive my father for I have sinned. + } + } + + EXIT; + return retval; + } + + void heap_push(struct heap* this, void* new) + { + ENTER; + + if (this->n + 1 > this->cap) + { + this->cap = this->cap << 1 ?: 1; + + this->data = realloc(this->data, sizeof(*this->data) * this->cap); + } + + size_t i = this->n++, j; + void** const data = this->data, *swap; + + data[i] = new; + + for (; i > 0 && this->cmp(data[j = (i - 1) / 2], data[i]) > 0; i = j) + { + swap = data[i]; + data[i] = data[j]; + data[j] = swap; + } + + EXIT; + } + + void add_dep( + struct avl_tree_t* dependent_of, + struct automata* a_on, struct automata* b_on, + struct automata* a_of, struct automata* b_of) + { + ENTER; + + assert(a_on < b_on); + + if (a_of > b_of) + { + struct automata* swap = b_of; + + b_of = a_of, a_of = swap; + } + + struct avl_node_t* node = avl_search(dependent_of, + &(struct pair){a_of, b_of}); + + if (node) + { + struct dependent_of_node* old = node->item; + + if (!avl_search(old->dependent_of, &(struct pair){a_on, b_on})) + { + struct pair* dep = new_pair(a_on, b_on); + + avl_insert(old->dependent_of, dep); + } + } + else + { + struct dependent_of_node* new = new_dependent_of_node(a_of, b_of); + + struct pair* dep = new_pair(a_on, b_on); + + avl_insert(new->dependent_of, dep); + + avl_insert(dependent_of, new); + } + + EXIT; + } + + + struct automataset* build_universe(struct automata* start) + { + ENTER; + + struct automataset* universe = new_automataset(); + + struct quack* todo = new_quack(); + + quack_append(todo, start); + + automataset_add(universe, start); + + while (todo->n) + { + struct automata* node = quack_pop(todo); + + for (int value = 0; value < 2; value++) + { + struct automata* const to = node->on[value]; + + if (to && automataset_add(universe, to)) + { + quack_append(todo, to); + } + } + } + + free_quack(todo); + + EXIT; + return universe; + } + + struct avl_tree_t* dependent_of = avl_alloc_tree( + compare_dependent_of_nodes, free_dependent_of_node); + + struct automataset* universe = build_universe(original); + + struct heap* todo = new_heap(compare_tasks); + + automataset_foreach(universe, ({ + void runme(struct automata* a) { + automataset_foreach(universe, ({ + void runme(struct automata* b) { + if (a < b) + { + bool unequal = false; + + if (a->is_accepting != b->is_accepting) + { + unequal = true; + } + else for (int value = 0; !unequal && value < 2; value++) + { + struct automata* a_to = a->on[value]; + struct automata* b_to = b->on[value]; + + if (!a_to != !b_to) + { + unequal = true; + } + else if (a_to && b_to) + { + add_dep(dependent_of, a, b, a_to, b_to); + } + } + + if (unequal) + { + heap_push(todo, new_task(a, b, 0)); + } + } + } + runme; + })); + } + runme; + })); + + TODO; + #if 0 + + #ifdef VERBOSE + void handler12(int _) + { + char ptr[200] = {}; + + size_t len = snprintf(ptr, 200, + "\e[K" "zebu: automata simplify (allocating sets): %ju of %ju (%.2f%%)\r", + count, n, (((double) count * 100) / n)); + + if (write(1, ptr, len) != len) + { + abort(); + } + } + + { + count = 0, n = automataset_len(universe); + + #ifdef LINUX_PLATFORM + signal(SIGALRM, handler12); + #else + #ifdef WINDOWS_PLATFORM + timer_handler = handler12; + #else + #error bad platform + #endif + #endif + } + #endif + + struct avl_tree_t* connections = avl_alloc_tree(compare_same_as_nodes, free_same_as_node); + + automataset_foreach(universe, ({ + void runme(void* ptr) { + struct automata* a = ptr; + + struct automataset* uni = automataset_clone(universe); + + struct same_as_node* sa = new_same_as_node(a, uni); + + avl_insert(connections, sa); + + #ifdef VERBOSE + count++; + #endif + } + runme; + })); + + struct avl_tree_t* connections = avl_alloc_tree(compare_same_as_nodes, free_same_as_node); + + automataset_foreach(universe, ({ + void runme(void* ptr) { + struct automata* a = ptr; + + struct automataset* uni = automataset_clone(universe); + + struct same_as_node* sa = new_same_as_node(a, uni); + + avl_insert(connections, sa); + + #ifdef VERBOSE + count++; + #endif + } + runme; + })); + + #ifdef VERBOSE + unsigned completed = 0; + + void handler2(int _) + { + char buffer[1000] = {}; + + unsigned total = completed + heap_len(todo); + + size_t len = snprintf(buffer, sizeof(buffer), + "\e[K" "zebu: automata simplify (percolate): %u of %u (%.2f%%)\r", + completed, total, + (double) completed * 100 / total); + + if (write(1, buffer, len) != len) + { + abort(); + } + } + + #ifdef LINUX_PLATFORM + signal(SIGALRM, handler2); + #else + #ifdef WINDOWS_PLATFORM + timer_handler = handler2; + #else + #error bad platform + #endif + #endif + #endif + + while (heap_is_nonempty(todo)) + { + #ifdef VERBOSE + completed++; + #endif + + struct task* task = heap_pop(todo); + + if (mark_as_unequal(connections, &task->pair)) + { + struct avl_node_t* node = avl_search(dependent_of, &task->pair); + + if (node) + { + struct dependent_of_node* dep = node->item; + + unsigned hopcount = task->hopcount + 1; + + avl_tree_foreach(dep->dependent_of, ({ + void runme(void* ptr) { + const struct pair* pair = ptr; + heap_push(todo, new_task(pair->a, pair->b, hopcount)); + } + runme; + })); + } + } + + free(task); + } + + // consider which states can reach any accepting state. + + struct automata* new_start = clone(connections, original); + + avl_free_tree(dependent_of); + + free_automataset(universe); + + avl_free_tree(connections); + + free_heap(todo); + + #ifdef VERBOSE + #ifdef LINUX_PLATFORM + signal(SIGALRM, default_sighandler); + #else + #ifdef WINDOWS_PLATFORM + timer_handler = default_sighandler; + #else + #error bad platform + #endif + #endif + #endif + + EXIT; + return new_start; + + #endif + + size_t total_number_of_states = 0; + + TODO; + + if (flags->verbose) + { + printf("%*s" "returned automata with %lu states" "\n", + depth, "", total_number_of_states); + } + + EXIT; +} + +void free_automata( + struct automata* this) +{ + TODO; +} + +struct clause +{ + struct clause_bundle { + unsigned variable; + bool value; + }* data; + + size_t n, cap; +}; + +struct clause* new_clause(void) +{ + struct clause* this = smalloc(sizeof(*this)); + + this->data = NULL; + + this->n = 0; + this->cap = 0; + + return this; +} + +void clause_append( + struct clause* this, + unsigned variable, + bool value) +{ + ENTER; + + if (this->n == this->cap) + { + this->cap = this->cap << 1 ?: 1; + + this->data = srealloc(this->data, sizeof(*this->data) * this->cap); + } + + this->data[this->n++] = (struct clause_bundle) {variable, value}; + + EXIT; +} + +void free_clause( + struct clause* this) +{ + TODO; +} + +struct problem +{ + unsigned number_of_variables; + + struct { + struct clause** data; + + size_t n, cap; + } clauses; +}; + +struct problem* new_problem( + unsigned number_of_variables) +{ + ENTER; + + struct problem* this = smalloc(sizeof(*this)); + + this->number_of_variables = number_of_variables; + + this->clauses.data = NULL; + this->clauses.n = 0; + this->clauses.cap = 0; + + EXIT; + return this; +} + +void problem_append( + struct problem* this, + struct clause* clause) +{ + ENTER; + + if (this->clauses.n == this->clauses.cap) + { + this->clauses.cap = this->clauses.cap << 1 ?: 1; + + this->clauses.data = srealloc( + this->clauses.data, + sizeof(*this->clauses.data) * this->clauses.cap); + } + + this->clauses.data[this->clauses.n++] = clause; + + EXIT; +} + +void free_problem( + struct problem* this) +{ + TODO; +} + +struct problems +{ + struct problem** data; + size_t n, cap; +}; + +struct problems* new_problems(void) +{ + ENTER; + + struct problems* this = smalloc(sizeof(*this)); + + this->data = NULL; + this->n = 0; + this->cap = 0; + + EXIT; + return this; +} + +void problems_append( + struct problems* this, + struct problem* problem) +{ + ENTER; + + if (this->n == this->cap) + { + this->cap = this->cap << 1 ?: 1; + + this->data = srealloc(this->data, sizeof(*this->data) * this->cap); + } + + this->data[this->n++] = problem; + + EXIT; +} + +void free_problems( + struct problems* this) +{ + TODO; +} + + +struct problems* parse(const char* file) +{ + ENTER; + + dpvs(file); + + struct problems* problems = new_problems(); + + FILE* stream = fopen(file, "r"); + + char *line = NULL; + size_t len = 0; + ssize_t nread; + + while ((nread = getline(&line, &len, stream)) > 0) + { + line[--nread] = 0; + + dpvs(line); + + if (line[0] == '\0') continue; + if (line[0] == 'c') continue; + + if (line[0] != 'p') + { + TODO; + exit(1); + } + + unsigned number_of_variables; + unsigned number_of_clauses; + + int r = sscanf(line, " p %u %u ", &number_of_variables, &number_of_clauses); + + if (r < 2) + { + TODO; + exit(1); + } + + dpvu(number_of_variables); + + dpvu(number_of_clauses); + + struct problem* problem = new_problem(number_of_variables); + + for (unsigned i = 0; i < number_of_clauses; i++) + { + nread = getline(&line, &len, stream); + + if (nread < 0) + { + TODO; + exit(1); + } + + line[--nread] = 0; + + dpvs(line); + + struct clause* clause = new_clause(); + + char *moving = line; + + for (char* word; (word = strtok_r(NULL, " ", &moving)); ) + { + dpvs(word); + + errno = 0; + + char* m; + + signed variable = strtol(word, &m, 10); + + if (errno || *m) + { + TODO; + exit(1); + } + + bool value = true; + + if (variable < 0) + { + variable = -variable; + value = !value; + } + + dpvi(variable); + + dpvb(value); + + assert(variable > 0); + + clause_append(clause, variable, value); + } + + problem_append(problem, clause); + } + + problems_append(problems, problem); + } + + free(line); + fclose(stream); + + EXIT; + return problems; +} + +struct automata* build_automata( + struct cmdln_flags* flags, + struct problem* problem) +{ + ENTER; + + unsigned number_of_variables = problem->number_of_variables; + + struct { + unsigned* data; + size_t n, cap; + } variable_lookup = {}; + + unsigned variable_to_index(signed variable) + { + unsigned retval; + ENTER; + + assert(variable > 0); + + dpvi(variable); + dpvlu(variable_lookup.cap); + + if ((unsigned) variable < variable_lookup.cap) + { + dpvu(variable_lookup.data[variable]); + + if (variable_lookup.data[variable] == (unsigned) -1) + { + variable_lookup.data[variable] = variable_lookup.n++; + } + + dpvu(variable_lookup.data[variable]); + + retval = variable_lookup.data[variable]; + } + else + { + while ((unsigned) variable >= variable_lookup.cap) + { + size_t oldcap = variable_lookup.cap; + size_t newcap = oldcap << 1 ?: 1; + + variable_lookup.data = srealloc( + variable_lookup.data, + sizeof(*variable_lookup.data) * newcap); + + for (size_t i = oldcap; i < newcap; i++) + { + variable_lookup.data[i] = -1; + } + + variable_lookup.cap = newcap; + + dpvlu(variable_lookup.cap); + } + + retval = variable_lookup.data[variable] = variable_lookup.n++; + } + + dpvu(retval); + + EXIT; + return retval; + } + + int depth = 0; + + for (unsigned i = 0, n = problem->clauses.n; i < n; i++) + { + struct clause* clause = problem->clauses.data[i]; + + struct automata* clause_automata = NULL; + + depth++; + + for (unsigned j = 0, m = clause->n; j < m; j++) + { + depth++; + + struct clause_bundle bundle = clause->data[j]; + + unsigned index = variable_to_index(bundle.variable); + + struct automata* variable_automata = create_variable_automata( + depth, flags, + index, bundle.value, number_of_variables); + + if (flags->dump_automata) + { + dump_automata(variable_automata, + "label = \"%i (%u) = %s\"", bundle.variable, index, + bundle.value ? "true" : "false"); + } + + if (clause_automata) + { + struct automata* old = clause_automata; + + struct automata* new = automata_union( + depth, flags, old, variable_automata); + + struct automata* simp = automata_simplify( + depth, flags, new); + + clause_automata = simp; + + free_automata(new); + + free_automata(old); + } + else + { + clause_automata = variable_automata; + } + + depth--; + } + + TODO; + +/* if args.dump_automata:*/ +/* title = " or ".join(f"{a} = {b}" for a, b in clause);*/ +/* */ +/* dump_automata(clause_automata, title);*/ +/* */ +/* clause_automatas.append(clause_automata); */ + + depth--; + } + + TODO; + + free(variable_lookup.data); + + EXIT; +} + +int main( + int argc, + char* const* argv) +{ + ENTER; + + struct cmdln_flags* flags = parse_args(argc, argv); + + struct problems* problems = parse(flags->input_file); + + for (unsigned i = 0, n = problems->n; i < n; i++) + { + struct problem* problem = problems->data[i]; + + struct automata* automata = build_automata(flags, problem); + + TODO; + + free_automata(automata); + } + + free_problems(problems); + + free_cmdln_flags(flags); + + EXIT; + return 0; +} + + + + + + + + + + + + + + + +#endif diff --git a/main.cpp b/main.cpp new file mode 100644 index 0000000..815339c --- /dev/null +++ b/main.cpp @@ -0,0 +1,45 @@ + +#include + +#include + +#include + +#include + +#include + +int main( + int argc, + char* const* argv) +{ + cmdln_flags flags(argc, argv); + + auto problems = parse(flags.input_path); + + for (const auto &problem: problems) + { + automata* start = build_automata(flags, problem); + + find_solutions(problem->number_of_variables, start); + + automata::free(start); + } + + return 0; +} + + + + + + + + + + + + + + + diff --git a/main.py b/main.py new file mode 100755 index 0000000..19d0061 --- /dev/null +++ b/main.py @@ -0,0 +1,605 @@ +#!/usr/bin/env python3.10 + +import string; +import itertools; +import argparse; + +def parse_args(): + parser = argparse.ArgumentParser( + prog = 'main', + description = """ + Proof-of-concept SAT solver. + """, + epilog = """ + Bottom Text. + """) + + parser.add_argument('input_file', help = """ + Set input file path. + """) + + parser.add_argument('-d', '--dump-automata', action = 'store_true', help = """ + While solving the SAT problem, print out intermmediate automatas + and the final automata. + The .dot file output file names will follow the form: "dot/%%05u.dot" + """) + + parser.add_argument('-v', '--validate', action = "store_true", + help = """ + Automatically validate the solution (or every solution) by feeding + each solution back into the boolean expression, checking that the + conclusions made by the solver truely are correct. + + If the solver concludes that there are no solutions, this option + will check that by evaluating all inputs, checking that they + are indeed no solutions. + + If the solver concludes that all possible inputs are valid + solutions, this option will check all inputs, checking that they + are indeed valid solutions. + """); + + return parser.parse_args(sys.argv[1:]); + +def parse_file(filename): + # list of tuple of (number-of-variables, list of clauses). + # list of clauses is a tuple of (variable, value) tuples. + problems = list(); + + with open(filename) as stream: + iterator = iter(stream); + + for line in iterator: + line = line.strip(); + + # skip blank lines: + if not line: continue; + + # skip comment lines: + if line.startswith("c"): continue; + + assert(line.startswith("p")); + + words = line.split(); + + number_of_variables = int(words[1]); + + number_of_clauses = int(words[2]); + + print(f"number_of_variables = {number_of_variables}"); + + print(f"number_of_clauses = {number_of_clauses}"); + + clauses = list(); + # list of clauses is a list of (variable, value) tuples + + for _ in range(number_of_clauses): + line = next(iterator); + + clause = list(); + + for x in line.split(): + y = int(x); + z = abs(y); + if y < 0: + clause.append((z, 0)); + else: + clause.append((z, 1)); + + clauses.append(clause); + + problems.append((number_of_variables, clauses)); + + return problems; + +def create_variable_automata(variable, value, number_of_variables): + print(f"create_variable_automata()"); + + automata = [(0, (i + 1, i + 1)) for i in range(number_of_variables)]; + + automata.append((1, (None, None))); + + v = variable; +# v = variable - 1; + + if value: + automata[v] = (0, (None, v + 1)); + else: + automata[v] = (0, (v + 1, None)); + + return automata; + +def mass_union(args, subautomatas): + print(f"mass_union(subautomatas = {subautomatas})"); + + n = len(subautomatas); + + mapping = {((0,) * n): 0}; # (indexes of subautomatas) -> index in automata + + todo = [((0, ) * n, 0)] + + automata = [()]; + + while todo: + subindexes, index = todo.pop(0); + + accepting = int(any(0 if x is None else subautomatas[i][x][0] for i, x in enumerate(subindexes))) + + newtos = [None, None]; + + for on, to in enumerate(zip(*((None, None) if x is None else subautomatas[i][x][1] for i, x in enumerate(subindexes)))): + if any(x is not None for x in to): + if to in mapping: + newtos[on] = mapping[to]; + else: + newto = len(automata); + + newtos[on] = newto; + + automata.append(()); + + mapping[to] = newto; + + todo.append((to, newto)); + + automata[index] = (accepting, newtos); + + return automata; + +def intersect_automata(args, lauto, rauto): + print(f"intersect_automata(left = {lauto}, right = {rauto})"); + + mapping = {(0, 0): 0}; # (left index, right index) -> new index + + todo = [((0, 0), 0)] + + nauto = [()]; + + while todo: + (lindex, rindex), nindex = todo.pop(0); + + laccepting, ltos = lauto[lindex]; + + raccepting, rtos = rauto[rindex]; + + naccepting = int(laccepting and raccepting); + + newtos = [None, None]; + + for on, to in enumerate(zip(ltos, rtos)): + if to[0] != None and to[1] != None: + if to in mapping: + newtos[on] = mapping[to]; + else: + newto = len(nauto); + + newtos[on] = newto; + + nauto.append(()); + + mapping[to] = newto; + + todo.append((to, newto)); + + nauto[nindex] = (naccepting, newtos); + + if args.dump_automata: + dump_automata(nauto, title = f"intersection: {len(nauto)}"); + + return nauto; + +def mass_intersection(args, subautomatas): + print(f"mass_intersection(subautomatas = {subautomatas})"); + + assert(subautomatas); + + if len(subautomatas) == 1: + return subautomatas[0]; + else: + n = len(subautomatas) // 2; + + left = mass_intersection(args, subautomatas[:n]); + + right = mass_intersection(args, subautomatas[n:]); + + automata = intersect_automata(args, left, right); + + if args.dump_automata: + dump_automata(automata, title = f"mass-intersection: {len(automata)}"); + + automata = simplify_automata(automata); + + if args.dump_automata: + dump_automata(automata, title = f"simplified mass-intersection: {len(automata)}"); + + return automata; + +#def mass_intersection(args, subautomatas): +# print(f"mass_intersection(subautomatas = {subautomatas})"); +# +# n = len(subautomatas); +# +# mapping = {((0,) * n): 0}; # (indexes of subautomatas) -> index in automata +# +# todo = [((0, ) * n, 0)] +# +# automata = [()]; +# +# while todo: +# subindexes, index = todo.pop(0); +# +# accepting = int(all(subautomatas[i][x][0] for i, x in enumerate(subindexes))) +# +# newtos = [None, None]; +# +# for on, to in enumerate(zip(*(subautomatas[i][x][1] for i, x in enumerate(subindexes)))): +# if all(x is not None for x in to): +# if to in mapping: +# newtos[on] = mapping[to]; +# else: +# newto = len(automata); +# +# newtos[on] = newto; +# +# automata.append(()); +# +# mapping[to] = newto; +# +# todo.append((to, newto)); +# +# automata[index] = (accepting, newtos); +# +# if args.dump_automata: +# dump_automata(automata, title = f"mass-intersection: {len(automata)}"); +# +# return automata; + +def complement_automata(automata): + mapping = {0: 0}; # old index -> new index + + todo = [(0, 0)] + + new_automata = [()]; + + phiindex = None; + + while todo: + oldindex, newindex = todo.pop(0); + + oldaccepting, oldtos = automata[oldindex]; + + newaccepting = int(not oldaccepting); + + newtos = [None, None]; + + for on, oldto in enumerate(oldtos): + if oldto is not None: + if oldto in mapping: + newtos[on] = mapping[oldto]; + else: + newto = len(new_automata); + + newtos[on] = newto; + + new_automata.append(()); + + mapping[oldto] = newto; + + todo.append((oldto, newto)); + else: + if phiindex is None: + phiindex = len(new_automata); + + new_automata.append((1, (phiindex, phiindex))); + + newtos[on] = phiindex; + + new_automata[newindex] = (newaccepting, newtos); + + return new_automata; + +def simplify_automata(automata): + print(f"simplify_automata()"); + + n = len(automata); + + print(f"n = {n}"); + + same_as = {i: set(range(n)) for i in range(n)}; + + dep_on = dict(); # pair of two states [affects this] set of pairs of states + + todo = set() # pair of states whose difference we need to process + + print(f"simplify_automata: trivial differences"); + + for i, j in itertools.product(range(n), range(n)): + +# percent = (i * n + j) / (n * n) * 100; +# +# print(f"percent = {percent:.2f}%"); + + def is_different(): + iaccepting, itos = automata[i]; + jaccepting, jtos = automata[j]; + + if iaccepting != jaccepting: + return True; + + for x, y in zip(itos, jtos): + if (x is None) != (y is None): + return True; + + return False; + + if is_different(): + todo.add((i, j)); + else: + for dep in zip(automata[i][1], automata[j][1]): + if dep not in dep_on: + dep_on[dep] = set(); + + dep_on[dep].add((i, j)); + + print(f"simplify_automata: nontrivial differences"); + + x = 0; + + while todo: + print(f"simplify_automata: {x} of {x + len(todo)} ({x * 100 / (x + len(todo)):.2f}%)"); + + i, j = todo.pop(); + + same_as[i].discard(j); + same_as[j].discard(i); + + if (i, j) in dep_on: + todo.update(dep_on[(i, j)]); + + x += 1; + + print(f"simplify_automata: reachable"); + + # which states can even reach any accepting state? +# print(f"can_reach: start"); + can_reach = set(); + + dep_on = dict(); + + todo = set() + + for i in range(len(automata)): + if automata[i][0]: +# print(f"can_reach: accepting: {i}"); + todo.add(i); + else: + for to in automata[i][1]: + if to not in dep_on: + dep_on[to] = set(); + +# print(f"can_reach: {to} -> {i}"); + + dep_on[to].add(i); + + while todo: + i = todo.pop(); + +# print(f"can_reach: {i}"); + + can_reach.add(i); + + if i in dep_on: + todo.update(dep_on[i]); + + + print(f"simplify_automata: clone"); + + mapping = {0: 0}; # old index -> new index + + todo = [(0, 0)] + + new_automata = [()]; + + phiindex = None; + + while todo: + oldindex, newindex = todo.pop(0); + + accepting, oldtos = automata[oldindex]; + + newtos = [None, None]; + + for on, oldto in enumerate(oldtos): + if oldto is not None and oldto in can_reach: + oldto = min(same_as[oldto]); + + if oldto is not None: + if oldto in mapping: + newtos[on] = mapping[oldto]; + else: + newto = len(new_automata); + + newtos[on] = newto; + + new_automata.append(()); + + mapping[oldto] = newto; + + todo.append((oldto, newto)); + + new_automata[newindex] = (accepting, newtos); + + return new_automata; + +dump_id = 0; + +def dump_automata(automata, title = ""): + global dump_id; + + with open(f"{dump_id:05}.dot", "w") as stream: + stream.write(f""" + digraph {{ + rankdir = LR; + + label = "{title}" + + node [ + shape = circle + ]; + """); + + for i, x in enumerate(automata): + if x: + (accepting, (on0, on1)) = x; + + if accepting: + stream.write(f"{i} [ shape = doublecircle ];\n"); + + if on0 is not None: + stream.write(f"{i} -> {on0} [label = \"0\"];\n"); + + if on1 is not None: + stream.write(f"{i} -> {on1} [label = \"1\"];\n"); + + stream.write(""" + } + """); + + dump_id += 1; + +def build_automata(args, problem): + number_of_variables, clauses = problem; + + clause_automatas = list(); + + variable_lookup = dict(); + + for clause in clauses: + variable_automatas = list(); + + for variable, value in clause: + + if variable not in variable_lookup: + variable_lookup[variable] = len(variable_lookup); + + variable_index = variable_lookup[variable]; + + variable_automata = create_variable_automata( + variable_index, value, number_of_variables); + + if args.dump_automata: + title = f"{variable} ({variable_index}) = {value}" + + dump_automata(variable_automata, title); + + variable_automatas.append(variable_automata); + + clause_automata = mass_union(args, variable_automatas); + + clause_automata = simplify_automata(clause_automata); + + if args.dump_automata: + title = " or ".join(f"{a} = {b}" for a, b in clause); + + dump_automata(clause_automata, title); + + clause_automatas.append(clause_automata); + + automata = mass_intersection(args, clause_automatas); + + if args.dump_automata: + dump_automata(automata, "final"); + + automata = simplify_automata(automata); + + if args.dump_automata: + dump_automata(automata, "simplified: final"); + + return automata; + +def find_solutions(number_of_variables, automata): + # we have three cases: all, none, or some. + + def depth_first_search(automata): + def helper(prefix, stateindex): + accepting, tos = automata[stateindex]; + + if accepting and len(prefix) == number_of_variables: + yield prefix; + + if len(prefix) < number_of_variables: + for on, to in enumerate(tos): + if to is not None: + yield from helper(prefix = prefix + (on, ), stateindex = to); + + yield from helper(prefix = (), stateindex = 0); + + x = depth_first_search(complement_automata(automata)); + + if next(x, "all solutions") == "all solutions": + return "all solutions"; + + x = depth_first_search(automata); + + if next(x, "no solutions") == "no solutions": + return "no solutions"; + + for solution in depth_first_search(automata): + pretty_solution = ", ".join( + f"{v} = {s}" for v, s in enumerate(solution)); + + return pretty_solution; + +def do_valdation(automata, solution, number_of_variables): + assert(not "TODO"); + +def main(args): + problems = parse_file(args.input_file); + + for problem in problems: + print(f"problem = {problem}"); + + number_of_variables, _ = problem; + + automata = build_automata(args, problem); + + solution = find_solutions(number_of_variables, automata); + + if args.validate: + do_valdation(automata); + + solution = f"{solution} (validated.)"; + + print(solution); + +import sys; + +sys.exit(main(parse_args())); + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/makefile b/makefile new file mode 100644 index 0000000..c32cf9d --- /dev/null +++ b/makefile @@ -0,0 +1,69 @@ + +# vim: noexpandtab tabstop=4 : + +buildtype ?= release + +buildtype_options = buildtypes/${buildtype}.txt + +prefix = bin/${buildtype}-buildtype + +objs = $(patsubst %.cpp,${prefix}/%.o,$(srcs)) + +default: ${prefix}/sat-solver + +srclist.mk: + find -name '*.cpp' -! -path '*/junk/*' | sed 's/^/srcs += /' | sort -V > $@ + +include srclist.mk + +.PRECIOUS: %/ + +%/: + @mkdir -p $@ + +${prefix}/sat-solver: ${buildtype_options} ${objs} | ${prefix}/ + @echo "${buildtype}: linking ${@} ..." + @gcc @${buildtype_options} ${objs} -o $@ -lstdc++ -static-libasan + +${prefix}/%.o ${prefix}/%.d: %.cpp ${buildtype_options} | ${prefix}/%/ + @echo "${buildtype}: compiling ${*}.cpp ..." + @gcc -c @${buildtype_options} $< -MD -MF ${prefix}/${*}.d -o ${prefix}/${*}.o + +#args += -d +args += -v + +#args += -i ./inputs/0.txt +#args += -i ./inputs/1.txt +#args += -i ./inputs/2.txt +args += -i ./inputs/3.txt +#args += -i ./inputs/all.txt +#args += -i ./inputs/none.txt + +run: ${prefix}/sat-solver + ${env} $< ${args} + +gdbrun: ${prefix}/sat-solver + gdb --args $< ${args} + +valrun: ${prefix}/sat-solver + valgrind --gen-suppressions=yes -- $< ${args} + +valrun-leak: ${prefix}/sat-solver + valgrind --leak-check=full --gen-suppressions=yes -- $< ${args} + +include $(patsubst %.cpp,${prefix}/%.d,$(srcs)) + + + + + + + + + + + + + + + diff --git a/parse.cpp b/parse.cpp new file mode 100644 index 0000000..288641b --- /dev/null +++ b/parse.cpp @@ -0,0 +1,114 @@ + +#include +#include + +#include +#include +#include +#include +#include + +refcounted>> parse(const char* path) +{ + refcounted>> problems = new list>(); + + FILE* stream = fopen(path, "r"); + + char *line = NULL; + size_t len = 0; + ssize_t nread; + + while ((nread = getline(&line, &len, stream)) > 0) + { + line[--nread] = 0; + + if (line[0] == '\0') continue; + if (line[0] == 'c') continue; + + if (line[0] != 'p') + { + assert(!"TODO"); + exit(1); + } + + unsigned number_of_variables; + unsigned number_of_clauses; + + int r = sscanf(line, " p %u %u ", &number_of_variables, &number_of_clauses); + + if (r < 2) + { + puts("syntax error"); + exit(1); + } + + refcounted p = new problem(number_of_variables); + + for (unsigned i = 0; i < number_of_clauses; i++) + { + nread = getline(&line, &len, stream); + + if (nread < 0) + { + puts("syntax error"); + exit(1); + } + + line[--nread] = 0; + + refcounted c = new clause(); + + char *moving = line; + + for (char* word; (word = strtok_r(NULL, " ", &moving)); ) + { + errno = 0; + + char* m; + + signed variable = strtol(word, &m, 10); + + if (errno || *m) + { + puts("syntax error"); + exit(1); + } + + bool value = true; + + if (variable < 0) + { + variable = -variable; + value = !value; + } + + assert(variable > 0); + + c->bundles.append( + (clause::bundle) {(unsigned) variable, value}); + } + + p->clauses.append(c); + } + + problems->append(p); + } + + free(line); + + fclose(stream); + + return problems; +} + + + + + + + + + + + + diff --git a/parse.hpp b/parse.hpp new file mode 100644 index 0000000..8bfd2ff --- /dev/null +++ b/parse.hpp @@ -0,0 +1,7 @@ + +#include + +#include + +refcounted>> parse(const char* path); + diff --git a/print.cpp b/print.cpp new file mode 100644 index 0000000..c6bb2f8 --- /dev/null +++ b/print.cpp @@ -0,0 +1,74 @@ + +#include + +template <> void print(const bool b) +{ + printf("%s", b ? "true" : "false"); +} + +template <> void print(char* x) +{ + printf("%s", x); +} + +template <> void print(const char* x) +{ + printf("%s", x); +} + +template <> void print(const char x) +{ + printf("%c", x); +} + +template <> void print(const signed char x) +{ + printf("%hhi", x); +} + +template <> void print(const unsigned char x) +{ + printf("%hhuU", x); +} + +template <> void print(const signed short x) +{ + printf("%hi", x); +} + +template <> void print(const unsigned short x) +{ + printf("%huU", x); +} + +template <> void print(const signed int x) +{ + printf("%i", x); +} + +template <> void print(const unsigned int x) +{ + printf("%uU", x); +} + +template <> void print(const signed long x) +{ + printf("%liL", x); +} + +template <> void print(const unsigned long x) +{ + printf("%luUL", x); +} + +template <> void print(const float x) +{ + printf("%gf", x); +} + +template <> void print(const double x) +{ + printf("%lf", x); +} + + diff --git a/print.hpp b/print.hpp new file mode 100644 index 0000000..e1c3fe1 --- /dev/null +++ b/print.hpp @@ -0,0 +1,45 @@ + + +#include + +template void print(const T t); + +template <> void print(const bool b); + +template <> void print(char* x); + +template <> void print(const char* x); + +template <> void print(const char x); + +template <> void print(const signed char x); + +template <> void print(const unsigned char x); + +template <> void print(const signed short x); + +template <> void print(const unsigned short x); + +template <> void print(const signed int x); + +template <> void print(const unsigned int x); + +template <> void print(const signed long x); + +template <> void print(const unsigned long x); + +template <> void print(const float x); + +template <> void print(const double x); + +template void print(const F& f, const R&... r) +{ + print(f), print(r ...), puts(""); +} + +template void println(const T&... t) +{ + print(t ...); +} + + diff --git a/problem.cpp b/problem.cpp new file mode 100644 index 0000000..4b6c373 --- /dev/null +++ b/problem.cpp @@ -0,0 +1,11 @@ + +#include + +problem::problem( + unsigned number_of_variables_): + number_of_variables(number_of_variables_) +{ + ; +} + + diff --git a/problem.hpp b/problem.hpp new file mode 100644 index 0000000..7b4838a --- /dev/null +++ b/problem.hpp @@ -0,0 +1,34 @@ + +#ifndef CLASS_PROBLEM +#define CLASS_PROBLEM + +#include + +#include + +class clause +{ + public: + struct bundle + { + unsigned variable; + + bool value; + }; + + public: + list bundles; +}; + +class problem +{ + public: + unsigned number_of_variables; + + list> clauses; + + public: + problem(unsigned); +}; + +#endif diff --git a/quack.hpp b/quack.hpp new file mode 100644 index 0000000..5da4e2b --- /dev/null +++ b/quack.hpp @@ -0,0 +1,128 @@ + +#include +#include + +#include +#include + +template < + typename T> class quack +{ + public: + T* data = NULL; + size_t i = 0, n = 0, cap = 0; + + private: + void helper() + { + ; + } + + template + void helper(first f, rest... r) + { + append(f); + + helper(r...); + } + + public: + quack() + { + ; + } + + template + quack(all... a) + { + helper(a...); + } + + void append(T item) + { + if (n == cap) + { + cap = cap << 1 ?: 1; + + if constexpr (std::is_trivially_copyable_v) + { + data = (T*) realloc(data, sizeof(*data) * cap); + + if (i) + { + memmove( + /* dest: */ data + cap - (n - i), + /* src: */ data + i, + /* len: */ (n - i) * sizeof(T)); + + i = cap - (n - i); + } + } + else + { + if (i) + { + assert(!"TODO"); + } + else + { + T* new_data = new T[cap](); + + for (size_t i = 0; i < n; i++) + { + new_data[i] = std::move(data[i]); + } + + delete[] data; + + data = new_data; + } + } + } + + data[(i + n++) % cap] = std::move(item); + } + + T pop() + { + assert(n); + + assert(i < cap); + + T retval = data[i]; + + if (i + 1 == cap) + i = 0; + else + i++; + + n--; + + return retval; + } + + ~quack() + { + if (std::is_trivially_copyable_v) + { + free(data); + } + else + { + delete[] data; + } + } +}; + + + + + + + + + + + + + diff --git a/refcounted.hpp b/refcounted.hpp new file mode 100644 index 0000000..493052b --- /dev/null +++ b/refcounted.hpp @@ -0,0 +1,139 @@ + + +#ifndef CLASS_REFCOUNT +#define CLASS_REFCOUNT + +template class refcounted +{ + T* ptr; + size_t* refcount; + + public: + refcounted() + { + ptr = NULL, refcount = NULL; + } + + refcounted(T* _ptr) + { + ptr = _ptr; + + refcount = new size_t(1); + } + + refcounted(const refcounted& other): + ptr(other.ptr), + refcount(other.refcount) + { + VALGRIND_CHECK_VALUE_IS_DEFINED(other.ptr); + VALGRIND_CHECK_VALUE_IS_DEFINED(other.refcount); + + if (refcount) + { + (*refcount)++; + } + } + + refcounted(refcounted&& other) noexcept : + ptr(std::move(other.ptr)), + refcount(std::move(other.refcount)) + { + ; + } + + auto begin() + { + return ptr->begin(); + } + + auto end() + { + return ptr->end(); + } + + auto begin() const + { + return ptr->begin(); + } + + auto end() const + { + return ptr->end(); + } + + operator bool() const + { + return !!ptr; + } + + const T operator*() const + { + return *ptr; + } + + T* operator->() + { + return ptr; + } + + const T* operator->() const + { + return ptr; + } + + auto operator <=> (const struct refcounted& other) const + { + return (*(const T*) ptr <=> **other); + } + + refcounted& operator=(const refcounted& other) + { + if (ptr) + { + assert(refcount); + + if (!--*refcount) + { + // decrement the old refcount, possibly free old ptr + assert(!"TODO"); + } + } + + ptr = other.ptr; + + refcount = other.refcount; + + if (refcount) + { + (*refcount)++; + } + + return *this; + } + + ~refcounted() + { + if (refcount) + { + if (!--*refcount) + { + delete ptr; + + delete refcount; + } + } + } +}; + +#endif + + + + + + + + + + + diff --git a/set.hpp b/set.hpp new file mode 100644 index 0000000..1e7e93c --- /dev/null +++ b/set.hpp @@ -0,0 +1,173 @@ + +#ifndef CLASS_SET +#define CLASS_SET + +#include "avl.hpp" + +template class set +{ + private: + struct avl_tree_t tree; + + private: + void helper() + { + ; + } + + template + void helper(first f, rest... r) + { + add(f); + + helper(r...); + } + + public: + set() + { + ; + } + + set(const set& other) + { + update(other); + } + + public: + template + set(all... a) + { + helper(a...); + } + + template + set(iterator_t a) + { + for (auto &x: a) + { + add(x); + } + } + + bool add(T element) + { + return !!tree.insert(element); + } + + bool discard(T element) + { + return tree.delete_item(element); + } + + bool update(const set& other) + { + // ENTER; + + bool are_any_new = false; + + for (auto & element : other) + { + if (this->add(element)) + { + are_any_new = true; + } + } + + // EXIT; + return are_any_new; + } + + operator bool() const + { + return !!tree.head; + } + + bool is_nonempty() const + { + return !!tree.head; + } + + int operator <=> (const set& other) const + { + // ENTER; + + int cmp = 0; + + auto node_a = this->tree.head, node_b = other.tree.head; + + for (; !cmp && node_a && node_b; + node_a = node_a->next, node_b = node_b->next) + { + auto c = node_a->item <=> node_b->item; + + if (c > 0) + cmp = 1; + else if (c < 0) + cmp = -1; + } + + if (!cmp) + { + if (node_a) + { + cmp = +1; + } + else if (node_b) + { + cmp = -1; + } + } + + // dpvi(cmp); + + // EXIT; + return cmp; + } + + T min() const + { + assert(tree.head); + + return tree.head->item; + } + + bool operator == (const set& other) const + { + return ((*this) <=> (other)) == 0; + } + + avl_tree_t::iterable begin() const + { + return tree.begin(); + } + + avl_tree_t::iterable end() const + { + return tree.end(); + } + + ~set() + { + ; + } +}; + + + + + + + + + + + + + + + + + + +#endif diff --git a/srclist.mk b/srclist.mk new file mode 100644 index 0000000..b4cafb7 --- /dev/null +++ b/srclist.mk @@ -0,0 +1,8 @@ +srcs += ./automata.cpp +srcs += ./build_automata.cpp +srcs += ./cmdln_flags.cpp +srcs += ./find_solutions.cpp +srcs += ./main.cpp +srcs += ./parse.cpp +srcs += ./print.cpp +srcs += ./problem.cpp diff --git a/tuple.hpp b/tuple.hpp new file mode 100644 index 0000000..a9d12a4 --- /dev/null +++ b/tuple.hpp @@ -0,0 +1,206 @@ + +#ifndef CLASS_TUPLE +#define CLASS_TUPLE + +#include + +namespace std +{ + template + struct tuple_size; + +// template +// struct tuple_element; + + template + struct tuple_element; + +}; + +static constexpr int maximum(int a, int b) +{ + if (a > b) + return a; + return b; +} + +template + struct ArgType + { + using type = + typename std::conditional< + index == 0, + A, + typename ArgType::type>::type; + }; + +template + struct ArgType<0, T> + { + using type = T; + }; + +template + class tuple + { + public: + struct empty + { + auto operator <=> (const empty& other __attribute__((unused))) const + { + return 0; + } + }; + + template + struct elements_t + { + static const size_t index = _index; + + M car; + + typename std::conditional< + sizeof...(Es) == 0, + empty, + elements_t<_index + 1, Es...>>::type cdr; + + elements_t() + { + ; + } + + elements_t(M m, Es... e): + car(m), cdr(e...) + { + ; + } + + int operator <=> (const elements_t& other) const + { + auto car_res = (car <=> other.car); + + if (car_res > 0) + return 1; + if (car_res < 0) + return -1; + + auto cdr_res = (cdr <=> other.cdr); + + if (cdr_res > 0) + return 1; + if (cdr_res < 0) + return -1; + + return 0; + } + }; + + public: + elements_t<0, Ts...> elements; + + public: + tuple() + { + ; + } + + tuple(Ts... _elements): + elements(_elements...) + { + ; + } + + private: + template + R& helper(T& holder) + { + if constexpr(T::index == index) + return holder.car; + else + return helper(holder.cdr); + }; + + public: + template + ArgType::type& get() + { + return helper::type>(elements); + } + + auto first() + { + return this->get<0>(); + } + + auto second() + { + return this->get<1>(); + } + + int operator <=> (const tuple& other) const + { + return elements <=> other.elements; + } + + ~tuple() + { + ; + } + }; + + +template + struct std::tuple_size> + { + static constexpr size_t value = sizeof...(Ts); + }; + +template + struct std::tuple_element<0, std::tuple> + { + using type = car; + }; + +template + struct std::tuple_element>: + std::tuple_element> + { + }; + +template + struct std::tuple_element<0, tuple> + { + using type = car; + }; + +template + struct std::tuple_element>: + std::tuple_element> + { + }; + + + + + + + + + + + + + + + + + + + + + + + +#endif + +