1 files changed, 123 insertions, 0 deletions
diff --git a/libnormalform_free.c b/libnormalform_free.c
new file mode 100644
index 0000000..3bce4df
--- /dev/null
+++ b/libnormalform_free.c
@@ -0,0 +1,123 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+/**
+ * Recursively deallocate a `LIBNORMALFORM_SENTENCE *`
+ * according to `libnormalform_free`
+ *
+ * @param  this  The object to deallocate
+ */
+NONNULL_INPUT static void
+free_sentence(LIBNORMALFORM_SENTENCE *this)
+{
+	LIBNORMALFORM_SENTENCE *head = NULL, *a, *b;
+
+	if (--this->refcount)
+		return;
+
+	do {
+		if (this->atom && !--this->atom->refcount)
+			free(this->atom);
+
+		if (IS_BRANCH(this)) {
+			a = LEFT(this);
+			b = RIGHT(this);
+			if (b && !--b->refcount)
+				PUSH(&head, b);
+		push_a:
+			if (a && !--a->refcount)
+				PUSH(&head, a);
+		} else if (this->type == TYPE_TRANS) {
+			a = this->data.trans.input;
+			goto push_a;
+		}
+
+		free(this);
+	} while (POP(&head, &this));
+}
+
+
+/**
+ * Recursively deallocate a `LIBNORMALFORM_SENTENCE *`
+ * according to `libnormalform_free`, but do not
+ * deallocate the pointer itself
+ *
+ * @param  this  The object to deallocate
+ */
+NONNULL_INPUT static void
+destroy_term(struct libnormalform_term *this)
+{
+	switch (this->type) {
+	case LIBNORMALFORM_DISJUNCTION:
+	case LIBNORMALFORM_CONJUNCTION:
+	case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION:
+		while (this->term.clause.nterms)
+			destroy_term(&this->term.clause.terms[--this->term.clause.nterms]);
+		free(this->term.clause.terms);
+		free(this);
+		break;
+
+	case LIBNORMALFORM_TRANSFORMATION:
+		free(this->term.transformation.sentence);
+		free(this);
+		return;
+
+	case LIBNORMALFORM_FOR_ALL:
+	case LIBNORMALFORM_NEGATED_FOR_ALL:
+	case LIBNORMALFORM_FOR_ANY:
+	case LIBNORMALFORM_NEGATED_FOR_ANY:
+	case LIBNORMALFORM_FOR_ONE:
+	case LIBNORMALFORM_NEGATED_FOR_ONE:
+		destroy_term(this->term.qualification.antecedent);
+		destroy_term(this->term.qualification.predicate);
+		free(this->term.qualification.antecedent);
+		free(this->term.qualification.predicate);
+		/* fall through */
+
+	case LIBNORMALFORM_VARIABLE:
+	case LIBNORMALFORM_NEGATED_VARIABLE:
+	case LIBNORMALFORM_FUNCTION:
+	case LIBNORMALFORM_NEGATED_FUNCTION:
+		free(this);
+		break;
+
+	default:
+		abort();
+	}
+}
+
+
+void
+(libnormalform_free)(void *this)
+{
+	if (!this)
+		return;
+
+	if (*(enum libnormalform_term_type *)this >= SENTENCE_TYPE_OFFSET) {
+		free_sentence(this);
+	} else {
+		destroy_term(this);
+		free(this);
+	}
+}
+
+
+#else
+
+
+int
+main(void)
+{
+	TEST_BEGIN;
+
+	libnormalform_free(NULL);
+
+	/* Tested in other tests */
+
+	TEST_END;
+}
+
+
+#endif