Second commitHEADmaster

Signed-off-by: Mattias Andrée <m@maandree.se>

1 files changed, 710 insertions, 126 deletions

diff --git a/libnormalform.h b/libnormalform.h
index ed3b256..c618485 100644
--- a/libnormalform.h
+++ b/libnormalform.h
@@ -10,6 +10,12 @@
 #if defined(__GNUC__)
 # pragma GCC diagnostic push
 # pragma GCC diagnostic ignored "-Winline"
+# pragma GCC diagnostic ignored "-Wpadded"
+# pragma GCC diagnostic ignored "-Wvla"
+# if defined(__clang__)
+#  pragma GCC diagnostic ignored "-Wdocumentation"
+#  pragma GCC diagnostic ignored "-Wunsafe-buffer-usage" /* clang is currently exceptionally stupid */
+# endif
 #endif
 
 
@@ -17,7 +23,11 @@
 
 #if defined(__GNUC__)
 # define LIBNORMALFORM_USE_RESULT__ __attribute__((__warn_unused_result__))
-# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) __attribute__((__malloc__(DESTRUCTOR)))
+# if defined(__clang__)
+#  define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR)
+# else
+#  define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) __attribute__((__malloc__(DESTRUCTOR)))
+# endif
 # define LIBNORMALFORM_USE_FREE__ __attribute__((__malloc__))
 # define LIBNORMALFORM_NONNULL_INPUT__ __attribute__((__nonnull__))
 # define LIBNORMALFORM_ONE_NONNULL_INPUT__(INDEX) __attribute__((__nonnull__(INDEX)))
@@ -148,8 +158,8 @@ struct libnormalform_term;
 #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_REDUCE_XOR                    (UINT64_C(1) <<  4) /**< Rewrite XOR to negation normal form */
+#define LIBNORMALFORM_RELAX_XOR                     (UINT64_C(1) <<  5) /**< Relax any non-reduce XOR to OR */
 #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)) */
@@ -166,7 +176,7 @@ struct libnormalform_term;
 #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_DISTRIBUTE_QUALIFIERS         (UINT64_C(1) << 21) /**< Duplicate qualifers to move out clauses */
 #define LIBNORMALFORM_ALL_EXPRESS_FLAGS__          ((UINT64_C(1) << 23) - 1U) /* For internal use */
 
 
@@ -183,81 +193,13 @@ 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_CONJUNCTION,            /**< AND clause; empty clause is used for tautology */
+	LIBNORMALFORM_DISJUNCTION,            /**< OR  clause; empty clause is used for contradiction */
 	LIBNORMALFORM_EXCLUSIVE_DISJUNCTION,  /**< XOR clause; never used for empty clauses */
 	LIBNORMALFORM_TRANSFORMATION,         /**< Transformater function with input **/
 	LIBNORMALFORM_VARIABLE,               /**< Positive variable literal **/
