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

// Verify every equivalence in Table 11.

// 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    "relations_408.h"
#include    "local_orderings_496.h"


int main(int argc, const char * argv[])
{
    int     equiv, j, k, m;
    int     type, first_j = 0, first_k = 0;

    for (equiv=1; equiv<75; equiv++)
    {
        type = 0;
        for (j=0; j<34; j++)
            for (k=0; k<34; k++)
            {
                if (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 496 local 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<496; m++)
                    {
                        if (local_orderings_on_kf[m][j][k])
                        {
                            if (type == 1)
                            {
                                if(!local_orderings_on_kf[m][first_j][first_k])
                                {
                                    printf("Error: local ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                            else
                            {
                                if (!(local_orderings_on_kf[m][first_j][first_k]*local_orderings_on_kf[m][first_k][first_j]))
                                {
                                    printf("Error: local ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                        }
                        else
                        {
                            if (type == 1)
                            {
                                if(local_orderings_on_kf[m][first_j][first_k])
                                {
                                    printf("Error: local ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                            else
                            {
                                if (local_orderings_on_kf[m][first_j][first_k]*local_orderings_on_kf[m][first_k][first_j])
                                {
                                    printf("Error: local ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                        }
                    }
                }
                
                if (equation_classes[j][k] == equiv)
                {
                    if (!type)
                    {
                        type = 2;
                        first_j = j;
                        first_k = k;
                        continue;
                    }
                    for (m=0; m<496; m++)
                    {
                        if (local_orderings_on_kf[m][j][k]*local_orderings_on_kf[m][k][j])
                        {
                            if (type == 1)
                            {
                                if(!local_orderings_on_kf[m][first_j][first_k])
                                {
                                    printf("Error: local ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                            else
                            {
                                if (!(local_orderings_on_kf[m][first_j][first_k]*local_orderings_on_kf[m][first_k][first_j]))
                                {
                                    printf("Error: local ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                        }
                        else
                        {
                            if (type == 1)
                            {
                                if(local_orderings_on_kf[m][first_j][first_k])
                                {
                                    printf("Error: local ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                            else
                            {
                                if (local_orderings_on_kf[m][first_j][first_k]*local_orderings_on_kf[m][first_k][first_j])
                                {
                                    printf("Error: local ordering refutes equivalence.\n\n");
                                    exit(0);
                                }
                            }
                        }
                    }
                }
            }
    }

    printf("\nEvery equivalence in Table 11 holds.\n\n");

    return EXIT_SUCCESS;
}