diff options
Diffstat (limited to '')
| -rw-r--r-- | libnormalform.h | 836 |
1 files changed, 710 insertions, 126 deletions
diff --git a/libnormalform.h b/libnormalform.h index ed3b256..c618485 100644 --- a/libnormalform.h +++ b/libnormalform.h @@ -10,6 +10,12 @@ #if defined(__GNUC__) # pragma GCC diagnostic push # pragma GCC diagnostic ignored "-Winline" +# pragma GCC diagnostic ignored "-Wpadded" +# pragma GCC diagnostic ignored "-Wvla" +# if defined(__clang__) +# pragma GCC diagnostic ignored "-Wdocumentation" +# pragma GCC diagnostic ignored "-Wunsafe-buffer-usage" /* clang is currently exceptionally stupid */ +# endif #endif @@ -17,7 +23,11 @@ #if defined(__GNUC__) # define LIBNORMALFORM_USE_RESULT__ __attribute__((__warn_unused_result__)) -# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) __attribute__((__malloc__(DESTRUCTOR))) +# if defined(__clang__) +# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) +# else +# define LIBNORMALFORM_FREE_WITH__(DESTRUCTOR) __attribute__((__malloc__(DESTRUCTOR))) +# endif # define LIBNORMALFORM_USE_FREE__ __attribute__((__malloc__)) # define LIBNORMALFORM_NONNULL_INPUT__ __attribute__((__nonnull__)) # define LIBNORMALFORM_ONE_NONNULL_INPUT__(INDEX) __attribute__((__nonnull__(INDEX))) @@ -148,8 +158,8 @@ struct libnormalform_term; #define LIBNORMALFORM_AVOID_NEGATED_FOR_ALL (UINT64_C(1) << 1) /**< Prefer ∃x.¬φ over ¬∀x.φ */ #define LIBNORMALFORM_AVOID_FOR_ANY (UINT64_C(1) << 2) /**< Prefer ¬∀x.¬φ over ∃x.φ */ #define LIBNORMALFORM_AVOID_NEGATED_FOR_ANY (UINT64_C(1) << 3) /**< Prefer ∀x.¬φ over ¬∃x.φ */ -#define LIBNORMALFORM_RELAX_FOR_ONE (UINT64_C(1) << 4) /**< Relax any positive ∃!x.φ into ∃x.φ */ -#define LIBNORMALFORM_REDUCE_XOR (UINT64_C(1) << 5) /**< Rewrite XOR to negation normal form */ +#define LIBNORMALFORM_REDUCE_XOR (UINT64_C(1) << 4) /**< Rewrite XOR to negation normal form */ +#define LIBNORMALFORM_RELAX_XOR (UINT64_C(1) << 5) /**< Relax any non-reduce XOR to OR */ #define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL (UINT64_C(1) << 6) /**< Express φ(x)∀x:θ(x) on the form ∀x.(θ(x) → φ(x)) */ #define LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL (UINT64_C(1) << 7) /**< Express ¬(φ(x)∀x:θ(x)) on the form ¬∀x.(θ(x) → φ(x)) */ #define LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY (UINT64_C(1) << 8) /**< Express φ(x)∃x:θ(x) on the form ∃x.(θ(x) ∧ φ(x)) */ @@ -166,7 +176,7 @@ struct libnormalform_term; #define LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE (UINT64_C(1) << 19) /**< Relax any negative variable literal to ⊤ */ #define LIBNORMALFORM_ELIMINATE_FUNCTION (UINT64_C(1) << 20) /**< Relax any positive function literal to ⊤ */ #define LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION (UINT64_C(1) << 21) /**< Relax any negative function literal to ⊤ */ -#define LIBNORMALFORM_ELIMINATE_XOR (UINT64_C(1) << 22) /**< Relax any non-reduce XOR to ⊤ */ +#define LIBNORMALFORM_DISTRIBUTE_QUALIFIERS (UINT64_C(1) << 21) /**< Duplicate qualifers to move out clauses */ #define LIBNORMALFORM_ALL_EXPRESS_FLAGS__ ((UINT64_C(1) << 23) - 1U) /* For internal use */ @@ -183,81 +193,13 @@ typedef struct libnormalform_sentence LIBNORMALFORM_SENTENCE; /** - * Specification for how application provided strings - * shall be interpreted - */ -struct libnormalform_representation_spec { - /** - * Application-specific data that will be passed into - * `.get_variable`, `.get_function`, `.get_map`, and - * `.get_transformer` (making it reenterant so it can be - * called by multiple threads, or to configure the function) - * - * May be `NULL` - */ - void *user_data; - - /** - * Deserialise a variable from a unterminated string - * - * The function shall be able to return the reference - * to any `struct libnormalform_variable` given its - * `.identifier` sans NUL-termination - * - * The function shall be pure in the sence that if - * it is called twice (or more) with the identifer - * at the beginning of `s` it shall return the same - * pointer, not two different copies (`user_data` be - * use used to store the variables if they are - * constructed dynamically) - * - * May be `NULL` - * - * @param s The string beginning with the variable's - * identifier - * @param end_out Output parameter for the position in - * `s` after the last byte in the identifer - * @param user_data `.user_data` - * @return A pointer to the referenced variable, `NULL` - * on failure (`errno` may be set) - * - * It is recommended that, on failure, `errno` is set - * according to the below specification, however it is - * up to the application to choose what to do with `errno` - * - * @throws EINVAL `s` in not formatted to represent a valid variable - * @throws ENOENT `s` does not represent any known variable - */ - struct libnormalform_variable *(*get_variable)(char *s, char **end_out, void *user_data); - - /** - * Same as `.get_variable` except that it returns - * reference to a function (`struct libnormalform_function *`) - */ - struct libnormalform_function *(*get_function)(char *s, char **end_out, void *user_data); - - /** - * Same as `.get_variable` except that it returns - * reference to a domain (`struct libnormalform_map *`) - */ - struct libnormalform_map *(*get_map)(char *s, char **end_out, void *user_data); - - /** - * Same as `.get_transformer` except that it returns - * reference to a function (`struct libnormalform_transformer *`) - */ - struct libnormalform_transformer *(*get_transformer)(char *s, char **end_out, void *user_data); -}; - - -/** * Type if a `struct libnormalform_term`, used to * determine which member of `.term` to use and * whether it is negated */ enum libnormalform_term_type { - LIBNORMALFORM_CONJUNCTION, /**< AND clause; empty clause is used for contradiction */ - LIBNORMALFORM_DISJUNCTION, /**< OR clause; empty clause is used for tautology */ + LIBNORMALFORM_CONJUNCTION, /**< AND clause; empty clause is used for tautology */ + LIBNORMALFORM_DISJUNCTION, /**< OR clause; empty clause is used for contradiction */ LIBNORMALFORM_EXCLUSIVE_DISJUNCTION, /**< XOR clause; never used for empty clauses */ LIBNORMALFORM_TRANSFORMATION, /**< Transformater function with input **/ LIBNORMALFORM_VARIABLE, /**< Positive variable literal **/ @@ -293,9 +235,19 @@ enum libnormalform_builtin_transformer { /** + * Boolean with possibly of being unknown + */ +enum libnormalform_ternary { + LIBNORMALFORM_NO, /**< No/False */ + LIBNORMALFORM_MAYBE, /**< Maybe/Unknown */ + LIBNORMALFORM_YES /**< Yes/True */ +}; + + +/** * Relationship (dependency) between the value of two sentences */ -enum libnormalform_sentences_relationship { +enum libnormalform_sentence_relationship { /** * Left-hand implies right-hand (⊨ P → Q) * @@ -718,7 +670,107 @@ enum libnormalform_domain_relationship { * - ⋁A → ⋁B cannot be simplified * - ⋁A ← ⋁B cannot be simplified */ - LIBNORMALFORM_CONJOINT_WITH + LIBNORMALFORM_CONJOINT_WITH, + + /** + * Both sets have no formal relationship + * + * Venn diagram of possibly non-empty intersections: + * ┌────────────────────────────┐ + * │ ┌─A─────────────┐ │ + * │ │███████████████│ │ + * │ │██████┌────────┼──────┐ │ + * │ │██████│████████│██████│ │ + * │ │██████│████████│██████│ │ + * │ └──────┼────────┘██████│ │ + * │ │███████████████│ │ + * │ └─────────────B─┘ │ + * └────────────────────────────┘ + * + * Consequence: + * - A ∩ B cannot be simplified + * - A ∪ B cannot be simplified + * - A ∆ B cannot be simplified + * - ⋀A ∧ ⋀B = ⋀(A ∪ B) + * - ⋀A ∨ ⋀B cannot be simplified + * - ⋀A ⊕ ⋀B cannot be simplified + * - ⋀A → ⋀B cannot be simplified + * - ⋀A ← ⋀B cannot be simplified + * - ⋁A ∧ ⋁B cannot be simplified + * - ⋁A ∨ ⋁B = ⋁(A ∪ B) + * - ⋁A ⊕ ⋁B cannot be simplified + * - ⋁A → ⋁B cannot be simplified + * - ⋁A ← ⋁B cannot be simplified + */ + LIBNORMALFORM_UNRELATED_TO +}; + + +/** + * Specification for how application provided strings + * shall be interpreted + */ +struct libnormalform_representation_spec { + /** + * Application-specific data that will be passed into + * `.get_variable`, `.get_function`, `.get_map`, and + * `.get_transformer` (making it reenterant so it can be + * called by multiple threads, or to configure the function) + * + * May be `NULL` + */ + void *user_data; + + /** + * Deserialise a variable from a unterminated string + * + * The function shall be able to return the reference + * to any `struct libnormalform_variable` given its + * `.identifier` sans NUL-termination + * + * The function shall be pure in the sence that if + * it is called twice (or more) with the identifer + * at the beginning of `s` it shall return the same + * pointer, not two different copies (`user_data` be + * use used to store the variables if they are + * constructed dynamically) + * + * May be `NULL` + * + * @param s The string beginning with the variable's + * identifier + * @param end_out Output parameter for the position in + * `s` after the last byte in the identifer + * @param user_data `.user_data` + * @return A pointer to the referenced variable, `NULL` + * on failure (`errno` may be set) + * + * It is recommended that, on failure, `errno` is set + * according to the below specification, however it is + * up to the application to choose what to do with `errno` + * + * @throws EINVAL `s` in not formatted to represent a valid variable + * @throws ENOENT `s` does not represent any known variable + */ + struct libnormalform_variable *(*get_variable)(char *s, char **end_out, void *user_data); + + /** + * Same as `.get_variable` except that it returns + * reference to a function (`struct libnormalform_function *`) + */ + struct libnormalform_function *(*get_function)(char *s, char **end_out, void *user_data); + + /** + * Same as `.get_variable` except that it returns + * reference to a domain (`struct libnormalform_map *`) + */ + struct libnormalform_map *(*get_map)(char *s, char **end_out, void *user_data); + + /** + * Same as `.get_transformer` except that it returns + * reference to a function (`struct libnormalform_transformer *`) + */ + struct libnormalform_transformer *(*get_transformer)(char *s, char **end_out, void *user_data); }; @@ -1030,26 +1082,507 @@ struct libnormalform_map { }; -struct libnormalform_atom_comparsion { +/** + * Variable/function (atom sentence) comparison results + */ +struct libnormalform_atom_comparison { + /** + * The library will set this to the version of the `struct` + * that it uses, but before returning, if and only if the + * application uses an older version, it shall set the + * version number here + * + * Current version number is 1 + * + * @since `.version == 1` + */ int version; - enum libnormalform_sentences_relationship relationship; + + /** + * Output field for the dependency relationship + * between the two atomic sentences + * + * @since `.version == 1` + */ + enum libnormalform_sentence_relationship relationship; + + /** + * The application can store any data here that will + * be useful for it's callback functions stored in + * the other fields + * + * May be `NULL`, and initialised so by the library + * + * @since `.version == 1` + */ + void *user_data; + + /** + * Called with `.user_data` (even if `.user_data` is `NULL`) + * before the library stops using the `struct` + * + * May be `NULL`, and initialised so by the library + * + * @param user_data `.user_data` + * + * @since `.version == 1` + */ + void (*release_user_data)(void *user_data); + + /** + * The library will call this function for every function, + * that the library will not use, that the application in + * one of the `struct`'s fields + * + * May be `NULL`, and initialised so by the library + * + * @param function The unused function + * @param user_data `.user_data` + * + * @since `.version == 1` + */ + void (*dont_want_function)(struct libnormalform_function *function, void *user_data); + + /** + * The library will call this function for every variable, + * that the library will not use, that the application in + * one of the `struct`'s fields + * + * May be `NULL`, and initialised so by the library + * + * @param variable The unused variable + * @param user_data `.user_data` + * + * @since `.version == 1` + */ + void (*dont_want_variable)(struct libnormalform_variable *variable, void *user_data); + + /** + * Set by the library to a hint to the application on + * whether it would like to create a conjunction of + * the two atomic sentences + * + * @since `.version == 1` + */ + enum libnormalform_ternary conjunction_is_useful; + + /** + * The library will set this field to `NULL`, but + * if the application has created a conjunction + * of the two atomic sentences, it should be stored + * here, if the conjunction is a function + * + * @since `.version == 1` + */ + struct libnormalform_function *created_conjunction_as_function; + + /** + * The library will set this field to `NULL`, but if + * the application is able to create a conjunction + * of the two atomic sentences, it shall store a pointer + * the a function for doing so in this field, if the + * result will be a function + * + * @param left The left-hand atomic sentence, will be the same + * (and thus have the same type) as the left-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param right The right-hand atomic sentence, will be the same + * (and thus have the same type) as the right-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param out Output parameter for the conjunction of the + * two atomic sentences + * @param user_data `.user_data` + * @return 1 on success if `*out` was created, + * 0 if it turned out that a conjunction could + * not be constructed, -1 on failure + * + * @since `.version == 1` + */ + int (*create_conjunction_as_function)(void *left, void *right, struct libnormalform_function **out, void *user_data); + + /** + * The library will set this field to `NULL`, but + * if the application has created a conjunction + * of the two atomic sentences, it should be stored + * here, if the conjunction is a variable + * + * @since `.version == 1` + */ + struct libnormalform_variable *created_conjunction_as_variable; + + /** + * The library will set this field to `NULL`, but if + * the application is able to create a conjunction + * of the two atomic sentences, it shall store a pointer + * the a function for doing so in this field, if the + * result will be a variable + * + * @param left The left-hand atomic sentence, will be the same + * (and thus have the same type) as the left-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param right The right-hand atomic sentence, will be the same + * (and thus have the same type) as the right-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param out Output parameter for the conjunction of the + * two atomic sentences + * @param user_data `.user_data` + * @return 1 on success if `*out` was created, + * 0 if it turned out that a conjunction could + * not be constructed, -1 on failure + * + * @since `.version == 1` + */ + int (*create_conjunction_as_variable)(void *left, void *right, struct libnormalform_variable **out, void *user_data); + + /** + * Set by the library to a hint to the application on + * whether it would like to create a disjunction of + * the two atomic sentences + * + * @since `.version == 1` + */ + enum libnormalform_ternary disjunction_is_useful; + + /** + * The library will set this field to `NULL`, but + * if the application has created a disjunction + * of the two atomic sentences, it should be stored + * here, if the disjunction is a function + * + * @since `.version == 1` + */ + struct libnormalform_function *created_disjunction_as_function; + + /** + * The library will set this field to `NULL`, but if + * the application is able to create a disjunction + * of the two atomic sentences, it shall store a pointer + * the a function for doing so in this field, if the + * result will be a function + * + * @param left The left-hand atomic sentence, will be the same + * (and thus have the same type) as the left-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param right The right-hand atomic sentence, will be the same + * (and thus have the same type) as the right-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param out Output parameter for the disjunction of the + * two atomic sentences + * @param user_data `.user_data` + * @return 1 on success if `*out` was created, + * 0 if it turned out that a disjunction could + * not be constructed, -1 on failure + * + * @since `.version == 1` + */ + int (*create_disjunction_as_function)(void *left, void *right, struct libnormalform_function **out, void *user_data); + + /** + * The library will set this field to `NULL`, but + * if the application has created a disjunction + * of the two atomic sentences, it should be stored + * here, if the disjunction is a variable + * + * @since `.version == 1` + */ + struct libnormalform_variable *created_disjunction_as_variable; + + /** + * The library will set this field to `NULL`, but if + * the application is able to create a disjunction + * of the two atomic sentences, it shall store a pointer + * the a function for doing so in this field, if the + * result will be a variable + * + * @param left The left-hand atomic sentence, will be the same + * (and thus have the same type) as the left-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param right The right-hand atomic sentence, will be the same + * (and thus have the same type) as the right-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param out Output parameter for the disjunction of the + * two atomic sentences + * @param user_data `.user_data` + * @return 1 on success if `*out` was created, + * 0 if it turned out that a disjunction could + * not be constructed, -1 on failure + * + * @since `.version == 1` + */ + int (*create_disjunction_as_variable)(void *left, void *right, struct libnormalform_variable **out, void *user_data); + + /** + * Set by the library to a hint to the application on + * whether it would like to create an exclusive disjunction + * of the two atomic sentences + * + * @since `.version == 1` + */ + enum libnormalform_ternary exclusive_disjunction_is_useful; + + /** + * The library will set this field to `NULL`, but + * if the application has created an exclusive disjunction + * of the two atomic sentences, it should be stored + * here, if the exclusive disjunction is a function + * + * @since `.version == 1` + */ + struct libnormalform_function *created_exclusive_disjunction_as_function; + + /** + * The library will set this field to `NULL`, but if + * the application is able to create an exclusive disjunction + * of the two atomic sentences, it shall store a pointer + * the a function for doing so in this field, if the + * result will be a function + * + * @param left The left-hand atomic sentence, will be the same + * (and thus have the same type) as the left-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param right The right-hand atomic sentence, will be the same + * (and thus have the same type) as the right-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param out Output parameter for the exclusive disjunction + * of the two atomic sentences + * @param user_data `.user_data` + * @return 1 on success if `*out` was created, + * 0 if it turned out that an exclusive disjunction + * could not be constructed, -1 on failure + * + * @since `.version == 1` + */ + int (*create_exclusive_disjunction_as_function)(void *left, void *right, struct libnormalform_function **out, void *user_data); + + /** + * The library will set this field to `NULL`, but + * if the application has created an exclusive disjunction + * of the two atomic sentences, it should be stored + * here, if the exclusive disjunction is a variable + * + * @since `.version == 1` + */ + struct libnormalform_variable *created_exclusive_disjunction_as_variable; + + /** + * The library will set this field to `NULL`, but if + * the application is able to create an exclusive disjunction + * of the two atomic sentences, it shall store a pointer + * the a function for doing so in this field, if the + * result will be a variable + * + * @param left The left-hand atomic sentence, will be the same + * (and thus have the same type) as the left-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param right The right-hand atomic sentence, will be the same + * (and thus have the same type) as the right-hand + * atomic sentence that was input the the application + * function together with this `struct` + * @param out Output parameter for the exclusive disjunction + * of the two atomic sentences + * @param user_data `.user_data` + * @return 1 on success if `*out` was created, + * 0 if it turned out that an exclusive disjunction + * could not be constructed, -1 on failure + * + * @since `.version == 1` + */ + int (*create_exclusive_disjunction_as_variable)(void *left, void *right, struct libnormalform_variable **out, void *user_data); }; -struct libnormalform_domain_comparsion { + +/** + * Domain comparison results + */ +struct libnormalform_domain_comparison { + /** + * The library will set this to the version of the `struct` + * that it uses, but before returning, if and only if the + * application uses an older version, it shall set the + * version number here + * + * Current version number is 1 + * + * @since `.version == 1` + */ int version; + + /** + * Output field for the dependency relationship + * between the two domains + * + * @since `.version == 1` + */ enum libnormalform_domain_relationship relationship; + + /** + * The application can store any data here that will + * be useful for it's callback functions stored in + * the other fields + * + * May be `NULL`, and initialised so by the library + * + * @since `.version == 1` + */ + void *user_data; + + /** + * Called with `.user_data` (even if `.user_data` is `NULL`) + * before the library stops using the `struct` + * + * May be `NULL`, and initialised so by the library + * + * @param user_data `.user_data` + * + * @since `.version == 1` + */ + void (*release_user_data)(void *user_data); + + /** + * The library will call this function for every domain, + * that the library will not use, that the application in + * one of the `struct`'s fields + * + * May be `NULL`, and initialised so by the library + * + * @param domain The unused domain + * @param user_data `.user_data` + * + * @since `.version == 1` + */ + void (*dont_want_domain)(struct libnormalform_map *domain, void *user_data); + + /** + * Set by the library to a hint to the application on + * whether it would like to create a union of the two + * domains + * + * @since `.version == 1` + */ + enum libnormalform_ternary union_is_useful; + + /** + * The library will set this field to `NULL`, but + * if the application has created a union of the + * two domains, it should be stored here + * + * @since `.version == 1` + */ + struct libnormalform_map *created_union; + + /** + * The library will set this field to `NULL`, but if + * the application is able to create a union of the + * two domains, it shall store a pointer the a function + * for doing so in this field + * + * @param left The left-hand domain, will be the same as the + * left-hand domain that was input the the application + * function together with this `struct` + * @param right The right-hand domain, will be the same as the + * right-hand domain that was input the the application + * function together with this `struct` + * @param out Output parameter for the union of the two domains + * @param user_data `.user_data` + * @return 1 on success if `*out` was created, + * 0 if it turned out that a union could not be + * constructed, -1 on failure + * + * @since `.version == 1` + */ + int (*create_union)(struct libnormalform_map *left, struct libnormalform_map *right, + struct libnormalform_map *out, void *user_data); }; -struct libnormalform_analysers { /* TODO doc */ + +/** + * Callback functions for comparing atomic sentences + * and for comparing domains + */ +struct libnormalform_analysers { + /** + * The application can store any data here that will + * be useful for it's callback functions stored in + * the other fields + * + * May be `NULL` + */ void *user_data; - int (*compare_variable_to_variable)(void *user_data, struct libnormalform_atom_comparsion *result, - struct libnormalform_variable *left, struct libnormalform_variable *right); - int (*compare_function_to_function)(void *user_data, struct libnormalform_atom_comparsion *result, - struct libnormalform_function *left, struct libnormalform_function *right); - int (*compare_variable_to_function)(void *user_data, struct libnormalform_atom_comparsion *result, - struct libnormalform_variable *left, struct libnormalform_function *right); - int (*compare_domains)(void *user_data, struct libnormalform_domain_comparsion *result, - struct libnormalform_map *left, struct libnormalform_map *right); + + /** + * Callback function for comparing two variables + * + * @param left The left-hand atomic sentience (variable) + * @param right The right-hand atomic sentience (variable) + * @param result Structure where the application shall store results + * @param user_data `.user_data` + * @return 1 on success and a comparison was made, + * 0 on success but the sentences were incommensurable, + * -1 on failure + * + * May be `NULL` + */ + int (*compare_variable_to_variable)(struct libnormalform_variable *left, struct libnormalform_variable *right, + struct libnormalform_atom_comparison *result, void *user_data); + + /** + * Callback function for comparing two functions + * + * @param left The left-hand atomic sentience (function) + * @param right The right-hand atomic sentience (function) + * @param result Structure where the application shall store results + * @param user_data `.user_data` + * @return 1 on success and a comparison was made, + * 0 on success but the sentences were incommensurable, + * -1 on failure + * + * May be `NULL` + */ + int (*compare_function_to_function)(struct libnormalform_function *left, struct libnormalform_function *right, + struct libnormalform_atom_comparison *result, void *user_data); + + /** + * Callback function for comparing a variable and a function + * + * @param left The left-hand atomic sentience (variable) + * @param right The right-hand atomic sentience (function) + * @param result Structure where the application shall store results + * @param user_data `.user_data` + * @return 1 on success and a comparison was made, + * 0 on success but the sentences were incommensurable, + * -1 on failure + * + * May be `NULL` + */ + int (*compare_variable_to_function)(struct libnormalform_variable *left, struct libnormalform_function *right, + struct libnormalform_atom_comparison *result, void *user_data); + + /** + * Callback function for comparing two domains + * + * @param left The left-hand domain + * @param right The right-hand domain + * @param result Structure where the application shall store results + * @param user_data `.user_data` + * @return 1 on success and a comparison was made, + * 0 on success but the sentences were incommensurable, + * -1 on failure + * + * May be `NULL` + */ + int (*compare_domains)(struct libnormalform_map *left, struct libnormalform_map *right, + struct libnormalform_domain_comparison *result, void *user_data); }; @@ -1057,7 +1590,7 @@ struct libnormalform_analysers { /* TODO doc */ * Qualifier */ struct libnormalform_qualification { - struct libnormalform_map *map; /**< The domain of interest */ + struct libnormalform_map *domain; /**< The domain of interest */ struct libnormalform_term *antecedent; /**< The antecedent, `NULL` if joined with the predicate */ struct libnormalform_term *predicate; /**< The predicate */ }; @@ -1100,14 +1633,14 @@ struct libnormalform_term { */ union { /** - * Use if `.type` is `LIBNORMALFORM_DISJUNCTION` + * Use if `.type` is `LIBNORMALFORM_CONJUNCTION` */ - struct libnormalform_clause disjunction; + struct libnormalform_clause conjunction; /** - * Use if `.type` is `LIBNORMALFORM_CONJUNCTION` + * Use if `.type` is `LIBNORMALFORM_DISJUNCTION` */ - struct libnormalform_clause conjunction; + struct libnormalform_clause disjunction; /** * Use if `.type` is `LIBNORMALFORM_EXCLUSIVE_DISJUNCTION` @@ -1302,22 +1835,22 @@ int (libnormalform_evaluate)(LIBNORMALFORM_SENTENCE *this); /** - * Return an application readable expression of a statement in negation - * normal form, optionally with XOR, and reduce the statement to a - * statement that is at least as true (but as false as possible), and + * Return an application-readable expression of a sentence in negation + * normal form, optionally with XOR, and reduce the sentence to a + * sentence that is at least as true (but as false as possible), and * is minimised, according what the application specifies that it can * work with * * Before calling this function, the application shall set `.relaxation` - * `.requires_relaxation` in each `struct libnormalform_function` used - * used by the sentence. `.requires_relaxation` may be set as 0 if the + * and `.requires_relaxation` in each `struct libnormalform_function` used + * used in the sentence. `.requires_relaxation` may be set to 0 if the * function shall not be replaced (in this case `.relaxation` need not * be set), but set to 1 if the function most be replaced with a more * true function. In the latter case, `.relaxation` shall either be set - * to the new function or to `NULL`; if set to null, the function is - * reduced to a tautological sentence. For any `libnormalform_transformer` + * to the new function or to `NULL`; if set to `NULL`, the function is + * reduced to a tautological sentence. For any `struct libnormalform_transformer` * it must also set `.requires_elimination` to 1 if the transformation - * must be replaces with a tautology, and 0 otherwise. + * must be replaces with a tautology, and to 0 otherwise. * * @param this The sentence to describe * @param flags The bitwise OR of any number of the following values: @@ -1325,9 +1858,10 @@ int (libnormalform_evaluate)(LIBNORMALFORM_SENTENCE *this); * - LIBNORMALFORM_AVOID_NEGATED_FOR_ALL: Prefer ∃x.¬φ over ¬∀x.φ * - LIBNORMALFORM_AVOID_FOR_ANY: Prefer ¬∀x.¬φ over ∃x.φ * - LIBNORMALFORM_AVOID_NEGATED_FOR_ANY: Prefer ∀x.¬φ over ¬∃x.φ - * - LIBNORMALFORM_RELAX_FOR_ONE: Relax any positive ∃!x.φ into ∃x.φ - * - LIBNORMALFORM_REDUCE_XOR: Do not use XOR in the returned statement, + * - LIBNORMALFORM_REDUCE_XOR: Do not use XOR in the returned sentence, * but transform it to negation normal form + * - LIBNORMALFORM_RELAX_XOR Relax any XOR or OR + * (nullified by `LIBNORMALFORM_REDUCE_XOR`) * - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL Express φ(x)∀x:θ(x) on the form ∀x.(θ(x) → φ(x)) * - LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL Express ¬(φ(x)∀x:θ(x)) on the form ¬∀x.(θ(x) → φ(x)) * - LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY Express φ(x)∃x:θ(x) on the form ∃x.(θ(x) ∧ φ(x)) @@ -1337,72 +1871,123 @@ int (libnormalform_evaluate)(LIBNORMALFORM_SENTENCE *this); * - LIBNORMALFORM_ELIMINATE_FOR_ALL Relax any non-translatable ∀x.φ to ⊤ * - LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL Relax any non-translatable ¬∀x.φ to ⊤ * - LIBNORMALFORM_ELIMINATE_FOR_ANY Relax any non-translatable ∃x.φ to ⊤ - * - LIBNORMALFORM_ELIMINATE_IN_NEGATED_FOR_ANY Relax any non-translatable ¬∃x.φ to ⊤ - * - LIBNORMALFORM_ELIMINATE_IN_FOR_ONE Relax any non-translatable ∃!x.φ to ⊤ - * - LIBNORMALFORM_ELIMINATE_IN_NEGATED_FOR_ONE Relax any ¬∃!x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY Relax any non-translatable ¬∃x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_FOR_ONE Relax any non-translatable ∃!x.φ to ⊤ + * - LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE Relax any ¬∃!x.φ to ⊤ * - LIBNORMALFORM_ELIMINATE_VARIABLE Relax any positive variable literal to ⊤ * - LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE Relax any negative variable literal to ⊤ * - LIBNORMALFORM_ELIMINATE_FUNCTION Relax any positive function literal to ⊤ * - LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION Relax any negative function literal to ⊤ - * - LIBNORMALFORM_ELIMINATE_XOR Remove all XOR's (nullified by `LIBNORMALFORM_REDUCE_XOR`) - * @param analysers Application provided functions to help reduce the statement, or `NULL` + * - LIBNORMALFORM_DISTRIBUTE_QUALIFIERS Express (⋀ᵩφ(y) ∀ ⟨x,y⟩ ∈ D : α(x)) as + * ⋀ᵩ(φ(y) ∀ ⟨x,y⟩ ∈ D : α(x)), + * express ¬(⋀ᵩφ(y) ∀ ⟨x,y⟩ ∈ D : α(x)) as + * ⋁ᵩ¬(φ(y) ∀ ⟨x,y⟩ ∈ D : α(x)), + * express (⋁ᵩφ(y) ∃ ⟨x,y⟩ ∈ D : α(x)) as + * ⋁ᵩ(φ(y) ∃ ⟨x,y⟩ ∈ D : α(x), and + * express ¬(⋁ᵩφ(y) ∃ ⟨x,y⟩ ∈ D : α(x)) as + * ⋀ᵩ¬(φ(y) ∃ ⟨x,y⟩ ∈ D : α(x)); + * where α may be tautology (represented as `NULL`), + * and instead φ(y) would be φ({x,y}), due to + * `LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL`, + * `LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ALL`, + * `LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY`, or + * `LIBNORMALFORM_JOIN_SIDES_IN_NEGATED_FOR_ANY` + * @param analysers Application provided functions to help reduce the sentence, or `NULL` * @return The description of the sentence, `NULL` on failure; * the returned pointer shall be deallocated with * `libnormalform_free` when it is no longer needed * + * @throws ENOMEM Insufficient memory available + * @throws EINVAL `flags` contained unsupported options + * * @seealso libnormalform_dnf * @seealso libnormalform_cnf + * @seealso libnormalform_cdnf */ LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1) -struct libnormalform_term *(libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO man */ +struct libnormalform_term *(libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers); /** - * Variant of `libnormalform_express` that always canonicalises - * the statement to disjunctive normal form + * Variant of `libnormalform_express` that always normalises + * the sentence to disjunctive normal form * * @param this The sentence to describe - * @param flags See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR` + * @param flags See `libnormalform_express`; `LIBNORMALFORM_RELAX_XOR` * is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not, * but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless * there is a risk that it would be too costly (EXPSPACE) - * @param analysers Application provided functions to help reduce the statement, or `NULL` + * @param analysers Application provided functions to help reduce the sentence, or `NULL` * @return The description of the sentence, `NULL` on failure; * the returned pointer shall be deallocated with * `libnormalform_free` when it is no longer needed * + * @throws ENOMEM Insufficient memory available + * @throws EINVAL `flags` contained unsupported options + * * @seealso libnormalform_express + * @seealso libnormalform_cdnf * @seealso libnormalform_cnf */ LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1) -struct libnormalform_term *(libnormalform_dnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO */ /* TODO man */ +struct libnormalform_term *(libnormalform_dnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers); /** - * Variant of `libnormalform_express` that always canonicalises - * the statement to conjuctive normal form + * Variant of `libnormalform_express` that always normalises + * the sentence to conjuctive normal form * * @param this The sentence to describe - * @param flags See `libnormalform_express`; `LIBNORMALFORM_ELIMINATE_XOR` + * @param flags See `libnormalform_express`; `LIBNORMALFORM_RELAX_XOR` * is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not, * but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless * there is a risk that it would be too costly (EXPSPACE) - * @param analysers Application provided functions to help reduce the statement, or `NULL` + * @param analysers Application provided functions to help reduce the sentence, or `NULL` * @return The description of the sentence, `NULL` on failure; * the returned pointer shall be deallocated with * `libnormalform_free` when it is no longer needed * + * @throws ENOMEM Insufficient memory available + * @throws EINVAL `flags` contained unsupported options + * * @seealso libnormalform_express * @seealso libnormalform_dnf + * @seealso libnormalform_cdnf */ LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1) -struct libnormalform_term *(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, /* TODO */ /* TODO man */ +struct libnormalform_term *(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers); /** + * Variant of `libnormalform_express` that always normalises + * the sentence to canonical disjunctive normal form + * + * @param this The sentence to describe + * @param flags See `libnormalform_express`; `LIBNORMALFORM_RELAX_XOR` + * is always applied, however `LIBNORMALFORM_REDUCE_XOR` is not, + * but the user is adviced use `LIBNORMALFORM_REDUCE_XOR` unless + * there is a risk that it would be too costly (EXPSPACE) + * @param analysers Application provided functions to help reduce the sentence, or `NULL` + * @return The description of the sentence, `NULL` on failure; + * the returned pointer shall be deallocated with + * `libnormalform_free` when it is no longer needed + * + * @throws ENOMEM Insufficient memory available + * @throws EINVAL `flags` contained unsupported options + * + * @seealso libnormalform_express + * @seealso libnormalform_dnf + * @seealso libnormalform_cnf + */ +LIBNORMALFORM_USE_RESULT__ LIBNORMALFORM_FREE_WITH__(libnormalform_free) LIBNORMALFORM_ONE_NONNULL_INPUT__(1) +struct libnormalform_term *(libnormalform_cdnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, + const struct libnormalform_analysers *analysers); + + +/** * Convert a sentence object to a string that can be parsed * by `libnormalform_from_string` (and is somewhat human-readable) * @@ -1415,9 +2000,8 @@ struct libnormalform_term *(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uin * (e.g., eithout there being a NUL-terminator) * * Note that when a sentence is created, it is optimised and - * reduced into fewer types of connetives (it's reducted into - * negation normal form, except with XOR allowed, but not - * necessarily to any canonical form) during construction, + * reduced into fewer types of connetives (it's reduced into + * negation normal form, except with XOR allowed) during construction, * so this function will not necessarily reproduce the sentence * as it was specified when it was constructed. * @@ -1621,7 +2205,7 @@ LIBNORMALFORM_SENTENCE *(libnormalform_not)(LIBNORMALFORM_SENTENCE *x); * - ∀x∈D.P(x) → ⊤ = ⊤ * - ∀x∈D.⊥ → Q(x) = ⊤ * - ∀x∈D.⊤ → ⊥ ⊨ D = ∅ - * - Conjunction + * - Conjunction: (⋀ᵩ(φ(y)) ∀ ⟨x,y⟩ ∈ D : α(x)) = ⋀ᵩ(φ(y) ∀ ⟨x,y⟩ ∈ D : α(x)) * * Commonly written "∀" ("∀x∈d.k(x) → v(x)", "∀x∈d (k(x) → v(x))", or "v(x) ∀ x∈d : k(x)") * @@ -1664,7 +2248,7 @@ LIBNORMALFORM_SENTENCE *(libnormalform_all)(struct libnormalform_map *d, LIBNORM * - ∃x∈D.P(x) ∧ ⊥ = ⊥ * - ∃x∈D.⊥ ∧ Q(x) = ⊥ * - ∃x∈D.⊤ ∧ ⊤ ⊨ D ⊃ ∅ - * - Disjunction + * - Disjunction: (⋁ᵩ(φ(y)) ∃ ⟨x,y⟩ ∈ D : α(x)) = ⋁ᵩ(φ(y) ∃ ⟨x,y⟩ ∈ D : α(x)) * * Commonly written "∃" ("∃x∈d.k(x) ∧ v(x)", "∃x∈d (k(x) ∧ v(x))", or "v(x) ∃ x∈d : k(x)") * @@ -1868,7 +2452,7 @@ LIBNORMALFORM_SENTENCE *(libnormalform_or)(LIBNORMALFORM_SENTENCE **xs); * Commonly written "⊕" ("⨁" if n-ary), "⊻", "↮", "⇎", "≢", or "^" * * Note that the name Exclusive disjunction is misleading - * when there are more than two terms, as the statement + * when there are more than two terms, as the sentence * will not check that exactly one term is true, but rather * calculate the parity of the terms. * @@ -2240,7 +2824,7 @@ LIBNORMALFORM_SENTENCE *(libnormalform_nif)(LIBNORMALFORM_SENTENCE **xs); /** * NIMPLY: Material nonimplication * - * Also known as NIMPLIES, BUT NOT or Material abjunction + * Also known as NIMPLIES, NOT..WITH, BUT NOT or Material abjunction * * Creates a chain where any condition must be more * satisfied than the condition left to it (xs[0] < xs[1]) |