Second commitHEADmaster

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

39 files changed, 1782 insertions, 50 deletions

diff --git a/man3/enum_libnormalform_domain_relationship.3 b/man3/enum_libnormalform_domain_relationship.3
new file mode 120000
index 0000000..d76da20
--- /dev/null
+++ b/man3/enum_libnormalform_domain_relationship.3
@@ -0,0 +1 @@
+struct_libnormalform_domain_comparison.3
\ No newline at end of file
diff --git a/man3/enum_libnormalform_sentences_relationship.3 b/man3/enum_libnormalform_sentences_relationship.3
new file mode 120000
index 0000000..3b51671
--- /dev/null
+++ b/man3/enum_libnormalform_sentences_relationship.3
@@ -0,0 +1 @@
+struct_libnormalform_atom_comparison.3
\ No newline at end of file
diff --git a/man3/enum_libnormalform_ternary.3 b/man3/enum_libnormalform_ternary.3
new file mode 120000
index 0000000..0d9b1eb
--- /dev/null
+++ b/man3/enum_libnormalform_ternary.3
@@ -0,0 +1 @@
+struct_libnormalform_analysers.3
\ No newline at end of file
diff --git a/man3/libnormalform_all.3 b/man3/libnormalform_all.3
index 901bba2..207243f 100644
--- a/man3/libnormalform_all.3
+++ b/man3/libnormalform_all.3
@@ -154,9 +154,9 @@ The
 .BR libnormalform_all ()
 and
 .BR libnormalform_universally ()
-functions fails if:
+functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_analysers.3 b/man3/libnormalform_analysers.3
new file mode 120000
index 0000000..0d9b1eb
--- /dev/null
+++ b/man3/libnormalform_analysers.3
@@ -0,0 +1 @@
+struct_libnormalform_analysers.3
\ No newline at end of file
diff --git a/man3/libnormalform_and.3 b/man3/libnormalform_and.3
index bb65a74..aeb4fa0 100644
--- a/man3/libnormalform_and.3
+++ b/man3/libnormalform_and.3
@@ -110,9 +110,9 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_any.3 b/man3/libnormalform_any.3
index ac44b0b..57ad55c 100644
--- a/man3/libnormalform_any.3
+++ b/man3/libnormalform_any.3
@@ -221,9 +221,9 @@ The
 .BR libnormalform_empty (),
 and
 .BR libnormalform_nonempty (),
-functions fails if:
+functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_atom_comparison.3 b/man3/libnormalform_atom_comparison.3
new file mode 120000
index 0000000..3b51671
--- /dev/null
+++ b/man3/libnormalform_atom_comparison.3
@@ -0,0 +1 @@
+struct_libnormalform_atom_comparison.3
\ No newline at end of file
diff --git a/man3/libnormalform_cdnf.3 b/man3/libnormalform_cdnf.3
new file mode 100644
index 0000000..461e63e
--- /dev/null
+++ b/man3/libnormalform_cdnf.3
@@ -0,0 +1,134 @@
+.TH LIBNORMALFORM_CDNF 3 LIBNORMALFORM
+.SH NAME
+libnormalform_cdnf \- Reduce and express in canonical disjunctive normal form
+
+.SH SYNOPSIS
+.nf
+#include <libnormalform.h>
+
+/* See \fBlibnormalform_express\fP(3) for relevant types and constants */
+
+struct libnormalform_term *
+libnormalform_cdnf(LIBNORMALFORM_SENTENCE *\fIthis\fP, uint64_t \fIflags\fP,
+                   const struct libnormalform_analysers *\fIanalysers\fP);
+.fi
+.PP
+Link with
+.IR -lnormalform .
+
+.SH DESCRIPTION
+The
+.BR libnormalform_cdnf ()
+function is similar to the
+.BR libnormalform_express (3)
+function, please refer to
+.BR libnormalform_express (3)
+for a detailed explanation. There are however
+the following differences:
+.PP
+The result will never contain a
+.I LIBNORMALFORM_EXCLUSIVE_DISJUNCTION
+clause, instead these are always relax
+to disjunctions
+.RI ( LIBNORMALFORM_RELAX_XOR ),
+or reduced to an equivalent form if the
+.I LIBNORMALFORM_REDUCE_XOR
+flag is used.
+.PP
+.I LIBNORMALFORM_CONJUNCTION
+and
+.I LIBNORMALFORM_DISJUNCTION
+clauses in the result can be singleton
+clauses.
+.PP
+The root term is always a
+.I LIBNORMALFORM_DISJUNCTION
+clause containing only
+.I LIBNORMALFORM_CONJUNCTION
+clauses, each containing only literals
+(boolean variables and boolean-output
+functions), input transformations on
+literals, and qualifications. Additionally
+each conjunctive clause contains a complete
+enumerate of all atomic sentences (boolean
+variables and boolean-output functions)
+and qualifications (universal and existential
+qualifiers either be negated or translated to
+the other depending on the specified
+.IR flags )
+used in any of the conjuctive clauses within
+the root disjuntive clause. That is
+the returned expression is always
+.I this
+(or some relaxation) expressed in
+canonical disjunctive normal form.
+.PP
+Each
+.RI non- NULL
+.I .term.qualifier.antecedent
+is expressed in canonical disjunctive normal form.
+.PP
+Each
+.I .term.qualifier.predicate
+is expressed in canonical disjunctive normal form.
+
+.SH RETURN VALUE
+Upon successful completion, the
+.BR libnormalform_cdnf ()
+function return an object representing
+the sentence, which is to be deallocated
+by the application using the
+.BR libnormalform_free (3)
+function; otherwise, the function returns
+.I NULL
+and set
+.I errno
+to indicate the error; if the function
+fails because an application-provided
+callback function fails,
+.I errno
+will remain as set by that function
+(or be unmodified if that function did
+not set
+.IR errno ).
+
+.SH ERRORS
+The
+.BR libnormalform_cdnf ()
+function fails if:
+.TP
+.B ENOMEM
+Insufficient memory was available to
+create the representation of the sentence.
+.TP
+.B EINVAL
+.I flags
+contain unsupported options.
+
+.SH ATTRIBUTES
+For an explanation of the terms used in this
+section, see
+.BR attributes (7)
+and
+.IR "info \(dq(libc)POSIX Safety Concepts\(dq" .
+.TS
+allbox;
+lb lb lb
+l l l.
+Interface	Attribute	Value
+T{
+.BR libnormalform_cdnf ()
+T}	Thread safety	MT-Safe race:\fIthis\fP
+T{
+.BR libnormalform_cdnf ()
+T}	Async-signal safety	AS-Unsafe heap
+T{
+.BR libnormalform_cdnf ()
+T}	Async-cancel safety	AC-Safe mem, AC-Unsafe heap
+.TE
+
+.SH SEE ALSO
+.BR libnormalform (7),
+.BR libnormalform_express (3),
+.BR libnormalform_dnf (3),
+.BR libnormalform_cnf (3)
diff --git a/man3/libnormalform_clone.3 b/man3/libnormalform_clone.3
index 0906a44..02cf5ca 100644
--- a/man3/libnormalform_clone.3
+++ b/man3/libnormalform_clone.3
@@ -63,7 +63,7 @@ The
 .BR libnormalform_clone ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_cnf.3 b/man3/libnormalform_cnf.3
new file mode 100644
index 0000000..c0d7438
--- /dev/null
+++ b/man3/libnormalform_cnf.3
@@ -0,0 +1,125 @@
+.TH LIBNORMALFORM_CNF 3 LIBNORMALFORM
+.SH NAME
+libnormalform_cnf \- Reduce and express in conjunctive normal form
+
+.SH SYNOPSIS
+.nf
+#include <libnormalform.h>
+
+/* See \fBlibnormalform_express\fP(3) for relevant types and constants */
+
+struct libnormalform_term *
+libnormalform_cnf(LIBNORMALFORM_SENTENCE *\fIthis\fP, uint64_t \fIflags\fP,
+                  const struct libnormalform_analysers *\fIanalysers\fP);
+.fi
+.PP
+Link with
+.IR -lnormalform .
+
+.SH DESCRIPTION
+The
+.BR libnormalform_cnf ()
+function is similar to the
+.BR libnormalform_express (3)
+function, please refer to
+.BR libnormalform_express (3)
+for a detailed explanation. There are however
+the following differences:
+.PP
+The result will never contain a
+.I LIBNORMALFORM_EXCLUSIVE_DISJUNCTION
+clause, instead these are always relax
+to disjunctions
+.RI ( LIBNORMALFORM_RELAX_XOR ),
+or reduced to an equivalent form if the
+.I LIBNORMALFORM_REDUCE_XOR
+flag is used.
+.PP
+.I LIBNORMALFORM_CONJUNCTION
+and
+.I LIBNORMALFORM_DISJUNCTION
+clauses in the result can be singleton
+clauses.
+.PP
+The root term is always a
+.I LIBNORMALFORM_CONJUNCTION
+clause containing only
+.I LIBNORMALFORM_DISJUNCTION
+clauses, each containing only literals
+(boolean variables and boolean-output
+functions), input transformations on
+literals, and qualifications. That is
+the returned expression is always
+.I this
+(or some relaxation) expressed in
+conjunctive normal form.
+.PP
+Each
+.RI non- NULL
+.I .term.qualifier.antecedent
+is expressed in conjunctive normal form.
+.PP
+Each
+.I .term.qualifier.predicate
+is expressed in conjunctive normal form.
+
+.SH RETURN VALUE
+Upon successful completion, the
+.BR libnormalform_cnf ()
+function return an object representing
+the sentence, which is to be deallocated
+by the application using the
+.BR libnormalform_free (3)
+function; otherwise, the function returns
+.I NULL
+and set
+.I errno
+to indicate the error; if the function
+fails because an application-provided
+callback function fails,
+.I errno
+will remain as set by that function
+(or be unmodified if that function did
+not set
+.IR errno ).
+
+.SH ERRORS
+The
+.BR libnormalform_cnf ()
+function fails if:
+.TP
+.B ENOMEM
+Insufficient memory was available to
+create the representation of the sentence.
+.TP
+.B EINVAL
+.I flags
+contain unsupported options.
+
+.SH ATTRIBUTES
+For an explanation of the terms used in this
+section, see
+.BR attributes (7)
+and
+.IR "info \(dq(libc)POSIX Safety Concepts\(dq" .
+.TS
+allbox;
+lb lb lb
+l l l.
+Interface	Attribute	Value
+T{
+.BR libnormalform_cnf ()
+T}	Thread safety	MT-Safe race:\fIthis\fP
+T{
+.BR libnormalform_cnf ()
+T}	Async-signal safety	AS-Unsafe heap
+T{
+.BR libnormalform_cnf ()
+T}	Async-cancel safety	AC-Safe mem, AC-Unsafe heap
+.TE
+
+.SH SEE ALSO
+.BR libnormalform (7),
+.BR libnormalform_express (3),
+.BR libnormalform_dnf (3),
+.BR libnormalform_cdnf (3)
diff --git a/man3/libnormalform_dnf.3 b/man3/libnormalform_dnf.3
new file mode 100644
index 0000000..825ff1b
--- /dev/null
+++ b/man3/libnormalform_dnf.3
@@ -0,0 +1,125 @@
+.TH LIBNORMALFORM_DNF 3 LIBNORMALFORM
+.SH NAME
+libnormalform_dnf \- Reduce and express in disjunctive normal form
+
+.SH SYNOPSIS
+.nf
+#include <libnormalform.h>
+
+/* See \fBlibnormalform_express\fP(3) for relevant types and constants */
+
+struct libnormalform_term *
+libnormalform_dnf(LIBNORMALFORM_SENTENCE *\fIthis\fP, uint64_t \fIflags\fP,
+                  const struct libnormalform_analysers *\fIanalysers\fP);
+.fi
+.PP
+Link with
+.IR -lnormalform .
+
+.SH DESCRIPTION
+The
+.BR libnormalform_dnf ()
+function is similar to the
+.BR libnormalform_express (3)
+function, please refer to
+.BR libnormalform_express (3)
+for a detailed explanation. There are however
+the following differences:
+.PP
+The result will never contain a
+.I LIBNORMALFORM_EXCLUSIVE_DISJUNCTION
+clause, instead these are always relax
+to disjunctions
+.RI ( LIBNORMALFORM_RELAX_XOR ),
+or reduced to an equivalent form if the
+.I LIBNORMALFORM_REDUCE_XOR
+flag is used.
+.PP
+.I LIBNORMALFORM_CONJUNCTION
+and
+.I LIBNORMALFORM_DISJUNCTION
+clauses in the result can be singleton
+clauses.
+.PP
+The root term is always a
+.I LIBNORMALFORM_DISJUNCTION
+clause containing only
+.I LIBNORMALFORM_CONJUNCTION
+clauses, each containing only literals
+(boolean variables and boolean-output
+functions), input transformations on
+literals, and qualifications. That is
+the returned expression is always
+.I this
+(or some relaxation) expressed in
+disjunctive normal form.
+.PP
+Each
+.RI non- NULL
+.I .term.qualifier.antecedent
+is expressed in disjunctive normal form.
+.PP
+Each
+.I .term.qualifier.predicate
+is expressed in disjunctive normal form.
+
+.SH RETURN VALUE
+Upon successful completion, the
+.BR libnormalform_dnf ()
+function return an object representing
+the sentence, which is to be deallocated
+by the application using the
+.BR libnormalform_free (3)
+function; otherwise, the function returns
+.I NULL
+and set
+.I errno
+to indicate the error; if the function
+fails because an application-provided
+callback function fails,
+.I errno
+will remain as set by that function
+(or be unmodified if that function did
+not set
+.IR errno ).
+
+.SH ERRORS
+The
+.BR libnormalform_dnf ()
+function fails if:
+.TP
+.B ENOMEM
+Insufficient memory was available to
+create the representation of the sentence.
+.TP
+.B EINVAL
+.I flags
+contain unsupported options.
+
+.SH ATTRIBUTES
+For an explanation of the terms used in this
+section, see
+.BR attributes (7)
+and
+.IR "info \(dq(libc)POSIX Safety Concepts\(dq" .
+.TS
+allbox;
+lb lb lb
+l l l.
+Interface	Attribute	Value
+T{
+.BR libnormalform_dnf ()
+T}	Thread safety	MT-Safe race:\fIthis\fP
+T{
+.BR libnormalform_dnf ()
+T}	Async-signal safety	AS-Unsafe heap
+T{
+.BR libnormalform_dnf ()
+T}	Async-cancel safety	AC-Safe mem, AC-Unsafe heap
+.TE
+
+.SH SEE ALSO
+.BR libnormalform (7),
+.BR libnormalform_express (3),
+.BR libnormalform_cnf (3),
+.BR libnormalform_cdnf (3)
diff --git a/man3/libnormalform_domain_comparison.3 b/man3/libnormalform_domain_comparison.3
new file mode 120000
index 0000000..d76da20
--- /dev/null
+++ b/man3/libnormalform_domain_comparison.3
@@ -0,0 +1 @@
+struct_libnormalform_domain_comparison.3
\ No newline at end of file
diff --git a/man3/libnormalform_domain_relationship.3 b/man3/libnormalform_domain_relationship.3
new file mode 120000
index 0000000..a243086
--- /dev/null
+++ b/man3/libnormalform_domain_relationship.3
@@ -0,0 +1 @@
+enum_libnormalform_domain_relationship.3
\ No newline at end of file
diff --git a/man3/libnormalform_express.3 b/man3/libnormalform_express.3
new file mode 100644
index 0000000..b28750a
--- /dev/null
+++ b/man3/libnormalform_express.3
@@ -0,0 +1,1336 @@
+.TH LIBNORMALFORM_EXPRESS 3 LIBNORMALFORM
+.SH NAME
+libnormalform_express \- Sentence reduction and normalisation
+
+.SH SYNOPSIS
+.nf
+#include <libnormalform.h>
+
+#define \fILIBNORMALFORM_AVOID_FOR_ALL\fP                 /* ... */
+#define \fILIBNORMALFORM_AVOID_NEGATED_FOR_ALL\fP         /* ... */
+#define \fILIBNORMALFORM_AVOID_FOR_ANY\fP                 /* ... */
+#define \fILIBNORMALFORM_AVOID_NEGATED_FOR_ANY\fP         /* ... */
+#define \fILIBNORMALFORM_REDUCE_XOR\fP                    /* ... */
+#define \fILIBNORMALFORM_RELAX_XOR\fP                     /* ... */
+#define \fILIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL\fP         /* ... */
+#define \fILIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL\fP /* ... */
+#define \fILIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY\fP         /* ... */
+#define \fILIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY\fP /* ... */
+#define \fILIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE\fP         /* ... */
+#define \fILIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ONE\fP /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_FOR_ALL\fP             /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL\fP     /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_FOR_ANY\fP             /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY\fP     /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_FOR_ONE\fP             /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE\fP     /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_VARIABLE\fP            /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE\fP    /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_FUNCTION\fP            /* ... */
+#define \fILIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION\fP    /* ... */
+#define \fILIBNORMALFORM_DISTRIBUTE_QUALIFIERS\fP         /* ... */
+
+enum libnormalform_term_type {
+        \fILIBNORMALFORM_CONJUNCTION\fP,
+        \fILIBNORMALFORM_DISJUNCTION\fP,
+        \fILIBNORMALFORM_EXCLUSIVE_DISJUNCTION\fP,
+        \fILIBNORMALFORM_TRANSFORMATION\fP,
+        \fILIBNORMALFORM_VARIABLE\fP,
+        \fILIBNORMALFORM_NEGATED_VARIABLE\fP,
+        \fILIBNORMALFORM_FUNCTION\fP,
+        \fILIBNORMALFORM_NEGATED_FUNCTION\fP,
+        \fILIBNORMALFORM_FOR_ALL\fP,
+        \fILIBNORMALFORM_NEGATED_FOR_ALL\fP,
+        \fILIBNORMALFORM_FOR_ANY\fP,
+        \fILIBNORMALFORM_NEGATED_FOR_ANY\fP,
+        \fILIBNORMALFORM_FOR_ONE\fP,
+        \fILIBNORMALFORM_NEGATED_FOR_ONE\fP
+};
+
+enum libnormalform_ternary {
+        \fILIBNORMALFORM_NO\fP = 0,
+        \fILIBNORMALFORM_MAYBE\fP = 1,
+        \fILIBNORMALFORM_YES\fP = 2
+};
+
+enum libnormalform_sentence_relationship [
+        \fILIBNORMALFORM_MATERIAL_IMPLICATION\fP = -1,
+        \fILIBNORMALFORM_IDENTICAL\fP = 0,
+        \fILIBNORMALFORM_CONVERSE_IMPLICATION\fP = 1,
+        /* the following are >1 */
+        \fILIBNORMALFORM_MUTUALLY_INVERSE\fP,
+        \fILIBNORMALFORM_MUTUALLY_EXCLUSIVE\fP,
+        \fILIBNORMALFORM_JOINTLY_UNDENIABLE\fP,
+        \fILIBNORMALFORM_MUTUALLY_INDEPENDENT\fP
+};
+
+enum libnormalform_domain_relationship {
+        \fILIBNORMALFORM_SUPERSET_OF\fP = -1,
+        \fILIBNORMALFORM_SAME_AS\fP = 0,
+        \fILIBNORMALFORM_SUBSET_OF\fP = 1,
+        /* the following are >1 */
+        \fILIBNORMALFORM_DISJOINT_WITH\fP,
+        \fILIBNORMALFORM_CONJOINT_WITH\fP,
+        \fILIBNORMALFORM_UNRELATED_TO\fP
+};
+
+struct libnormalform_atom_comparison {
+    /* since .version == 1 { */
+        int \fIversion\fP;
+        enum libnormalform_sentence_relationship \fIrelationship\fP;
+        void *\fIuser_data\fP;
+
+        void (*\fIrelease_user_data\fP)(void *user_data);
+        void (*\fIdont_want_function\fP)(struct libnormalform_function *function, void *user_data);
+        void (*\fIdont_want_variable\fP)(struct libnormalform_variable *variable, void *user_data);
+
+        enum libnormalform_ternary \fIconjunction_is_useful\fP;
+        struct libnormalform_function *\fIcreated_conjunction_as_function\fP;
+        int (*\fIcreate_conjunction_as_function\fP)(void *left, void *right,
+                                              struct libnormalform_function **out,
+                                              void *user_data);
+        struct libnormalform_variable *\fIcreated_conjunction_as_variable\fP;
+        int (*\fIcreate_conjunction_as_variable\fP)(void *left, void *right,
+                                              struct libnormalform_variable **out,
+                                              void *user_data);
+
+        enum libnormalform_ternary \fIdisjunction_is_useful\fP;
+        struct libnormalform_function *\fIcreated_disjunction_as_function\fP;
+        int (*\fIcreate_disjunction_as_function\fP)(void *left, void *right,
+                                              struct libnormalform_function **out,
+                                              void *user_data);
+        struct libnormalform_variable *\fIcreated_disjunction_as_variable\fP;
+        int (*\fIcreate_disjunction_as_variable\fP)(void *left, void *right,
+                                              struct libnormalform_variable **out,
+                                              void *user_data);
+
+        enum libnormalform_ternary \fIexclusive_disjunction_is_useful\fP;
+        struct libnormalform_function *\fIcreated_exclusive_disjunction_as_function\fP;
+        int (*\fIcreate_exclusive_disjunction_as_function\fP)(void *left, void *right,
+                                                        struct libnormalform_function **out,
+                                                        void *user_data);
+        struct libnormalform_variable *\fIcreated_exclusive_disjunction_as_variable\fP;
+        int (*\fIcreate_exclusive_disjunction_as_variable\fP)(void *left, void *right,
+                                                        struct libnormalform_variable **out,
+                                                        void *user_data);
+    /* } */
+};
+
+struct libnormalform_domain_comparison {
+    /* since .version == 1 { */
+        int \fIversion\fP;
+        enum libnormalform_domain_relationship \fIrelationship\fP;
+
+        void *\fIuser_data\fP;
+        void (*\fIrelease_user_data\fP)(void *user_data);
+        void (*\fIdont_want_domain\fP)(struct libnormalform_map *domain, void *user_data);
+
+        enum libnormalform_ternary \fIunion_is_useful\fP;
+        struct libnormalform_map *\fIcreated_union\fP;
+        int (*\fIcreate_union\fP)(struct libnormalform_map *left,
+                            struct libnormalform_map *right,
+                            struct libnormalform_map *out, void *user_data);
+    /* } */
+};
+
+struct libnormalform_analysers {
+        void *\fIuser_data\fP;
+        int (*\fIcompare_variable_to_variable\fP)(struct libnormalform_variable *left,
+                                            struct libnormalform_variable *right,
+                                            struct libnormalform_atom_comparison *result,
+                                            void *user_data);
+        int (*\fIcompare_function_to_function\fP)(struct libnormalform_function *left,
+                                            struct libnormalform_function *right,
+                                            struct libnormalform_atom_comparison *result,
+                                            void *user_data);
+        int (*\fIcompare_variable_to_function\fP)(struct libnormalform_variable *left,
+                                            struct libnormalform_function *right,
+                                            struct libnormalform_atom_comparison *result,
+                                            void *user_data);
+        int (*\fIcompare_domains\fP)(struct libnormalform_map *left,
+                               struct libnormalform_map *right,
+                               struct libnormalform_domain_comparison *result,
+                               void *user_data);
+};
+
+struct libnormalform_clause {
+        struct libnormalform_term *\fIterms\fP;
+        size_t \fInterms\fP;
+};
+
+struct libnormalform_qualification {
+        struct libnormalform_map *\fIdomain\fP;
+        struct libnormalform_term *\fIantecedent\fP;
+        struct libnormalform_term *\fIpredicate\fP;
+};
+
+struct libnormalform_transformation {
+        struct libnormalform_transformer *\fItransformer\fP;
+        struct libnormalform_term *\fIsentence\fP;
+};
+
+struct libnormalform_term {
+        enum libnormalform_term_type \fItype\fP;
+        int \fIreduced\fP;
+        union {
+                struct libnormalform_clause \fIconjunction\fP;
+                struct libnormalform_clause \fIdisjunction\fP;
+                struct libnormalform_clause \fIexclusive_disjunction\fP;
+                struct libnormalform_clause \fIclause\fP;
+                struct libnormalform_transformation \fItransformation\fP;
+                struct libnormalform_variable *\fIvariable\fP;
+                struct libnormalform_function *\fIfunction\fP;
+                struct libnormalform_qualification \fIfor_all\fP;
+                struct libnormalform_qualification \fIfor_any\fP;
+                struct libnormalform_qualification \fIfor_one\fP;
+                struct libnormalform_qualification \fIqualification\fP;
+        } \fIterm\fP;
+};
+
+struct libnormalform_term *
+libnormalform_express(LIBNORMALFORM_SENTENCE *\fIthis\fP, uint64_t \fIflags\fP,
+                      const struct libnormalform_analysers *\fIanalysers\fP);
+.fi
+.PP
+Link with
+.IR -lnormalform .
+
+.SH DESCRIPTION
+The
+.BR libnormalform_express ()
+function creates an application-readable expression of
+the sentence
+.I this
+in negation normal form, optionally extended 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. For example, if the application shall serialise
+the sentence but has no way to express unique existential
+qualifications, it is reduced to existential qualification,
+but if existential qualifications cannot be represented,
+it is converted to a negated universal qualification,
+and if that cannot be represented it is eliminated.
+.PP
+Before calling this function, the application shall set
+.I .relaxation
+and
+.I .requires_relaxation
+in each
+.I struct
+.IR libnormalform_function (3)
+used in
+.IR this .
+.I .requires_relaxation
+mat be set to 0 if the function shall not be replaced
+in this case
+.I .relaxation
+need not be set), but set to 1 if the function most be
+replaced with a more true functon. In the latter case,
+.I .relaxation
+shall either beset to the new function or to
+.IR NULL ;
+if set to
+.Ir NULL ,
+the function is reduced to a tautological sentence.
+For any
+.I struct
+.IR libnormalform_transformer (3)
+it must also set
+.I .requires_elimination
+to 1 if the transformation must be replaced with a
+tautology, and to 0 otherwise (if it can be kept).
+.PP
+.I flags
+shall be the OR of zero or more of the following constants:
+.TP
+.B LIBNORMALFORM_AVOID_FOR_ALL
+The function shall, it it would not relax the sentence,
+express any non-negated universal qualification as a
+negated existential qualification.
+.TP
+.B LIBNORMALFORM_AVOID_NEGATED_FOR_ALL
+The function shall, it it would not relax the sentence,
+express any negated universal qualification as a
+non-negated existential qualification.
+.TP
+.B LIBNORMALFORM_AVOID_FOR_ANY
+The function shall, it it would not relax the sentence,
+express any non-negated existential qualification as a
+negated universal qualification.
+.TP
+.B LIBNORMALFORM_AVOID_NEGATED_FOR_ANY
+The function shall, it it would not relax the sentence,
+express any negated existential qualification as a
+non-negated universal qualification.
+.TP
+.B LIBNORMALFORM_REDUCE_XOR
+The function shall express every exclusive disjunction
+in negation normal form.
+.TP
+.B LIBNORMALFORM_RELAX_XOR
+The function shall relax every exclusive disjunction
+into a disjunction. This option nullifies the effects
+of the
+.I LIBNORMALFORM_REDUCE_XOR
+option.
+.TP
+.B LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL
+The function shall express any non-negated universal
+qualification with the antecedent and the predicate
+joined into once sentence, stored in
+.I .predicate
+for the returned
+.IR "struct libnormalform_qualification" ,
+leaving
+.I .antecedent
+set to
+.IR NULL .
+This will require the function to insert builtin
+transformations of the types
+.I LIBNORMALFORM_DOMAIN_VIEW
+(if the antecedent contains a boolean-output function)
+and
+.I LIBNORMALFORM_IMAGE_VIEW
+(if the predicate contains a boolean-output function);
+see
+.BR libnormalform_transformation (3)
+for more information.
+
+Without this option, the antecedent and the predicate
+will be stored separately, in
+.I .antecedent
+and
+.I .predicate
+respectively.
+.TP
+.B LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL
+The function shall express any negated universal
+qualification with the antecedent and the predicate
+joined into once sentence, stored in
+.I .predicate
+for the returned
+.IR "struct libnormalform_qualification" ,
+leaving
+.I .antecedent
+set to
+.IR NULL .
+This will require the function to insert builtin
+transformations of the types
+.I LIBNORMALFORM_DOMAIN_VIEW
+(if the antecedent contains a boolean-output function)
+and
+.I LIBNORMALFORM_IMAGE_VIEW
+(if the predicate contains a boolean-output function);
+see
+.BR libnormalform_transformation (3)
+for more information.
+
+Without this option, the antecedent and the predicate
+will be stored separately, in
+.I .antecedent
+and
+.I .predicate
+respectively.
+.TP
+.B LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY
+The function shall express any non-negated existential
+qualification with the antecedent and the predicate
+joined into once sentence, stored in
+.I .predicate
+for the returned
+.IR "struct libnormalform_qualification" ,
+leaving
+.I .antecedent
+set to
+.IR NULL .
+This will require the function to insert builtin
+transformations of the types
+.I LIBNORMALFORM_DOMAIN_VIEW
+(if the antecedent contains a boolean-output function)
+and
+.I LIBNORMALFORM_IMAGE_VIEW
+(if the predicate contains a boolean-output function);
+see
+.BR libnormalform_transformation (3)
+for more information.
+
+Without this option, the antecedent and the predicate
+will be stored separately, in
+.I .antecedent
+and
+.I .predicate
+respectively.
+.TP
+.B LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY
+The function shall express any negated existential
+qualification with the antecedent and the predicate
+joined into once sentence, stored in
+.I .predicate
+for the returned
+.IR "struct libnormalform_qualification" ,
+leaving
+.I .antecedent
+set to
+.IR NULL .
+This will require the function to insert builtin
+transformations of the types
+.I LIBNORMALFORM_DOMAIN_VIEW
+(if the antecedent contains a boolean-output function)
+and
+.I LIBNORMALFORM_IMAGE_VIEW
+(if the predicate contains a boolean-output function);
+see
+.BR libnormalform_transformation (3)
+for more information.
+
+Without this option, the antecedent and the predicate
+will be stored separately, in
+.I .antecedent
+and
+.I .predicate
+respectively.
+.TP
+.B LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE
+The function shall express any non-negated unique
+existential qualification with the antecedent and
+the predicate joined into once sentence, stored in
+.I .predicate
+for the returned
+.IR "struct libnormalform_qualification" ,
+leaving
+.I .antecedent
+set to
+.IR NULL .
+This will require the function to insert builtin
+transformations of the types
+.I LIBNORMALFORM_DOMAIN_VIEW
+(if the antecedent contains a boolean-output function)
+and
+.I LIBNORMALFORM_IMAGE_VIEW
+(if the predicate contains a boolean-output function);
+see
+.BR libnormalform_transformation (3)
+for more information.
+
+Without this option, the antecedent and the predicate
+will be stored separately, in
+.I .antecedent
+and
+.I .predicate
+respectively.
+.TP
+.B LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ONE
+The function shall express any negated unique
+existential qualification with the antecedent and
+the predicate joined into once sentence, stored in
+.I .predicate
+for the returned
+.IR "struct libnormalform_qualification" ,
+leaving
+.I .antecedent
+set to
+.IR NULL .
+This will require the function to insert builtin
+transformations of the types
+.I LIBNORMALFORM_DOMAIN_VIEW
+(if the antecedent contains a boolean-output function)
+and
+.I LIBNORMALFORM_IMAGE_VIEW
+(if the predicate contains a boolean-output function);
+see
+.BR libnormalform_transformation (3)
+for more information.
+
+Without this option, the antecedent and the predicate
+will be stored separately, in
+.I .antecedent
+and
+.I .predicate
+respectively.
+.TP
+.B LIBNORMALFORM_ELIMINATE_FOR_ALL
+The function shall relax any non-negated universal
+qualification into a tautology. However, unless
+.I LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY
+is also specified, the qualification will instead be
+converted into a negated existential qualification.
+.TP
+.B LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL
+The function shall relax any negated universal
+qualification into a tautology. However, unless
+.I LIBNORMALFORM_ELIMINATE_FOR_ANY
+is also specified, the qualification will instead be
+converted into a non-negated existential qualification.
+.TP
+.B LIBNORMALFORM_ELIMINATE_FOR_ANY
+The function shall relax any non-negated existential
+qualification into a tautology. However, unless
+.I LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL
+is also specified, the qualification will instead be
+converted into a negated universal qualification.
+.TP
+.B LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY
+The function shall relax any negated existential
+qualification into a tautology. However, unless
+.I LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL
+is also specified, the qualification will instead be
+converted into a non-negated universal qualification.
+.TP
+.B LIBNORMALFORM_ELIMINATE_FOR_ONE
+The function shall relax any non-negated unique
+existential qualification into a tautology. However,
+unless both
+.I LIBNORMALFORM_ELIMINATE_FOR_ANY
+and
+.I LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL
+is also specified, the qualification will instead be
+converted into a non-negated existential qualification
+or secondarily a negated universal qualification.
+.TP
+.B LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE
+The function shall relax any negated unique
+existential qualification into a tautology.
+.TP
+.B LIBNORMALFORM_ELIMINATE_VARIABLE
+The function shall relax any non-negated
+variable into a tautology.
+.TP
+.B LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE
+The function shall relax any negated
+variable into a tautology.
+.TP
+.B LIBNORMALFORM_ELIMINATE_FUNCTION
+The function shall relax any non-negated
+boolean-output function into a tautology.
+.TP
+.B LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION
+The function shall relax any negated
+boolean-output function into a tautology.
+.TP
+.B LIBNORMALFORM_DISTRIBUTE_QUALIFIERS
+Whenever possible, the function shall distribute
+a qualification over the clause of it's predicate.
+For example, if a for-all qualification has a
+predicate which is a conjuctive clause, it is
+rewritten as a conjuctive clause of for-all
+qualification, each having it's own term form
+the original qualification's clause as it's
+predicates. This is applied to both universal
+and existential qualifications, whether they are
+negated or not, but it does not apply to
+unique existential qualifications (neither
+negated nor non-negated) as these cannot be
+distributed).
+.PP
+Unless
+.I analysers
+is
+.I NULL
+it will be used by the function to query the
+application about relationships between different
+variables, boolean-output functions, and
+domains of interest for qualifiers. In this case,
+.I analysers->user_data
+may be set freely by the application and will
+be passed into the callback functions:
+.TP
+.I analysers->compare_variable_to_variable
+Will be used, unless it is
+.IR NULL ,
+by the application to query the relationship
+between two variables.
+.TP
+.I analysers->compare_function_to_function
+Will be used, unless it is
+.IR NULL ,
+by the application to query the relationship
+between two boolean-output functions.
+.TP
+.I analysers->compare_variable_to_function
+Will be used, unless it is
+.IR NULL ,
+by the application to query the relationship
+between a variable and a boolean-output function.
+.TP
+.I compare_domains
+Will be used, unless it is
+.IR NULL ,
+by the application to query the relationship
+between domains of interest for qualifiers.
+.PP
+For each of these functions
+.I left
+and
+.I right
+will be set to the two items being compare,
+.I result
+will be set structure where the application
+shall store it's results, and
+.I user_data
+will be set to
+.IR analysers->user_data .
+The functions shall return 1 if it could
+successfully compare the items, 0 if it was
+unable to compare the items, and -1 on failure
+(in which case it may also set
+.IR errno
+so the application knows what went wrong).
+The library will initialise all pointers in
+.I *result
+to
+.I NULL
+and set
+.I result->version
+to the version of the structed the library
+is compiled against, which currently is 1.
+It will also set following fields accordingly
+(refer to the
+.B SYNOPSIS
+section to see which fields, as hints, exists
+for the different callback functions):
+.TP
+.I result->conjunction_is_useful
+Set to
+.I LIBNORMALFORM_YES
+if the library will have use for a conjunction
+between the two atomic sentences,
+.I LIBNORMALFORM_NO
+otherwise, and
+.I LIBNORMALFORM_MAYBE
+if unknown.
+.TP
+.I result->disjunction_is_useful
+Set to
+.I LIBNORMALFORM_YES
+if the library will have use for a disjunction
+between the two atomic sentences,
+.I LIBNORMALFORM_NO
+otherwise, and
+.I LIBNORMALFORM_MAYBE
+if unknown.
+.TP
+.I result->exclusive_disjunction_is_useful
+Set to
+.I LIBNORMALFORM_YES
+if the library will have use for an
+exclusive disjunction between the two
+atomic sentences,
+.I LIBNORMALFORM_NO
+otherwise, and
+.I LIBNORMALFORM_MAYBE
+if unknown.
+.TP
+.I result->union_is_useful
+Set to
+.I LIBNORMALFORM_YES
+if the library will have use for an
+union between the two domains,
+.I LIBNORMALFORM_NO
+otherwise, and
+.I LIBNORMALFORM_MAYBE
+if unknown.
+.PP
+If the callback function returns 1,
+the application shall the set
+.I result->version
+the version number it is written for, but
+only if it is lower than the libraries version.
+It shall also set
+.I result->relationship
+to the relationship between the items. The
+application may also choose to set the other
+fields accordingly
+(refer to the
+.B SYNOPSIS
+section to see which fields exists for the
+different callback functions):
+.TP
+.I result->user_data
+The application may set this freely, and will
+be passed in as is to the functions in the
+structure.
+.TP
+.I result->release_user_data
+Will be called when the structure is no longer
+need, even if
+.I result->user_data
+is
+.IR NULL ;
+(of course it will not be called if this
+function pointer itself is
+.IR NULL ).
+.TP
+.I result->dont_want_function
+Will be called for any
+.I struct libnormalform_function *
+stored in
+.I *result
+that the library does not have use for.
+.TP
+.I result->dont_want_variable
+Will be called for any
+.I struct libnormalform_variable *
+stored in
+.I *result
+that the library does not have use for.
+.TP
+.I result->dont_want_domain
+Will be called for any
+.I struct libnormalform_map *
+stored in
+.I *result
+that the library does not have use for.
+.TP
+.I result->created_conjunction_as_function
+If the application created (or has) a
+boolean-output function that is the conjunction
+of the two atomic sentences, it should be stored
+here. (See
+.I result->create_conjunction_as_function
+for an alternative.)
+.TP
+.I result->created_conjunction_as_variable
+If the application created (or has) a variable
+that is the conjunction of the two atomic
+sentences, it should be stored here. (See
+.I result->create_conjunction_as_variable
+for an alternative.)
+.TP
+.I result->created_disjunction_as_function
+If the application created (or has) a
+boolean-output function that is the disjunction
+of the two atomic sentences, it should be stored
+here. (See
+.I result->create_disjunction_as_function
+for an alternative.)
+.TP
+.I result->created_disjunction_as_variable
+If the application created (or has) a variable
+that is the disjunction of the two atomic
+sentences, it should be stored here. (See
+.I result->create_disjunction_as_variable
+for an alternative.)
+.TP
+.I result->created_exclusive_disjunction_as_function
+If the application created (or has) a boolean-output
+function that is the exclusive disjunction
+of the two atomic sentences, it should be stored
+here. (See
+.I result->create_exclusive_disjunction_as_function
+for an alternative.)
+.TP
+.I result->created_exclusive_disjunction_as_variable
+If the application created (or has) a variable
+that is the exclusive disjunction of the two atomic
+sentences, it should be stored here. (See
+.I result->create_exclusive_disjunction_as_variable
+for an alternative.)
+.TP
+.I result->created_union
+If the application created (or has) a domain that
+is the union of the two domains, it should be stored
+here. (See
+.I result->create_union
+for an alternative.)
+.TP
+.I result->create_conjunction_as_function
+If the application thinks that it can create a
+boolean-output function that is the conjunction of
+.I left
+and
+.IR right ,
+a pointer to a function for doing so should be
+stored in this field.
+.I out
+is used as the output parameter for the result;
+the function shall return 1 on success, 0 if
+it couldn't create the conjunction or if the
+conjunction is a variable (the library will than
+call
+.I *result->create_conjunction_as_variable
+instead unless
+.I result->create_conjunction_as_variable
+is
+.IR NULL ),
+and -1 on failure (in which case it may set
+.I errno
+to let the application know what went wrong).
+.TP
+.I result->create_conjunction_as_variable
+If the application thinks that it can create
+a variable that is the conjunction of
+.I left
+and
+.IR right ,
+a pointer to a function for doing so should be
+stored in this field.
+.I out
+is used as the output parameter for the result;
+the function shall return 1 on success, 0 if
+it couldn't create the conjunction or if the
+conjunction is a boolean-output function (the
+library will than call
+.I *result->create_conjunction_as_function
+instead unless
+.I result->create_conjunction_as_function
+is
+.IR NULL ),
+and -1 on failure (in which case it may set
+.I errno
+to let the application know what went wrong).
+.TP
+.I result->create_disjunction_as_function
+If the application thinks that it can create a
+boolean-output function that is the disjunction of
+.I left
+and
+.IR right ,
+a pointer to a function for doing so should be
+stored in this field.
+.I out
+is used as the output parameter for the result;
+the function shall return 1 on success, 0 if
+it couldn't create the disjunction or if the
+disjunction is a variable (the library will than
+call
+.I *result->create_disjunction_as_variable
+instead unless
+.I result->create_disjunction_as_variable
+is
+.IR NULL ),
+and -1 on failure (in which case it may set
+.I errno
+to let the application know what went wrong).
+.TP
+.I result->create_disjunction_as_variable
+If the application thinks that it can create
+a variable that is the disjunction of
+.I left
+and
+.IR right ,
+a pointer to a function for doing so should be
+stored in this field.
+.I out
+is used as the output parameter for the result;
+the function shall return 1 on success, 0 if
+it couldn't create the disjunction or if the
+disjunction is a boolean-output function (the
+library will than call
+.I *result->create_disjunction_as_function
+instead unless
+.I result->create_disjunction_as_function
+is
+.IR NULL ),
+and -1 on failure (in which case it may set
+.I errno
+to let the application know what went wrong).
+.TP
+.I result->create_exclusive_disjunction_as_function
+If the application thinks that it can create a
+boolean-output function that is the exclusive
+disjunction of
+.I left
+and
+.IR right ,
+a pointer to a function for doing so should be
+stored in this field.
+.I out
+is used as the output parameter for the result;
+the function shall return 1 on success, 0 if
+it couldn't create the exclusive disjunction or if
+the exclusive_ disjunction is a variable (the
+library will than call
+.I *result->create_exclusive_disjunction_as_variable
+instead unless
+.I result->create_exclusive_disjunction_as_variable
+is
+.IR NULL ),
+and -1 on failure (in which case it may set
+.I errno
+to let the application know what went wrong).
+.TP
+.I result->create_exclusive_disjunction_as_variable
+If the application thinks that it can create
+a variable that is the exclusive disjunction of
+.I left
+and
+.IR right ,
+a pointer to a function for doing so should be
+stored in this field.
+.I out
+is used as the output parameter for the result;
+the function shall return 1 on success, 0 if
+it couldn't create the exclusive disjunction or
+if the exclusive disjunction is a boolean-output
+function (the library will than call
+.I *result->create_exclusive_disjunction_as_function
+instead unless
+.I result->create_exclusive_disjunction_as_function
+is
+.IR NULL ),
+and -1 on failure (in which case it may set
+.I errno
+to let the application know what went wrong).
+.TP
+.I result->create_union
+If the application thinks that it can create
+a domain that is the union of
+.I left
+and
+.IR right ,
+a pointer to a function for doing so should be
+stored in this field.
+.I out
+is used as the output parameter for the result;
+the function shall return 1 on success,
+0 if it couldn't create the union,
+and -1 on failure (in which case it may set
+.I errno
+to let the application know what went wrong).
+.PP
+For each of functions the parameter
+.I user_data
+will be
+.IR result->user_data ,
+and for the functions that have the parameters
+.I left
+and
+.IR right ,
+these will have the same value (and thus type)
+as the parameters with the same names that the
+callback function was called with
+.RI ( left
+will be
+.I left
+and
+.I right
+will be
+.IR right ).
+.PP
+The type of
+.I result->relationship
+depends on which callback function is called.
+For 
+.IR analysers->compare_variable_to_variable ,
+.IR analysers->compare_function_to_function ,
+and
+.I analysers->compare_variable_to_function
+it is a
+.IR "enum libnormalform_sentence_relationship" .
+For
+.I analysers->compare_domains
+it is a
+.IR "enum libnormalform_domain_relationship" .
+.PP
+If
+.I result->relationship
+is a
+.IR "enum libnormalform_sentence_relationship"
+it shall be set to one the following constants
+if the callback function returns 1:
+.TP
+.B LIBNORMALFORM_MATERIAL_IMPLICATION
+.I right
+is always at least as true as
+.IR left .
+.TP
+.B LIBNORMALFORM_IDENTICAL
+.I left
+and
+.I right
+always have the same value.
+.TP
+.B LIBNORMALFORM_CONVERSE_IMPLICATION
+.I left
+is always at least as true as
+.IR right .
+.TP
+.B LIBNORMALFORM_MUTUALLY_INVERSE
+.I left
+and
+.I right
+always have the opposite value.
+.TP
+.B LIBNORMALFORM_MUTUALLY_EXCLUSIVE
+.I left
+and
+.I right
+can never both be true.
+.TP
+.B LIBNORMALFORM_JOINTLY_UNDENIABLE
+.I left
+and
+.I right
+can never both be false.
+.TP
+.B LIBNORMALFORM_MUTUALLY_INDEPENDENT
+The value of
+.I left
+and
+.I right
+are independent of each other.
+.PP
+If
+.I result->relationship
+is a
+.IR "enum libnormalform_domain_relationship"
+it shall be set to one the following constants
+if the callback function returns 1:
+.TP
+.B LIBNORMALFORM_SUPERSET_OF
+.I right
+can never contain any elements
+that are not also in
+.IR left .
+.TP
+.B LIBNORMALFORM_SAME_AS
+.I left
+and
+.I right
+always have the exact some elements.
+.TP
+.B LIBNORMALFORM_SUBSET_OF
+.I left
+can never contain any elements
+that are not also in
+.IR right .
+.TP
+.B LIBNORMALFORM_DISJOINT_WITH
+.I left
+and
+.I right
+can never have any elements in common.
+.TP
+.B LIBNORMALFORM_CONJOINT_WITH
+.I left
+and
+.I right
+can both have unique and common elements.
+.TP
+.B LIBNORMALFORM_UNRELATED_TO
+.I left
+and
+.I right
+are unrelated to each other.
+
+This is formally equivalent to
+.IR LIBNORMALFORM_CONJOINT_WITH ,
+but is semantically distinct.
+.PP
+Refer to the header file
+.B <libnormalform.h>
+for a more in-depth explanation of
+.IR "enum libnormalform_sentence_relationship"
+and
+.IR "enum libnormalform_domain_relationship" .
+.PP
+In the return object, and any subobject of
+the same type,
+.I .reduced
+will be 1 if the term recursively contains
+reductions such that it's can be true falsely,
+whereas
+.I .type
+is used to indicate the type's term, which
+determine which field in
+.I .term
+that is used:
+.TP
+.B LIBNORMALFORM_CONJUNCTION
+.I .term.conjunction
+.RI ( .term.clause
+may also be used) will contain a non-singleton
+set of terms. The clause is true exactly when
+all of these terms are true. The clause is
+empty, it is always true. The number terms is
+stored in
+.IR .term.conjunction.nterms ,
+and the terms are stored in
+.I .term.conjunction.terms
+as values (not as pointers).
+.TP
+.B LIBNORMALFORM_DISJUNCTION
+.I .term.disjunction
+.RI ( .term.clause
+may also be used) will contain a non-singleton
+set of terms. The clause is true exactly when
+at least one of these terms is true. The clause
+is empty, it is always false. The number terms
+is stored in
+.IR .term.disjunction.nterms ,
+and the terms are stored in
+.I .term.disjunction.terms
+as values (not as pointers).
+.TP
+.B LIBNORMALFORM_EXCLUSIVE_DISJUNCTION
+.I .term.exclusive_disjunction
+.RI ( .term.clause
+may also be used) will contain a non-singleton
+set of terms. The clause is true exactly when
+an odd number of these terms are true. The clause
+will never be empty (however if it were to be empty,
+it would always be false). The number terms
+is stored in
+.IR .term.exclusive_disjunction.nterms ,
+and the terms are stored in
+.I .term.exclusive_disjunction.terms
+as values (not as pointers).
+.TP
+.B LIBNORMALFORM_TRANSFORMATION
+.I .term.transformation.transformer
+will be either a built-in or application-provided
+input morphism
+.RI ( "struct libnormalform_transformer *" )
+that is applied over the input for the sentence
+.I .term.transformation.sentence .
+.TP
+.B LIBNORMALFORM_VARIABLE
+The term is
+.IR .term.variable ,
+which is an application-provided boolean variable.
+.TP
+.B LIBNORMALFORM_NEGATED_VARIABLE
+The term is negation of
+.IR .term.variable ,
+which is an application-provided boolean variable.
+.TP
+.B LIBNORMALFORM_FUNCTION
+The term is
+.IR .term.function ,
+which is an application-provided boolean-output
+function.
+.TP
+.B LIBNORMALFORM_NEGATED_FUNCTION
+The term is negation of
+.IR .term.function ,
+which is an application-provided boolean-output
+function.
+.TP
+.B LIBNORMALFORM_FOR_ALL
+The term is the universal qualification of
+the domain
+.IR .term.for_all.domain ,
+with predicate
+.IR .term.for_all.predicate .
+Additionally, depending on
+.I flags ,
+.I .term.for_all.antecedent
+may or may not be
+.IR NULL .
+.I .term.for_all.antecedent
+is
+.IR NULL ,
+.I .term.for_all.predicate
+operates both on the elements in the domain
+and image of it's value-mapping, with built-in
+transformations inserted to select between the
+domain-values and the image-values, but if
+.I .term.for_all.antecedent
+is not
+.IR NULL ,
+the domain-values are tested in
+.I .term.for_all.antecedent
+without any built-in transformation, and
+the image-values are tested in
+.I .term.for_all.predicate
+without any built-in transformation.
+The qualification is true exactly when the
+predicate is true for each element in the
+domain for which the antecedent is true.
+If there are not elements in the domain,
+or if the antecedent is false for each
+element in the domain, the qualification
+is true.
+.RI ( .terms.qualification
+may be used instead of
+.IR .terms.for_all .)
+.TP
+.B LIBNORMALFORM_NEGATED_FOR_ALL
+Identical to
+.BR LIBNORMALFORM_FOR_ALL ,
+except the qualification is negated, so
+resulting value is inverted. (The same
+field in
+.I .term
+is used.)
+.TP
+.B LIBNORMALFORM_FOR_ANY
+The term is the existential qualification of
+the domain
+.IR .term.for_any.domain ,
+with predicate
+.IR .term.for_any.predicate .
+Additionally, depending on
+.I flags ,
+.I .term.for_any.antecedent
+may or may not be
+.IR NULL .
+.I .term.for_any.antecedent
+is
+.IR NULL ,
+.I .term.for_any.predicate
+operates both on the elements in the domain
+and image of it's value-mapping, with built-in
+transformations inserted to select between the
+domain-values and the image-values, but if
+.I .term.for_any.antecedent
+is not
+.IR NULL ,
+the domain-values are tested in
+.I .term.for_any.antecedent
+without any built-in transformation, and
+the image-values are tested in
+.I .term.for_any.predicate
+without any built-in transformation.
+The qualification is true exactly when the
+predicate is true for at least one element
+in the domain for which the antecedent is
+true. If there are not elements in the
+domain, or if the antecedent is false for
+each element in the domain, the qualification
+is false.
+.RI ( .terms.qualification
+may be used instead of
+.IR .terms.for_any .)
+.TP
+.B LIBNORMALFORM_NEGATED_FOR_ALL
+Identical to
+.BR LIBNORMALFORM_FOR_ALL ,
+except the qualification is negated, so
+resulting value is inverted. (The same
+field in
+.I .term
+is used.)
+.TP
+.B LIBNORMALFORM_NEGATED_FOR_ANY
+Identical to
+.BR LIBNORMALFORM_FOR_ANY ,
+except the qualification is negated, so
+resulting value is inverted. (The same
+field in
+.I .term
+is used.)
+.TP
+.B LIBNORMALFORM_FOR_ONE
+The term is the unique existential qualification
+of the domain
+.IR .term.for_one.domain ,
+with predicate
+.IR .term.for_one.predicate .
+Additionally, depending on
+.I flags ,
+.I .term.for_one.antecedent
+may or may not be
+.IR NULL .
+.I .term.for_one.antecedent
+is
+.IR NULL ,
+.I .term.for_one.predicate
+operates both on the elements in the domain
+and image of it's value-mapping, with built-in
+transformations inserted to select between the
+domain-values and the image-values, but if
+.I .term.for_one.antecedent
+is not
+.IR NULL ,
+the domain-values are tested in
+.I .term.for_one.antecedent
+without any built-in transformation, and
+the image-values are tested in
+.I .term.for_one.predicate
+without any built-in transformation.
+The qualification is true exactly when the
+predicate is true for exactly one element
+in the domain for which the antecedent is
+true. If there are not elements in the
+domain, or if the antecedent is false for
+each element in the domain, the qualification
+is false.
+.RI ( .terms.qualification
+may be used instead of
+.IR .terms.for_one .)
+.TP
+.B LIBNORMALFORM_NEGATED_FOR_ONE
+Identical to
+.BR LIBNORMALFORM_FOR_ONE ,
+except the qualification is negated, so
+resulting value is inverted. (The same
+field in
+.I .term
+is used.)
+.PP
+.I this
+must not be
+.IR NULL .
+.PP
+The returned pointer shall either be
+deallocated with the
+.BR libnormalform_free (3)
+function.
+.PP
+This function
+.I does not
+consume
+.IR this .
+
+.SH RETURN VALUE
+Upon successful completion, the
+.BR libnormalform_express ()
+function return an object representing
+the sentence, which is to be deallocated
+by the application using the
+.BR libnormalform_free (3)
+function; otherwise, the function returns
+.I NULL
+and set
+.I errno
+to indicate the error; if the function
+fails because an application-provided
+callback function fails,
+.I errno
+will remain as set by that function
+(or be unmodified if that function did
+not set
+.IR errno ).
+
+.SH ERRORS
+The
+.BR libnormalform_express ()
+function fails if:
+.TP
+.B ENOMEM
+Insufficient memory was available to
+create the representation of the sentence.
+.TP
+.B EINVAL
+.I flags
+contain unsupported options.
+
+.SH ATTRIBUTES
+For an explanation of the terms used in this
+section, see
+.BR attributes (7)
+and
+.IR "info \(dq(libc)POSIX Safety Concepts\(dq" .
+.TS
+allbox;
+lb lb lb
+l l l.
+Interface	Attribute	Value
+T{
+.BR libnormalform_express ()
+T}	Thread safety	MT-Safe race:\fIthis\fP
+T{
+.BR libnormalform_express ()
+T}	Async-signal safety	AS-Unsafe heap
+T{
+.BR libnormalform_express ()
+T}	Async-cancel safety	AC-Safe mem, AC-Unsafe heap
+.TE
+
+.SH SEE ALSO
+.BR libnormalform (7),
+.BR libnormalform_dnf (3),
+.BR libnormalform_cnf (3),
+.BR libnormalform_cdnf (3)
diff --git a/man3/libnormalform_false.3 b/man3/libnormalform_false.3
index 83dd97a..54131c4 100644
--- a/man3/libnormalform_false.3
+++ b/man3/libnormalform_false.3
@@ -40,7 +40,7 @@ The
 .BR libnormalform_false ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 
diff --git a/man3/libnormalform_from_string.3 b/man3/libnormalform_from_string.3
index f0bfc98..108c5a7 100644
--- a/man3/libnormalform_from_string.3
+++ b/man3/libnormalform_from_string.3
@@ -111,14 +111,14 @@ The
 .BR libnormalform_from_string ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .TP
-.I EINVAL
+.B EINVAL
 The representation is invalid.
 .TP
-.I EINVAL
+.B EINVAL
 .I end_out
 is
 .I NULL
@@ -126,35 +126,35 @@ but there are non-whitespace characters in
 .I s
 after the detected end of the representation.
 .TP
-.I EDOM
+.B EDOM
 The described sentence contains an empty clause
 for a connective that does not support empty
 clauses.
 .TP
-.I EDOM
+.B EDOM
 The described sentence contains a transformation
 somewhere over a qualifer.
 .TP
-.I ENOENT
+.B ENOENT
 The described sentence contains a boolean variable but
 .I spec->get_variable
 was
 .IR NULL .
 .TP
-.I ENOENT
+.B ENOENT
 The described sentence contains a boolean function but
 .I spec->get_function
 was
 .IR NULL .
 .TP
-.I ENOENT
+.B ENOENT
 The described sentence contains (a domain of interest
 for a) qualifier  but
 .I spec->get_map
 was
 .IR NULL .
 .TP
-.I ENOENT
+.B ENOENT
 The described sentence contains a transformation
 (a input transformation function) but
 .I spec->get_transformer
diff --git a/man3/libnormalform_function.3 b/man3/libnormalform_function.3
index d89c0e9..87edd46 100644
--- a/man3/libnormalform_function.3
+++ b/man3/libnormalform_function.3
@@ -121,7 +121,7 @@ The
 .BR libnormalform_function ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 
diff --git a/man3/libnormalform_if.3 b/man3/libnormalform_if.3
index 86fde19..02c69dc 100644
--- a/man3/libnormalform_if.3
+++ b/man3/libnormalform_if.3
@@ -111,13 +111,13 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .TP
-.I EDOM
+.B EDOM
 The function was not given any subsentences.
 .PP
 The
diff --git a/man3/libnormalform_imply.3 b/man3/libnormalform_imply.3
index b6e0284..852d965 100644
--- a/man3/libnormalform_imply.3
+++ b/man3/libnormalform_imply.3
@@ -111,9 +111,9 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_nand.3 b/man3/libnormalform_nand.3
index a3604ae..3973dca 100644
--- a/man3/libnormalform_nand.3
+++ b/man3/libnormalform_nand.3
@@ -113,13 +113,13 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .TP
-.I EDOM
+.B EDOM
 The function was not given any subsentences.
 .PP
 The
