diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_one.c | 449 |
1 files changed, 449 insertions, 0 deletions
diff --git a/libnormalform_one.c b/libnormalform_one.c new file mode 100644 index 0000000..b5c17f1 --- /dev/null +++ b/libnormalform_one.c @@ -0,0 +1,449 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +/** + * See `.inverse` in `struct libnormalform_sentence` (FOR ONE implementation) + */ +static LIBNORMALFORM_SENTENCE * +one_inverse(LIBNORMALFORM_SENTENCE *this) +{ + /* ¬∃x.φ ⇒ ∀x.¬φ */ + LIBNORMALFORM_SENTENCE *ret; + ret = libnormalform_one(this->data.qualifier.domain, + libnormalform_ref(this->data.qualifier.antecedent), + libnormalform_ref(this->data.qualifier.predicate)); + if (ret) { + if (this->atom) { + ret->atom = this->atom; + ret->atom->refcount += 1; + } + ret->type = TYPE_ONE ^ TYPE_NOT_ONE ^ this->type; + } + return ret; +} + + +/** + * See `.equals` in `struct libnormalform_sentence` (FOR ONE implementation) + */ +static int +one_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out) +{ + int r; + + if (this->hash != other->hash) + return 0; + + if (other->type != TYPE_ONE && other->type != TYPE_NOT_ONE) + 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) + return 0; + + *inv_out = this->type != other->type; + return r; +} + + +/** + * See `.evaluate` in `struct libnormalform_sentence` (FOR ONE implementation) + */ +static int +one_evaluate(LIBNORMALFORM_SENTENCE *this, void *input) +{ + size_t i, n = this->data.qualifier.domain->nmappings; + void *k, *v; + int r, ret = 0; + + (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) { + if (r < 0) + return r; + if (++ret == 2) + return this->type == TYPE_NOT_ONE; + } + } + + return ret ^ (this->type == TYPE_NOT_ONE); +} + + +LIBNORMALFORM_SENTENCE * +(libnormalform_one)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v) +{ + static const struct libnormalform_sentence prototype = { + PROTOTYPE_COMMON, + .type = TYPE_ONE, + .inverse = &one_inverse, + .equals = &one_equals, + .evaluate = &one_evaluate + }; + + LIBNORMALFORM_SENTENCE *ret; + + if (!k || !v) { + libnormalform_free(k); + libnormalform_free(v); + return NULL; + } + + if (k->type == TYPE_FALSE) { + libnormalform_free(v); + return k; + } + if (v->type == TYPE_FALSE) { + libnormalform_free(k); + return v; + } + + ret = malloc(sizeof(*ret)); + if (ret) { + *ret = prototype; + ret->hash = ONE_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[3]; + 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_one(&dom1, NULL, REF(v1)) && errno == 0); + errno = 1; + ASSERT(!libnormalform_one(&dom1, NULL, REF(v1)) && errno == 1); + errno = 0; + ASSERT(!libnormalform_one(&dom1, REF(v1), NULL) && errno == 0); + errno = 1; + ASSERT(!libnormalform_one(&dom1, REF(v1), NULL) && errno == 1); + errno = 0; + ASSERT(!libnormalform_one(&dom1, NULL, NULL) && errno == 0); + errno = 1; + ASSERT(!libnormalform_one(&dom1, NULL, NULL) && errno == 1); + + dom1.mappings = map; + memset(map, 0, sizeof(map)); + + /* ∃!x.(⊥ ∧ φ(x)) = ⊥ */ + ASSUME(a = libnormalform_one(&dom1, libnormalform_false(), REF(v1))); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* ∃!x.(⊤ ∧ φ(x)) irreducable */ + ASSUME(a = libnormalform_one(&dom1, libnormalform_true(), REF(v1))); + ASSERT(a->type == TYPE_ONE); + libnormalform_free(a); + + /* ∃!x.(φ(x) ∧ ⊤) irreducable */ + ASSUME(a = libnormalform_one(&dom1, REF(v1), libnormalform_true())); + ASSERT(a->type == TYPE_ONE); + libnormalform_free(a); + + /* ∃!x.(φ(x) ∧ ⊥) = ⊥ */ + ASSUME(a = libnormalform_one(&dom1, REF(v1), libnormalform_false())); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + ASSUME(a = libnormalform_one(&dom1, REF(v1), REF(v2))); + ASSERT(a->type == TYPE_ONE); + ASSERT(a->refcount == 1); + + dom1.nmappings = 1; + + /* ∃!x∈{a}.(⊥ ∧ ⊥) = ⊥ */ + var1.value = LIBNORMALFORM_FALSE; + var2.value = LIBNORMALFORM_FALSE; + ASSERT(libnormalform_evaluate(a) == 0); + + /* ∃!x∈{a}.(⊥ ∧ ⊤) = ⊥ */ + var1.value = LIBNORMALFORM_FALSE; + var2.value = LIBNORMALFORM_TRUE; + ASSERT(libnormalform_evaluate(a) == 0); + + /* ∃!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) == 0); + + /* ∃!x∈{a,b}.(⊥ ∧ ⊤) = ⊥ */ + var1.value = LIBNORMALFORM_FALSE; + var2.value = LIBNORMALFORM_TRUE; + ASSERT(libnormalform_evaluate(a) == 0); + + /* ∃!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) == 0); + + dom1.nmappings = 0; + + /* ∃!x∈∅.(⊥ ∧ ⊥) = ⊥ */ + var1.value = LIBNORMALFORM_FALSE; + var2.value = LIBNORMALFORM_FALSE; + ASSERT(libnormalform_evaluate(a) == 0); + + /* ∃!x∈∅.(⊥ ∧ ⊤) = ⊥ */ + var1.value = LIBNORMALFORM_FALSE; + var2.value = LIBNORMALFORM_TRUE; + ASSERT(libnormalform_evaluate(a) == 0); + + /* ∃!x∈∅.(⊤ ∧ ⊥) = ⊥ */ + var1.value = LIBNORMALFORM_TRUE; + var2.value = LIBNORMALFORM_FALSE; + ASSERT(libnormalform_evaluate(a) == 0); + + /* ∃!x∈∅.(⊤ ∧ ⊤) = ⊥ */ + var1.value = LIBNORMALFORM_TRUE; + var2.value = LIBNORMALFORM_TRUE; + ASSERT(libnormalform_evaluate(a) == 0); + + dom1.nmappings = 0; + + libnormalform_free(a); + + fun1.evaluate = &evalbool; + dom1.nmappings = 2; + + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(a = libnormalform_one(&dom1, libnormalform_true(), a)); + 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); + + libnormalform_free(a); + + ASSUME(a = libnormalform_function(&fun1)); + ASSUME(a = libnormalform_one(&dom1, a, libnormalform_true())); + ASSERT(a->type == TYPE_ONE); + 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) == 0); + + /* ∃!x∈{⊤, ⊤, ⊤}.(x ∧ ⊤) = ⊥ */ + dom1.nmappings = 3; + map[0].key = &t; + map[1].key = &t; + map[2].key = &t; + ASSERT(libnormalform_evaluate(a) == 0); + + libnormalform_free(a); + + ASSUME(a = libnormalform_one(&dom1, REF(v1), REF(v2))); + + /* ∃!x∈X.(P(x) ∧ Q(x)) = ∃!x∈X.(P(x) ∧ Q(x)) */ + ASSUME(b = libnormalform_one(&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_one(&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_one(&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(c = libnormalform_not(REF(a))); + ASSUME(b = libnormalform_not(libnormalform_one(&dom1, REF(v1), REF(v2)))); + ASSERT_EQUAL(c, b); + ASSERT(c->type == TYPE_NOT_ONE); + 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)) = ∀x∈X.(P(x) → Q(x)) */ + ASSUME(b = libnormalform_all(&dom1, 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), REF(v2))); + ASSERT_NOTEQUAL(a, b); + + /* ∃!x∈X.(P(x) ∧ Q(x)) = ¬∃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.(¬Q(x) ∧ Q(y)) = ∃!{x,y}∈X.⊥ = ⊥ ∵ 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 = ¬Q ⊭ P(x) = ¬Q(y) */ + ASSUME(b = libnormalform_one(&dom1, libnormalform_false(), libnormalform_false())); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + ASSUME(b = libnormalform_false()); + 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 |