path: root/libnormalform.h

/* See LICENSE file for copyright and license details. */
#ifndef LIBNORMALFORM_H
#define LIBNORMALFORM_H

#include <stdarg.h>
#include <stddef.h>
#include <stdint.h>


#if defined(__GNUC__)
# pragma GCC diagnostic push
# pragma GCC diagnostic ignored "-Winline"
#endif


/* For internal use { */

#if defined(__GNUC__)
# define LIBNORMALFORM_USE_RESULT__ __attribute__((__warn_unused_result__))
# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) __attribute__((__malloc__(DESTRUCTOR)))
# define LIBNORMALFORM_USE_FREE__ __attribute__((__malloc__))
# define LIBNORMALFORM_NONNULL_INPUT__ __attribute__((__nonnull__))
# define LIBNORMALFORM_ONE_NONNULL_INPUT__(INDEX) __attribute__((__nonnull__(INDEX)))
# if defined(LIBNORMALFORM_ALLOW_BAD_WARNINGS)
#  define LIBNORMALFORM_NULL_LAST__ __attribute__((__sentinel__))
# else
#  define LIBNORMALFORM_NULL_LAST__
# endif
/*
 * Unfortunately __attribute__((__sentinel__)) requires (in contrary to the
 * documentation) the `NULL` to be inside `...`, and not at the argument before
 * the `...`, so a "-Wformat=" warning will be generated if and empty list is
 * used when constructing a sentence. Therefore, by default this attribute is
 * not used, as the user may have configured the compiler to fail if the warning
 * is generated.
 */
#else
# define LIBNORMALFORM_USE_RESULT__
# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR)
# define LIBNORMALFORM_USE_FREE__
# define LIBNORMALFORM_NONNULL_INPUT__
# define LIBNORMALFORM_ONE_NONNULL_INPUT__(INDEX)
# define LIBNORMALFORM_NULL_LAST__
#endif


#define LIBNORMALFORM_CHECKED__(CONNECTIVE)\
	size_t i__ = 0;\
	while (xs[i__])\
		i__ += 1;\
	if (i__ < n) {\
		while (n--)\
			libnormalform_free(xs[n]);\
		return NULL;\
	}\
	return libnormalform_##CONNECTIVE(xs);

#define LIBNORMALFORM_VALIST__(CONNECTIVE)\
	size_t n__ = 0, i__ = 0;\
	va_list args2__;\
	va_copy(args2__, args);\
	if (a) {\
		do {\
			n__ += 1;\
		} while (va_arg(args2__, LIBNORMALFORM_SENTENCE *));\
	}\
	va_end(args2__);\
	{\
		LIBNORMALFORM_SENTENCE *xs[n__ + 1U];\
		if (n__) {\
			xs[i__++] = a;\
			while (--n__)\
				xs[i__++] = va_arg(args, LIBNORMALFORM_SENTENCE *);\
		}\
		xs[i__] = NULL;\
		return libnormalform_##CONNECTIVE(xs);\
	}

#define LIBNORMALFORM_ELLIPSIS__(CONNECTIVE)\
	LIBNORMALFORM_SENTENCE *ret__;\
	va_list args__;\
	va_start(args__, a);\
	ret__ = libnormalform_v##CONNECTIVE(a, args__);\
	va_end(args__);\
	return ret__;

#define LIBNORMALFORM_VALIST_CHECKED__(CONNECTIVE)\
	size_t n__ = 0, i__ = 0;\
	va_list args2__;\
	va_copy(args2__, args);\
	if (a) {\
		do {\
			n__ += 1;\
		} while (va_arg(args2__, LIBNORMALFORM_SENTENCE *));\
	}\
	va_end(args2__);\
	if (n__ < n) {\
		if (n) {\
			libnormalform_free(a);\
			while (--n)\
				libnormalform_free(va_arg(args2__, LIBNORMALFORM_SENTENCE *));\
		}\
		return NULL;\
	}\
	{\
		LIBNORMALFORM_SENTENCE *xs__[n__ + 1U];\
		if (n__) {\
			xs__[i__++] = a;\
			while (--n__)\
				xs__[i__++] = va_arg(args, LIBNORMALFORM_SENTENCE *);\
		}\
		xs__[i__] = NULL;\
		return libnormalform_##CONNECTIVE(xs__);\
	}

#define LIBNORMALFORM_ELLIPSIS_CHECKED__(CONNECTIVE)\
	LIBNORMALFORM_SENTENCE *ret__;\
	va_list args__;\
	va_start(args__, a);\
	ret__ = libnormalform_v##CONNECTIVE##_checked(n, a, args__);\
	va_end(args__);\
	return ret__;

#define LIBNORMALFORM_TWO__(CONNECTIVE)\
	LIBNORMALFORM_SENTENCE *xs__[3] = {l, r, NULL};\
	if (!l || !r) {\
		libnormalform_free(l);\
		libnormalform_free(r);\
		return NULL;\
	}\
	return libnormalform_##CONNECTIVE(xs__);

#define LIBNORMALFORM_MACRO__(CONNECTIVE, ...)\
	(libnormalform_##CONNECTIVE##_checked(\
		sizeof((LIBNORMALFORM_SENTENCE *[]){__VA_OPT__(__VA_ARGS__,) NULL}) / sizeof(LIBNORMALFORM_SENTENCE *) - 1U,\
		(LIBNORMALFORM_SENTENCE *[]){__VA_OPT__(__VA_ARGS__,) NULL}))

/* } */


struct libnormalform_term;





#define LIBNORMALFORM_AVOID_FOR_ALL                 (UINT64_C(1) <<  0) /**< Prefer ¬∃x.¬φ over ∀x.φ */
#define LIBNORMALFORM_AVOID_NEGATED_FOR_ALL         (UINT64_C(1) <<  1) /**< Prefer  ∃x.¬φ over ¬∀x.φ */
#define LIBNORMALFORM_AVOID_FOR_ANY                 (UINT64_C(1) <<  2) /**< Prefer ¬∀x.¬φ over ∃x.φ */
#define LIBNORMALFORM_AVOID_NEGATED_FOR_ANY         (UINT64_C(1) <<  3) /**< Prefer  ∀x.¬φ over ¬∃x.φ */
#define LIBNORMALFORM_RELAX_FOR_ONE                 (UINT64_C(1) <<  4) /**< Relax any positive ∃!x.φ into ∃x.φ */
#define LIBNORMALFORM_REDUCE_XOR                    (UINT64_C(1) <<  5) /**< Rewrite XOR to negation normal form */
#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL         (UINT64_C(1) <<  6) /**< Express   φ(x)∀x:θ(x)   on the form  ∀x.(θ(x) → φ(x)) */
#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL (UINT64_C(1) <<  7) /**< Express ¬(φ(x)∀x:θ(x))  on the form ¬∀x.(θ(x) → φ(x)) */
#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY         (UINT64_C(1) <<  8) /**< Express   φ(x)∃x:θ(x)   on the form  ∃x.(θ(x) ∧ φ(x)) */
#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY (UINT64_C(1) <<  9) /**< Express ¬(φ(x)∃x:θ(x))  on the form ¬∃x.(θ(x) ∧ φ(x)) */
#define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE         (UINT64_C(1) << 10) /**< Express   φ(x)∃!x:θ(x)  on the form  ∃!x.(θ(x) ∧ φ(x)) */
#define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ONE (UINT64_C(1) << 11) /**< Express ¬(φ(x)∃!x:θ(x)) on the form ¬∃!x.(θ(x) ∧ φ(x)) */
#define LIBNORMALFORM_ELIMINATE_FOR_ALL             (UINT64_C(1) << 12) /**< Relax any non-translatable  ∀x.φ to ⊤ */
#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL     (UINT64_C(1) << 13) /**< Relax any non-translatable ¬∀x.φ to ⊤ */
#define LIBNORMALFORM_ELIMINATE_FOR_ANY             (UINT64_C(1) << 14) /**< Relax any non-translatable  ∃x.φ to ⊤ */
#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY     (UINT64_C(1) << 15) /**< Relax any non-translatable ¬∃x.φ to ⊤ */
#define LIBNORMALFORM_ELIMINATE_FOR_ONE             (UINT64_C(1) << 16) /**< Relax any non-translatable ∃!x.φ to ⊤ */
#define LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE     (UINT64_C(1) << 17) /**< Relax any ¬∃!x.φ to ⊤ */
#define LIBNORMALFORM_ELIMINATE_VARIABLE            (UINT64_C(1) << 18) /**< Relax any positive variable literal to ⊤ */
#define LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE    (UINT64_C(1) << 19) /**< Relax any negative variable literal to ⊤ */
#define LIBNORMALFORM_ELIMINATE_FUNCTION            (UINT64_C(1) << 20) /**< Relax any positive function literal to ⊤ */
#define LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION    (UINT64_C(1) << 21) /**< Relax any negative function literal to ⊤ */
#define LIBNORMALFORM_ELIMINATE_XOR                 (UINT64_C(1) << 22) /**< Relax any non-reduce XOR to ⊤ */
#define LIBNORMALFORM_ALL_EXPRESS_FLAGS__          ((UINT64_C(1) << 23) - 1U) /* For internal use */


/**
 * Opaque data type use to express and sentences
 *
 * This object incluses caches and preallocated memory
 * makes object unsafe to be used from two different
 * threads at the same time
 *
 * @seealso  libnormalform_clone
 */
typedef struct libnormalform_sentence LIBNORMALFORM_SENTENCE;


/**
 * Specification for how application provided strings
 * shall be interpreted
 */
struct libnormalform_representation_spec {
	/**
	 * Application-specific data that will be passed into
	 * `.get_variable`, `.get_function`, `.get_map`, and
	 * `.get_transformer` (making it reenterant so it can be
	 * called by multiple threads, or to configure the function)
	 * 
	 * May be `NULL`
	 */
	void *user_data;

	/**
	 * Deserialise a variable from a unterminated string
	 * 
	 * The function shall be able to return the reference
	 * to any `struct libnormalform_variable` given its
	 * `.identifier` sans NUL-termination
	 * 
	 * The function shall be pure in the sence that if
	 * it is called twice (or more) with the identifer
	 * at the beginning of `s` it shall return the same
	 * pointer, not two different copies (`user_data` be
	 * use used to store the variables if they are
	 * constructed dynamically)
	 * 
	 * May be `NULL`
	 * 
	 * @param   s           The string beginning with the variable's
	 *                      identifier
	 * @param   end_out     Output parameter for the position in
	 *                      `s` after the last byte in the identifer
	 * @param   user_data   `.user_data`
	 * @return              A pointer to the referenced variable, `NULL`
	 *                      on failure (`errno` may be set)
	 * 
	 * It is recommended that, on failure, `errno` is set
	 * according to the below specification, however it is
	 * up to the application to choose what to do with `errno`
	 * 
	 * @throws  EINVAL  `s` in not formatted to represent a valid variable
	 * @throws  ENOENT  `s` does not represent any known variable
	 */
	struct libnormalform_variable *(*get_variable)(char *s, char **end_out, void *user_data);

	/**
	 * Same as `.get_variable` except that it returns
	 * reference to a function (`struct libnormalform_function *`)
	 */
	struct libnormalform_function *(*get_function)(char *s, char **end_out, void *user_data);

	/**
	 * Same as `.get_variable` except that it returns
	 * reference to a domain (`struct libnormalform_map *`)
	 */
	struct libnormalform_map *(*get_map)(char *s, char **end_out, void *user_data);

	/**
	 * Same as `.get_transformer` except that it returns
	 * reference to a function (`struct libnormalform_transformer *`)
	 */
	struct libnormalform_transformer *(*get_transformer)(char *s, char **end_out, void *user_data);
};


/**
 * Type if a `struct libnormalform_term`, used to
 * determine which member of `.term` to use and
 * whether it is negated
 */
enum libnormalform_term_type {
	LIBNORMALFORM_CONJUNCTION,            /**< AND clause; empty clause is used for contradiction */
	LIBNORMALFORM_DISJUNCTION,            /**< OR  clause; empty clause is used for tautology */
	LIBNORMALFORM_EXCLUSIVE_DISJUNCTION,  /**< XOR clause; never used for empty clauses */
	LIBNORMALFORM_TRANSFORMATION,         /**< Transformater function with input **/
	LIBNORMALFORM_VARIABLE,               /**< Positive variable literal **/
	LIBNORMALFORM_NEGATED_VARIABLE,       /**< Negative variable literal **/
	LIBNORMALFORM_FUNCTION,               /**< Positive boolean function literal **/
	LIBNORMALFORM_NEGATED_FUNCTION,       /**< Negative boolean function literal **/
	LIBNORMALFORM_FOR_ALL,                /**<  ∀x∈D.(P(x) → Q(x)) expression */
	LIBNORMALFORM_NEGATED_FOR_ALL,        /**< ¬∀x∈D.(P(x) → Q(x)) expression */
	LIBNORMALFORM_FOR_ANY,                /**<  ∃x∈D.(P(x) ∧ Q(x)) expression */
	LIBNORMALFORM_NEGATED_FOR_ANY,        /**< ¬∃x∈D.(P(x) ∧ Q(x)) expression */
	LIBNORMALFORM_FOR_ONE,                /**<  ∃!x∈D.(P(x) ∧ Q(x)) expression */
	LIBNORMALFORM_NEGATED_FOR_ONE         /**< ¬∃!x∈D.(P(x) ∧ Q(x)) expression */
};


