#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] [-m int]\n\t-i CNF file to solve\n\t-t Number of threads to use\n\t-s Silent mode\n\t-m Max iteration number\n", prog);
    exit(1);
}

int main(int argc, char* argv[]) {
    extern char * optarg; 
    int nbThread = DEFAULT_NB_THREAD;
    int maxIteration = 0;
    bool verbose = true;
    int opt;
    bool optI = 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:m:")) != -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 'm':
                maxIteration = atoi(optarg);
                break;
            case '?':
                help(argv[0]); 
        }
    }

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

}