// main.c
// Copyright (C) 2023 Mark Bowron

// Verify Figure 8.

// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.

// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.


#include    <stdio.h>
#include    <stdlib.h>
#include    <inttypes.h>
#include    <stdbool.h>
#include    <string.h>
#include    "set_operators.h"
#include    "set_families.h"
#include    "set_relations.h"
#include    "collapses.h"
#include    "topologies.h"
#include    "relations_408.h"
#include    "global_orderings_9.h"


int main(int argc, const char * argv[])
{
    int   **implications, equiv, flag, j, k, m;
    int   **copy, **tc, **ab, **tr; // For transitive reduction only.
    int     type, first_j = 0, first_k = 0;
    REL    *canon = CreateREL(8);

// There are 74 equivalence classes of set relations in Table 11 but only eight classes
// of operator relations in Figure 8.  We number them 1,...,8 vertically from the top
// and from the left within each row.  figure_eight[] translates Table 11 to Figure 8.

    static const int figure_eight[75] = {0,3,6,1,1,3,0,0,0,0,
                                         3,1,3,3,1,0,0,0,3,6,
                                         6,1,0,0,0,4,2,0,6,0,
                                         6,6,5,0,0,6,6,6,0,0,
                                         6,7,0,0,7,7,8,6,6,0,
                                         0,0,8,7,8,7,0,0,0,0,
                                         8,8,7,6,0,0,0,8,8,7,
                                         0,0,8,8,0};

    implications = (int **)malloc(8 * sizeof(int *));
    if (implications==0)
    {
        printf("\nCould not allocate space for implications.\n");
        exit(0);
    }
    copy = (int **)malloc(8 * sizeof(int *));
    if (copy==0)
    {
        printf("\nCould not allocate space for copy.\n");
        exit(0);
    }
    tc = (int **)malloc(8 * sizeof(int *));
    if (tc==0)
    {
        printf("\nCould not allocate space for tc.\n");
        exit(0);
    }
    ab = (int **)malloc(8 * sizeof(int *));
    if (ab==0)
    {
        printf("\nCould not allocate space for ab.\n");
        exit(0);
    }
    tr = (int **)malloc(8 * sizeof(int *));
    if (tr==0)
    {
        printf("\nCould not allocate space for tr.\n");
        exit(0);
    }
    for (j=0; j<8; j++)
    {
        implications[j] = (int *)malloc(8 * sizeof(int));
        if (implications[j]==0)
        {
            printf("\nCould not allocate space for implications[%d].\n", j);
            exit(0);
        }
        copy[j] = (int *)malloc(8 * sizeof(int));
        if (copy[j]==0)
        {
            printf("\nCould not allocate space for copy[%d].\n", j);
            exit(0);
        }
        tc[j] = (int *)malloc(8 * sizeof(int));
        if (tc[j]==0)
        {
            printf("\nCould not allocate space for tc[%d].\n", j);
            exit(0);
        }
        ab[j] = (int *)malloc(8 * sizeof(int));
        if (ab[j]==0)
        {
            printf("\nCould not allocate space for ab[%d].\n", j);
            exit(0);
        }
        tr[j] = (int *)malloc(8 * sizeof(int));
        if (tr[j]==0)
        {
            printf("\nCould not allocate space for tr[%d].\n", j);
            exit(0);
        }
        for (k=0; k<8; k++)
        {
            implications[j][k] = 1;
            copy[j][k] = 0;
            tc[j][k] = 0;
            ab[j][k] = 0;
            tr[j][k] = 0;
        }
    }

// With only minor modification, much of what follows is from other other programs.

// Confirm that every equivalence in Figure 8 holds.

    for (equiv=1; equiv<75; equiv++)
    {
        type = 0;
        for (j=0; j<34; j++)
            for (k=0; k<34; k++)
            {
                if (figure_eight[inequality_classes[j][k]] == equiv)
                {
                    if (!type)
                    {

// If type == 0 then we record j and k and continue our search;
// whenever we find a new relation in the same equivalence class,
// we verify that for each of the 9 global orderings on KF, the
// initial relation and the new one either both hold or both fail.

                        type = 1;
                        first_j = j;
                        first_k = k;
                        continue;
                    }
                    for (m=0; m<9; m++)
                    {
                        if (global_orderings_on_kf[m][j][k])
                        {
                            if (type == 1)
                            {
                                if(!global_orderings_on_kf[m][first_j][first_k])
                                {
                                    printf("Error: global ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                            else
                            {
                                if (!(global_orderings_on_kf[m][first_j][first_k]*global_orderings_on_kf[m][first_k][first_j]))
                                {
                                    printf("Error: global ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                        }
                        else
                        {
                            if (type == 1)
                            {
                                if(global_orderings_on_kf[m][first_j][first_k])
                                {
                                    printf("Error: global ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                            else
                            {
                                if (global_orderings_on_kf[m][first_j][first_k]*global_orderings_on_kf[m][first_k][first_j])
                                {
                                    printf("Error: global ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                        }
                    }
                }
                
                if (figure_eight[equation_classes[j][k]] == equiv)
                {
                    if (!type)
                    {
                        type = 2;
                        first_j = j;
                        first_k = k;
                        continue;
                    }
                    for (m=0; m<9; m++)
                    {
                        if (global_orderings_on_kf[m][j][k]*global_orderings_on_kf[m][k][j])
                        {
                            if (type == 1)
                            {
                                if(!global_orderings_on_kf[m][first_j][first_k])
                                {
                                    printf("Error: global ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                            else
                            {
                                if (!(global_orderings_on_kf[m][first_j][first_k]*global_orderings_on_kf[m][first_k][first_j]))
                                {
                                    printf("Error: global ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                        }
                        else
                        {
                            if (type == 1)
                            {
                                if(global_orderings_on_kf[m][first_j][first_k])
                                {
                                    printf("Error: global ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                            else
                            {
                                if (global_orderings_on_kf[m][first_j][first_k]*global_orderings_on_kf[m][first_k][first_j])
                                {
                                    printf("Error: global ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                        }
                    }
                }
            }
    }

    printf("\nEvery equivalence in Figure 8 holds.\n\n");

// Find one representative for each equivalence class in Figure 8.

    for (equiv=0; equiv<8; equiv++)
    {
        flag = 0;
        for (j=0; j<34; j++)
        {
            for (k=0; k<34; k++)
            {
                if (figure_eight[inequality_classes[j][k]] == equiv+1)
                {
                    canon->_type[equiv] = 1;
                    canon->_x[equiv] = j;
                    canon->_y[equiv] = k;
                    flag = 1;
                    break;
                }
            }
            if (flag) break;
        }
        if (!flag)
        {
            for (j=0; j<34; j++)
            {
                for (k=0; k<34; k++)
                {
                    if (figure_eight[equation_classes[j][k]] == equiv+1)
                    {
                        canon->_type[equiv] = 2;
                        canon->_x[equiv] = j;
                        canon->_y[equiv] = k;
                        flag = 1;
                        break;
                    }
                }
                if (flag) break;
            }
        }
    }

// We now test for each of the 8*7 = 56 nontrivial implications that can hold among
// the eight equivalence classes of operator relations in Figure 8.  Such an implication
// holds in general if and only if it holds for each of the 9 global orderings on KF.

    for (j=0; j<8; j++)
        for (k=0; k<8; k++)
        {
            if (j == k) continue;
            if (canon->_type[j] == 1)
            {
                for (m=0; m<9; m++)
                {
                    if (global_orderings_on_kf[m][canon->_x[j]][canon->_y[j]])
                    {
                        if (!global_orderings_on_kf[m][canon->_x[k]][canon->_y[k]])
                        {
                            implications[j][k] = 0;
                            break;
                        }
                        if (canon->_type[k] == 2)
                        {
                            if (!global_orderings_on_kf[m][canon->_y[k]][canon->_x[k]])
                            {
                                implications[j][k] = 0;
                                break;
                            }
                        }
                    }
                }
            }
            else // canon[j] is an equation
            {
                for (m=0; m<9; m++)
                {
                    if (global_orderings_on_kf[m][canon->_x[j]][canon->_y[j]]*
                        global_orderings_on_kf[m][canon->_y[j]][canon->_x[j]])
                    {
                        if (!global_orderings_on_kf[m][canon->_x[k]][canon->_y[k]])
                        {
                            implications[j][k] = 0;
                            break;
                        }
                        if (canon->_type[k] == 2)
                        {
                            if (!global_orderings_on_kf[m][canon->_y[k]][canon->_x[k]])
                            {
                                implications[j][k] = 0;
                                break;
                            }
                        }
                    }
                }
            }
        }

// Our final task is to compute the transitive reduction of the implications[][] matrix.

    getTransitiveReduction(implications,copy,tc,ab,tr,8);

// Print all edges in Figure 7.

    for (j=8; j>0; j--)
    {
        for (k=0; k<8; k++)
            if (tr[j-1][k]) printf("\n%d < %d", j, k+1);
        if (j>8) printf("\n");
    }

    for (j=0; j<8; j++)
    {
        free(implications[j]);
        free(copy[j]);
        free(tc[j]);
        free(ab[j]);
        free(tr[j]);
    }
    free(implications);
    free(copy);
    free(tc);
    free(ab);
    free(tr);
    FreeREL(canon);
    printf("\n\n");
    return EXIT_SUCCESS;
}