/**
 * Value of an atomic sentence
 */
enum libnormalform_value {
	LIBNORMALFORM_FALSE = 0,  /**< Variable has the value False */
	LIBNORMALFORM_TRUE = 1    /**< Variable has the value True */
};


/**
 * Built in transformer functions
 */
enum libnormalform_builtin_transformer {
	LIBNORMALFORM_NOT_BUILT_IN = 0,  /**< Application provided transformer */
	LIBNORMALFORM_DOMAIN_VIEW,   /**< Selects the `.key` from a `struct libnormalform_mapping *` */
	LIBNORMALFORM_IMAGE_VIEW     /**< Selects the `.value` from a `struct libnormalform_mapping *` */
};


/**
 * Relationship (dependency) between the value of two sentences
 */
enum libnormalform_sentences_relationship {
	/**
	 * Left-hand implies right-hand (⊨ P → Q)
	 * 
	 * Example:
	 * -  P = ⋀{a, b}, Q = ⋀{a}
	 * 
	 * Truthtable:
	 *    P: 001
	 *    Q: 011
	 *    ∧: 001
	 *    ∨: 011
	 *    ⊕: 010
	 *    →: 111
	 *    ←: 101
	 * 
	 * Consequence:
	 * -  P ∧ Q = P
	 * -  P ∨ Q = Q
	 * -  P ⊕ Q = ¬P ∧ Q
	 * -  P → Q = ⊤
	 * -  P ← Q cannot be simplified
	 */
	LIBNORMALFORM_MATERIAL_IMPLICATION = -1,

	/**
	 * The terms are identical (⊨ P ↔ Q)
	 * 
	 * Example:
	 * -  P = ⋀{a, b}, Q = ⋀{a, b}
	 * 
	 * Truthtable:
	 *    P: 01
	 *    Q: 01
	 *    ∧: 01
	 *    ∨: 01
	 *    ⊕: 00
	 *    →: 11
	 *    ←: 11
	 * 
	 * Consequence:
	 * -  P ∧ Q = P = Q
	 * -  P ∨ Q = P = Q
	 * -  P ⊕ Q = ⊥
	 * -  P → Q = ⊤
	 * -  P ← Q = ⊤
	 */
	LIBNORMALFORM_IDENTICAL,

	/**
	 * Right-hand implies left-hand (⊨ P ← Q)
	 * 
	 * Example:
	 * -  P = ⋀{a}, Q = ⋀{a, b}
	 * 
	 * Truthtable:
	 *    P: 011
	 *    Q: 001
	 *    ∧: 001
	 *    ∨: 011
	 *    ⊕: 010
	 *    →: 101
	 *    ←: 111
	 * 
	 * Consequence:
	 * -  P ∧ Q = Q
	 * -  P ∨ Q = P
	 * -  P ⊕ Q = P ∧ ¬Q
	 * -  P → Q cannot be simplified
	 * -  P ← Q = ⊤
	 */
	LIBNORMALFORM_CONVERSE_IMPLICATION,

	/**
	 * The terms are the inverse of each other (⊨ P ↮ Q)
	 * 
	 * Example:
	 * -  P = a, Q = ¬a
	 * 
	 * Truthtable:
	 *    P: 01
	 *    Q: 10
	 *    ∧: 00
	 *    ∨: 11
	 *    ⊕: 11
	 *    →: 10
	 *    ←: 01
	 * 
	 * Consequence:
	 * -  P ∧ Q = ⊥
	 * -  P ∨ Q = ⊤
	 * -  P ⊕ Q = ⊤
	 * -  P → Q = Q
	 * -  P ← Q = P
	 */
	LIBNORMALFORM_MUTUALLY_INVERSE,

	/**
	 * Both terms cannot be satisfied at the same time,
	 * but are not each other's inverse (⊨ P ⊼ Q)
	 * 
	 * Example:
	 * -  P = ⋀{a, b}, Q = ⋀{¬b}
	 * 
	 * Truthtable:
	 *    P: 001
	 *    Q: 010
	 *    ∧: 000
	 *    ∨: 011
	 *    ⊕: 011
	 *    →: 110
	 *    ←: 101
	 * 
	 * Consequence:
	 * -  P ∧ Q = ⊥
	 * -  P ∨ Q cannot be simplified
	 * -  P ⊕ Q = P ∨ Q
	 * -  P → Q = ¬P
	 * -  P ← Q = ¬Q
	 */
	LIBNORMALFORM_MUTUALLY_EXCLUSIVE,

	/**
	 * The terms cannot be unsatisfied at the same time,
	 * but they are not identical (⊨ P ∨ Q)
	 * 
	 * Example:
	 * -  P = ⋁{a, b}, Q = ⋁{¬b}
	 * 
	 * Truthtable:
	 *    P: 011
	 *    Q: 101
	 *    ∧: 001
	 *    ∨: 111
	 *    ⊕: 110
	 *    →: 101
	 *    ←: 011
	 * 
	 * Consequence:
	 * -  P ∧ Q cannot be simplified
	 * -  P ∨ Q = ⊤
	 * -  P ⊕ Q = ¬P ∨ ¬Q
	 * -  P → Q = Q
	 * -  P ← Q = P
	 */
	LIBNORMALFORM_JOINTLY_UNDENIABLE,

	/**
	 * The terms are unrelated to each other
	 * 
	 * Example:
	 * -  P = a, Q = b
	 * 
	 * Truthtable:
	 *    P: 0011
	 *    Q: 0101
	 *    ∧: 0001
	 *    ∨: 0111
	 *    ⊕: 0110
	 *    →: 1101
	 *    ←: 1011
	 * 
	 * Consequence:
	 * -  P ∧ Q cannot be simplified
	 * -  P ∨ Q cannot be simplified
	 * -  P ⊕ Q cannot be simplified
	 * -  P → Q cannot be simplified
	 * -  P ← Q cannot be simplified
	 */
	LIBNORMALFORM_MUTUALLY_INDEPENDENT
};



/**
 * Relationship (commonality) between the value of two domains
 *
 * (The documentation uses the term "set", however,
 * properly they are bags (multisets), however this
 * is only important for uniqueness qualification;
 * for the mathematics, you can thing about it as
 * sets)
 */
enum libnormalform_domain_relationship {
	/**
	 * The left-hand set is a superset of the right-hand set (A ⊇ B)
	 * 
	 * Example:
	 * -  A = {a, b}, B = {a}
	 * 
	 * Euler diagram:
	 *    ┌────────────────────────────┐
	 *    │  ┌─A────────────────┐      │
	 *    │  │╱╱╱╱╱╱╱┌─B──────┐╱│      │
	 *    │  │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│      │
	 *    │  │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│      │
	 *    │  │╱╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╱│      │
	 *    │  │╱╱╱╱╱╱╱└────────┘╱│      │
	 *    │  │╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱│      │
	 *    │  └──────────────────┘      │
	 *    └────────────────────────────┘
	 * 
	 * Venn diagram of possibly non-empty intersections:
	 *    ┌────────────────────────────┐
	 *    │  ┌─A─────────────┐         │
	 *    │  │███████████████│         │
	 *    │  │██████┌────────┼──────┐  │
	 *    │  │██████│████████│      │  │
	 *    │  │██████│████████│      │  │
	 *    │  └──────┼────────┘      │  │
	 *    │         │               │  │
	 *    │         └─────────────B─┘  │
	 *    └────────────────────────────┘
	 * 
	 * Consequence:
	 * -  A ∩ B = B
	 * -  A ∪ B = A
	 * -  A ∆ B = A ∖ B
	 * -  ⋀A ⊨ ⋀B
	 * -  ⋁B ⊨ ⋁A
	 * -  ⋀A ∧ ⋀B = ⋀A
	 * -  ⋀A ∨ ⋀B = ⋀B
	 * -  ⋀A ⊕ ⋀B = ¬⋀A ∧ ⋀B
         * -  ⋀A → ⋀B = ⊤
	 * -  ⋀A ← ⋀B cannot be simplified
	 * -  ⋁A ∧ ⋁B = ⋁B
	 * -  ⋁A ∨ ⋁B = ⋁A
	 * -  ⋁A ⊕ ⋁B = ⋁A ∧ ¬⋁B
         * -  ⋁A → ⋁B cannot be simplified
	 * -  ⋁A ← ⋁B = ⊤
	 */
	LIBNORMALFORM_SUPERSET_OF = -1,

	/**
	 * The two terms are identical (A = B)
	 * 
	 * Example:
	 * -  A = {a, b}, B = {a, b}
	 * 
	 * Euler diagram:
	 *    ┌────────────────────────────┐
	 *    │    ┌─A,B──────────────┐    │
	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
	 *    │    │╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳│    │
	 *    │    └──────────────────┘    │
	 *    └────────────────────────────┘
	 * 
	 * Venn diagram of possibly non-empty intersections:
	 *    ┌────────────────────────────┐
	 *    │  ┌─A─────────────┐         │
	 *    │  │               │         │
	 *    │  │      ┌────────┼──────┐  │
	 *    │  │      │████████│      │  │
	 *    │  │      │████████│      │  │
	 *    │  └──────┼────────┘      │  │
	 *    │         │               │  │
	 *    │         └─────────────B─┘  │
	 *    └────────────────────────────┘
	 * 
	 * Consequence:
	 * -  A ∩ B = A = B
	 * -  A ∪ B = A = B
	 * -  A ∆ B = ∅
	 * -  ⋀A = ⋀B
	 * -  ⋁A = ⋁B
	 * -  ⋀A ∧ ⋀B = ⋀A = ⋀B
	 * -  ⋀A ∨ ⋀B = ⋀A = ⋀B
	 * -  ⋀A ⊕ ⋀B = ⊥
         * -  ⋀A → ⋀B = ⊤
	 * -  ⋀A ← ⋀B = ⊤
	 * -  ⋁A ∧ ⋁B = ⋁A = ⋁B
	 * -  ⋁A ∨ ⋁B = ⋁A = ⋁B
	 * -  ⋁A ⊕ ⋁B = ⊥
         * -  ⋁A → ⋁B = ⊤
	 * -  ⋁A ← ⋁B = ⊤
	 */
	LIBNORMALFORM_SAME_AS,

	/**
	 * The left-hand set is a subset of the right-hand set (A ⊆ B)
	 * 
	 * Example:
	 * -  A = {a}, B = {a, b}
	 * 
	 * Euler diagram:
	 *    ┌────────────────────────────┐
	 *    │      ┌─B────────────────┐  │
	 *    │      │╲┌─A──────┐╲╲╲╲╲╲╲│  │
	 *    │      │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│  │
	 *    │      │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│  │
	 *    │      │╲│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲╲│  │
	 *    │      │╲└────────┘╲╲╲╲╲╲╲│  │
	 *    │      │╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲│  │
	 *    │      └──────────────────┘  │
	 *    └────────────────────────────┘
	 * 
	 * Venn diagram of possibly non-empty intersections:
	 *    ┌────────────────────────────┐
	 *    │  ┌─A─────────────┐         │
	 *    │  │               │         │
	 *    │  │      ┌────────┼──────┐  │
	 *    │  │      │████████│██████│  │
	 *    │  │      │████████│██████│  │
	 *    │  └──────┼────────┘██████│  │
	 *    │         │███████████████│  │
	 *    │         └─────────────B─┘  │
	 *    └────────────────────────────┘
	 * 
	 * Consequence:
	 * -  A ∩ B = A
	 * -  A ∪ B = B
	 * -  A ∆ B = B ∖ A
	 * -  ⋀B ⊨ ⋀A
	 * -  ⋁A ⊨ ⋁B
	 * -  ⋀A ∧ ⋀B = ⋀B
	 * -  ⋀A ∨ ⋀B = ⋀A
	 * -  ⋀A ⊕ ⋀B = ⋀A ∧ ¬⋀B
         * -  ⋀A → ⋀B cannot be simplified
	 * -  ⋀A ← ⋀B = ⊤
	 * -  ⋁A ∧ ⋁B = ⋁A
	 * -  ⋁A ∨ ⋁B = ⋁B
	 * -  ⋁A ⊕ ⋁B = ¬⋁A ∧ ⋁B
         * -  ⋁A → ⋁B = ⊤
	 * -  ⋁A ← ⋁B cannot be simplified
	 */
	LIBNORMALFORM_SUBSET_OF,

