First commit

Signed-off-by: Mattias Andrée <maandree@kth.se>

1 files changed, 452 insertions, 0 deletions

diff --git a/libnormalform_all.c b/libnormalform_all.c
new file mode 100644
index 0000000..1b8d6fc
--- /dev/null
+++ b/libnormalform_all.c
@@ -0,0 +1,452 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+/** 
+ * See `.inverse` in `struct libnormalform_sentence` (FOR ALL implementation)
+ */
+static LIBNORMALFORM_SENTENCE *
+all_inverse(LIBNORMALFORM_SENTENCE *this)
+{
+	/* ¬∀x.φ ⇒ ∃x.¬φ */
+	LIBNORMALFORM_SENTENCE *ret;
+	ret = libnormalform_any(this->data.qualifier.domain,
+	                        libnormalform_ref(this->data.qualifier.antecedent),
+	                        this->data.qualifier.predicate->inverse(this->data.qualifier.predicate));
+        if (ret && this->atom) {
+		ret->atom = this->atom;
+                ret->atom->refcount += 1;
+	}
+	return ret;
+}
+
+
+/** 
+ * See `.equals` in `struct libnormalform_sentence` (FOR ALL implementation)
+ */
+static int
+all_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out)
+{
+	int r, inv_expect;
+
+	if (this->hash != other->hash)
+		return 0;
+
+	if (other->type == TYPE_ALL)
+		inv_expect = 0;
+	else if (other->type == TYPE_ANY)
+		inv_expect = 1;
+	else
+		return 0;
+
+	if (this->data.qualifier.domain != other->data.qualifier.domain)
+		return 0;
+
+	r = this->data.qualifier.antecedent->equals(this->data.qualifier.antecedent, other->data.qualifier.antecedent, inv_out);
+	if (r <= 0)
+		return r;
+	if (*inv_out)
+		return 0;
+
+	r = this->data.qualifier.predicate->equals(this->data.qualifier.predicate, other->data.qualifier.predicate, inv_out);
+	if (r <= 0)
+		return r;
+	if (*inv_out != inv_expect)
+		return 0;
+
+	return r;
+}
+
+
+/** 
+ * See `.evaluate` in `struct libnormalform_sentence` (FOR ALL implementation)
+ */
+static int
+all_evaluate(LIBNORMALFORM_SENTENCE *this, void *input)
+{
+	size_t i, n = this->data.qualifier.domain->nmappings;
+	void *k, *v;
+	int r;
+
+	(void) input;
+
+	for (i = 0; i < n; i++) {
+		k = this->data.qualifier.domain->mappings[i].key;
+		v = this->data.qualifier.domain->mappings[i].value;
+		r = this->data.qualifier.antecedent->evaluate(this->data.qualifier.antecedent, k);
+		if (r <= 0) {
+			if (!r)
+				continue;
+			return r;
+		}
+		r = this->data.qualifier.predicate->evaluate(this->data.qualifier.predicate, v);
+		if (r <= 0)
+			return r;
+	}
+
+	return 1;
+}
+
+
+LIBNORMALFORM_SENTENCE *
+(libnormalform_all)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v)
+{
+	static const struct libnormalform_sentence prototype = {
+		PROTOTYPE_COMMON,
+		.type = TYPE_ALL,
+		.inverse = &all_inverse,
+		.equals = &all_equals,
+		.evaluate = &all_evaluate
+	};
+
+	LIBNORMALFORM_SENTENCE *ret;
+
+	if (!k || !v) {
+		libnormalform_free(k);
+		libnormalform_free(v);
+		return NULL;
+	}
+
+	if (v->type == TYPE_TRUE) {
+		libnormalform_free(k);
+		return v;
+	}
+	if (k->type == TYPE_FALSE) {
+		libnormalform_free(k);
+		libnormalform_free(v);
+		return libnormalform_true();
+	}
+
+	ret = malloc(sizeof(*ret));
+	if (ret) {
+		*ret = prototype;
+		ret->hash = ANY_ALL_HASH(d, k, v);
+		ret->data.qualifier.domain = d;
+		ret->data.qualifier.antecedent = k;
+		ret->data.qualifier.predicate = v;
+	}
+	return ret;
+}
+
+
+#else
+
+
+static int
+evalbool(void *user_data, void *input)
+{
+	int *vp = input;
+	(void) user_data;
+	return *vp;
+}
+
+
+int
+main(void)
+{
+	TEST_BEGIN;
+
+	struct libnormalform_variable var1, var2;
+	struct libnormalform_function fun1;
+	struct libnormalform_map dom1, dom2;
+	struct libnormalform_mapping map[2];
+	struct libnormalform_transformer trans;
+	LIBNORMALFORM_SENTENCE *a, *b, *c, *v1, *v2;
+	int t = 1, f = 0;
+
+	ASSUME(v1 = libnormalform_variable(&var1));
+	ASSUME(v2 = libnormalform_variable(&var2));
+
+	errno = 0;
+	ASSERT(!libnormalform_all(&dom1, NULL, REF(v1)) && errno == 0);
+	errno = 1;
+	ASSERT(!libnormalform_all(&dom1, NULL, REF(v1)) && errno == 1);
+	errno = 0;
+	ASSERT(!libnormalform_all(&dom1, REF(v1), NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!libnormalform_all(&dom1, REF(v1), NULL) && errno == 1);
+	errno = 0;
+	ASSERT(!libnormalform_all(&dom1, NULL, NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!libnormalform_all(&dom1, NULL, NULL) && errno == 1);
+
+	dom1.mappings = map;
+	memset(map, 0, sizeof(map));
+
+	/* ∀x.(⊥ → φ(x)) = ⊤ */
+	ASSUME(a = libnormalform_all(&dom1, libnormalform_false(), REF(v1)));
+	ASSERT(a->type == TYPE_TRUE);
+	libnormalform_free(a);
+
+	/* ∀x.(⊤ → φ(x)) irreducable */
+	ASSUME(a = libnormalform_all(&dom1, libnormalform_true(), REF(v1)));
+	ASSERT(a->type == TYPE_ALL);
+	libnormalform_free(a);
+
+	/* ∀x.(φ(x) → ⊤) = ⊤ */
+	ASSUME(a = libnormalform_all(&dom1, REF(v1), libnormalform_true()));
+	ASSERT(a->type == TYPE_TRUE);
+	libnormalform_free(a);
+
+	/* ∀x.(φ(x) → ⊥) irreducable */
+	ASSUME(a = libnormalform_all(&dom1, REF(v1), libnormalform_false()));
+	ASSERT(a->type == TYPE_ALL);
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_all(&dom1, REF(v1), REF(v2)));
+	ASSERT(a->type == TYPE_ALL);
+	ASSERT(a->refcount == 1);
+
+	dom1.nmappings = 1;
+
+	/* ∀x∈{a}.(⊥ → ⊥) = ⊤ */
+	var1.value = LIBNORMALFORM_FALSE;
+	var2.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∀x∈{a}.(⊥ → ⊤) = ⊤ */
+	var1.value = LIBNORMALFORM_FALSE;
+	var2.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∀x∈{a}.(⊤ → ⊥) = ⊥ */
+	var1.value = LIBNORMALFORM_TRUE;
+	var2.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∀x∈{a}.(⊤ → ⊤) = ⊤ */
+	var1.value = LIBNORMALFORM_TRUE;
+	var2.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	dom1.nmappings = 2;
+
+	/* ∀x∈{a,b}.(⊥ → ⊥) = ⊤ */
+	var1.value = LIBNORMALFORM_FALSE;
+	var2.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∀x∈{a,b}.(⊥ → ⊤) = ⊤ */
+	var1.value = LIBNORMALFORM_FALSE;
+	var2.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∀x∈{a,b}.(⊤ → ⊥) = ⊥ */
+	var1.value = LIBNORMALFORM_TRUE;
+	var2.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∀x∈{a,b}.(⊤ → ⊤) = ⊤ */
+	var1.value = LIBNORMALFORM_TRUE;
+	var2.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	dom1.nmappings = 0;
+
+	/* ∀x∈∅.(⊥ → ⊥) = ⊤ */
+	var1.value = LIBNORMALFORM_FALSE;
+	var2.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∀x∈∅.(⊥ → ⊤) = ⊤ */
+	var1.value = LIBNORMALFORM_FALSE;
+	var2.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∀x∈∅.(⊤ → ⊥) = ⊤ */
+	var1.value = LIBNORMALFORM_TRUE;
+	var2.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∀x∈∅.(⊤ → ⊤) = ⊤ */
+	var1.value = LIBNORMALFORM_TRUE;
+	var2.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	dom1.nmappings = 0;
+
+	libnormalform_free(a);
+
+	fun1.evaluate = &evalbool;
+	dom1.nmappings = 2;
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(a = libnormalform_all(&dom1, libnormalform_true(), a));
+	ASSERT(a->type == TYPE_ALL);
+	map[0].key = NULL;
+	map[1].key = NULL;
+
+	/* ∀x∈{⊥, ⊥}.(⊤ → x) = ⊥ */
+	map[0].value = &f;
+	map[1].value = &f;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∀x∈{⊥, ⊤}.(⊤ → x) = ⊥ */
+	map[0].value = &f;
+	map[1].value = &t;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∀x∈{⊤, ⊥}.(⊤ → x) = ⊥ */
+	map[0].value = &t;
+	map[1].value = &f;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∀x∈{⊤, ⊤}.(⊤ → x) = ⊤ */
+	map[0].value = &t;
+	map[1].value = &t;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_function(&fun1));
+	ASSUME(a = libnormalform_all(&dom1, a, libnormalform_false()));
+	ASSERT(a->type == TYPE_ALL);
+	map[0].value = NULL;
+	map[1].value = NULL;
+
+	/* ∀x∈{⊥, ⊥}.(x → ⊥) = ⊤ */
+	map[0].key = &f;
+	map[1].key = &f;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∀x∈{⊥, ⊤}.(x → ⊥) = ⊥ */
+	map[0].key = &f;
+	map[1].key = &t;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∀x∈{⊤, ⊥}.(x → ⊥) = ⊥ */
+	map[0].key = &t;
+	map[1].key = &f;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∀x∈{⊤, ⊤}.(x → ⊥) = ⊥ */
+	map[0].key = &t;
+	map[1].key = &t;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_all(&dom1, REF(v1), REF(v2)));
+
+	/* ∀x∈X.(P(x) → Q(x)) = ∀x∈X.(P(x) → Q(x)) */
+	ASSUME(b = libnormalform_all(&dom1, REF(v1), REF(v2)));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from ∀x∈X.(Q(x) → P(x)) */
+	ASSUME(b = libnormalform_all(&dom1, REF(v2), REF(v1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from ∀x∈Y.(P(x) → Q(x)) */
+	ASSUME(b = libnormalform_all(&dom2, REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) = ¬(∃x∈X.(P(x) → ¬Q(x))) */
+	ASSUME(b = libnormalform_any(&dom1, REF(v1), libnormalform_not(REF(v2))));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ¬∀x∈X.(P(x) → Q(x)) = ∃x∈X.(P(x) → ¬Q(x)) */
+	ASSUME(c = libnormalform_not(REF(a)));
+	ASSUME(b = libnormalform_any(&dom1, REF(v1), libnormalform_not(REF(v2))));
+	ASSERT_EQUAL(c, b);
+	ASSERT(c->type == TYPE_ANY);
+	libnormalform_free(b);
+	libnormalform_free(c);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from TRUE */
+	ASSUME(b = libnormalform_true());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from FALSE */
+	ASSUME(b = libnormalform_false());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from variable1 */
+	ASSUME(b = libnormalform_variable(&var1));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from NOT variable1 */
+	ASSUME(b = libnormalform_not(libnormalform_variable(&var1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from function1 */
+	ASSUME(b = libnormalform_function(&fun1));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from NOT function1 */
+	ASSUME(b = libnormalform_not(libnormalform_function(&fun1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from T(function1) */
+	ASSUME(b = libnormalform_transformation(&trans, libnormalform_function(&fun1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from ∃x∈X.(P(x) → Q(x)) */
+	ASSUME(b = libnormalform_any(&dom1, REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from ∃!x∈X.(P(x) → Q(x)) */
+	ASSUME(b = libnormalform_one(&dom1, REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from ¬∃!x∈X.(P(x) → Q(x)) */
+	ASSUME(b = libnormalform_not(b));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from AND (P, Q) */
+	ASSUME(b = libnormalform_and2(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from OR (P, Q) */
+	ASSUME(b = libnormalform_or2(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∀x∈X.(P(x) → Q(x)) independent from XOR (P, Q) */
+	ASSUME(b = libnormalform_xor2(REF(v1), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* P = Q ⊭ ∀{x,y}∈X.(P(x) → Q(y)) = ∀{x,y}∈X.(P(x) → P(y)) = ∀{x,y}∈X.⊤ = ⊤ ∵ P → Q ⊭ P(x) → Q(y) */
+	ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), libnormalform_true()));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+	ASSUME(b = libnormalform_true());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* P = ¬Q ⊭ ∀{x,y}∈X.(P(x) → Q(y)) = ∀{x,y}∈X.(¬Q(x) → Q(y)) = ∀{x,y}∈X.(⊤ → Q(y)) ∵ P → ¬Q ⊭ P(x) → ¬Q(y) */
+	/* P = ¬Q ⊭ ∀{x,y}∈X.(P(x) → Q(y)) = ∀{x,y}∈X.(P(x) → ¬P(y)) = ∀{x,y}∈X.(⊤ → ¬P(y)) ∵ P → ¬Q ⊭ P(x) → ¬Q(y) */
+	ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), REF(v2)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+	ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), libnormalform_not(REF(v1))));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	libnormalform_free(a);
+
+	libnormalform_free(v1);
+	libnormalform_free(v2);
+
+	/* cascading of evaluation failure is tested in libnormalform_function.c */
+
+	TEST_END;
+}
+
+
+#endif