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


/**
 * Check whether inverting a sentence would require
 * it to be relaxes before it can be represented
 *
 * @param   this  The sentence to check
 * @param   flags  Flags from `libnormalform_express`
 * @return         1 if the inversion can be exactly represented,
 *                 0 if the inversion requires relaxation be
 */
PURE static int
inversion_would_relax(struct expression *this, uint64_t flags)
{
	size_t i;

beginning:
	switch (this->type) {
	case LIBNORMALFORM_CONJUNCTION:
	case LIBNORMALFORM_DISJUNCTION:
		for (i = 0; i < this->nterms; i++)
			if (inversion_would_relax(this->terms[i], flags))
				return 1;
		return 0;

	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
		for (i = 0; i < this->nterms; i++)
			if (!inversion_would_relax(this->terms[i], flags))
				return 0;
		return 1;

	case LIBNORMALFORM_VARIABLE:
		return flags & LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE;

	case LIBNORMALFORM_NEGATED_VARIABLE:
		return flags & LIBNORMALFORM_ELIMINATE_VARIABLE;

	case LIBNORMALFORM_FUNCTION:
		return flags & LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION;

	case LIBNORMALFORM_NEGATED_FUNCTION:
		return flags & LIBNORMALFORM_ELIMINATE_FUNCTION;

	case LIBNORMALFORM_TRANSFORMATION:
		this = this->terms[0];
		goto beginning;

	case LIBNORMALFORM_FOR_ALL:
		if (!(flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL))
			return 0;
		if (flags & LIBNORMALFORM_ELIMINATE_FOR_ANY)
			return 1;
		this = this->terms[this->nterms - 1];
		goto beginning;

	case LIBNORMALFORM_NEGATED_FOR_ALL:
		if (!(flags & LIBNORMALFORM_ELIMINATE_FOR_ALL))
			return 0;
		if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY)
			return 1;
		this = this->terms[this->nterms - 1];
		goto beginning;

	case LIBNORMALFORM_FOR_ANY:
		if (!(flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY))
			return 0;
		if (flags & LIBNORMALFORM_ELIMINATE_FOR_ALL)
			return 1;
		this = this->terms[this->nterms - 1];
		goto beginning;

	case LIBNORMALFORM_NEGATED_FOR_ANY:
		if (!(flags & LIBNORMALFORM_ELIMINATE_FOR_ANY))
			return 0;
		if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL)
			return 1;
		this = this->terms[this->nterms - 1];
		goto beginning;

	case LIBNORMALFORM_FOR_ONE:
		return flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE;

	case LIBNORMALFORM_NEGATED_FOR_ONE:
		return flags & LIBNORMALFORM_ELIMINATE_FOR_ONE;

	default:
		abort();
	}
}


