/* See LICENSE file for copyright and license details. */
#include "common.h"
#ifndef TEST


#define OPT_SPACE\
	do {\
		while (isspace(*s))\
			s++;\
	} while (0)

#define LEFT_BRACKET\
	do {\
		if (!STARTS("("))\
			goto einval;\
		OPT_SPACE;\
	} while (0)

#define COMMA\
	do {\
		OPT_SPACE;\
		if (!STARTS(","))\
			goto einval;\
		OPT_SPACE;\
	} while (0)

#define RIGHT_BRACKET\
	do {\
		OPT_SPACE;\
		if (!STARTS(")"))\
			goto einval;\
	} while (0)


/**
 * Parse a reference number
 * 
 * @param   s        String beginning with the first digit in the number
 * @param   end_out  Output parameter for the end of the number
 * @param   id_out   Output parameter for the reference number
 * @return           0 on success, -1 on failure
 * 
 * @throws  EINVAL   The string does not begin with a number
 * @throws  EINVAL   The number is too large
 */
USE_RESULT NONNULL_INPUT
static int
get_reference_id(char *s, char **end_out, size_t *id_out)
{
	size_t digit;

	*id_out = 0;

	if (*s == '0') {
		*end_out = &s[1];
		return 0;
	}

	if ('1' > *s || *s > '9')
		goto einval;

	while (isdigit(*s)) {
		digit = (size_t)(*s & 15);
		
		if (*id_out > (SIZE_MAX / sizeof(void *) - 1U - digit) / 10U)
			goto einval;
		*id_out = *id_out * 10U + digit;
	}

	*end_out = s;
	return 0;

einval:
	errno = EINVAL;
	return -1;
}


/**
 * Parse a reference number and allocate a reference slot for it
 * 
 * The reference slot will be initialised to `NULL`
 * 
 * @param   s             String beginning with the first digit in the number
 * @param   end_out       Output parameter for the end of the number
 * @param   id_out        Output parameter for the reference number
 * @param   referencesp   Reference to array of references points
 * @param   nreferencesp  Reference to the number of elements in `*referencesp`,
 *                        will be incremented by 1 on success
 * @return                0 on success, -1 on failure
 * 
 * @throws  EINVAL   The string does not begin with a number
 * @throws  EINVAL   The number is not `*nreferencesp`
 * @throws  ENOMEM   Insufficient memory available to allocate the slot
 */
USE_RESULT NONNULL_INPUT
static int
get_reference_id_and_allocate_slot(char *s, char **end_out, size_t *id_out,
                                   LIBNORMALFORM_SENTENCE ***referencesp, size_t *nreferencesp)
{
	void *new;

	OPT_SPACE;
	if (get_reference_id(s, &s, id_out))
		return -1;
	if (*id_out != *nreferencesp) {
		errno = EINVAL;
		return -1;
	}
	OPT_SPACE;

	new = realloc(*referencesp, (*id_out + 1U) * sizeof(**referencesp));
	if (!new)
		return -1;
	*referencesp = new;
	(*referencesp)[(*nreferencesp)++] = NULL;

	*end_out = s;
	return 0;
}


/**
 * `libnormalform_from_string` with some additional parameters:
 * 
 * @param  truep         Reference to any already constructed TRUE sentence (`*truep` is `NULL` until then)
 * @param  falsep        Reference to any already constructed FALSE sentence (`*falsep` is `NULL` until then)
 * @param  referencesp   Reference to array of references points
 * @param  nreferencesp  Reference to the number of elements in `*referencesp`
 */