	/**
	 * The sets have no common elements (A ∩ B = ∅)
	 * 
	 * Example:
	 * -  A = {a}, B = {b}
	 * 
	 * Euler diagram:
	 *    ┌────────────────────────────┐
	 *    │  ┌─A───────┐  ┌─B───────┐  │
	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
	 *    │  │╱╱╱╱╱╱╱╱╱│  │╲╲╲╲╲╲╲╲╲│  │
	 *    │  └─────────┘  └─────────┘  │
	 *    └────────────────────────────┘
	 * 
	 * Venn diagram of possibly non-empty intersections:
	 *    ┌────────────────────────────┐
	 *    │  ┌─A─────────────┐         │
	 *    │  │███████████████│         │
	 *    │  │██████┌────────┼──────┐  │
	 *    │  │██████│        │██████│  │
	 *    │  │██████│        │██████│  │
	 *    │  └──────┼────────┘██████│  │
	 *    │         │███████████████│  │
	 *    │         └─────────────B─┘  │
	 *    └────────────────────────────┘
	 * 
	 * Consequence:
	 * -  A ∩ B = ∅
	 * -  A ∪ B cannot be simplified
	 * -  A ∆ B = A ∪ B
	 * -  ⋀A ∧ ⋀B = ⋀(A ∪ B)
	 * -  ⋀A ∨ ⋀B cannot be simplified
	 * -  ⋀A ⊕ ⋀B cannot be simplified
         * -  ⋀A → ⋀B cannot be simplified
	 * -  ⋀A ← ⋀B cannot be simplified
	 * -  ⋁A ∧ ⋁B cannot be simplified
	 * -  ⋁A ∨ ⋁B = ⋁(A ∪ B)
	 * -  ⋁A ⊕ ⋁B cannot be simplified
         * -  ⋁A → ⋁B cannot be simplified
	 * -  ⋁A ← ⋁B cannot be simplified
	 */
	LIBNORMALFORM_DISJOINT_WITH,

	/**
	 * Both sets have unique elements (A ⊆ A ∪ B ⊇ B, A ∩ B ⊇ ∅)
	 * 
	 * Example:
	 * -  A = {a, b}, B = {b, c}
	 * 
	 * Euler diagram:
	 *    ┌────────────────────────────┐
	 *    │  ┌─A─────────────┐         │
	 *    │  │╱╱╱╱╱╱╱╱╱╱╱╱╱╱╱│         │
	 *    │  │╱╱╱╱╱╱┌────────┼────B─┐  │
	 *    │  │╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲│  │
	 *    │  │╱╱╱╱╱╱│╳╳╳╳╳╳╳╳│╲╲╲╲╲╲│  │
	 *    │  └──────┼────────┘╲╲╲╲╲╲│  │
	 *    │         │╲╲╲╲╲╲╲╲╲╲╲╲╲╲╲│  │
	 *    │         └───────────────┘  │
	 *    └────────────────────────────┘
	 * 
	 * Venn diagram of possibly non-empty intersections:
	 *    ┌────────────────────────────┐
	 *    │  ┌─A─────────────┐         │
	 *    │  │███████████████│         │
	 *    │  │██████┌────────┼──────┐  │
	 *    │  │██████│████████│██████│  │
	 *    │  │██████│████████│██████│  │
	 *    │  └──────┼────────┘██████│  │
	 *    │         │███████████████│  │
	 *    │         └─────────────B─┘  │
	 *    └────────────────────────────┘
	 * 
	 * Consequence:
	 * -  A ∩ B cannot be simplified
	 * -  A ∪ B cannot be simplified
	 * -  A ∆ B cannot be simplified
	 * -  ⋀A ∧ ⋀B = ⋀(A ∪ B)
	 * -  ⋀A ∨ ⋀B cannot be simplified
	 * -  ⋀A ⊕ ⋀B cannot be simplified
         * -  ⋀A → ⋀B cannot be simplified
	 * -  ⋀A ← ⋀B cannot be simplified
	 * -  ⋁A ∧ ⋁B cannot be simplified
	 * -  ⋁A ∨ ⋁B = ⋁(A ∪ B)
	 * -  ⋁A ⊕ ⋁B cannot be simplified
         * -  ⋁A → ⋁B cannot be simplified
	 * -  ⋁A ← ⋁B cannot be simplified
	 */
	LIBNORMALFORM_CONJOINT_WITH
};


/**
 * Variable that can be referenced in a sentence
 */
struct libnormalform_variable {
	/**
	 * The value of the sentence
	 *
	 * This need not be sent when the sentence is constructed,
	 * but not be set before it is evaluated; it is only used
	 * by `libnormalform_evaluate`
	 */
	enum libnormalform_value value;

	/**
	 * Application-specific data that the application
	 * could use to identify the variable
	 * 
	 * May be `NULL`
	 */
	void *user_data;

	/**
	 * Identifier for variable
	 *
	 * This need only be set when `libnormalform_to_string`
	 * is called. The value must be parsable by the application
	 * without any explicit termination
	 */
	const char *identifier;

	/**
	 * `NULL` or copy of of the object for `libnormalform_clone`
	 * 
	 * This field should normally be unset, but before calling
	 * `libnormalform_clone`, the application must set it
	 * either to `NULL` (if the clone can use the same reference)
	 * or to a clone of the variable.
	 */
	struct libnormalform_variable *copy_for_clone;
};


/**
 * Boolean-codomain function that can be referenced in a sentence
 */
struct libnormalform_function {
	/**
	 * Function that is used to evaluate the trueness of something
	 * 
	 * @param   user_data  `.user_data`
	 * @param   input      Input to the function, normally it will
	 *                     be `NULL`, but it is inside the antecedent
	 *                     for a qualifier, it will be the `.key`
	 *                     for some `struct libnormalform_mapping`,
	 *                     and if it is inside the predicate of a
	 *                     qualifier, it will be the `.value`
	 *                     for some `struct libnormalform_mapping`
	 * @return             1 if the function is true,
	 *                     0 if the function is false,
	 *                     -1 on failure (the function may set `errno`)
	 * 
	 * For `libnormalform_exists`, `libnormalform_nexists`,
	 * and `libnormalform_unique`, it will only be called
	 * for the `.key` for `struct libnormalform_mapping`'s
	 * 
	 * For `libnormalform_universally`, `libnormalform_existentially`,
	 * and `libnormalform_uniquely`, it will only be called
	 * for the `.value` for `struct libnormalform_mapping`'s
	 */
	int (*evaluate)(void *user_data, void *input);

	/**
	 * Application-specific data that will be passed into
	 * `.evaluate` (making it reenterant so it can be called
	 * by multiple threads, or to configure the function)
	 * 
	 * May be `NULL`
	 */
	void *user_data;

	/**
	 * Identifier for function
	 *
	 * This need only be set when `libnormalform_to_string`
	 * is called. The value must be parsable by the application
	 * without any explicit termination
	 */
	const char *identifier;

	/**
	 * `NULL` or copy of of the object for `libnormalform_clone`
	 * 
	 * This field should normally be unset, but before calling
	 * `libnormalform_clone`, the application must set it
	 * either to `NULL` (if the clone can use the same reference)
	 * or to a clone of the variable.
	 */
	struct libnormalform_function *copy_for_clone;

	/**
	 * See `.requires_relaxation`
	 */
	struct libnormalform_function *relaxation;

	/**
	 * Before calling `libnormalform_express`, `libnormalform_dnf`,
	 * or `libnormalform_cnf` this shall be set to 0 if the function
	 * may keep the function as is, or to a non-0 value if it shall
	 * be replaced `.relaxation` or by TRUE if `.relaxation` is `NULL`
	 */
	int requires_relaxation;
};


/**
 * Generic function that can be referenced in a sentence
 * 
 * The function must be pure and distributive over any boolean operator
 * (it must be an endomorphism). That is, the output is always the
 * same for the same input without any side effects, and for any sentence
 * A * B, where * is any boolean operator and F is the function,
 * F(A * B) = F(A) * F(B).
 */
struct libnormalform_transformer {
	/**
	 * Function that is used to transform input
	 * 
	 * @param   user_data  `.user_data`
	 * @param   input      Input to the function, normally it will
	 *                     be `NULL`, but it is inside the antecedent
	 *                     for a qualifier, it will be the `.key`
	 *                     for some `struct libnormalform_mapping`,
	 *                     and if it is inside the predicate of a
	 *                     qualifier, it will be the `.value`
	 *                     for some `struct libnormalform_mapping`,
	 *                     except that during the create of a
	 *                     `struct libnormalform_term`, the library
	 *                     may insert builtin transformers that will
	 *                     have the `struct libnormalform_mapping *`
	 *                     as input and will output the `.key` or
	 *                     `.value`
	 * @return             The transformation of `input` (not `NULL`),
	 *                     `NULL` on failure (the function may set `errno`)
	 * 
	 * For `libnormalform_exists`, `libnormalform_nexists`,
	 * and `libnormalform_unique`, it will only be called
	 * for the `.key` for `struct libnormalform_mapping`'s
	 * 
	 * For `libnormalform_universally`, `libnormalform_existentially`,
	 * and `libnormalform_uniquely`, it will only be called
	 * for the `.value` for `struct libnormalform_mapping`'s
	 */
	void *(*transform)(void *user_data, void *input);

	/**
	 * The function is called when the output of `.transform`
	 * is not longer needed by the library
	 * 
	 * May be `NULL`
	 * 
	 * This function is not called if `.transform` output `NULL`
	 * 
	 * @param  user_data  `.user_data`
	 * @param  output     The pointer that was returned by `.transform`
	 */
	void (*deallocate)(void *user_data, void *output);

	/**
	 * Application-specific data that will be passed into
	 * `.transform` and `.deallocate` (making them reenterant
	 * so it can be called by multiple threads, or to
	 * configure the function)
	 * 
	 * May be `NULL`
	 */
	void *user_data;

	/**
	 * Identifier for function
	 *
	 * This need only be set when `libnormalform_to_string`
	 * is called. The value must be parsable by the application
	 * without any explicit termination
	 */
	const char *identifier;

	/**
	 * `NULL` or copy of of the object for `libnormalform_clone`
	 * 
	 * This field should normally be unset, but before calling
	 * `libnormalform_clone`, the application must set it
	 * either to `NULL` (if the clone can use the same reference)
	 * or to a clone of the variable.
	 */
	struct libnormalform_transformer *copy_for_clone;

	/**
	 * Before calling `libnormalform_express`, `libnormalform_dnf`,
	 * or `libnormalform_cnf` this shall be set to 0 if the function
	 * may keep the function, or to a non-0 value if it shall
	 * be replaced with a tautology
	 */
	int requires_elimination;

	/**
	 * This field will automatically be set to `LIBNORMALFORM_NOT_BUILT_IN`
	 * to indicated that the object originates in the application,
	 * however a `struct libnormalform_term *` created by the library
	 * (via `libnormalform_express`, `libnormalform_dnf`, or
	 * `libnormalform_cnf`) can contain objects with other values in this
	 * field, to describe what it does. In particular, depending on the
	 * flags used when creating the `struct libnormalform_term *`,
	 * qualification sentences may contain `LIBNORMALFORM_DOMAIN_VIEW`
	 * and `LIBNORMALFORM_IMAGE_VIEW` and transformers.
	 */
	enum libnormalform_builtin_transformer builtin;
};


/**
 * Key–value pair
 */
struct libnormalform_mapping {
	/**
	 * Key
	 * 
	 * In mapped qualifiers (`libnormalform_all`,
	 * `libnormalform_any`, `libnormalform_one`), this
	 * is used as the input for the antecedent
	 * 
	 * In unmapped qualifiers (`libnormalform_exists`,
	 * `libnormalform_nexists`, `libnormalform_unique`),
	 * is this used as the input for the predicate
	 * 
	 * In premapped qualifiers (`libnormalform_universally`,
	 * `libnormalform_existentially`, `libnormalform_uniquely`),
	 * is this unused
	 * 
	 * Unused for domain size checks (`libnormalform_empty`,
	 * `libnormalform_nonempty`, `libnormalform_singleton`)
	 */
	void *key;

	/**
	 * Value
	 * 
	 * In mapped qualifiers (`libnormalform_all`,
	 * `libnormalform_any`, `libnormalform_one`), this
	 * is used as the input for the predicate
	 * 
	 * In unmapped qualifiers (`libnormalform_exists`,
	 * `libnormalform_nexists`, `libnormalform_unique`),
	 * is this unused
	 * 
	 * In premapped qualifiers (`libnormalform_universally`,
	 * `libnormalform_existentially`, `libnormalform_uniquely`),
	 * is this used as the input for the predicate
	 * 
	 * Unused for domain size checks (`libnormalform_empty`,
	 * `libnormalform_nonempty`, `libnormalform_singleton`)
	 */
	void *value;
};


/**
 * Domain of interest for qualifiers
 */
struct libnormalform_map {
	/**
	 * Associative array over values in the domain
	 */
	struct libnormalform_mapping *mappings;

	/**
	 * The number of elements in `.mappings`
	 */
	size_t nmappings;

	/**
	 * Application-specific data that the application
	 * could use to identify the domain
	 * 
	 * May be `NULL`
	 */
	void *user_data;

	/**
	 * Identifier for domain
	 *
	 * This need only be set when `libnormalform_to_string`
	 * is called. The value must be parsable by the application
	 * without any explicit termination
	 */
	const char *identifier;

	/**
	 * `NULL` or copy of of the object for `libnormalform_clone`
	 * 
	 * This field should normally be unset, but before calling
	 * `libnormalform_clone`, the application must set it
	 * either to `NULL` (if the clone can use the same reference)
	 * or to a clone of the variable.
	 */
	struct libnormalform_map *copy_for_clone;
};


struct libnormalform_atom_comparsion {
	int version;
	enum libnormalform_sentences_relationship relationship;
};

struct libnormalform_domain_comparsion {
	int version;
	enum libnormalform_domain_relationship relationship;
};

