main.c

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <ctype.h>
#include <time.h>

#define MALLOC_CHECK(ptr) ({ if (!ptr) { fprintf(stderr, "[%s] malloc failed\n", __func__); exit(EXIT_FAILURE); }})

typedef enum { VARIABLE, NEGATION, CONJUNCTION, DISJUNCTION, IMPLICATION } type_t;
typedef enum { FALSE, TRUE } value_t;

typedef struct {
  type_t type;
} term_t;

#define IS_VARIABLE(term) ((term)->type == VARIABLE)
#define IS_NEGATION(term) ((term)->type == NEGATION)
#define IS_CONJUNCTION(term) ((term)->type == CONJUNCTION)
#define IS_DISJUNCTION(term) ((term)->type == DISJUNCTION)
#define IS_IMPLICATION(term) ((term)->type == IMPLICATION)
#define IS_LITERAL(term) (IS_VARIABLE(term) || (IS_NEGATION(term) && IS_VARIABLE(NEGATION_LEFT(term))))

typedef struct {
  type_t type;
  value_t value;
  char *name;
} variable_term_t;

typedef struct {
  type_t type;
  term_t *left;
} negation_term_t;

typedef struct {
  type_t type;
  term_t *left;
  term_t *right;
} conjunction_term_t;

typedef struct {
  type_t type;
  term_t *left;
  term_t *right;
} disjunction_term_t;

typedef struct {
  type_t type;
  term_t *left;
  term_t *right;
} implication_term_t;

#define VARIABLE_NAME(term) (((variable_term_t *)(term))->name)
#define VARIABLE_VALUE(term) (((variable_term_t *)(term))->value)
#define NEGATION_LEFT(term) (((negation_term_t *)(term))->left)
#define CONJUNCTION_LEFT(term) (((conjunction_term_t *)(term))->left)
#define CONJUNCTION_RIGHT(term) (((conjunction_term_t *)(term))->right)
#define DISJUNCTION_LEFT(term) (((disjunction_term_t *)(term))->left)
#define DISJUNCTION_RIGHT(term) (((disjunction_term_t *)(term))->right)
#define IMPLICATION_LEFT(term) (((implication_term_t *)(term))->left)
#define IMPLICATION_RIGHT(term) (((implication_term_t *)(term))->right)

term_t *alloc_term(type_t type) {
  term_t *ptr = NULL;

  switch (type) {
  case VARIABLE: ptr = malloc(sizeof(variable_term_t)); ptr->type = type; break;
  case NEGATION: ptr = malloc(sizeof(negation_term_t)); ptr->type = type; break;
  case CONJUNCTION: ptr = malloc(sizeof(conjunction_term_t)); ptr->type = type; break;
  case DISJUNCTION: ptr = malloc(sizeof(disjunction_term_t)); ptr->type = type; break;
  case IMPLICATION: ptr = malloc(sizeof(implication_term_t)); ptr->type = type; break;
  default:
	fprintf(stderr, "[%s] unknown type %d\n", __func__, type);
	exit(EXIT_FAILURE);
  }

  MALLOC_CHECK(ptr);

  return ptr;
}

term_t *variable_term(const char *name) {
  term_t *ptr = alloc_term(VARIABLE);

  VARIABLE_NAME(ptr) = malloc(strlen(name) + 1);
  MALLOC_CHECK(VARIABLE_NAME(ptr));
  strcpy(VARIABLE_NAME(ptr), name);
  VARIABLE_VALUE(ptr) = -1;

  return ptr;
}

term_t *negation_term(term_t *term) {
  term_t *ptr= alloc_term(NEGATION);

  NEGATION_LEFT(ptr) = term;

  return ptr;
}

term_t *conjunction_term(term_t *left_term, term_t *right_term) {
  term_t *ptr = alloc_term(CONJUNCTION);

  CONJUNCTION_LEFT(ptr) = left_term;
  CONJUNCTION_RIGHT(ptr) = right_term;

  return ptr;
}

term_t *disjunction_term(term_t *left_term, term_t *right_term) {
  term_t *ptr = alloc_term(DISJUNCTION);

  DISJUNCTION_LEFT(ptr) = left_term;
  DISJUNCTION_RIGHT(ptr) = right_term;

  return ptr;
}

