#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdint.h>
#include <stdbool.h>
#include <sys/stat.h>
#include <math.h>
#include <ctype.h>
#include <regex.h>

unsigned model_vars = 0;
char *model;
unsigned m_sz = 0;

char *read_whitespace(char *p)
{
    while ((*p >= 9 && *p <= 13) || *p == 32)
        ++p;
    return p;
}

char *read_int(char *p, int *i)
{
    *i = 0;
    bool sym = true;
    while (*p < '0' || *p > '9')
    {
        if (*p == '\0')
            return p;
        if (*p == '-')
            sym = false;
        ++p;
    }
    while (*p >= '0' && *p <= '9')
    {
        if (*p == '\0')
            return p;
        *i = *i * 10 + *p - '0';
        ++p;
    }
    if (!sym)
        *i = -(*i);
    return p;
}

void load_model(char *model_file)
{
    bool sat_model = false;
    FILE *fp = fopen(model_file, "r");
    struct stat sb;
    if (stat(model_file, &sb) == -1)
    {
        perror("stat");
        exit(EXIT_FAILURE);
    }

    char *file_contents = malloc(sb.st_size);

    while (fscanf(fp, "%[^\n] ", file_contents) != EOF)
    {
        if (file_contents[0] == 'v')
        {
            char *end = file_contents + strlen(file_contents);
            char *p = file_contents + 1;
            while (p < end)
            {
                int int_read = 0;
                bool sym = true;
                while ((p < end) && (*p < '0' || *p > '9'))
                {
                    if (*p == '-')
                        sym = false;
                    ++p;
                }
                while ((p < end) && (*p >= '0' && *p <= '9'))
                {
                    int_read = int_read * 10 + *p - '0';
                    ++p;
                }
                if (!sym)
                    int_read = -int_read;
                if (int_read == 0)
                    break;

                int var = abs(int_read);
                int phase = (int_read > 0 ? 1 : 0);
                if (var >= m_sz)
                { // enlarge
                    if (m_sz == 0)
                    {
                        int cap = 256 > (var + 1) ? 256 : (var + 1);
                        model = realloc(model, cap);
                        m_sz = cap;
                        for (int ii = 0; ii < cap; ++ii)
                        {
                            model[ii] = 2;
                        }
                    }
                    else
                    {
                        int cap = (m_sz << 1) > (var + 1) ? (m_sz << 1) : (var + 1);
                        model = realloc(model, cap);
                        for (int ii = m_sz; ii < cap; ++ii)
                        {
                            model[ii] = 2;
                        }
                        m_sz = cap;
                    }
                }
                if (var > model_vars)
                    model_vars = var;
                model[var] = phase;
            }
        }
        else if (file_contents[0] == 's')
        {
            regex_t regex;
            int reti;
            char msgbuf[100];
            reti = regcomp(&regex, "s.*UNSAT", 0);
            reti = regexec(&regex, file_contents, 0, NULL, 0);
            if (!reti)
            {
                puts("c ERROR: check_sat do not support UNSAT");
                exit(0);
            }
            else
            {
                reti = regcomp(&regex, "s.*SAT", 0);
                reti = regexec(&regex, file_contents, 0, NULL, 0);
                if (!reti)
                    sat_model = true;
            }
        }
    }
    if (sat_model == false)
    {
        puts("c ERROR: check UNKNOWN File");
        exit(0);
    }

    fclose(fp);
}

char *casat_read_until_new_line(char *p)
{
    while (*p != '\n')
    {
        if (*p == '\0')
        {
            printf("parse error: unexpected EOF");
            exit(0);
        }
        ++p;
        // printf("%c",p[0]);
    }
    return ++p;
}

bool check_model(char *cnf_file)
{
    int num_vars = 0;
    int num_clauses = 0;

    bool flag = false;

    FILE *fp = fopen(cnf_file, "r");
    fseek(fp, 0, SEEK_END);
    uint64_t length = ftell(fp);
    char *fbuffer;
    fbuffer = (char *)malloc((length + 1) * sizeof(char));
    rewind(fp);
    length = fread(fbuffer, 1, length, fp);
    // strip the last white space
    while (isspace(fbuffer[length - 1]))
        length--;
    fbuffer[length] = '\0';
    char *p = fbuffer;
    int tmp_var = 0;
    int tmp_cls = 0;
    int cur_cls_sz = 0;
    int *cur_cls;
    int res = true;
    while (*p != '\0')
    {
        p = read_whitespace(p);
        if (*p == '\n')
            p = casat_read_until_new_line(p);
        else if (*p == 'c')
            p = casat_read_until_new_line(p);
        else if (*p == 'p')
        {
            // p += 5;
            p = read_int(p, &tmp_var);
            if(tmp_var >= m_sz){
                model = realloc(model, tmp_var + 1);
                for(int i = m_sz; i<tmp_var+1;++i){
                    model[i] = 2;
                }
                m_sz = tmp_var + 1;
            }
            p = read_int(p, &tmp_cls);
            cur_cls = (int *)malloc(sizeof(int) * tmp_var);
        }
        else
        {
            int32_t dimacs_lit;
            p = read_int(p, &dimacs_lit);
            if (*p == '\0' && dimacs_lit != 0)
            {
                printf("c PARSE ERROR! Unexpected EOF\n");
                exit(0);
            }
            if (dimacs_lit == 0)
            {
                num_clauses += 1;
                if (flag == false)
                {
                    printf("c UNSAT clause %d :", num_clauses);
                    for (int i = 0; i < cur_cls_sz; ++i)
                    {
                        printf("%d ", cur_cls[i]);
                    }
                    printf("\n");
                    res = false;
                }

                cur_cls_sz = 0;
                flag = false;
            }
            else
            {
                bool sym = (dimacs_lit > 0 ? 1 : 0);
                int var = abs(dimacs_lit);
                num_vars = (var > num_vars ? var : num_vars);
                cur_cls[cur_cls_sz++] = dimacs_lit;
                if (sym == model[var])
                {
                    flag = true;
                }
            }
        }
    }

    if (tmp_var != num_vars)
    {
        printf("c WARNING! The number of variable is not match head. (%d %d)\n", tmp_var, num_vars);
    }
    if (tmp_cls != num_clauses)
    {
        printf("c WARNING! The number of clauses is not match head.\n");
    }
    if (tmp_var != model_vars)
    {
        printf("c WARNING! The number of vars is not match the size of given model.\n");
    }

    free(fbuffer);
    free(cur_cls);
    return res;
}

int main(unsigned argc, char **argv)
{
    char *cnf_file = argv[1];
    char *model_file = argv[2];
    load_model(model_file);
    bool res = check_model(cnf_file);
    if (res == true)
    {
        printf("c SAT-VERIFIED\n");
    }
    else
    {
        printf("c WRONG\n");
    }
    if (model)
        free(model);
    return 0;
}