#include "bdd.h"
#include <fstream>
#include <chrono>
using namespace std;

#define NUM_OB 9 //========================= число объектов
#define NUM_P 4 //========================= число свойств
#define LOG_N 4
#define NUM_VAR 144 //=================== число булевых переменных

#define NUM_COLUMN 3 //=================== число столбиков в таблице для соседей
#define COUNT 20 //==================== сумма свойств объекта
ofstream out;

void fun(char* varset, int size); // функция, используемая для вывода решений
void print();

//Ограничение 1 типа
bdd prop1 (const bdd p [NUM_OB][NUM_OB], const int num, const int val) {
    return p[num][val];
}

//Ограничение 2 типа
bdd prop2 (const bdd p1 [NUM_OB][NUM_OB], const bdd p2 [NUM_OB][NUM_OB], const int val1, const int val2) {
    bdd temp = bddtrue;
    for (int i = 0; i < NUM_OB; i++)
        temp &= !(p1[i][val1] ^ p2[i][val2]);
    return temp;
}

//Ограничение 3 типа
bdd bound3(const bdd(&mainObj)[NUM_OB][NUM_OB], const int mainVal, const bdd(&neighObj)[NUM_OB][NUM_OB], const int neighVal, const int offset)
{
    // В зависимости от значения offset обращаемся к разным соседям
    bdd task = bddtrue;
    int neighPos = 0;

    // Кто не может быть соседом
    if (offset == 2)
    {
        for (int i = 0; i < NUM_OB; i++)
        {
            if (i % NUM_COLUMN == 0)
                task &= !mainObj[i][mainVal]; // все элементы 1 столбика не могут быть соседом справа

            if (i % NUM_COLUMN == NUM_COLUMN - 1)
                task &= !neighObj[i][neighVal];  // все элементы последнего столбика не могут быть соседом слева (то есть гл. элементом)
        }

        for (int i = 0; i < NUM_COLUMN; i++)
        {
            task &= !neighObj[i][neighVal];  // все верхние элементы не могут быть соседом снизу
        }

        for (int i = NUM_OB - NUM_COLUMN; i < NUM_OB; i++)
        {
            task &= !mainObj[i][mainVal];   // все нижние элементы не могут быть соседом сверху (в данном контексте главным элементом)
        }

    }

    for (int i = 0; i < NUM_OB - offset; i++)
    {
        neighPos = i + offset;
        task &= !(mainObj[i][mainVal] ^ neighObj[neighPos][neighVal]);
    }

    return task;
}

//Ограничение 4 типа
bdd bound4(const bdd(&mainObj)[NUM_OB][NUM_OB], const int mainVal, const bdd(&neighObj)[NUM_OB][NUM_OB], const int neighVal)
{
    bdd temp1 = bddtrue;
    bdd temp2 = bddtrue;

    temp1 &= bound3(mainObj, mainVal, neighObj, neighVal, 2); // сосед слева снизу
    temp2 &= bound3(neighObj, neighVal, mainObj, mainVal, 2); // сосед справа сверху


    return temp1 | temp2;
}