term_t *implication_term(term_t *left_term, term_t *right_term) {
  term_t *ptr = alloc_term(IMPLICATION);

  IMPLICATION_LEFT(ptr) = left_term;
  IMPLICATION_RIGHT(ptr) = right_term;

  return ptr;
}

term_t *true;
term_t *false;

value_t equal_terms(term_t *term1, term_t *term2) {
  if (IS_VARIABLE(term1) && IS_VARIABLE(term2)) {
	if (strcmp(VARIABLE_NAME(term1), VARIABLE_NAME(term2)) == 0) {
	  return TRUE;
	}
  } else if (IS_NEGATION(term1) && IS_NEGATION(term2)) {
	return equal_terms(NEGATION_LEFT(term1), NEGATION_LEFT(term2));
  } else if (IS_CONJUNCTION(term1) && IS_CONJUNCTION(term2)) {
	return equal_terms(CONJUNCTION_LEFT(term1), CONJUNCTION_LEFT(term2)) && equal_terms(CONJUNCTION_RIGHT(term1), CONJUNCTION_RIGHT(term2));
  } else if (IS_DISJUNCTION(term1) && IS_DISJUNCTION(term2)) {
	return equal_terms(DISJUNCTION_LEFT(term1), DISJUNCTION_LEFT(term2)) && equal_terms(DISJUNCTION_RIGHT(term1), DISJUNCTION_RIGHT(term2));
  }else if (IS_IMPLICATION(term1) && IS_IMPLICATION(term2)) {
	return equal_terms(IMPLICATION_LEFT(term1), IMPLICATION_LEFT(term2)) && equal_terms(IMPLICATION_RIGHT(term1), IMPLICATION_RIGHT(term2));
  }

  return FALSE;
}

void print_term(const term_t *term) {
  switch (term->type) {
  case VARIABLE: printf("%s", VARIABLE_NAME(term)); break;
  case NEGATION: printf("~"); print_term(NEGATION_LEFT(term)); break;
  case CONJUNCTION: printf("("); print_term(CONJUNCTION_RIGHT(term)); printf(" & "); print_term(CONJUNCTION_LEFT(term)); printf(")"); break;
  case DISJUNCTION: printf("("); print_term(DISJUNCTION_RIGHT(term)); printf(" | "); print_term(DISJUNCTION_LEFT(term)); printf(")"); break;
  case IMPLICATION: printf("("); print_term(IMPLICATION_RIGHT(term)); printf(" -> "); print_term(IMPLICATION_LEFT(term)); printf(")"); break;
  default:
	printf("[%s] unknown type: %d\n", __func__, term->type);
  }
}

typedef struct _environment_t environment_t;

typedef struct _environment_t {
  term_t *value;
  size_t size;
  environment_t *next;
} environment_t;

environment_t *alloc_environment() {
  environment_t *ptr = malloc(sizeof(*ptr));

  MALLOC_CHECK(ptr);

  return ptr;
}

term_t *search_environment(term_t *term, const environment_t *env) {
  while (env->value != NULL) {
	if (equal_terms(term, env->value)) {
	  return env->value;
	}

	env = env->next;
  }

  return NULL;
}

void add_to_environment(term_t *term, environment_t **env) {
  if (search_environment(term, (*env)) == NULL) {
	environment_t *ptr = alloc_environment();

	ptr->value = term;
	ptr->next = (*env);
	ptr->size = (*env)->size + 1;

	(*env) = ptr;
  }
}

environment_t *initialise_environment() {
  environment_t *ptr = alloc_environment();

  ptr->size = 0;

  true = variable_term("#T");
  false = variable_term("#F");
  VARIABLE_VALUE(true) = TRUE;
  VARIABLE_VALUE(false) = FALSE;

  add_to_environment(true, &ptr);
  add_to_environment(false, &ptr);

  return ptr;
}

void filter_literals(term_t *term, environment_t **env) {
  if (IS_NEGATION(term) && !IS_VARIABLE(NEGATION_LEFT(term))) {
	filter_literals(NEGATION_LEFT(term), env);
  } else if (IS_CONJUNCTION(term)) {
	filter_literals(CONJUNCTION_LEFT(term), env);
	filter_literals(CONJUNCTION_RIGHT(term), env);
  } else if (IS_DISJUNCTION(term)) {
	filter_literals(DISJUNCTION_LEFT(term), env);
	filter_literals(DISJUNCTION_RIGHT(term), env);
  } else if (IS_IMPLICATION(term)) {
	filter_literals(IMPLICATION_LEFT(term), env);
	filter_literals(IMPLICATION_RIGHT(term), env);
  } else if (IS_LITERAL(term)) {
	add_to_environment(term, env);
  }
}

