4-variable-simplifier/calculate_simplifications.c

#include <unistd.h>
#include <stdio.h>
#include <limits.h>
#include <assert.h>
#include <stdbool.h>

#include <debug.h>

#include <cmdln.h>

#include <print.h>

#ifdef MULTITHREADED_BUILD
#include <pthread.h>
#endif

#include "calculate_simplifications.h"

void helper(
    const struct cmdln_flags* flags,
    struct simplifications* simps,
    bool have_extra_variable,
    uint16_t A)
{
    ENTER;
    
    struct row* row = have_extra_variable ? &simps->with_vars[A] : &simps->main;
    
    // init 'row->data':
    {
        for (int i = 0; i < N; i++)
        {
            row->data[i].kind = ek_unreachable;
            
            row->data[i].cost = INT_MAX;
        }
    }
    
    // heap of truthtables; key = cost
    struct {
        uint16_t data[N];
        int n;
        
        // truthtable -> index in 'todo'
        int reverse[N];
    } todo;
    
    // init 'todo':
    {
        todo.n = 0;
        
        for (int i = 0; i < N; i++)
        {
            todo.reverse[i] = -1;
        }
    }
    
    uint16_t pop(void)
    {
        assert(todo.n > 0);

        uint16_t retval = todo.data[0];

        todo.reverse[retval] = -1;

        uint16_t moving = todo.data[todo.n-- - 1];

        int cost = row->data[moving].cost;

        int index = 0;

        again:
        {
            int left = index * 2 + 1;
            int right = index * 2 + 2;

            uint16_t smallest = moving;

            if (left < todo.n && row->data[todo.data[left]].cost < cost)
                smallest = todo.data[left];

            if (right < todo.n && row->data[todo.data[right]].cost < row->data[smallest].cost)
                smallest = todo.data[right];

            if (smallest == moving)
            {
                todo.data[index] = moving;

                todo.reverse[moving] = index;
            }
            else
            {
                int new = todo.reverse[smallest];

                todo.data[index] = smallest;

                todo.reverse[smallest] = index;

                index = new;

                goto again;
            }
        }

        return retval;
    }

    void append(uint16_t truthtable, int cost)
    {
        assert(todo.reverse[truthtable] == -1);

        int index = todo.n++, new_index;

        while (index > 0 && row->data[todo.data[new_index = (index - 1) / 2]].cost > cost)
        {
            todo.data[index] = todo.data[new_index];

            todo.reverse[todo.data[new_index]] = index;

            index = new_index;
        }
        
        todo.data[index] = truthtable;
        
        todo.reverse[truthtable] = index;
        
        row->data[truthtable].cost = cost;
    }

    void update(uint16_t truthtable, int cost)
    {
        assert(todo.reverse[truthtable] != -1);

        assert(cost < row->data[truthtable].cost);

        int index =todo. reverse[truthtable], new_index;

        while (index > 0 && row->data[todo.data[new_index = (index - 1) / 2]].cost > cost)
        {
            todo.data[index] = todo.data[new_index];

            todo.reverse[todo.data[new_index]] = index;

            index = new_index;
        }

        todo.data[index] = truthtable;
        todo.reverse[truthtable] = index;

        row->data[truthtable].cost = cost;
    }
    
    // create a list of the "done" truthtables
    struct {
        int headtails[N], next[N], head;
        
        // for debugging:
        #if ZDEBUG
        bool in[N];
        #endif
    } done = {};
    
    // init 'done':
    {
        done.head = -1;
        
        for (int i = 0; i < N; i++)
        {
            done.headtails[i] = -1;
            
            #if ZDEBUG
            done.in[i] = false;
            #endif
        }
    }
    
    void insert(int index)
    {
        #if ZDEBUG
        assert(!done.in[index]);
        #endif
        
        int head = index & 1 ? index & ~(index & -index) : index, prevhead = -1;
        
        while (done.headtails[head] == -1 || index < done.headtails[head])
        {
            done.headtails[head] = index;
            
            prevhead = head, head = head & ~(head & -head);
        }
        
        if (done.headtails[head] < index)
        {
            if (prevhead == -1)
            {
                assert(done.headtails[head] == head);
                
                done.next[head] = index;
            }
            else
            {
                int tophalftail = done.headtails[prevhead - 1];
                
                assert(tophalftail != -1);
                
                done.next[tophalftail] = index;
            }
        }
        else
        {
            done.head = index;
        }
        
        int n = ~index & M;
        int tail = index & 1 ? index : index | (n & -n), prevtail = -1;
        
        while (done.headtails[tail] == -1 || done.headtails[tail] < index)
        {
            done.headtails[tail] = index;
            
            prevtail = tail, tail = tail | (n = ~tail & M, n & -n);
        }
        
        if (index < done.headtails[tail])
        {
            if (prevtail == -1)
            {
                assert(done.headtails[tail] == tail);
                
                #if ZDEBUG
                assert(done.in[tail]);
                #endif
                
                done.next[index] = tail;
            }
            else
            {
                int bottomhalfhead = done.headtails[prevtail + 1];
                
                assert(bottomhalfhead != -1);
                
                done.next[index] = bottomhalfhead;
            }
        }
        else
        {
            done.next[index] = -1;
        }
        
        #if ZDEBUG
        done.in[index] = true;
        #endif
    }
    
    append(W, 0), row->data[W].kind = ek_W;
    append(X, 0), row->data[X].kind = ek_X;
    append(Y, 0), row->data[Y].kind = ek_Y;
    append(Z, 0), row->data[Z].kind = ek_Z;
    
    append(0, 1), row->data[0].kind = ek_0;
    append(M, 1), row->data[M].kind = ek_1;
    
    if (have_extra_variable && todo.reverse[A] == -1)
    {
        append(A, 0), row->data[A].kind = ek_A;
    }
    
    // disable terminal autowrap:
    if (!ZDEBUG && flags->verbose && flags->print_with_color)
    {
        printf("\e[?7l");
    }

    for (int iterations = 1; todo.n && iterations <= N; iterations++)
    {
        uint16_t truthtable = pop();
        
        insert(truthtable);
        
        int cost = row->data[truthtable].cost;

        if (flags->verbose)
        {
            if (!ZDEBUG && flags->print_with_color)
            {
                printf("\e[2K");
            }

            printf("%i of %i (%.2f%%): [%i] ",
                iterations, N, (100.0 * iterations / N), cost);

            if (have_extra_variable)
            {
                printf("a = 0b%016b, ", A);
            }
            
            print(flags, simps, row, truthtable);
            
            puts("");

            if (!ZDEBUG && flags->print_with_color)
            {
                printf("\e[1A");
            }
        }

        // consider NOT:
        if (flags->use_operators.not)
        {
            uint16_t not_truthtable = ~truthtable & M;

            int not_cost = cost + 1;

            if (not_cost < row->data[not_truthtable].cost)
            {
                if (todo.reverse[not_truthtable] == -1)
                {
                    append(not_truthtable, not_cost);
                }
                else
                {
                    update(not_truthtable, not_cost);
                }

                row->data[not_truthtable].kind = ek_not;
                row->data[not_truthtable].left = truthtable;
            }
        }

        #define BINARY_OPERATOR(ekind, function) \
        { \
            for (int i = done.head; i != -1; i = done.next[i]) \
            { \
                { \
                    uint16_t bin_truthtable = function(truthtable, i) & M; \
                     \
                    int bin_cost = 1 + cost + row->data[i].cost; \
                     \
                    if (bin_cost < row->data[bin_truthtable].cost) \
                    { \
                        if (todo.reverse[bin_truthtable] == -1) \
                            append(bin_truthtable, bin_cost); \
                        else \
                            update(bin_truthtable, bin_cost); \
                         \
                        row->data[bin_truthtable].kind = ekind; \
                        row->data[bin_truthtable].left = truthtable; \
                        row->data[bin_truthtable].right = i; \
                    } \
                } \
                \
                { \
                    uint16_t bin_truthtable = function(i, truthtable) & M; \
                     \
                    int bin_cost = 1 + cost + row->data[i].cost; \
                     \
                    if (bin_cost < row->data[bin_truthtable].cost) \
                    { \
                        if (todo.reverse[bin_truthtable] == -1) \
                            append(bin_truthtable, bin_cost); \
                        else \
                            update(bin_truthtable, bin_cost); \
                         \
                        row->data[bin_truthtable].kind = ekind; \
                        row->data[bin_truthtable].left = i; \
                        row->data[bin_truthtable].right = truthtable; \
                    } \
                } \
            } \
        }

        #define  OR(a, b) ((a) | (b))
        #define AND(a, b) ((a) & (b))

        #define  ORN(a, b)  (~(a) |  (b))
        #define  NOR(a, b) ~( (a) |  (b))
        #define ANDN(a, b)  (~(a) &  (b))
        #define NAND(a, b) ~( (a) &  (b))
        #define  XOR(a, b)  (( a) ^  (b))
        #define NXOR(a, b) ~( (a) ^  (b))

        #define   LT(a, b)  ((~a) &  (b))
        #define  LTE(a, b)  ((~a) |  (b))
        #define   GT(a, b)  (( a) & ~(b))
        #define  GTE(a, b)  (( a) | ~(b))

        if (flags->use_operators.or)
        {
            BINARY_OPERATOR(ek_or, OR);
        }

        if (flags->use_operators.and)
        {
            BINARY_OPERATOR(ek_and, AND);
        }

        if (flags->use_operators.orn)
        {
            BINARY_OPERATOR(ek_orn, ORN);
        }

        if (flags->use_operators.nor)
        {
            BINARY_OPERATOR(ek_nor, NOR);
        }

        if (flags->use_operators.andn)
        {
            BINARY_OPERATOR(ek_andn, ANDN);
        }

        if (flags->use_operators.nand)
        {
            BINARY_OPERATOR(ek_nand, NAND);
        }

        if (flags->use_operators.xor)
        {
            BINARY_OPERATOR(ek_xor,   XOR);
        }

        if (flags->use_operators.nxor)
        {
            BINARY_OPERATOR(ek_nxor, NXOR);
        }

        if (flags->use_operators.lt)
        {
            BINARY_OPERATOR(ek_lt,  LT);
        }

        if (flags->use_operators.lte)
        {
            BINARY_OPERATOR(ek_lte, LTE);
        }

        if (flags->use_operators.gt)
        {
            BINARY_OPERATOR(ek_gt,  GT);
        }

        if (flags->use_operators.gte)
        {
            BINARY_OPERATOR(ek_gte, GTE);
        }

        if (flags->use_operators.ternary)
        {
            for (int i = done.head; i != -1; i = done.next[i])
            {
                for (int j = done.head; j != -1; j = done.next[j])
                {
                    int ternary_cost = 1 + cost + row->data[i].cost + row->data[j].cost;

                    #define TERNARY(C, T, F) \
                    { \
                        uint16_t ternary_truthtable = \
                            ((C) & (T)) | (~(C) & (F)); \
                        \
                        if (ternary_cost < row->data[ternary_truthtable].cost) \
                        { \
                            if (todo.reverse[ternary_truthtable] == -1) \
                            { \
                                append(ternary_truthtable, ternary_cost); \
                            } \
                            else \
                            { \
                                update(ternary_truthtable, ternary_cost); \
                            } \
                            \
                            row->data[ternary_truthtable].kind = ek_ternary; \
                            row->data[ternary_truthtable].cond = (C); \
                            row->data[ternary_truthtable].left = (T); \
                            row->data[ternary_truthtable].right = (F); \
                        } \
                    } \

                    TERNARY(truthtable, i, j);
                    TERNARY(i, truthtable, j);
                    TERNARY(i, j, truthtable);
                }
            }
        }
        
        if (flags->use_operators.assignment)
        {
            assert(row == &simps->main);
            
            for (int t = 0; t < N; t++)
            {
                int using_me_cost = simps->with_vars[truthtable].data[t].cost;
                
                if (using_me_cost < INT_MAX)
                {
                    // int assign_cost = cost + 1 + using_me_cost;

                    // what if an assignment was free?
                    int assign_cost = cost + 0 + using_me_cost;
                    
                    if (assign_cost < simps->main.data[t].cost)
                    {
                        if (todo.reverse[t] == -1)
                        {
                            append(t, assign_cost);
                        }
                        else
                        {
                            update(t, assign_cost);
                        }

                        row->data[t].kind = ek_assignment;
                        row->data[t].left = truthtable;
                        row->data[t].right = t;
                    }
                }
            }
        }
    }

    // clear progress line, enable terminal autowrap:
    if (!ZDEBUG && flags->verbose && flags->print_with_color)
    {
        printf("\e[2K"), printf("\e[?7h");
    }
    
    EXIT;
}