struct libnormalform_analysers { /* TODO doc */
	void *user_data;
	int (*compare_variable_to_variable)(void *user_data, struct libnormalform_atom_comparsion *result,
	                                    struct libnormalform_variable *left, struct libnormalform_variable *right);
	int (*compare_function_to_function)(void *user_data, struct libnormalform_atom_comparsion *result,
	                                    struct libnormalform_function *left, struct libnormalform_function *right);
	int (*compare_variable_to_function)(void *user_data, struct libnormalform_atom_comparsion *result,
	                                    struct libnormalform_variable *left, struct libnormalform_function *right);
	int (*compare_domains)(void *user_data, struct libnormalform_domain_comparsion *result,
	                       struct libnormalform_map *left, struct libnormalform_map *right);
};


/**
 * Qualifier
 */
struct libnormalform_qualification {
	struct libnormalform_map *map;          /**< The domain of interest */
	struct libnormalform_term *antecedent;  /**< The antecedent, `NULL` if joined with the predicate */
	struct libnormalform_term *predicate;   /**< The predicate */
};


/**
 * Clause of terms
 */
struct libnormalform_clause {
	struct libnormalform_term *terms;  /**< The terms in the clause */
	size_t nterms;                     /**< The number of terms in the clause */
};


/**
 * Transformater function with input
 */
struct libnormalform_transformation {
	struct libnormalform_transformer *transformer;  /**< The transformer function */
	struct libnormalform_term *sentence;            /**< The sentence the transformation is over */
};


/**
 * Application-readable sentence
 */
struct libnormalform_term {
	/**
	 * The type of the clause, qualifier, literal, or transformation
	 */
	enum libnormalform_term_type type;

	/**
	 * Whether the term or own of its subterms have been reduced;
	 */
	int reduced;

	/**
	 * The description of the sentence
	 */
	union {
		/**
		 * Use if `.type` is `LIBNORMALFORM_DISJUNCTION`
		 */
		struct libnormalform_clause disjunction;

		/**
		 * Use if `.type` is `LIBNORMALFORM_CONJUNCTION`
		 */
		struct libnormalform_clause conjunction;

		/**
		 * Use if `.type` is `LIBNORMALFORM_EXCLUSIVE_DISJUNCTION`
		 */
		struct libnormalform_clause exclusive_disjunction;

		/**
		 * Use if `.type` is `LIBNORMALFORM_DISJUNCTION`,
		 * `LIBNORMALFORM_CONJUNCTION`, or
		 * `LIBNORMALFORM_EXCLUSIVE_DISJUNCTION`
		 */
		struct libnormalform_clause clause;

		/**
		 * Use if `.type` is `LIBNORMALFORM_TRANSFORMATION`
		 */
		struct libnormalform_transformation transformation;

		/**
		 * Use if `.type` is `LIBNORMALFORM_VARIABLE` or
		 * `LIBNORMALFORM_NEGATED_VARIABLE`
		 */
		struct libnormalform_variable *variable;

		/**
		 * Use if `.type` is `LIBNORMALFORM_FUNCTION` or
		 * `LIBNORMALFORM_NEGATED_FUNCTION`
		 */
		struct libnormalform_function *function;

		/**
		 * Use if '.type` is `LIBNORMALFORM_FOR_ALL` or
		 * `LIBNORMALFORM_NEGATED_FOR_ALL`
		 */
		struct libnormalform_qualification for_all;

		/**
		 * Use if '.type` is `LIBNORMALFORM_FOR_ANY` or
		 * `LIBNORMALFORM_NEGATED_FOR_ANY`
		 */
		struct libnormalform_qualification for_any;

		/**
		 * Use if '.type` is `LIBNORMALFORM_FOR_ONE` or
		 * `LIBNORMALFORM_NEGATED_FOR_ONE`
		 */
		struct libnormalform_qualification for_one;

		/**
		 * Use if '.type` is `LIBNORMALFORM_FOR_ALL`,
		 * `LIBNORMALFORM_NEGATED_FOR_ALL`, `LIBNORMALFORM_FOR_ANY`,
		 * `LIBNORMALFORM_NEGATED_FOR_ANY`, `LIBNORMALFORM_FOR_ONT`,
		 * or `LIBNORMALFORM_NEGATED_FOR_ONE`
		 */
		struct libnormalform_qualification qualification;
	} term;
};





/**
 * Increase the reference count of a sentence object by 1
 * 
 * @param   this  The sentence object
 * @return        `this` on success, `NULL` on failure
 * 
 * @throws  ENOMEM  The reference count is already maximised (at SIZE_MAX)
 * 
 * Reasonable application can safely assume that `this` is always returned
 * 
 * Note, `NULL` is returned without `errno` modified if `this` is `NULL`
 * 
 * Be aware that this function is not thread-safe
 * 
 * @seealso  libnormalform_clone
 * @seealso  libnormalform_free
 */
LIBNORMALFORM_SENTENCE *(libnormalform_ref)(LIBNORMALFORM_SENTENCE *this);


/**
 * Create a copy of a sentence object
 * 
 * This may be necessary as usage of sentence objects are not thread-safe,
 * creating a copy of a sentence object will allow one thread to safely
 * use one copy and another thread the other copy
 * 
 * Before calling this function, the application shall set `.copy_for_clone`
 * in each `struct libnormalform_variable`, `struct libnormalform_function`,
 * `struct libnormalform_map` and `struct libnormalform_transformer`, used
 * by the sentence. `.copy_for_clone` shall either be set to `NULL` or a copy
 * of object. If `NULL` is used, the copy of `this` will use the same
 * instance of the object as `this`.
 * 
 * @param   this  The sentence object
 * @return        A unique pointer on success or `NULL` if
 *                `this` is `NULL`; `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create a copy of `this`
 * 
 * Be aware that this function is not thread-safe
 * 
 * @seealso  libnormalform_ref
 * @seealso  libnormalform_free
 */
LIBNORMALFORM_USE_RESULT__
LIBNORMALFORM_SENTENCE *(libnormalform_clone)(LIBNORMALFORM_SENTENCE *this);


/**
 * When `this` is a `LIBNORMALFORM_SENTENCE *`:
 * 
 *     Decrease the reference count of a sentence object by 1, 
 *     if the object reference count reaches 0, deallocate the
 *     object.
 * 
 *     Because all functions that return a new sentence object
 *     (excluding `libnormalform_clone`), adopt the ownership
 *     of the reference to each input sentence (and may create
 *     it's own subsentences), this function is called recursively,
 *     and the application shall not attempt to call this function
 *     for sentences used to create other sentences
 * 
 *     Be aware the this function will not deallocate any
 *     `struct libnormalform_variable *`,
 *     `struct libnormalform_function *`, or
 *     `struct libnormalform_map *` used in the sentence as
 *     these are owned any managed by the application
 * 
 * When `this` is a `struct libnormalform_term *`:
 * 
 *     Recursively deallocate `this`. This will only deallocate
 *     `this` and subobjects with the same type
 * 
 *     If `.type` is invalid for `this` or any subobject, the
 *     function's behaviour is undefined
 * 
 * This function is a no-operation function when `this` is `NULL`
 * 
 * @param   this  The object
 * 
 * This function's behaviour is undefined if `this` is not `NULL`
 * but not of the one of the above listed types
 * 
 * Be aware that this function is not thread-safe
 */
void (libnormalform_free)(void *this);


/**
 * Evaluate a sentence to determine it's trueness
 * 
 * Before calling this function, the application code shall
 * configure any `struct libnormalform_variable`,
 * `struct libnormalform_function`, and `struct libnormalform_map`
 * used by the sentence. For each `struct libnormalform_variable`,
 * `.value` shall either be set to `LIBNORMALFORM_TRUE` or
 * `LIBNORMALFORM_FALSE` to indicate the value of the atom.
 * For each `struct libnormalform_function`, `.evaluate` shall
 * be set to a pointer to function that evaluates the input and
 * `.user_data` shall be set to any application data the function
 * needs to operate; `.evaluate` shall return 1, 0, or -1 as
 * specified for this function; and may set `errno` to indicate
 * an error (library itself does not look at `errno`, but may
 * be used to signal the error to the application, of course
 * the error may also be specified to the application in an
 * application-specific way). For each `struct libnormalform_map`,
 * `.mappings` shall be to the associated array of values
 * that shall be tested by the qualifier-sentence it is
 * used by, and `.nmappings` shall be set to the number of
 * pairs in this array.
 * 
 * @param   this  The sentence to evaluate
 * @return        1 if the sentence is true,
 *                0 if the sentence is false,
 *                -1 on failure
 * 
 * Only application code may cause this function to
 * fail, therefore no error codes are predefined for
 * this function, instead `errno` is only set by
 * the failing application code
 * 
 * Be aware that this function is not thread-safe
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
int (libnormalform_evaluate)(LIBNORMALFORM_SENTENCE *this);





/**
 * Return an application readable expression of a statement in negation
 * normal form, optionally with XOR, and reduce the statement to a
 * statement that is at least as true (but as false as possible), and
 * is minimised, according what the application specifies that it can
 * work with
 * 
 * Before calling this function, the application shall set `.relaxation`
 * `.requires_relaxation` in each `struct libnormalform_function` used
 * used by the sentence. `.requires_relaxation` may be set as 0 if the
 * function shall not be replaced (in this case `.relaxation` need not
 * be set), but set to 1 if the function most be replaced with a more
 * true function. In the latter case, `.relaxation` shall either be set
 * to the new function or to `NULL`; if set to null, the function is
 * reduced to a tautological sentence. For any `libnormalform_transformer`
 * it must also set `.requires_elimination` to 1 if the transformation
 * must be replaces with a tautology, and 0 otherwise.
 * 
 * @param   this       The sentence to describe
 * @param   flags      The bitwise OR of any number of the following values:
 *                     - LIBNORMALFORM_AVOID_FOR_ALL:                   Prefer ¬∃x.¬φ over ∀x.φ
 *                     - LIBNORMALFORM_AVOID_NEGATED_FOR_ALL:           Prefer  ∃x.¬φ over ¬∀x.φ
 *                     - LIBNORMALFORM_AVOID_FOR_ANY:                   Prefer ¬∀x.¬φ over ∃x.φ
 *                     - LIBNORMALFORM_AVOID_NEGATED_FOR_ANY:           Prefer  ∀x.¬φ over ¬∃x.φ
 *                     - LIBNORMALFORM_RELAX_FOR_ONE:                   Relax any positive ∃!x.φ into ∃x.φ
 *                     - LIBNORMALFORM_REDUCE_XOR:                      Do not use XOR in the returned statement,
 *                                                                      but transform it to negation normal form
 *                     - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL            Express   φ(x)∀x:θ(x)   on the form  ∀x.(θ(x) → φ(x))
 *                     - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL    Express ¬(φ(x)∀x:θ(x))  on the form ¬∀x.(θ(x) → φ(x))
 *                     - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY            Express   φ(x)∃x:θ(x)   on the form  ∃x.(θ(x) ∧ φ(x))
 *                     - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY    Express ¬(φ(x)∃x:θ(x))  on the form ¬∃x.(θ(x) ∧ φ(x))
 *                     - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE            Express   φ(x)∃!x:θ(x)  on the form  ∃!x.(θ(x) ∧ φ(x))
 *                     - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ONE    Express ¬(φ(x)∃!x:θ(x)) on the form ¬∃!x.(θ(x) ∧ φ(x))
 *                     - LIBNORMALFORM_ELIMINATE_FOR_ALL                Relax any non-translatable  ∀x.φ to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL        Relax any non-translatable ¬∀x.φ to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_FOR_ANY                Relax any non-translatable  ∃x.φ to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_IN_NEGATED_FOR_ANY     Relax any non-translatable ¬∃x.φ to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_IN_FOR_ONE             Relax any non-translatable ∃!x.φ to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_IN_NEGATED_FOR_ONE     Relax any ¬∃!x.φ to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_VARIABLE               Relax any positive variable literal to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE       Relax any negative variable literal to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_FUNCTION               Relax any positive function literal to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION       Relax any negative function literal to ⊤
 *                     - LIBNORMALFORM_ELIMINATE_XOR                    Remove all XOR's (nullified by `LIBNORMALFORM_REDUCE_XOR`)
 * @param   analysers  Application provided functions to help reduce the statement, or `NULL`
 * @return             The description of the sentence, `NULL` on failure;
 *                     the returned pointer shall be deallocated with
 *                     `libnormalform_free` when it is no longer needed
 * 
 * @seealso  libnormalform_dnf
 * @seealso  libnormalform_cnf
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
struct libnormalform_term *(libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO man */
                                                   const struct libnormalform_analysers *analysers);


/**
 * Variant of `libnormalform_express` that always canonicalises
 * the statement to disjunctive normal form
 * 
 * @param   this       The sentence to describe
 * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR`
 *                     is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not,
 *                     but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless
 *                     there is a risk that it would be too costly (EXPSPACE)
 * @param   analysers  Application provided functions to help reduce the statement, or `NULL`
 * @return             The description of the sentence, `NULL` on failure;
 *                     the returned pointer shall be deallocated with
 *                     `libnormalform_free` when it is no longer needed
 * 
 * @seealso  libnormalform_express
 * @seealso  libnormalform_cnf
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
struct libnormalform_term *(libnormalform_dnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO */ /* TODO man */
                                               const struct libnormalform_analysers *analysers);


