#include "GSAT/GSAT.hpp"
#include "GSATThread.hpp"
#include <stdio.h>
#include <stdlib.h>
#include <unistd.h>
#include <string.h>

using namespace std;

void help(char* prog) {
    fprintf(stderr, "usage: %s -i file.cnf [-t int] [-s] [-e double] [-d]\n\t-i CNF file to solve\n\t-t Number of threads to use\n\t-s Silent mode\n\t-e Use epsilon greedy method with the value (0 <= value <= 1)\n\t-d Use dynamic alpha (default is static alpha = %.1f)\n", prog, ALPHA_STATIC);
    exit(1);
}

int main(int argc, char* argv[]) {
    extern char * optarg; 
    int nbThread = DEFAULT_NB_THREAD;
    bool verbose = true;
    int opt;
    bool optI = false;
    bool optE = false;
    double epsilon = 0.1;
    bool optD = false;

    char** gsatArg = (char**) malloc(sizeof(char*) * 3);
    gsatArg[0] = (char*) malloc(sizeof(char) * strlen(argv[0]) + 1);
    memset(gsatArg[0], 0, strlen(argv[0]) + 1);
    strncpy(gsatArg[0], argv[0], strlen(argv[0]));

    while((opt = getopt(argc, argv, "si:t:e:d")) != -1) {
        switch(opt) {
            case 'i':
                optI = true;
                gsatArg[1] = (char*) malloc(sizeof(char) * 3);
                memset(gsatArg[1], 0, 3);
                strncpy(gsatArg[1], "-i", 2);
                gsatArg[2] = (char*) malloc(sizeof(char) * strlen(optarg) + 1);
                memset(gsatArg[2], 0, strlen(optarg) + 1);
                strncpy(gsatArg[2], optarg, strlen(optarg));
                break;
            case 't':
                nbThread = atoi(optarg);
                if(nbThread < 1) {
                    nbThread = 1;
                }
                break;
            case 's':
                verbose = false;
                break;
            case 'e':
                optE = true;
                epsilon = strtod(optarg, NULL);
                break;
            case 'd':
                optD = true;
                break;
            case '?':
                help(argv[0]); 
        }
    }

    if(!optI) {
        help(argv[0]);
    }
  
    GSATThread* gsat = new GSATThread(nbThread, 3, gsatArg);
    if(optE) {
        gsat->useEpsilonMethod(epsilon, !optD);
    } else {
        gsat->useEmaMethod(!optD);
    }
    printf("c nbThreads: %d\n", nbThread);
    printf("c nbVariables: %d\n", gsat->getNbVariables());
    printf("c nbClauses: %d\n", gsat->getNbClauses());
    bool result = gsat->solve(verbose);
    if(!verbose) {
        printf("s %s\n", result?"SATISFIABLE":"NOT FOUND");
    }
    

}