void calculate_simplifications(
    const struct cmdln_flags* flags,
    struct simplifications* simps)
{
    ENTER;
    
    if (flags->use_operators.assignment)
    {
        struct cmdln_flags flag_no_assign = *flags;
        
        flag_no_assign.use_operators.assignment = false;
        
        #ifdef MULTITHREADED_BUILD
        {
            int num_cores = sysconf(_SC_NPROCESSORS_ONLN);
            
            zprintf("num_cores = %i" "\n", num_cores);
            
            assert(0 < num_cores && num_cores < 100);
            
            struct cmdln_flags flag_no_verbose = flag_no_assign;
            
            if (!flags->quiet && flags->verbose)
            {
                printf(""
                    "note: the usual verbosity is disabled in the "
                    "multithreaded section" "\n"
                "");
                
                flag_no_verbose.verbose = false;
            }
            
            int starts[num_cores];
            
            void* runner(void* _start)
            {
                const int* start = _start;
                
                for (int a = *start; a < N; a += num_cores)
                {
                    if (flags->verbose)
                    {
                        printf("a = 0b%016b" "\n", a);
                    }
                    
                    helper(
                        /* cmdln flags: */ &flag_no_verbose,
                        /* simplifications */ simps,
                        /* have extra variable? */ true,
                        /* extra variable value: */ a);
                }
                
                return NULL;
            }
            
            pthread_t handles[num_cores];
            
            for (int i = 0; i < num_cores; i++)
            {
                starts[i] = i;
                
                pthread_create(
                    /* handle */ &handles[i],
                    /* attributes: */ NULL,
                    /* start_routine: */ runner,
                    /* arg: */ &starts[i]);
            }
            
            for (int i = 0; i < num_cores; i++)
            {
                pthread_join(
                    /* handle: */ handles[i],
                    /* return value: */ (void*[1]){});
            }
        }
        #else
        {
            for (int a = 0; a < N; a++)
            {
                helper(
                    /* cmdln flags: */ &flag_no_assign,
                    /* simplifications */ simps,
                    /* have extra variable? */ true,
                    /* extra variable value: */ a);
            }
        }
        #endif
    }
    
    helper(
        /* cmdln flags: */ flags,
        /* simplifications */ simps,
        /* have extra variable? */ false,
        /* extra variable value: */ 0);
    
    EXIT;
}