Created
February 3, 2017 04:46
-
-
Save matthew-ball/ba1c1934366328c4063491af4388cf1d to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#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; | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment