diff options
Diffstat (limited to 'libnormalform_exists.c')
| -rw-r--r-- | libnormalform_exists.c | 243 |
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 |