/*  File   : boolexpr.c
    Author : Richard A. O'Keefe
    Updated: %G%
    Purpose: Read, store, and write Boolean expressions.

    For simplicity, we use the following external form:

    <be> ::= f				% false
          |  t				% true
          |  v<nat>			% variable
          |  n(<be>)			% not
          |  a(<be>,<be>)		% and
          |  o(<be>,<be>)		% or
          |  i(<be>,<be>)		% implies
          |  e(<be>,<be>)		% equivalent

    The internal form is a faithful reflection of the external form,
    except "hash consing" is used; there is just one internal copy of
    each subexprssion, no matter how many occurrences there are in the
    external form.

    If you use readln_expr(), an expression may be followed by ".\n"
    as in Prolog.  If you use writeln_expr(), an expression will be
    followed by ".\n" as in Prolog.  The reader actually allows any
    amount of white space and %-end-of-line comments between tokens,
    but please don't put anything between a letter and the following
    left parenthesis, or Prolog won't be able to read it.

    A certain amount of normalisation will be done if you compile with
    NORMALIZE defined:
	n(t) -> f; n(f) -> t; n(n(X)) -> X;
	a(t,X) -> X; a(f,X) -> f;   a(X,t) -> X; a(X,f) -> f;    a(X,X) -> X;
	o(t,X) -> t; o(f,X) -> X;   o(X,t) -> t; o(X,f) -> X;    o(X,X) -> X;
	i(t,X) -> X; i(f,X) -> t;   i(X,t) -> t; i(X,f) -> n(X); i(X,X) -> t;
	e(t,X) -> X; e(f,X) -> n(X);e(X,t) -> X; e(X,f) -> n(X); e(X,X) -> t;
    and the operands of a, o, or e will be swapped if necessary so that
    g(X,Y) and g(Y,X) have the same internal form.
*/
#include <stdio.h>
#include <stdlib.h>
#include "boolexpr.h"

/*  f      -> {.op = LIT, .number = 0}
    t      -> {.op = LIT, .number = 1}
    vNNN   -> {.op = VAR, .number = NNN, .right = next var}
    n(X)   -> {.op = NOT, .left = X}
    a(X,Y) -> {.op = AND, .left = X, .right = Y}
    o(X,Y) -> {.op = IOR, .left = X, .right = Y}
    i(X,Y) -> {.op = IMP, .left = X, .right = Y}
    e(X,Y) -> {.op = EQV, .left = X, .right = Y}

    All the variable occurrences are linked together in an arbitrary
    order, so we can easily find all the variables.  When we are reading
    a formula, the y.hash field holds a hash code, so that we can easily
    expand the hash table.  (This is not yet done.)  When we have finished,
    that field is spare, and may be used by applications to associate
    information (such as a normal form) with an expression.
*/

void write_expr(FILE *file, BE_Ptr expr) {
    switch (expr->op) {
        case LIT:
	    putc(expr->number ? 't' : 'f', file);
	    return;
	case VAR:
	    fprintf(file, "v%u", expr->number);
	    return;
	case NOT:
	    fprintf(file, "n(");
	    write_expr(file, expr->left);
	    putc(')', file);
	    return;
	case AND:	    
	    putc('a', file);
	    break;
	case IOR:
	    putc('o', file);
	    break;
	case IMP:
	    putc('i', file);
	    break;
	case EQV:
	    putc('e', file);
	    break;
	default:
	    abort();
	    break;
    }
    putc('(', file);
    write_expr(file, expr->left);
    putc(',', file);
    write_expr(file, expr->right);
    putc(')', file);
}

void writeln_expr(FILE *file, BE_Ptr expr) {
    write_expr(file, expr);
    putc('.', file);
    putc('\n', file);
}


#define TABLE_SIZE (8*1024) /* must be a power of two */
static struct BE_Rec r_false = {0, 0, {0}, {0}, LIT};
static struct BE_Rec r_true  = {0, 0, {1}, {1}, LIT};
static BE_Ptr var_list = 0;
static BE_Ptr table[TABLE_SIZE] = {&r_false, &r_true};

static void bad_input(FILE *file, char const *msg) {
    fprintf(stderr, "Bad input at byte %ld: %s\n", ftell(file), msg);
    exit(EXIT_FAILURE);
}

static int get_skip(FILE *file) {
    int c;

    do c = getc(file); while (c <= ' ' && c >= '\0');
    while (c == '%') {
	do c = getc(file); while (c >= '\0' && c != '\n');
	if (c < '\0') return c;
	do c = getc(file); while (c <= ' ' && c >= '\0');
    }
    return c;
}

static long cell_count = 0, node_count = 0;

