#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "verifier.h"

int num_vars_;
int num_clauses_;
int clause_length_;

int main(int argc, char *argv[])
{
	int i, j;
	FILE *fin;
	char **clauses;
	char bracket;
	char *assignment;
	
	--argc; ++argv;
	if (argc != 2)
	{
		fprintf(stderr, "Usage: ./verify <clauses_file> <assignment_file>\n");
		exit(1);
	}
	
	fin = fopen(argv[0], "r");
	if (fin == NULL)
	{
		fprintf(stderr, "Clauses file %s not found!\n", argv[0]);
		exit(1);
	}

	fscanf(fin, "%d", &num_vars_);
	fscanf(fin, "%d", &num_clauses_);
	fscanf(fin, "%d", &clause_length_);

	clauses = (char**)malloc(num_clauses_ * sizeof(char*));
	for (i = 0; i < num_clauses_; ++i)
		clauses[i] = (char*)malloc(num_vars_ * sizeof(char));
	assignment = (char*)malloc(num_vars_ * sizeof(char));
	for (i = 0; i < num_vars_; ++i)
		assignment[i] = UNASSIGNED;

	for (i = 0; i < num_clauses_; ++i)
	{
		int var_index;
		clauses[i] = (char*)malloc(num_vars_ * sizeof(char));
		for (j = 0; j < num_vars_; ++j)
			clauses[i][j] = UNASSIGNED;
		fscanf(fin, "%c", &bracket);
		fscanf(fin, "%c", &bracket);
		for (j = 0; j < clause_length_; ++j)
		{
			fscanf(fin, "%d", &var_index);
			if (var_index > 0)
				clauses[i][var_index - 1] = TRUE;
			else
			{
				var_index *= -1;
				clauses[i][var_index - 1] = FALSE;
			}
		}
		fscanf(fin, "%c", &bracket);
		fscanf(fin, "%c", &bracket);
	}
	fclose(fin);

	fin = fopen(argv[1], "r");
	if (fin == NULL)
	{
		fprintf(stderr, "Assignment file %s not found!\n", argv[0]);
		exit(1);
	}
	for (i = 0; i < num_vars_; ++i)
	{
		fscanf(fin, "%d", &j);
		if (j > 0)
		{
			if (j != (i + 1))
				assert(NULL);
			assignment[i] = TRUE;
		}
		else if (j < 0)
		{
			j *= - 1;
			if (j != (i + 1))
				assert(NULL);
			assignment[i] = FALSE;
		}
		else
			assert(NULL);
	}

	if (check_if_all_clauses_true(clauses, assignment))
		printf("Correct!\n");
	else
		printf("Incorrect!\n");

	return 0;
}

int check_if_all_clauses_true(char **clauses, char *assignment)
{
	int i, j;

	for (i = 0; i < num_clauses_; ++i)
	{
		for (j = 0; j < num_vars_; ++j)
		{
			if (clauses[i][j] != 0 && ((clauses[i][j] ^ assignment[j]) == 0))
				break;
		}
		if (j == num_vars_)
		{
//			fprintf(stderr, "Clause %d is false because of variable %d\n", i, j);
			return 0;
		}
	}

	return 1;
}