#include <stdio.h>
#include <string.h>
#include <stdlib.h>

#include "jmgraph.h"


int nColours;
int nVariables;
int nClauses;

int **edges;


void initializeVars(jmgraph *g) {
    edges = (int **) malloc(sizeof(int *) * g->n);
    for (int v = 0; v < g->n; v++) {
        edges[v] = (int *) malloc(sizeof(int) * g->maxDegree);
        for (int i = 0; i < g->maxDegree; i++) {
            edges[v][i] = -1;
        }
    }
    int count = 0;
    for (int v = 0; v < g->n; v++) {
        for (int i = 0; i < g->maxDegree; i++) {
            int u = g->e[v][i];
            if ((u != -1) && (u > v)) {
                edges[v][i] = count;
                for (int j = 0; j < g->maxDegree; j++) {
                    if (g->e[u][j] == v)
                        edges[u][j] = count;
                }
                count++;
            }
        }
    }
    nVariables = 3 * count;
/*    for (int v = 0; v < N; v++) {
        for (int u = 0; u < N; u++) {
            printf("%2d ", edges[v][u]);
        }
        printf("\n");
    }*/
}


void destroyVars(jmgraph *g) {
    for (int i = 0; i < g->n; i++) {
        free(edges[i]);
    }
    free(edges);
}


int var(int v, int i, int c) {
    // shifted by 1 because variables in cnf format are numbered from 1
    return nColours * edges[v][i] + (c - 1) + 1;
}


void addVar(char *f, int v, int i, int c) {
    char s[1000];
    sprintf(s, "%d ", var(v, i, c));
    strcat(f, s);
}


void addVarNeg(char *f, int v, int i, int c) {
    char s[1000];
    sprintf(s, "%d ", -var(v, i, c));
    strcat(f, s);
}


void endClause(char *f) {
    nClauses++;
    strcat(f, "0\n");    
}


// assuming the input graph is subcubic
char *formula_sat_edge(jmgraph *g, int colours) {
    nColours = colours;
    initializeVars(g);

    int formulaLength = 1000 * g->n + 1000; 
    char *f = (char *) malloc(sizeof(char) * formulaLength);
    f[0] = '\0';
    nClauses = 0;
    for (int v = 0; v < g->n; v++) {
        for (int i = 0; i < deg(g, v); i++) {            
            if (g->e[v][i] < v)
                continue;

            // at least one colour
            for (int c = 1; c <= nColours; c++)
                addVar(f, v, i, c);
            endClause(f);

            // at most one colour
            for (int c = 1; c <= nColours; c++) {
                for (int d = 1; d <= nColours; d++) {
                    if (d != c)
                        addVarNeg(f, v, i, d);
                }
                endClause(f);
            }
        }
        // different colours for any two incident edges
        for (int i = 0; i < deg(g, v); i++) {
            for (int j = i+1; j < deg(g, v); j++) {
                for (int c = 1; c <= nColours; c++) {
                    addVarNeg(f, v, i, c);
                    addVarNeg(f, v, j, c);
                    endClause(f);
                }
            }
        }
    }
    destroyVars(g);
    char *ff = (char *) malloc(sizeof(char) * formulaLength);
    ff[0] = '\0';
    sprintf(ff, "p cnf %d %d\n%s", nVariables, nClauses, f);
    free(f);
    return ff;
}
