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