diff --git a/man3/libnormalform_nif.3 b/man3/libnormalform_nif.3
index 174b9d4..39caec1 100644
--- a/man3/libnormalform_nif.3
+++ b/man3/libnormalform_nif.3
@@ -109,9 +109,9 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_nimply.3 b/man3/libnormalform_nimply.3
index ca7a0e9..c2d3d8e 100644
--- a/man3/libnormalform_nimply.3
+++ b/man3/libnormalform_nimply.3
@@ -109,13 +109,13 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .TP
-.I EDOM
+.B EDOM
 The function was not given any subsentences.
 .PP
 The
diff --git a/man3/libnormalform_nor.3 b/man3/libnormalform_nor.3
index 164e8c5..23eaae2 100644
--- a/man3/libnormalform_nor.3
+++ b/man3/libnormalform_nor.3
@@ -113,13 +113,13 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .TP
-.I EDOM
+.B EDOM
 The function was not given any subsentences.
 .PP
 The
diff --git a/man3/libnormalform_not.3 b/man3/libnormalform_not.3
index 0ebe548..ed6fdca 100644
--- a/man3/libnormalform_not.3
+++ b/man3/libnormalform_not.3
@@ -53,7 +53,7 @@ The
 .BR libnormalform_not ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_one.3 b/man3/libnormalform_one.3