USE_RESULT SOME_NONNULL_INPUT(1, 3, 4, 5, 6, 7)
static LIBNORMALFORM_SENTENCE *
from_string(char *s, char **end_out, const struct libnormalform_representation_spec *spec,
            LIBNORMALFORM_SENTENCE **truep, LIBNORMALFORM_SENTENCE **falsep,
            LIBNORMALFORM_SENTENCE ***referencesp, size_t *nreferencesp)
{
#define STARTS(WANT) (!strncmp(s, WANT, (n = sizeof(WANT) - 1U)) ? (s = &s[n]) : NULL)

	LIBNORMALFORM_SENTENCE *(*qualifier2)(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *, LIBNORMALFORM_SENTENCE *) = NULL;
	LIBNORMALFORM_SENTENCE *(*qualifier1)(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *) = NULL;
	LIBNORMALFORM_SENTENCE *(*qualifier0)(struct libnormalform_map *) = NULL;
	LIBNORMALFORM_SENTENCE *(*variadic)(LIBNORMALFORM_SENTENCE **) = NULL;
	LIBNORMALFORM_SENTENCE *(*unary)(LIBNORMALFORM_SENTENCE *) = NULL;
	LIBNORMALFORM_SENTENCE *ret = NULL, *k = NULL, *v = NULL, *x = NULL;
	size_t n, refid = SIZE_MAX;

	if (STARTS("TRUE")) {
		if (*truep)
			ret = libnormalform_ref(*truep);
		else
			ret = *truep = libnormalform_true();
	} else if (STARTS("FALSE")) {
		if (*falsep)
			ret = libnormalform_ref(*falsep);
		else
			ret = *falsep = libnormalform_false();
	} else if (STARTS("REF")) {
		LEFT_BRACKET;
		if (get_reference_id(s, &s, &refid))
			return NULL;
		RIGHT_BRACKET;
		if (refid >= *nreferencesp)
			goto einval;
		ret = (*referencesp)[refid];
		if (!ret)
			goto einval;
		ret = libnormalform_ref(ret);
		if (!ret)
			return NULL;
	} else if (STARTS("NOT")) {
		unary = &libnormalform_not;
	} else if (STARTS("AND")) {
		variadic = &libnormalform_and;
	} else if (STARTS("OR")) {
		variadic = &libnormalform_or;
	} else if (STARTS("XOR")) {
		variadic = &libnormalform_xor;
	} else if (STARTS("IF")) {
		variadic = &libnormalform_if;
	} else if (STARTS("IMPLY")) {
		variadic = &libnormalform_imply;
	} else if (STARTS("NAND")) {
		variadic = &libnormalform_nand;
	} else if (STARTS("NOR")) {
		variadic = &libnormalform_nor;
	} else if (STARTS("XNOR")) {
		variadic = &libnormalform_xnor;
	} else if (STARTS("NIF")) {
		variadic = &libnormalform_nif;
	} else if (STARTS("NIMPLY")) {
		variadic = &libnormalform_nimply;
	} else if (STARTS("ALL")) {
		qualifier2 = &libnormalform_all;
	} else if (STARTS("ANY")) {
		qualifier2 = &libnormalform_any;
	} else if (STARTS("ONE")) {
		qualifier2 = &libnormalform_one;
	} else if (STARTS("EXISTENTIALLY")) {
		qualifier1 = &libnormalform_existentially;
	} else if (STARTS("UNIVERSALLY")) {
		qualifier1 = &libnormalform_universally;
	} else if (STARTS("UNIQUELY")) {
		qualifier1 = &libnormalform_uniquely;
	} else if (STARTS("EXISTS")) {
		qualifier1 = &libnormalform_exists;
	} else if (STARTS("NEXISTS")) {
		qualifier1 = &libnormalform_nexists;
	} else if (STARTS("UNIQUE")) {
		qualifier1 = &libnormalform_unique;
	} else if (STARTS("EMPTY")) {
		qualifier0 = &libnormalform_empty;
	} else if (STARTS("NONEMPTY")) {
		qualifier0 = &libnormalform_nonempty;
	} else if (STARTS("SINGLETON")) {
		qualifier0 = &libnormalform_singleton;
	} else if (STARTS("VARIABLE")) {
		struct libnormalform_variable *a;
		OPT_SPACE;
		if (*s == '@' && get_reference_id_and_allocate_slot(&s[1], &s, &refid, referencesp, nreferencesp))
			return NULL;
		LEFT_BRACKET;
		if (!spec->get_variable)
			goto enoent;
		a = spec->get_variable(s, &s, spec->user_data);
		if (!a)
			return NULL;
		RIGHT_BRACKET;
		ret = libnormalform_variable(a);
	} else if (STARTS("FUNCTION")) {
		struct libnormalform_function *a;
		OPT_SPACE;
		if (*s == '@' && get_reference_id_and_allocate_slot(&s[1], &s, &refid, referencesp, nreferencesp))
			return NULL;
		LEFT_BRACKET;
		if (!spec->get_function)
			goto enoent;
		a = spec->get_function(s, &s, spec->user_data);
		if (!a)
			return NULL;
		RIGHT_BRACKET;
		ret = libnormalform_function(a);
	} else if (STARTS("TRANSFORMATION")) {
		struct libnormalform_transformer *a;
		OPT_SPACE;
		if (*s == '@' && get_reference_id_and_allocate_slot(&s[1], &s, &refid, referencesp, nreferencesp))
			return NULL;
		LEFT_BRACKET;
		if (!spec->get_transformer)
			goto enoent;
		a = spec->get_transformer(s, &s, spec->user_data);
		if (!a)
			return NULL;
		COMMA;
		x = from_string(s, &s, spec, truep, falsep, referencesp, nreferencesp);
		if (!x)
			return NULL;
		RIGHT_BRACKET;
		ret = libnormalform_transformation(a, x);
		x = NULL;
	} else {
		goto einval;
	}

	if (!ret) {
		OPT_SPACE;
		if (*s == '@' && get_reference_id_and_allocate_slot(&s[1], &s, &refid, referencesp, nreferencesp))
			return NULL;
		LEFT_BRACKET;
	}

	if (qualifier2) {
		struct libnormalform_map *d;
		if (!spec->get_map)
			goto enoent;
		d = spec->get_map(s, &s, spec->user_data);
		if (!d)
			return NULL;
		COMMA;
		k = from_string(s, &s, spec, truep, falsep, referencesp, nreferencesp);
		if (!k)
			return NULL;
		COMMA;
		v = from_string(s, &s, spec, truep, falsep, referencesp, nreferencesp);
		if (!v) {
			libnormalform_free(k);
			return NULL;
		}
		RIGHT_BRACKET;
		ret = (*qualifier2)(d, k, v);
		k = v = NULL;

	} else if (qualifier1) {
		struct libnormalform_map *d;
		if (!spec->get_map)
			goto enoent;
		d = spec->get_map(s, &s, spec->user_data);
		if (!d)
			return NULL;
		COMMA;
		k = from_string(s, &s, spec, truep, falsep, referencesp, nreferencesp);
		if (!k)
			return NULL;
		RIGHT_BRACKET;
		ret = (*qualifier1)(d, k);

	} else if (qualifier0) {
		struct libnormalform_map *d;
		if (!spec->get_map)
			goto enoent;
		d = spec->get_map(s, &s, spec->user_data);
		if (!d)
			return NULL;
		RIGHT_BRACKET;
		ret = (*qualifier0)(d);

	} else if (unary) {
		x = from_string(s, &s, spec, truep, falsep, referencesp, nreferencesp);
		if (!x)
			return NULL;
		RIGHT_BRACKET;
		ret = (*unary)(x);
		x = NULL;

	} else if (variadic) {
		LIBNORMALFORM_SENTENCE **xs = NULL;
		size_t nxs = 0;
		void *new;
		goto fit_one_more;
		do {
			xs[nxs] = from_string(s, &s, spec, truep, falsep, referencesp, nreferencesp);
			if (!xs[nxs])
				goto fail_variadic;
			nxs++;

			OPT_SPACE;
			if (STARTS(",")) {
				OPT_SPACE;
			} else if (*s != ')') {
				errno = EINVAL;
			fail_variadic:
				while (nxs--)
					libnormalform_free(xs[nxs]);
				free(xs);
				return NULL;
			}

		fit_one_more:
			new = realloc(xs, (nxs + 1U) * sizeof(*xs));
			if (!new)
				goto fail_variadic;
			xs = new;
		} while (!STARTS(")"));
		xs[nxs] = NULL;
		ret = (*variadic)(xs);
		free(xs);
	}

	if (end_out) {
		*end_out = s;
	} else if (*s) {
		OPT_SPACE;
		if (*s) {
			libnormalform_free(ret);
		einval:
			libnormalform_free(k);
			libnormalform_free(v);
			libnormalform_free(x);
			errno = EINVAL;
			return NULL;
		}
	}

	if (refid != SIZE_MAX)
		(*referencesp)[refid] = ret;

	return ret;

enoent:
	errno = ENOENT;
	return NULL;

#undef STARTS
}


LIBNORMALFORM_SENTENCE *
(libnormalform_from_string)(char *s, char **end_out, const struct libnormalform_representation_spec *spec)
{
	LIBNORMALFORM_SENTENCE *true_obj = NULL;
	LIBNORMALFORM_SENTENCE *false_obj = NULL;
	LIBNORMALFORM_SENTENCE **references = NULL;
	size_t nreferences = 0;
	LIBNORMALFORM_SENTENCE *ret;
	while (isspace(*s))
		s++;
	ret = from_string(s, end_out, spec, &true_obj, &false_obj, &references, &nreferences);
	free(references);
	return ret;
}


#undef OPT_SPACE
#undef LEFT_BRACKET
#undef COMMA
#undef RIGHT_BRACKET


#else


static struct libnormalform_variable var1 = {.identifier = "var1"};
static struct libnormalform_variable var2 = {.identifier = "var2"};
static struct libnormalform_variable var3 = {.identifier = "var3"};
static struct libnormalform_function fun1 = {.identifier = "fun1"};
static struct libnormalform_function fun2 = {.identifier = "fun2"};
static struct libnormalform_map dom1 = {.identifier = "dom1"};
static struct libnormalform_map dom2 = {.identifier = "dom2"};
static struct libnormalform_transformer trans1 = {.identifier = "trans1"};