BE_Ptr read_expr(FILE *file) {
    /*  The VAR and LIT entries in the following table MUST be zero,
	especially the VAR entry.  The other entries are arbitrary,
	except that it helps if they are all different.  I don't know
	a good way to choose these masks.
    */
    static unsigned long const hash_mask[] = {
	0LU,		/* VAR */
	0LU,		/* LIT */
	0x407FF704LU,	/* NOT */
	0x4EDCCDE4LU,	/* AND */
	0x104BB401LU,	/* IOR */
	0x15B22B51LU,	/* IMP */
	0xEEE00EEELU,	/* EQV */
    };
    struct BE_Rec dummy;
    unsigned long hash;
    BE_Ptr p;
    
    node_count++;
    switch (get_skip(file)) {
        case 'f': case 'F':
	    return &r_false;
	case 't': case 'T':
	    return &r_true;
	case 'v': case 'V':
	    if (1 != fscanf(file, "%u", &dummy.number))
		bad_input(file, "v number");
	    dummy.op = VAR;
	    hash = dummy.number + 2;
	    break;
	case 'n':
	    if (get_skip(file) != '(') bad_input(file, "( expected");
	    dummy.left = read_expr(file);
	    dummy.op = NOT;
	    hash = dummy.left->y.hash ^ hash_mask[NOT];
	    if (get_skip(file) != ')') bad_input(file, ") expected");
	    break;
	case 'a':
	    dummy.op = AND;
	    break;
	case 'o':
	    dummy.op = IOR;
	    break;
	case 'i':
	    dummy.op = IMP;
	    break;
	case 'e':
	    dummy.op = EQV;
	    break;
	case EOF:
	    bad_input(file, "end of file in formula");
	    return &r_false;		/* just help compiler */
	default:
	    bad_input(file, "unknown character");
	    return &r_false;		/* just help compiler */
    }
    if (dummy.op >= AND) {
	unsigned long a, b;

	if (get_skip(file) != '(') bad_input(file, "( expected");
	dummy.left = read_expr(file);
	if (get_skip(file) != ',') bad_input(file, ", expected");
	dummy.right = read_expr(file);
	if (get_skip(file) != ')') bad_input(file, ") expected");
	a = dummy.left->y.hash;
	b = dummy.right->y.hash;
	hash = hash_mask[dummy.op]
             ^ ((a << 3) | (a >> (32-3)))
             ^ ((b << 5) | (b >> (32-5)));
    }
#ifdef NORMALIZE
    switch (dummy.op) {
        case VAR:
        case LIT:
            break;
	case NOT:
	    if (dummy.left == &r_false) return &r_true;
	    if (dummy.left == &r_true ) return &r_false;
	    if (dummy.left->op == NOT) return dummy.left->left;
	    break;
	case AND:
	    if (dummy.left  == &r_false) return &r_false;
	    if (dummy.left  == &r_true ) return dummy.right;
	    if (dummy.right == &r_false) return &r_false;
	    if (dummy.right == &r_true ) return dummy.left;
	    if (dummy.right == dummy.left) return dummy.left;
	    if (dummy.left->y.hash > dummy.right->y.hash)
		p = dummy.left, dummy.left = dummy.right, dummy.right = p;
	    break;
	case IOR:
	    if (dummy.left  == &r_false) return dummy.right;
	    if (dummy.left  == &r_true ) return &r_true;
	    if (dummy.right == &r_false) return dummy.left;
	    if (dummy.right == &r_true ) return &r_true;
	    if (dummy.right == dummy.left) return dummy.left;
	    if (dummy.left->y.hash > dummy.right->y.hash)
		p = dummy.left, dummy.left = dummy.right, dummy.right = p;
	    break;
	case IMP:
	    if (dummy.left  == &r_false) return &r_true;
	    if (dummy.left  == &r_true ) return dummy.right;
	    if (dummy.right == &r_false) { dummy.op = NOT; break; }
	    if (dummy.right == &r_true ) return &r_true;
	    if (dummy.right == dummy.left) return &r_true;
	    break;
	case EQV:
	    if (dummy.left  == &r_false) {
		dummy.op = NOT; dummy.left = dummy.right; break; }
	    if (dummy.left  == &r_true) return dummy.right;
	    if (dummy.right == &r_false) { dummy.op = NOT; break; }
	    if (dummy.right == &r_true ) return dummy.left;
	    if (dummy.right == dummy.left) return &r_true;
	    if (dummy.left->y.hash > dummy.right->y.hash)
		p = dummy.left, dummy.left = dummy.right, dummy.right = p;
	    break;
	default:
	    break;
    }
#endif/*NORMALIZE*/
    {
        BE_Ptr *h = &table[hash & (TABLE_SIZE - 1)];

	for (p = *h; p != 0; p = p->next) {
	    if (p->op != dummy.op) continue;
	    switch (dummy.op) {
		case LIT:
		case VAR:
		    if (p->number == dummy.number) return p;
		    break;
		case NOT:
		    if (p->left == dummy.left) return p;
		    break;
		default:
		    if (p->left  == dummy.left
		     && p->right == dummy.right
		    ) return p;
		    break;
	    }
	}
	p = malloc(sizeof *p);
	if (p == 0) bad_input(file, "memory ran out");
	cell_count++;
	*p = dummy;
	p->y.hash = hash;
	p->next = *h;
	if (dummy.op == VAR) {
	    p->right = var_list;	    
	    var_list = p;
	}
	*h = p;
	return p;
    }
}

BE_Ptr readln_expr(FILE *file) {
    int c;
    BE_Ptr r = read_expr(file);

    do c = getc(file); while (c == ' ' || c == '\t');
    if (c == '.') {
	do c = getc(file); while (c == ' ' || c == '\t');
    }
    if (c != '\n') ungetc(c, file);
    return r;
}

void free_expr(void) {
    int i;
    BE_Ptr p, q;

    node_count = 0;
    for (i = 0; i < TABLE_SIZE; i++) {
	for (p = table[i]; p != 0; p = q) {
	    q = p->next;
	    if (p->op != LIT) free(p), cell_count--;
	}
	table[i] = 0;
    }
    table[0] = &r_false;
    table[1] = &r_true;
    var_list = 0;
    if (cell_count != 0) {
	fprintf(stderr, "free_expr() left cell_count=%ld\n", cell_count);
	abort();
    }
}

#ifdef TEST
int main(void) {
    BE_Ptr x;
    int c;

    while ((c = get_skip(stdin)) >= '\0') {
	ungetc(c, stdin);
        x = readln_expr(stdin);
	writeln_expr(stdout, x);
	printf("node_count = %ld, cell_count = %ld (%lu bytes)\n\n",
	       node_count, cell_count, cell_count * sizeof *x);
	free_expr();
    }
    return 0;
}

#endif