diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_if.c | 249 |
1 files changed, 249 insertions, 0 deletions
diff --git a/libnormalform_if.c b/libnormalform_if.c new file mode 100644 index 0000000..17bb380 --- /dev/null +++ b/libnormalform_if.c @@ -0,0 +1,249 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +LIBNORMALFORM_SENTENCE * +(libnormalform_if)(LIBNORMALFORM_SENTENCE **xs) +{ + LIBNORMALFORM_SENTENCE *x, *ret; + int inv; + + /* 0 ← x = ¬x, but 1 ← x = 1, so at least one argument is required */ + ret = *xs++; + if (!ret) { + errno = EDOM; + return NULL; + } + + if (ret->type == TYPE_TRUE) { + /* 1 ← x = 1 */ + goto return_asis; + } + + for (; (x = *xs); xs++) { + if (!ret) { + /* error handling */ + libnormalform_free(x); + + } else if (x->type == TYPE_FALSE) { + /* x ← 0 ← y = 1 ← y = 1 */ + goto return_true; + + } else if (x->type == TYPE_TRUE) { + /* x ← 1 = x */ + libnormalform_free(x); + + } else if (x->equals(x, ret, &inv)) { + if (!inv) { + /* x ← x ← y = 1 ← y = 1 */ + goto return_true; + + } else { + /* x ← ¬x = x */ + libnormalform_free(x); + } + + } else if (ret->type == TYPE_FALSE) { + /* 0 ← x = ¬x */ + libnormalform_free(ret); + ret = libnormalform_not(x); + + } else { + /* l ← r = r → l = ¬(r ∧ ¬l) = ¬r ∨ l = l ∨ ¬r */ + ret = libnormalform_or2(ret, libnormalform_not(x)); + if (ret && ret->type == TYPE_TRUE) { + /* 1 ← x = 1 */ + goto return_true; + } + } + } + + return ret; + +return_true: + libnormalform_free(ret); + ret = libnormalform_true(); +return_asis: + while (*xs) + libnormalform_free(*xs++); + return ret; +} + + +#else + + +#define IF(...) LIBNORMALFORM_IF(__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(!IF(REF(v1), NULL) && errno == 0); + errno = 1; + ASSERT(!IF(REF(v1), NULL) && errno == 1); + errno = 0; + ASSERT(!IF(NULL, REF(v1)) && errno == 0); + errno = 1; + ASSERT(!IF(NULL, REF(v1)) && errno == 1); + errno = 0; + ASSERT(!IF(NULL, NULL) && errno == 0); + errno = 1; + ASSERT(!IF(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 = IF(__VA_ARGS__));\ + ASSERT(a->type == TYPE_##VALUE);\ + libnormalform_free(a);\ + } while (0) + +#define ASSERT_EVAL2(VALUE, V1, V2)\ + do {\ + ASSUME(a = IF(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 + + /* IF () -> EDOM */ + errno = 0; + ASSERT(!IF() && errno == EDOM); + +#if defined(__GNUC__) +# pragma GCC diagnostic pop +#endif + + ASSERT_CONST(TRUE, T); /* IF (TRUE) -> TRUE */ + ASSERT_CONST(FALSE, F); /* IF (FALSE) -> FALSE */ + +#endif + + ASSERT_CONST(TRUE, F, F); /* IF (FALSE, FALSE) -> TRUE */ + ASSERT_CONST(FALSE, F, T); /* IF (FALSE, TRUE) -> FALSE */ + ASSERT_CONST(TRUE, T, F); /* IF (TRUE, FALSE) -> TRUE */ + ASSERT_CONST(TRUE, T, T); /* IF (TRUE, TRUE) -> TRUE */ + + ASSERT_EVAL2(TRUE, F, F); /* IF (var(FALSE), var(FALSE)) => TRUE */ + ASSERT_EVAL2(FALSE, F, T); /* IF (var(FALSE), var(TRUE)) => FALSE */ + ASSERT_EVAL2(TRUE, T, F); /* IF (var(TRUE), var(FALSE)) => TRUE */ + ASSERT_EVAL2(TRUE, T, T); /* IF (var(TRUE), var(TRUE)) => TRUE */ + +#ifndef USE_TWO + + /* IF (x) -> x */ + ASSUME(a = IF(REF(v1))); + ASSERT(a == v1); + ASSERT(a->refcount == 2); + libnormalform_free(a); + +#endif + + /* IF (x, TRUE) -> x */ + ASSUME(a = IF(REF(v1), T)); + ASSERT(a == v1); + libnormalform_free(a); + + /* IF (TRUE, x) -> TRUE */ + ASSUME(a = IF(T, REF(v1))); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + + /* IF (x, FALSE) -> TRUE */ + ASSUME(a = IF(REF(v1), F)); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + + /* IF (FALSE, x) -> NOT x */ + ASSUME(a = IF(F, REF(v1))); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* IF (x, x) -> TRUE */ + ASSUME(a = IF(REF(v1), REF(v1))); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + + /* IF (x, NOT x) -> x */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(a = IF(REF(v1), a)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* IF (x, y) -> OR (x, NOT y) */ + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_or2(REF(v1), b)); + ASSUME(a = IF(REF(v1), REF(v2))); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#ifndef USE_TWO + + /* IF (x, y, z) -> NOT AND (NOT x, y, z) */ + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_andl(b, REF(v2), REF(v3), NULL)); + ASSUME(a = IF(REF(v1), REF(v2), REF(v3))); + ASSERT_INVEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* IF (x, y) -> independence from IF (y, x) */ + ASSUME(a = IF(REF(v1), REF(v2))); + ASSUME(b = IF(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 |