static struct libnormalform_variable *
get_variable(char *s, char **end_out, void *user_data)
{
	struct libnormalform_variable *ret;
	(void) user_data;
	if (!strncmp(s, "var1", 4))
		ret = &var1;
	else if (!strncmp(s, "var2", 4))
		ret = &var2;
	else if (!strncmp(s, "var3", 4))
		ret = &var3;
	else
		return NULL;
	*end_out = &s[4];
	return ret;
}


static struct libnormalform_function *
get_function(char *s, char **end_out, void *user_data)
{
	struct libnormalform_function *ret;
	(void) user_data;
	if (!strncmp(s, "fun1", 4))
		ret = &fun1;
	else if (!strncmp(s, "fun2", 4))
		ret = &fun2;
	else
		return NULL;
	*end_out = &s[4];
	return ret;
}


static struct libnormalform_map *
get_map(char *s, char **end_out, void *user_data)
{
	struct libnormalform_map *ret;
	(void) user_data;
	if (!strncmp(s, "dom1", 4))
		ret = &dom1;
	else if (!strncmp(s, "dom2", 4))
		ret = &dom2;
	else
		return NULL;
	*end_out = &s[4];
	return ret;
}


static struct libnormalform_transformer *
get_transformer(char *s, char **end_out, void *user_data)
{
	struct libnormalform_transformer *ret;
	(void) user_data;
	if (!strncmp(s, "trans1", 6))
		ret = &trans1;
	else
		return NULL;
	*end_out = &s[6];
	return ret;
}


static struct libnormalform_representation_spec spec = {
	.get_variable = get_variable,
	.get_function = get_function,
	.get_map = get_map,
	.get_transformer = get_transformer
};