/**
 * Variant of `libnormalform_express` that always canonicalises
 * the statement to conjuctive normal form
 * 
 * @param   this       The sentence to describe
 * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR`
 *                     is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not,
 *                     but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless
 *                     there is a risk that it would be too costly (EXPSPACE)
 * @param   analysers  Application provided functions to help reduce the statement, or `NULL`
 * @return             The description of the sentence, `NULL` on failure;
 *                     the returned pointer shall be deallocated with
 *                     `libnormalform_free` when it is no longer needed
 * 
 * @seealso  libnormalform_express
 * @seealso  libnormalform_dnf
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
struct libnormalform_term *(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO */ /* TODO man */
                                               const struct libnormalform_analysers *analysers);


/**
 * Convert a sentence object to a string that can be parsed
 * by `libnormalform_from_string` (and is somewhat human-readable)
 * 
 * Before calling this function, the application shall set `.identifier`
 * in each `struct libnormalform_variable`, `struct libnormalform_function`,
 * `struct libnormalform_map`, and `struct libnormalform_transformer` used
 * by the sentence to a non-`NULL`, unique string that identifies (but
 * does not necessarily describe) the object. The application must be able
 * to find the end of any such string without any explicit termination
 * (e.g., eithout there being a NUL-terminator)
 * 
 * Note that when a sentence is created, it is optimised and
 * reduced into fewer types of connetives (it's reducted into
 * negation normal form, except with XOR allowed, but not
 * necessarily to any canonical form) during construction,
 * so this function will not necessarily reproduce the sentence
 * as it was specified when it was constructed.
 * 
 * @param   this  The sentence object to serialise
 * @return        String-representation of `this`, `NULL` failure;
 *                the caller shall deallocate the returned pointer
 *                with free(3) when it is no longer needed
 *
 * @throws  ENOMEM  Insufficient memory available to serialise `this`
 * 
 * @seealso  libnormalform_from_string
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_USE_FREE__ LIBNORMALFORM_NONNULL_INPUT__
char *(libnormalform_to_string)(LIBNORMALFORM_SENTENCE *this);


/**
 * Convert a string, created with `libnormalform_to_string`
 * (or is on similar form), to sentence object
 * 
 * The string shall be on the whitespace-insensitive form:
 * 
 *     constant         ::= "TRUE" | "FALSE";
 *     connective1      ::= "NOT";
 *     connective2      ::= "AND" | "OR" | "XOR" | "IF" | "IMPLY" |
 *                          "NAND" | "NOR" | "XNOR" | "NIF" | "NIMPLY";
 *     qualifier0       ::= "EMPTY" | "NONEMPTY" | "SINGLETON";
 *     qualifier1       ::= "EXISTS" | "NEXISTS" | "UNIQUE" |
 *                          "EXISTENTIALLY" | "UNIVERSALLY" | "UNIQUELY";
 *     qualifier2       ::= "ALL" | "ANY" | "ONE";
 *     unary            ::= connective1 [reference-point] "(" sentence ")";
 *     variadic         ::= connective2 [reference-point] "(" [sentence-list] ")";
 *     sentence-list    ::= sentence ["," sentence-list];
 *     qualified0       ::= qualifier0 [reference-point] "(" map ")";
 *     qualified1       ::= qualifier1 [reference-point] "(" map "," sentence ")";
 *     qualified2       ::= qualifier2 [reference-point] "(" map "," sentence "," sentence ")";
 *     atom             ::= atom-var | atom-fun;
 *     atom-var         ::= "VARIABLE" [reference-point] "(" variable ")";
 *     atom-fun         ::= "FUNCTION" [reference-point] "(" function ")";
 *     transformation   ::= "TRANSFORMATION" [reference-point] "(" transformer "," sentence ")";
 *     reference-point  ::= "@" decimal-number;
 *     reference        ::= "REF(" decimal-number ")";
 *     one-to-nine      ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9";
 *     zero-to-nine     ::= "0" | one-to-nine;
 *     decimal-number   ::= "0" | positive-decimal;
 *     positive-decimal ::= one-to-nine [digits];
 *     digits           ::= zero-to-nine [digits];
 *     sentence         ::= constant | unary | variadic | qualified0 | qualified1 |
 *                          qualified2 | atom | transformation | reference;
 * 
 * where "sentence" is the root, and where "map" is parsed by `*spec->get_map`,
 * "variable" is parsed by `*spec->get_variable`, "function" is parsed by
 * `*spec->get_function`, and "transformer" is parsed by `*spec->get_transformer`.
 * References must start at 0 and increment by one, in left-to-right order,
 * every time reference point is specified, and forward-references are not allowed
 * (this includes reference to containing sentence (whose reference ID is lower
 * because it is written earlier)).
 * 
 * @param   s        The representation of the sentence to deserialise
 * @param   end_out  Output parameter for the end of `s`;
 *                   if `NULL` the function will fail if `s` contains
 *                   excess information
 * @param   spec     Specification for how application managed objects
 *                   are to be deserialise
 * @return           A unique pointer, that is a deserialisation of `s`,
 *                   or `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to deserialise `s`
 * @throws  EINVAL  `s` was not properly formatted
 * @throws  EINVAL  `end_out` was `NULL` and `s` containd excess information
 * @throws  EDOM    `s` contained a empty clause for a connective
 *                  that does not support empty clauses
 * @throws  EDOM    `s` contained a transformation over a qualifer
 * @throws  ENOENT  `s` contained a variable but `spec->get_variable` was `NULL`
 * @throws  ENOENT  `s` contained a boolean function but `spec->get_function` was `NULL`
 * @throws  ENOENT  `s` contained a domain but `spec->get_map` was `NULL`
 * @throws  ENOENT  `s` contained a transformation but `spec->get_transformer` was `NULL`
 * 
 * If function in `spec` fails, this function will fail and keep `errno`
 * as set by the function that failed
 * 
 * The function itself does not modify `s` and can operate on read-only
 * memory, however an offset of the string may be passed into application
 * code. The application is free to modify `s` if it knows the memory
 * is indeed writable.
 * 
 * @seealso  libnormalform_to_string
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1) LIBNORMALFORM_ONE_NONNULL_INPUT__(3)
LIBNORMALFORM_SENTENCE *(libnormalform_from_string)(char *s, char **end_out, const struct libnormalform_representation_spec *spec);





/**
 * Create an atomic sentence whose value is externally set
 * 
 * @param   variable  The variable the sentence shall express
 * @return            A sentence object referencing `variable`, `NULL` on failure
 * @throws  ENOMEM    Insufficient memory available to create the sentence
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_variable)(struct libnormalform_variable *variable);


/**
 * Create an atomic sentence whose value is externally evaluated
 * 
 * @param   function  The function the sentence shall express
 * @return            A sentence object referencing `function`, `NULL` on failure
 * @throws  ENOMEM    Insufficient memory available to create the sentence
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_function)(struct libnormalform_function *function);


/**
 * Create an endomorphic transformation of the input for a sentence
 *
 * `function->builtin` will automatically be initialised to `LIBNORMALFORM_NOT_BUILT_IN`
 * 
 * @param   function  The transformation function
 * @param   sentence  The sentence whose input shall be transformed
 * @return            A sentence whose input is transformed by `function`, `NULL` on failure
 * @throws  ENOMEM    Insufficient memory available to create the sentence
 * @throws  EDOM      `sentence` is a qualifier
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
LIBNORMALFORM_SENTENCE *(libnormalform_transformation)(struct libnormalform_transformer *function, LIBNORMALFORM_SENTENCE *sentence);


/**
 * TRUE: Tautology
 *
 * Always true
 *
 * Commonly written "⊤", "1", or "T"
 * 
 * @return            An atomic sentence with a constant value of True, `NULL` on failure
 * @throws  ENOMEM    Insufficient memory available to create the sentence
 */
LIBNORMALFORM_USE_RESULT__
LIBNORMALFORM_SENTENCE *(libnormalform_true)(void);


/**
 * FALSE: Contradiction
 * 
 * Always false
 * 
 * Commonly written "⊥", "1", or "F"
 * 
 * @return            An atomic sentence with a constant value of False, `NULL` on failure
 * @throws  ENOMEM    Insufficient memory available to create the sentence
 */
LIBNORMALFORM_USE_RESULT__
LIBNORMALFORM_SENTENCE *(libnormalform_false)(void);


