path: root/man3/libnormalform_express.3

.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)