diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform_variable.c | 153 |
1 files changed, 153 insertions, 0 deletions
diff --git a/libnormalform_variable.c b/libnormalform_variable.c new file mode 100644 index 0000000..0c8b0bf --- /dev/null +++ b/libnormalform_variable.c @@ -0,0 +1,153 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +/** + * See `.inverse` in `struct libnormalform_sentence` (Variable literal implementation) + */ +static LIBNORMALFORM_SENTENCE * +variable_inverse(LIBNORMALFORM_SENTENCE *this) +{ + LIBNORMALFORM_SENTENCE *ret = libnormalform_variable(this->data.literal.atom.variable); + if (ret) + ret->data.literal.inverted = this->data.literal.inverted ^ 1; + return ret; +} + + +/** + * See `.equals` in `struct libnormalform_sentence` (Variable literal implementation) + */ +static int +variable_equals(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out) +{ + if (other->type != TYPE_VARIABLE || this->data.literal.atom.variable != other->data.literal.atom.variable) + return 0; + *inv_out = this->data.literal.inverted ^ other->data.literal.inverted; + return 1; +} + + +/** + * See `.evaluate` in `struct libnormalform_sentence` (Variable literal implementation) + */ +PURE static int +variable_evaluate(LIBNORMALFORM_SENTENCE *this, void *input) +{ + (void) input; + return (this->data.literal.atom.variable->value != LIBNORMALFORM_FALSE) ^ this->data.literal.inverted; +} + + +LIBNORMALFORM_SENTENCE * +(libnormalform_variable)(struct libnormalform_variable *variable) +{ + static const struct libnormalform_sentence prototype = { + PROTOTYPE_COMMON, + .type = TYPE_VARIABLE, + .inverse = &variable_inverse, + .equals = &variable_equals, + .evaluate = &variable_evaluate + }; + + LIBNORMALFORM_SENTENCE *ret = malloc(sizeof(*ret)); + if (ret) { + *ret = prototype; + ret->hash = LITERAL_HASH(variable); + ret->data.literal.atom.variable = variable; + ret->data.literal.inverted = 0; + } + return ret; +} + + +#else + + +int +main(void) +{ + TEST_BEGIN; + + struct libnormalform_variable var1, var2; + struct libnormalform_function fun1, fun2; + struct libnormalform_map domain; + LIBNORMALFORM_SENTENCE *a, *b, *v1, *v2, *f1, *f2; + + ASSUME(a = libnormalform_variable(&var1)); + ASSERT(a->refcount == 1); + ASSERT(a->travel_index == 0); + ASSERT(a->travel_count == 0); + ASSERT(a->type == TYPE_VARIABLE); + ASSERT(a->data.literal.inverted == 0); + ASSERT(a->data.literal.atom.variable == &var1); + ASSERT_EQUAL(a, a); + var1.value = LIBNORMALFORM_TRUE; + ASSERT(libnormalform_evaluate(a) == 1); + var1.value = LIBNORMALFORM_FALSE; + ASSERT(libnormalform_evaluate(a) == 0); + + ASSUME(b = libnormalform_variable(&var1)); + ASSERT_EQUAL(a, b); + ASSUME(b = libnormalform_not(b)); + ASSERT_INVEQUAL(a, b); + ASSERT_INVEQUAL(b, a); + libnormalform_free(b); + + ASSUME(b = libnormalform_variable(&var2)); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_true()); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_false()); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(v1 = libnormalform_variable(&var1)); + ASSUME(v2 = libnormalform_variable(&var2)); + ASSUME(f1 = libnormalform_function(&fun1)); + ASSUME(f2 = libnormalform_function(&fun2)); + + ASSERT_NOTEQUAL(a, f1); + + ASSUME(b = libnormalform_and2(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_or2(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_xor2(REF(v1), REF(v2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_all(&domain, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_any(&domain, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + ASSUME(b = libnormalform_one(&domain, REF(f1), REF(f2))); + ASSERT_NOTEQUAL(a, b); + ASSUME(b = libnormalform_not(b)); + ASSERT_NOTEQUAL(a, b); + libnormalform_free(b); + + libnormalform_free(a); + libnormalform_free(v1); + libnormalform_free(v2); + libnormalform_free(f1); + libnormalform_free(f2); + + TEST_END; +} + + +#endif |