/**
 * NOT: Negation
 *
 * The condition must not be met:
 * ¬0 = 1
 * ¬1 = 0
 *
 * Properties:
 * -  Involution
 * -  Distribution over AND changes connective to OR (De Morgan's law)
 * -  Distribution over OR changes connective to AND (De Morgan's law)
 * 
 * Commonly written "¬" ("¬x"), "~", or "!", or with overstroke
 * 
 * @param   x  The sentence that should be negated;
 *             ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `x` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `x` to
 * be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
LIBNORMALFORM_SENTENCE *(libnormalform_not)(LIBNORMALFORM_SENTENCE *x);


/**
 * FOR ALL: Universal quantification (mapped)
 * 
 * The predicate must be met for every element that the antecedent
 * is met for; if no element exists, or the antecedent is false for
 * every element, the sentence is true
 * 
 * Properties:
 * -  Vacuous truth
 * -  ∀x∈D.P(x) → ⊤ = ⊤
 * -  ∀x∈D.⊥ → Q(x) = ⊤
 * -  ∀x∈D.⊤ → ⊥ ⊨ D = ∅
 * -  Conjunction
 * 
 * Commonly written "∀" ("∀x∈d.k(x) → v(x)", "∀x∈d (k(x) → v(x))", or "v(x) ∀ x∈d : k(x)")
 * 
 * The antecedent is tested for every `.key` in the domain,
 * and the predicate is tested for every associated `.value`
 * where the antecedent is met; but the testing is cut short
 * if the antecedent is met and not the predicate for an element
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   k  The antecedent; ownership is transfered to this function
 * @param   v  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `k` or `v` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `k` or
 * `v` to be `NULL`)
 * 
 * @seealso  libnormalform_nexists
 * @seealso  libnormalform_universally
 * @seealso  libnormalform_any
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
LIBNORMALFORM_SENTENCE *(libnormalform_all)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v);


/**
 * THERE EXISTS: Existential quantification (mapped)
 * 
 * The predicate must be met for at least one element that the
 * antecedent is met for; if no element exists, or the antecedent is
 * false for every element, the sentence is false
 * 
 * Properties:
 * -  Vacuous falsity
 * -  ∃x∈D.P(x) ∧ ⊥ = ⊥
 * -  ∃x∈D.⊥ ∧ Q(x) = ⊥
 * -  ∃x∈D.⊤ ∧ ⊤ ⊨ D ⊃ ∅
 * -  Disjunction
 * 
 * Commonly written "∃" ("∃x∈d.k(x) ∧ v(x)", "∃x∈d (k(x) ∧ v(x))", or "v(x) ∃ x∈d : k(x)")
 * 
 * The antecedent is tested for every `.key` in the domain,
 * and the predicate is tested for every associated `.value`
 * where the antecedent is met; but the testing is cut short
 * if both the antecedent and predicate is met for an element
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   k  The antecedent; ownership is transfered to this function
 * @param   v  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `k` or `v` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `k` or
 * `v` to be `NULL`)
 * 
 * @seealso  libnormalform_exists
 * @seealso  libnormalform_existentially
 * @seealso  libnormalform_one
 * @seealso  libnormalform_all
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
LIBNORMALFORM_SENTENCE *(libnormalform_any)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v);


/**
 * THERE EXISTS ONE: Unique existential quantification (mapped)
 * 
 * The predicate must be met for exactly one element that the
 * antecedent is met for; if no element exists, or the antecedent is
 * false for every element, the sentence is false
 * 
 * Properties:
 * -  Vacuous falsity
 * -  ∃!x∈D.P(x) ∧ ⊥ = ⊥
 * -  ∃!x∈D.⊥ ∧ Q(x) = ⊥
 * -  ∃!x∈D.⊤ ∧ ⊤ ⊨ |D| = 1
 * 
 * Commonly written "∃!" ("∃!x∈d.k(x) ∧ v(x)", "∃!x∈d (k(x) ∧ v(x))", or "v(x) ∃! x∈d : k(x)")
 * 
 * The antecedent is tested for every `.key` in the domain,
 * and the predicate is tested for every associated `.value`
 * where the antecedent is met; but the testing is cut short
 * if both the antecedent and predicate is met for two elements
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   k  The antecedent; ownership is transfered to this function
 * @param   v  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `k` or `v` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `k` or
 * `v` to be `NULL`)
 * 
 * @seealso  libnormalform_unique
 * @seealso  libnormalform_uniquely
 * @seealso  libnormalform_any
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
LIBNORMALFORM_SENTENCE *(libnormalform_one)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k, LIBNORMALFORM_SENTENCE *v);





/**
 * AND: Conjunction
 *
 * Also known as BUT
 * 
 * All conditions must be met
 * 
 * 0 ∧ 0 = 0
 * 0 ∧ 1 = 0
 * 1 ∧ 0 = 0
 * 1 ∧ 1 = 1
 * 
 * Properties:
 * -  Vacuous truth
 * -  Identity singleton
 * -  Commutative
 * -  Associative
 * -  Distributive over OR
 * -  Distributive over XOR
 * -  ⊤ as identity
 * -  Dominated by ⊥
 * -  Idempotent
 * -  Connecting complement results in contradiction
 * -  More lax term is absorbed (A ∧ (A ∨ B) simplifies to A)
 * 
 * Commonly written "∧" ("⋀" if n-ary), "&", or with juxtaposition
 * 
 * @param   xs  `NULL`-terminated list of sentences that should be
 *              joined by the connective AND; this can be any number
 *              of arguments, even none; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_AND
 * @seealso  libnormalform_and_checked
 * @seealso  libnormalform_andl_checked
 * @seealso  libnormalform_vand_checked
 * @seealso  libnormalform_andl
 * @seealso  libnormalform_vand
 * @seealso  libnormalform_and2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_and)(LIBNORMALFORM_SENTENCE **xs);


/**
 * OR: Disjunction
 * 
 * Also known as Inclusive disjunction
 * 
 * At least one condition must be met
 * 
 * 0 ∨ 0 = 0
 * 0 ∨ 1 = 1
 * 1 ∨ 0 = 1
 * 1 ∨ 1 = 1
 * 
 * Properties:
 * -  Vacuous falsity
 * -  Identity singleton
 * -  Commutative
 * -  Associative
 * -  Distributive over AND
 * -  ⊥ as identity
 * -  Dominated by ⊤
 * -  Idempotent
 * -  Connecting complement results in tautology
 * -  More strict term is absorbed (A ∨ (A ∧ B) simplifies to A)
 * 
 * Commonly written "∨" ("⋁" if n-ary), "|", or "+"
 * 
 * @param   xs  `NULL`-terminated list of sentences that should be
 *              joined by the connective OR; this can be any number
 *              of arguments, even none; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_OR
 * @seealso  libnormalform_or_checked
 * @seealso  libnormalform_orl_checked
 * @seealso  libnormalform_vor_checked
 * @seealso  libnormalform_orl
 * @seealso  libnormalform_vor
 * @seealso  libnormalform_or2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_or)(LIBNORMALFORM_SENTENCE **xs);


/**
 * XOR: Exclusive disjunction
 * 
 * Also known as EOR, EXOR, NEQ, NIFF, Parity (especially when n-ary),
 * Exclusive alternation, Exclusive or, Logical non-equivalence,
 * Logical non-equivalence, Logical inequality, Not if and only if,
 * or Unless and only unless
 * 
 * An odd number of conditions must be met
 * 
 * 0 ⊕ 0 = 0
 * 0 ⊕ 1 = 1
 * 1 ⊕ 0 = 1
 * 1 ⊕ 1 = 0
 * 
 * Properties:
 * -  Vacuous falsity
 * -  Identity singleton
 * -  Commutative
 * -  Associative
 * -  ⊥ as identity
 * -  Complemented by ⊤
 * -  Annihiliation by reflextion
 * -  Connecting complement results in tautology
 * -  A ⊕ B is reduced to (A ∨ B) ∧ (¬A ∨ ¬B) or
 *    (A ∧ ¬B) ∨ (¬A ∧ B) in negation normal form
 * 
 * Commonly written "⊕" ("⨁" if n-ary), "⊻", "↮", "⇎", "≢", or "^"
 * 
 * Note that the name Exclusive disjunction is misleading
 * when there are more than two terms, as the statement
 * will not check that exactly one term is true, but rather
 * calculate the parity of the terms.
 * 
 * @param   xs  `NULL`-terminated list of sentences that should be
 *              joined by the connective XOR; this can be any number
 *              of arguments, even none; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_XOR
 * @seealso  libnormalform_xor_checked
 * @seealso  libnormalform_xorl_checked
 * @seealso  libnormalform_vxor_checked
 * @seealso  libnormalform_xorl
 * @seealso  libnormalform_vxor
 * @seealso  libnormalform_xor2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_xor)(LIBNORMALFORM_SENTENCE **xs);


/**
 * IF: Converse implication
 * 
 * Also known as Converse conditional
 * 
 * Creates a chain where any condition must be at least
 * as satisfied as the condition left to it (xs[0] ≤ xs[1])
 * (Not xs[1] without xs[0]); it is false only when only
 * the left-most term is false
 * 
 * 0 ← 0 = 1
 * 0 ← 1 = 0
 * 1 ← 0 = 1
 * 1 ← 1 = 1
 * 
 * Properties:
 * -  Identity singleton
 * -  Non-commutative
 * -  Left-associative: A ← B ← C = (A ← B) ← C ≠ A ← (B ← C)
 * -  Complemented by left ⊥
 * -  Dominated by left ⊤
 * -  Right falsity results in tautology
 * -  ⊤ as right identity
 * -  Contrapositivity: A ← B = ¬B ← ¬A
 * -  Transitive: (A ← B) ∧ (B ← C) ⊨ A ← C
 * -  Reflexive: A ← A = ⊤
 * -  Complete: (A ← B) ∨ (B ← A) = ⊤
 * -  Excluded middle: (A ← B) ∨ (¬A ← B) = ⊤
 * -  Import-export: (A ← B) ← C = A ← (B ∧ C)
 * -  Commutativity of antecedents: (A ← B) ← C = (A ← C) ← B
 * -  Vacuous conditional: ¬A ⊨ B ← A
 * -  Antecedent strengthening: A ← B ⊨ A ← (B ∧ C)
 * -  Right-distributive: (A ← B) ← C = (A ← C) ← (B ← C)
 * -  Distributive over left AND
 * -  Distributive over left OR
 * -  Distributing over right AND changes AND to OR
 * -  Distributing over right OR changes OR to AND
 * -  A ← B is reduced to A ∨ ¬B in negation normal form
 * 
 * Commonly written "←", "⇐", "<-", "<=", "≤", "⩽", or "⊂"
 * 
 * @param   xs  `NULL`-terminated list of sentences that should be
 *              joined by the connective IF; this can be any positive
 *              number of arguments; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * @throws  EDOM    `xs` contains no term (but only `NULL`)
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_IF
 * @seealso  libnormalform_if_checked
 * @seealso  libnormalform_ifl_checked
 * @seealso  libnormalform_vif_checked
 * @seealso  libnormalform_ifl
 * @seealso  libnormalform_vif
 * @seealso  libnormalform_if2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_if)(LIBNORMALFORM_SENTENCE **xs);


/**
 * IMPLY: Material implication
 * 
 * Also known as IMPLIES, IF..THEN, NOT..WITHOUT or material conditional
 * 
 * Creates a chain where any condition must be at most
 * as satisfied as the condition left to it (xs[0] ≥ xs[1])
 * (Not xs[0] without xs[1]); it is false only when only
 * the right-most term is false
 * 
 * 0 → 0 = 1
 * 0 → 1 = 1
 * 1 → 0 = 0
 * 1 → 1 = 1
 * 
 * Properties:
 * -  Vacuous truth
 * -  Identity singleton
 * -  Non-commutative
 * -  Right-associative: A → B → C = A → (B → C) ≠ (A → B) → C
 * -  Complemented by right ⊥
 * -  Dominated by right ⊤
 * -  Left falsity results in tautology
 * -  ⊤ as left identity
 * -  Contrapositivity: A → B = ¬B → ¬A
 * -  Transitive: (A → B) ∧ (B → C) ⊨ A → C
 * -  Reflexive: A → A = ⊤
 * -  Complete: (A → B) ∨ (B → A) = ⊤
 * -  Excluded middle: (A → B) ∨ (A → ¬B) = ⊤
 * -  Import-export: A → (B → C) = (A ∧ B) → C
 * -  Commutativity of antecedents: A → (B → C) = B → (A → C)
 * -  Vacuous conditional: ¬A ⊨ A → B
 * -  Antecedent strengthening: A → B ⊨ (A ∧ C) → B
 * -  Left-distributive: A → (B → C) = (A → B) → (A → C)
 * -  Distributive over right AND
 * -  Distributive over right OR
 * -  Distributing over left AND changes AND to OR
 * -  Distributing over left OR changes OR to AND
 * -  A → B is reduced to ¬A ∨ B in negation normal form
 * 
 * Commonly written "→", "⇒", "->", "=>", ">=", "≥", "⩾", or "⊃"
 * 
 * @param   xs  `NULL`-terminated list of sentences that should
 *              be joined by the connective IMPLY; this can be any
 *              number of arguments; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_IMPLY
 * @seealso  libnormalform_imply_checked
 * @seealso  libnormalform_implyl_checked
 * @seealso  libnormalform_vimply_checked
 * @seealso  libnormalform_implyl
 * @seealso  libnormalform_vimply
 * @seealso  libnormalform_imply2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_imply)(LIBNORMALFORM_SENTENCE **xs);


/**
 * NAND: Alternative denial
 * 
 * Also known as Non-conjunction, Negated conjunction,
 * Mutual exclusion, or Sheffer stroke
 * 
 * Creates a left-associated NAND-chain; in NAND, the
 * two conditions must not be met at the same time
 * 
 * 0 ⊼ 0 = 1
 * 0 ⊼ 1 = 1
 * 1 ⊼ 0 = 1
 * 1 ⊼ 1 = 0
 *
 * There is no good interpretation for a NAND-chain
 * 
 * Commonly written "⊼", "↑", or as AND with the expression over-struck
 * 
 * Properties:
 * -  Identity singleton
 * -  Commutative (however A ⊼ B ⊼ C ≠ A ⊼ C ⊼ B due to non-associativity)
 * -  Left-associative: A ⊼ B ⊼ C = (A ⊼ B) ⊼ C ≠ A ⊼ (B ⊼ C)
 * -  Antireflexive: A ⊼ A = ⊥
 * -  Annihilated by ⊥: A ⊼ ⊥ = ⊤
 * -  Complemented by ⊤
 * -  Distributative over AND
 * -  A ⊼ B is reduced to ¬A ∨ ¬B in negation normal form
 * 
 * @param   xs  `NULL`-terminated list of sentences that should be
 *              joined by the connective NAND; this can be any positive
 *              number of arguments; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * @throws  EDOM    `xs` contains no term (but only `NULL`)
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_NAND
 * @seealso  libnormalform_nand_checked
 * @seealso  libnormalform_nandl_checked
 * @seealso  libnormalform_vnand_checked
 * @seealso  libnormalform_nandl
 * @seealso  libnormalform_vnand
 * @seealso  libnormalform_nand2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_nand)(LIBNORMALFORM_SENTENCE **xs);


/**
 * NOR: Joint denial
 * 
 * Also known as Non-disjunction, Negated disjunction, Peirce arrow,
 * Quine dagger, or Webb operator
 * 
 * Creates a left-associated NOR-chain; in NOR, the
 * two conditions must be unmet at same time
 * 
 * 0 ⊽ 0 = 1
 * 0 ⊽ 1 = 0
 * 1 ⊽ 0 = 0
 * 1 ⊽ 1 = 0
 * 
 * There is no good interpretation for a NOR-chain
 * 
 * Commonly written "⊽", "↓", or as OR with the expression over-struck
 * 
 * Properties:
 * -  Identity singleton
 * -  Commutative (however A ⊽ B ⊽ C ≠ A ⊽ C ⊽ B due to non-associativity)
 * -  Left-associative: A ⊽ B ⊽ C = (A ⊽ B) ⊽ C ≠ A ⊽ (B ⊽ C)
 * -  Anti-idempotent: A ⊽ A = ¬A
 * -  Annihilated by ⊤: A ⊽ ⊤ = ⊥
 * -  Complemented by ⊤
 * -  Distributing over AND changes AND to OR
 * -  Distributing over OR changes OR to AND
 * -  A ⊽ B is reduced to ¬A ∧ ¬B in negation normal form
 * 
 * @param   xs  `NULL`-terminated list of sentences that should be
 *              joined by the connective NOR; this can be any positive
 *              number of arguments; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * @throws  EDOM    `xs` contains no term (but only `NULL`)
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_NOR
 * @seealso  libnormalform_nor_checked
 * @seealso  libnormalform_norl_checked
 * @seealso  libnormalform_vnor_checked
 * @seealso  libnormalform_norl
 * @seealso  libnormalform_vnor
 * @seealso  libnormalform_nor2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_nor)(LIBNORMALFORM_SENTENCE **xs);


/**
 * XNOR: Logical bicondition
 * 
 * Also known as ENOR, EXNOR, NXOR, XAND, EQ, IFF, Exclusive NOR,
 * Material biconditional, Logical equivalence, Biimplication,
 * Bientailment, If and only if, Negated XOR, or Exclusive non-disjunction
 * 
 * Creates a left-associated XNOR-chain; in XNOR, the
 * two conditions must equally true
 * 
 * 0 ⊙ 0 = 1
 * 0 ⊙ 1 = 0
 * 1 ⊙ 0 = 0
 * 1 ⊙ 1 = 1
 * 
 * The interpretation of a XNOR-chain depends on it's length,
 * if it's length is even, is equivalent to XOR, otherwise,
 * it's its complement
 * 
 * Commonly written "⊙" ("⨀" if n-ary), "↔", "⇔", "≡", "==", or
 * as XOR with the expression over-struck
 * 
 * Properties:
 * -  Vacuous truth
 * -  Identity singleton
 * -  Commutative
 * -  Associative
 * -  ⊤ as identity
 * -  Complemented by ⊥
 * -  Reflexive: A ⊙ A = ⊤
 * -  Annihilated by ⊤: A ⊽ ⊤ = ⊥
 * -  Connecting complement results in contradiction
 * -  A ⊙ B is reduced to (A ∨ ¬B) ∧ (¬A ∨ B) or
 *    (A ∧ B) ∨ (¬A ∧ ¬B) in negation normal form
 * 
 * @param   xs  `NULL`-terminated list of sentences that should
 *              be joined by the connective XNOR; this can be any
 *              number of arguments; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_NXOR
 * @seealso  libnormalform_nxor_checked
 * @seealso  libnormalform_nxorl_checked
 * @seealso  libnormalform_vxnor_checked
 * @seealso  libnormalform_xnorl
 * @seealso  libnormalform_vxnor
 * @seealso  libnormalform_xnor2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_xnor)(LIBNORMALFORM_SENTENCE **xs);


/**
 * NIF: Converse nonimplication
 * 
 * Also known as NOT..BUT, Converse abjunction
 * 
 * Creates a chain where any condition must be less
 * satisfied than the condition left to it (xs[0] > xs[1])
 * 
 * 0 ↚ 0 = 0
 * 0 ↚ 1 = 1
 * 1 ↚ 0 = 0
 * 1 ↚ 1 = 0
 * 
 * Properties:
 * -  Vacuous falsity
 * -  Identity singleton
 * -  Non-commutative
 * -  Left-associative: A ↚ B ↚ C = (A ↚ B) ↚ C ≠ A ↚ (B ↚ C)
 * -  Complemented by right ⊤
 * -  Dominated by right ⊥
 * -  Left truth results in contradiction
 * -  ⊥ as left identity
 * -  Contrapositivity: A ↚ B = ¬B ↚ ¬A
 * -  Antireflexive: A ↚ A = ⊥
 * -  Left-distributive: A ↚ (B ↚ C) = (A ↚ B) ↚ (A ↚ C)
 * -  Distributive over right AND
 * -  Distributive over right OR
 * -  Distributing over left AND changes AND to OR
 * -  Distributing over left OR changes OR to AND
 * -  A ↚ B is reduced to ¬A ∧ B in negation normal form
 * 
 * Commonly written "↚", "⇍", "!<-", "<-~", "</-", "!<=", "<=~", "</=", "⊄", "⭉" (or "←̃"), or ">"
 * 
 * @param   xs  `NULL`-terminated list of sentences that should be
 *              joined by the connective NIF; this can be any number
 *              of arguments, even none; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_NIF
 * @seealso  libnormalform_nif_checked
 * @seealso  libnormalform_nifl_checked
 * @seealso  libnormalform_vnif_checked
 * @seealso  libnormalform_nifl
 * @seealso  libnormalform_vnif
 * @seealso  libnormalform_nif2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_nif)(LIBNORMALFORM_SENTENCE **xs);


/**
 * NIMPLY: Material nonimplication
 * 
 * Also known as NIMPLIES, BUT NOT or Material abjunction
 * 
 * Creates a chain where any condition must be more
 * satisfied than the condition left to it (xs[0] < xs[1])
 * 
 * 0 ↛ 0 = 0
 * 0 ↛ 1 = 0
 * 1 ↛ 0 = 1
 * 1 ↛ 1 = 0
 * 
 * Properties:
 * -  Identity singleton
 * -  Non-commutative
 * -  Right-associative: A ↛ B ↛ C = A ↛ (B ↛ C) ≠ (A ↛ B) → C
 * -  Complemented by left ⊤
 * -  Dominated by left ⊥
 * -  Right truth results in contradiction
 * -  ⊥ as right identity
 * -  Contrapositivity: A ↛ B = ¬B ↛ ¬A
 * -  Antireflexive: A ↛ A = ⊥
 * -  Right-distributive: (A ↛ B) ↛ C = (A ↛ C) ↛ (B → C)
 * -  Distributive over left AND
 * -  Distributive over left OR
 * -  Distributing over right AND changes AND to OR
 * -  Distributing over right OR changes OR to AND
 * -  A ↛ B is reduced to A ∧ ¬B in negation normal form
 * 
 * Commonly written "↛", "⇏", "!->", "->~", "-/>", "!=>", "=>~", "=/>", "⊅", "⥲" (or "→̃"), or "<"
 * 
 * @param   xs  `NULL`-terminated list of sentences that should be
 *              joined by the connective NIMPLY; this can be any positive
 *              number of arguments; ownership of object in the array
 *              (but not the array itself) is transfered to this function
 * @return      The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * @throws  EDOM    `xs` contains no term (but only `NULL`)
 * 
 * Ownership is always transfered, even on failure
 * 
 * @seealso  LIBNORMALFORM_NIMPLY
 * @seealso  libnormalform_nimply_checked
 * @seealso  libnormalform_nimplyl_checked
 * @seealso  libnormalform_vnimply_checked
 * @seealso  libnormalform_nimplyl
 * @seealso  libnormalform_vnimply
 * @seealso  libnormalform_nimply2
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
LIBNORMALFORM_SENTENCE *(libnormalform_nimply)(LIBNORMALFORM_SENTENCE **xs);





/**
 * THERE EXISTS: Existential quantification (unmapped)
 * 
 * The predicate must be met for at least one element;
 * if no element exists, the sentence is false
 * 
 * Commonly written "∃" ("∃x∈d.k", "∃x∈d k(x)", or "∃ x∈d : k(x)")
 * 
 * The predicate is tested on `.key` in each element
 * in the domain, and `.value` is unused
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   k  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `k` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `k` to
 * be `NULL`)
 * 
 * @seealso  libnormalform_any
 * @seealso  libnormalform_existentially
 * @seealso  libnormalform_nexists
 * @seealso  libnormalform_unique
 * @seealso  libnormalform_nonempty
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_exists)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k)
{ return libnormalform_any(d, k, libnormalform_true()); }


/**
 * THERE EXISTS NO: Negated existential quantification (unmapped)
 * 
 * The predicate must be unmet for every element;
 * if no element exists, the sentence is true
 * 
 * Commonly written "∄" ("∄x∈d.k", "∄x∈d k(x)", or "∄ x∈d : k(x)"),
 * "~∃", "¬∃", or as THERE EXISTS with overline
 * 
 * The predicate is tested on `.key` in each element
 * in the domain, and `.value` is unused
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   k  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `k` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `k` to
 * be `NULL`)
 * 
 * @seealso  libnormalform_all
 * @seealso  libnormalform_exists
 * @seealso  libnormalform_empty
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nexists)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k)
{ return libnormalform_all(d, k, libnormalform_false()); }


/**
 * THERE EXISTS ONE: Unique existential quantification (unmapped)
 * 
 * The predicate must be met for exactly one element;
 * if no element exists, the sentence is false
 * 
 * Commonly written "∃!" ("∃!x∈d.k", "∃!x∈d k(x)", or "∃! x∈d : k(x)")
 * 
 * The predicate is tested on `.key` in each element
 * in the domain, and `.value` is unused
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   k  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `k` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `k` to
 * be `NULL`)
 * 
 * @seealso  libnormalform_one
 * @seealso  libnormalform_uniquely
 * @seealso  libnormalform_exists
 * @seealso  libnormalform_singleton
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_unique)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *k)
{ return libnormalform_one(d, k, libnormalform_true()); }





/**
 * SOMEWHERE: Existential quantification (premapped)
 * 
 * The predicate must be met for at least one element;
 * if no element exists, the sentence is false
 * 
 * Commonly written "∃" ("∃x∈d.v", "∃x∈d v(x)", or "v(x) ∃ x∈d")
 * 
 * The predicate is tested on `.value` in each element
 * in the domain, and `.key` is unused
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   v  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `v` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `v` to
 * be `NULL`)
 * 
 * @seealso  libnormalform_any
 * @seealso  libnormalform_exists
 * @seealso  libnormalform_universally
 * @seealso  libnormalform_uniquely
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_existentially)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v)
{ return libnormalform_any(d, libnormalform_true(), v); }


/**
 * EVERYWHERE: Universal quantification (premapped)
 * 
 * The predicate must be unmet for every element;
 * if no element exists, the sentence is true
 * 
 * Commonly written "∀" ("∀x∈d.v", "∀x∈d v(x)", or "v(x) ∀ x∈d")
 * 
 * The predicate is tested on `.value` in each element
 * in the domain, and `.key` is unused
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   v  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `v` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `v` to
 * be `NULL`)
 * 
 * @seealso  libnormalform_all
 * @seealso  libnormalform_existentially
 * @seealso  libnormalform_uniquely
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_universally)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v)
{ return libnormalform_all(d, libnormalform_true(), v); }


/**
 * ONEWHERE: Unique existential quantification (premapped)
 * 
 * The predicate must be met for exactly one element;
 * if no element exists, the sentence is false
 * 
 * Commonly written "∃!" ("∃!x∈d.v", "∃!x∈d v(x)", or "v(x) ∃! x∈d")
 * 
 * The predicate is tested on `.value` in each element
 * in the domain, and `.key` is unused
 * 
 * @param   d  The domain of interest; ownership is retained by the caller
 * @param   v  The predicate; ownership is transfered to this function
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `v` is `NULL`, this function will return `NULL`
 * (indicating failure) without modified `errno` (expecting
 * it to be set by a function that failed, causing `v` to
 * be `NULL`)
 * 
 * @seealso  libnormalform_one
 * @seealso  libnormalform_unique
 * @seealso  libnormalform_existentially
 * @seealso  libnormalform_universially
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_uniquely)(struct libnormalform_map *d, LIBNORMALFORM_SENTENCE *v)
{ return libnormalform_one(d, libnormalform_true(), v); }





/**
 * Create a sentence that checks whether a set is empty
 *
 * The sentence technically classifies as a qualification
 * 
 * Commonly written "X=∅" or "|X|=0"
 * 
 * @param   d  The set; ownership is retained by the caller
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * @seealso  libnormalform_nonempty
 * @seealso  libnormalform_singleton
 * @seealso  libnormalform_nexists
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_empty)(struct libnormalform_map *d)
{ return libnormalform_all(d, libnormalform_true(), libnormalform_false()); }


/**
 * Create a sentence that checks whether a set is non-empty
 *
 * The sentence technically classifies as a qualification
 * 
 * Commonly written "X≠∅", "X⊃∅", "X⊋∅" "|X|≠0", or "|X|>0"
 * 
 * @param   d  The set; ownership is retained by the caller
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * @seealso  libnormalform_empty
 * @seealso  libnormalform_singleton
 * @seealso  libnormalform_exists
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nonempty)(struct libnormalform_map *d)
{ return libnormalform_any(d, libnormalform_true(), libnormalform_true()); }


/**
 * Create a sentence that checks whether a set is a singleton
 * (contains exactly one element)
 *
 * The sentence technically classifies as a qualification
 * 
 * Commonly written "|X|=1", "∃! x : X={x}", "X={x} ∃! x", or just "X={x}"
 * 
 * @param   d  The set; ownership is retained by the caller
 * @return     The constructed sentence, `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * @seealso  libnormalform_empty
 * @seealso  libnormalform_nonempty
 * @seealso  libnormalform_unique
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_singleton)(struct libnormalform_map *d)
{ return libnormalform_one(d, libnormalform_true(), libnormalform_true()); }





/**
 * Variant of `libnormalform_and` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_and`
 * @return      See `libnormalform_and`
 * @throws      See `libnormalform_and`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_and_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(and) }


/**
 * Variant of `libnormalform_or` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_or`
 * @return      See `libnormalform_or`
 * @throws      See `libnormalform_or`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_or_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(or) }


/**
 * Variant of `libnormalform_xor` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_xor`
 * @return      See `libnormalform_xor`
 * @throws      See `libnormalform_xor`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_xor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(xor) }


/**
 * Variant of `libnormalform_if` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_if`
 * @return      See `libnormalform_if`
 * @throws      See `libnormalform_if`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_if_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(if) }


/**
 * Variant of `libnormalform_imply` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_imply`
 * @return      See `libnormalform_imply`
 * @throws      See `libnormalform_imply`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_imply_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(imply) }


/**
 * Variant of `libnormalform_nand` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_nand`
 * @return      See `libnormalform_nand`
 * @throws      See `libnormalform_nand`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nand_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(nand) }


/**
 * Variant of `libnormalform_nor` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_nor`
 * @return      See `libnormalform_nor`
 * @throws      See `libnormalform_nor`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(nor) }


/**
 * Variant of `libnormalform_xnor` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_xnor`
 * @return      See `libnormalform_xnor`
 * @throws      See `libnormalform_xnor`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_xnor_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(xnor) }


/**
 * Variant of `libnormalform_nif` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_nif`
 * @return      See `libnormalform_nif`
 * @throws      See `libnormalform_nif`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nif_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(nif) }


/**
 * Variant of `libnormalform_nimply` that checks
 * for unexpected `NULL` input
 *
 * @param   n   The number of expected non-`NULL` terms
 * @param   xs  See `libnormalform_nimply`
 * @return      See `libnormalform_nimply`
 * @throws      See `libnormalform_nimply`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NONNULL_INPUT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nimply_checked)(size_t n, LIBNORMALFORM_SENTENCE **xs)
{ LIBNORMALFORM_CHECKED__(nimply) }





/**
 * Variant of `libnormalform_andl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_andl`
 * @throws           See `libnormalform_andl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vand)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(and) }


/**
 * Variant of `libnormalform_orl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_orl`
 * @throws           See `libnormalform_orl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vor)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(or) }


/**
 * Variant of `libnormalform_xorl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_xorl`
 * @throws           See `libnormalform_xorl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vxor)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(xor) }


/**
 * Variant of `libnormalform_ifl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_ifl`
 * @throws           See `libnormalform_ifl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vif)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(if) }


/**
 * Variant of `libnormalform_implyl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_implyl`
 * @throws           See `libnormalform_implyl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vimply)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(imply) }


/**
 * Variant of `libnormalform_nandl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_nandl`
 * @throws           See `libnormalform_nandl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vnand)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(nand) }


/**
 * Variant of `libnormalform_norl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_norl`
 * @throws           See `libnormalform_norl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vnor)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(nor) }


/**
 * Variant of `libnormalform_xnorl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_xnorl`
 * @throws           See `libnormalform_xnorl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vxnor)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(xnor) }


/**
 * Variant of `libnormalform_nifl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_nifl`
 * @throws           See `libnormalform_nifl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vnif)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(nif) }


/**
 * Variant of `libnormalform_nimplyl` that uses `va_list`
 * instead of variadic arguments
 * 
 * @param   a, args  `NULL`-terminated list of terms; the function
 *                   will take ownership of each input reference,
 *                   so the caller shall not attempt to deallocate
 *                   or use them again.
 * @return           See `libnormalform_nimplyl`
 * @throws           See `libnormalform_nimplyl`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vnimply)(LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST__(nimply) }





/**
 * Variant of `libnormalform_and` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_and`
 * @throws          See `libnormalform_and`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_andl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(and) }


/**
 * Variant of `libnormalform_or` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_or`
 * @throws          See `libnormalform_or`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_orl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(or) }


/**
 * Variant of `libnormalform_xor` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_xor`
 * @throws          See `libnormalform_xor`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_xorl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(xor) }


/**
 * Variant of `libnormalform_if` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_if`
 * @throws          See `libnormalform_if`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_ifl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(if) }


/**
 * Variant of `libnormalform_imply` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_imply`
 * @throws          See `libnormalform_imply`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_implyl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(imply) }


/**
 * Variant of `libnormalform_nand` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_nand`
 * @throws          See `libnormalform_nand`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nandl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(nand) }


/**
 * Variant of `libnormalform_nor` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_nor`
 * @throws          See `libnormalform_nor`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_norl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(nor) }


/**
 * Variant of `libnormalform_xnor` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_xnor`
 * @throws          See `libnormalform_xnor`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_xnorl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(xnor) }


/**
 * Variant of `libnormalform_nif` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_nif`
 * @throws          See `libnormalform_nif`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nifl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(nif) }


/**
 * Variant of `libnormalform_nimply` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_nimply`
 * @throws          See `libnormalform_nimply`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nimplyl)(LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS__(nimply) }





/**
 * Variant of `libnormalform_vand` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vand`
 * @return           See `libnormalform_vand`
 * @throws           See `libnormalform_vand`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vand_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(and) }


/**
 * Variant of `libnormalform_vor` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vor`
 * @return           See `libnormalform_vor`
 * @throws           See `libnormalform_vor`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(or) }


/**
 * Variant of `libnormalform_vxor` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vxor`
 * @return           See `libnormalform_vxor`
 * @throws           See `libnormalform_vxor`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vxor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(xor) }


/**
 * Variant of `libnormalform_vif` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vif`
 * @return           See `libnormalform_vif`
 * @throws           See `libnormalform_vif`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vif_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(if) }


/**
 * Variant of `libnormalform_vimply` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vimply`
 * @return           See `libnormalform_vimply`
 * @throws           See `libnormalform_vimply`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vimply_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(imply) }


/**
 * Variant of `libnormalform_vnand` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vnand`
 * @return           See `libnormalform_vnand`
 * @throws           See `libnormalform_vnand`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vnand_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(nand) }


/**
 * Variant of `libnormalform_vnor` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vnor`
 * @return           See `libnormalform_vnor`
 * @throws           See `libnormalform_vnor`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vnor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(nor) }


/**
 * Variant of `libnormalform_vxnor` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vxnor`
 * @return           See `libnormalform_vxnor`
 * @throws           See `libnormalform_vxnor`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vxnor_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(xnor) }


/**
 * Variant of `libnormalform_vnif` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vnif`
 * @return           See `libnormalform_vnif`
 * @throws           See `libnormalform_vnif`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vnif_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(nif) }


/**
 * Variant of `libnormalform_vnimply` that checks
 * for unexpected `NULL` input
 *
 * @param   n        The number of expected non-`NULL` terms
 * @param   a, args  See `libnormalform_vnimply`
 * @return           See `libnormalform_vnimply`
 * @throws           See `libnormalform_vnimply`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_vnimply_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, va_list args)
{ LIBNORMALFORM_VALIST_CHECKED__(nimply) }





/**
 * Variant of `libnormalform_andl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_andl`
 * @return          See `libnormalform_andl`
 * @throws          See `libnormalform_andl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_andl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(and) }


/**
 * Variant of `libnormalform_orl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_orl`
 * @return          See `libnormalform_orl`
 * @throws          See `libnormalform_orl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_orl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(or) }


/**
 * Variant of `libnormalform_xorl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_xorl`
 * @return          See `libnormalform_xorl`
 * @throws          See `libnormalform_xorl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_xorl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(xor) }


/**
 * Variant of `libnormalform_ifl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_ifl`
 * @return          See `libnormalform_ifl`
 * @throws          See `libnormalform_ifl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_ifl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(if) }


/**
 * Variant of `libnormalform_implyl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_implyl`
 * @return          See `libnormalform_implyl`
 * @throws          See `libnormalform_implyl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_implyl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(imply) }


/**
 * Variant of `libnormalform_nandl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_nandl`
 * @return          See `libnormalform_nandl`
 * @throws          See `libnormalform_nandl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nandl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nand) }


/**
 * Variant of `libnormalform_norl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_norl`
 * @return          See `libnormalform_norl`
 * @throws          See `libnormalform_norl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_norl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nor) }


/**
 * Variant of `libnormalform_xnorl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_xnorl`
 * @return          See `libnormalform_xnorl`
 * @throws          See `libnormalform_xnorl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_xnorl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(xnor) }


/**
 * Variant of `libnormalform_nifl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_nifl`
 * @return          See `libnormalform_nifl`
 * @throws          See `libnormalform_nifl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nifl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nif) }


/**
 * Variant of `libnormalform_nimplyl` that checks
 * for unexpected `NULL` input
 *
 * @param   n       The number of expected non-`NULL` terms
 * @param   a, ...  See `libnormalform_nimplyl`
 * @return          See `libnormalform_nimplyl`
 * @throws          See `libnormalform_nimplyl`
 * 
 * If the function finds any unexpected `NULL` terms,
 * it will call `libnormalform_free` on all non-`NULL` terms
 * and return `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_NULL_LAST__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nimplyl_checked)(size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{ LIBNORMALFORM_ELLIPSIS_CHECKED__(nimply) }





/**
 * Variant of `libnormalform_and` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_and`
 * @throws     See `libnormalform_and`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
LIBNORMALFORM_SENTENCE *(libnormalform_and2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);


/**
 * Variant of `libnormalform_or` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_or`
 * @throws     See `libnormalform_or`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
LIBNORMALFORM_SENTENCE *(libnormalform_or2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);


/**
 * Variant of `libnormalform_xor` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_xor`
 * @throws     See `libnormalform_xor`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
LIBNORMALFORM_SENTENCE *(libnormalform_xor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);


/**
 * Variant of `libnormalform_if` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_if`
 * @throws     See `libnormalform_if`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_if2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{ LIBNORMALFORM_TWO__(if) }


/**
 * Variant of `libnormalform_imply` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_imply`
 * @throws     See `libnormalform_imply`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_imply2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{ LIBNORMALFORM_TWO__(imply) }


/**
 * Variant of `libnormalform_nand` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_nand`
 * @throws     See `libnormalform_nand`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nand2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{ LIBNORMALFORM_TWO__(nand) }


/**
 * Variant of `libnormalform_nor` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_nor`
 * @throws     See `libnormalform_nor`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{ LIBNORMALFORM_TWO__(nor) }


/**
 * Variant of `libnormalform_xnor` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_xnor`
 * @throws     See `libnormalform_xnor`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_xnor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{ LIBNORMALFORM_TWO__(xnor) }


/**
 * Variant of `libnormalform_nif` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_nif`
 * @throws     See `libnormalform_nif`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nif2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{ LIBNORMALFORM_TWO__(nif) }


/**
 * Variant of `libnormalform_nimply` that takes exactly two terms
 *
 * @param   l  The left-hand term
 * @param   r  The right-hand term
 * @return     See `libnormalform_nimply`
 * @throws     See `libnormalform_nimply`
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
LIBNORMALFORM_USE_RESULT__
inline LIBNORMALFORM_SENTENCE *
(libnormalform_nimply2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r)
{ LIBNORMALFORM_TWO__(nimply) }





/* These are macro versions of function with the same name */

