diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_xor.c | 710 |
1 files changed, 710 insertions, 0 deletions
diff --git a/libnormalform_xor.c b/libnormalform_xor.c new file mode 100644 index 0000000..451fbf9 --- /dev/null +++ b/libnormalform_xor.c @@ -0,0 +1,710 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +/** + * Check if a sentence equivalent to a specific sentence + * or its inverse is in an array of sentences + * + * @param x The sentence to look for + * @param among The array of sentences to look in + * @param n The number of sentences in `among` + * @param index_out Output parameter for the offset, in `among`, + * of the found sentence + * @param inv_out Output parameter for equivalency of `x` and the + * sentence found in `among`; set to 0 if the two + * are equivalent or 1 if `x` is equivalent to the + * inverse of the sentence found in `among` + * @return 1 if a sentence equivalent to `x` or its inverse + * was found, 0 otherwise + */ +static int +find(LIBNORMALFORM_SENTENCE *x, LIBNORMALFORM_SENTENCE **among, size_t n, size_t *index_out, int *inv_out) +{ + for (*index_out = 0; *index_out < n; ++*index_out) + if (x->equals(x, among[*index_out], inv_out)) + return 1; + return 0; +} + + +LIBNORMALFORM_SENTENCE * +(libnormalform_xor)(LIBNORMALFORM_SENTENCE **xs) +{ + LIBNORMALFORM_SENTENCE *x, *ret, **saved = xs; + size_t n = 0, i; + int inv; + + /* ⨁∅ = {⨁X ⊕ (x ⊕ x) = ⨁X ⊕ 0 = ⨁X ⇒ ⨁X = ⨁(X ∪ {x, x})} = x ⊕ x = 0 */ + ret = libnormalform_false(); + + for (; (x = *xs); xs++) { + if (x->type == TYPE_FALSE) { + /* ⨁X ⊕ 0 = ⨁X */ + libnormalform_free(x); + + } else if (x->type == TYPE_TRUE) { + /* ⨁X ⊕ 1 = ¬⨁X */ + libnormalform_free(x); + invert: + ret = libnormalform_not(ret); + + } else if (find(x, saved, n, &i, &inv)) { + /* ⨁X ⊕ x ⊕ x = ⨁X ⊕ (x ⊕ x) = ⨁X ⊕ 0 = ⨁X */ + /* ⨁X ⊕ x ⊕ ¬x = ⨁X ⊕ (x ⊕ ¬x) = ⨁X ⊕ 1 = ¬⨁X */ + libnormalform_free(saved[i]); + libnormalform_free(x); + saved[i] = saved[--n]; + if (inv) + goto invert; + + } else { + saved[n++] = x; + } + } + + saved[n] = NULL; + /* ⨁(X ∪ x) = ⨁X ⊕ x */ + for (; *saved; saved++) + ret = libnormalform_xor2(ret, *saved); + + return ret; +} + + +#else + + +#define XOR(...) LIBNORMALFORM_XOR(__VA_ARGS__) + + +int +main(void) +{ + TEST_BEGIN; + + struct libnormalform_variable var1, var2, var3, var4; + struct libnormalform_function fun1, fun2; + struct libnormalform_map domain; + struct libnormalform_transformer trans; + LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *v3, *v4, *f1, *f2; + LIBNORMALFORM_SENTENCE *ts, *fs; + + ASSUME(v1 = libnormalform_variable(&var1)); + ASSUME(v2 = libnormalform_variable(&var2)); + ASSUME(v3 = libnormalform_variable(&var3)); + ASSUME(v4 = libnormalform_variable(&var4)); + ASSUME(f1 = libnormalform_function(&fun1)); + ASSUME(f2 = libnormalform_function(&fun2)); + ASSUME(ts = libnormalform_true()); + ASSUME(fs = libnormalform_false()); + +#ifdef USE_CHECKED_VERSION + errno = 0; + ASSERT(!XOR(REF(v1), NULL) && errno == 0); + errno = 1; + ASSERT(!XOR(REF(v1), NULL) && errno == 1); + errno = 0; + ASSERT(!XOR(NULL, REF(v1)) && errno == 0); + errno = 1; + ASSERT(!XOR(NULL, REF(v1)) && errno == 1); + errno = 0; + ASSERT(!XOR(NULL, NULL) && errno == 0); + errno = 1; + ASSERT(!XOR(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 = XOR(__VA_ARGS__));\ + ASSERT(a->type == TYPE_##VALUE);\ + libnormalform_free(a);\ + } while (0) + +#define ASSERT_EVAL2(VALUE, V1, V2)\ + do {\ + ASSUME(a = XOR(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) + +#define ASSERT_EVAL3(VALUE, V1, V2, V3)\ + do {\ + ASSUME(a = XOR(REF(v1), REF(v2), REF(v3)));\ + ASSERT(a->type != TYPE_TRUE && a->type != TYPE_FALSE);\ + var1.value = V1##V;\ + var2.value = V2##V;\ + var3.value = V3##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); /* XOR () -> FALSE */ + +#if defined(__GNUC__) +# pragma GCC diagnostic pop +#endif + + ASSERT_CONST(TRUE, T); /* XOR (TRUE) -> TRUE */ + ASSERT_CONST(FALSE, F); /* XOR (FALSE) -> FALSE */ + +#endif + + ASSERT_CONST(FALSE, F, F); /* XOR (FALSE, FALSE) -> FALSE */ + ASSERT_CONST(TRUE, F, T); /* XOR (FALSE, TRUE) -> TRUE */ + ASSERT_CONST(TRUE, T, F); /* XOR (TRUE, FALSE) -> TRUE */ + ASSERT_CONST(FALSE, T, T); /* XOR (TRUE, TRUE) -> FALSE */ + + ASSERT_EVAL2(FALSE, F, F); /* XOR (var(FALSE), var(FALSE)) => FALSE */ + ASSERT_EVAL2(TRUE, F, T); /* XOR (var(FALSE), var(TRUE)) => TRUE */ + ASSERT_EVAL2(TRUE, T, F); /* XOR (var(TRUE), var(FALSE)) => TRUE */ + ASSERT_EVAL2(FALSE, T, T); /* XOR (var(TRUE), var(TRUE)) => FALSE */ + +#ifndef USE_TWO + + ASSERT_CONST(FALSE, F, F, F); /* XOR (FALSE, FALSE, FALSE) -> FALSE */ + ASSERT_CONST(TRUE, F, F, T); /* XOR (FALSE, FALSE, TRUE) -> TRUE */ + ASSERT_CONST(TRUE, F, T, F); /* XOR (FALSE, TRUE, FALSE) -> TRUE */ + ASSERT_CONST(FALSE, F, T, T); /* XOR (FALSE, TRUE, TRUE) -> FALSE */ + ASSERT_CONST(TRUE, T, F, F); /* XOR (TRUE, FALSE, FALSE) -> TRUE */ + ASSERT_CONST(FALSE, T, F, T); /* XOR (TRUE, FALSE, TRUE) -> FALSE */ + ASSERT_CONST(FALSE, T, T, F); /* XOR (TRUE, TRUE, FALSE) -> FALSE */ + ASSERT_CONST(TRUE, T, T, T); /* XOR (TRUE, TRUE, TRUE) -> TRUE */ + + ASSERT_EVAL3(FALSE, F, F, F); /* XOR (var(FALSE), var(FALSE), var(FALSE)) => FALSE */ + ASSERT_EVAL3(TRUE, F, F, T); /* XOR (var(FALSE), var(FALSE), var(TRUE)) => TRUE */ + ASSERT_EVAL3(TRUE, F, T, F); /* XOR (var(FALSE), var(TRUE), var(FALSE)) => TRUE */ + ASSERT_EVAL3(FALSE, F, T, T); /* XOR (var(FALSE), var(TRUE), var(TRUE)) => FALSE */ + ASSERT_EVAL3(TRUE, T, F, F); /* XOR (var(TRUE), var(FALSE), var(FALSE)) => TRUE */ + ASSERT_EVAL3(FALSE, T, F, T); /* XOR (var(TRUE), var(FALSE), var(TRUE)) => FALSE */ + ASSERT_EVAL3(FALSE, T, T, F); /* XOR (var(TRUE), var(TRUE), var(FALSE)) => FALSE */ + ASSERT_EVAL3(TRUE, T, T, T); /* XOR (var(TRUE), var(TRUE), var(TRUE)) => TRUE */ + + /* XOR (x) -> x */ + ASSUME(a = XOR(REF(v1))); + ASSERT(a == v1); + ASSERT(a->refcount == 2); + libnormalform_free(a); + +#endif + + /* XOR (x, TRUE) -> NOT x */ + ASSUME(a = XOR(REF(v1), T)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (TRUE, x) -> NOT x */ + ASSUME(a = XOR(T, REF(v1))); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (x, FALSE) -> x */ + ASSUME(a = XOR(REF(v1), F)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XOR (FALSE, x) -> x */ + ASSUME(a = XOR(F, REF(v1))); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + +#ifndef USE_TWO + + /* XOR (x, FALSE, FALSE) -> x */ + ASSUME(a = XOR(REF(v1), F, F)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XOR (x, FALSE, TRUE) -> NOT x */ + ASSUME(a = XOR(REF(v1), F, T)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (x, TRUE, FALSE) -> NOT x */ + ASSUME(a = XOR(REF(v1), T, F)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (x, TRUE, TRUE) -> x */ + ASSUME(a = XOR(REF(v1), T, T)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XOR (FALSE, x, FALSE) -> x */ + ASSUME(a = XOR(F, REF(v1), F)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XOR (FALSE, x, TRUE) -> NOT x */ + ASSUME(a = XOR(F, REF(v1), T)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (TRUE, x, FALSE) -> NOT x */ + ASSUME(a = XOR(T, REF(v1), F)); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (TRUE, x, TRUE) -> x */ + ASSUME(a = XOR(T, REF(v1), T)); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XOR (FALSE, FALSE, x) -> x */ + ASSUME(a = XOR(F, F, REF(v1))); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + + /* XOR (FALSE, TRUE, x) -> NOT x */ + ASSUME(a = XOR(F, T, REF(v1))); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (TRUE, FALSE, x) -> NOT x */ + ASSUME(a = XOR(T, F, REF(v1))); + ASSERT_INVEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (TRUE, TRUE, x) -> x */ + ASSUME(a = XOR(T, T, REF(v1))); + ASSERT_EQUAL(a, v1); + ASSERT(a == v1); + libnormalform_free(a); + +#endif + + /* XOR (x, x) -> FALSE */ + ASSUME(a = XOR(REF(v1), REF(v1))); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + +#ifndef USE_TWO + + /* XOR (x, x, FALSE) -> FALSE */ + ASSUME(a = XOR(REF(v1), REF(v1), F)); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* XOR (x, x, FALSE, FALSE) -> FALSE */ + ASSUME(a = XOR(REF(v1), REF(v1), F, F)); + ASSERT(a->type == TYPE_FALSE); + libnormalform_free(a); + + /* XOR (x, x, TRUE) -> TRUE */ + ASSUME(a = XOR(REF(v1), REF(v1), T)); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + +#endif + + /* XOR (x, NOT x) -> TRUE */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(a = XOR(REF(v1), a)); + ASSERT(a->type == TYPE_TRUE); + libnormalform_free(a); + + /* XOR (x, y) -> XOR (x, y) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = XOR(REF(v1), REF(v2))); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (y, x) -> XOR (x, y) */ + ASSUME(a = XOR(REF(v2), REF(v1))); + ASSUME(b = XOR(REF(v1), REF(v2))); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#ifndef USE_TWO + + /* XOR (TRUE, x, y) -> NOT XOR (x, y) */ + ASSUME(a = XOR(T, REF(v1), REF(v2))); + ASSUME(b = XOR(REF(v1), REF(v2))); + ASSERT_INVEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, TRUE, y) -> NOT XOR (x, y) */ + ASSUME(a = XOR(REF(v1), T, REF(v2))); + ASSUME(b = XOR(REF(v1), REF(v2))); + ASSERT_INVEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y, TRUE) -> NOT XOR (x, y) */ + ASSUME(a = XOR(REF(v1), REF(v2), T)); + ASSUME(b = XOR(REF(v1), REF(v2))); + ASSERT_INVEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (FALSE, x, y) -> XOR (x, y) */ + ASSUME(a = XOR(F, REF(v1), REF(v2))); + ASSUME(b = XOR(REF(v1), REF(v2))); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, FALSE, y) -> XOR (x, y) */ + ASSUME(a = XOR(REF(v1), F, REF(v2))); + ASSUME(b = XOR(REF(v1), REF(v2))); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y, FALSE) -> XOR (x, y) */ + ASSUME(a = XOR(REF(v1), REF(v2), F)); + ASSUME(b = XOR(REF(v1), REF(v2))); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#endif + + /* NOT XOR (x, y) -> XOR (NOT x, y) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(a = libnormalform_not(a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_xorl(b, REF(v2), NULL)); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* NOT XOR (x, y) -> XOR (x, NOT y) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(a = libnormalform_not(a)); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_xorl(REF(v1), b, NULL)); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* NOT XOR (x, y) -> XOR (x, y, TRUE) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(a = libnormalform_not(a)); + ASSUME(b = libnormalform_xorl(REF(v1), REF(v2), T, NULL)); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from XOR (x, z) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_xor2(REF(v1), REF(v3))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from XOR (z, x) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_xor2(REF(v3), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from XOR (z, w) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_xor2(REF(v3), REF(v4))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from AND (x, y) */ + ASSUME(a = REF(v1)); + ASSUME(b = REF(v2)); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from AND (x, NOT y) */ + ASSUME(a = REF(v1)); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from AND (NOT x, y) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = REF(v2)); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from AND (NOT x, NOT y) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from OR (x, y) */ + ASSUME(a = REF(v1)); + ASSUME(b = REF(v2)); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from OR (x, NOT y) */ + ASSUME(a = REF(v1)); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from OR (NOT x, y) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = REF(v2)); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from OR (NOT x, NOT y) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from TRUE */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_true()); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from FALSE */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_false()); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from variable1 */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, v1); + libnormalform_free(a); + + /* XOR (x, y) -> independence from NOT variable1 */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_not(REF(v1))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from function1 */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, f1); + libnormalform_free(a); + + /* XOR (x, y) -> independence from NOT function1 */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_not(REF(f1))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from T(function1) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_transformation(&trans, REF(f1))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from ALL (domain1, function1, function2) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_all(&domain, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from ANY (domain1, function1, function2) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_any(&domain, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from ONE (domain1, function1, function2) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_one(&domain, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> independence from NOT ONE (domain1, function1, function2) */ + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSUME(b = libnormalform_one(&domain, REF(f1), REF(f2))); + ASSUME(b = libnormalform_not(b)); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> OR (AND (x, NOT y), AND (NOT x, y)) */ + ASSUME(a = libnormalform_not(REF(v2))); + ASSUME(a = libnormalform_and2(REF(v1), a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_and2(b, REF(v2))); + ASSUME(b = libnormalform_or2__(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_OR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> AND (OR (x, y), OR (NOT x, NOT y)) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = libnormalform_or2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_and2__(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_AND); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> OR (AND (x, NOT y), AND (NOT x, y)) */ + ASSUME(a = libnormalform_not(REF(v2))); + ASSUME(a = libnormalform_and2(REF(v1), a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_and2(b, REF(v2))); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_XOR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> AND (OR (x, y), OR (NOT x, NOT y)) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = libnormalform_or2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_and2(a, b)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_XOR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> OR (AND (NOT x, y), AND (x, NOT y)) */ + ASSUME(a = libnormalform_not(REF(v2))); + ASSUME(a = libnormalform_and2(REF(v1), a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_and2(b, REF(v2))); + ASSUME(b = libnormalform_or2__(b, a)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_OR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> AND (OR (NOT x, NOT y), OR (x, y)) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = libnormalform_or2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_and2__(b, a)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_AND); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> OR (AND (NOT x, y), AND (x, NOT y)) */ + ASSUME(a = libnormalform_not(REF(v2))); + ASSUME(a = libnormalform_and2(REF(v1), a)); + ASSUME(b = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_and2(b, REF(v2))); + ASSUME(b = libnormalform_or2(b, a)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_XOR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + + /* XOR (x, y) -> AND (OR (NOT x, NOT y), OR (x, y)) */ + ASSUME(a = libnormalform_not(REF(v1))); + ASSUME(b = libnormalform_not(REF(v2))); + ASSUME(b = libnormalform_or2(a, b)); + ASSUME(a = libnormalform_or2(REF(v1), REF(v2))); + ASSUME(b = libnormalform_and2(b, a)); + ASSUME(a = XOR(REF(v1), REF(v2))); + ASSERT(a->type == TYPE_XOR); + ASSERT(b->type == TYPE_XOR); + ASSERT_EQUAL(a, b); + libnormalform_free(a); + libnormalform_free(b); + +#undef T +#undef F +#undef TV +#undef FV + +#undef ASSERT_CONST +#undef ASSERT_EVAL2 +#undef ASSERT_EVAL3 + + libnormalform_free(v1); + libnormalform_free(v2); + libnormalform_free(v3); + libnormalform_free(v4); + libnormalform_free(f1); + libnormalform_free(f2); + libnormalform_free(ts); + libnormalform_free(fs); + + /* cascading of evaluation failure is tested in libnormalform_function.c */ + + TEST_END; +} + + +#endif |