@@ -293,9 +235,19 @@ enum libnormalform_builtin_transformer {
 
 
 /**
+ * Boolean with possibly of being unknown
+ */
+enum libnormalform_ternary {
+	LIBNORMALFORM_NO,    /**< No/False */
+	LIBNORMALFORM_MAYBE, /**< Maybe/Unknown */
+	LIBNORMALFORM_YES    /**< Yes/True */
+};
+
+
+/**
  * Relationship (dependency) between the value of two sentences
  */
-enum libnormalform_sentences_relationship {
+enum libnormalform_sentence_relationship {
 	/**
 	 * Left-hand implies right-hand (⊨ P → Q)
 	 * 
@@ -718,7 +670,107 @@ enum libnormalform_domain_relationship {
          * -  ⋁A → ⋁B cannot be simplified
 	 * -  ⋁A ← ⋁B cannot be simplified
 	 */
-	LIBNORMALFORM_CONJOINT_WITH
+	LIBNORMALFORM_CONJOINT_WITH,
+
+	/**
+	 * Both sets have no formal relationship
+	 * 
+	 * 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_UNRELATED_TO
+};
+
+
+/**
+ * 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);
 };
 
 
@@ -1030,26 +1082,507 @@ struct libnormalform_map {
 };
 
 
-struct libnormalform_atom_comparsion {
+/**
+ * Variable/function (atom sentence) comparison results
+ */
+struct libnormalform_atom_comparison {
+	/**
+	 * The library will set this to the version of the `struct`
+	 * that it uses, but before returning, if and only if the
+	 * application uses an older version, it shall set the
+	 * version number here
+	 * 
+	 * Current version number is 1
+	 * 
+	 * @since  `.version == 1`
+	 */
 	int version;
-	enum libnormalform_sentences_relationship relationship;
+
+	/**
+	 * Output field for the dependency relationship
+	 * between the two atomic sentences
+	 * 
+	 * @since  `.version == 1`
+	 */
+	enum libnormalform_sentence_relationship relationship;
+
+	/**
+	 * The application can store any data here that will
+	 * be useful for it's callback functions stored in
+	 * the other fields
+	 * 
+	 * May be `NULL`, and initialised so by the library
+	 * 
+	 * @since  `.version == 1`
+	 */
+	void *user_data;
+
+	/**
+	 * Called with `.user_data` (even if `.user_data` is `NULL`)
+	 * before the library stops using the `struct`
+	 * 
+	 * May be `NULL`, and initialised so by the library
+	 * 
+	 * @param  user_data  `.user_data`
+	 * 
+	 * @since  `.version == 1`
+	 */
+	void (*release_user_data)(void *user_data);
+
+	/**
+	 * The library will call this function for every function,
+	 * that the library will not use, that the application in
+	 * one of the `struct`'s fields
+	 * 
+	 * May be `NULL`, and initialised so by the library
+	 * 
+	 * @param  function   The unused function
+	 * @param  user_data  `.user_data`
+	 * 
+	 * @since  `.version == 1`
+	 */
+	void (*dont_want_function)(struct libnormalform_function *function, void *user_data);
+
+	/**
+	 * The library will call this function for every variable,
+	 * that the library will not use, that the application in
+	 * one of the `struct`'s fields
+	 * 
+	 * May be `NULL`, and initialised so by the library
+	 * 
+	 * @param  variable   The unused variable
+	 * @param  user_data  `.user_data`
+	 * 
+	 * @since  `.version == 1`
+	 */
+	void (*dont_want_variable)(struct libnormalform_variable *variable, void *user_data);
+
+	/**
+	 * Set by the library to a hint to the application on
+	 * whether it would like to create a conjunction of
+	 * the two atomic sentences
+	 * 
+	 * @since  `.version == 1`
+	 */
+	enum libnormalform_ternary conjunction_is_useful;
+
+	/**
+	 * The library will set this field to `NULL`, but
+	 * if the application has created a conjunction
+	 * of the two atomic sentences, it should be stored
+	 * here, if the conjunction is a function
+	 * 
+	 * @since  `.version == 1`
+	 */
+	struct libnormalform_function *created_conjunction_as_function;
+
+	/**
+	 * The library will set this field to `NULL`, but if
+	 * the application is able to create a conjunction
+	 * of the two atomic sentences, it shall store a pointer
+	 * the a function for doing so in this field, if the
+	 * result will be a function
+	 * 
+	 * @param   left       The left-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the left-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   right      The right-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the right-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   out        Output parameter for the conjunction of the
+	 *                     two atomic sentences
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success if `*out` was created,
+	 *                     0 if it turned out that a conjunction could
+	 *                     not be constructed, -1 on failure
+	 * 
+	 * @since  `.version == 1`
+	 */
+	int (*create_conjunction_as_function)(void *left, void *right, struct libnormalform_function **out, void *user_data);
+
+	/**
+	 * The library will set this field to `NULL`, but
+	 * if the application has created a conjunction
+	 * of the two atomic sentences, it should be stored
+	 * here, if the conjunction is a variable
+	 * 
+	 * @since  `.version == 1`
+	 */
+	struct libnormalform_variable *created_conjunction_as_variable;
+
+	/**
+	 * The library will set this field to `NULL`, but if
+	 * the application is able to create a conjunction
+	 * of the two atomic sentences, it shall store a pointer
+	 * the a function for doing so in this field, if the
+	 * result will be a variable
+	 * 
+	 * @param   left       The left-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the left-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   right      The right-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the right-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   out        Output parameter for the conjunction of the
+	 *                     two atomic sentences
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success if `*out` was created,
+	 *                     0 if it turned out that a conjunction could
+	 *                     not be constructed, -1 on failure
+	 * 
+	 * @since  `.version == 1`
+	 */
+	int (*create_conjunction_as_variable)(void *left, void *right, struct libnormalform_variable **out, void *user_data);
+
+	/**
+	 * Set by the library to a hint to the application on
+	 * whether it would like to create a disjunction of
+	 * the two atomic sentences
+	 * 
+	 * @since  `.version == 1`
+	 */
+	enum libnormalform_ternary disjunction_is_useful;
+
+	/**
+	 * The library will set this field to `NULL`, but
+	 * if the application has created a disjunction
+	 * of the two atomic sentences, it should be stored
+	 * here, if the disjunction is a function
+	 * 
+	 * @since  `.version == 1`
+	 */
+	struct libnormalform_function *created_disjunction_as_function;
+
+	/**
+	 * The library will set this field to `NULL`, but if
+	 * the application is able to create a disjunction
+	 * of the two atomic sentences, it shall store a pointer
+	 * the a function for doing so in this field, if the
+	 * result will be a function
+	 * 
+	 * @param   left       The left-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the left-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   right      The right-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the right-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   out        Output parameter for the disjunction of the
+	 *                     two atomic sentences
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success if `*out` was created,
+	 *                     0 if it turned out that a disjunction could
+	 *                     not be constructed, -1 on failure
+	 * 
+	 * @since  `.version == 1`
+	 */
+	int (*create_disjunction_as_function)(void *left, void *right, struct libnormalform_function **out, void *user_data);
+
+	/**
+	 * The library will set this field to `NULL`, but
+	 * if the application has created a disjunction
+	 * of the two atomic sentences, it should be stored
+	 * here, if the disjunction is a variable
+	 * 
+	 * @since  `.version == 1`
+	 */
+	struct libnormalform_variable *created_disjunction_as_variable;
+
+	/**
+	 * The library will set this field to `NULL`, but if
+	 * the application is able to create a disjunction
+	 * of the two atomic sentences, it shall store a pointer
+	 * the a function for doing so in this field, if the
+	 * result will be a variable
+	 * 
+	 * @param   left       The left-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the left-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   right      The right-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the right-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   out        Output parameter for the disjunction of the
+	 *                     two atomic sentences
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success if `*out` was created,
+	 *                     0 if it turned out that a disjunction could
+	 *                     not be constructed, -1 on failure
+	 * 
+	 * @since  `.version == 1`
+	 */
+	int (*create_disjunction_as_variable)(void *left, void *right, struct libnormalform_variable **out, void *user_data);
+
+	/**
+	 * Set by the library to a hint to the application on
+	 * whether it would like to create an exclusive disjunction
+	 * of the two atomic sentences
+	 * 
+	 * @since  `.version == 1`
+	 */
+	enum libnormalform_ternary exclusive_disjunction_is_useful;
+
+	/**
+	 * The library will set this field to `NULL`, but
+	 * if the application has created an exclusive disjunction
+	 * of the two atomic sentences, it should be stored
+	 * here, if the exclusive disjunction is a function
+	 * 
+	 * @since  `.version == 1`
+	 */
+	struct libnormalform_function *created_exclusive_disjunction_as_function;
+
+	/**
+	 * The library will set this field to `NULL`, but if
+	 * the application is able to create an exclusive disjunction
+	 * of the two atomic sentences, it shall store a pointer
+	 * the a function for doing so in this field, if the
+	 * result will be a function
+	 * 
+	 * @param   left       The left-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the left-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   right      The right-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the right-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   out        Output parameter for the exclusive disjunction
+	 *                     of the two atomic sentences
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success if `*out` was created,
+	 *                     0 if it turned out that an exclusive disjunction
+	 *                     could not be constructed, -1 on failure
+	 * 
+	 * @since  `.version == 1`
+	 */
+	int (*create_exclusive_disjunction_as_function)(void *left, void *right, struct libnormalform_function **out, void *user_data);
+
+	/**
+	 * The library will set this field to `NULL`, but
+	 * if the application has created an exclusive disjunction
+	 * of the two atomic sentences, it should be stored
+	 * here, if the exclusive disjunction is a variable
+	 * 
+	 * @since  `.version == 1`
+	 */
+	struct libnormalform_variable *created_exclusive_disjunction_as_variable;
+
+	/**
+	 * The library will set this field to `NULL`, but if
+	 * the application is able to create an exclusive disjunction
+	 * of the two atomic sentences, it shall store a pointer
+	 * the a function for doing so in this field, if the
+	 * result will be a variable
+	 * 
+	 * @param   left       The left-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the left-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   right      The right-hand atomic sentence, will be the same
+	 *                     (and thus have the same type) as the right-hand
+	 *                     atomic sentence that was input the the application
+	 *                     function together with this `struct`
+	 * @param   out        Output parameter for the exclusive disjunction
+	 *                     of the two atomic sentences
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success if `*out` was created,
+	 *                     0 if it turned out that an exclusive disjunction
+	 *                     could not be constructed, -1 on failure
+	 * 
+	 * @since  `.version == 1`
+	 */
+	int (*create_exclusive_disjunction_as_variable)(void *left, void *right, struct libnormalform_variable **out, void *user_data);
 };
 
-struct libnormalform_domain_comparsion {
+
+/**
+ * Domain comparison results
+ */
+struct libnormalform_domain_comparison {
+	/**
+	 * The library will set this to the version of the `struct`
+	 * that it uses, but before returning, if and only if the
+	 * application uses an older version, it shall set the
+	 * version number here
+	 * 
+	 * Current version number is 1
+	 * 
+	 * @since  `.version == 1`
+	 */
 	int version;
+
+	/**
+	 * Output field for the dependency relationship
+	 * between the two domains
+	 * 
+	 * @since  `.version == 1`
+	 */
 	enum libnormalform_domain_relationship relationship;
+
+	/**
+	 * The application can store any data here that will
+	 * be useful for it's callback functions stored in
+	 * the other fields
+	 * 
+	 * May be `NULL`, and initialised so by the library
+	 * 
+	 * @since  `.version == 1`
+	 */
+	void *user_data;
+
+	/**
+	 * Called with `.user_data` (even if `.user_data` is `NULL`)
+	 * before the library stops using the `struct`
+	 * 
+	 * May be `NULL`, and initialised so by the library
+	 * 
+	 * @param  user_data  `.user_data`
+	 * 
+	 * @since  `.version == 1`
+	 */
+	void (*release_user_data)(void *user_data);
+
+	/**
+	 * The library will call this function for every domain,
+	 * that the library will not use, that the application in
+	 * one of the `struct`'s fields
+	 * 
+	 * May be `NULL`, and initialised so by the library
+	 * 
+	 * @param  domain     The unused domain
+	 * @param  user_data  `.user_data`
+	 * 
+	 * @since  `.version == 1`
+	 */
+	void (*dont_want_domain)(struct libnormalform_map *domain, void *user_data);
+
+	/**
+	 * Set by the library to a hint to the application on
+	 * whether it would like to create a union of the two
+	 * domains
+	 * 
+	 * @since  `.version == 1`
+	 */
+	enum libnormalform_ternary union_is_useful;
+
+	/**
+	 * The library will set this field to `NULL`, but
+	 * if the application has created a union of the
+	 * two domains, it should be stored here
+	 * 
+	 * @since  `.version == 1`
+	 */
+	struct libnormalform_map *created_union;
+
+	/**
+	 * The library will set this field to `NULL`, but if
+	 * the application is able to create a union of the
+	 * two domains, it shall store a pointer the a function
+	 * for doing so in this field
+	 * 
+	 * @param   left       The left-hand domain, will be the same as the
+	 *                     left-hand domain that was input the the application
+	 *                     function together with this `struct`
+	 * @param   right      The right-hand domain, will be the same as the
+	 *                     right-hand domain that was input the the application
+	 *                     function together with this `struct`
+	 * @param   out        Output parameter for the union of the two domains
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success if `*out` was created,
+	 *                     0 if it turned out that a union could not be
+	 *                     constructed, -1 on failure
+	 * 
+	 * @since  `.version == 1`
+	 */
+	int (*create_union)(struct libnormalform_map *left, struct libnormalform_map *right,
+	                    struct libnormalform_map *out, void *user_data);
 };
 
-struct libnormalform_analysers { /* TODO doc */
+
+/**
+ * Callback functions for comparing atomic sentences
+ * and for comparing domains
+ */
+struct libnormalform_analysers {
+	/**
+	 * The application can store any data here that will
+	 * be useful for it's callback functions stored in
+	 * the other fields
+	 * 
+	 * May be `NULL`
+	 */
 	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);
+
+	/**
+	 * Callback function for comparing two variables
+	 * 
+	 * @param   left       The left-hand atomic sentience (variable)
+	 * @param   right      The right-hand atomic sentience (variable)
+	 * @param   result     Structure where the application shall store results
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success and a comparison was made,
+	 *                     0 on success but the sentences were incommensurable,
+	 *                     -1 on failure
+	 * 
+	 * May be `NULL`
+	 */
+	int (*compare_variable_to_variable)(struct libnormalform_variable *left, struct libnormalform_variable *right,
+	                                    struct libnormalform_atom_comparison *result, void *user_data);
+
+	/**
+	 * Callback function for comparing two functions
+	 * 
+	 * @param   left       The left-hand atomic sentience (function)
+	 * @param   right      The right-hand atomic sentience (function)
+	 * @param   result     Structure where the application shall store results
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success and a comparison was made,
+	 *                     0 on success but the sentences were incommensurable,
+	 *                     -1 on failure
+	 * 
+	 * May be `NULL`
+	 */
+	int (*compare_function_to_function)(struct libnormalform_function *left, struct libnormalform_function *right,
+	                                    struct libnormalform_atom_comparison *result, void *user_data);
+
+	/**
+	 * Callback function for comparing a variable and a function
+	 * 
+	 * @param   left       The left-hand atomic sentience (variable)
+	 * @param   right      The right-hand atomic sentience (function)
+	 * @param   result     Structure where the application shall store results
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success and a comparison was made,
+	 *                     0 on success but the sentences were incommensurable,
+	 *                     -1 on failure
+	 * 
+	 * May be `NULL`
+	 */
+	int (*compare_variable_to_function)(struct libnormalform_variable *left, struct libnormalform_function *right,
+	                                    struct libnormalform_atom_comparison *result, void *user_data);
+
+	/**
+	 * Callback function for comparing two domains
+	 * 
+	 * @param   left       The left-hand domain
+	 * @param   right      The right-hand domain
+	 * @param   result     Structure where the application shall store results
+	 * @param   user_data  `.user_data`
+	 * @return             1 on success and a comparison was made,
+	 *                     0 on success but the sentences were incommensurable,
+	 *                     -1 on failure
+	 * 
+	 * May be `NULL`
+	 */
+	int (*compare_domains)(struct libnormalform_map *left, struct libnormalform_map *right,
+	                       struct libnormalform_domain_comparison *result, void *user_data);
 };
 
 
@@ -1057,7 +1590,7 @@ struct libnormalform_analysers { /* TODO doc */
  * Qualifier
  */
 struct libnormalform_qualification {
-	struct libnormalform_map *map;          /**< The domain of interest */
+	struct libnormalform_map *domain;       /**< The domain of interest */
 	struct libnormalform_term *antecedent;  /**< The antecedent, `NULL` if joined with the predicate */
 	struct libnormalform_term *predicate;   /**< The predicate */
 };
@@ -1100,14 +1633,14 @@ struct libnormalform_term {
 	 */
 	union {
 		/**
-		 * Use if `.type` is `LIBNORMALFORM_DISJUNCTION`
+		 * Use if `.type` is `LIBNORMALFORM_CONJUNCTION`
 		 */
-		struct libnormalform_clause disjunction;
+		struct libnormalform_clause conjunction;
 
 		/**
-		 * Use if `.type` is `LIBNORMALFORM_CONJUNCTION`
+		 * Use if `.type` is `LIBNORMALFORM_DISJUNCTION`
 		 */
-		struct libnormalform_clause conjunction;
+		struct libnormalform_clause disjunction;
 
 		/**
 		 * Use if `.type` is `LIBNORMALFORM_EXCLUSIVE_DISJUNCTION`
@@ -1302,22 +1835,22 @@ 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
+ * Return an application-readable expression of a sentence in negation
+ * normal form, optionally with XOR, and reduce the sentence to a
+ * sentence 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
+ * and `.requires_relaxation` in each `struct libnormalform_function` used
+ * used in the sentence. `.requires_relaxation` may be set to 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`
+ * to the new function or to `NULL`; if set to `NULL`, the function is
+ * reduced to a tautological sentence. For any `struct libnormalform_transformer`
  * it must also set `.requires_elimination` to 1 if the transformation
- * must be replaces with a tautology, and 0 otherwise.
+ * must be replaces with a tautology, and to 0 otherwise.
  * 
  * @param   this       The sentence to describe
  * @param   flags      The bitwise OR of any number of the following values:
@@ -1325,9 +1858,10 @@ int (libnormalform_evaluate)(LIBNORMALFORM_SENTENCE *this);
  *                     - 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,
+ *                     - LIBNORMALFORM_REDUCE_XOR:                      Do not use XOR in the returned sentence,
  *                                                                      but transform it to negation normal form
+ *                     - LIBNORMALFORM_RELAX_XOR                        Relax any XOR or OR
+ *                                                                      (nullified by `LIBNORMALFORM_REDUCE_XOR`)
  *                     - 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))
@@ -1337,72 +1871,123 @@ int (libnormalform_evaluate)(LIBNORMALFORM_SENTENCE *this);
  *                     - 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_NEGATED_FOR_ANY        Relax any non-translatable ¬∃x.φ to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_FOR_ONE                Relax any non-translatable ∃!x.φ to ⊤
+ *                     - LIBNORMALFORM_ELIMINATE_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`
+ *                     - LIBNORMALFORM_DISTRIBUTE_QUALIFIERS            Express (⋀ᵩφ(y) ∀ ⟨x,y⟩ ∈ D : α(x)) as
+ *                                                                              ⋀ᵩ(φ(y) ∀ ⟨x,y⟩ ∈ D : α(x)),
+ *                                                                      express ¬(⋀ᵩφ(y) ∀ ⟨x,y⟩ ∈ D : α(x)) as
+ *                                                                              ⋁ᵩ¬(φ(y) ∀ ⟨x,y⟩ ∈ D : α(x)),
+ *                                                                      express (⋁ᵩφ(y) ∃ ⟨x,y⟩ ∈ D : α(x)) as
+ *                                                                              ⋁ᵩ(φ(y) ∃ ⟨x,y⟩ ∈ D : α(x), and
+ *                                                                      express ¬(⋁ᵩφ(y) ∃ ⟨x,y⟩ ∈ D : α(x)) as
+ *                                                                              ⋀ᵩ¬(φ(y) ∃ ⟨x,y⟩ ∈ D : α(x));
+ *                                                                      where α may be tautology (represented as `NULL`),
+ *                                                                      and instead φ(y) would be φ({x,y}), due to
+ *                                                                      `LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL`,
+ *                                                                      `LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL`,
+ *                                                                      `LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY`, or
+ *                                                                      `LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY`
+ * @param   analysers  Application provided functions to help reduce the sentence, 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
  * 
+ * @throws  ENOMEM  Insufficient memory available
+ * @throws  EINVAL  `flags` contained unsupported options
+ * 
  * @seealso  libnormalform_dnf
  * @seealso  libnormalform_cnf
+ * @seealso  libnormalform_cdnf
  */
 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 */
+struct libnormalform_term *(libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags,
                                                    const struct libnormalform_analysers *analysers);
 
 
 /**
- * Variant of `libnormalform_express` that always canonicalises
- * the statement to disjunctive normal form
+ * Variant of `libnormalform_express` that always normalises
+ * the sentence to disjunctive normal form
  * 
  * @param   this       The sentence to describe
- * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR`
+ * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_RELAX_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`
+ * @param   analysers  Application provided functions to help reduce the sentence, 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
  * 
+ * @throws  ENOMEM  Insufficient memory available
+ * @throws  EINVAL  `flags` contained unsupported options
+ * 
  * @seealso  libnormalform_express
+ * @seealso  libnormalform_cdnf
  * @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 */
+struct libnormalform_term *(libnormalform_dnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags,
                                                const struct libnormalform_analysers *analysers);
 
 
 /**
- * Variant of `libnormalform_express` that always canonicalises
- * the statement to conjuctive normal form
+ * Variant of `libnormalform_express` that always normalises
+ * the sentence to conjuctive normal form
  * 
  * @param   this       The sentence to describe
- * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR`
+ * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_RELAX_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`
+ * @param   analysers  Application provided functions to help reduce the sentence, 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
  * 
+ * @throws  ENOMEM  Insufficient memory available
+ * @throws  EINVAL  `flags` contained unsupported options
+ * 
  * @seealso  libnormalform_express
  * @seealso  libnormalform_dnf
+ * @seealso  libnormalform_cdnf
  */
 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 */
+struct libnormalform_term *(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags,
                                                const struct libnormalform_analysers *analysers);
 
 
 /**
+ * Variant of `libnormalform_express` that always normalises
+ * the sentence to canonical disjunctive normal form
+ * 
+ * @param   this       The sentence to describe
+ * @param   flags      See `libnormalform_express`; `LIBNORMALFORM_RELAX_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 sentence, 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
+ * 
+ * @throws  ENOMEM  Insufficient memory available
+ * @throws  EINVAL  `flags` contained unsupported options
+ * 
+ * @seealso  libnormalform_express
+ * @seealso  libnormalform_dnf
+ * @seealso  libnormalform_cnf
+ */
+LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1)
+struct libnormalform_term *(libnormalform_cdnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags,
+                                                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)
  * 
@@ -1415,9 +2000,8 @@ struct libnormalform_term *(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uin
  * (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,
+ * reduced into fewer types of connetives (it's reduced into
+ * negation normal form, except with XOR allowed) during construction,
  * so this function will not necessarily reproduce the sentence
  * as it was specified when it was constructed.
  * 
@@ -1621,7 +2205,7 @@ LIBNORMALFORM_SENTENCE *(libnormalform_not)(LIBNORMALFORM_SENTENCE *x);
  * -  ∀x∈D.P(x) → ⊤ = ⊤
  * -  ∀x∈D.⊥ → Q(x) = ⊤
  * -  ∀x∈D.⊤ → ⊥ ⊨ D = ∅
- * -  Conjunction
+ * -  Conjunction: (⋀ᵩ(φ(y)) ∀ ⟨x,y⟩ ∈ D : α(x)) = ⋀ᵩ(φ(y) ∀ ⟨x,y⟩ ∈ D : α(x))
  * 
  * Commonly written "∀" ("∀x∈d.k(x) → v(x)", "∀x∈d (k(x) → v(x))", or "v(x) ∀ x∈d : k(x)")
  * 
@@ -1664,7 +2248,7 @@ LIBNORMALFORM_SENTENCE *(libnormalform_all)(struct libnormalform_map *d, LIBNORM
  * -  ∃x∈D.P(x) ∧ ⊥ = ⊥
  * -  ∃x∈D.⊥ ∧ Q(x) = ⊥
  * -  ∃x∈D.⊤ ∧ ⊤ ⊨ D ⊃ ∅
- * -  Disjunction
+ * -  Disjunction: (⋁ᵩ(φ(y)) ∃ ⟨x,y⟩ ∈ D : α(x)) = ⋁ᵩ(φ(y) ∃ ⟨x,y⟩ ∈ D : α(x))
  * 
  * Commonly written "∃" ("∃x∈d.k(x) ∧ v(x)", "∃x∈d (k(x) ∧ v(x))", or "v(x) ∃ x∈d : k(x)")
  * 
@@ -1868,7 +2452,7 @@ LIBNORMALFORM_SENTENCE *(libnormalform_or)(LIBNORMALFORM_SENTENCE **xs);
  * Commonly written "⊕" ("⨁" if n-ary), "⊻", "↮", "⇎", "≢", or "^"
  * 
  * Note that the name Exclusive disjunction is misleading
- * when there are more than two terms, as the statement
+ * when there are more than two terms, as the sentence
  * will not check that exactly one term is true, but rather
  * calculate the parity of the terms.
  * 
@@ -2240,7 +2824,7 @@ LIBNORMALFORM_SENTENCE *(libnormalform_nif)(LIBNORMALFORM_SENTENCE **xs);
 /**
  * NIMPLY: Material nonimplication
  * 
- * Also known as NIMPLIES, BUT NOT or Material abjunction
+ * Also known as NIMPLIES, NOT..WITH, 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])