int main() {
    setlocale(LC_ALL, "rus");
    // инициализация
    bdd_init(10000000, 1000000);

    bdd_setvarnum(NUM_VAR);

    // ->--- вводим функцию p(k, i, j) следующим образом ( p[k][i][j] ):
    bdd p[NUM_P][NUM_OB][NUM_OB];

    unsigned I = 0;
    for (unsigned i = 0; i < NUM_OB; i++) {
        for (unsigned j = 0; j < NUM_OB; j++)
            for (int m = 0; m < NUM_P; m++) {
                p[m][i][j] = bddtrue;
                for (unsigned k = 0; k < LOG_N; k++) p[m][i][j] &= ((j >> k) & 1) ? bdd_ithvar(I + LOG_N * m + k) : bdd_nithvar(I + LOG_N * m + k);
            }
        I += LOG_N*NUM_P;
    }
    // -<---

    bdd task = bddtrue; // булева функция, определяющая решение, начальное значение true

    // ->--- ограничение по-умолчанию 6
    for (unsigned i = 0; i < NUM_OB; i++) {
        bdd temp[NUM_P];
        for (int m = 0; m < NUM_P; m++)
            temp[m] = bddfalse;
        for (unsigned j = 0; j < NUM_OB; j++)
            for (int m = 0; m < NUM_P; m++)
                temp[m] |= p[m][i][j];
        for (int m = 0; m < NUM_P; m++)
            task &= temp[m];
    }

    // ограничение типа 1
    task &= prop1(p[0], 4, 4);
    task &= prop1(p[0], 6, 8);
    task &= prop1(p[0], 2, 2);
    task &= prop1(p[3], 2, 4);

    task &= prop1(p[3], 3, 3); //add
    task &= prop1(p[1], 0, 8); //add
    task &= prop1(p[0], 1, 1); //add
    //


    // ограничение типа 2
    task &= prop2(p[1], p[2], 8, 7);
    task &= prop2(p[1], p[3], 1, 5);
    task &= prop2(p[3], p[2], 2, 2);
    task &= prop2(p[0], p[1], 2, 7);
    task &= prop2(p[0], p[2], 6, 4);
    task &= prop2(p[0], p[2], 3, 3);

    task &= prop2(p[0], p[1], 7, 4); // add
    task &= prop2(p[0], p[1], 8, 2); // add
    task &= prop2(p[1], p[2], 5, 5); // add
    //


    //ограничение типа 3
    task &= bound3(p[0], 1, p[1], 3, 2);
    task &= bound3(p[3], 0, p[0], 5, 2);
    task &= bound3(p[0], 3, p[2], 1, 2);
    task &= bound3(p[2], 3, p[0], 7, 2);
    //


    //ограничение типа 4
    task &= bound4(p[3], 4, p[1], 5);
    task &= bound4(p[1], 3, p[2], 6);

    task &= bound4(p[2], 1, p[1], 6); // add
    task &= bound4(p[0], 7, p[3], 8); // add
    task &= bound4(p[2], 1, p[0], 3); // add
    //


    //ограничение типа 7

    bdd temp;

    for (int i = 0; i < NUM_OB; i++)
    {
        temp = bddtrue;

        for (int j1 = 0; j1 < NUM_OB; j1++)
        {
            for (int j2 = 0; j2 < NUM_OB; j2++)
            {
                for (int j3 = 0; j3 < NUM_OB; j3++)
                {
                    for (int j4 = 0; j4 < NUM_OB; j4++)
                    {
                        if (j1 + j2 + j3 + j4 > COUNT)
                        {
                            temp &= !(p[0][i][j1] & p[1][i][j2] & p[2][i][j3] & p[3][i][j4]);
                        }
                    }
                }
            }
        }
        task &= temp; // вставка условия в общее решение
    }


    chrono::high_resolution_clock::time_point d1 = chrono::high_resolution_clock::now();

    // ->--- ограничение по-умолчанию 5
    for (unsigned j = 0; j < NUM_OB; j++)
        for (unsigned i = 0; i < NUM_OB - 1; i++)
            for (unsigned k = i + 1; k < NUM_OB; k++) {
                cout << j << i << k << endl;
                for (int m = 0; m < NUM_P; m++)
                    task &= p[m][i][j] >> !p[m][k][j];
            }

    // -<---
    chrono::high_resolution_clock::time_point d2 = chrono::high_resolution_clock::now();

    chrono::duration<double> time_span_D = chrono::duration_cast<chrono::duration<double>>(d2 - d1);
    cout << "" << "5-е ограничение: " << time_span_D.count() << " sec\n\n\n\n\n\n";
    out.open("out.txt");
    unsigned satcount = (unsigned)bdd_satcount(task);
    out << satcount << " solutions:\n" << endl;
    if (satcount) bdd_allsat(task, fun);
    out.close();


    bdd_done(); // завершение работы библиотеки
    return 0;
}

// Ниже реализация функций, управляющих выводом результатов.
// Рекомендуется самостоятельно с ними ознакомиться.
// В собственных заданиях следует использовать эти функции
// или придумать собственные.

char var[NUM_VAR];

void print() {
    for (unsigned i = 0; i < NUM_OB; i++) {
        out << i << ": ";
        for (unsigned j = 0; j < NUM_P; j++) {
            int J = i * NUM_P * LOG_N + j * LOG_N;
            int num = 0;
            for (unsigned k = 0; k < LOG_N; k++) num += (unsigned)(var[J + k] << k);
            out << num << ' ';
        }
        out << endl;
    }
    out << endl;
}

void build(char* varset, unsigned n, unsigned I) {
    if (I == n - 1) {
        if (varset[I] >= 0) {
            var[I] = varset[I];
            print();
            return;
        }
        var[I] = 0;
        print();
        var[I] = 1;
        print();
        return;
    }
    if (varset[I] >= 0) {
        var[I] = varset[I];
        build(varset, n, I + 1);
        return;
    }
    var[I] = 0;
    build(varset, n, I + 1);
    var[I] = 1;
    build(varset, n, I + 1);
}

void fun(char* varset, int size) {
    build(varset, size, 0);
}