/* See LICENSE file for copyright and license details. */ #ifndef LIBNORMALFORM_H #define LIBNORMALFORM_H #include #include #include #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 "↚", "⇍", "!<-", "<-~", "" * * @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