diff options
Diffstat (limited to '')
| -rw-r--r-- | man3/libnormalform_express.3 | 1336 |
1 files changed, 1336 insertions, 0 deletions
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) |