int
main(void)
{
	TEST_BEGIN;

	LIBNORMALFORM_SENTENCE *a, *b;
	char *s, *p;

	ASSUME(s = strdup("AND(VARIABLE(var1), VARIABLE(var2))"));
	ASSUME(a = libnormalform_and2(libnormalform_variable(&var1), libnormalform_variable(&var2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("AND(VARIABLE(var1), VARIABLE(var2))"));
	spec.get_variable = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_variable = &get_variable;
	free(s);

	ASSUME(s = strdup("OR(VARIABLE(var1), VARIABLE(var2))"));
	ASSUME(a = libnormalform_or2(libnormalform_variable(&var1), libnormalform_variable(&var2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("XOR(VARIABLE(var1), VARIABLE(var2))"));
	ASSUME(a = libnormalform_xor2(libnormalform_variable(&var1), libnormalform_variable(&var2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("ALL(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	ASSUME(a = libnormalform_all(&dom1, libnormalform_function(&fun1), libnormalform_function(&fun2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("ALL(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	spec.get_function = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_function = &get_function;
	free(s);

	ASSUME(s = strdup("ANY(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	ASSUME(a = libnormalform_any(&dom1, libnormalform_function(&fun1), libnormalform_function(&fun2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("ANY(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	spec.get_function = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_function = &get_function;
	free(s);

	ASSUME(s = strdup("ONE(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	ASSUME(a = libnormalform_one(&dom1, libnormalform_function(&fun1), libnormalform_function(&fun2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("ONE(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	spec.get_function = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_function = &get_function;
	free(s);

	ASSUME(s = strdup("NOT(ONE(dom1, TRUE, FALSE))"));
	ASSUME(a = libnormalform_not(libnormalform_one(&dom1, libnormalform_true(), libnormalform_false())));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("NOT(ONE(dom1, FUNCTION(fun1), FUNCTION(fun2)))"));
	spec.get_function = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_function = &get_function;
	free(s);

	ASSUME(s = strdup("  XNOR(VARIABLE(var1), VARIABLE(var2))"));
	ASSUME(a = libnormalform_xnor2(libnormalform_variable(&var1), libnormalform_variable(&var2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("IF(VARIABLE(var1), VARIABLE(var2))  "));
	ASSUME(a = libnormalform_if2(libnormalform_variable(&var1), libnormalform_variable(&var2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("IMPLY ( VARIABLE ( var1 )  ,   VARIABLE  (  var2  )  )"));
	ASSUME(a = libnormalform_imply2(libnormalform_variable(&var1), libnormalform_variable(&var2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("\nNIF(VARIABLE(var1),VARIABLE(var2))\t"));
	ASSUME(a = libnormalform_nif2(libnormalform_variable(&var1), libnormalform_variable(&var2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("\tNIMPLY(VARIABLE(var1)\n,\t VARIABLE(var2))\n"));
	ASSUME(a = libnormalform_nimply2(libnormalform_variable(&var1), libnormalform_variable(&var2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("EXISTS(dom1, FUNCTION(fun1))"));
	ASSUME(a = libnormalform_exists(&dom1, libnormalform_function(&fun1)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("NEXISTS(dom1, FUNCTION(fun1))"));
	ASSUME(a = libnormalform_nexists(&dom1, libnormalform_function(&fun1)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("UNIQUE(dom2, FUNCTION(fun2))"));
	ASSUME(a = libnormalform_unique(&dom2, libnormalform_function(&fun2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("EXISTENTIALLY(dom1, FUNCTION(fun1))"));
	ASSUME(a = libnormalform_existentially(&dom1, libnormalform_function(&fun1)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("UNIVERSALLY(dom1, FUNCTION(fun1))"));
	ASSUME(a = libnormalform_universally(&dom1, libnormalform_function(&fun1)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("UNIQUELY(dom2, FUNCTION(fun2))"));
	ASSUME(a = libnormalform_uniquely(&dom2, libnormalform_function(&fun2)));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("EMPTY(dom1)"));
	ASSUME(a = libnormalform_empty(&dom1));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("NONEMPTY(dom1)"));
	ASSUME(a = libnormalform_nonempty(&dom1));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("SINGLETON(dom2)"));
	ASSUME(a = libnormalform_singleton(&dom2));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("ALL(dom1, FUNCTION@0(fun1), REF(0))"));
	ASSUME(a = libnormalform_function(&fun1));
	ASSUME(b = libnormalform_ref(a));
	ASSUME(a = libnormalform_all(&dom1, a, b));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	free(s);
	ASSERT_EQUAL(a, b);
	ASSERT(a->type == TYPE_ALL);
	ASSERT(b->type == TYPE_ALL);
	ASSERT(a->data.qualifier.antecedent->refcount == 2);
	ASSERT(a->data.qualifier.predicate->refcount == 2);
	ASSERT(a->data.qualifier.antecedent == a->data.qualifier.predicate);
	ASSERT(b->data.qualifier.antecedent->refcount == 2);
	ASSERT(b->data.qualifier.predicate->refcount == 2);
	ASSERT(b->data.qualifier.antecedent == b->data.qualifier.predicate);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("ALL(dom1, VARIABLE(var1), FALSE)"));
	ASSUME(a = libnormalform_from_string(s, NULL, &spec));
	libnormalform_free(a);
	free(s);

	ASSUME(s = strdup("ALL(dom1, ZZRIABLE(var1), FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, VARIABLE(var1), FALSE) X"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, VARIABLE(var1), FALSE) X"));
	ASSERT(a = libnormalform_from_string(s, &p, &spec));
	libnormalform_free(a);
	ASSERT(!strcmp(p, " X"));
	free(s);

	ASSUME(s = strdup("ALL(dom1, VARIABLE(var1), FALSE"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("AL"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, VARIABLE(var1), FALSE,"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, VARIABLE(var1) FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1 VARIABLE(var1), FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, REF(0), FUNCTION@0(fun1))"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, FUNCTION@1(fun1), FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, REF(2), FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, AND@0(VARIABLE(var1), REF(0)), FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EINVAL);
	free(s);

	ASSUME(s = strdup("ALL(dom1, VARIABLE(varx), FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == 1);
	free(s);

	ASSUME(s = strdup("ALL(dom1, FUNCTION(funx), FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == 1);
	free(s);

	ASSUME(s = strdup("ALL(domx, VARIABLE(var1), FALSE)"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == 0);
	errno = 1;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == 1);
	free(s);

	ASSUME(s = strdup("ALL(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	spec.get_map = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_map = &get_map;
	free(s);

	ASSUME(s = strdup("ANY(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	spec.get_map = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_map = &get_map;
	free(s);

	ASSUME(s = strdup("ONE(dom1, FUNCTION(fun1), FUNCTION(fun2))"));
	spec.get_map = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_map = &get_map;
	free(s);

	ASSUME(s = strdup("NOT(ONE(dom1, FUNCTION(fun1), FUNCTION(fun2)))"));
	spec.get_map = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_map = &get_map;
	free(s);

	ASSUME(s = strdup("AND()"));
	errno = 0;
	ASSUME(a = libnormalform_from_string(s, NULL, &spec));
	ASSERT(a->type == TYPE_TRUE);
	libnormalform_free(a);
	free(s);

	ASSUME(s = strdup("OR()"));
	errno = 0;
	ASSUME(a = libnormalform_from_string(s, NULL, &spec));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);
	free(s);

	ASSUME(s = strdup("XOR()"));
	errno = 0;
	ASSUME(a = libnormalform_from_string(s, NULL, &spec));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);
	free(s);

	ASSUME(s = strdup("XNOR()"));
	errno = 0;
	ASSUME(a = libnormalform_from_string(s, NULL, &spec));
	ASSERT(a->type == TYPE_TRUE);
	libnormalform_free(a);
	free(s);

	ASSUME(s = strdup("IMPLY()"));
	errno = 0;
	ASSUME(a = libnormalform_from_string(s, NULL, &spec));
	ASSERT(a->type == TYPE_TRUE);
	libnormalform_free(a);
	free(s);

	ASSUME(s = strdup("NIF()"));
	errno = 0;
	ASSUME(a = libnormalform_from_string(s, NULL, &spec));
	ASSERT(a->type == TYPE_FALSE);
	libnormalform_free(a);
	free(s);

	ASSUME(s = strdup("NIMPLY()"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EDOM);
	free(s);

	ASSUME(s = strdup("IF()"));
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == EDOM);
	free(s);

	ASSUME(s = strdup("XOR(ALL(dom1, TRUE, FALSE), ALL(dom2, TRUE, FALSE))"));
	ASSUME(a = libnormalform_all(&dom1, libnormalform_true(), libnormalform_false()));
	ASSUME(b = libnormalform_all(&dom2, libnormalform_true(), libnormalform_false()));
	ASSUME(a = libnormalform_xor2(a, b));
	ASSUME(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	ASSUME(s = strdup("TRANSFORMATION(trans1, FUNCTION(fun1))"));
	spec.get_transformer = NULL;
	errno = 0;
	ASSERT(!libnormalform_from_string(s, NULL, &spec) && errno == ENOENT);
	spec.get_transformer = &get_transformer;
	free(s);

	ASSUME(s = strdup("TRANSFORMATION(trans1, FUNCTION(fun1))"));
	ASSUME(a = libnormalform_transformation(&trans1, libnormalform_function(&fun1)));
	ASSERT(b = libnormalform_from_string(s, NULL, &spec));
	ASSERT_EQUAL(a, b);
	free(s);
	libnormalform_free(a);
	libnormalform_free(b);

	TEST_END;
}


#endif