diff options
Diffstat (limited to 'common.h')
| -rw-r--r-- | common.h | 311 |
1 files changed, 311 insertions, 0 deletions
@@ -1,4 +1,7 @@ /* See LICENSE file for copyright and license details. */ +#ifndef COMMON_H +#define COMMON_H + #ifndef LIBNORMALFORM_ALLOW_BAD_WARNINGS # define LIBNORMALFORM_ALLOW_BAD_WARNINGS #endif @@ -13,6 +16,22 @@ #if defined(__GNUC__) +# pragma GCC diagnostic ignored "-Wpadded" +# if defined(__clang__) +# pragma GCC diagnostic ignored "-Wcomma" +# pragma GCC diagnostic ignored "-Wcovered-switch-default" +# pragma GCC diagnostic ignored "-Wdisabled-macro-expansion" /* stupid, and exist in system header files */ +# pragma GCC diagnostic ignored "-Wunsafe-buffer-usage" /* clang is currently exceptionally stupid */ +# pragma GCC diagnostic ignored "-Wimplicit-fallthrough" /* clang requires [[fallthrough]], we use GCC-compatible comments */ +# ifdef TEST +# pragma GCC diagnostic ignored "-Wgnu-zero-variadic-macro-arguments" +# pragma GCC diagnostic ignored "-Wsentinel" +# endif +# endif +#endif + + +#if defined(__GNUC__) # define PURE __attribute__((__pure__)) # define CONST __attribute__((__const__)) # define HIDDEN __attribute__((__visibility__("hidden"))) @@ -118,6 +137,16 @@ /** + * Normal forms + */ +enum normal_form { + NNF, /**< Negation normal form, optinally with XOR */ + DNF, /**< Disjunctive normal form */ + CNF /**< Conjunctive normal form */ +}; + + +/** * Sentence classification */ enum type { @@ -293,6 +322,86 @@ struct libnormalform_sentence { /** + * Temporary data type for conversion between + * `LIBNORMALFORM_SENTENCE *` and `struct libnormalform_term *` + * + * For connective-clauses, `.nterms` can be any value + * (except exclusive disjunction is converted into + * inclusive disjunction if the clause becomes empty), + * and `.user_item` is `NULL` + * + * For literals, `.nterms` is 0, and the atomic + * sentence (which is application-provided) is + * stored in `.user_item` + * + * For transformations, `.nterms` is 1, and the + * input is stored in `.terms[0]`, whereas the + * function morphism (which may or may not be + * application-provided) is stored in `.user_item` + * + * For qualifications, the domain is stored in + * `.user_items` and `.nterms` is either 1 or 2; + * if 1 the antecedent and predicate are jointly + * expressed in `.terms[0]`, if 2 the antecedent + * is stored in `.terms[0]` and the predicate is + * stored in `.terms[1]` + */ +struct expression { + enum libnormalform_term_type type; + + /** + * Whether the term is true more of often + * than the term it is used to represent + */ + unsigned char reduced; + + /** + * Whether the needs to be inverted, + * must be 1 or 0 + */ + unsigned char invert; + + /** + * Number of references to this object + */ + size_t refcount; + + /** + * The number of subterms + */ + size_t nterms; + + /** + * List of subterms, + * see description of `struct expression` + */ + struct expression **terms; + + /** + * Non-sentence data for the term, + * see description of `struct expression` + */ + void *user_item; +}; + +/** + * Intial values for `struct expression` + * + * @param TYPE:enum libnormalform_term_type The term's type + */ +#define EXPRESSION_INIT(TYPE)\ + ((struct expression){\ + .type = (TYPE),\ + .reduced = 0,\ + .invert = 0,\ + .refcount = 1,\ + .nterms = 0,\ + .terms = NULL,\ + .user_item = NULL\ + }) + + +/** * Helper macro to make macros type self, for macros that take sentences */ #define REQ_SENTENCE(OBJ, ASTERISKS, EXP) _Generic((OBJ), LIBNORMALFORM_SENTENCE ASTERISKS: (EXP)) @@ -440,6 +549,206 @@ size_t (libnormalform_set_indices_and_counts__)(LIBNORMALFORM_SENTENCE *this); HIDDEN NONNULL_INPUT void (libnormalform_reset_indices_and_counts__)(LIBNORMALFORM_SENTENCE *this); +/** + * This function implements `libnormalform_express`, + * `libnormalform_dnf`, `libnormalform_cnf`, or + * `libnormalform_cdnf`, depending on `form` and + * `canonicalise` + * + * See above mentions functions for more information + * + * @param this The sentence to describe + * @param flags Refer to `libnormalform_express` (`LIBNORMALFORM_RELAX_XOR` + * is _not_ implied when `form` is `DNF` or `CNF`) + * @param analysers Refer to `libnormalform_express` + * @param form One of the following values: + * - NNF: Implement `libnormalform_express` + * - DNF: Implement `libnormalform_dnf` + * - CNF: Implement `libnormalform_cnf` + * @param canonicalise `NULL` or pointer to callback function to use + * to canonicalise the expression (used togather with + * `form == DNF` to implement `libnormalform_cdnf`); + * the first argument will be the final form of `this` + * before it is returned and should be modified in place, + * argument will be `flags`; the function shall return + * 0 on success and -1 on failure + * @return Refer to `libnormalform_express` + */ +HIDDEN USE_RESULT SOME_NONNULL_INPUT(1) +struct libnormalform_term *(libnormalform_express__)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, + const struct libnormalform_analysers *analysers, enum normal_form form, + int (*canonicalise)(struct expression *this, uint64_t flags)); + +/** + * Deallocate `struct expression *` + * + * @param this The object to deallocate + */ +HIDDEN +void (libnormalform_free_expression__)(struct expression *this); + +/** + * Apply a transformation on sentence, pushing it down + * to any already existing transformation (so that they + * stack up) or literal. + * + * It is distributed over clauses (applied to each term), + * and is dropped for any constant, boolean variable, + * or qualifier + * + * All objects must have a reference count of 1 + * + * @param this The sentence to apply `transformer` on (in place) + * @param transformer The transformation function to apply over `this` + * @return 0 on success, -1 on failure + */ +HIDDEN USE_RESULT NONNULL_INPUT +int (libnormalform_apply_transformation__)(struct expression *this, enum libnormalform_builtin_transformer transformer); + +/** + * Create a binary clause + * + * All objects must have a reference count of 1 + * + * @param invert_left Whether `left` should be inverted (1, otherwise 0) + * @param left Desired left-hand proposition (inverted if `invert_left`) + * @param invert_right Whether `right` should be inverted (1, otherwise 0) + * @param right Desired right-hand proposition (inverted if `invert_right`) + * @param type The connective for the clause + * @return The described clause, `NULL` on failure + */ +HIDDEN USE_RESULT NONNULL_INPUT +struct expression *(libnormalform_make_binary__)(int invert_left, struct expression *left, + int invert_right, struct expression *right, + enum libnormalform_term_type type); + +/** + * Apply any pending inversion and apply relaxation + * that is required for the application to be able + * to create a represention of the sentence + * + * All objects must have a reference count of 1 + * + * @param this The sentence (modified in place) + * @param flags Flags from `libnormalform_express` + * @param require_inversion Pointer to the value 1 or 0, if it stores + * the value 1, there is in inversion required + * (possibility in addition to `this->invert`) + * which the function may choose to apply + * provided that this would not relax the + * sentence. If it stores the value 0, it + * is ignored. If the function applies the + * inversion marked by `require_inversion`, + * it will set the value to 0. + * @param reduced Should point to the value 0 (if called from, + * another function), and will be set to 1 + * if the sentence was modified such that it + * is not logically equivalent to input sentence + * @return 0 on success, -1 on failure + */ +HIDDEN USE_RESULT NONNULL_INPUT +int (libnormalform_fix_presentation__)(struct expression *this, uint64_t flags, unsigned char *require_inversion, int *reduced); + +/** + * Compare two `struct expression`'s, which are literals + * or qualifiers, for sorting, where both items have one + * level of indirection + * + * For any items x and y such that x ≺ y, x ≺ ¬x ≺ y ≺ ¬y + * + * @param a Left-hand item + * @param b Rigth-hand item + * @return Negative if the left-hand should be first, + * positive if the right-hand should be first + * 0 if the items are identical; the absolute + * value is 1 i the terms are each other's + * inverse, 2 they are otherwise different + */ +HIDDEN PURE USE_RESULT NONNULL_INPUT +int (libnormalform_literal_cmp__)(struct expression *a, struct expression *b); + +/** + * Compare two `struct expression`'s, which are literals + * or qualifiers, for sorting, where both items have two + * levels of indirection + * + * For any items x and y such that x ≺ y, x ≺ ¬x ≺ y ≺ ¬y + * + * @param a Left-hand item + * @param b Rigth-hand item + * @return Negative if the left-hand should be first, + * positive if the right-hand should be first + * 0 if the items are identical; the absolute + * value is 1 i the terms are each other's + * inverse, 2 they are otherwise different + */ +HIDDEN PURE USE_RESULT NONNULL_INPUT +int (libnormalform_literal_sort_cmp__)(const void *a, const void *b); + +/** + * Compare two `struct expression`'s, which are clauses, + * for sorting, where both items have one level of indirection + * + * @param a Left-hand item + * @param b Rigth-hand item + * @return -1 if the left-hand should be first, + * +1 if the right-hand should be first + * 0 if the items are identical + */ +HIDDEN PURE USE_RESULT NONNULL_INPUT +int (libnormalform_clause_cmp__)(struct expression *a, struct expression *b); + +/** + * Compare two `struct expression`'s, which are clauses, + * for sorting, where both items have two levels of indirection + * + * @param a Left-hand item + * @param b Rigth-hand item + * @return -1 if the left-hand should be first, + * +1 if the right-hand should be first + * 0 if the items are identical + */ +HIDDEN PURE USE_RESULT NONNULL_INPUT +int (libnormalform_clause_sort_cmp__)(const void *a, const void *b); + +/** + * Check whether one clause contains another clause + * + * @param this The proposed superclause, most be recursively sorted + * @param clause The proposed subclause, most be sorted + * @param ignore Index of term to ignore in `this` + * @return 1 if `this` contains `clause`, 0 otherwise + */ +HIDDEN PURE USE_RESULT NONNULL_INPUT +int (libnormalform_contains_clause__)(struct expression *this, struct expression *clause, size_t ignore); + +/** + * Convert a sentence expressed in the temporary type + * `struct expression *` into the application-readable + * type `struct libnormalform_term *` without any + * transformations of the sentece + * + * @param out Output parameter for the application-readable representation + * @param this The sentence to convert + * @return 0 on success, -1 on failure + */ +HIDDEN USE_RESULT NONNULL_INPUT +int (libnormalform_expression_to_term__)(struct libnormalform_term *out, struct expression *this); + +/** + * Get the dependency of the values between two sentences + * + * @param left The left-hand sentence + * @param right The right-hand sentence + * @param analysers Application-provided analysis functions, or `NULL` + * @param relationship_out Output parameter for the relationship + * @return 0 on success, -1 on failure + */ +HIDDEN PURE USE_RESULT SOME_NONNULL_INPUT(1, 2, 4) +int (libnormalform_get_relationship__)(struct expression *left, struct expression *right, + const struct libnormalform_analysers *analysers, + enum libnormalform_sentence_relationship *relationship_out); + #ifdef DEBUG /* libnormalform_to_string.c */ @@ -630,3 +939,5 @@ vatrampoline(LIBNORMALFORM_SENTENCE *(*f)(size_t, LIBNORMALFORM_SENTENCE *, va_l DO_TEST /* no indent before, breaking the word TO|DO to hide from grep */ CONST int main(void) {return 0;} #endif + +#endif |