.TH LIBNORMALFORM_EXPRESS 3 LIBNORMALFORM .SH NAME libnormalform_express \- Sentence reduction and normalisation .SH SYNOPSIS .nf #include #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 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)