int
(libnormalform_fix_presentation__)(struct expression *this, uint64_t flags, unsigned char *require_inversion, int *reduced)
{
#define WILL_ELIMINATE(BASETYPE, INVERT)\
	(flags & (LIBNORMALFORM_ELIMINATE_##BASETYPE <<\
	          ((this->type ^ ((LIBNORMALFORM_##BASETYPE ^ LIBNORMALFORM_NEGATED_##BASETYPE) *\
	                          (INVERT))) -\
	           LIBNORMALFORM_##BASETYPE)))

	size_t i;
	unsigned char zero = 0;
	struct expression *new;
	int may_switch = 1;

	switch (this->type) {
	case LIBNORMALFORM_CONJUNCTION:
	case LIBNORMALFORM_DISJUNCTION:
		this->type ^= LIBNORMALFORM_CONJUNCTION ^ LIBNORMALFORM_DISJUNCTION;
		if (this->invert) {
			if (*require_inversion) {
				this->invert ^= 1;
				*require_inversion = 0;
			}
			for (i = 0; i < this->nterms; i++)
				this->terms[i]->invert ^= 1;
		}
		require_inversion = &zero;
		break;

	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
		if (!this->nterms)
			abort();
		if (*require_inversion) { /* TODO always? */
			this->invert ^= 1;
			*require_inversion = 0;
		}
		for (i = 0; i < this->nterms; i++)
			if (libnormalform_fix_presentation__(this->terms[i], flags, &this->invert, reduced))
				return -1;
		if (this->invert) {
			/* TODO this is not necessarily the best element to invert,
			 *      possibly the previous loop could be used to determine
			 *      which is best (notably, clauses are not analysed) */
			this->invert = 0;
			this->terms[0]->invert ^= 1;
			if (libnormalform_fix_presentation__(this->terms[0], flags, &zero, reduced))
				return -1;
		}
		return 0;

	case LIBNORMALFORM_VARIABLE:
	case LIBNORMALFORM_NEGATED_VARIABLE:
		if (!WILL_ELIMINATE(VARIABLE, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else if (WILL_ELIMINATE(VARIABLE, this->invert)) {
			goto eliminate;
		}
		this->type ^= (LIBNORMALFORM_VARIABLE ^ LIBNORMALFORM_NEGATED_VARIABLE) * this->invert;
		break;

	case LIBNORMALFORM_FUNCTION:
	case LIBNORMALFORM_NEGATED_FUNCTION:
		if (!WILL_ELIMINATE(FUNCTION, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else if (WILL_ELIMINATE(FUNCTION, this->invert)) {
			goto eliminate;
		}
		this->type ^= (LIBNORMALFORM_FUNCTION ^ LIBNORMALFORM_NEGATED_FUNCTION) * this->invert;
		break;

	case LIBNORMALFORM_TRANSFORMATION:
		this->terms[0]->invert ^= this->invert;
		break;

	case LIBNORMALFORM_FOR_ALL:
	case LIBNORMALFORM_NEGATED_FOR_ALL:
		if (!WILL_ELIMINATE(FOR_ALL, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else for_all: if (WILL_ELIMINATE(FOR_ALL, this->invert)) {
			if (!may_switch)
				goto eliminate;
			may_switch = 0;
			this->invert = 0;
			this->terms[this->nterms - 1]->invert ^= 1;
			this->type = LIBNORMALFORM_NEGATED_FOR_ANY - (this->type - LIBNORMALFORM_FOR_ALL);
			goto for_any;
		}
		this->type ^= (LIBNORMALFORM_FOR_ALL ^ LIBNORMALFORM_NEGATED_FOR_ALL) * this->invert;
		this->invert = 0;
		if (flags & (LIBNORMALFORM_AVOID_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL))) {
			if (!inversion_would_relax(this, flags)) {
				this->terms[this->nterms - 1]->invert ^= 1;
				this->type = LIBNORMALFORM_NEGATED_FOR_ANY - (this->type - LIBNORMALFORM_FOR_ALL);
				goto for_any_maybe_join_sides;
			}
		}
	for_all_maybe_join_sides:
		if (this->nterms > 1)
			break;
		if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL)))
			goto for_all_join_sides;
		break;

	case LIBNORMALFORM_FOR_ANY:
	case LIBNORMALFORM_NEGATED_FOR_ANY:
		if (!WILL_ELIMINATE(FOR_ANY, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else for_any: if (WILL_ELIMINATE(FOR_ANY, this->invert)) {
			if (!may_switch)
				goto eliminate;
			may_switch = 0;
			this->invert = 0;
			this->terms[this->nterms - 1]->invert ^= 1;
			this->type = LIBNORMALFORM_NEGATED_FOR_ALL - (this->type - LIBNORMALFORM_FOR_ANY);
			goto for_all;
		}
		this->type ^= (LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY) * this->invert;
		this->invert = 0;
		if (flags & (LIBNORMALFORM_AVOID_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY))) {
			if (!inversion_would_relax(this, flags)) {
				this->terms[this->nterms - 1]->invert ^= 1;
				this->type = LIBNORMALFORM_NEGATED_FOR_ALL - (this->type - LIBNORMALFORM_FOR_ANY);
				goto for_all_maybe_join_sides;
			}
		}
	for_any_maybe_join_sides:
		if (this->nterms > 1)
			break;
		if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY)))
			goto for_any_join_sides;
		break;

	case LIBNORMALFORM_FOR_ONE:
	case LIBNORMALFORM_NEGATED_FOR_ONE:
		if (!WILL_ELIMINATE(FOR_ONE, this->invert ^ *require_inversion)) {
			this->invert ^= *require_inversion;
			*require_inversion = 0;
		} else if (WILL_ELIMINATE(FOR_ONE, this->invert)) {
			this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert;
			if (this->type == LIBNORMALFORM_FOR_ONE) {
				this->invert = 0;
				this->reduced = 1;
				*reduced = 1;
				goto for_any;
			}
			goto eliminate;
		}
		this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert;
		if (this->type == LIBNORMALFORM_FOR_ONE) {
			if (flags & LIBNORMALFORM_ELIMINATE_FOR_ONE) {
				this->type = LIBNORMALFORM_FOR_ANY;
				this->invert = 0;
				this->reduced = 1;
				*reduced = 1;
				goto for_any;
			}
		}
		if (this->nterms > 1)
			break;
		if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE << (this->type - LIBNORMALFORM_FOR_ONE)))
			goto for_any_join_sides;
		break;

	default:
		abort();
	}

	this->invert = 0;

	for (i = 0; i < this->nterms; i++)
		if (libnormalform_fix_presentation__(this->terms[i], flags, require_inversion, reduced))
			return -1;

	return 0;

eliminate:
	*require_inversion = 0;
	this->refcount = 1;
	this->reduced = 1;
	this->invert = 0;
	while (this->nterms)
		libnormalform_free_expression__(this->terms[--this->nterms]);
	free(this->terms);
	this->terms = NULL;
	this->type = LIBNORMALFORM_CONJUNCTION;
	*reduced = 1;
	return 0;

for_all_join_sides:
	new = libnormalform_make_binary__(1, this->terms[0], 0, this->terms[1], LIBNORMALFORM_DISJUNCTION);
	goto join_sides;

for_any_join_sides:
	new = libnormalform_make_binary__(0, this->terms[0], 0, this->terms[1], LIBNORMALFORM_CONJUNCTION);
join_sides:
	if (!new)
		return -1;
	this->terms[0] = new;
	this->nterms--;
	if (libnormalform_apply_transformation__(this->terms[0]->terms[0], LIBNORMALFORM_DOMAIN_VIEW))
		return -1;
	if (libnormalform_apply_transformation__(this->terms[0]->terms[1], LIBNORMALFORM_IMAGE_VIEW))
		return -1;
	*reduced = 1;
	return 0;

#undef WILL_ELIMINATE
}


#else

TODO_TEST

#endif