/**
 * Variant of `libnormalform_and` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_and`
 * @throws          See `libnormalform_and`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_andl(...) (libnormalform_and((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_or` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_or`
 * @throws          See `libnormalform_or`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_orl(...) (libnormalform_or((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_xor` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_xor`
 * @throws          See `libnormalform_xor`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_xorl(...) (libnormalform_xor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_if` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_if`
 * @throws          See `libnormalform_if`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_ifl(...) (libnormalform_if((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_imply` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_imply`
 * @throws          See `libnormalform_imply`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_implyl(...) (libnormalform_imply((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_nand` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_nand`
 * @throws          See `libnormalform_nand`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_nandl(...) (libnormalform_nand((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_nor` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_nor`
 * @throws          See `libnormalform_nor`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_norl(...) (libnormalform_nor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_xnor` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_xnor`
 * @throws          See `libnormalform_xnor`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_xnorl(...) (libnormalform_xnor((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_nif` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_nif`
 * @throws          See `libnormalform_nif`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_nifl(...) (libnormalform_nif((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))


/**
 * Variant of `libnormalform_nimply` that uses variadic arguments
 * 
 * @param   a, ...  `NULL`-terminated list of terms; the function
 *                  will take ownership of each input reference,
 *                  so the caller shall not attempt to deallocate
 *                  or use them again.
 * @return          See `libnormalform_nimply`
 * @throws          See `libnormalform_nimply`
 * 
 * Be careful not in inputing any `NULL` apart from
 * the list terminator as the function will not be
 * able to see them.
 */