index bf79161..8aa88a5 100644
--- a/man3/libnormalform_one.3
+++ b/man3/libnormalform_one.3
@@ -192,9 +192,9 @@ The
 .BR libnormalform_uniquely (),
 and
 .BR libnormalform_singleton ()
-functions fails if:
+functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_or.3 b/man3/libnormalform_or.3
index 9d57ee8..c0f58d8 100644
--- a/man3/libnormalform_or.3
+++ b/man3/libnormalform_or.3
@@ -110,9 +110,9 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_ref.3 b/man3/libnormalform_ref.3
index 5592e48..9295f12 100644
--- a/man3/libnormalform_ref.3
+++ b/man3/libnormalform_ref.3
@@ -48,7 +48,7 @@ The
 .BR libnormalform_ref ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 The reference count of
 .I x
 was already maximised (at
diff --git a/man3/libnormalform_sentences_relationship.3 b/man3/libnormalform_sentences_relationship.3
new file mode 120000
index 0000000..03be66c
--- /dev/null
+++ b/man3/libnormalform_sentences_relationship.3
@@ -0,0 +1 @@
+enum_libnormalform_sentences_relationship.3
\ No newline at end of file
diff --git a/man3/libnormalform_ternary.3 b/man3/libnormalform_ternary.3
new file mode 120000
index 0000000..96ac9d0
--- /dev/null
+++ b/man3/libnormalform_ternary.3
@@ -0,0 +1 @@
+enum_libnormalform_ternary.3
\ No newline at end of file
diff --git a/man3/libnormalform_to_string.3 b/man3/libnormalform_to_string.3
index 7008990..2150a10 100644
--- a/man3/libnormalform_to_string.3
+++ b/man3/libnormalform_to_string.3
@@ -62,7 +62,7 @@ The
 .BR libnormalform_to_string ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 serialise the sentence object.
 
@@ -93,7 +93,7 @@ When a
 .I LIBNORMALFORM_SENTENCE
 is created, it is optimised (this includes eliminiation
 of redundant information and reordering) and reduced to
-into fewer types of connetives (it's reducted into negation
+into fewer types of connetives (it's reduced into negation
 normal form, except with XOR allowed, but not necessarily
 to any canonical form) during construction, so the
 .BR libnormalform_to_string ()
diff --git a/man3/libnormalform_transformation.3 b/man3/libnormalform_transformation.3
index 7bb129e..d08ea47 100644
--- a/man3/libnormalform_transformation.3
+++ b/man3/libnormalform_transformation.3
@@ -202,11 +202,11 @@ The
 .BR libnormalform_transformation ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .TP
-.I EDOM
+.B EDOM
 .I sentence
 contains a qualifier.
 
diff --git a/man3/libnormalform_true.3 b/man3/libnormalform_true.3
index a5da907..77bdf39 100644
--- a/man3/libnormalform_true.3
+++ b/man3/libnormalform_true.3
@@ -40,7 +40,7 @@ The
 .BR libnormalform_true ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 
diff --git a/man3/libnormalform_variable.3 b/man3/libnormalform_variable.3
index ad30a37..dca3d1e 100644
--- a/man3/libnormalform_variable.3
+++ b/man3/libnormalform_variable.3
@@ -96,7 +96,7 @@ The
 .BR libnormalform_variable ()
 function fails if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 
diff --git a/man3/libnormalform_xnor.3 b/man3/libnormalform_xnor.3
index 56a3cab..322becc 100644
--- a/man3/libnormalform_xnor.3
+++ b/man3/libnormalform_xnor.3
@@ -111,9 +111,9 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/libnormalform_xor.3 b/man3/libnormalform_xor.3
index 70e9584..38571b4 100644
--- a/man3/libnormalform_xor.3
+++ b/man3/libnormalform_xor.3
@@ -110,9 +110,9 @@ and set
 to indicate the error.
 
 .SH ERRORS
-These functions fails if:
+These functions fail if:
 .TP
-.I ENOMEM
+.B ENOMEM
 Insufficient memory was available to
 create the sentence object.
 .PP
diff --git a/man3/struct_libnormalform_analysers.3 b/man3/struct_libnormalform_analysers.3
new file mode 120000
index 0000000..eae3a15
--- /dev/null
+++ b/man3/struct_libnormalform_analysers.3
@@ -0,0 +1 @@
+libnormalform_express.3
\ No newline at end of file
diff --git a/man3/struct_libnormalform_atom_comparison.3 b/man3/struct_libnormalform_atom_comparison.3
new file mode 120000
index 0000000..0d9b1eb
--- /dev/null
+++ b/man3/struct_libnormalform_atom_comparison.3
@@ -0,0 +1 @@
+struct_libnormalform_analysers.3
\ No newline at end of file
diff --git a/man3/struct_libnormalform_domain_comparison.3 b/man3/struct_libnormalform_domain_comparison.3
new file mode 120000
index 0000000..0d9b1eb
--- /dev/null
+++ b/man3/struct_libnormalform_domain_comparison.3
@@ -0,0 +1 @@
+struct_libnormalform_analysers.3
\ No newline at end of file