diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform.h | 4213 |
1 files changed, 4213 insertions, 0 deletions
diff --git a/libnormalform.h b/libnormalform.h new file mode 100644 index 0000000..ed3b256 --- /dev/null +++ b/libnormalform.h @@ -0,0 +1,4213 @@ +/* See LICENSE file for copyright and license details. */ +#ifndef LIBNORMALFORM_H +#define LIBNORMALFORM_H + +#include <stdarg.h> +#include <stddef.h> +#include <stdint.h> + + +#if defined(__GNUC__) +# pragma GCC diagnostic push +# pragma GCC diagnostic ignored "-Winline" +#endif + + +/* For internal use { */ + +#if defined(__GNUC__) +# define LIBNORMALFORM_USE_RESULT__ __attribute__((__warn_unused_result__)) +# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) __attribute__((__malloc__(DESTRUCTOR))) +# define LIBNORMALFORM_USE_FREE__ __attribute__((__malloc__)) +# define LIBNORMALFORM_NONNULL_INPUT__ __attribute__((__nonnull__)) +# define LIBNORMALFORM_ONE_NONNULL_INPUT__(INDEX) __attribute__((__nonnull__(INDEX))) +# if defined(LIBNORMALFORM_ALLOW_BAD_WARNINGS) +# define LIBNORMALFORM_NULL_LAST__ __attribute__((__sentinel__)) +# else +# define LIBNORMALFORM_NULL_LAST__ +# endif +/* + * Unfortunately __attribute__((__sentinel__)) requires (in contrary to the + * documentation) the `NULL` to be inside `...`, and not at the argument before + * the `...`, so a "-Wformat=" warning will be generated if and empty list is + * used when constructing a sentence. Therefore, by default this attribute is + * not used, as the user may have configured the compiler to fail if the warning + * is generated. + */ +#else +# define LIBNORMALFORM_USE_RESULT__ +# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) +# define LIBNORMALFORM_USE_FREE__ +# define LIBNORMALFORM_NONNULL_INPUT__ +# define LIBNORMALFORM_ONE_NONNULL_INPUT__(INDEX) +# define LIBNORMALFORM_NULL_LAST__ +#endif + + +#define LIBNORMALFORM_CHECKED__(CONNECTIVE)\ + size_t i__ = 0;\ + while (xs[i__])\ + i__ += 1;\ + if (i__ < n) {\ + while (n--)\ + libnormalform_free(xs[n]);\ + return NULL;\ + }\ + return libnormalform_##CONNECTIVE(xs); + +#define LIBNORMALFORM_VALIST__(CONNECTIVE)\ + size_t n__ = 0, i__ = 0;\ + va_list args2__;\ + va_copy(args2__, args);\ + if (a) {\ + do {\ + n__ += 1;\ + } while (va_arg(args2__, LIBNORMALFORM_SENTENCE *));\ + }\ + va_end(args2__);\ + {\ + LIBNORMALFORM_SENTENCE *xs[n__ + 1U];\ + if (n__) {\ + xs[i__++] = a;\ + while (--n__)\ + xs[i__++] = va_arg(args, LIBNORMALFORM_SENTENCE *);\ + }\ + xs[i__] = NULL;\ + return libnormalform_##CONNECTIVE(xs);\ + } + +#define LIBNORMALFORM_ELLIPSIS__(CONNECTIVE)\ + LIBNORMALFORM_SENTENCE *ret__;\ + va_list args__;\ + va_start(args__, a);\ + ret__ = libnormalform_v##CONNECTIVE(a, args__);\ + va_end(args__);\ + return ret__; + +#define LIBNORMALFORM_VALIST_CHECKED__(CONNECTIVE)\ + size_t n__ = 0, i__ = 0;\ + va_list args2__;\ + va_copy(args2__, args);\ + if (a) {\ + do {\ + n__ += 1;\ + } while (va_arg(args2__, LIBNORMALFORM_SENTENCE *));\ + }\ + va_end(args2__);\ + if (n__ < n) {\ + if (n) {\ + libnormalform_free(a);\ + while (--n)\ + libnormalform_free(va_arg(args2__, LIBNORMALFORM_SENTENCE *));\ + }\ + return NULL;\ + }\ + {\ + LIBNORMALFORM_SENTENCE *xs__[n__ + 1U];\ + if (n__) {\ + xs__[i__++] = a;\ + while (--n__)\ + xs__[i__++] = va_arg(args, LIBNORMALFORM_SENTENCE *);\ + }\ + xs__[i__] = NULL;\ + return libnormalform_##CONNECTIVE(xs__);\ + } + +#define LIBNORMALFORM_ELLIPSIS_CHECKED__(CONNECTIVE)\ + LIBNORMALFORM_SENTENCE *ret__;\ + va_list args__;\ + va_start(args__, a);\ + ret__ = libnormalform_v##CONNECTIVE##_checked(n, a, args__);\ + va_end(args__);\ + return ret__; + +#define LIBNORMALFORM_TWO__(CONNECTIVE)\ + LIBNORMALFORM_SENTENCE *xs__[3] = {l, r, NULL};\ + if (!l || !r) {\ + libnormalform_free(l);\ + libnormalform_free(r);\ + return NULL;\ + }\ + return libnormalform_##CONNECTIVE(xs__); + +#define LIBNORMALFORM_MACRO__(CONNECTIVE, ...)\ + (libnormalform_##CONNECTIVE##_checked(\ + sizeof((LIBNORMALFORM_SENTENCE *[]){__VA_OPT__(__VA_ARGS__,) NULL}) / sizeof(LIBNORMALFORM_SENTENCE *) - 1U,\ + (LIBNORMALFORM_SENTENCE *[]){__VA_OPT__(__VA_ARGS__,) NULL})) + +/* } */ + + +struct libnormalform_term; + + + + + +#define LIBNORMALFORM_AVOID_FOR_ALL (UINT64_C(1) << 0) /**< Prefer ¬∃x.¬φ over ∀x.φ */ +#define LIBNORMALFORM_AVOID_NEGATED_FOR_ALL (UINT64_C(1) << 1) /**< Prefer ∃x.¬φ over ¬∀x.φ */ +#define LIBNORMALFORM_AVOID_FOR_ANY (UINT64_C(1) << 2) /**< Prefer ¬∀x.¬φ over ∃x.φ */ +#define LIBNORMALFORM_AVOID_NEGATED_FOR_ANY (UINT64_C(1) << 3) /**< Prefer ∀x.¬φ over ¬∃x.φ */ +#define LIBNORMALFORM_RELAX_FOR_ONE (UINT64_C(1) << 4) /**< Relax any positive ∃!x.φ into ∃x.φ */ +#define LIBNORMALFORM_REDUCE_XOR (UINT64_C(1) << 5) /**< Rewrite XOR to negation normal form */ +#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL (UINT64_C(1) << 6) /**< Express φ(x)∀x:θ(x) on the form ∀x.(θ(x) → φ(x)) */ +#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL (UINT64_C(1) << 7) /**< Express ¬(φ(x)∀x:θ(x)) on the form ¬∀x.(θ(x) → φ(x)) */ +#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY (UINT64_C(1) << 8) /**< Express φ(x)∃x:θ(x) on the form ∃x.(θ(x) ∧ φ(x)) */ +#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY (UINT64_C(1) << 9) /**< Express ¬(φ(x)∃x:θ(x)) on the form ¬∃x.(θ(x) ∧ φ(x)) */ +#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE (UINT64_C(1) << 10) /**< Express φ(x)∃!x:θ(x) on the form ∃!x.(θ(x) ∧ φ(x)) */ +#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ONE (UINT64_C(1) << 11) /**< Express ¬(φ(x)∃!x:θ(x)) on the form ¬∃!x.(θ(x) ∧ φ(x)) */ +#define LIBNORMALFORM_ELIMINATE_FOR_ALL (UINT64_C(1) << 12) /**< Relax any non-translatable ∀x.φ to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL (UINT64_C(1) << 13) /**< Relax any non-translatable ¬∀x.φ to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_FOR_ANY (UINT64_C(1) << 14) /**< Relax any non-translatable ∃x.φ to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY (UINT64_C(1) << 15) /**< Relax any non-translatable ¬∃x.φ to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_FOR_ONE (UINT64_C(1) << 16) /**< Relax any non-translatable ∃!x.φ to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE (UINT64_C(1) << 17) /**< Relax any ¬∃!x.φ to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_VARIABLE (UINT64_C(1) << 18) /**< Relax any positive variable literal to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE (UINT64_C(1) << 19) /**< Relax any negative variable literal to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_FUNCTION (UINT64_C(1) << 20) /**< Relax any positive function literal to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION (UINT64_C(1) << 21) /**< Relax any negative function literal to ⊤ */ +#define LIBNORMALFORM_ELIMINATE_XOR (UINT64_C(1) << 22) /**< Relax any non-reduce XOR to ⊤ */ +#define LIBNORMALFORM_ALL_EXPRESS_FLAGS__ ((UINT64_C(1) << 23) - 1U) /* For internal use */ + + +/** + * Opaque data type use to express and sentences + * + * This object incluses caches and preallocated memory + * makes object unsafe to be used from two different + * threads at the same time + * + * @seealso libnormalform_clone + */ +typedef struct libnormalform_sentence LIBNORMALFORM_SENTENCE; + + +/** + * Specification for how application provided strings + * shall be interpreted + */ +struct libnormalform_representation_spec { + /** + * Application-specific data that will be passed into + * `.get_variable`, `.get_function`, `.get_map`, and + * `.get_transformer` (making it reenterant so it can be + * called by multiple threads, or to configure the function) + * + * May be `NULL` + */ + void *user_data; + + /** + * Deserialise a variable from a unterminated string + * + * The function shall be able to return the reference + * to any `struct libnormalform_variable` given its + * `.identifier` sans NUL-termination + * + * The function shall be pure in the sence that if + * it is called twice (or more) with the identifer + * at the beginning of `s` it shall return the same + * pointer, not two different copies (`user_data` be + * use used to store the variables if they are + * constructed dynamically) + * + * May be `NULL` + * + * @param s The string beginning with the variable's + * identifier + * @param end_out Output parameter for the position in + * `s` after the last byte in the identifer + * @param user_data `.user_data` + * @return A pointer to the referenced variable, `NULL` + * on failure (`errno` may be set) + * + * It is recommended that, on failure, `errno` is set + * according to the below specification, however it is + * up to the application to choose what to do with `errno` + * + * @throws EINVAL `s` in not formatted to represent a valid variable + * @throws ENOENT `s` does not represent any known variable + */ + struct libnormalform_variable *(*get_variable)(char *s, char **end_out, void *user_data); + + /** + * Same as `.get_variable` except that it returns + * reference to a function (`struct libnormalform_function *`) + */ + struct libnormalform_function *(*get_function)(char *s, char **end_out, void *user_data); + + /** + * Same as `.get_variable` except that it returns + * reference to a domain (`struct libnormalform_map *`) + */ + struct libnormalform_map *(*get_map)(char *s, char **end_out, void *user_data); + + /** + * Same as `.get_transformer` except that it returns + * reference to a function (`struct libnormalform_transformer *`) + */ + struct libnormalform_transformer *(*get_transformer)(char *s, char **end_out, void *user_data); +}; + + +/** + * Type if a `struct libnormalform_term`, used to + * determine which member of `.term` to use and + * whether it is negated + */ +enum libnormalform_term_type { + LIBNORMALFORM_CONJUNCTION, /**< AND clause; empty clause is used for contradiction */ + LIBNORMALFORM_DISJUNCTION, /**< OR clause; empty clause is used for tautology */ + LIBNORMALFORM_EXCLUSIVE_DISJUNCTION, /**< XOR clause; never used for empty clauses */ + LIBNORMALFORM_TRANSFORMATION, /**< Transformater function with input **/ + LIBNORMALFORM_VARIABLE, /**< Positive variable literal **/ + LIBNORMALFORM_NEGATED_VARIABLE, /**< Negative variable literal **/ + LIBNORMALFORM_FUNCTION, /**< Positive boolean function literal **/ + LIBNORMALFORM_NEGATED_FUNCTION, /**< Negative boolean function literal **/ + LIBNORMALFORM_FOR_ALL, /**< ∀x∈D.(P(x) → Q(x)) expression */ + LIBNORMALFORM_NEGATED_FOR_ALL, /**< ¬∀x∈D.(P(x) → Q(x)) expression */ + LIBNORMALFORM_FOR_ANY, /**< ∃x∈D.(P(x) ∧ Q(x)) expression */ + LIBNORMALFORM_NEGATED_FOR_ANY, /**< ¬∃x∈D.(P(x) ∧ Q(x)) expression */ + LIBNORMALFORM_FOR_ONE, /**< ∃!x∈D.(P(x) ∧ Q(x)) expression */ + LIBNORMALFORM_NEGATED_FOR_ONE /**< ¬∃!x∈D.(P(x) ∧ Q(x)) expression */ +}; + + +/** + * Value of an atomic sentence + */ +enum libnormalform_value { + LIBNORMALFORM_FALSE = 0, /**< Variable has the value False */ + LIBNORMALFORM_TRUE = 1 /**< Variable has the value True */ +}; + + +/** + * Built in transformer functions + */ +enum libnormalform_builtin_transformer { + LIBNORMALFORM_NOT_BUILT_IN = 0, /**< Application provided transformer */ + LIBNORMALFORM_DOMAIN_VIEW, /**< Selects the `.key` from a `struct libnormalform_mapping *` */ + LIBNORMALFORM_IMAGE_VIEW /**< Selects the `.value` from a `struct libnormalform_mapping *` */ +}; + + +/** + * Relationship (dependency) between the value of two sentences + */ +enum libnormalform_sentences_relationship { + /** + * Left-hand implies right-hand (⊨ P → Q) + * + * Example: + * - P = ⋀{a, b}, Q = ⋀{a} + * + * Truthtable: + * P: 001 + * Q: 011 + * ∧: 001 + * ∨: 011 + * ⊕: 010 + * →: 111 + * ←: 101 + * + * Consequence: + * - P ∧ Q = P + * - P ∨ Q = Q + * - P ⊕ Q = ¬P ∧ Q + * - P → Q = ⊤ + * - P ← Q cannot be simplified + */ + LIBNORMALFORM_MATERIAL_IMPLICATION = -1, + + /** + * The terms are identical (⊨ P ↔ Q) + * + * Example: + * - P = ⋀{a, b}, Q = ⋀{a, b} + * + * Truthtable: + * P: 01 + * Q: 01 + * ∧: 01 + * ∨: 01 + * ⊕: 00 + * →: 11 + * ←: 11 + * + * Consequence: + * - P ∧ Q = P = Q + * - P ∨ Q = P = Q + * - P ⊕ Q = ⊥ + * - P → Q = ⊤ + * - P ← Q = ⊤ + */ + LIBNORMALFORM_IDENTICAL, + + /** + * Right-hand implies left-hand (⊨ P ← Q) + * + * Example: + * - P = ⋀{a}, Q = ⋀{a, b} + * + * Truthtable: + * P: 011 + * Q: 001 + * ∧: 001 + * ∨: 011 + * ⊕: 010 + * →: 101 + * ←: 111 + * + * Consequence: + * - P ∧ Q = Q + * - P ∨ Q = P + * - P ⊕ Q = P ∧ ¬Q + * - P → Q cannot be simplified + * - P ← Q = ⊤ + */ + LIBNORMALFORM_CONVERSE_IMPLICATION, + + /** + * The terms are the inverse of each other (⊨ P ↮ Q) + * + * Example: + * - P = a, Q = ¬a + * + * Truthtable: + * P: 01 + * Q: 10 + * ∧: 00 + * ∨: 11 + * ⊕: 11 + * →: 10 + * ←: 01 + * + * Consequence: + * - P ∧ Q = ⊥ + * - P ∨ Q = ⊤ + * - P ⊕ Q = ⊤ + * - P → Q = Q + * - P ← Q = P + */ + LIBNORMALFORM_MUTUALLY_INVERSE, + + /** + * Both terms cannot be satisfied at the same time, + * but are not each other's inverse (⊨ P ⊼ Q) + * + * Example: + * - P = ⋀{a, b}, Q = ⋀{¬b} + * + * Truthtable: + * P: 001 + * Q: 010 + * ∧: 000 + * ∨: 011 + * ⊕: 011 + * →: 110 + * ←: 101 + * + * Consequence: + * - P ∧ Q = ⊥ + * - P ∨ Q cannot be simplified + * - P ⊕ Q = P ∨ Q + * - P → Q = ¬P + * - P ← Q = ¬Q + */ + LIBNORMALFORM_MUTUALLY_EXCLUSIVE, + + /** + * The terms cannot be unsatisfied at the same time, + * but they are not identical (⊨ P ∨ Q) + * + * Example: + * - P = ⋁{a, b}, Q = ⋁{¬b} + * + * Truthtable: + * P: 011 + * Q: 101 + * ∧: 001 + * ∨: 111 + * ⊕: 110 + * →: 101 + * ←: 011 + * + * Consequence: + * - P ∧ Q cannot be simplified + * - P ∨ Q = ⊤ + * - P ⊕ Q = ¬P ∨ ¬Q + * - P → Q = Q + * - P ← Q = P + */ + LIBNORMALFORM_JOINTLY_UNDENIABLE, + + /** + * The terms are unrelated to each other + * + * Example: + * - P = a, Q = b + * + * Truthtable: + * P: 0011 + * Q: 0101 + * ∧: 0001 + * ∨: 0111 + * ⊕: 0110 + * →: 1101 + * ←: 1011 + * + * Consequence: + * - P ∧ Q cannot be simplified + * - P ∨ Q cannot be simplified + * - P ⊕ Q cannot be simplified + * - P → Q cannot be simplified + * - P ← Q cannot be simplified + */ + LIBNORMALFORM_MUTUALLY_INDEPENDENT +}; + + + +/** + * Relationship (commonality) between the value of two domains + * + * (The documentation uses the term "set", however, + * properly they are bags (multisets), however this + * is only important for uniqueness qualification; + * for the mathematics, you can thing about it as + * sets) + */ +enum libnormalform_domain_relationship { + /** + * The left-hand set is a superset of the right-hand set (A ⊇ B) + * + * Example: + * - A = {a, b}, B = {a} + * + * Euler diagram: + * ┌────────────────────────────┐ + * │ ┌─A────────────────┐ │ + * │ │╱╱╱╱╱╱╱┌─B──────┐╱│ │ + * │ │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│ │ + * │ │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│ │ + * │ │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│ │ + * │ │╱╱╱╱╱╱╱└────────┘╱│ │ + * │ │╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱│ │ + * │ └──────────────────┘ │ + * └────────────────────────────┘ + * + * Venn diagram of possibly non-empty intersections: + * ┌────────────────────────────┐ + * │ ┌─A─────────────┐ │ + * │ │███████████████│ │ + * │ │██████┌────────┼──────┐ │ + * │ │██████│████████│ │ │ + * │ │██████│████████│ │ │ + * │ └──────┼────────┘ │ │ + * │ │ │ │ + * │ └─────────────B─┘ │ + * └────────────────────────────┘ + * + * Consequence: + * - A ∩ B = B + * - A ∪ B = A + * - A ∆ B = A ∖ B + * - ⋀A ⊨ ⋀B + * - ⋁B ⊨ ⋁A + * - ⋀A ∧ ⋀B = ⋀A + * - ⋀A ∨ ⋀B = ⋀B + * - ⋀A ⊕ ⋀B = ¬⋀A ∧ ⋀B + * - ⋀A → ⋀B = ⊤ + * - ⋀A ← ⋀B cannot be simplified + * - ⋁A ∧ ⋁B = ⋁B + * - ⋁A ∨ ⋁B = ⋁A + * - ⋁A ⊕ ⋁B = ⋁A ∧ ¬⋁B + * - ⋁A → ⋁B cannot be simplified + * - ⋁A ← ⋁B = ⊤ + */ + LIBNORMALFORM_SUPERSET_OF = -1, + + /** + * The two terms are identical (A = B) + * + * Example: + * - A = {a, b}, B = {a, b} + * + * Euler diagram: + * ┌────────────────────────────┐ + * │ ┌─A,B──────────────┐ │ + * │ │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│ │ + * │ │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│ │ + * │ │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│ │ + * │ │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│ │ + * │ │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│ │ + * │ │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│ │ + * │ └──────────────────┘ │ + * └────────────────────────────┘ + * + * Venn diagram of possibly non-empty intersections: + * ┌────────────────────────────┐ + * │ ┌─A─────────────┐ │ + * │ │ │ │ + * │ │ ┌────────┼──────┐ │ + * │ │ │████████│ │ │ + * │ │ │████████│ │ │ + * │ └──────┼────────┘ │ │ + * │ │ │ │ + * │ └─────────────B─┘ │ + * └────────────────────────────┘ + * + * Consequence: + * - A ∩ B = A = B + * - A ∪ B = A = B + * - A ∆ B = ∅ + * - ⋀A = ⋀B + * - ⋁A = ⋁B + * - ⋀A ∧ ⋀B = ⋀A = ⋀B + * - ⋀A ∨ ⋀B = ⋀A = ⋀B + * - ⋀A ⊕ ⋀B = ⊥ + * - ⋀A → ⋀B = ⊤ + * - ⋀A ← ⋀B = ⊤ + * - ⋁A ∧ ⋁B = ⋁A = ⋁B + * - ⋁A ∨ ⋁B = ⋁A = ⋁B + * - ⋁A ⊕ ⋁B = ⊥ + * - ⋁A → ⋁B = ⊤ + * - ⋁A ← ⋁B = ⊤ + */ + LIBNORMALFORM_SAME_AS, + + /** + * The left-hand set is a subset of the right-hand set (A ⊆ B) + * + * Example: + * - A = {a}, B = {a, b} + * + * Euler diagram: + * ┌────────────────────────────┐ + * │ ┌─B────────────────┐ │ + * │ │╲┌─A──────┐╲╲╲╲╲╲╲│ │ + * │ │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│ │ + * │ │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│ │ + * │ │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│ │ + * │ │╲└────────┘╲╲╲╲╲╲╲│ │ + * │ │╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲│ │ + * │ └──────────────────┘ │ + * └────────────────────────────┘ + * + * Venn diagram of possibly non-empty intersections: + * ┌────────────────────────────┐ + * │ ┌─A─────────────┐ │ + * │ │ │ │ + * │ │ ┌────────┼──────┐ │ + * │ │ │████████│██████│ │ + * │ │ │████████│██████│ │ + * │ └──────┼────────┘██████│ │ + * │ │███████████████│ │ + * │ └─────────────B─┘ │ + * └────────────────────────────┘ + * + * Consequence: + * - A ∩ B = A + * - A ∪ B = B + * - A ∆ B = B ∖ A + * - ⋀B ⊨ ⋀A + * - ⋁A ⊨ ⋁B + * - ⋀A ∧ ⋀B = ⋀B + * - ⋀A ∨ ⋀B = ⋀A + * - ⋀A ⊕ ⋀B = ⋀A ∧ ¬⋀B + * - ⋀A → ⋀B cannot be simplified + * - ⋀A ← ⋀B = ⊤ + * - ⋁A ∧ ⋁B = ⋁A + * - ⋁A ∨ ⋁B = ⋁B + * - ⋁A ⊕ ⋁B = ¬⋁A ∧ ⋁B + * - ⋁A → ⋁B = ⊤ + * - ⋁A ← ⋁B cannot be simplified + */ + LIBNORMALFORM_SUBSET_OF, + + /** + * The sets have no common elements (A ∩ B = ∅) + * + * Example: + * - A = {a}, B = {b} + * + * Euler diagram: + * ┌────────────────────────────┐ + * │ ┌─A───────┐ ┌─B───────┐ │ + * │ │╱╱╱╱╱╱╱╱╱│ │╲╲╲╲╲╲╲╲╲│ │ + * │ │╱╱╱╱╱╱╱╱╱│ │╲╲╲╲╲╲╲╲╲│ │ + * │ │╱╱╱╱╱╱╱╱╱│ │╲╲╲╲╲╲╲╲╲│ │ + * │ │╱╱╱╱╱╱╱╱╱│ │╲╲╲╲╲╲╲╲╲│ │ + * │ │╱╱╱╱╱╱╱╱╱│ │╲╲╲╲╲╲╲╲╲│ │ + * │ │╱╱╱╱╱╱╱╱╱│ │╲╲╲╲╲╲╲╲╲│ │ + * │ └─────────┘ └─────────┘ │ + * └────────────────────────────┘ + * + * Venn diagram of possibly non-empty intersections: + * ┌────────────────────────────┐ + * │ ┌─A─────────────┐ │ + * │ │███████████████│ │ + * │ │██████┌────────┼──────┐ │ + * │ │██████│ │██████│ │ + * │ │██████│ │██████│ │ + * │ └──────┼────────┘██████│ │ + * │ │███████████████│ │ + * │ └─────────────B─┘ │ + * └────────────────────────────┘ + * + * Consequence: + * - A ∩ B = ∅ + * - A ∪ B cannot be simplified + * - A ∆ B = A ∪ B + * - ⋀A ∧ ⋀B = ⋀(A ∪ B) + * - ⋀A ∨ ⋀B cannot be simplified + * - ⋀A ⊕ ⋀B cannot be simplified + * - ⋀A → ⋀B cannot be simplified + * - ⋀A ← ⋀B cannot be simplified + * - ⋁A ∧ ⋁B cannot be simplified + * - ⋁A ∨ ⋁B = ⋁(A ∪ B) + * - ⋁A ⊕ ⋁B cannot be simplified + * - ⋁A → ⋁B cannot be simplified + * - ⋁A ← ⋁B cannot be simplified + */ + LIBNORMALFORM_DISJOINT_WITH, + + /** + * Both sets have unique elements (A ⊆ A ∪ B ⊇ B, A ∩ B ⊇ ∅) + * + * Example: + * - A = {a, b}, B = {b, c} + * + * Euler diagram: + * ┌────────────────────────────┐ + * │ ┌─A─────────────┐ │ + * │ │╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱│ │ + * │ │╱╱╱╱╱╱┌────────┼────B─┐ │ + * │ │╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲│ │ + * │ │╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲│ │ + * │ └──────┼────────┘╲╲╲╲╲╲│ │ + * │ │╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲│ │ + * │ └───────────────┘ │ + * └────────────────────────────┘ + * + * Venn diagram of possibly non-empty intersections: + * ┌────────────────────────────┐ + * │ ┌─A─────────────┐ │ + * │ │███████████████│ │ + * │ │██████┌────────┼──────┐ │ + * │ │██████│████████│██████│ │ + * │ │██████│████████│██████│ │ + * │ └──────┼────────┘██████│ │ + * │ │███████████████│ │ + * │ └─────────────B─┘ │ + * └────────────────────────────┘ + * + * Consequence: + * - A ∩ B cannot be simplified + * - A ∪ B cannot be simplified + * - A ∆ B cannot be simplified + * - ⋀A ∧ ⋀B = ⋀(A ∪ B) + * - ⋀A ∨ ⋀B cannot be simplified + * - ⋀A ⊕ ⋀B cannot be simplified + * - ⋀A → ⋀B cannot be simplified + * - ⋀A ← ⋀B cannot be simplified + * - ⋁A ∧ ⋁B cannot be simplified + * - ⋁A ∨ ⋁B = ⋁(A ∪ B) + * - ⋁A ⊕ ⋁B cannot be simplified + * - ⋁A → ⋁B cannot be simplified + * - ⋁A ← ⋁B cannot be simplified + */ + LIBNORMALFORM_CONJOINT_WITH +}; + + +/** + * Variable that can be referenced in a sentence + */ +struct libnormalform_variable { + /** + * The value of the sentence + * + * This need not be sent when the sentence is constructed, + * but not be set before it is evaluated; it is only used + * by `libnormalform_evaluate` + */ + enum libnormalform_value value; + + /** + * Application-specific data that the application + * could use to identify the variable + * + * May be `NULL` + */ + void *user_data; + + /** + * Identifier for variable + * + * This need only be set when `libnormalform_to_string` + * is called. The value must be parsable by the application + * without any explicit termination + */ + const char *identifier; + + /** + * `NULL` or copy of of the object for `libnormalform_clone` + * + * This field should normally be unset, but before calling + * `libnormalform_clone`, the application must set it + * either to `NULL` (if the clone can use the same reference) + * or to a clone of the variable. + */ + struct libnormalform_variable *copy_for_clone; +}; + + +/** + * Boolean-codomain function that can be referenced in a sentence + */ +struct libnormalform_function { + /** + * Function that is used to evaluate the trueness of something + * + * @param user_data `.user_data` + * @param input Input to the function, normally it will + * be `NULL`, but it is inside the antecedent + * for a qualifier, it will be the `.key` + * for some `struct libnormalform_mapping`, + * and if it is inside the predicate of a + * qualifier, it will be the `.value` + * for some `struct libnormalform_mapping` + * @return 1 if the function is true, + * 0 if the function is false, + * -1 on failure (the function may set `errno`) + * + * For `libnormalform_exists`, `libnormalform_nexists`, + * and `libnormalform_unique`, it will only be called + * for the `.key` for `struct libnormalform_mapping`'s + * + * For `libnormalform_universally`, `libnormalform_existentially`, + * and `libnormalform_uniquely`, it will only be called + * for the `.value` for `struct libnormalform_mapping`'s + */ + int (*evaluate)(void *user_data, void *input); + + /** + * Application-specific data that will be passed into + * `.evaluate` (making it reenterant so it can be called + * by multiple threads, or to configure the function) + * + * May be `NULL` + */ + void *user_data; + + /** + * Identifier for function + * + * This need only be set when `libnormalform_to_string` + * is called. The value must be parsable by the application + * without any explicit termination + */ + const char *identifier; + + /** + * `NULL` or copy of of the object for `libnormalform_clone` + * + * This field should normally be unset, but before calling + * `libnormalform_clone`, the application must set it + * either to `NULL` (if the clone can use the same reference) + * or to a clone of the variable. + */ + struct libnormalform_function *copy_for_clone; + + /** + * See `.requires_relaxation` + */ + struct libnormalform_function *relaxation; + + /** + * Before calling `libnormalform_express`, `libnormalform_dnf`, + * or `libnormalform_cnf` this shall be set to 0 if the function + * may keep the function as is, or to a non-0 value if it shall + * be replaced `.relaxation` or by TRUE if `.relaxation` is `NULL` + */ + int requires_relaxation; +}; + + +/** + * Generic function that can be referenced in a sentence + * + * The function must be pure and distributive over any boolean operator + * (it must be an endomorphism). That is, the output is always the + * same for the same input without any side effects, and for any sentence + * A * B, where * is any boolean operator and F is the function, + * F(A * B) = F(A) * F(B). + */ +struct libnormalform_transformer { + /** + * Function that is used to transform input + * + * @param user_data `.user_data` + * @param input Input to the function, normally it will + * be `NULL`, but it is inside the antecedent + * for a qualifier, it will be the `.key` + * for some `struct libnormalform_mapping`, + * and if it is inside the predicate of a + * qualifier, it will be the `.value` + * for some `struct libnormalform_mapping`, + * except that during the create of a + * `struct libnormalform_term`, the library + * may insert builtin transformers that will + * have the `struct libnormalform_mapping *` + * as input and will output the `.key` or + * `.value` + * @return The transformation of `input` (not `NULL`), + * `NULL` on failure (the function may set `errno`) + * + * For `libnormalform_exists`, `libnormalform_nexists`, + * and `libnormalform_unique`, it will only be called + * for the `.key` for `struct libnormalform_mapping`'s + * + * For `libnormalform_universally`, `libnormalform_existentially`, + * and `libnormalform_uniquely`, it will only be called + * for the `.value` for `struct libnormalform_mapping`'s + */ + void *(*transform)(void *user_data, void *input); + + /** + * The function is called when the output of `.transform` + * is not longer needed by the library + * + * May be `NULL` + * + * This function is not called if `.transform` output `NULL` + * + * @param user_data `.user_data` + * @param output The pointer that was returned by `.transform` + */ + void (*deallocate)(void *user_data, void *output); + + /** + * Application-specific data that will be passed into + * `.transform` and `.deallocate` (making them reenterant + * so it can be called by multiple threads, or to + * configure the function) + * + * May be `NULL` + */ + void *user_data; + + /** + * Identifier for function + * + * This need only be set when `libnormalform_to_string` + * is called. The value must be parsable by the application + * without any explicit termination + */ + const char *identifier; + + /** + * `NULL` or copy of of the object for `libnormalform_clone` + * + * This field should normally be unset, but before calling + * `libnormalform_clone`, the application must set it + * either to `NULL` (if the clone can use the same reference) + * or to a clone of the variable. + */ + struct libnormalform_transformer *copy_for_clone; + + /** + * Before calling `libnormalform_express`, `libnormalform_dnf`, + * or `libnormalform_cnf` this shall be set to 0 if the function + * may keep the function, or to a non-0 value if it shall + * be replaced with a tautology + */ + int requires_elimination; + + /** + * This field will automatically be set to `LIBNORMALFORM_NOT_BUILT_IN` + * to indicated that the object originates in the application, + * however a `struct libnormalform_term *` created by the library + * (via `libnormalform_express`, `libnormalform_dnf`, or + * `libnormalform_cnf`) can contain objects with other values in this + * field, to describe what it does. In particular, depending on the + * flags used when creating the `struct libnormalform_term *`, + * qualification sentences may contain `LIBNORMALFORM_DOMAIN_VIEW` + * and `LIBNORMALFORM_IMAGE_VIEW` and transformers. + */ + enum libnormalform_builtin_transformer builtin; +}; + + +/** + * Key–value pair + */ +struct libnormalform_mapping { + /** + * Key + * + * In mapped qualifiers (`libnormalform_all`, + * `libnormalform_any`, `libnormalform_one`), this + * is used as the input for the antecedent + * + * In unmapped qualifiers (`libnormalform_exists`, + * `libnormalform_nexists`, `libnormalform_unique`), + * is this used as the input for the predicate + * + * In premapped qualifiers (`libnormalform_universally`, + * `libnormalform_existentially`, `libnormalform_uniquely`), + * is this unused + * + * Unused for domain size checks (`libnormalform_empty`, + * `libnormalform_nonempty`, `libnormalform_singleton`) + */ + void *key; + + /** + * Value + * + * In mapped qualifiers (`libnormalform_all`, + * `libnormalform_any`, `libnormalform_one`), this + * is used as the input for the predicate + * + * In unmapped qualifiers (`libnormalform_exists`, + * `libnormalform_nexists`, `libnormalform_unique`), + * is this unused + * + * In premapped qualifiers (`libnormalform_universally`, + * `libnormalform_existentially`, `libnormalform_uniquely`), + * is this used as the input for the predicate + * + * Unused for domain size checks (`libnormalform_empty`, + * `libnormalform_nonempty`, `libnormalform_singleton`) + */ + void *value; +}; + + +/** + * Domain of interest for qualifiers + */ +struct libnormalform_map { + /** + * Associative array over values in the domain + */ + struct libnormalform_mapping *mappings; + + /** + * The number of elements in `.mappings` + */ + size_t nmappings; + + /** + * Application-specific data that the application + * could use to identify the domain + * + * May be `NULL` + */ + void *user_data; + + /** + * Identifier for domain + * + * This need only be set when `libnormalform_to_string` + * is called. The value must be parsable by the application + * without any explicit termination + */ + const char *identifier; + + /** + * `NULL` or copy of of the object for `libnormalform_clone` + * + * This field should normally be unset, but before calling + * `libnormalform_clone`, the application must set it + * either to `NULL` (if the clone can use the same reference) + * or to a clone of the variable. + */ + struct libnormalform_map *copy_for_clone; +}; + + +struct libnormalform_atom_comparsion { + int version; + enum libnormalform_sentences_relationship relationship; +}; + +struct libnormalform_domain_comparsion { + int version; + enum libnormalform_domain_relationship relationship; +}; + +struct libnormalform_analysers { /* TODO doc */ + void *user_data; + int (*compare_variable_to_variable)(void *user_data, struct libnormalform_atom_comparsion *result, + struct libnormalform_variable *left, struct libnormalform_variable *right); + int (*compare_function_to_function)(void *user_data, struct libnormalform_atom_comparsion *result, + struct libnormalform_function *left, struct libnormalform_function *right); + int (*compare_variable_to_function)(void *user_data, struct libnormalform_atom_comparsion *result, + struct libnormalform_variable *left, struct libnormalform_function *right); + int (*compare_domains)(void *user_data, struct libnormalform_domain_comparsion *result, + struct libnormalform_map *left, struct libnormalform_map *right); +}; + + +/** + * Qualifier + */ +struct libnormalform_qualification { + struct libnormalform_map *map; /**< The domain of interest */ + struct libnormalform_term *antecedent; /**< The antecedent, `NULL` if joined with the predicate */ + struct libnormalform_term *predicate; /**< The predicate */ +}; + + +/** + * Clause of terms + */ +struct libnormalform_clause { + struct libnormalform_term *terms; /**< The terms in the clause */ + size_t nterms; /**< The number of terms in the clause */ +}; + + +/** + * Transformater function with input + */ +struct libnormalform_transformation { + struct libnormalform_transformer *transformer; /**< The transformer function */ + struct libnormalform_term *sentence; /**< The sentence the transformation is over */ +}; + + +/** + * Application-readable sentence + */ +struct libnormalform_term { + /** + * The type of the clause, qualifier, literal, or transformation + */ + enum libnormalform_term_type type; + + /** + * Whether the term or own of its subterms have been reduced; + */ + int reduced; + + /** + * The description of the sentence + */ + union { + /** + * Use if `.type` is `LIBNORMALFORM_DISJUNCTION` + */ + struct libnormalform_clause disjunction; + + /** + * Use if `.type` is `LIBNORMALFORM_CONJUNCTION` + */ + struct libnormalform_clause conjunction; + + /** + * Use if `.type` is `LIBNORMALFORM_EXCLUSIVE_DISJUNCTION` + */ + struct libnormalform_clause exclusive_disjunction; + + /** + * Use if `.type` is `LIBNORMALFORM_DISJUNCTION`, + * `LIBNORMALFORM_CONJUNCTION`, or + * `LIBNORMALFORM_EXCLUSIVE_DISJUNCTION` + */ + struct libnormalform_clause clause; + + /** + * Use if `.type` is `LIBNORMALFORM_TRANSFORMATION` + */ + struct libnormalform_transformation transformation; + + /** + * Use if `.type` is `LIBNORMALFORM_VARIABLE` or + * `LIBNORMALFORM_NEGATED_VARIABLE` + */ + struct libnormalform_variable *variable; + + /** + * Use if `.type` is `LIBNORMALFORM_FUNCTION` or + * `LIBNORMALFORM_NEGATED_FUNCTION` + */ + struct libnormalform_function *function; + + /** + * Use if '.type` is `LIBNORMALFORM_FOR_ALL` or + * `LIBNORMALFORM_NEGATED_FOR_ALL` + */ + struct libnormalform_qualification for_all; + + /** + * Use if '.type` is `LIBNORMALFORM_FOR_ANY` or + * `LIBNORMALFORM_NEGATED_FOR_ANY` + */ + struct libnormalform_qualification for_any; + + /** + * Use if '.type` is `LIBNORMALFORM_FOR_ONE` or + * `LIBNORMALFORM_NEGATED_FOR_ONE` + */ + struct libnormalform_qualification for_one; + + /** + * Use if '.type` is `LIBNORMALFORM_FOR_ALL`, + * `LIBNORMALFORM_NEGATED_FOR_ALL`, `LIBNORMALFORM_FOR_ANY`, + * `LIBNORMALFORM_NEGATED_FOR_ANY`, `LIBNORMALFORM_FOR_ONT`, + * or `LIBNORMALFORM_NEGATED_FOR_ONE` + */ + struct libnormalform_qualification qualification; + } term; +}; + + + + + +/** + * Increase the reference count of a sentence object by 1 + * + * @param this The sentence object + * @return `this` on success, `NULL` on failure + * + * @throws ENOMEM The reference count is already maximised (at SIZE_MAX) + * + * Reasonable application can safely assume that `this` is always returned + * + * Note, `NULL` is returned without `errno` modified if `this` is `NULL` + * + * Be aware that this function is not thread-safe + * + * @seealso libnormalform_clone + * @seealso libnormalform_free + */ +LIBNORMALFORM_SENTENCE *(libnormalform_ref)(LIBNORMALFORM_SENTENCE *this); + + +/** + * Create a copy of a sentence object + * + * This may be necessary as usage of sentence objects are not thread-safe, + * creating a copy of a sentence object will allow one thread to safely + * use one copy and another thread the other copy + * + * Before calling this function, the application shall set `.copy_for_clone` + * in each `struct libnormalform_variable`, `struct libnormalform_function`, + * `struct libnormalform_map` and `struct libnormalform_transformer`, used + * by the sentence. `.copy_for_clone` shall either be set to `NULL` or a copy + * of object. If `NULL` is used, the copy of `this` will use the same + * instance of the object as `this`. + * + * @param this The sentence object + * @return A unique pointer on success or `NULL` if + * `this` is `NULL`; `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create a copy of `this` + * + * Be aware that this function is not thread-safe + * + * @seealso libnormalform_ref + * @seealso libnormalform_free + */ +LIBNORMALFORM_USE_RESULT__ +LIBNORMALFORM_SENTENCE *(libnormalform_clone)(LIBNORMALFORM_SENTENCE *this); + + +/** + * When `this` is a `LIBNORMALFORM_SENTENCE *`: + * + * Decrease the reference count of a sentence object by 1, + * if the object reference count reaches 0, deallocate the + * object. + * + * Because all functions that return a new sentence object + * (excluding `libnormalform_clone`), adopt the ownership + * of the reference to each input sentence (and may create + * it's own subsentences), this function is called recursively, + * and the application shall not attempt to call this function + * for sentences used to create other sentences + * + * Be aware the this function will not deallocate any + * `struct libnormalform_variable *`, + * `struct libnormalform_function *`, or + * `struct libnormalform_map *` used in the sentence as + * these are owned any managed by the application + * + * When `this` is a `struct libnormalform_term *`: + * + * Recursively deallocate `this`. This will only deallocate + * `this` and subobjects with the same type + * + * If `.type` is invalid for `this` or any subobject, the + * function's behaviour is undefined + * + * This function is a no-operation function when `this` is `NULL` + * + * @param this The object + * + * This function's behaviour is undefined if `this` is not `NULL` + * but not of the one of the above listed types + * + * Be aware that this function is not thread-safe + */ +void (libnormalform_free)(void *this); + + +/** + * Evaluate a sentence to determine it's trueness + * + * Before calling this function, the application code shall + * configure any `struct libnormalform_variable`, + * `struct libnormalform_function`, and `struct libnormalform_map` + * used by the sentence. For each `struct libnormalform_variable`, + * `.value` shall either be set to `LIBNORMALFORM_TRUE` or + * `LIBNORMALFORM_FALSE` to indicate the value of the atom. + * For each `struct libnormalform_function`, `.evaluate` shall + * be set to a pointer to function that evaluates the input and + * `.user_data` shall be set to any application data the function + * needs to operate; `.evaluate` shall return 1, 0, or -1 as + * specified for this function; and may set `errno` to indicate + * an error (library itself does not look at `errno`, but may + * be used to signal the error to the application, of course + * the error may also be specified to the application in an + * application-specific way). For each `struct libnormalform_map`, + * `.mappings` shall be to the associated array of values + * that shall be tested by the qualifier-sentence it is + * used by, and `.nmappings` shall be set to the number of + * pairs in this array. + * + * @param this The sentence to evaluate + * @return 1 if the sentence is true, + * 0 if the sentence is false, + * -1 on failure + * + * Only application code may cause this function to + * fail, therefore no error codes are predefined for + * this function, instead `errno` is only set by + * the failing application code + * + * Be aware that this function is not thread-safe + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +int (libnormalform_evaluate)(LIBNORMALFORM_SENTENCE *this); + + + + + +/** + * Return an application readable expression of a statement in negation + * normal form, optionally with XOR, and reduce the statement to a + * statement that is at least as true (but as false as possible), and + * is minimised, according what the application specifies that it can + * work with + * + * Before calling this function, the application shall set `.relaxation` + * `.requires_relaxation` in each `struct libnormalform_function` used + * used by the sentence. `.requires_relaxation` may be set as 0 if the + * function shall not be replaced (in this case `.relaxation` need not + * be set), but set to 1 if the function most be replaced with a more + * true function. In the latter case, `.relaxation` shall either be set + * to the new function or to `NULL`; if set to null, the function is + * reduced to a tautological sentence. For any `libnormalform_transformer` + * it must also set `.requires_elimination` to 1 if the transformation + * must be replaces with a tautology, and 0 otherwise. + * + * @param this The sentence to describe + * @param flags The bitwise OR of any number of the following values: + * - LIBNORMALFORM_AVOID_FOR_ALL: Prefer ¬∃x.¬φ over ∀x.φ + * - LIBNORMALFORM_AVOID_NEGATED_FOR_ALL: Prefer ∃x.¬φ over ¬∀x.φ + * - LIBNORMALFORM_AVOID_FOR_ANY: Prefer ¬∀x.¬φ over ∃x.φ + * - LIBNORMALFORM_AVOID_NEGATED_FOR_ANY: Prefer ∀x.¬φ over ¬∃x.φ + * - LIBNORMALFORM_RELAX_FOR_ONE: Relax any positive ∃!x.φ into ∃x.φ + * - LIBNORMALFORM_REDUCE_XOR: Do not use XOR in the returned statement, + * but transform it to negation normal form + * - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL Express φ(x)∀x:θ(x) on the form ∀x.(θ(x) → φ(x)) + * - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL Express ¬(φ(x)∀x:θ(x)) on the form ¬∀x.(θ(x) → φ(x)) + * - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY Express φ(x)∃x:θ(x) on the form ∃x.(θ(x) ∧ φ(x)) + * - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY Express ¬(φ(x)∃x:θ(x)) on the form ¬∃x.(θ(x) ∧ φ(x)) + * - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE Express φ(x)∃!x:θ(x) on the form ∃!x.(θ(x) ∧ φ(x)) + * - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ONE Express ¬(φ(x)∃!x:θ(x)) on the form ¬∃!x.(θ(x) ∧ φ(x)) + * - LIBNORMALFORM_ELIMINATE_FOR_ALL Relax any non-translatable ∀x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL Relax any non-translatable ¬∀x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_FOR_ANY Relax any non-translatable ∃x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_IN_NEGATED_FOR_ANY Relax any non-translatable ¬∃x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_IN_FOR_ONE Relax any non-translatable ∃!x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_IN_NEGATED_FOR_ONE Relax any ¬∃!x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_VARIABLE Relax any positive variable literal to ⊤ + * - LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE Relax any negative variable literal to ⊤ + * - LIBNORMALFORM_ELIMINATE_FUNCTION Relax any positive function literal to ⊤ + * - LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION Relax any negative function literal to ⊤ + * - LIBNORMALFORM_ELIMINATE_XOR Remove all XOR's (nullified by `LIBNORMALFORM_REDUCE_XOR`) + * @param analysers Application provided functions to help reduce the statement, or `NULL` + * @return The description of the sentence, `NULL` on failure; + * the returned pointer shall be deallocated with + * `libnormalform_free` when it is no longer needed + * + * @seealso libnormalform_dnf + * @seealso libnormalform_cnf + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1) +struct libnormalform_term *(libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO man */ + const struct libnormalform_analysers *analysers); + + +/** + * Variant of `libnormalform_express` that always canonicalises + * the statement to disjunctive normal form + * + * @param this The sentence to describe + * @param flags See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR` + * is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not, + * but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless + * there is a risk that it would be too costly (EXPSPACE) + * @param analysers Application provided functions to help reduce the statement, or `NULL` + * @return The description of the sentence, `NULL` on failure; + * the returned pointer shall be deallocated with + * `libnormalform_free` when it is no longer needed + * + * @seealso libnormalform_express + * @seealso libnormalform_cnf + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1) +struct libnormalform_term *(libnormalform_dnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO */ /* TODO man */ + const struct libnormalform_analysers *analysers); + + +/** + * Variant of `libnormalform_express` that always canonicalises + * the statement to conjuctive normal form + * + * @param this The sentence to describe + * @param flags See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR` + * is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not, + * but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless + * there is a risk that it would be too costly (EXPSPACE) + * @param analysers Application provided functions to help reduce the statement, or `NULL` + * @return The description of the sentence, `NULL` on failure; + * the returned pointer shall be deallocated with + * `libnormalform_free` when it is no longer needed + * + * @seealso libnormalform_express + * @seealso libnormalform_dnf + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1) +struct libnormalform_term *(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO */ /* TODO man */ + const struct libnormalform_analysers *analysers); + + +/** + * Convert a sentence object to a string that can be parsed + * by `libnormalform_from_string` (and is somewhat human-readable) + * + * Before calling this function, the application shall set `.identifier` + * in each `struct libnormalform_variable`, `struct libnormalform_function`, + * `struct libnormalform_map`, and `struct libnormalform_transformer` used + * by the sentence to a non-`NULL`, unique string that identifies (but + * does not necessarily describe) the object. The application must be able + * to find the end of any such string without any explicit termination + * (e.g., eithout there being a NUL-terminator) + * + * Note that when a sentence is created, it is optimised and + * reduced into fewer types of connetives (it's reducted into + * negation normal form, except with XOR allowed, but not + * necessarily to any canonical form) during construction, + * so this function will not necessarily reproduce the sentence + * as it was specified when it was constructed. + * + * @param this The sentence object to serialise + * @return String-representation of `this`, `NULL` failure; + * the caller shall deallocate the returned pointer + * with free(3) when it is no longer needed + * + * @throws ENOMEM Insufficient memory available to serialise `this` + * + * @seealso libnormalform_from_string + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_USE_FREE__ LIBNORMALFORM_NONNULL_INPUT__ +char *(libnormalform_to_string)(LIBNORMALFORM_SENTENCE *this); + + +/** + * Convert a string, created with `libnormalform_to_string` + * (or is on similar form), to sentence object + * + * The string shall be on the whitespace-insensitive form: + * + * constant ::= "TRUE" | "FALSE"; + * connective1 ::= "NOT"; + * connective2 ::= "AND" | "OR" | "XOR" | "IF" | "IMPLY" | + * "NAND" | "NOR" | "XNOR" | "NIF" | "NIMPLY"; + * qualifier0 ::= "EMPTY" | "NONEMPTY" | "SINGLETON"; + * qualifier1 ::= "EXISTS" | "NEXISTS" | "UNIQUE" | + * "EXISTENTIALLY" | "UNIVERSALLY" | "UNIQUELY"; + * qualifier2 ::= "ALL" | "ANY" | "ONE"; + * unary ::= connective1 [reference-point] "(" sentence ")"; + * variadic ::= connective2 [reference-point] "(" [sentence-list] ")"; + * sentence-list ::= sentence ["," sentence-list]; + * qualified0 ::= qualifier0 [reference-point] "(" map ")"; + * qualified1 ::= qualifier1 [reference-point] "(" map "," sentence ")"; + * qualified2 ::= qualifier2 [reference-point] "(" map "," sentence "," sentence ")"; + * atom ::= atom-var | atom-fun; + * atom-var ::= "VARIABLE" [reference-point] "(" variable ")"; + * atom-fun ::= "FUNCTION" [reference-point] "(" function ")"; + * transformation ::= "TRANSFORMATION" [reference-point] "(" transformer "," sentence ")"; + * reference-point ::= "@" decimal-number; + * reference ::= "REF(" decimal-number ")"; + * one-to-nine ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"; + * zero-to-nine ::= "0" | one-to-nine; + * decimal-number ::= "0" | positive-decimal; + * positive-decimal ::= one-to-nine [digits]; + * digits ::= zero-to-nine [digits]; + * sentence ::= constant | unary | variadic | qualified0 | qualified1 | + * qualified2 | atom | transformation | reference; + * + * where "sentence" is the root, and where "map" is parsed by `*spec->get_map`, + * "variable" is parsed by `*spec->get_variable`, "function" is parsed by + * `*spec->get_function`, and "transformer" is parsed by `*spec->get_transformer`. + * References must start at 0 and increment by one, in left-to-right order, + * every time reference point is specified, and forward-references are not allowed + * (this includes reference to containing sentence (whose reference ID is lower + * because it is written earlier)). + * + * @param s The representation of the sentence to deserialise + * @param end_out Output parameter for the end of `s`; + * if `NULL` the function will fail if `s` contains + * excess information + * @param spec Specification for how application managed objects + * are to be deserialise + * @return A unique pointer, that is a deserialisation of `s`, + * or `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to deserialise `s` + * @throws EINVAL `s` was not properly formatted + * @throws EINVAL `end_out` was `NULL` and `s` containd excess information + * @throws EDOM `s` contained a empty clause for a connective + * that does not support empty clauses + * @throws EDOM `s` contained a transformation over a qualifer + * @throws ENOENT `s` contained a variable but `spec->get_variable` was `NULL` + * @throws ENOENT `s` contained a boolean function but `spec->get_function` was `NULL` + * @throws ENOENT `s` contained a domain but `spec->get_map` was `NULL` + * @throws ENOENT `s` contained a transformation but `spec->get_transformer` was `NULL` + * + * If function in `spec` fails, this function will fail and keep `errno` + * as set by the function that failed + * + * The function itself does not modify `s` and can operate on read-only + * memory, however an offset of the string may be passed into application + * code. The application is free to modify `s` if it knows the memory + * is indeed writable. + * + * @seealso libnormalform_to_string + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1) LIBNORMALFORM_ONE_NONNULL_INPUT__(3) +LIBNORMALFORM_SENTENCE *(libnormalform_from_string)(char *s, char **end_out, const struct libnormalform_representation_spec *spec); + + + + + +/** + * Create an atomic sentence whose value is externally set + * + * @param variable The variable the sentence shall express + * @return A sentence object referencing `variable`, `NULL` on failure + * @throws ENOMEM Insufficient memory available to create the sentence + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_variable)(struct libnormalform_variable *variable); + + +/** + * Create an atomic sentence whose value is externally evaluated + * + * @param function The function the sentence shall express + * @return A sentence object referencing `function`, `NULL` on failure + * @throws ENOMEM Insufficient memory available to create the sentence + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_function)(struct libnormalform_function *function); + + +/** + * Create an endomorphic transformation of the input for a sentence + * + * `function->builtin` will automatically be initialised to `LIBNORMALFORM_NOT_BUILT_IN` + * + * @param function The transformation function + * @param sentence The sentence whose input shall be transformed + * @return A sentence whose input is transformed by `function`, `NULL` on failure + * @throws ENOMEM Insufficient memory available to create the sentence + * @throws EDOM `sentence` is a qualifier + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1) +LIBNORMALFORM_SENTENCE *(libnormalform_transformation)(struct libnormalform_transformer *function, LIBNORMALFORM_SENTENCE *sentence); + + +/** + * TRUE: Tautology + * + * Always true + * + * Commonly written "⊤", "1", or "T" + * + * @return An atomic sentence with a constant value of True, `NULL` on failure + * @throws ENOMEM Insufficient memory available to create the sentence + */ +LIBNORMALFORM_USE_RESULT__ +LIBNORMALFORM_SENTENCE *(libnormalform_true)(void); + + +/** + * FALSE: Contradiction + * + * Always false + * + * Commonly written "⊥", "1", or "F" + * + * @return An atomic sentence with a constant value of False, `NULL` on failure + * @throws ENOMEM Insufficient memory available to create the sentence + */ +LIBNORMALFORM_USE_RESULT__ +LIBNORMALFORM_SENTENCE *(libnormalform_false)(void); + + +/** + * NOT: Negation + * + * The condition must not be met: + * ¬0 = 1 + * ¬1 = 0 + * + * Properties: + * - Involution + * - Distribution over AND changes connective to OR (De Morgan's law) + * - Distribution over OR changes connective to AND (De Morgan's law) + * + * Commonly written "¬" ("¬x"), "~", or "!", or with overstroke + * + * @param x The sentence that should be negated; + * ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `x` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `x` to + * be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +LIBNORMALFORM_SENTENCE *(libnormalform_not)(LIBNORMALFORM_SENTENCE *x); + + +/** + * FOR ALL: Universal quantification (mapped) + * + * The predicate must be met for every element that the antecedent + * is met for; if no element exists, or the antecedent is false for + * every element, the sentence is true + * + * Properties: + * - Vacuous truth + * - ∀x∈D.P(x) → ⊤ = ⊤ + * - ∀x∈D.⊥ → Q(x) = ⊤ + * - ∀x∈D.⊤ → ⊥ ⊨ D = ∅ + * - Conjunction + * + * Commonly written "∀" ("∀x∈d.k(x) → v(x)", "∀x∈d (k(x) → v(x))", or "v(x) ∀ x∈d : k(x)") + * + * The antecedent is tested for every `.key` in the domain, + * and the predicate is tested for every associated `.value` + * where the antecedent is met; but the testing is cut short + * if the antecedent is met and not the predicate for an element + * + * @param d The domain of interest; ownership is retained by the caller + * @param k The antecedent; ownership is transfered to this function + * @param v The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `k` or `v` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `k` or + * `v` to be `NULL`) + * + * @seealso libnormalform_nexists + * @seealso libnormalform_universally + * @seealso libnormalform_any + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1) +LIBNORMALFORM_SENTENCE *(libnormalform_all)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v); + + +/** + * THERE EXISTS: Existential quantification (mapped) + * + * The predicate must be met for at least one element that the + * antecedent is met for; if no element exists, or the antecedent is + * false for every element, the sentence is false + * + * Properties: + * - Vacuous falsity + * - ∃x∈D.P(x) ∧ ⊥ = ⊥ + * - ∃x∈D.⊥ ∧ Q(x) = ⊥ + * - ∃x∈D.⊤ ∧ ⊤ ⊨ D ⊃ ∅ + * - Disjunction + * + * Commonly written "∃" ("∃x∈d.k(x) ∧ v(x)", "∃x∈d (k(x) ∧ v(x))", or "v(x) ∃ x∈d : k(x)") + * + * The antecedent is tested for every `.key` in the domain, + * and the predicate is tested for every associated `.value` + * where the antecedent is met; but the testing is cut short + * if both the antecedent and predicate is met for an element + * + * @param d The domain of interest; ownership is retained by the caller + * @param k The antecedent; ownership is transfered to this function + * @param v The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `k` or `v` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `k` or + * `v` to be `NULL`) + * + * @seealso libnormalform_exists + * @seealso libnormalform_existentially + * @seealso libnormalform_one + * @seealso libnormalform_all + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1) +LIBNORMALFORM_SENTENCE *(libnormalform_any)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v); + + +/** + * THERE EXISTS ONE: Unique existential quantification (mapped) + * + * The predicate must be met for exactly one element that the + * antecedent is met for; if no element exists, or the antecedent is + * false for every element, the sentence is false + * + * Properties: + * - Vacuous falsity + * - ∃!x∈D.P(x) ∧ ⊥ = ⊥ + * - ∃!x∈D.⊥ ∧ Q(x) = ⊥ + * - ∃!x∈D.⊤ ∧ ⊤ ⊨ |D| = 1 + * + * Commonly written "∃!" ("∃!x∈d.k(x) ∧ v(x)", "∃!x∈d (k(x) ∧ v(x))", or "v(x) ∃! x∈d : k(x)") + * + * The antecedent is tested for every `.key` in the domain, + * and the predicate is tested for every associated `.value` + * where the antecedent is met; but the testing is cut short + * if both the antecedent and predicate is met for two elements + * + * @param d The domain of interest; ownership is retained by the caller + * @param k The antecedent; ownership is transfered to this function + * @param v The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `k` or `v` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `k` or + * `v` to be `NULL`) + * + * @seealso libnormalform_unique + * @seealso libnormalform_uniquely + * @seealso libnormalform_any + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1) +LIBNORMALFORM_SENTENCE *(libnormalform_one)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v); + + + + + +/** + * AND: Conjunction + * + * Also known as BUT + * + * All conditions must be met + * + * 0 ∧ 0 = 0 + * 0 ∧ 1 = 0 + * 1 ∧ 0 = 0 + * 1 ∧ 1 = 1 + * + * Properties: + * - Vacuous truth + * - Identity singleton + * - Commutative + * - Associative + * - Distributive over OR + * - Distributive over XOR + * - ⊤ as identity + * - Dominated by ⊥ + * - Idempotent + * - Connecting complement results in contradiction + * - More lax term is absorbed (A ∧ (A ∨ B) simplifies to A) + * + * Commonly written "∧" ("⋀" if n-ary), "&", or with juxtaposition + * + * @param xs `NULL`-terminated list of sentences that should be + * joined by the connective AND; this can be any number + * of arguments, even none; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_AND + * @seealso libnormalform_and_checked + * @seealso libnormalform_andl_checked + * @seealso libnormalform_vand_checked + * @seealso libnormalform_andl + * @seealso libnormalform_vand + * @seealso libnormalform_and2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_and)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * OR: Disjunction + * + * Also known as Inclusive disjunction + * + * At least one condition must be met + * + * 0 ∨ 0 = 0 + * 0 ∨ 1 = 1 + * 1 ∨ 0 = 1 + * 1 ∨ 1 = 1 + * + * Properties: + * - Vacuous falsity + * - Identity singleton + * - Commutative + * - Associative + * - Distributive over AND + * - ⊥ as identity + * - Dominated by ⊤ + * - Idempotent + * - Connecting complement results in tautology + * - More strict term is absorbed (A ∨ (A ∧ B) simplifies to A) + * + * Commonly written "∨" ("⋁" if n-ary), "|", or "+" + * + * @param xs `NULL`-terminated list of sentences that should be + * joined by the connective OR; this can be any number + * of arguments, even none; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_OR + * @seealso libnormalform_or_checked + * @seealso libnormalform_orl_checked + * @seealso libnormalform_vor_checked + * @seealso libnormalform_orl + * @seealso libnormalform_vor + * @seealso libnormalform_or2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_or)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * XOR: Exclusive disjunction + * + * Also known as EOR, EXOR, NEQ, NIFF, Parity (especially when n-ary), + * Exclusive alternation, Exclusive or, Logical non-equivalence, + * Logical non-equivalence, Logical inequality, Not if and only if, + * or Unless and only unless + * + * An odd number of conditions must be met + * + * 0 ⊕ 0 = 0 + * 0 ⊕ 1 = 1 + * 1 ⊕ 0 = 1 + * 1 ⊕ 1 = 0 + * + * Properties: + * - Vacuous falsity + * - Identity singleton + * - Commutative + * - Associative + * - ⊥ as identity + * - Complemented by ⊤ + * - Annihiliation by reflextion + * - Connecting complement results in tautology + * - A ⊕ B is reduced to (A ∨ B) ∧ (¬A ∨ ¬B) or + * (A ∧ ¬B) ∨ (¬A ∧ B) in negation normal form + * + * Commonly written "⊕" ("⨁" if n-ary), "⊻", "↮", "⇎", "≢", or "^" + * + * Note that the name Exclusive disjunction is misleading + * when there are more than two terms, as the statement + * will not check that exactly one term is true, but rather + * calculate the parity of the terms. + * + * @param xs `NULL`-terminated list of sentences that should be + * joined by the connective XOR; this can be any number + * of arguments, even none; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_XOR + * @seealso libnormalform_xor_checked + * @seealso libnormalform_xorl_checked + * @seealso libnormalform_vxor_checked + * @seealso libnormalform_xorl + * @seealso libnormalform_vxor + * @seealso libnormalform_xor2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_xor)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * IF: Converse implication + * + * Also known as Converse conditional + * + * Creates a chain where any condition must be at least + * as satisfied as the condition left to it (xs[0] ≤ xs[1]) + * (Not xs[1] without xs[0]); it is false only when only + * the left-most term is false + * + * 0 ← 0 = 1 + * 0 ← 1 = 0 + * 1 ← 0 = 1 + * 1 ← 1 = 1 + * + * Properties: + * - Identity singleton + * - Non-commutative + * - Left-associative: A ← B ← C = (A ← B) ← C ≠ A ← (B ← C) + * - Complemented by left ⊥ + * - Dominated by left ⊤ + * - Right falsity results in tautology + * - ⊤ as right identity + * - Contrapositivity: A ← B = ¬B ← ¬A + * - Transitive: (A ← B) ∧ (B ← C) ⊨ A ← C + * - Reflexive: A ← A = ⊤ + * - Complete: (A ← B) ∨ (B ← A) = ⊤ + * - Excluded middle: (A ← B) ∨ (¬A ← B) = ⊤ + * - Import-export: (A ← B) ← C = A ← (B ∧ C) + * - Commutativity of antecedents: (A ← B) ← C = (A ← C) ← B + * - Vacuous conditional: ¬A ⊨ B ← A + * - Antecedent strengthening: A ← B ⊨ A ← (B ∧ C) + * - Right-distributive: (A ← B) ← C = (A ← C) ← (B ← C) + * - Distributive over left AND + * - Distributive over left OR + * - Distributing over right AND changes AND to OR + * - Distributing over right OR changes OR to AND + * - A ← B is reduced to A ∨ ¬B in negation normal form + * + * Commonly written "←", "⇐", "<-", "<=", "≤", "⩽", or "⊂" + * + * @param xs `NULL`-terminated list of sentences that should be + * joined by the connective IF; this can be any positive + * number of arguments; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * @throws EDOM `xs` contains no term (but only `NULL`) + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_IF + * @seealso libnormalform_if_checked + * @seealso libnormalform_ifl_checked + * @seealso libnormalform_vif_checked + * @seealso libnormalform_ifl + * @seealso libnormalform_vif + * @seealso libnormalform_if2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_if)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * IMPLY: Material implication + * + * Also known as IMPLIES, IF..THEN, NOT..WITHOUT or material conditional + * + * Creates a chain where any condition must be at most + * as satisfied as the condition left to it (xs[0] ≥ xs[1]) + * (Not xs[0] without xs[1]); it is false only when only + * the right-most term is false + * + * 0 → 0 = 1 + * 0 → 1 = 1 + * 1 → 0 = 0 + * 1 → 1 = 1 + * + * Properties: + * - Vacuous truth + * - Identity singleton + * - Non-commutative + * - Right-associative: A → B → C = A → (B → C) ≠ (A → B) → C + * - Complemented by right ⊥ + * - Dominated by right ⊤ + * - Left falsity results in tautology + * - ⊤ as left identity + * - Contrapositivity: A → B = ¬B → ¬A + * - Transitive: (A → B) ∧ (B → C) ⊨ A → C + * - Reflexive: A → A = ⊤ + * - Complete: (A → B) ∨ (B → A) = ⊤ + * - Excluded middle: (A → B) ∨ (A → ¬B) = ⊤ + * - Import-export: A → (B → C) = (A ∧ B) → C + * - Commutativity of antecedents: A → (B → C) = B → (A → C) + * - Vacuous conditional: ¬A ⊨ A → B + * - Antecedent strengthening: A → B ⊨ (A ∧ C) → B + * - Left-distributive: A → (B → C) = (A → B) → (A → C) + * - Distributive over right AND + * - Distributive over right OR + * - Distributing over left AND changes AND to OR + * - Distributing over left OR changes OR to AND + * - A → B is reduced to ¬A ∨ B in negation normal form + * + * Commonly written "→", "⇒", "->", "=>", ">=", "≥", "⩾", or "⊃" + * + * @param xs `NULL`-terminated list of sentences that should + * be joined by the connective IMPLY; this can be any + * number of arguments; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_IMPLY + * @seealso libnormalform_imply_checked + * @seealso libnormalform_implyl_checked + * @seealso libnormalform_vimply_checked + * @seealso libnormalform_implyl + * @seealso libnormalform_vimply + * @seealso libnormalform_imply2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_imply)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * NAND: Alternative denial + * + * Also known as Non-conjunction, Negated conjunction, + * Mutual exclusion, or Sheffer stroke + * + * Creates a left-associated NAND-chain; in NAND, the + * two conditions must not be met at the same time + * + * 0 ⊼ 0 = 1 + * 0 ⊼ 1 = 1 + * 1 ⊼ 0 = 1 + * 1 ⊼ 1 = 0 + * + * There is no good interpretation for a NAND-chain + * + * Commonly written "⊼", "↑", or as AND with the expression over-struck + * + * Properties: + * - Identity singleton + * - Commutative (however A ⊼ B ⊼ C ≠ A ⊼ C ⊼ B due to non-associativity) + * - Left-associative: A ⊼ B ⊼ C = (A ⊼ B) ⊼ C ≠ A ⊼ (B ⊼ C) + * - Antireflexive: A ⊼ A = ⊥ + * - Annihilated by ⊥: A ⊼ ⊥ = ⊤ + * - Complemented by ⊤ + * - Distributative over AND + * - A ⊼ B is reduced to ¬A ∨ ¬B in negation normal form + * + * @param xs `NULL`-terminated list of sentences that should be + * joined by the connective NAND; this can be any positive + * number of arguments; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * @throws EDOM `xs` contains no term (but only `NULL`) + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_NAND + * @seealso libnormalform_nand_checked + * @seealso libnormalform_nandl_checked + * @seealso libnormalform_vnand_checked + * @seealso libnormalform_nandl + * @seealso libnormalform_vnand + * @seealso libnormalform_nand2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_nand)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * NOR: Joint denial + * + * Also known as Non-disjunction, Negated disjunction, Peirce arrow, + * Quine dagger, or Webb operator + * + * Creates a left-associated NOR-chain; in NOR, the + * two conditions must be unmet at same time + * + * 0 ⊽ 0 = 1 + * 0 ⊽ 1 = 0 + * 1 ⊽ 0 = 0 + * 1 ⊽ 1 = 0 + * + * There is no good interpretation for a NOR-chain + * + * Commonly written "⊽", "↓", or as OR with the expression over-struck + * + * Properties: + * - Identity singleton + * - Commutative (however A ⊽ B ⊽ C ≠ A ⊽ C ⊽ B due to non-associativity) + * - Left-associative: A ⊽ B ⊽ C = (A ⊽ B) ⊽ C ≠ A ⊽ (B ⊽ C) + * - Anti-idempotent: A ⊽ A = ¬A + * - Annihilated by ⊤: A ⊽ ⊤ = ⊥ + * - Complemented by ⊤ + * - Distributing over AND changes AND to OR + * - Distributing over OR changes OR to AND + * - A ⊽ B is reduced to ¬A ∧ ¬B in negation normal form + * + * @param xs `NULL`-terminated list of sentences that should be + * joined by the connective NOR; this can be any positive + * number of arguments; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * @throws EDOM `xs` contains no term (but only `NULL`) + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_NOR + * @seealso libnormalform_nor_checked + * @seealso libnormalform_norl_checked + * @seealso libnormalform_vnor_checked + * @seealso libnormalform_norl + * @seealso libnormalform_vnor + * @seealso libnormalform_nor2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_nor)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * XNOR: Logical bicondition + * + * Also known as ENOR, EXNOR, NXOR, XAND, EQ, IFF, Exclusive NOR, + * Material biconditional, Logical equivalence, Biimplication, + * Bientailment, If and only if, Negated XOR, or Exclusive non-disjunction + * + * Creates a left-associated XNOR-chain; in XNOR, the + * two conditions must equally true + * + * 0 ⊙ 0 = 1 + * 0 ⊙ 1 = 0 + * 1 ⊙ 0 = 0 + * 1 ⊙ 1 = 1 + * + * The interpretation of a XNOR-chain depends on it's length, + * if it's length is even, is equivalent to XOR, otherwise, + * it's its complement + * + * Commonly written "⊙" ("⨀" if n-ary), "↔", "⇔", "≡", "==", or + * as XOR with the expression over-struck + * + * Properties: + * - Vacuous truth + * - Identity singleton + * - Commutative + * - Associative + * - ⊤ as identity + * - Complemented by ⊥ + * - Reflexive: A ⊙ A = ⊤ + * - Annihilated by ⊤: A ⊽ ⊤ = ⊥ + * - Connecting complement results in contradiction + * - A ⊙ B is reduced to (A ∨ ¬B) ∧ (¬A ∨ B) or + * (A ∧ B) ∨ (¬A ∧ ¬B) in negation normal form + * + * @param xs `NULL`-terminated list of sentences that should + * be joined by the connective XNOR; this can be any + * number of arguments; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_NXOR + * @seealso libnormalform_nxor_checked + * @seealso libnormalform_nxorl_checked + * @seealso libnormalform_vxnor_checked + * @seealso libnormalform_xnorl + * @seealso libnormalform_vxnor + * @seealso libnormalform_xnor2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_xnor)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * NIF: Converse nonimplication + * + * Also known as NOT..BUT, Converse abjunction + * + * Creates a chain where any condition must be less + * satisfied than the condition left to it (xs[0] > xs[1]) + * + * 0 ↚ 0 = 0 + * 0 ↚ 1 = 1 + * 1 ↚ 0 = 0 + * 1 ↚ 1 = 0 + * + * Properties: + * - Vacuous falsity + * - Identity singleton + * - Non-commutative + * - Left-associative: A ↚ B ↚ C = (A ↚ B) ↚ C ≠ A ↚ (B ↚ C) + * - Complemented by right ⊤ + * - Dominated by right ⊥ + * - Left truth results in contradiction + * - ⊥ as left identity + * - Contrapositivity: A ↚ B = ¬B ↚ ¬A + * - Antireflexive: A ↚ A = ⊥ + * - Left-distributive: A ↚ (B ↚ C) = (A ↚ B) ↚ (A ↚ C) + * - Distributive over right AND + * - Distributive over right OR + * - Distributing over left AND changes AND to OR + * - Distributing over left OR changes OR to AND + * - A ↚ B is reduced to ¬A ∧ B in negation normal form + * + * Commonly written "↚", "⇍", "!<-", "<-~", "</-", "!<=", "<=~", "</=", "⊄", "⭉" (or "←̃"), or ">" + * + * @param xs `NULL`-terminated list of sentences that should be + * joined by the connective NIF; this can be any number + * of arguments, even none; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_NIF + * @seealso libnormalform_nif_checked + * @seealso libnormalform_nifl_checked + * @seealso libnormalform_vnif_checked + * @seealso libnormalform_nifl + * @seealso libnormalform_vnif + * @seealso libnormalform_nif2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_nif)(LIBNORMALFORM_SENTENCE **xs); + + +/** + * NIMPLY: Material nonimplication + * + * Also known as NIMPLIES, BUT NOT or Material abjunction + * + * Creates a chain where any condition must be more + * satisfied than the condition left to it (xs[0] < xs[1]) + * + * 0 ↛ 0 = 0 + * 0 ↛ 1 = 0 + * 1 ↛ 0 = 1 + * 1 ↛ 1 = 0 + * + * Properties: + * - Identity singleton + * - Non-commutative + * - Right-associative: A ↛ B ↛ C = A ↛ (B ↛ C) ≠ (A ↛ B) → C + * - Complemented by left ⊤ + * - Dominated by left ⊥ + * - Right truth results in contradiction + * - ⊥ as right identity + * - Contrapositivity: A ↛ B = ¬B ↛ ¬A + * - Antireflexive: A ↛ A = ⊥ + * - Right-distributive: (A ↛ B) ↛ C = (A ↛ C) ↛ (B → C) + * - Distributive over left AND + * - Distributive over left OR + * - Distributing over right AND changes AND to OR + * - Distributing over right OR changes OR to AND + * - A ↛ B is reduced to A ∧ ¬B in negation normal form + * + * Commonly written "↛", "⇏", "!->", "->~", "-/>", "!=>", "=>~", "=/>", "⊅", "⥲" (or "→̃"), or "<" + * + * @param xs `NULL`-terminated list of sentences that should be + * joined by the connective NIMPLY; this can be any positive + * number of arguments; ownership of object in the array + * (but not the array itself) is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * @throws EDOM `xs` contains no term (but only `NULL`) + * + * Ownership is always transfered, even on failure + * + * @seealso LIBNORMALFORM_NIMPLY + * @seealso libnormalform_nimply_checked + * @seealso libnormalform_nimplyl_checked + * @seealso libnormalform_vnimply_checked + * @seealso libnormalform_nimplyl + * @seealso libnormalform_vnimply + * @seealso libnormalform_nimply2 + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +LIBNORMALFORM_SENTENCE *(libnormalform_nimply)(LIBNORMALFORM_SENTENCE **xs); + + + + + +/** + * THERE EXISTS: Existential quantification (unmapped) + * + * The predicate must be met for at least one element; + * if no element exists, the sentence is false + * + * Commonly written "∃" ("∃x∈d.k", "∃x∈d k(x)", or "∃ x∈d : k(x)") + * + * The predicate is tested on `.key` in each element + * in the domain, and `.value` is unused + * + * @param d The domain of interest; ownership is retained by the caller + * @param k The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `k` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `k` to + * be `NULL`) + * + * @seealso libnormalform_any + * @seealso libnormalform_existentially + * @seealso libnormalform_nexists + * @seealso libnormalform_unique + * @seealso libnormalform_nonempty + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_exists)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k) +{ return libnormalform_any(d, k, libnormalform_true()); } + + +/** + * THERE EXISTS NO: Negated existential quantification (unmapped) + * + * The predicate must be unmet for every element; + * if no element exists, the sentence is true + * + * Commonly written "∄" ("∄x∈d.k", "∄x∈d k(x)", or "∄ x∈d : k(x)"), + * "~∃", "¬∃", or as THERE EXISTS with overline + * + * The predicate is tested on `.key` in each element + * in the domain, and `.value` is unused + * + * @param d The domain of interest; ownership is retained by the caller + * @param k The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `k` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `k` to + * be `NULL`) + * + * @seealso libnormalform_all + * @seealso libnormalform_exists + * @seealso libnormalform_empty + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nexists)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k) +{ return libnormalform_all(d, k, libnormalform_false()); } + + +/** + * THERE EXISTS ONE: Unique existential quantification (unmapped) + * + * The predicate must be met for exactly one element; + * if no element exists, the sentence is false + * + * Commonly written "∃!" ("∃!x∈d.k", "∃!x∈d k(x)", or "∃! x∈d : k(x)") + * + * The predicate is tested on `.key` in each element + * in the domain, and `.value` is unused + * + * @param d The domain of interest; ownership is retained by the caller + * @param k The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `k` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `k` to + * be `NULL`) + * + * @seealso libnormalform_one + * @seealso libnormalform_uniquely + * @seealso libnormalform_exists + * @seealso libnormalform_singleton + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_unique)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k) +{ return libnormalform_one(d, k, libnormalform_true()); } + + + + + +/** + * SOMEWHERE: Existential quantification (premapped) + * + * The predicate must be met for at least one element; + * if no element exists, the sentence is false + * + * Commonly written "∃" ("∃x∈d.v", "∃x∈d v(x)", or "v(x) ∃ x∈d") + * + * The predicate is tested on `.value` in each element + * in the domain, and `.key` is unused + * + * @param d The domain of interest; ownership is retained by the caller + * @param v The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `v` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `v` to + * be `NULL`) + * + * @seealso libnormalform_any + * @seealso libnormalform_exists + * @seealso libnormalform_universally + * @seealso libnormalform_uniquely + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_existentially)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v) +{ return libnormalform_any(d, libnormalform_true(), v); } + + +/** + * EVERYWHERE: Universal quantification (premapped) + * + * The predicate must be unmet for every element; + * if no element exists, the sentence is true + * + * Commonly written "∀" ("∀x∈d.v", "∀x∈d v(x)", or "v(x) ∀ x∈d") + * + * The predicate is tested on `.value` in each element + * in the domain, and `.key` is unused + * + * @param d The domain of interest; ownership is retained by the caller + * @param v The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `v` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `v` to + * be `NULL`) + * + * @seealso libnormalform_all + * @seealso libnormalform_existentially + * @seealso libnormalform_uniquely + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_universally)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v) +{ return libnormalform_all(d, libnormalform_true(), v); } + + +/** + * ONEWHERE: Unique existential quantification (premapped) + * + * The predicate must be met for exactly one element; + * if no element exists, the sentence is false + * + * Commonly written "∃!" ("∃!x∈d.v", "∃!x∈d v(x)", or "v(x) ∃! x∈d") + * + * The predicate is tested on `.value` in each element + * in the domain, and `.key` is unused + * + * @param d The domain of interest; ownership is retained by the caller + * @param v The predicate; ownership is transfered to this function + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * Ownership is always transfered, even on failure + * + * If `v` is `NULL`, this function will return `NULL` + * (indicating failure) without modified `errno` (expecting + * it to be set by a function that failed, causing `v` to + * be `NULL`) + * + * @seealso libnormalform_one + * @seealso libnormalform_unique + * @seealso libnormalform_existentially + * @seealso libnormalform_universially + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_uniquely)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v) +{ return libnormalform_one(d, libnormalform_true(), v); } + + + + + +/** + * Create a sentence that checks whether a set is empty + * + * The sentence technically classifies as a qualification + * + * Commonly written "X=∅" or "|X|=0" + * + * @param d The set; ownership is retained by the caller + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * @seealso libnormalform_nonempty + * @seealso libnormalform_singleton + * @seealso libnormalform_nexists + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_empty)(struct libnormalform_map *d) +{ return libnormalform_all(d, libnormalform_true(), libnormalform_false()); } + + +/** + * Create a sentence that checks whether a set is non-empty + * + * The sentence technically classifies as a qualification + * + * Commonly written "X≠∅", "X⊃∅", "X⊋∅" "|X|≠0", or "|X|>0" + * + * @param d The set; ownership is retained by the caller + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * @seealso libnormalform_empty + * @seealso libnormalform_singleton + * @seealso libnormalform_exists + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nonempty)(struct libnormalform_map *d) +{ return libnormalform_any(d, libnormalform_true(), libnormalform_true()); } + + +/** + * Create a sentence that checks whether a set is a singleton + * (contains exactly one element) + * + * The sentence technically classifies as a qualification + * + * Commonly written "|X|=1", "∃! x : X={x}", "X={x} ∃! x", or just "X={x}" + * + * @param d The set; ownership is retained by the caller + * @return The constructed sentence, `NULL` on failure + * + * @throws ENOMEM Insufficient memory available to create the sentence + * + * @seealso libnormalform_empty + * @seealso libnormalform_nonempty + * @seealso libnormalform_unique + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_singleton)(struct libnormalform_map *d) +{ return libnormalform_one(d, libnormalform_true(), libnormalform_true()); } + + + + + +/** + * Variant of `libnormalform_and` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_and` + * @return See `libnormalform_and` + * @throws See `libnormalform_and` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_and_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(and) } + + +/** + * Variant of `libnormalform_or` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_or` + * @return See `libnormalform_or` + * @throws See `libnormalform_or` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_or_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(or) } + + +/** + * Variant of `libnormalform_xor` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_xor` + * @return See `libnormalform_xor` + * @throws See `libnormalform_xor` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_xor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(xor) } + + +/** + * Variant of `libnormalform_if` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_if` + * @return See `libnormalform_if` + * @throws See `libnormalform_if` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_if_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(if) } + + +/** + * Variant of `libnormalform_imply` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_imply` + * @return See `libnormalform_imply` + * @throws See `libnormalform_imply` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_imply_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(imply) } + + +/** + * Variant of `libnormalform_nand` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_nand` + * @return See `libnormalform_nand` + * @throws See `libnormalform_nand` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nand_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(nand) } + + +/** + * Variant of `libnormalform_nor` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_nor` + * @return See `libnormalform_nor` + * @throws See `libnormalform_nor` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(nor) } + + +/** + * Variant of `libnormalform_xnor` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_xnor` + * @return See `libnormalform_xnor` + * @throws See `libnormalform_xnor` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_xnor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(xnor) } + + +/** + * Variant of `libnormalform_nif` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_nif` + * @return See `libnormalform_nif` + * @throws See `libnormalform_nif` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nif_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(nif) } + + +/** + * Variant of `libnormalform_nimply` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param xs See `libnormalform_nimply` + * @return See `libnormalform_nimply` + * @throws See `libnormalform_nimply` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nimply_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs) +{ LIBNORMALFORM_CHECKED__(nimply) } + + + + + +/** + * Variant of `libnormalform_andl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_andl` + * @throws See `libnormalform_andl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vand)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(and) } + + +/** + * Variant of `libnormalform_orl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_orl` + * @throws See `libnormalform_orl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vor)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(or) } + + +/** + * Variant of `libnormalform_xorl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_xorl` + * @throws See `libnormalform_xorl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vxor)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(xor) } + + +/** + * Variant of `libnormalform_ifl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_ifl` + * @throws See `libnormalform_ifl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vif)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(if) } + + +/** + * Variant of `libnormalform_implyl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_implyl` + * @throws See `libnormalform_implyl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vimply)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(imply) } + + +/** + * Variant of `libnormalform_nandl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nandl` + * @throws See `libnormalform_nandl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vnand)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(nand) } + + +/** + * Variant of `libnormalform_norl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_norl` + * @throws See `libnormalform_norl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vnor)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(nor) } + + +/** + * Variant of `libnormalform_xnorl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_xnorl` + * @throws See `libnormalform_xnorl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vxnor)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(xnor) } + + +/** + * Variant of `libnormalform_nifl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nifl` + * @throws See `libnormalform_nifl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vnif)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(nif) } + + +/** + * Variant of `libnormalform_nimplyl` that uses `va_list` + * instead of variadic arguments + * + * @param a, args `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nimplyl` + * @throws See `libnormalform_nimplyl` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vnimply)(LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST__(nimply) } + + + + + +/** + * Variant of `libnormalform_and` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_and` + * @throws See `libnormalform_and` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_andl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(and) } + + +/** + * Variant of `libnormalform_or` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_or` + * @throws See `libnormalform_or` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_orl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(or) } + + +/** + * Variant of `libnormalform_xor` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_xor` + * @throws See `libnormalform_xor` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_xorl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(xor) } + + +/** + * Variant of `libnormalform_if` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_if` + * @throws See `libnormalform_if` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_ifl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(if) } + + +/** + * Variant of `libnormalform_imply` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_imply` + * @throws See `libnormalform_imply` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_implyl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(imply) } + + +/** + * Variant of `libnormalform_nand` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nand` + * @throws See `libnormalform_nand` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nandl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(nand) } + + +/** + * Variant of `libnormalform_nor` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nor` + * @throws See `libnormalform_nor` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_norl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(nor) } + + +/** + * Variant of `libnormalform_xnor` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_xnor` + * @throws See `libnormalform_xnor` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_xnorl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(xnor) } + + +/** + * Variant of `libnormalform_nif` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nif` + * @throws See `libnormalform_nif` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nifl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(nif) } + + +/** + * Variant of `libnormalform_nimply` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nimply` + * @throws See `libnormalform_nimply` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nimplyl)(LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS__(nimply) } + + + + + +/** + * Variant of `libnormalform_vand` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vand` + * @return See `libnormalform_vand` + * @throws See `libnormalform_vand` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vand_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(and) } + + +/** + * Variant of `libnormalform_vor` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vor` + * @return See `libnormalform_vor` + * @throws See `libnormalform_vor` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(or) } + + +/** + * Variant of `libnormalform_vxor` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vxor` + * @return See `libnormalform_vxor` + * @throws See `libnormalform_vxor` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vxor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(xor) } + + +/** + * Variant of `libnormalform_vif` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vif` + * @return See `libnormalform_vif` + * @throws See `libnormalform_vif` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vif_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(if) } + + +/** + * Variant of `libnormalform_vimply` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vimply` + * @return See `libnormalform_vimply` + * @throws See `libnormalform_vimply` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vimply_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(imply) } + + +/** + * Variant of `libnormalform_vnand` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vnand` + * @return See `libnormalform_vnand` + * @throws See `libnormalform_vnand` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vnand_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(nand) } + + +/** + * Variant of `libnormalform_vnor` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vnor` + * @return See `libnormalform_vnor` + * @throws See `libnormalform_vnor` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vnor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(nor) } + + +/** + * Variant of `libnormalform_vxnor` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vxnor` + * @return See `libnormalform_vxnor` + * @throws See `libnormalform_vxnor` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vxnor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(xnor) } + + +/** + * Variant of `libnormalform_vnif` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vnif` + * @return See `libnormalform_vnif` + * @throws See `libnormalform_vnif` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vnif_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(nif) } + + +/** + * Variant of `libnormalform_vnimply` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, args See `libnormalform_vnimply` + * @return See `libnormalform_vnimply` + * @throws See `libnormalform_vnimply` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_vnimply_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args) +{ LIBNORMALFORM_VALIST_CHECKED__(nimply) } + + + + + +/** + * Variant of `libnormalform_andl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_andl` + * @return See `libnormalform_andl` + * @throws See `libnormalform_andl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_andl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(and) } + + +/** + * Variant of `libnormalform_orl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_orl` + * @return See `libnormalform_orl` + * @throws See `libnormalform_orl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_orl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(or) } + + +/** + * Variant of `libnormalform_xorl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_xorl` + * @return See `libnormalform_xorl` + * @throws See `libnormalform_xorl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_xorl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(xor) } + + +/** + * Variant of `libnormalform_ifl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_ifl` + * @return See `libnormalform_ifl` + * @throws See `libnormalform_ifl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_ifl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(if) } + + +/** + * Variant of `libnormalform_implyl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_implyl` + * @return See `libnormalform_implyl` + * @throws See `libnormalform_implyl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_implyl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(imply) } + + +/** + * Variant of `libnormalform_nandl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_nandl` + * @return See `libnormalform_nandl` + * @throws See `libnormalform_nandl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nandl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nand) } + + +/** + * Variant of `libnormalform_norl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_norl` + * @return See `libnormalform_norl` + * @throws See `libnormalform_norl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_norl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nor) } + + +/** + * Variant of `libnormalform_xnorl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_xnorl` + * @return See `libnormalform_xnorl` + * @throws See `libnormalform_xnorl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_xnorl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(xnor) } + + +/** + * Variant of `libnormalform_nifl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_nifl` + * @return See `libnormalform_nifl` + * @throws See `libnormalform_nifl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nifl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nif) } + + +/** + * Variant of `libnormalform_nimplyl` that checks + * for unexpected `NULL` input + * + * @param n The number of expected non-`NULL` terms + * @param a, ... See `libnormalform_nimplyl` + * @return See `libnormalform_nimplyl` + * @throws See `libnormalform_nimplyl` + * + * If the function finds any unexpected `NULL` terms, + * it will call `libnormalform_free` on all non-`NULL` terms + * and return `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nimplyl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...) +{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nimply) } + + + + + +/** + * Variant of `libnormalform_and` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_and` + * @throws See `libnormalform_and` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +LIBNORMALFORM_SENTENCE *(libnormalform_and2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r); + + +/** + * Variant of `libnormalform_or` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_or` + * @throws See `libnormalform_or` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +LIBNORMALFORM_SENTENCE *(libnormalform_or2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r); + + +/** + * Variant of `libnormalform_xor` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_xor` + * @throws See `libnormalform_xor` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +LIBNORMALFORM_SENTENCE *(libnormalform_xor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r); + + +/** + * Variant of `libnormalform_if` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_if` + * @throws See `libnormalform_if` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_if2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) +{ LIBNORMALFORM_TWO__(if) } + + +/** + * Variant of `libnormalform_imply` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_imply` + * @throws See `libnormalform_imply` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_imply2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) +{ LIBNORMALFORM_TWO__(imply) } + + +/** + * Variant of `libnormalform_nand` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_nand` + * @throws See `libnormalform_nand` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nand2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) +{ LIBNORMALFORM_TWO__(nand) } + + +/** + * Variant of `libnormalform_nor` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_nor` + * @throws See `libnormalform_nor` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) +{ LIBNORMALFORM_TWO__(nor) } + + +/** + * Variant of `libnormalform_xnor` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_xnor` + * @throws See `libnormalform_xnor` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_xnor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) +{ LIBNORMALFORM_TWO__(xnor) } + + +/** + * Variant of `libnormalform_nif` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_nif` + * @throws See `libnormalform_nif` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nif2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) +{ LIBNORMALFORM_TWO__(nif) } + + +/** + * Variant of `libnormalform_nimply` that takes exactly two terms + * + * @param l The left-hand term + * @param r The right-hand term + * @return See `libnormalform_nimply` + * @throws See `libnormalform_nimply` + * + * If `l` or `r` is `NULL`, the function will call + * `libnormalform_free` on both arguments and return + * `NULL` (indicating failure) without setting + * `errno` (expected to already be set in indicate the + * error that caused one of the terms to be `NULL`) + */ +LIBNORMALFORM_USE_RESULT__ +inline LIBNORMALFORM_SENTENCE * +(libnormalform_nimply2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) +{ LIBNORMALFORM_TWO__(nimply) } + + + + + +/* These are macro versions of function with the same name */ + +/** + * Variant of `libnormalform_and` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_and` + * @throws See `libnormalform_and` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_andl(...) (libnormalform_and((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_or` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_or` + * @throws See `libnormalform_or` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_orl(...) (libnormalform_or((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_xor` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_xor` + * @throws See `libnormalform_xor` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_xorl(...) (libnormalform_xor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_if` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_if` + * @throws See `libnormalform_if` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_ifl(...) (libnormalform_if((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_imply` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_imply` + * @throws See `libnormalform_imply` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_implyl(...) (libnormalform_imply((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_nand` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nand` + * @throws See `libnormalform_nand` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_nandl(...) (libnormalform_nand((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_nor` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nor` + * @throws See `libnormalform_nor` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_norl(...) (libnormalform_nor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_xnor` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_xnor` + * @throws See `libnormalform_xnor` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_xnorl(...) (libnormalform_xnor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_nif` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nif` + * @throws See `libnormalform_nif` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_nifl(...) (libnormalform_nif((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + +/** + * Variant of `libnormalform_nimply` that uses variadic arguments + * + * @param a, ... `NULL`-terminated list of terms; the function + * will take ownership of each input reference, + * so the caller shall not attempt to deallocate + * or use them again. + * @return See `libnormalform_nimply` + * @throws See `libnormalform_nimply` + * + * Be careful not in inputing any `NULL` apart from + * the list terminator as the function will not be + * able to see them. + */ +#define libnormalform_nimplyl(...) (libnormalform_nimply((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__})) + + + + + +/** + * Macro variant of `libnormalform_andl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_andl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_AND(...) LIBNORMALFORM_MACRO__(and, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_orl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_orl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_OR(...) LIBNORMALFORM_MACRO__(or, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_xorl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_xorl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_XOR(...) LIBNORMALFORM_MACRO__(xor, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_ifl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_ifl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_IF(...) LIBNORMALFORM_MACRO__(if, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_implyl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_implyl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_IMPLY(...) LIBNORMALFORM_MACRO__(imply, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_nandl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_nandl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_NAND(...) LIBNORMALFORM_MACRO__(nand, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_norl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_norl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_NOR(...) LIBNORMALFORM_MACRO__(nor, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_xnorl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_xnorl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_XNOR(...) LIBNORMALFORM_MACRO__(xnor, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_nifl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_nifl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_NIF(...) LIBNORMALFORM_MACRO__(nif, __VA_ARGS__) + + +/** + * Macro variant of `libnormalform_nimplyl_checked`, that + * will add the `NULL` to the end of the list and, before + * the list, the number of terms in the list + * + * @param ... List of terms, _without_ `NULL`-terinator + * @return See `libnormalform_nimplyl_checked` + * + * Either any argument is `NULL`, `libnormalform_free` on + * will be called for all non-`NULL` terms, the `NULL` + * with be return (indicating failure) without `errno` + * being modified (it is expected to already be set in + * indicate the error that caused one of the terms to be + * `NULL`) + */ +#define LIBNORMALFORM_NIMPLY(...) LIBNORMALFORM_MACRO__(nimply, __VA_ARGS__) + + + + + +#undef LIBNORMALFORM_CHECKED__ +#undef LIBNORMALFORM_VALIST__ +#undef LIBNORMALFORM_ELLIPSIS__ +#undef LIBNORMALFORM_VALIST_CHECKED__ +#undef LIBNORMALFORM_ELLIPSIS_CHECKED__ +#undef LIBNORMALFORM_TWO__ + +#undef LIBNORMALFORM_USE_RESULT__ +#undef LIBNORMALFORM_FREE_WITH__ +#undef LIBNORMALFORM_USE_FREE__ +#undef LIBNORMALFORM_NONNULL_INPUT__ +#undef LIBNORMALFORM_ONE_NONNULL_INPUT__ +#undef LIBNORMALFORM_NULL_LAST__ + + +#if defined(__GNUC__) +# pragma GCC diagnostic pop +#endif + +#endif |