diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_existentially.c | 235 |
1 files changed, 235 insertions, 0 deletions
diff --git a/libnormalform_existentially.c b/libnormalform_existentially.c new file mode 100644 index 0000000..16ff9fa --- /dev/null +++ b/libnormalform_existentially.c @@ -0,0 +1,235 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +extern inline LIBNORMALFORM_SENTENCE *(libnormalform_existentially)(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_existentially(&dom1, NULL) && errno == 0); + errno = 1; + ASSERT(!libnormalform_existentially(&dom1, NULL) && errno == 1); + + dom1.mappings = map; + memset(map, 0, sizeof(map)); + + /* ∃x.⊥ = ⊥ */ + ASSUME(a = libnormalform_existentially(&dom1, libnormalform_false())); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* ∃x.φ irreducable */ + ASSUME(a = libnormalform_existentially(&dom1, REF(v1))); + ASSERT(a->type == TYPE_ANY); + libnormalform_free(a); + + /* ∃x.⊤ irreducable */ + ASSUME(a = libnormalform_existentially(&dom1, libnormalform_true())); + ASSERT(a->type == TYPE_ANY); + libnormalform_free(a); + + ASSUME(a = libnormalform_existentially(&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_existentially(&dom1, libnormalform_function(&fun1))); + ASSERT(a->type == TYPE_ANY); + 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) == 1); + + /* ∃x∈{⊤, ⊥}.x = ⊤ */ + map[0].value = &t; + map[1].value = &f; + ASSERT(libnormalform_evaluate(a) == 1); + + /* ∃x∈{⊤, ⊤}.x = ⊤ */ + map[0].value = &t; + map[1].value = &t; + ASSERT(libnormalform_evaluate(a) == 1); + + /* ∃x∈{⊤, ⊤, ⊤}.x = ⊤ */ + map[0].value = &t; + map[1].value = &t; + map[2].value = &t; + ASSERT(libnormalform_evaluate(a) == 1); + + libnormalform_free(a); + + ASSUME(a = libnormalform_existentially(&dom1, REF(v1))); + + /* ∃x∈X.P(x) = ∃x∈X.(⊤ ∧ P(x)) */ + ASSUME(b = libnormalform_any(&dom1, libnormalform_true(), REF(v1))); + ASSERT_EQUAL(a, b); + libnormalform_free(b); + + /* ∃x∈X.P(x) independent from ∃x∈X.Q(x) */ + ASSUME(b = libnormalform_existentially(&dom1, libnormalform_function(&fun1))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + /* ∃x∈X.P(x) independent from ∃x∈Y.P(x)) */ + ASSUME(b = libnormalform_existentially(&dom2, REF(v1))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + /* ∃x∈X.P(x) = ¬(∀x∈X.(⊤ → ¬P(x))) */ + ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), libnormalform_not(REF(v1)))); + 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, libnormalform_true(), libnormalform_not(REF(v1)))); + 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, libnormalform_true(), REF(v1))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + /* ∃x∈X.P(x) independent from ∃!x∈X.(⊤ ∧ P(x)) */ + ASSUME(b = libnormalform_one(&dom1, libnormalform_true(), REF(v1))); + 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); + + libnormalform_free(a); + + libnormalform_free(v1); + + TEST_END; +} + + +#endif |