First commit

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

1 files changed, 243 insertions, 0 deletions

diff --git a/libnormalform_exists.c b/libnormalform_exists.c
new file mode 100644
index 0000000..0c40729
--- /dev/null
+++ b/libnormalform_exists.c
@@ -0,0 +1,243 @@
+/* See LICENSE file for copyright and license details. */
+#include "common.h"
+#ifndef TEST
+
+
+extern inline LIBNORMALFORM_SENTENCE *(libnormalform_exists)(struct libnormalform_map *, LIBNORMALFORM_SENTENCE *);
+
+
+#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;
+	struct libnormalform_function fun1;
+	struct libnormalform_map dom1, dom2;
+	struct libnormalform_mapping map[3];
+	struct libnormalform_transformer trans;
+	LIBNORMALFORM_SENTENCE *a, *b, *c, *v1;
+	int t = 1, f = 0;
+
+	ASSUME(v1 = libnormalform_variable(&var1));
+
+	errno = 0;
+	ASSERT(!libnormalform_exists(&dom1, NULL) && errno == 0);
+	errno = 1;
+	ASSERT(!libnormalform_exists(&dom1, NULL) && errno == 1);
+
+	dom1.mappings = map;
+	memset(map, 0, sizeof(map));
+
+	/* ∃x.⊥ = ⊥ */
+	ASSUME(a = libnormalform_exists(&dom1, libnormalform_false()));
+	ASSERT(a->type == TYPE_FALSE);
+	libnormalform_free(a);
+
+	/* ∃x.φ irreducable */
+	ASSUME(a = libnormalform_exists(&dom1, REF(v1)));
+	ASSERT(a->type == TYPE_ANY);
+	libnormalform_free(a);
+
+	/* ∃x.⊤ irreducable */
+	ASSUME(a = libnormalform_exists(&dom1, libnormalform_true()));
+	ASSERT(a->type == TYPE_ANY);
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_exists(&dom1, REF(v1)));
+	ASSERT(a->type == TYPE_ANY);
+	ASSERT(a->refcount == 1);
+
+	dom1.nmappings = 1;
+
+	/* ∃x∈{a}.⊥ = ⊥ */
+	var1.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∃x∈{a}.⊤ = ⊤ */
+	var1.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	dom1.nmappings = 2;
+
+	/* ∃x∈{a,b}.⊥ = ⊥ */
+	var1.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∃x∈{a,b}.⊤ = ⊤ */
+	var1.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	dom1.nmappings = 0;
+
+	/* ∃x∈∅.⊥ = ⊥ */
+	var1.value = LIBNORMALFORM_FALSE;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∃x∈∅.⊤ = ⊥ */
+	var1.value = LIBNORMALFORM_TRUE;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	dom1.nmappings = 0;
+
+	libnormalform_free(a);
+
+	fun1.evaluate = &evalbool;
+	dom1.nmappings = 2;
+
+	ASSUME(a = libnormalform_exists(&dom1, libnormalform_function(&fun1)));
+	ASSERT(a->type == TYPE_ANY);
+	map[0].value = NULL;
+	map[1].value = NULL;
+
+	/* ∃x∈{⊥, ⊥}.x = ⊥ */
+	map[0].key = &f;
+	map[1].key = &f;
+	ASSERT(libnormalform_evaluate(a) == 0);
+
+	/* ∃x∈{⊥, ⊤}.x = ⊤ */
+	map[0].key = &f;
+	map[1].key = &t;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∃x∈{⊤, ⊥}.x = ⊤ */
+	map[0].key = &t;
+	map[1].key = &f;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∃x∈{⊤, ⊤}.x = ⊤ */
+	map[0].key = &t;
+	map[1].key = &t;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	/* ∃x∈{⊤, ⊤, ⊤}.x = ⊤ */
+	map[0].key = &t;
+	map[1].key = &t;
+	map[2].key = &t;
+	ASSERT(libnormalform_evaluate(a) == 1);
+
+	libnormalform_free(a);
+
+	ASSUME(a = libnormalform_exists(&dom1, REF(v1)));
+
+	/* ∃x∈X.P(x) = ∃x∈X.(P(x) ∧ ⊤) */
+	ASSUME(b = libnormalform_any(&dom1, REF(v1), libnormalform_true()));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from ∃x∈X.Q(x) */
+	ASSUME(b = libnormalform_exists(&dom1, libnormalform_function(&fun1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from ∃x∈Y.P(x)) */
+	ASSUME(b = libnormalform_exists(&dom2, REF(v1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) = ¬(∀x∈X.(P(x) → ⊥)) */
+	ASSUME(b = libnormalform_all(&dom1, REF(v1), libnormalform_false()));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ¬∃x∈X.P(x) = ∀x∈X.(P(x) → ⊥) */
+	ASSUME(c = libnormalform_not(REF(a)));
+	ASSUME(b = libnormalform_all(&dom1, REF(v1), libnormalform_false()));
+	ASSERT_EQUAL(c, b);
+	ASSERT(c->type == TYPE_ALL);
+	libnormalform_free(b);
+	libnormalform_free(c);
+
+	/* ∃x∈X.P(x) independent from TRUE */
+	ASSUME(b = libnormalform_true());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from FALSE */
+	ASSUME(b = libnormalform_false());
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from variable1 */
+	ASSUME(b = libnormalform_variable(&var1));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from NOT variable1 */
+	ASSUME(b = libnormalform_not(libnormalform_variable(&var1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from function1 */
+	ASSUME(b = libnormalform_function(&fun1));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from NOT function1 */
+	ASSUME(b = libnormalform_not(libnormalform_function(&fun1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from T(function1) */
+	ASSUME(b = libnormalform_transformation(&trans, libnormalform_function(&fun1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from ∀x∈X.(P(x) → ⊤) */
+	ASSUME(b = libnormalform_all(&dom1, REF(v1), libnormalform_true()));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from ∃!x∈X.(P(x) ∧ ⊤) */
+	ASSUME(b = libnormalform_one(&dom1, REF(v1), libnormalform_true()));
+	ASSERT_NOTEQUAL(a, b);
+
+	/* ∃x∈X.P(x) independent from ¬∃!x∈X.(P(x) ∧ ⊤) */
+	ASSUME(b = libnormalform_not(b));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from AND (P, P) */
+	ASSUME(b = libnormalform_and2__(REF(v1), REF(v1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(X) independent from OR (P, P) */
+	ASSUME(b = libnormalform_or2__(REF(v1), REF(v1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) independent from XOR (P, P) */
+	ASSUME(b = libnormalform_xor2__(REF(v1), REF(v1)));
+	ASSERT_NOTEQUAL(a, b);
+	libnormalform_free(b);
+
+	/* ∃x∈X.P(x) = ¬∄x∈X.P(x) */
+	ASSUME(b = libnormalform_nexists(&dom1, REF(v1)));
+	ASSERT_INVEQUAL(a, b);
+	libnormalform_free(b);
+	ASSUME(b = libnormalform_not(libnormalform_nexists(&dom1, REF(v1))));
+	ASSERT_EQUAL(a, b);
+	libnormalform_free(b);
+
+	libnormalform_free(a);
+
+	libnormalform_free(v1);
+
+	TEST_END;
+}
+
+
+#endif