environment_t *collect_literals(term_t *term) {
  environment_t *ptr = alloc_environment();

  ptr->size = 0;
  filter_literals(term, &ptr);

  return ptr;
}

term_t *choose_literal(const environment_t *environment) {
  srand(time(NULL));
  size_t random = rand() % environment->size, i;

  for (i = 0; i < random; i++) {
	environment = environment->next;
  }

  return environment->value;
}

void print_environment(const environment_t *environment) {
  printf("{");

  while (environment->value != NULL) {
	print_term(environment->value);
	environment = environment->next;

	if (environment->next != NULL) {
	  printf(", ");
	}
  }

  printf("}");
}

term_t *simplify(term_t *term) {
  if (IS_IMPLICATION(term)) {
	if (equal_terms(IMPLICATION_LEFT(term), IMPLICATION_RIGHT(term))) {
	  return simplify(IMPLICATION_LEFT(term));
	} else {
	  return disjunction_term(IMPLICATION_LEFT(term), negation_term(IMPLICATION_RIGHT(term)));
	}
  } else if (IS_NEGATION(term)) {
	if (IS_NEGATION(NEGATION_LEFT(term))) {
	  return NEGATION_LEFT(NEGATION_LEFT(term));
	}
  } else if (IS_CONJUNCTION(term)) {
	if (equal_terms(CONJUNCTION_LEFT(term), CONJUNCTION_RIGHT(term))) {
	  return simplify(CONJUNCTION_LEFT(term));
	}
  } else if (IS_DISJUNCTION(term)) {
	if (equal_terms(DISJUNCTION_LEFT(term), DISJUNCTION_RIGHT(term))) {
	  return simplify(DISJUNCTION_LEFT(term));
	}
  }

  return term;
}

term_t *resolution(term_t *term, environment_t *environment) {
  return term;
}

#define MAX_BUFFER 1024

term_t *next_token(FILE *input) {
  char buffer[MAX_BUFFER];
  size_t index = 0;
  int ch;

  ch = getc(input);

  while (isspace(ch)) {
	ch = getc(input);
  }

  if (ch == '\n') {
	ch = getc(input);
  }

  if (ch == EOF) {
	exit(EXIT_SUCCESS);
  }

  if (ch == '(') {
	return next_token(input);
  }

  if (ch == ')') {
	return variable_term(")");
  }

  while (!isspace(ch) && ch != ')') {
	buffer[index++] = ch;
	ch = getc(input);
  }

  buffer[index++] = '\0';

  return variable_term(buffer);
}

term_t *read_term(FILE *input) {
  term_t *token = next_token(input);

  if (strcmp(VARIABLE_NAME(token), ")") == 0) {
	return NULL;
  } else if (strcmp(VARIABLE_NAME(token), "negation") == 0) {
	return negation_term(read_term(input));
  } else if (strcmp(VARIABLE_NAME(token), "conjunction") == 0) {
	return conjunction_term(read_term(input), read_term(input));
  } else if (strcmp(VARIABLE_NAME(token), "disjunction") == 0) {
	return disjunction_term(read_term(input), read_term(input));
  } else if (strcmp(VARIABLE_NAME(token), "implication") == 0) {
	return implication_term(read_term(input), read_term(input));
  }

  return token;
}

void repl(FILE *input, environment_t **environment, int interactive) {
  term_t *term = NULL;
  int check = 1;

  while (1) {
	if (check && interactive < 2) {
	  printf("eval> ");
	}

	term = read_term(input);

	if (term != NULL) {
	  print_term(term); printf(" => "); print_term(resolution(term, *environment)); printf("\n");

	  if (check != 1) {
		check = 1;
	  }
	} else {
	  check = 0;
	}
  }
}

int main(int argc, char *argv[]) {
  FILE *input = (argc > 1) ? fopen(argv[1], "r") : stdin;
  environment_t *environment = initialise_environment();

  repl(input, &environment, argc);

  fclose(input);

  return EXIT_SUCCESS;
}