first commit

automata.cpp

@@ -0,0 +1,555 @@
+
+#include <string.h>
+#include <stdarg.h>
+#include <limits.h>
+
+#include <quack.hpp>
+#include <heap.hpp>
+#include <set.hpp>
+#include <print.hpp>
+#include <automata.hpp>
+#include <tuple.hpp>
+#include <dict.hpp>
+
+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<automata*> todo;
+    
+    set<automata*> 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<const automata*, automata*> mapping;
+    
+    struct automata* start = new automata();
+    
+    struct automata* phi = NULL;
+    
+    quack<decltype(mapping)::keyvalue_pair*> 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<tuple<const automata*, const automata*>, automata*> mapping;
+    
+    size_t total_number_of_states = 0;
+    
+    struct automata* start = new automata();
+    
+    total_number_of_states++;
+    
+    quack<decltype(mapping)::keyvalue_pair*> 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<tuple<const automata*, const automata*>, automata*> mapping;
+    
+    size_t total_number_of_states = 0;
+    
+    struct automata* start = new automata();
+    
+    total_number_of_states++;
+    
+    quack<decltype(mapping)::keyvalue_pair*> 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<const automata*> universe;
+	{
+	    quack<const automata*> 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<const automata*, const automata*> pair_t;
+    
+    dict<pair_t, set<pair_t>> dependent_of;
+    
+    heap<tuple<unsigned /* hopcount */, pair_t>> 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<pair_t>());
+                        }
+
+                        dependent_of[tuple(a_to, b_to)].add(tuple(a, b));
+                    }
+                }
+                
+                if (are_different)
+                {
+                    todo.push(tuple(0U, tuple(a, b)));
+                }
+            }
+        }
+    }
+    
+    dict<const automata*, set<const automata*>> same_as;
+    
+    for (const automata* state: universe)
+    {
+        same_as.add(state, set<const automata*>(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<const automata*, automata*> mapping;
+        
+        quack<decltype(mapping)::keyvalue_pair*> 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<automata*> queued;
+    
+    quack<automata*> 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;
+    }
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

automata.hpp

@@ -0,0 +1,49 @@
+
+#ifndef STRUCT_AUTOMATA
+#define STRUCT_AUTOMATA
+
+#include <cmdln_flags.hpp>
+
+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
+
+

avl.hpp

@@ -0,0 +1,625 @@
+
+#ifndef CLASS_AVL_TREE_T
+#define CLASS_AVL_TREE_T
+
+#include <stddef.h>
+#include <errno.h>
+
+/* 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

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);
+    
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

build_automata.cpp

@@ -0,0 +1,136 @@
+
+#include <dict.hpp>
+
+#include <print.hpp>
+
+#include <build_automata.hpp>
+
+automata* build_automata(
+    cmdln_flags& flags,
+    refcounted<problem> 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;
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

build_automata.hpp

@@ -0,0 +1,11 @@
+
+#include <automata.hpp>
+
+#include <problem.hpp>
+
+#include <cmdln_flags.hpp>
+
+automata* build_automata(
+    cmdln_flags& flags,
+    refcounted<problem> p);
+

buildtypes/debug.txt

@@ -0,0 +1,13 @@
+
+-fsanitize=undefined
+-fsanitize=address
+
+-std=c++20
+
+-I .
+
+-D DEBUG_BUILD
+
+-g
+
+-Wall -Werror -Wextra -Wfatal-errors

buildtypes/release.txt

@@ -0,0 +1,12 @@
+
+-O3
+
+-std=c++20
+
+-I .
+
+-D TEST_BUILD
+
+-g
+
+-Wall -Werror -Wextra -Wfatal-errors

buildtypes/test.txt

@@ -0,0 +1,10 @@
+
+-std=c++20
+
+-I .
+
+-D TEST_BUILD
+
+-g
+
+-Wall -Werror -Wextra -Wfatal-errors

cmdln_flags.cpp

@@ -0,0 +1,57 @@
+
+#include <unistd.h>
+#include <getopt.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+#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);
+    }
+}
+
+
+
+
+
+
+
+
+
+
+

cmdln_flags.hpp

@@ -0,0 +1,20 @@
+
+#ifndef CLASS_CMDLN_FLAGS
+#define CLASS_CMDLN_FLAGS
+
+#include <stddef.h>
+
+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

dict.hpp

@@ -0,0 +1,145 @@
+
+#ifndef CLASS_DICT
+#define CLASS_DICT
+
+#include <stdio.h>
+#include <stdlib.h>
+
+#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<keyvalue_pair> tree;
+    
+    public:
+        avl_tree_t<keyvalue_pair>::iterable begin()
+        {
+            return tree.begin();
+        }
+        
+        avl_tree_t<keyvalue_pair>::iterable end()
+        {
+            return tree.end();
+        }
+    
+        avl_tree_t<keyvalue_pair>::iterable begin() const
+        {
+            return tree.begin();
+        }
+        
+        avl_tree_t<keyvalue_pair>::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

find_solutions.cpp

@@ -0,0 +1,106 @@
+
+#include <assert.h>
+#include <stdio.h>
+
+#include <automata.hpp>
+
+#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;
+    }
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

find_solutions.hpp

@@ -0,0 +1,7 @@
+
+struct automata;
+
+void find_solutions(
+    unsigned number_of_variables,
+    const struct automata* start);
+

heap.hpp

@@ -0,0 +1,127 @@
+
+template <typename T> 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<T>)
+                {
+                    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<T>)
+            {
+                free(data);
+            }
+            else
+            {
+                delete[] data;
+            }
+        }
+};
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

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

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

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
+
+

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
+
+

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.
+
+

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.
+

list.hpp

@@ -0,0 +1,210 @@
+
+#ifndef CLASS_LIST
+#define CLASS_LIST
+
+#include <stddef.h>
+#include <assert.h>
+#include <stdlib.h>
+
+#include <valgrind/memcheck.h>
+
+#include <type_traits>
+#include <new>
+#include <utility>
+
+template<typename T> 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<T>)
+            {
+                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<T>)
+            {
+                free(data);
+            }
+            else
+            {
+                delete[] data;
+            }
+        }
+};
+
+#endif
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

main.cpp

@@ -0,0 +1,45 @@
+
+#include <cmdln_flags.hpp>
+
+#include <parse.hpp>
+
+#include <build_automata.hpp>
+
+#include <automata.hpp>
+
+#include <find_solutions.hpp>
+
+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;
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

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()));
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

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))
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

parse.cpp

@@ -0,0 +1,114 @@
+
+#include <errno.h>
+#include <string.h>
+
+#include <parse.hpp>
+#include <problem.hpp>
+#include <list.hpp>
+#include <refcounted.hpp>
+#include <print.hpp>
+
+refcounted<list<refcounted<problem>>> parse(const char* path)
+{
+    refcounted<list<refcounted<problem>>> problems = new list<refcounted<problem>>();
+    
+    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<problem> 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<clause> 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;
+}
+
+
+
+
+
+
+
+
+
+
+
+

parse.hpp

@@ -0,0 +1,7 @@
+
+#include <list.hpp>
+
+#include <problem.hpp>
+
+refcounted<list<refcounted<problem>>> parse(const char* path);
+

print.cpp

@@ -0,0 +1,74 @@
+
+#include <print.hpp>
+
+template <> void print<bool>(const bool b)
+{
+    printf("%s", b ? "true" : "false");
+}
+
+template <> void print<char*>(char* x)
+{
+    printf("%s", x);
+}
+
+template <> void print<const char*>(const char* x)
+{
+    printf("%s", x);
+}
+
+template <> void print<char>(const char x)
+{
+    printf("%c", x);
+}
+
+template <> void print<signed char>(const signed char x)
+{
+    printf("%hhi", x);
+}
+
+template <> void print<unsigned char>(const unsigned char x)
+{
+    printf("%hhuU", x);
+}
+
+template <> void print<signed short>(const signed short x)
+{
+    printf("%hi", x);
+}
+
+template <> void print<unsigned short>(const unsigned short x)
+{
+    printf("%huU", x);
+}
+
+template <> void print<signed int>(const signed int x)
+{
+    printf("%i", x);
+}
+
+template <> void print<unsigned int>(const unsigned int x)
+{
+    printf("%uU", x);
+}
+
+template <> void print<signed long>(const signed long x)
+{
+    printf("%liL", x);
+}
+
+template <> void print<unsigned long>(const unsigned long x)
+{
+    printf("%luUL", x);
+}
+
+template <> void print<float>(const float x)
+{
+    printf("%gf", x);
+}
+
+template <> void print<double>(const double x)
+{
+    printf("%lf", x);
+}
+
+

print.hpp

@@ -0,0 +1,45 @@
+
+
+#include <stdio.h>
+
+template <typename T> void print(const T t);
+
+template <> void print<bool>(const bool b);
+
+template <> void print<char*>(char* x);
+
+template <> void print<const char*>(const char* x);
+
+template <> void print<char>(const char x);
+
+template <> void print<signed char>(const signed char x);
+
+template <> void print<unsigned char>(const unsigned char x);
+
+template <> void print<signed short>(const signed short x);
+
+template <> void print<unsigned short>(const unsigned short x);
+
+template <> void print<signed int>(const signed int x);
+
+template <> void print<unsigned int>(const unsigned int x);
+
+template <> void print<signed long>(const signed long x);
+
+template <> void print<unsigned long>(const unsigned long x);
+
+template <> void print<float>(const float x);
+
+template <> void print<double>(const double x);
+
+template <typename F, typename ...R> void print(const F& f, const R&... r)
+{
+    print(f), print(r ...), puts("");
+}
+
+template <typename ...T> void println(const T&... t)
+{
+    print(t ...);
+}
+
+

problem.cpp

@@ -0,0 +1,11 @@
+
+#include <problem.hpp>
+
+problem::problem(
+    unsigned number_of_variables_):
+        number_of_variables(number_of_variables_)
+{
+    ;
+}
+
+

problem.hpp

@@ -0,0 +1,34 @@
+
+#ifndef CLASS_PROBLEM
+#define CLASS_PROBLEM
+
+#include <list.hpp>
+
+#include <refcounted.hpp>
+
+class clause
+{
+    public:
+        struct bundle
+        {
+            unsigned variable;
+            
+            bool value;
+        };
+    
+    public:
+        list<bundle> bundles;
+};
+
+class problem
+{
+    public:
+        unsigned number_of_variables;
+        
+        list<refcounted<clause>> clauses;
+        
+    public:
+        problem(unsigned);
+};
+
+#endif

quack.hpp

@@ -0,0 +1,128 @@
+
+#include <stddef.h>
+#include <assert.h>
+
+#include <type_traits>
+#include <utility>
+
+template <
+    typename T> class quack
+{
+    public:
+        T* data = NULL;
+        size_t i = 0, n = 0, cap = 0;
+    
+    private:
+        void helper()
+        {
+            ;
+        }
+        
+        template <typename first, typename ...rest>
+            void helper(first f, rest... r)
+            {
+                append(f);
+                
+                helper(r...);
+            }
+    
+    public:
+        quack()
+        {
+            ;
+        }
+        
+        template <typename ...all>
+            quack(all... a)
+            {
+                helper(a...);
+            }
+        
+        void append(T item)
+        {
+            if (n == cap)
+            {
+                cap = cap << 1 ?: 1;
+                
+                if constexpr (std::is_trivially_copyable_v<T>)
+                {
+                    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<T>)
+            {
+                free(data);
+            }
+            else
+            {
+                delete[] data;
+            }
+        }
+};
+
+
+
+
+
+
+
+
+
+
+
+
+

refcounted.hpp

@@ -0,0 +1,139 @@
+
+
+#ifndef CLASS_REFCOUNT
+#define CLASS_REFCOUNT
+
+template<typename T> 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
+
+
+
+
+
+
+
+
+
+
+

set.hpp

@@ -0,0 +1,173 @@
+
+#ifndef CLASS_SET
+#define CLASS_SET
+
+#include "avl.hpp"
+
+template<typename T> class set
+{
+    private:
+        struct avl_tree_t<T> tree;
+    
+    private:
+        void helper()
+        {
+            ;
+        }
+        
+        template <typename first, typename ...rest>
+            void helper(first f, rest... r)
+            {
+                add(f);
+                
+                helper(r...);
+            }
+    
+    public:
+        set()
+        {
+            ;
+        }
+        
+        set(const set& other)
+        {
+            update(other);
+        }
+        
+    public:
+        template <typename ...all>
+            set(all... a)
+            {
+                helper(a...);
+            }
+        
+        template <typename iterator_t>
+            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<T>::iterable begin() const
+        {
+            return tree.begin();
+        }
+        
+        avl_tree_t<T>::iterable end() const
+        {
+            return tree.end();
+        }
+        
+        ~set()
+        {
+            ;
+        }
+};
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#endif

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

tuple.hpp

@@ -0,0 +1,206 @@
+
+#ifndef CLASS_TUPLE
+#define CLASS_TUPLE
+
+#include <type_traits>
+
+namespace std
+{
+    template<class T>
+        struct tuple_size;
+
+//    template<std::size_t I, class... Types>
+//        struct tuple_element;
+    
+    template<size_t __i, typename _Tp>
+        struct tuple_element;
+    
+};
+
+static constexpr int maximum(int a, int b)
+{
+    if (a > b)
+        return a;
+    return b;
+}
+
+template<int index, typename A = void, typename... Args>
+    struct ArgType
+    {
+        using type =
+            typename std::conditional<
+                index == 0,
+                A,
+                typename ArgType<maximum(index - 1, 0), Args...>::type>::type;
+    };
+
+template<typename T>
+    struct ArgType<0, T>
+    {
+        using type = T;
+    };
+
+template<typename... Ts>
+    class tuple
+    {
+        public:
+            struct empty
+            {
+                auto operator <=> (const empty& other __attribute__((unused))) const
+                {
+                    return 0;
+                }
+            };
+            
+            template <size_t _index, typename M = void, typename... Es>
+                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<size_t index, typename R, typename T>
+                R& helper(T& holder)
+                {
+                    if constexpr(T::index == index)
+                        return holder.car;
+                    else
+                        return helper<index, R>(holder.cdr);
+                };
+        
+        public:
+            template<size_t index>
+                ArgType<index, Ts...>::type& get()
+                {
+                    return helper<index, typename ArgType<index, Ts...>::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<typename... Ts>
+    struct std::tuple_size<tuple<Ts ...>>
+    {
+        static constexpr size_t value = sizeof...(Ts);
+    };
+
+template<class car, class... cdr>
+    struct std::tuple_element<0, std::tuple<car, cdr ...>>
+    {
+        using type = car;
+    };
+
+template<std::size_t I, class car, class... cdr>
+    struct std::tuple_element<I, std::tuple<car, cdr ...>>:
+        std::tuple_element<I - 1, std::tuple<cdr ...>>
+    {
+    };
+
+template<class car, class... cdr>
+    struct std::tuple_element<0, tuple<car, cdr ...>>
+    {
+        using type = car;
+    };
+
+template<std::size_t I, class car, class... cdr>
+    struct std::tuple_element<I, tuple<car, cdr ...>>:
+        std::tuple_element<I - 1, tuple<cdr ...>>
+    {
+    };
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+#endif
+
+