#define libnormalform_nimplyl(...) (libnormalform_nimply((LIBNORMALFORM_SENTENCE *[]){__VA_ARGS__}))





/**
 * Macro variant of `libnormalform_andl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_andl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_AND(...) LIBNORMALFORM_MACRO__(and, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_orl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_orl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_OR(...) LIBNORMALFORM_MACRO__(or, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_xorl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_xorl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_XOR(...) LIBNORMALFORM_MACRO__(xor, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_ifl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_ifl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_IF(...) LIBNORMALFORM_MACRO__(if, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_implyl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_implyl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_IMPLY(...) LIBNORMALFORM_MACRO__(imply, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_nandl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_nandl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_NAND(...) LIBNORMALFORM_MACRO__(nand, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_norl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_norl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_NOR(...) LIBNORMALFORM_MACRO__(nor, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_xnorl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_xnorl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_XNOR(...) LIBNORMALFORM_MACRO__(xnor, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_nifl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_nifl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_NIF(...) LIBNORMALFORM_MACRO__(nif, __VA_ARGS__)


/**
 * Macro variant of `libnormalform_nimplyl_checked`, that
 * will add the `NULL` to the end of the list and, before
 * the list, the number of terms in the list
 * 
 * @param   ...  List of terms, _without_ `NULL`-terinator
 * @return       See `libnormalform_nimplyl_checked`
 *
 * Either any argument is `NULL`, `libnormalform_free` on
 * will be called for all non-`NULL` terms, the `NULL`
 * with be return (indicating failure) without `errno`
 * being modified (it is expected to already be set in
 * indicate the error that caused one of the terms to be
 * `NULL`)
 */
#define LIBNORMALFORM_NIMPLY(...) LIBNORMALFORM_MACRO__(nimply, __VA_ARGS__)





#undef LIBNORMALFORM_CHECKED__
#undef LIBNORMALFORM_VALIST__
#undef LIBNORMALFORM_ELLIPSIS__
#undef LIBNORMALFORM_VALIST_CHECKED__
#undef LIBNORMALFORM_ELLIPSIS_CHECKED__
#undef LIBNORMALFORM_TWO__

#undef LIBNORMALFORM_USE_RESULT__
#undef LIBNORMALFORM_FREE_WITH__
#undef LIBNORMALFORM_USE_FREE__
#undef LIBNORMALFORM_NONNULL_INPUT__
#undef LIBNORMALFORM_ONE_NONNULL_INPUT__
#undef LIBNORMALFORM_NULL_LAST__


#if defined(__GNUC__)
# pragma GCC diagnostic pop
#endif

#endif