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