diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_nif.c | 228 |
1 files changed, 228 insertions, 0 deletions
diff --git a/libnormalform_nif.c b/libnormalform_nif.c new file mode 100644 index 0000000..5b2ae24 --- /dev/null +++ b/libnormalform_nif.c @@ -0,0 +1,228 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +LIBNORMALFORM_SENTENCE * +(libnormalform_nif)(LIBNORMALFORM_SENTENCE **xs) +{ + LIBNORMALFORM_SENTENCE *x, *ret; + int inv; + + /* 0 ↚ x = x, but 1 ↚ x = 0 */ + ret = libnormalform_false(); + + for (; (x = *xs); xs++) { + if (!ret) { + /* error handling */ + libnormalform_free(x); + + } else if (ret->type == TYPE_TRUE || x->type == TYPE_FALSE) { + set_to_false: + /* 1 ↚ x = 0 */ + /* x ↚ 0 = 0 */ + libnormalform_free(x); + libnormalform_free(ret); + ret = libnormalform_false(); + + } else if (ret->type == TYPE_FALSE) { + set_to_x: + /* 0 ↚ x = x */ + libnormalform_free(ret); + ret = x; + + } else if (ret->equals(ret, x, &inv)) { + if (!inv) { + /* x ↚ x = 0 */ + goto set_to_false; + + } else { + /* ¬x ↚ x = x (0 ↚ 1 = 1, 1 ↚ 0 = 0) */ + goto set_to_x; + } + + } else { + /* l ↚ r = ¬(l ← r) = ¬(r → l) = ¬¬(r ∧ ¬l) = r ∧ ¬l = ¬l ∧ r */ + ret = libnormalform_and2(libnormalform_not(ret), x); + } + } + + return ret; +} + + +#else + + +#define NIF(...) LIBNORMALFORM_NIF(__VA_ARGS__) + + +int +main(void) +{ + TEST_BEGIN; + + struct libnormalform_variable var1, var2, var3; + LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *v3; + LIBNORMALFORM_SENTENCE *ts, *fs; + + ASSUME(v1 = libnormalform_variable(&var1)); + ASSUME(v2 = libnormalform_variable(&var2)); + ASSUME(v3 = libnormalform_variable(&var3)); + ASSUME(ts = libnormalform_true()); + ASSUME(fs = libnormalform_false()); + +#ifdef USE_CHECKED_VERSION + errno = 0; + ASSERT(!NIF(REF(v1), NULL) && errno == 0); + errno = 1; + ASSERT(!NIF(REF(v1), NULL) && errno == 1); + errno = 0; + ASSERT(!NIF(NULL, REF(v1)) && errno == 0); + errno = 1; + ASSERT(!NIF(NULL, REF(v1)) && errno == 1); + errno = 0; + ASSERT(!NIF(NULL, NULL) && errno == 0); + errno = 1; + ASSERT(!NIF(NULL, NULL) && errno == 1); +#endif + +#define T REF(ts) +#define F REF(fs) +#define TV LIBNORMALFORM_TRUE +#define FV LIBNORMALFORM_FALSE + +#define ASSERT_CONST(VALUE, ...)\ + do {\ + ASSUME(a = NIF(__VA_ARGS__));\ + ASSERT(a->type == TYPE_##VALUE);\ + libnormalform_free(a);\ + } while (0) + +#define ASSERT_EVAL2(VALUE, V1, V2)\ + do {\ + ASSUME(a = NIF(REF(v1), REF(v2)));\ + ASSERT(a->type != TYPE_TRUE && a->type != TYPE_FALSE);\ + var1.value = V1##V;\ + var2.value = V2##V;\ + ASSERT(libnormalform_evaluate(a) == (int)LIBNORMALFORM_##VALUE);\ + libnormalform_free(a);\ + } while (0) + +#ifndef USE_TWO + +#if defined(__GNUC__) +# pragma GCC diagnostic push +# pragma GCC diagnostic ignored "-Wformat" +#endif + + ASSERT_CONST(FALSE); /* NIF () -> FALSE */ + +#if defined(__GNUC__) +# pragma GCC diagnostic pop +#endif + + ASSERT_CONST(TRUE, T); /* NIF (TRUE) -> TRUE */ + ASSERT_CONST(FALSE, F); /* NIF (FALSE) -> FALSE */ + +#endif + + ASSERT_CONST(FALSE, F, F); /* NIF (FALSE, FALSE) -> FALSE */ + ASSERT_CONST(TRUE, F, T); /* NIF (FALSE, TRUE) -> TRUE */ + ASSERT_CONST(FALSE, T, F); /* NIF (TRUE, FALSE) -> FALSE */ + ASSERT_CONST(FALSE, T, T); /* NIF (TRUE, TRUE) -> FALSE */ + + ASSERT_EVAL2(FALSE, F, F); /* NIF (var(FALSE), var(FALSE)) => FALSE */ + ASSERT_EVAL2(TRUE, F, T); /* NIF (var(FALSE), var(TRUE)) => TRUE */ + ASSERT_EVAL2(FALSE, T, F); /* NIF (var(TRUE), var(FALSE)) => FALSE */ + ASSERT_EVAL2(FALSE, T, T); /* NIF (var(TRUE), var(TRUE)) => FALSE */ + +#ifndef USE_TWO + + /* NIF (x) -> x */ + ASSUME(a = NIF(REF(v1))); + ASSERT(a == v1); + ASSERT(a->refcount == 2); + libnormalform_free(a); + +#endif + + /* NIF (x, TRUE) -> NOT x */ + ASSUME(a = NIF(REF(v1), T)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* NIF (TRUE, x) -> FALSE */ + ASSUME(a = NIF(T, REF(v1))); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* NIF (x, FALSE) -> FALSE */ + ASSUME(a = NIF(REF(v1), F)); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* NIF (FALSE, x) -> x */ + ASSUME(a = NIF(F, REF(v1))); + ASSERT_EQUAL(a, v1); + libnormalform_free(a); + + /* NIF (x, x) -> FALSE */ + ASSUME(a = NIF(REF(v1), REF(v1))); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* NIF (NOT x, x) -> x */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(a = NIF(a, REF(v1))); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* NIF (x, y) -> AND (NOT x, y) */ + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_and2(b, REF(v2))); + ASSUME(a = NIF(REF(v1), REF(v2))); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#ifndef USE_TWO + + /* NIF (x, y, z) -> AND (NOT AND (NOT x, y), z) */ + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_nand2(b, REF(v2))); + ASSUME(b = libnormalform_and2(b, REF(v3))); + ASSUME(a = NIF(REF(v1), REF(v2), REF(v3))); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* NIF (x, y) -> independence from NIF (y, x) */ + ASSUME(a = NIF(REF(v1), REF(v2))); + ASSUME(b = NIF(REF(v2), REF(v1))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#endif + +#undef T +#undef F +#undef TV +#undef FV + +#undef ASSERT_CONST +#undef ASSERT_EVAL2 + + libnormalform_free(v1); + libnormalform_free(v2); + libnormalform_free(v3); + libnormalform_free(ts); + libnormalform_free(fs); + + TEST_END; +} + + +#endif |