#include <fstream>
#include <iostream>
#include <vector>
#include <cstdlib>
#include <time.h>
#include <string>
#include <algorithm>
#include <ctime>
using namespace std;

int main() {
    srand(time(NULL));

    cout << "Porownanie algorytmow WalkSAT i GSAT\n\n";
    int ilosc_zmiennych, ilosc_implicentow, min_zmiennych, max_zmiennych;

    if(!ifstream("funkcja.txt")) {
        cout << "Nie znaleziono pliku funkcja.txt, generowanie.\n";
        ofstream plik("funkcja.txt");
        if(!plik) {
            cout << "Nie mozna utworzyc pliku.";
        }
        else {
            cout << "Podaj maksymalna liczbe zmiennych: ";
            cin >> ilosc_zmiennych;
            cout << "Podaj liczbe implicentow: ";
            cin >> ilosc_implicentow;
            cout << "Podaj minimalna liczbe zmiennych w implicencie: ";
            cin >> min_zmiennych;
            cout << "Podaj maksymalna liczbe zmiennych w implicencie (maksimum " << ilosc_zmiennych << "): ";
            cin >> max_zmiennych;

            vector <int> zmienne;
            for (size_t i = 0; i < ilosc_zmiennych; i++) {
                zmienne.push_back(i);
            }
            for (int i = 0; i < ilosc_implicentow; i++) {
                plik << "( ";
                int ile = rand() % (max_zmiennych - min_zmiennych + 1) + min_zmiennych;
                int* bufor = new int[ile];
                for (int j = 0; j < ile; j++) {
                    int zmienna = rand() % zmienne.size();
                    if (rand() % 2) {
                        plik << "x" << zmienne[zmienna];
                    }
                    else {
                        plik << "~x" << zmienne[zmienna];
                    }
                    bufor[j] = zmienne[zmienna];
                    zmienne.erase(zmienne.begin() + zmienna);
                    if (j != ile-1) {
                        plik << " v ";
                    }
                }
                for (int j = 0; j < ile; j++) {
                    zmienne.push_back(bufor[j]);
                }
                delete[] bufor;
                plik << " )";
                if (i != ilosc_implicentow-1) {
                    plik << " ^ ";
                }
            }
            plik.close();
            cout << "Wygenerowano.\n\n";
        }
    }

    ifstream plik("funkcja.txt");
    if(plik) {
        vector <vector <vector <int>>> funkcja;
        vector <int> zmienne, wartosci_zmiennych;
        string wyraz, a, b;
        while (plik >> a) {
            if (a == "(") {
                vector <vector <int>> implicent;
                while (plik >> b) {
                    if (b == ")") {
                        funkcja.push_back(implicent);
                        vector <vector <int>>().swap(implicent);
                        break;
                    }
                    else if (b[0] == 'x') {
                        implicent.push_back(vector <int> { atoi(b.substr(1).c_str()), 1 });
                        if(find(zmienne.begin(), zmienne.end(), atoi(b.substr(1).c_str())) == zmienne.end()) {
                            zmienne.push_back(atoi(b.substr(1).c_str()));
                            wartosci_zmiennych.push_back(0);
                        }
                    }
                    else if (b[0] == '~') {
                        implicent.push_back(vector <int> { atoi(b.substr(2).c_str()), 0 });
                        if(find(zmienne.begin(), zmienne.end(), atoi(b.substr(2).c_str())) == zmienne .end()) {
                            zmienne.push_back(atoi(b.substr(2).c_str()));
                            wartosci_zmiennych.push_back(0);
                        }
                    }
                }
            }
        }
        cout << "Zaladowano funkcje z pliku funkcja.txt, funkcja zawiera " << funkcja.size() << " implicentow oraz " << zmienne.size() << " roznych zmiennych.\n";
        //cout << "Zaczynam od ukladu zmiennych:\n";
        int czas_poddania_sie;
        cout << "Podaj czas, po ktorym algorytmy maja wystartowac ponownie, z nowym losowym przyporzadkowaniem (w sekundach): ";
        cin >> czas_poddania_sie;
        for (int i = 0; i < zmienne.size(); i++) {
            wartosci_zmiennych[i] = rand() % 2;
            //cout << "x" << zmienne[i] << " = " << wartosci_zmiennych[i];
            //if ((i+1) % 3 == 0) cout << endl;
            //else cout << "\t\t";
        }
        //cout << endl;

        //WalkSAT
        cout << "\nRozwiazywanie problemu metoda WalkSAT...";
        clock_t poczatek_walksata = clock();
        clock_t ostatnie_losowowanie = clock();
        int losowan_walksata = 1;
        int walksat_iteracje = 0;
        int ilosc_prawdziwych;
        bool* czy_implicent_prawdziwy = new bool[funkcja.size()]();
        while(ilosc_prawdziwych != funkcja.size()) {
            if ((double(clock() - ostatnie_losowowanie) / CLOCKS_PER_SEC) > czas_poddania_sie) {
                losowan_walksata++;
                for (int i = 0; i < zmienne.size(); i++) {
                    wartosci_zmiennych[i] = rand() % 2;
                }
                ostatnie_losowowanie = clock();
            }
            ilosc_prawdziwych = 0;

            for (int i = 0; i < funkcja.size(); i++) {
                czy_implicent_prawdziwy[i] = false;
                for (int j = 0; j < funkcja[i].size(); j++) {
                    int index_obecnej_zmiennej = distance(zmienne.begin(), find(zmienne.begin(), zmienne.end(), funkcja[i][j][0]));
                    if (wartosci_zmiennych[index_obecnej_zmiennej] == funkcja[i][j][1]) {
                            //cout << "x" << funkcja[i][j][0] << " == " << wartosci_zmiennych[index_obecnej_zmiennej] << endl;
                            czy_implicent_prawdziwy[i] = true;
                            ilosc_prawdziwych++;
                            break;
                    }
                }

            }

            for(int i = 0; i < funkcja.size(); i++) {
                //cout << "implicent nr " << i+1 << " zwraca " << czy_implicent_prawdziwy[i] << endl;
            }

            if (ilosc_prawdziwych == funkcja.size()) {
                clock_t koniec_walksata = clock();
                double czas_walksata = double(koniec_walksata - poczatek_walksata) / CLOCKS_PER_SEC;
                cout << "\n\nWalkSAT zakonczyl dzialanie sukcesem.\nDokonano " << walksat_iteracje << " iteracji w czasie " << czas_walksata*1000 << " milisekund, korzystajac z ponownego losowania " << losowan_walksata-1 << " raz(y).\nUzyskane rozwiazanie:\n";
                for (int i = 0; i < zmienne.size(); i++) {
                    cout << "x" << zmienne[i] << " = " << wartosci_zmiennych[i];
                    if ((i+1) % 4 == 0) cout << endl;
                    else cout << "\t\t";
                }
                cout << endl;
            }
            else {
                int wybrany_implicent = rand() % (funkcja.size() - ilosc_prawdziwych);
                int obecny_implicent = 0;
                for (int i = 0; i < funkcja.size(); i++) {
                    if (czy_implicent_prawdziwy[i]) continue;
                    if (obecny_implicent == wybrany_implicent) {
                        int wybrana_zmienna = rand() % funkcja[i].size();
                        int index_wybranej_zmiennej = distance(zmienne.begin(), find(zmienne.begin(), zmienne.end(), funkcja[i][wybrana_zmienna][0]));
                        wartosci_zmiennych[index_wybranej_zmiennej] = !wartosci_zmiennych[index_wybranej_zmiennej];
                        //cout << "zamieniam zmienna x" << funkcja[i][wybrana_zmienna][0] << endl;
                        walksat_iteracje++;
                        break;
                    }
                    else obecny_implicent++;
                }
            }

        }

        cout << endl;
        //GSAT
        cout << "Rozwiazywanie problemu metoda GSAT...";
        clock_t poczatek_gsata = clock();
        ostatnie_losowowanie = clock();
        int losowan_gsata = 1;
        for (int i = 0; i < zmienne.size(); i++) {
            wartosci_zmiennych[i] = rand() % 2;
        }
        ilosc_prawdziwych = 0;
        int gsat_iteracje = 0;
        int index_wybranej_zmiennej = 0;
        int rekord_prawdziwych_implicentow = 0;
        int* ilosc_prawdziwych_dla = new int[zmienne.size()]();
        while(ilosc_prawdziwych != funkcja.size()) {
            if ((double(clock() - ostatnie_losowowanie) / CLOCKS_PER_SEC) > czas_poddania_sie) {
                losowan_gsata++;
                for (int i = 0; i < zmienne.size(); i++) {
                    wartosci_zmiennych[i] = rand() % 2;
                }
                ostatnie_losowowanie = clock();
            }
            ilosc_prawdziwych = 0;

            for (int i = 0; i < funkcja.size(); i++) {
                czy_implicent_prawdziwy[i] = false;
                for (int j = 0; j < funkcja[i].size(); j++) {
                    int index_obecnej_zmiennej = distance(zmienne.begin(), find(zmienne.begin(), zmienne.end(), funkcja[i][j][0]));
                    if (wartosci_zmiennych[index_obecnej_zmiennej] == funkcja[i][j][1]) {
                            czy_implicent_prawdziwy[i] = true;
                            ilosc_prawdziwych++;
                            break;
                    }
                }

            }

            if (ilosc_prawdziwych == funkcja.size()) {
                clock_t koniec_gsata = clock();
                double czas_gsata = double(koniec_gsata - poczatek_gsata) / CLOCKS_PER_SEC;
                cout << "\n\nGSAT zakonczyl dzialanie sukcesem.\nDokonano " << gsat_iteracje << " iteracji w czasie " << czas_gsata*1000 << " milisekund, korzystajac z ponownego losowania " << losowan_gsata-1 << " raz(y).\nUzyskane rozwiazanie:\n";
                for (int i = 0; i < zmienne.size(); i++) {
                    cout << "x" << zmienne[i] << " = " << wartosci_zmiennych[i];
                    if ((i+1) % 4 == 0) cout << endl;
                    else cout << "\t\t";
                }
                cout << endl;
            }
            else {
                for (int i = 0; i < zmienne.size(); i++) {
                    wartosci_zmiennych[i] = !wartosci_zmiennych[i];
                    ilosc_prawdziwych_dla[i] = 0;
                    for (int j = 0; j < funkcja.size(); j++) {
                        for (int k = 0; k < funkcja[j].size(); k++) {
                            int index_obecnej_zmiennej = distance(zmienne.begin(), find(zmienne.begin(), zmienne.end(), funkcja[j][k][0]));
                            if (wartosci_zmiennych[index_obecnej_zmiennej] == funkcja[j][k][1]) {
                                    ilosc_prawdziwych_dla[i]++;
                                    break;
                            }
                        }
                    }
                    if (ilosc_prawdziwych_dla[i] > rekord_prawdziwych_implicentow) {
                        rekord_prawdziwych_implicentow = ilosc_prawdziwych_dla[i];
                        index_wybranej_zmiennej = i;
                    }
                    wartosci_zmiennych[i] = !wartosci_zmiennych[i];
                }
                wartosci_zmiennych[index_wybranej_zmiennej] = !wartosci_zmiennych[index_wybranej_zmiennej];
                gsat_iteracje++;
            }

        }

    }

    return 0;
}