diff options
Diffstat (limited to '')
71 files changed, 4939 insertions, 1042 deletions
@@ -1,6 +1,6 @@ ISC License -© 2024 Mattias Andrée <maandree@kth.se> +© 2024, 2025, 2026 Mattias Andrée <m@maandree.se> Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above @@ -22,6 +22,9 @@ OBJ_PUBLIC =\ libnormalform_clone.o\ libnormalform_evaluate.o\ libnormalform_express.o\ + libnormalform_dnf.o\ + libnormalform_cnf.o\ + libnormalform_cdnf.o\ libnormalform_to_string.o\ libnormalform_from_string.o\ libnormalform_variable.o\ @@ -111,7 +114,7 @@ OBJ_PUBLIC =\ libnormalform_nor2.o\ libnormalform_xnor2.o\ libnormalform_nif2.o\ - libnormalform_nimply2.o\ + libnormalform_nimply2.o OBJ =\ $(OBJ_PUBLIC)\ @@ -119,7 +122,19 @@ OBJ =\ libnormalform_or2__.o\ libnormalform_xor2__.o\ libnormalform_set_indices_and_counts__.o\ - libnormalform_reset_indices_and_counts__.o + libnormalform_reset_indices_and_counts__.o\ + libnormalform_express__.o\ + libnormalform_free_expression__.o\ + libnormalform_apply_transformation__.o\ + libnormalform_make_binary__.o\ + libnormalform_fix_presentation__.o\ + libnormalform_literal_cmp__.o\ + libnormalform_literal_sort_cmp__.o\ + libnormalform_clause_cmp__.o\ + libnormalform_clause_sort_cmp__.o\ + libnormalform_contains_clause__.o\ + libnormalform_expression_to_term__.o\ + libnormalform_get_relationship__.o TOBJ = $(OBJ:.o=.to)\ libnormalform_andl_macro_test.to\ @@ -164,7 +179,19 @@ MAN3 =\ libnormalform_value.3\ LIBNORMALFORM_SENTENCE.3\ struct_libnormalform_sentence.3\ - libnormalform_sentence.3 + libnormalform_sentence.3\ + enum_libnormalform_ternary.3\ + libnormalform_ternary.3\ + struct_libnormalform_atom_comparison.3\ + libnormalform_atom_comparison.3\ + struct_libnormalform_domain_comparison.3\ + libnormalform_domain_comparison.3\ + enum_libnormalform_domain_relationship.3\ + libnormalform_domain_relationship.3\ + enum_libnormalform_sentences_relationship.3\ + libnormalform_sentences_relationship.3\ + struct_libnormalform_analysers.3\ + libnormalform_analysers.3 LOBJ = $(OBJ:.o=.lo) TEST = $(TOBJ:.to=.t) @@ -190,6 +217,8 @@ $L_nor2.to $L_norl.to $L_vnor.to $L_nor_$C.to $L_norl_$C.to $L_vn $L_xnor2.to $L_xnorl.to $L_vxnor.to $L_xnor_$C.to $L_xnorl_$C.to $L_vxnor_$C.to $L_xnorl_macro_test.to : $L_xnor.c $L_nif2.to $L_nifl.to $L_vnif.to $L_nif_$C.to $L_nifl_$C.to $L_vnif_$C.to $L_nifl_macro_test.to : $L_nif.c $L_nimply2.to $L_nimplyl.to $L_vnimply.to $L_nimply_$C.to $L_nimplyl_$C.to $L_vnimply_$C.to $L_nimplyl_macro_test.to : $L_nimply.c +libnormalform_literal_sort_cmp__.to: libnormalform_literal_cmp__.c +libnormalform_clause_sort_cmp__.to: libnormalform_clause_cmp__.c .c.o: $(CC) -c -o $@ $< $(CFLAGS) $(CPPFLAGS) @@ -1,5 +1,5 @@ NAME - libnormalform - First-order logic sentence canonicalisation library + libnormalform - First-order logic sentence normalisation library SYNOPSIS #include <libnormalform.h> @@ -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 diff --git a/libnormalform.7 b/libnormalform.7 index 1607b34..88cfc91 100644 --- a/libnormalform.7 +++ b/libnormalform.7 @@ -1,6 +1,6 @@ .TH LIBNORMALFORM 7 LIBNORMALFORM .SH NAME -libnormalform \- First-order logic sentence canonicalisation library +libnormalform \- First-order logic sentence normalisation library .SH SYNOPSIS .nf 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]) diff --git a/libnormalform_all.c b/libnormalform_all.c index 1b8d6fc..1d948fc 100644 --- a/libnormalform_all.c +++ b/libnormalform_all.c @@ -421,7 +421,7 @@ main(void) ASSERT_NOTEQUAL(a, b); libnormalform_free(b); - /* P = Q ⊭ ∀{x,y}∈X.(P(x) → Q(y)) = ∀{x,y}∈X.(P(x) → P(y)) = ∀{x,y}∈X.⊤ = ⊤ ∵ P → Q ⊭ P(x) → Q(y) */ + /* P = Q ⊭ ∀⟨x,y⟩∈X.(P(x) → Q(y)) = ∀⟨x,y⟩∈X.(P(x) → P(y)) = ∀⟨x,y⟩∈X.⊤ = ⊤ ∵ P → Q ⊭ P(x) → Q(y) */ ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), libnormalform_true())); ASSERT_NOTEQUAL(a, b); libnormalform_free(b); @@ -429,8 +429,8 @@ main(void) ASSERT_NOTEQUAL(a, b); libnormalform_free(b); - /* P = ¬Q ⊭ ∀{x,y}∈X.(P(x) → Q(y)) = ∀{x,y}∈X.(¬Q(x) → Q(y)) = ∀{x,y}∈X.(⊤ → Q(y)) ∵ P → ¬Q ⊭ P(x) → ¬Q(y) */ - /* P = ¬Q ⊭ ∀{x,y}∈X.(P(x) → Q(y)) = ∀{x,y}∈X.(P(x) → ¬P(y)) = ∀{x,y}∈X.(⊤ → ¬P(y)) ∵ P → ¬Q ⊭ P(x) → ¬Q(y) */ + /* P = ¬Q ⊭ ∀⟨x,y⟩∈X.(P(x) → Q(y)) = ∀⟨x,y⟩∈X.(¬Q(x) → Q(y)) = ∀⟨x,y⟩∈X.(⊤ → Q(y)) ∵ P → ¬Q ⊭ P(x) → ¬Q(y) */ + /* P = ¬Q ⊭ ∀⟨x,y⟩∈X.(P(x) → Q(y)) = ∀⟨x,y⟩∈X.(P(x) → ¬P(y)) = ∀⟨x,y⟩∈X.(⊤ → ¬P(y)) ∵ P → ¬Q ⊭ P(x) → ¬Q(y) */ ASSUME(b = libnormalform_all(&dom1, libnormalform_true(), REF(v2))); ASSERT_NOTEQUAL(a, b); libnormalform_free(b); diff --git a/libnormalform_any.c b/libnormalform_any.c index 7e69210..1cd79fa 100644 --- a/libnormalform_any.c +++ b/libnormalform_any.c @@ -420,7 +420,7 @@ main(void) ASSERT_NOTEQUAL(a, b); libnormalform_free(b); - /* P = Q ⊭ ∃{x,y}∈X.(P(x) ∧ Q(y)) = ∃{x,y}∈X.(P(x) ∧ P(y)) = ∃{x,y}∈X.⊤ = ⊤ ∵ P = Q ⊭ P(x) = Q(y) */ + /* P = Q ⊭ ∃⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃⟨x,y⟩∈X.(P(x) ∧ P(y)) = ∃⟨x,y⟩∈X.⊤ = ⊤ ∵ P = Q ⊭ P(x) = Q(y) */ ASSUME(b = libnormalform_any(&dom1, libnormalform_true(), libnormalform_true())); ASSERT_NOTEQUAL(a, b); libnormalform_free(b); @@ -428,8 +428,8 @@ main(void) ASSERT_NOTEQUAL(a, b); libnormalform_free(b); - /* P = ¬Q ⊭ ∃{x,y}∈X.(P(x) ∧ Q(y)) = ∃{x,y}∈X.(¬Q(x) ∧ Q(y)) = ∃{x,y}∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */ - /* P = ¬Q ⊭ ∃{x,y}∈X.(P(x) ∧ Q(y)) = ∃{x,y}∈X.(P(x) ∧ ¬P(y)) = ∃{x,y}∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */ + /* P = ¬Q ⊭ ∃⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃⟨x,y⟩∈X.(¬Q(x) ∧ Q(y)) = ∃⟨x,y⟩∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */ + /* P = ¬Q ⊭ ∃⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃⟨x,y⟩∈X.(P(x) ∧ ¬P(y)) = ∃⟨x,y⟩∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */ ASSUME(b = libnormalform_any(&dom1, libnormalform_false(), libnormalform_false())); ASSERT_NOTEQUAL(a, b); libnormalform_free(b); diff --git a/libnormalform_apply_transformation__.c b/libnormalform_apply_transformation__.c new file mode 100644 index 0000000..03af62c --- /dev/null +++ b/libnormalform_apply_transformation__.c @@ -0,0 +1,124 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +/** + * Transformation function for `LIBNORMALFORM_DOMAIN_VIEW`, + * see `.transform` of `libnormalform_transformer` for + * more information + * + * Outputs the `.key` for `input`; `input` has the type + * `struct libnormalform_mapping *` + */ +static void * +domain_view_transform(void *user_data, void *input) +{ + struct libnormalform_mapping *kvpair = input; + (void) user_data; + return kvpair->key; +} + + +/** + * Transformation function for `LIBNORMALFORM_IMAGE_VIEW`, + * see `.transform` of `libnormalform_transformer` for + * more information + * + * Outputs the `.value` for `input`; `input` has the type + * `struct libnormalform_mapping *` + */ +static void * +image_view_transform(void *user_data, void *input) +{ + struct libnormalform_mapping *kvpair = input; + (void) user_data; + return kvpair->value; +} + + +int +(libnormalform_apply_transformation__)(struct expression *this, enum libnormalform_builtin_transformer transformer) +{ + /* Only .builtin is actually needed, but the others + * could be useful for debugging by the user */ + static struct libnormalform_transformer domain_view = { + .transform = &domain_view_transform, + .deallocate = NULL, + .user_data = NULL, + .identifier = "<builtin:domain-view>", + .builtin = LIBNORMALFORM_DOMAIN_VIEW + }; + static struct libnormalform_transformer image_view = { + .transform = &image_view_transform, + .deallocate = NULL, + .user_data = NULL, + .identifier = "<builtin:image-view>", + .builtin = LIBNORMALFORM_IMAGE_VIEW + }; + + size_t i; + struct expression *new, **term_singleton; + + switch (this->type) { + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + /* transformations are morphism */ + for (i = 0; i < this->nterms; i++) + if (libnormalform_apply_transformation__(this->terms[i], transformer)) + return -1; + break; + + case LIBNORMALFORM_TRANSFORMATION: + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_NEGATED_FUNCTION: + new = malloc(sizeof(*new)); + if (!new) + return -1; + term_singleton = malloc(sizeof(*term_singleton)); + if (!term_singleton) { + free(new); + return -1; + } + *new = *this; + *this = EXPRESSION_INIT(LIBNORMALFORM_TRANSFORMATION); + this->nterms = 1; + this->terms = term_singleton; + this->terms[0] = new; + switch (transformer) { + case LIBNORMALFORM_DOMAIN_VIEW: + this->user_item = &domain_view; + break; + case LIBNORMALFORM_IMAGE_VIEW: + this->user_item = &image_view; + break; + default: + case LIBNORMALFORM_NOT_BUILT_IN: + abort(); + } + break; + + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_NEGATED_VARIABLE: + /* variables are input-independent leafs */ + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + /* qualifiers reset input */ + default: + break; + } + + return 0; +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_cdnf.c b/libnormalform_cdnf.c new file mode 100644 index 0000000..d846a45 --- /dev/null +++ b/libnormalform_cdnf.c @@ -0,0 +1,560 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +static int canonicalise_dnf(struct expression *this, uint64_t flags); + + +/** + * Invert a sentence in place, but + * require the result to be unrelaxed + * + * The sentence may not contain XOR + * + * @param this The sentence to invert (in place) + * @param flags Flags from `libnormalform_express` + * @return 1 on success, 0 if the inversion could not + * be representated without being relaxed, + * -1 on failure + * + * In case the function returns 0 or -1, `this` may + * have been partially inverted + */ +static int +perfectly_invert_expression(struct expression *this, uint64_t flags) +{ + struct expression **outer; + size_t i, j, k, ci, cn, nouter; + int r; + +beginning: + switch (this->type) { + case LIBNORMALFORM_TRANSFORMATION: + this = this->terms[0]; + goto beginning; + + case LIBNORMALFORM_DISJUNCTION: + /* ¬⋁{⋀{x | x ∈ X} | X ∈ Y} = + * ⋀{¬⋀{x | x ∈ X} | X ∈ Y} = + * ⋀{⋁{¬x | x ∈ X} | X ∈ Y} = + * ⋁{¬x₁ ∧ … ∧ ¬xₙ | x₁ ∈ X₁, …, xₙ ∈ Xₙ, {X₁, …, Xₙ} = Y} */ + outer = NULL; + nouter = 1U; + for (i = 0; i < this->nterms; i++) { + if (this->terms[i]->type != LIBNORMALFORM_CONJUNCTION) + abort(); /* this function is only used for CDNF */ + if (!this->terms[i]->nterms) { + nouter = 0; + break; + } + if (this->terms[i]->nterms > SIZE_MAX / nouter) { + errno = ENOMEM; + return -1; + } + nouter *= this->terms[i]->nterms; + } + if (!nouter) { + for (i = 0; i < this->nterms; i++) + libnormalform_free_expression__(this->terms[i]); + free(this->terms); + this->terms = NULL; + this->nterms = 0; + return 0; + } + for (i = 0; i < this->nterms; i++) { + this->reduced |= this->terms[i]->reduced; + for (j = 0; j < this->terms[i]->nterms; j++) + this->terms[i]->terms[j]->invert = 1; + } + for (i = 0; i < this->nterms; i++) { + for (j = 0; j < this->terms[i]->nterms; j++) { + if (!this->terms[i]->terms[j]->invert) + continue; + this->terms[i]->terms[j]->invert = 0; + r = perfectly_invert_expression(this->terms[i]->terms[j], flags); + if (r <= 0) + return r; + if (nouter / this->terms[i]->nterms > SIZE_MAX - this->terms[i]->terms[j]->refcount) { + errno = ENOMEM; + return -1; + } + } + } + for (i = 0; i < nouter; i++) { + outer[i] = malloc(sizeof(*outer[i])); + if (!outer[i]) + return -1; + outer[i]->type = LIBNORMALFORM_CONJUNCTION; + outer[i]->reduced = 0; + outer[i]->invert = 0; + outer[i]->refcount = 1; + outer[i]->user_item = NULL; + outer[i]->nterms = 0; + outer[i]->terms = NULL; + if (!this->nterms) + continue; + outer[i]->terms = malloc(this->nterms * sizeof(*outer[i]->terms)); + if (!outer[i]->terms) { + free(outer[i]); + while (i--) { + free(outer[i]->terms); + free(outer[i]); + } + return -1; + } + } + cn = 1U; + for (i = this->nterms; i--;) { + for (k = 0; k < nouter;) { + for (j = 0; j < this->terms[i]->nterms; j++) { + this->terms[i]->terms[j]->refcount += cn; + for (ci = 0; ci < cn; ci++) + outer[k++]->terms[i] = this->terms[i]->terms[j]; + } + } + cn *= this->terms[i]->nterms; + libnormalform_free_expression__(this->terms[i]); + this->nterms--; + } + free(this->terms); + this->terms = outer; + this->nterms = nouter; + return canonicalise_dnf(this, flags) ? -1 : 1; + + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + if (!(flags & (LIBNORMALFORM_ELIMINATE_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL)))) { + this->type ^= LIBNORMALFORM_FOR_ALL ^ LIBNORMALFORM_NEGATED_FOR_ALL; + return 1; + } + /* ¬∀x.φ = ∃x.¬φ */ + if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ALL))) + return 0; + this->type = LIBNORMALFORM_FOR_ANY + (this->type - LIBNORMALFORM_FOR_ALL); + this = this->terms[this->nterms - 1]; + goto beginning; + + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + if (!(flags & (LIBNORMALFORM_ELIMINATE_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY)))) { + this->type ^= LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY; + return 1; + } + /* ¬∃x.φ = ∀x.¬φ */ + if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ANY))) + return 0; + this->type = LIBNORMALFORM_FOR_ALL + (this->type - LIBNORMALFORM_FOR_ANY); + this = this->terms[this->nterms - 1]; + goto beginning; + + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_NEGATED_FUNCTION: + if (flags & (LIBNORMALFORM_ELIMINATE_FUNCTION << (this->type - LIBNORMALFORM_FUNCTION))) + return 0; + this->type ^= LIBNORMALFORM_FUNCTION ^ LIBNORMALFORM_NEGATED_FUNCTION; + return 1; + + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_NEGATED_VARIABLE: + if (flags & (LIBNORMALFORM_ELIMINATE_VARIABLE << (this->type - LIBNORMALFORM_VARIABLE))) + return 0; + this->type ^= LIBNORMALFORM_VARIABLE ^ LIBNORMALFORM_NEGATED_VARIABLE; + return 1; + + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + if (flags & (LIBNORMALFORM_ELIMINATE_FOR_ONE << (this->type - LIBNORMALFORM_FOR_ONE))) + return 0; + this->type ^= LIBNORMALFORM_FOR_ONE ^LIBNORMALFORM_NEGATED_FOR_ONE; + return 1; + + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: /* disallowed since we only is this for CDNF */ + case LIBNORMALFORM_CONJUNCTION: /* disallowed since we only is this for CDNF */ + default: + abort(); + } +} + + +/** + * Convert from DNF to CDNF + * + * @param this The DNF to convert to CDNF (in place) + * @param flags Flags from `libnormalform_express` + * @return 0 on success, -1 on failure + */ +static int +canonicalise_dnf(struct expression *this, uint64_t flags) +{ + struct expression *clause, *new_clause, *term, *nested_term; + struct expression *positive = NULL, **req_positives = NULL; + struct expression *negative = NULL, **req_negatives = NULL; + struct expression *have, **want, **req_unsigneds = NULL; + size_t clause_i, term_i, req_i, req_n = 0, req_size, i, max; + int cmp, ret = -1, r; + void *new, *tmp; + + if (this->type != LIBNORMALFORM_DISJUNCTION) + abort(); + + max = 0; + for (clause_i = 0; clause_i < this->nterms; clause_i++) { + clause = this->terms[clause_i]; + if (clause->type != LIBNORMALFORM_CONJUNCTION) + abort(); + if (clause->nterms > max) + max = clause->nterms; + + for (i = 0; i < clause->nterms; i++) { + switch (clause->terms[i]->type) { + case LIBNORMALFORM_TRANSFORMATION: + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_NEGATED_VARIABLE: + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_NEGATED_FUNCTION: + break; + + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + if (canonicalise_dnf(clause->terms[i], flags)) + return -1; + break; + + default: + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + abort(); + } + } + + qsort(clause->terms, clause->nterms, sizeof(*clause->terms), &libnormalform_literal_sort_cmp__); + } + req_size = max; + req_positives = malloc(req_size * sizeof(*req_positives)); + if (!req_positives) + goto fail; + req_negatives = malloc(req_size * sizeof(*req_negatives)); + if (!req_negatives) + goto fail; + req_unsigneds = malloc(req_size * sizeof(*req_unsigneds)); + if (!req_unsigneds) + goto fail; + for (clause_i = 0; clause_i < this->nterms; clause_i++) { + clause = this->terms[clause_i]; + req_i = 0; + for (term_i = 0; term_i < clause->nterms; term_i++) { + term = clause->terms[term_i]; + req_again: + if (req_i == req_n) { + req_new: + if (req_n == req_size) { + req_size += 64; + new = realloc(req_positives, req_size * sizeof(*req_positives)); + if (!new) + goto fail; + req_positives = new; + req_negatives = realloc(req_negatives, req_size * sizeof(*req_negatives)); + if (!new) + goto fail; + req_negatives = new; + req_unsigneds = realloc(req_unsigneds, req_size * sizeof(*req_unsigneds)); + if (!new) + goto fail; + req_unsigneds = new; + } + memmove(&req_positives[req_i + 1U], &req_positives[req_i], (req_n - req_i) * sizeof(*req_positives)); + memmove(&req_negatives[req_i + 1U], &req_negatives[req_i], (req_n - req_i) * sizeof(*req_negatives)); + memmove(&req_unsigneds[req_i + 1U], &req_unsigneds[req_i], (req_n - req_i) * sizeof(*req_unsigneds)); + req_positives[req_i] = NULL; + req_negatives[req_i] = NULL; + req_unsigneds[req_i] = NULL; + req_n += 1; + nested_term = term; + positivity_again: + switch (nested_term->type) { + case LIBNORMALFORM_TRANSFORMATION: + nested_term = nested_term->terms[0]; + goto positivity_again; + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_FOR_ONE: + req_positives[req_i] = term; + req_positives[req_i]->refcount += 1; + break; + case LIBNORMALFORM_NEGATED_FUNCTION: + case LIBNORMALFORM_NEGATED_VARIABLE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + req_negatives[req_i] = term; + req_negatives[req_i]->refcount += 1; + break; + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + req_unsigneds[req_i] = term; + req_unsigneds[req_i]->refcount += 1; + break; + default: + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + abort(); + } + } else if (req_positives[req_i]) { + cmp = libnormalform_literal_cmp__(term, req_positives[req_i]); + if (cmp < -1) { + goto req_new; + } else if (cmp == -1) { + abort(); + } else if (cmp == +1) { + if (!req_negatives[req_i]) { + req_negatives[req_i] = term; + term->refcount += 1; + } + } else if (cmp > +1) { + req_i++; + goto req_again; + } else { + libnormalform_free_expression__(term); + clause->terms[term_i] = req_positives[req_i]; + } + } else if (req_negatives[req_i]) { + cmp = libnormalform_literal_cmp__(term, req_negatives[req_i]); + if (cmp < -1) { + goto req_new; + } else if (cmp == -1) { + req_positives[req_i] = term; + term->refcount += 1; + } else if (cmp == +1) { + abort(); + } else if (cmp > +1) { + req_i++; + goto req_again; + } else { + libnormalform_free_expression__(term); + clause->terms[term_i] = req_negatives[req_i]; + } + } else if (req_unsigneds[req_i]) { + cmp = libnormalform_literal_cmp__(term, req_unsigneds[req_i]); + if (cmp < -1) { + goto req_new; + } else if (cmp == -1) { + req_positives[req_i] = term; + term->refcount += 1; + req_negatives[req_i] = req_unsigneds[req_i]; + req_unsigneds[req_i] = NULL; + } else if (cmp == +1) { + req_negatives[req_i] = term; + term->refcount += 1; + req_positives[req_i] = req_unsigneds[req_i]; + req_unsigneds[req_i] = NULL; + } else if (cmp > +1) { + req_i++; + goto req_again; + } else { + libnormalform_free_expression__(term); + clause->terms[term_i] = req_unsigneds[req_i]; + } + } else { + abort(); + } + } + } + qsort(this->terms, this->nterms, sizeof(*this->terms), &libnormalform_clause_sort_cmp__); + + clause_i = 0; +again: + for (; clause_i < this->nterms; clause_i++) { + clause = this->terms[clause_i]; + + if (clause->nterms < req_n) { + new = realloc(clause->terms, req_n * sizeof(*clause->terms)); + if (!new) + goto fail; + clause->terms = new; + } + + for (term_i = req_i = 0; req_i < req_n; term_i++, req_i++) { + positive = req_positives[req_i]; + negative = req_negatives[req_i]; + have = positive ? positive : negative; + have = have ? have : req_unsigneds[req_i]; + if (!have) { + /* TODO (elimination) */ + } + + if (term_i < clause->nterms) { + cmp = libnormalform_literal_cmp__(have, clause->terms[term_i]); + if (cmp >= -1) { + if (cmp > +1) + abort(); + continue; + } + } + + if (!positive && !negative) { + positive = have; + negative = malloc(sizeof(*negative)); + *negative = *positive; + negative->refcount = 1; + negative->terms = malloc(negative->nterms * sizeof(*negative->terms)); + if (!negative->terms) { + free(negative); + goto fail; + } + for (i = 0; i < negative->nterms; i++) { + negative->terms[i] = positive->terms[i]; + negative->terms[i]->refcount += 1; + } + req_positives[req_i] = positive; + req_negatives[req_i] = negative; + req_unsigneds[req_i] = NULL; + r = perfectly_invert_expression(negative, flags); + if (r < 0) + goto fail; + if (!r) { + eliminate_term: + libnormalform_free_expression__(req_positives[req_i]); + libnormalform_free_expression__(req_negatives[req_i]); + req_positives[req_i] = NULL; + req_negatives[req_i] = NULL; + /* TODO (elimination) + * the term as to be eliminated, and the clause may have + * to be moved down (and potentially eliminated) + */ + } + cmp = libnormalform_literal_cmp__(positive, negative); + if (cmp == +1) { + tmp = positive, positive = negative, negative = tmp; + req_positives[req_i] = positive; + req_negatives[req_i] = negative; + } else if (cmp != -1) { + abort(); + } + } else if (!positive || !negative) { + want = positive ? &positive : &negative; + *want = malloc(sizeof(**want)); + **want = *have; + (*want)->refcount = 1; + (*want)->terms = malloc(have->nterms * sizeof(*have->terms)); + if (!(*want)->terms) { + free(*want); + goto fail; + } + for (i = 0; i < have->nterms; i++) { + (*want)->terms[i] = have->terms[i]; + (*want)->terms[i]->refcount += 1; + } + r = perfectly_invert_expression(*want, flags); + if (r < 0) + goto fail; + if (!r) + goto eliminate_term; + } + + memmove(&clause->terms[term_i + 1U], &clause->terms[term_i], + (clause->nterms++ - term_i) * sizeof(*clause->terms)); + + clause->terms[term_i] = negative; + if (libnormalform_contains_clause__(this, clause, clause_i)) { + libnormalform_free_expression__(negative); + negative = NULL; + } + + clause->terms[term_i] = positive; + if (libnormalform_contains_clause__(this, clause, clause_i)) { + libnormalform_free_expression__(positive); + positive = NULL; + } + + if (positive) { + clause->terms[term_i] = positive; + if (!negative) + continue; + } else if (negative) { + clause->terms[term_i] = negative; + continue; + } else { + libnormalform_free_expression__(clause); + memmove(&this->terms[clause_i], &this->terms[clause_i + 1U], + (--clause->nterms - clause_i) * sizeof(*clause->terms)); + goto again; + } + + new_clause = malloc(sizeof(*new_clause)); + if (!new_clause) { + libnormalform_free_expression__(negative); + goto fail; + } + *new_clause = *clause; + new_clause->refcount = 1; + new_clause->terms = malloc(new_clause->nterms * sizeof(*new_clause->terms)); + if (!new_clause->terms) { + libnormalform_free_expression__(negative); + free(new_clause); + goto fail; + } + for (i = 0; i < new_clause->nterms; i++) { + new_clause->terms[i] = clause->terms[i]; + new_clause->terms[i]->refcount += 1; + } + + new_clause->terms[term_i]->refcount -= 1; + new_clause->terms[term_i] = negative; + + new = realloc(this->terms, (this->nterms + 1U) * sizeof(*this->terms)); + if (!new) { + libnormalform_free_expression__(new_clause); + goto fail; + } + this->terms = new; + memmove(&this->terms[clause_i + 1U], &this->terms[clause_i], + (this->nterms++ - clause_i) * sizeof(*this->terms)); + this->terms[clause_i] = new_clause; + } + if (term_i != clause->nterms) + abort(); + } + + ret = 0; +fail: + if (req_positives) { + for (i = 0; i < req_n; i++) + if (req_positives[i]) + libnormalform_free_expression__(req_positives[i]); + free(req_positives); + } + if (req_negatives) { + for (i = 0; i < req_n; i++) + if (req_positives[i]) + libnormalform_free_expression__(req_positives[i]); + free(req_positives); + } + if (req_unsigneds) { + for (i = 0; i < req_n; i++) + if (req_unsigneds[i]) + libnormalform_free_expression__(req_unsigneds[i]); + free(req_unsigneds); + } + return ret; +} + + +struct libnormalform_term * +(libnormalform_cdnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers) +{ + return libnormalform_express__(this, flags | LIBNORMALFORM_RELAX_XOR, analysers, DNF, &canonicalise_dnf); +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_clause_cmp__.c b/libnormalform_clause_cmp__.c new file mode 100644 index 0000000..407ea11 --- /dev/null +++ b/libnormalform_clause_cmp__.c @@ -0,0 +1,24 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +int +(libnormalform_clause_cmp__)(struct expression *a, struct expression *b) +{ + size_t i = 0, j = 0, n = a->nterms, m = b->nterms; + int cmp; + for (; i < n && j < m; i++, j++) { + cmp = libnormalform_literal_cmp__(a->terms[i], b->terms[j]); + if (cmp) + return cmp; + } + return (i < n) - (j < m); +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_clause_sort_cmp__.c b/libnormalform_clause_sort_cmp__.c new file mode 100644 index 0000000..de9f754 --- /dev/null +++ b/libnormalform_clause_sort_cmp__.c @@ -0,0 +1,33 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +int +(libnormalform_clause_sort_cmp__)(const void *a, const void *b) +{ + struct expression *const *ap = a, *const *bp = b; + return libnormalform_clause_cmp__(*ap, *bp); +} + + +#else + + +#if defined(__GNUC__) /* TODO remove when testing is implemented in libnormalform_clause_sort_cmp__.c */ +# pragma GCC diagnostic ignored "-Wunused-function" +# pragma GCC diagnostic ignored "-Wunused-macros" +#endif + +#define libnormalform_clause_cmp__(...) cmptrampoline(__VA_ARGS__) + +PURE static int +cmptrampoline(struct expression *a, struct expression *b) +{ + return libnormalform_clause_sort_cmp__(&a, &b); +} + +#include "libnormalform_clause_cmp__.c" + + +#endif diff --git a/libnormalform_clone.c b/libnormalform_clone.c index 3f8d01f..311b807 100644 --- a/libnormalform_clone.c +++ b/libnormalform_clone.c @@ -15,12 +15,12 @@ * @param map Sufficiently large array of already constructed clones, * will be updated with a the clone if `this` has a slot * and `NULL` is stored in the slot - * @param ap_out Output parameter for one of `this`'s substatements; + * @param ap_out Output parameter for one of `this`'s subsentences; * `NULL` will be stored in `*ap_out` if `this` does not - * have any substatements - * @param bp_out Output parameter for `this`'s other substatement; + * have any subsentences + * @param bp_out Output parameter for `this`'s other subsentence; * `NULL` will be stored in `*bp_out` if `this` does not - * have any substatements + * have any subsentences * @return The clone of `this`, `NULL` on failure */ USE_RESULT SOME_NONNULL_INPUT(1, 3, 4) diff --git a/libnormalform_cnf.c b/libnormalform_cnf.c new file mode 100644 index 0000000..d687fc6 --- /dev/null +++ b/libnormalform_cnf.c @@ -0,0 +1,17 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +struct libnormalform_term * +(libnormalform_cnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers) +{ + return libnormalform_express__(this, flags | LIBNORMALFORM_RELAX_XOR, analysers, CNF, NULL); +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_contains_clause__.c b/libnormalform_contains_clause__.c new file mode 100644 index 0000000..6736e4a --- /dev/null +++ b/libnormalform_contains_clause__.c @@ -0,0 +1,31 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +int +(libnormalform_contains_clause__)(struct expression *this, struct expression *clause, size_t ignore) +{ + size_t i; + int cmp; + if (ignore > this->nterms) + ignore = this->nterms; + for (i = 0; i < ignore; i++) { + cmp = libnormalform_clause_cmp__(clause, this->terms[i]); + if (cmp >= 0) + return !cmp; + } + for (i++; i < this->nterms; i++) { + cmp = libnormalform_clause_cmp__(clause, this->terms[i]); + if (cmp >= 0) + return !cmp; + } + return 0; +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_dnf.c b/libnormalform_dnf.c new file mode 100644 index 0000000..79f1a3d --- /dev/null +++ b/libnormalform_dnf.c @@ -0,0 +1,17 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +struct libnormalform_term * +(libnormalform_dnf)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers) +{ + return libnormalform_express__(this, flags | LIBNORMALFORM_RELAX_XOR, analysers, DNF, NULL); +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_express.c b/libnormalform_express.c index 2532488..25c4d7c 100644 --- a/libnormalform_express.c +++ b/libnormalform_express.c @@ -3,842 +3,10 @@ #ifndef TEST -struct expression { - enum libnormalform_term_type type; - unsigned char reduced; - unsigned char invert; - size_t nterms; - struct expression **terms; - void *user_item; -}; - - -static enum libnormalform_sentences_relationship -get_relationship(struct expression *l, struct expression *r, const struct libnormalform_analysers *analysers) /* TODO */ -{ - (void) l; - (void) r; - (void) analysers; - return LIBNORMALFORM_MUTUALLY_INDEPENDENT; -} - - -static void -free_expression(struct expression *this) -{ - if (this->terms) { - while (this->nterms) - free_expression(this->terms[--this->nterms]); - free(this->terms); - } - free(this); -} - - -static struct expression * -sentence_to_expression(LIBNORMALFORM_SENTENCE *this, uint64_t flags) -{ - LIBNORMALFORM_SENTENCE *left, *right, *free1 = NULL, *free2 = NULL; - struct expression *ret, *sub; - - ret = malloc(sizeof(*ret)); - if (!ret) - return NULL; - ret->reduced = 0; - ret->invert = 0; - ret->nterms = 0; - ret->terms = NULL; - ret->user_item = NULL; - - switch (this->type) { - case TYPE_TRUE: - tautology: - ret->type = LIBNORMALFORM_CONJUNCTION; - goto out; - - case TYPE_FALSE: - contradiction: - ret->type = LIBNORMALFORM_DISJUNCTION; - goto out; - - case TYPE_XOR: - if (flags & LIBNORMALFORM_REDUCE_XOR) { - /* x ⊕ y = (x ∨ y) ∧ ¬(x ∧ y) = (x ∨ y) ∧ (¬x ∨ ¬y) */ - free1 = left = libnormalform_or2(libnormalform_ref(LEFT(this)), libnormalform_ref(RIGHT(this))); - free2 = right = libnormalform_or2(LEFT(this)->inverse(LEFT(this)), RIGHT(this)->inverse(RIGHT(this))); - if (!left || !right) - goto fail; - ret->type = LIBNORMALFORM_CONJUNCTION; - goto clause_prefetched_branches; - } - ret->type = LIBNORMALFORM_EXCLUSIVE_DISJUNCTION; - goto clause; - case TYPE_AND: - ret->type = LIBNORMALFORM_CONJUNCTION; - goto clause; - case TYPE_OR: - ret->type = LIBNORMALFORM_DISJUNCTION; - clause: - left = LEFT(this); - right = RIGHT(this); - clause_prefetched_branches: - sub = sentence_to_expression(left, flags); - if (sub) - goto fail; - if (sub->type == ret->type) { - free(ret); - ret = sub; - } else if (!sub->nterms && ret->type == LIBNORMALFORM_CONJUNCTION && sub->type == LIBNORMALFORM_DISJUNCTION) { - /* ⋀(X ∪ {⋁∅}) = ⋀(X ∪ {⊥}) = ⋀X ∧ ⊥ = ⊥ */ - if (!sub->reduced) { - free_expression(sub); - goto contradiction; - } - free_expression(sub); - ret->reduced |= 1; - } else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) { - /* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */ - free_expression(ret); - ret = sub; - goto tautology; - } else { - ret->terms = malloc(sizeof(*ret->terms)); - if (!ret->terms) { - free_expression(sub); - goto fail; - } - ret->nterms = 1; - ret->terms[0] = sub; - } - sub = sentence_to_expression(right, flags); - if (sub) - goto fail; - if (sub->type == ret->type) { - void *new = realloc(ret->terms, (ret->nterms + sub->nterms) * sizeof(*ret->terms)); - if (!new) { - free_expression(sub); - goto fail; - } - ret->terms = new; - memcpy(&ret->terms[ret->nterms], sub->terms, sub->nterms * sizeof(sub->terms)); - ret->nterms += sub->nterms; - free(sub->terms); - free(sub); - } else if (!sub->nterms && ret->type == LIBNORMALFORM_CONJUNCTION && sub->type == LIBNORMALFORM_DISJUNCTION) { - /* ⋀(X ∪ {⋁∅}) = ⋀(X ∪ {⊥}) = ⋀X ∧ ⊥ = ⊥ */ - if (!sub->reduced) { - free_expression(sub); - goto contradiction; - } - free_expression(sub); - ret->reduced |= 1; - } else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) { - /* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */ - free_expression(ret); - ret = sub; - goto tautology; - } else { - void *new = realloc(ret->terms, (ret->nterms + 1U) * sizeof(*ret->terms)); - if (!new) { - free_expression(sub); - goto fail; - } - ret->terms = new; - ret->terms[ret->nterms++] = sub; - } - break; - - case TYPE_ALL: - ret->type = LIBNORMALFORM_FOR_ALL; - goto qualifier; - case TYPE_ANY: - ret->type = LIBNORMALFORM_FOR_ANY; - goto qualifier; - case TYPE_ONE: - ret->type = LIBNORMALFORM_FOR_ONE; - goto qualifier; - case TYPE_NOT_ONE: - ret->type = LIBNORMALFORM_NEGATED_FOR_ONE; - qualifier: - ret->user_item = this->data.qualifier.domain; - ret->nterms = 2; - ret->terms = malloc(2 * sizeof(*ret->terms)); - if (!ret->terms) - goto fail; - ret->terms[0] = sentence_to_expression(this->data.qualifier.antecedent, flags); - if (!ret->terms[0]) - goto fail; - ret->terms[1] = sentence_to_expression(this->data.qualifier.predicate, flags); - if (!ret->terms[1]) - goto fail; - break; - - case TYPE_VARIABLE: - if ((flags & LIBNORMALFORM_ELIMINATE_VARIABLE) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE)) - goto eliminated; - ret->user_item = this->data.literal.atom.variable; - ret->type = LIBNORMALFORM_VARIABLE + this->data.literal.inverted; - break; - - case TYPE_FUNCTION: - if ((flags & LIBNORMALFORM_ELIMINATE_FUNCTION) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION)) - goto eliminated; - ret->reduced = !!this->data.literal.atom.function->requires_relaxation; - if (!ret->reduced) - ret->user_item = this->data.literal.atom.function; - else if (this->data.literal.atom.function->relaxation) - ret->user_item = this->data.literal.atom.function->relaxation; - else - goto eliminated; - ret->type = LIBNORMALFORM_FUNCTION + this->data.literal.inverted; - break; - - case TYPE_TRANS: - if (this->data.trans.function->requires_elimination) - goto eliminated; - ret->type = LIBNORMALFORM_TRANSFORMATION; - ret->user_item = this->data.trans.function; - ret->terms = malloc(sizeof(*ret->terms)); - if (ret->terms) - goto fail; - ret->terms[0] = sentence_to_expression(this->data.trans.input, flags); - if (!ret->terms[0]) - goto fail; - break; - - default: - abort(); - } - - goto out; - -eliminated: - ret->reduced = 1; - ret->type = LIBNORMALFORM_CONJUNCTION; -out: - libnormalform_free(free1); - libnormalform_free(free2); - return ret; - -fail: - libnormalform_free(free1); - libnormalform_free(free2); - free_expression(ret); - return NULL; -} - - -static struct expression * -make_binary(int invert_left, struct expression *left, int invert_right, struct expression *right, enum libnormalform_term_type type) -{ - struct expression *ret; - ret = malloc(sizeof(*ret)); - if (!ret) - return NULL; - ret->type = type; - ret->reduced = 0; - ret->invert = 0; - ret->user_item = NULL; - ret->nterms = 0; - ret->terms = malloc(2 * sizeof(*ret->terms)); - if (!ret->terms) { - free(ret); - return NULL; - } - (ret->terms[0] = left)->invert ^= (unsigned char)invert_left; - (ret->terms[1] = right)->invert ^= (unsigned char)invert_right; - return ret; -} - - -static int -reduce_expression(struct expression *this, const struct libnormalform_analysers *analysers) -{ - enum libnormalform_sentences_relationship relationship; - struct expression *new; - size_t i, j; - - for (i = 0; i < this->nterms; i++) - if (reduce_expression(this->terms[i], analysers)) - return -1; - - switch (this->type) { - case LIBNORMALFORM_CONJUNCTION: - for (i = 0; i < this->nterms; i++) { - left_eliminated_conjunction: - for (j = i + 1; j < this->nterms; j++) { - relationship = get_relationship(this->terms[i], this->terms[j], analysers); - switch (relationship) { - case LIBNORMALFORM_MATERIAL_IMPLICATION: - case LIBNORMALFORM_IDENTICAL: - free_expression(this->terms[j]); - this->terms[j--] = this->terms[--this->nterms]; - break; - case LIBNORMALFORM_CONVERSE_IMPLICATION: - free_expression(this->terms[i]); - this->terms[i--] = this->terms[--this->nterms]; - goto left_eliminated_conjunction; - case LIBNORMALFORM_MUTUALLY_INVERSE: - case LIBNORMALFORM_MUTUALLY_EXCLUSIVE: - goto contradiction; - case LIBNORMALFORM_JOINTLY_UNDENIABLE: - case LIBNORMALFORM_MUTUALLY_INDEPENDENT: - default: - break; - } - } - } - break; - contradiction: - for (i = 0; i < this->nterms; i++) - free_expression(this->terms[i]); - free(this->terms); - this->terms = NULL; - this->nterms = 0; - this->type = LIBNORMALFORM_DISJUNCTION; - break; - - case LIBNORMALFORM_DISJUNCTION: - for (i = 0; i < this->nterms; i++) { - left_eliminated_disjunction: - for (j = i + 1; j < this->nterms; j++) { - relationship = get_relationship(this->terms[i], this->terms[j], analysers); - switch (relationship) { - case LIBNORMALFORM_IDENTICAL: - case LIBNORMALFORM_CONVERSE_IMPLICATION: - free_expression(this->terms[j]); - this->terms[j--] = this->terms[--this->nterms]; - break; - case LIBNORMALFORM_MATERIAL_IMPLICATION: - free_expression(this->terms[i]); - this->terms[i--] = this->terms[--this->nterms]; - goto left_eliminated_disjunction; - case LIBNORMALFORM_MUTUALLY_INVERSE: - case LIBNORMALFORM_JOINTLY_UNDENIABLE: - goto tautology; - case LIBNORMALFORM_MUTUALLY_EXCLUSIVE: - case LIBNORMALFORM_MUTUALLY_INDEPENDENT: - default: - break; - } - } - } - break; - tautology: - for (i = 0; i < this->nterms; i++) - free_expression(this->terms[i]); - free(this->terms); - this->terms = NULL; - this->nterms = 0; - this->type = LIBNORMALFORM_CONJUNCTION; - break; - - case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: - i = 0; - both_eliminated_exclusive_disjunction: - for (; i < this->nterms; i++) { - for (j = i + 1; j < this->nterms; j++) { - relationship = get_relationship(this->terms[i], this->terms[j], analysers); - switch (relationship) { - case LIBNORMALFORM_MATERIAL_IMPLICATION: - new = make_binary(1, this->terms[i], 0, this->terms[j], LIBNORMALFORM_CONJUNCTION); - if (!new) - return -1; - goto xor_reduced; - case LIBNORMALFORM_CONVERSE_IMPLICATION: - new = make_binary(0, this->terms[i], 1, this->terms[j], LIBNORMALFORM_CONJUNCTION); - if (!new) - return -1; - goto xor_reduced; - case LIBNORMALFORM_MUTUALLY_INVERSE: - this->invert ^= 1; - /* fall-through */ - case LIBNORMALFORM_IDENTICAL: - free_expression(this->terms[i]); - free_expression(this->terms[j]); - this->terms[i--] = this->terms[--this->nterms]; - this->terms[j--] = this->terms[--this->nterms]; - goto both_eliminated_exclusive_disjunction; - case LIBNORMALFORM_MUTUALLY_EXCLUSIVE: - new = make_binary(0, this->terms[i], 0, this->terms[j], LIBNORMALFORM_DISJUNCTION); - if (!new) - return -1; - goto xor_reduced; - case LIBNORMALFORM_JOINTLY_UNDENIABLE: - new = make_binary(1, this->terms[i], 1, this->terms[j], LIBNORMALFORM_DISJUNCTION); - if (!new) - return -1; - goto xor_reduced; - case LIBNORMALFORM_MUTUALLY_INDEPENDENT: - default: - break; - xor_reduced: - free_expression(this->terms[i]); - free_expression(this->terms[j]); - this->terms[j--] = this->terms[--this->nterms]; - this->terms[i] = new; - goto both_eliminated_exclusive_disjunction; - } - } - } - if (!this->nterms) { - if (this->invert) { - this->invert = 0; - this->type = LIBNORMALFORM_CONJUNCTION; - } else { - this->type = LIBNORMALFORM_DISJUNCTION; - } - } - break; - - case LIBNORMALFORM_TRANSFORMATION: - case LIBNORMALFORM_VARIABLE: - case LIBNORMALFORM_NEGATED_VARIABLE: - case LIBNORMALFORM_FUNCTION: - case LIBNORMALFORM_NEGATED_FUNCTION: - case LIBNORMALFORM_FOR_ALL: - case LIBNORMALFORM_NEGATED_FOR_ALL: - case LIBNORMALFORM_FOR_ANY: - case LIBNORMALFORM_NEGATED_FOR_ANY: - case LIBNORMALFORM_FOR_ONE: - case LIBNORMALFORM_NEGATED_FOR_ONE: - default: - return 0; - } - - if (this->nterms == 1) { - new = this->terms[0]; - free(this->terms); - new->invert ^= this->invert; - *this = *new; - free(new); - } - - return 0; -} - - -static void * -domain_view_transform(void *user_data, void *input) -{ - struct libnormalform_mapping *kvpair = input; - (void) user_data; - return kvpair->key; -} - - -static void * -image_view_transform(void *user_data, void *input) -{ - struct libnormalform_mapping *kvpair = input; - (void) user_data; - return kvpair->value; -} - - -static int -apply_transformation(struct expression *this, enum libnormalform_builtin_transformer transformer) -{ - /* Only .builtin is actually needed, but the others - * could be useful for debugging by the user */ - static struct libnormalform_transformer domain_view = { - .transform = &domain_view_transform, - .deallocate = NULL, - .user_data = NULL, - .identifier = "<builtin:domain-view>", - .builtin = LIBNORMALFORM_DOMAIN_VIEW - }; - static struct libnormalform_transformer image_view = { - .transform = &image_view_transform, - .deallocate = NULL, - .user_data = NULL, - .identifier = "<builtin:image-view>", - .builtin = LIBNORMALFORM_IMAGE_VIEW - }; - - size_t i; - struct expression *new, **term_singleton; - - switch (this->type) { - case LIBNORMALFORM_CONJUNCTION: - case LIBNORMALFORM_DISJUNCTION: - case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: - /* transformations are morphism */ - for (i = 0; i < this->nterms; i++) - if (apply_transformation(this->terms[i], transformer)) - return -1; - break; - - case LIBNORMALFORM_TRANSFORMATION: - case LIBNORMALFORM_FUNCTION: - case LIBNORMALFORM_NEGATED_FUNCTION: - new = malloc(sizeof(*new)); - if (!new) - return -1; - term_singleton = malloc(sizeof(*term_singleton)); - if (!term_singleton) { - free(new); - return -1; - } - *new = *this; - this->type = LIBNORMALFORM_TRANSFORMATION; - this->reduced = 0; - this->invert = 0; - this->nterms = 1; - this->terms = term_singleton; - this->terms[0] = new; - switch (transformer) { - case LIBNORMALFORM_DOMAIN_VIEW: - this->user_item = &domain_view; - break; - case LIBNORMALFORM_IMAGE_VIEW: - this->user_item = &image_view; - break; - default: - case LIBNORMALFORM_NOT_BUILT_IN: - abort(); - } - break; - - case LIBNORMALFORM_VARIABLE: - case LIBNORMALFORM_NEGATED_VARIABLE: - /* variables are input-independent leafs */ - case LIBNORMALFORM_FOR_ALL: - case LIBNORMALFORM_NEGATED_FOR_ALL: - case LIBNORMALFORM_FOR_ANY: - case LIBNORMALFORM_NEGATED_FOR_ANY: - case LIBNORMALFORM_FOR_ONE: - case LIBNORMALFORM_NEGATED_FOR_ONE: - /* qualifiers reset input */ - default: - break; - } - - return 0; -} - - -static int -fix_presentation(struct expression *this, uint64_t flags, unsigned char *require_inversion, int *reduced) -{ -#define WILL_ELIMINATE(BASETYPE, INVERT)\ - (flags & (LIBNORMALFORM_ELIMINATE_##BASETYPE <<\ - ((this->type ^ ((LIBNORMALFORM_##BASETYPE ^ LIBNORMALFORM_NEGATED_##BASETYPE) *\ - (INVERT))) -\ - LIBNORMALFORM_##BASETYPE))) - - size_t i; - unsigned char zero = 0; - struct expression *new; - - switch (this->type) { - case LIBNORMALFORM_CONJUNCTION: - case LIBNORMALFORM_DISJUNCTION: - this->type ^= LIBNORMALFORM_CONJUNCTION ^ LIBNORMALFORM_DISJUNCTION; - if (this->invert) { - if (*require_inversion) { - this->invert ^= 1; - *require_inversion = 0; - } - for (i = 0; i < this->nterms; i++) - this->terms[i]->invert ^= 1; - } - require_inversion = &zero; - break; - - case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: - if (!this->nterms) - abort(); - if (*require_inversion) { - this->invert ^= 1; - *require_inversion = 0; - } - if (flags & LIBNORMALFORM_ELIMINATE_XOR) - goto eliminate; - for (i = 0; i < this->nterms; i++) - if (fix_presentation(this->terms[i], flags, &this->invert, reduced)) - return -1; - if (this->invert) { - this->invert = 0; - this->terms[0]->invert ^= 1; - if (fix_presentation(this->terms[0], flags, &zero, reduced)) - return -1; - } - return 0; - - case LIBNORMALFORM_VARIABLE: - case LIBNORMALFORM_NEGATED_VARIABLE: - if (!WILL_ELIMINATE(VARIABLE, this->invert ^ *require_inversion)) { - this->invert ^= *require_inversion; - *require_inversion = 0; - } else if (WILL_ELIMINATE(VARIABLE, this->invert)) { - goto eliminate; - } - this->type ^= (LIBNORMALFORM_VARIABLE ^ LIBNORMALFORM_NEGATED_VARIABLE) * this->invert; - break; - - case LIBNORMALFORM_FUNCTION: - case LIBNORMALFORM_NEGATED_FUNCTION: - if (!WILL_ELIMINATE(FUNCTION, this->invert ^ *require_inversion)) { - this->invert ^= *require_inversion; - *require_inversion = 0; - } else if (WILL_ELIMINATE(FUNCTION, this->invert)) { - goto eliminate; - } - this->type ^= (LIBNORMALFORM_FUNCTION ^ LIBNORMALFORM_NEGATED_FUNCTION) * this->invert; - break; - - case LIBNORMALFORM_TRANSFORMATION: - this->terms[0]->invert ^= this->invert; - break; - - case LIBNORMALFORM_FOR_ALL: - case LIBNORMALFORM_NEGATED_FOR_ALL: - if (!WILL_ELIMINATE(FOR_ALL, this->invert ^ *require_inversion)) { - this->invert ^= *require_inversion; - *require_inversion = 0; - } else if (WILL_ELIMINATE(FOR_ALL, this->invert)) { - goto eliminate; - } - this->type ^= (LIBNORMALFORM_FOR_ALL ^ LIBNORMALFORM_NEGATED_FOR_ALL) * this->invert; - this->invert = 0; - if (flags & (LIBNORMALFORM_AVOID_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL))) { - this->terms[this->nterms - 1]->invert ^= 1; - this->type = LIBNORMALFORM_AVOID_NEGATED_FOR_ANY - (this->type - LIBNORMALFORM_FOR_ALL); - goto for_any_maybe_join_sides; - } - for_all_maybe_join_sides: - if (this->nterms > 1) - break; - if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL))) - goto for_all_join_sides; - break; - - case LIBNORMALFORM_FOR_ANY: - case LIBNORMALFORM_NEGATED_FOR_ANY: - if (!WILL_ELIMINATE(FOR_ANY, this->invert ^ *require_inversion)) { - this->invert ^= *require_inversion; - *require_inversion = 0; - } else if (WILL_ELIMINATE(FOR_ANY, this->invert)) { - goto eliminate; - } - this->type ^= (LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY) * this->invert; - for_any: - this->invert = 0; - if (flags & (LIBNORMALFORM_AVOID_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY))) { - this->terms[this->nterms - 1]->invert ^= 1; - this->type = LIBNORMALFORM_AVOID_NEGATED_FOR_ALL - (this->type - LIBNORMALFORM_FOR_ANY); - goto for_all_maybe_join_sides; - } - for_any_maybe_join_sides: - if (this->nterms > 1) - break; - if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY))) - goto for_any_join_sides; - break; - - case LIBNORMALFORM_FOR_ONE: - case LIBNORMALFORM_NEGATED_FOR_ONE: - if (!WILL_ELIMINATE(FOR_ONE, this->invert ^ *require_inversion)) { - this->invert ^= *require_inversion; - *require_inversion = 0; - } else if (WILL_ELIMINATE(FOR_ONE, this->invert)) { - goto eliminate; - } - this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert; - if (this->type == LIBNORMALFORM_FOR_ONE) { - if (flags & LIBNORMALFORM_RELAX_FOR_ONE) { - this->type = LIBNORMALFORM_FOR_ANY; - goto for_any; - } - } - if (this->nterms > 1) - break; - if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE << (this->type - LIBNORMALFORM_FOR_ONE))) - goto for_any_join_sides; - break; - - default: - abort(); - } - - this->invert = 0; - - for (i = 0; i < this->nterms; i++) - if (fix_presentation(this->terms[i], flags, require_inversion, reduced)) - return -1; - - return 0; - -eliminate: - *require_inversion = 0; - this->reduced = 0; - this->invert = 0; - while (this->nterms) - free_expression(this->terms[--this->nterms]); - free(this->terms); - this->terms = NULL; - this->type = LIBNORMALFORM_CONJUNCTION; - *reduced = 1; - return 0; - -for_all_join_sides: - new = make_binary(1, this->terms[0], 0, this->terms[1], LIBNORMALFORM_DISJUNCTION); - goto join_sides; - -for_any_join_sides: - new = make_binary(0, this->terms[0], 0, this->terms[1], LIBNORMALFORM_CONJUNCTION); -join_sides: - if (!new) - return -1; - this->terms[0] = new; - this->nterms--; - if (apply_transformation(this->terms[0]->terms[0], LIBNORMALFORM_DOMAIN_VIEW)) - return -1; - if (apply_transformation(this->terms[0]->terms[1], LIBNORMALFORM_IMAGE_VIEW)) - return -1; - *reduced = 1; - return 0; - -#undef WILL_ELIMINATE -} - - -static int -expression_to_term(struct libnormalform_term *out, struct expression *this) -{ - size_t i; - - out->type = this->type; - out->reduced = this->reduced; - - switch (this->type) { - case LIBNORMALFORM_CONJUNCTION: - case LIBNORMALFORM_DISJUNCTION: - case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: - out->term.clause.nterms = 0; - out->term.clause.terms = calloc(this->nterms, sizeof(*out->term.clause.terms)); - if (!out->term.clause.terms) - return -1; - for (i = 0; i < this->nterms; i++) - if (expression_to_term(&out->term.clause.terms[out->term.clause.nterms++], this->terms[i])) - return -1; - break; - - case LIBNORMALFORM_TRANSFORMATION: - out->term.transformation.transformer = this->user_item; - out->term.transformation.sentence = calloc(1, sizeof(*out->term.transformation.sentence)); - if (!out->term.transformation.sentence || - expression_to_term(out->term.transformation.sentence, this->terms[0])) - return -1; - break; - - case LIBNORMALFORM_VARIABLE: - case LIBNORMALFORM_NEGATED_VARIABLE: - out->term.variable = this->user_item; - break; - - case LIBNORMALFORM_FUNCTION: - case LIBNORMALFORM_NEGATED_FUNCTION: - out->term.function = this->user_item; - break; - - case LIBNORMALFORM_FOR_ALL: - case LIBNORMALFORM_NEGATED_FOR_ALL: - case LIBNORMALFORM_FOR_ANY: - case LIBNORMALFORM_NEGATED_FOR_ANY: - case LIBNORMALFORM_FOR_ONE: - case LIBNORMALFORM_NEGATED_FOR_ONE: - out->term.qualification.map = this->user_item; - if (this->nterms == 1) { - out->term.qualification.antecedent = NULL; - out->term.qualification.predicate = calloc(1, sizeof(*out->term.qualification.predicate)); - if (!out->term.qualification.predicate || - expression_to_term(out->term.qualification.predicate, this->terms[0])) - return -1; - } else { - out->term.qualification.antecedent = calloc(1, sizeof(*out->term.qualification.antecedent)); - if (!out->term.qualification.antecedent) - return -1; - out->term.qualification.predicate = calloc(1, sizeof(*out->term.qualification.predicate)); - if (!out->term.qualification.predicate || - expression_to_term(out->term.qualification.antecedent, this->terms[0]) || - expression_to_term(out->term.qualification.predicate, this->terms[1])) - return -1; - } - break; - - default: - abort(); - } - - return 0; -} - - struct libnormalform_term * (libnormalform_express)(LIBNORMALFORM_SENTENCE *this, uint64_t flags, const struct libnormalform_analysers *analysers) { - struct libnormalform_term *ret; - struct expression *expression; - int reduced; - - if (flags & ~LIBNORMALFORM_ALL_EXPRESS_FLAGS__) { - errno = EINVAL; - return NULL; - } - - if (flags & LIBNORMALFORM_REDUCE_XOR) - flags &= ~LIBNORMALFORM_ELIMINATE_XOR; - if ((flags & LIBNORMALFORM_ELIMINATE_FOR_ANY) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL)) - flags &= ~LIBNORMALFORM_RELAX_FOR_ONE; - if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL) - flags &= ~LIBNORMALFORM_AVOID_FOR_ANY; - if (flags & LIBNORMALFORM_ELIMINATE_FOR_ALL) - flags &= ~LIBNORMALFORM_AVOID_NEGATED_FOR_ANY; - if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY) - flags &= ~LIBNORMALFORM_AVOID_FOR_ALL; - if (flags & LIBNORMALFORM_ELIMINATE_FOR_ANY) - flags &= ~LIBNORMALFORM_AVOID_NEGATED_FOR_ALL; - if ((flags & LIBNORMALFORM_AVOID_FOR_ANY) && (flags & LIBNORMALFORM_AVOID_NEGATED_FOR_ALL)) - flags ^= LIBNORMALFORM_AVOID_FOR_ANY | LIBNORMALFORM_AVOID_NEGATED_FOR_ALL; - if ((flags & LIBNORMALFORM_AVOID_FOR_ALL) && (flags & LIBNORMALFORM_AVOID_NEGATED_FOR_ANY)) - flags ^= LIBNORMALFORM_AVOID_FOR_ALL | LIBNORMALFORM_AVOID_NEGATED_FOR_ANY; - - expression = sentence_to_expression(this, flags); - if (!expression) - return NULL; - do { - if (reduce_expression(expression, analysers)) { - free_expression(expression); - return NULL; - } - reduced = 0; - if (fix_presentation(expression, flags, &(unsigned char){0}, &reduced)) { - free_expression(expression); - return NULL; - } - } while (reduced); - - ret = malloc(sizeof(*ret)); - if (!ret) { - free_expression(expression); - return NULL; - } - if (expression_to_term(ret, expression)) { -#if defined(__GNUC__) -# pragma GCC diagnostic push -# pragma GCC diagnostic ignored "-Wmismatched-dealloc" -#endif - libnormalform_free(ret); - ret = NULL; -#if defined(__GNUC__) -# pragma GCC diagnostic pop -#endif - } - free_expression(expression); - - return ret; + return libnormalform_express__(this, flags, analysers, NNF, NULL); } diff --git a/libnormalform_express__.c b/libnormalform_express__.c new file mode 100644 index 0000000..6c9373d --- /dev/null +++ b/libnormalform_express__.c @@ -0,0 +1,483 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + +/* TODO implement LIBNORMALFORM_DISTRIBUTE_QUALIFIERS */ + + +/** + * Convert a sentence of the type `LIBNORMALFORM_SENTENCE *` + * to the temporary type `struct expression *` + * + * This function will flatten the sentence so that no + * clause contains terms, that are direct children and, + * that are clauses using the same connective + * + * Literals and qualifiers cannot be represented will + * be removed, and any application-provided relaxation + * will be applied + * + * The flags `LIBNORMALFORM_RELAX_XOR` and + * `LIBNORMALFORM_REDUCE_XOR` will be applied + * + * @param this The sentence to convert + * @param flags Flags from `libnormalform_express` + * @return An sentence is at least as true as `this`, + * using the reductions and rewrites mentions, + * above expressed in the temporary type; + * `NULL` on failure + */ +static struct expression * +sentence_to_expression(LIBNORMALFORM_SENTENCE *this, uint64_t flags) +{ + LIBNORMALFORM_SENTENCE *left, *right, *free1 = NULL, *free2 = NULL; + struct expression *ret, *sub; + + ret = malloc(sizeof(*ret)); + if (!ret) + return NULL; + *ret = EXPRESSION_INIT(0); + + switch (this->type) { + case TYPE_TRUE: + tautology: + ret->type = LIBNORMALFORM_CONJUNCTION; + goto out; + + case TYPE_FALSE: + contradiction: + ret->type = LIBNORMALFORM_DISJUNCTION; + goto out; + + case TYPE_XOR: + if (flags & LIBNORMALFORM_RELAX_XOR) + goto inclusive_disjunction; + if (flags & LIBNORMALFORM_REDUCE_XOR) { + /* x ⊕ y = (x ∨ y) ∧ ¬(x ∧ y) = (x ∨ y) ∧ (¬x ∨ ¬y) */ + free1 = left = libnormalform_or2(libnormalform_ref(LEFT(this)), libnormalform_ref(RIGHT(this))); + free2 = right = libnormalform_or2(LEFT(this)->inverse(LEFT(this)), RIGHT(this)->inverse(RIGHT(this))); + if (!left || !right) + goto fail; + ret->type = LIBNORMALFORM_CONJUNCTION; + goto clause_prefetched_branches; + } + ret->type = LIBNORMALFORM_EXCLUSIVE_DISJUNCTION; + goto clause; + case TYPE_AND: + ret->type = LIBNORMALFORM_CONJUNCTION; + goto clause; + case TYPE_OR: + inclusive_disjunction: + ret->type = LIBNORMALFORM_DISJUNCTION; + clause: + left = LEFT(this); + right = RIGHT(this); + clause_prefetched_branches: + sub = sentence_to_expression(left, flags); + if (sub) + goto fail; + if (sub->type == ret->type) { + free(ret); + ret = sub; + } else if (!sub->nterms && ret->type == LIBNORMALFORM_CONJUNCTION && sub->type == LIBNORMALFORM_DISJUNCTION) { + /* ⋀(X ∪ {⋁∅}) = ⋀(X ∪ {⊥}) = ⋀X ∧ ⊥ = ⊥ */ + if (!sub->reduced) { + libnormalform_free_expression__(sub); + goto contradiction; + } + libnormalform_free_expression__(sub); + ret->reduced |= 1; + } else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) { + /* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */ + libnormalform_free_expression__(ret); + ret = sub; + goto tautology; + } else { + ret->terms = malloc(sizeof(*ret->terms)); + if (!ret->terms) { + libnormalform_free_expression__(sub); + goto fail; + } + ret->nterms = 1; + ret->terms[0] = sub; + } + sub = sentence_to_expression(right, flags); + if (sub) + goto fail; + if (sub->type == ret->type) { + void *new = realloc(ret->terms, (ret->nterms + sub->nterms) * sizeof(*ret->terms)); + if (!new) { + libnormalform_free_expression__(sub); + goto fail; + } + ret->terms = new; + memcpy(&ret->terms[ret->nterms], sub->terms, sub->nterms * sizeof(sub->terms)); + ret->nterms += sub->nterms; + free(sub->terms); + free(sub); + } else if (!sub->nterms && ret->type == LIBNORMALFORM_CONJUNCTION && sub->type == LIBNORMALFORM_DISJUNCTION) { + /* ⋀(X ∪ {⋁∅}) = ⋀(X ∪ {⊥}) = ⋀X ∧ ⊥ = ⊥ */ + if (!sub->reduced) { + libnormalform_free_expression__(sub); + goto contradiction; + } + libnormalform_free_expression__(sub); + ret->reduced |= 1; + } else if (!sub->nterms && ret->type == LIBNORMALFORM_DISJUNCTION && sub->type == LIBNORMALFORM_CONJUNCTION) { + /* ⋁(X ∪ {⋀∅}) = ⋁(X ∪ {⊤}) = ⋁X ∨ ⊤ = ⊤ */ + libnormalform_free_expression__(ret); + ret = sub; + goto tautology; + } else { + void *new = realloc(ret->terms, (ret->nterms + 1U) * sizeof(*ret->terms)); + if (!new) { + libnormalform_free_expression__(sub); + goto fail; + } + ret->terms = new; + ret->terms[ret->nterms++] = sub; + } + break; + + case TYPE_ALL: + ret->type = LIBNORMALFORM_FOR_ALL; + goto qualifier; + case TYPE_ANY: + ret->type = LIBNORMALFORM_FOR_ANY; + goto qualifier; + case TYPE_ONE: + ret->type = LIBNORMALFORM_FOR_ONE; + goto qualifier; + case TYPE_NOT_ONE: + ret->type = LIBNORMALFORM_NEGATED_FOR_ONE; + qualifier: + ret->user_item = this->data.qualifier.domain; + ret->nterms = 2; + ret->terms = malloc(2 * sizeof(*ret->terms)); + if (!ret->terms) + goto fail; + ret->terms[0] = sentence_to_expression(this->data.qualifier.antecedent, flags); + if (!ret->terms[0]) + goto fail; + ret->terms[1] = sentence_to_expression(this->data.qualifier.predicate, flags); + if (!ret->terms[1]) + goto fail; + break; + + case TYPE_VARIABLE: + if ((flags & LIBNORMALFORM_ELIMINATE_VARIABLE) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE)) + goto eliminated; + ret->user_item = this->data.literal.atom.variable; + ret->type = LIBNORMALFORM_VARIABLE + (enum libnormalform_term_type)this->data.literal.inverted; + break; + + case TYPE_FUNCTION: + if ((flags & LIBNORMALFORM_ELIMINATE_FUNCTION) && (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION)) + goto eliminated; + ret->reduced = !!this->data.literal.atom.function->requires_relaxation; + if (!ret->reduced) + ret->user_item = this->data.literal.atom.function; + else if (this->data.literal.atom.function->relaxation) + ret->user_item = this->data.literal.atom.function->relaxation; + else + goto eliminated; + ret->type = LIBNORMALFORM_FUNCTION + (enum libnormalform_term_type)this->data.literal.inverted; + break; + + case TYPE_TRANS: + if (this->data.trans.function->requires_elimination) + goto eliminated; + ret->type = LIBNORMALFORM_TRANSFORMATION; + ret->user_item = this->data.trans.function; + ret->terms = malloc(sizeof(*ret->terms)); + if (ret->terms) + goto fail; + ret->terms[0] = sentence_to_expression(this->data.trans.input, flags); + if (!ret->terms[0]) + goto fail; + break; + + default: + abort(); + } + + goto out; + +eliminated: + ret->reduced = 1; + ret->type = LIBNORMALFORM_CONJUNCTION; +out: + libnormalform_free(free1); + libnormalform_free(free2); + return ret; + +fail: + libnormalform_free(free1); + libnormalform_free(free2); + libnormalform_free_expression__(ret); + return NULL; +} + + + +/** + * Reduce a sentence as much as possible keeping it logically equivalent + * + * All objects must have a reference count of 1 + * + * @param this The sentence to reduce (in place) + * @param analysers Application-provided analysis functions, or `NULL` + * @return 0 on success, -1 on failure + */ +static int +reduce_expression(struct expression *this, const struct libnormalform_analysers *analysers) +{ + enum libnormalform_sentence_relationship relationship; + struct expression *new; + size_t i, j; + + for (i = 0; i < this->nterms; i++) + if (reduce_expression(this->terms[i], analysers)) + return -1; + + switch (this->type) { + case LIBNORMALFORM_CONJUNCTION: + for (i = 0; i < this->nterms; i++) { + left_eliminated_conjunction: + for (j = i + 1; j < this->nterms; j++) { + if (libnormalform_get_relationship__(this->terms[i], this->terms[j], analysers, &relationship)) + return -1; + switch (relationship) { + case LIBNORMALFORM_MATERIAL_IMPLICATION: + case LIBNORMALFORM_IDENTICAL: + libnormalform_free_expression__(this->terms[j]); + this->terms[j--] = this->terms[--this->nterms]; + break; + case LIBNORMALFORM_CONVERSE_IMPLICATION: + libnormalform_free_expression__(this->terms[i]); + this->terms[i--] = this->terms[--this->nterms]; + goto left_eliminated_conjunction; + case LIBNORMALFORM_MUTUALLY_INVERSE: + case LIBNORMALFORM_MUTUALLY_EXCLUSIVE: + goto contradiction; + case LIBNORMALFORM_JOINTLY_UNDENIABLE: + case LIBNORMALFORM_MUTUALLY_INDEPENDENT: + default: + break; + } + } + } + break; + contradiction: + for (i = 0; i < this->nterms; i++) + libnormalform_free_expression__(this->terms[i]); + free(this->terms); + this->terms = NULL; + this->nterms = 0; + this->type = LIBNORMALFORM_DISJUNCTION; + break; + + case LIBNORMALFORM_DISJUNCTION: + for (i = 0; i < this->nterms; i++) { + left_eliminated_disjunction: + for (j = i + 1; j < this->nterms; j++) { + if (libnormalform_get_relationship__(this->terms[i], this->terms[j], analysers, &relationship)) + return -1; + switch (relationship) { + case LIBNORMALFORM_IDENTICAL: + case LIBNORMALFORM_CONVERSE_IMPLICATION: + libnormalform_free_expression__(this->terms[j]); + this->terms[j--] = this->terms[--this->nterms]; + break; + case LIBNORMALFORM_MATERIAL_IMPLICATION: + libnormalform_free_expression__(this->terms[i]); + this->terms[i--] = this->terms[--this->nterms]; + goto left_eliminated_disjunction; + case LIBNORMALFORM_MUTUALLY_INVERSE: + case LIBNORMALFORM_JOINTLY_UNDENIABLE: + goto tautology; + case LIBNORMALFORM_MUTUALLY_EXCLUSIVE: + case LIBNORMALFORM_MUTUALLY_INDEPENDENT: + default: + break; + } + } + } + break; + tautology: + for (i = 0; i < this->nterms; i++) + libnormalform_free_expression__(this->terms[i]); + free(this->terms); + this->terms = NULL; + this->nterms = 0; + this->type = LIBNORMALFORM_CONJUNCTION; + break; + + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + i = 0; + both_eliminated_exclusive_disjunction: + for (; i < this->nterms; i++) { + for (j = i + 1; j < this->nterms; j++) { + if (libnormalform_get_relationship__(this->terms[i], this->terms[j], analysers, &relationship)) + return -1; + switch (relationship) { + case LIBNORMALFORM_MATERIAL_IMPLICATION: + new = libnormalform_make_binary__(1, this->terms[i], 0, this->terms[j], + LIBNORMALFORM_CONJUNCTION); + if (!new) + return -1; + goto xor_reduced; + case LIBNORMALFORM_CONVERSE_IMPLICATION: + new = libnormalform_make_binary__(0, this->terms[i], 1, this->terms[j], + LIBNORMALFORM_CONJUNCTION); + if (!new) + return -1; + goto xor_reduced; + case LIBNORMALFORM_MUTUALLY_INVERSE: + this->invert ^= 1; + /* fall through */ + case LIBNORMALFORM_IDENTICAL: + libnormalform_free_expression__(this->terms[i]); + libnormalform_free_expression__(this->terms[j]); + this->terms[i--] = this->terms[--this->nterms]; + this->terms[j--] = this->terms[--this->nterms]; + goto both_eliminated_exclusive_disjunction; + case LIBNORMALFORM_MUTUALLY_EXCLUSIVE: + new = libnormalform_make_binary__(0, this->terms[i], 0, this->terms[j], + LIBNORMALFORM_DISJUNCTION); + if (!new) + return -1; + goto xor_reduced; + case LIBNORMALFORM_JOINTLY_UNDENIABLE: + new = libnormalform_make_binary__(1, this->terms[i], 1, this->terms[j], + LIBNORMALFORM_DISJUNCTION); + if (!new) + return -1; + goto xor_reduced; + case LIBNORMALFORM_MUTUALLY_INDEPENDENT: + default: + break; + xor_reduced: + libnormalform_free_expression__(this->terms[i]); + libnormalform_free_expression__(this->terms[j]); + this->terms[j--] = this->terms[--this->nterms]; + this->terms[i] = new; + goto both_eliminated_exclusive_disjunction; + } + } + } + if (!this->nterms) { + if (this->invert) { + this->invert = 0; + this->type = LIBNORMALFORM_CONJUNCTION; + } else { + this->type = LIBNORMALFORM_DISJUNCTION; + } + } + break; + + case LIBNORMALFORM_TRANSFORMATION: + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_NEGATED_VARIABLE: + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_NEGATED_FUNCTION: + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + default: + return 0; + } + + if (this->nterms == 1) { + new = this->terms[0]; + free(this->terms); + new->invert ^= this->invert; + *this = *new; + free(new); + } + + return 0; +} + + +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)) +{ + struct libnormalform_term *ret; + struct expression *expression; + int reduced; + + if (flags & ~LIBNORMALFORM_ALL_EXPRESS_FLAGS__) { + errno = EINVAL; + return NULL; + } + + /* just to be safe */ + if (flags & LIBNORMALFORM_REDUCE_XOR) + flags |= LIBNORMALFORM_RELAX_XOR; + if ((flags & LIBNORMALFORM_AVOID_FOR_ANY) && (flags & LIBNORMALFORM_AVOID_NEGATED_FOR_ALL)) + flags ^= LIBNORMALFORM_AVOID_FOR_ANY | LIBNORMALFORM_AVOID_NEGATED_FOR_ALL; + if ((flags & LIBNORMALFORM_AVOID_FOR_ALL) && (flags & LIBNORMALFORM_AVOID_NEGATED_FOR_ANY)) + flags ^= LIBNORMALFORM_AVOID_FOR_ALL | LIBNORMALFORM_AVOID_NEGATED_FOR_ANY; + + (void) form; /* TODO respect form=={CNF,DNF} */ + expression = sentence_to_expression(this, flags); + if (!expression) + return NULL; + do { + if (reduce_expression(expression, analysers)) { + libnormalform_free_expression__(expression); + return NULL; + } + reduced = 0; + if (libnormalform_fix_presentation__(expression, flags, &(unsigned char){0}, &reduced)) { + libnormalform_free_expression__(expression); + return NULL; + } + } while (reduced); + + if (canonicalise) { + if ((*canonicalise)(expression, flags)) { + libnormalform_free_expression__(expression); + return NULL; + } + } + + ret = malloc(sizeof(*ret)); + if (!ret) { + libnormalform_free_expression__(expression); + return NULL; + } + if (libnormalform_expression_to_term__(ret, expression)) { +#if defined(__GNUC__) && !defined(__clang__) +# pragma GCC diagnostic push +# pragma GCC diagnostic ignored "-Wmismatched-dealloc" +#endif + libnormalform_free(ret); + ret = NULL; +#if defined(__GNUC__) && !defined(__clang__) +# pragma GCC diagnostic pop +#endif + } + libnormalform_free_expression__(expression); + + return ret; +} + + +#else + + +CONST int +main(void) +{ + return 0; /* indirectly tested via libnormalform_{express,dnf,cnf,cdnf} */ +} + + +#endif diff --git a/libnormalform_expression_to_term__.c b/libnormalform_expression_to_term__.c new file mode 100644 index 0000000..af988ea --- /dev/null +++ b/libnormalform_expression_to_term__.c @@ -0,0 +1,82 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +int +(libnormalform_expression_to_term__)(struct libnormalform_term *out, struct expression *this) +{ + size_t i; + + out->type = this->type; + out->reduced = this->reduced; + + switch (this->type) { + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + out->term.clause.nterms = 0; + out->term.clause.terms = calloc(this->nterms, sizeof(*out->term.clause.terms)); + if (!out->term.clause.terms) + return -1; + for (i = 0; i < this->nterms; i++) + if (libnormalform_expression_to_term__(&out->term.clause.terms[out->term.clause.nterms++], this->terms[i])) + return -1; + break; + + case LIBNORMALFORM_TRANSFORMATION: + out->term.transformation.transformer = this->user_item; + out->term.transformation.sentence = calloc(1, sizeof(*out->term.transformation.sentence)); + if (!out->term.transformation.sentence || + libnormalform_expression_to_term__(out->term.transformation.sentence, this->terms[0])) + return -1; + break; + + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_NEGATED_VARIABLE: + out->term.variable = this->user_item; + break; + + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_NEGATED_FUNCTION: + out->term.function = this->user_item; + break; + + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + out->term.qualification.domain = this->user_item; + if (this->nterms == 1) { + out->term.qualification.antecedent = NULL; + out->term.qualification.predicate = calloc(1, sizeof(*out->term.qualification.predicate)); + if (!out->term.qualification.predicate || + libnormalform_expression_to_term__(out->term.qualification.predicate, this->terms[0])) + return -1; + } else { + out->term.qualification.antecedent = calloc(1, sizeof(*out->term.qualification.antecedent)); + if (!out->term.qualification.antecedent) + return -1; + out->term.qualification.predicate = calloc(1, sizeof(*out->term.qualification.predicate)); + if (!out->term.qualification.predicate || + libnormalform_expression_to_term__(out->term.qualification.antecedent, this->terms[0]) || + libnormalform_expression_to_term__(out->term.qualification.predicate, this->terms[1])) + return -1; + } + break; + + default: + abort(); + } + + return 0; +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_fix_presentation__.c b/libnormalform_fix_presentation__.c new file mode 100644 index 0000000..8c0f4e0 --- /dev/null +++ b/libnormalform_fix_presentation__.c @@ -0,0 +1,313 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +/** + * Check whether inverting a sentence would require + * it to be relaxes before it can be represented + * + * @param this The sentence to check + * @param flags Flags from `libnormalform_express` + * @return 1 if the inversion can be exactly represented, + * 0 if the inversion requires relaxation be + */ +PURE static int +inversion_would_relax(struct expression *this, uint64_t flags) +{ + size_t i; + +beginning: + switch (this->type) { + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + for (i = 0; i < this->nterms; i++) + if (inversion_would_relax(this->terms[i], flags)) + return 1; + return 0; + + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + for (i = 0; i < this->nterms; i++) + if (!inversion_would_relax(this->terms[i], flags)) + return 0; + return 1; + + case LIBNORMALFORM_VARIABLE: + return flags & LIBNORMALFORM_ELIMINATE_NEGATED_VARIABLE; + + case LIBNORMALFORM_NEGATED_VARIABLE: + return flags & LIBNORMALFORM_ELIMINATE_VARIABLE; + + case LIBNORMALFORM_FUNCTION: + return flags & LIBNORMALFORM_ELIMINATE_NEGATED_FUNCTION; + + case LIBNORMALFORM_NEGATED_FUNCTION: + return flags & LIBNORMALFORM_ELIMINATE_FUNCTION; + + case LIBNORMALFORM_TRANSFORMATION: + this = this->terms[0]; + goto beginning; + + case LIBNORMALFORM_FOR_ALL: + if (!(flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL)) + return 0; + if (flags & LIBNORMALFORM_ELIMINATE_FOR_ANY) + return 1; + this = this->terms[this->nterms - 1]; + goto beginning; + + case LIBNORMALFORM_NEGATED_FOR_ALL: + if (!(flags & LIBNORMALFORM_ELIMINATE_FOR_ALL)) + return 0; + if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY) + return 1; + this = this->terms[this->nterms - 1]; + goto beginning; + + case LIBNORMALFORM_FOR_ANY: + if (!(flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ANY)) + return 0; + if (flags & LIBNORMALFORM_ELIMINATE_FOR_ALL) + return 1; + this = this->terms[this->nterms - 1]; + goto beginning; + + case LIBNORMALFORM_NEGATED_FOR_ANY: + if (!(flags & LIBNORMALFORM_ELIMINATE_FOR_ANY)) + return 0; + if (flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ALL) + return 1; + this = this->terms[this->nterms - 1]; + goto beginning; + + case LIBNORMALFORM_FOR_ONE: + return flags & LIBNORMALFORM_ELIMINATE_NEGATED_FOR_ONE; + + case LIBNORMALFORM_NEGATED_FOR_ONE: + return flags & LIBNORMALFORM_ELIMINATE_FOR_ONE; + + default: + abort(); + } +} + + +int +(libnormalform_fix_presentation__)(struct expression *this, uint64_t flags, unsigned char *require_inversion, int *reduced) +{ +#define WILL_ELIMINATE(BASETYPE, INVERT)\ + (flags & (LIBNORMALFORM_ELIMINATE_##BASETYPE <<\ + ((this->type ^ ((LIBNORMALFORM_##BASETYPE ^ LIBNORMALFORM_NEGATED_##BASETYPE) *\ + (INVERT))) -\ + LIBNORMALFORM_##BASETYPE))) + + size_t i; + unsigned char zero = 0; + struct expression *new; + int may_switch = 1; + + switch (this->type) { + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + this->type ^= LIBNORMALFORM_CONJUNCTION ^ LIBNORMALFORM_DISJUNCTION; + if (this->invert) { + if (*require_inversion) { + this->invert ^= 1; + *require_inversion = 0; + } + for (i = 0; i < this->nterms; i++) + this->terms[i]->invert ^= 1; + } + require_inversion = &zero; + break; + + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + if (!this->nterms) + abort(); + if (*require_inversion) { /* TODO always? */ + this->invert ^= 1; + *require_inversion = 0; + } + for (i = 0; i < this->nterms; i++) + if (libnormalform_fix_presentation__(this->terms[i], flags, &this->invert, reduced)) + return -1; + if (this->invert) { + /* TODO this is not necessarily the best element to invert, + * possibly the previous loop could be used to determine + * which is best (notably, clauses are not analysed) */ + this->invert = 0; + this->terms[0]->invert ^= 1; + if (libnormalform_fix_presentation__(this->terms[0], flags, &zero, reduced)) + return -1; + } + return 0; + + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_NEGATED_VARIABLE: + if (!WILL_ELIMINATE(VARIABLE, this->invert ^ *require_inversion)) { + this->invert ^= *require_inversion; + *require_inversion = 0; + } else if (WILL_ELIMINATE(VARIABLE, this->invert)) { + goto eliminate; + } + this->type ^= (LIBNORMALFORM_VARIABLE ^ LIBNORMALFORM_NEGATED_VARIABLE) * this->invert; + break; + + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_NEGATED_FUNCTION: + if (!WILL_ELIMINATE(FUNCTION, this->invert ^ *require_inversion)) { + this->invert ^= *require_inversion; + *require_inversion = 0; + } else if (WILL_ELIMINATE(FUNCTION, this->invert)) { + goto eliminate; + } + this->type ^= (LIBNORMALFORM_FUNCTION ^ LIBNORMALFORM_NEGATED_FUNCTION) * this->invert; + break; + + case LIBNORMALFORM_TRANSFORMATION: + this->terms[0]->invert ^= this->invert; + break; + + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + if (!WILL_ELIMINATE(FOR_ALL, this->invert ^ *require_inversion)) { + this->invert ^= *require_inversion; + *require_inversion = 0; + } else for_all: if (WILL_ELIMINATE(FOR_ALL, this->invert)) { + if (!may_switch) + goto eliminate; + may_switch = 0; + this->invert = 0; + this->terms[this->nterms - 1]->invert ^= 1; + this->type = LIBNORMALFORM_NEGATED_FOR_ANY - (this->type - LIBNORMALFORM_FOR_ALL); + goto for_any; + } + this->type ^= (LIBNORMALFORM_FOR_ALL ^ LIBNORMALFORM_NEGATED_FOR_ALL) * this->invert; + this->invert = 0; + if (flags & (LIBNORMALFORM_AVOID_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL))) { + if (!inversion_would_relax(this, flags)) { + this->terms[this->nterms - 1]->invert ^= 1; + this->type = LIBNORMALFORM_NEGATED_FOR_ANY - (this->type - LIBNORMALFORM_FOR_ALL); + goto for_any_maybe_join_sides; + } + } + for_all_maybe_join_sides: + if (this->nterms > 1) + break; + if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ALL << (this->type - LIBNORMALFORM_FOR_ALL))) + goto for_all_join_sides; + break; + + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + if (!WILL_ELIMINATE(FOR_ANY, this->invert ^ *require_inversion)) { + this->invert ^= *require_inversion; + *require_inversion = 0; + } else for_any: if (WILL_ELIMINATE(FOR_ANY, this->invert)) { + if (!may_switch) + goto eliminate; + may_switch = 0; + this->invert = 0; + this->terms[this->nterms - 1]->invert ^= 1; + this->type = LIBNORMALFORM_NEGATED_FOR_ALL - (this->type - LIBNORMALFORM_FOR_ANY); + goto for_all; + } + this->type ^= (LIBNORMALFORM_FOR_ANY ^ LIBNORMALFORM_NEGATED_FOR_ANY) * this->invert; + this->invert = 0; + if (flags & (LIBNORMALFORM_AVOID_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY))) { + if (!inversion_would_relax(this, flags)) { + this->terms[this->nterms - 1]->invert ^= 1; + this->type = LIBNORMALFORM_NEGATED_FOR_ALL - (this->type - LIBNORMALFORM_FOR_ANY); + goto for_all_maybe_join_sides; + } + } + for_any_maybe_join_sides: + if (this->nterms > 1) + break; + if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ANY << (this->type - LIBNORMALFORM_FOR_ANY))) + goto for_any_join_sides; + break; + + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + if (!WILL_ELIMINATE(FOR_ONE, this->invert ^ *require_inversion)) { + this->invert ^= *require_inversion; + *require_inversion = 0; + } else if (WILL_ELIMINATE(FOR_ONE, this->invert)) { + this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert; + if (this->type == LIBNORMALFORM_FOR_ONE) { + this->invert = 0; + this->reduced = 1; + *reduced = 1; + goto for_any; + } + goto eliminate; + } + this->type ^= (LIBNORMALFORM_FOR_ONE ^ LIBNORMALFORM_NEGATED_FOR_ONE) * this->invert; + if (this->type == LIBNORMALFORM_FOR_ONE) { + if (flags & LIBNORMALFORM_ELIMINATE_FOR_ONE) { + this->type = LIBNORMALFORM_FOR_ANY; + this->invert = 0; + this->reduced = 1; + *reduced = 1; + goto for_any; + } + } + if (this->nterms > 1) + break; + if (flags & (LIBNORMALFORM_JOIN_SIDES_IN_FOR_ONE << (this->type - LIBNORMALFORM_FOR_ONE))) + goto for_any_join_sides; + break; + + default: + abort(); + } + + this->invert = 0; + + for (i = 0; i < this->nterms; i++) + if (libnormalform_fix_presentation__(this->terms[i], flags, require_inversion, reduced)) + return -1; + + return 0; + +eliminate: + *require_inversion = 0; + this->refcount = 1; + this->reduced = 1; + this->invert = 0; + while (this->nterms) + libnormalform_free_expression__(this->terms[--this->nterms]); + free(this->terms); + this->terms = NULL; + this->type = LIBNORMALFORM_CONJUNCTION; + *reduced = 1; + return 0; + +for_all_join_sides: + new = libnormalform_make_binary__(1, this->terms[0], 0, this->terms[1], LIBNORMALFORM_DISJUNCTION); + goto join_sides; + +for_any_join_sides: + new = libnormalform_make_binary__(0, this->terms[0], 0, this->terms[1], LIBNORMALFORM_CONJUNCTION); +join_sides: + if (!new) + return -1; + this->terms[0] = new; + this->nterms--; + if (libnormalform_apply_transformation__(this->terms[0]->terms[0], LIBNORMALFORM_DOMAIN_VIEW)) + return -1; + if (libnormalform_apply_transformation__(this->terms[0]->terms[1], LIBNORMALFORM_IMAGE_VIEW)) + return -1; + *reduced = 1; + return 0; + +#undef WILL_ELIMINATE +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_free.c b/libnormalform_free.c index 3bce4df..26353c8 100644 --- a/libnormalform_free.c +++ b/libnormalform_free.c @@ -56,12 +56,11 @@ destroy_term(struct libnormalform_term *this) while (this->term.clause.nterms) destroy_term(&this->term.clause.terms[--this->term.clause.nterms]); free(this->term.clause.terms); - free(this); break; case LIBNORMALFORM_TRANSFORMATION: + destroy_term(this->term.transformation.sentence); free(this->term.transformation.sentence); - free(this); return; case LIBNORMALFORM_FOR_ALL: @@ -74,13 +73,12 @@ destroy_term(struct libnormalform_term *this) destroy_term(this->term.qualification.predicate); free(this->term.qualification.antecedent); free(this->term.qualification.predicate); - /* fall through */ + break; case LIBNORMALFORM_VARIABLE: case LIBNORMALFORM_NEGATED_VARIABLE: case LIBNORMALFORM_FUNCTION: case LIBNORMALFORM_NEGATED_FUNCTION: - free(this); break; default: diff --git a/libnormalform_free_expression__.c b/libnormalform_free_expression__.c new file mode 100644 index 0000000..d9f1a47 --- /dev/null +++ b/libnormalform_free_expression__.c @@ -0,0 +1,30 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +void +(libnormalform_free_expression__)(struct expression *this) +{ + if (!this || --this->refcount) + return; + if (this->terms) { + while (this->nterms) + libnormalform_free_expression__(this->terms[--this->nterms]); + free(this->terms); + } + free(this); +} + + +#else + + +CONST int +main(void) +{ + return 0; /* indirectly tested */ +} + + +#endif diff --git a/libnormalform_from_string.c b/libnormalform_from_string.c index 8d64c41..7555f8e 100644 --- a/libnormalform_from_string.c +++ b/libnormalform_from_string.c @@ -7,7 +7,7 @@ do {\ while (isspace(*s))\ s++;\ - } while (0); + } while (0) #define LEFT_BRACKET\ do {\ @@ -482,7 +482,7 @@ get_transformer(char *s, char **end_out, void *user_data) } -struct libnormalform_representation_spec spec = { +static struct libnormalform_representation_spec spec = { .get_variable = get_variable, .get_function = get_function, .get_map = get_map, diff --git a/libnormalform_get_relationship__.c b/libnormalform_get_relationship__.c new file mode 100644 index 0000000..baad786 --- /dev/null +++ b/libnormalform_get_relationship__.c @@ -0,0 +1,23 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +int +(libnormalform_get_relationship__)(struct expression *left, struct expression *right, /* TODO */ + const struct libnormalform_analysers *analysers, + enum libnormalform_sentence_relationship *relationship_out) +{ + (void) left; + (void) right; + (void) analysers; + *relationship_out = LIBNORMALFORM_MUTUALLY_INDEPENDENT; + return 0; +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_literal_cmp__.c b/libnormalform_literal_cmp__.c new file mode 100644 index 0000000..8d5e152 --- /dev/null +++ b/libnormalform_literal_cmp__.c @@ -0,0 +1,126 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +int +(libnormalform_literal_cmp__)(struct expression *a, struct expression *b) +{ + int a_class, b_class; + uintptr_t a_value, b_value; + +beginning: + switch (a->type) { + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_NEGATED_VARIABLE: + a_class = 0; + break; + + case LIBNORMALFORM_TRANSFORMATION: + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_NEGATED_FUNCTION: + a_class = 1; + break; + + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + a_class = 2; + break; + + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + a_class = 3; + break; + + default: + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + abort(); + } + + switch (b->type) { + case LIBNORMALFORM_VARIABLE: + case LIBNORMALFORM_NEGATED_VARIABLE: + b_class = 0; + break; + + case LIBNORMALFORM_TRANSFORMATION: + case LIBNORMALFORM_FUNCTION: + case LIBNORMALFORM_NEGATED_FUNCTION: + b_class = 1; + break; + + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + b_class = 2; + break; + + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + b_class = 3; + break; + + default: + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + abort(); + } + + if (a_class != b_class) + return a_class < b_class ? -2 : +2; + + a_value = (uintptr_t)a->user_item; + b_value = (uintptr_t)b->user_item; + if (a_value != b_value) + return a_value < b_value ? -2 : +2; + + switch (a->type) { + case LIBNORMALFORM_VARIABLE: + return -(b->type == LIBNORMALFORM_NEGATED_VARIABLE); + + case LIBNORMALFORM_NEGATED_VARIABLE: + return +(b->type == LIBNORMALFORM_VARIABLE); + + case LIBNORMALFORM_TRANSFORMATION: + a = a->terms[0]; + b = b->terms[0]; + goto beginning; + + case LIBNORMALFORM_FUNCTION: + return -(b->type == LIBNORMALFORM_NEGATED_FUNCTION); + + case LIBNORMALFORM_NEGATED_FUNCTION: + return +(b->type == LIBNORMALFORM_FUNCTION); + + case LIBNORMALFORM_FOR_ALL: + case LIBNORMALFORM_NEGATED_FOR_ALL: + case LIBNORMALFORM_FOR_ANY: + case LIBNORMALFORM_NEGATED_FOR_ANY: + /* TODO (not) all/any */ + return 0; + + case LIBNORMALFORM_FOR_ONE: + case LIBNORMALFORM_NEGATED_FOR_ONE: + /* TODO (not) one */ + return 0; + + default: + case LIBNORMALFORM_CONJUNCTION: + case LIBNORMALFORM_DISJUNCTION: + case LIBNORMALFORM_EXCLUSIVE_DISJUNCTION: + abort(); + } +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_literal_sort_cmp__.c b/libnormalform_literal_sort_cmp__.c new file mode 100644 index 0000000..c0b8937 --- /dev/null +++ b/libnormalform_literal_sort_cmp__.c @@ -0,0 +1,33 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +int +(libnormalform_literal_sort_cmp__)(const void *a, const void *b) +{ + struct expression *const *ap = a, *const *bp = b; + return libnormalform_literal_cmp__(*ap, *bp); +} + + +#else + + +#if defined(__GNUC__) /* TODO remove when testing is implemented in libnormalform_literal_sort_cmp__.c */ +# pragma GCC diagnostic ignored "-Wunused-function" +# pragma GCC diagnostic ignored "-Wunused-macros" +#endif + +#define libnormalform_literal_cmp__(...) cmptrampoline(__VA_ARGS__) + +PURE static int +cmptrampoline(struct expression *a, struct expression *b) +{ + return libnormalform_literal_sort_cmp__(&a, &b); +} + +#include "libnormalform_literal_cmp__.c" + + +#endif diff --git a/libnormalform_make_binary__.c b/libnormalform_make_binary__.c new file mode 100644 index 0000000..11bc0e1 --- /dev/null +++ b/libnormalform_make_binary__.c @@ -0,0 +1,31 @@ +/* See LICENSE file for copyright and license details. */ +#include "common.h" +#ifndef TEST + + +struct expression * +(libnormalform_make_binary__)(int invert_left, struct expression *left, + int invert_right, struct expression *right, enum libnormalform_term_type type) +{ + struct expression *ret; + ret = malloc(sizeof(*ret)); + if (!ret) + return NULL; + *ret = EXPRESSION_INIT(type); + ret->nterms = 2; + ret->terms = malloc(2 * sizeof(*ret->terms)); + if (!ret->terms) { + free(ret); + return NULL; + } + (ret->terms[0] = left)->invert ^= (unsigned char)invert_left; + (ret->terms[1] = right)->invert ^= (unsigned char)invert_right; + return ret; +} + + +#else + +TODO_TEST + +#endif diff --git a/libnormalform_one.c b/libnormalform_one.c index b5c17f1..3219097 100644 --- a/libnormalform_one.c +++ b/libnormalform_one.c @@ -426,8 +426,8 @@ main(void) ASSERT_NOTEQUAL(a, b); libnormalform_free(b); - /* P = ¬Q ⊭ ∃!{x,y}∈X.(P(x) ∧ Q(y)) = ∃!{x,y}∈X.(¬Q(x) ∧ Q(y)) = ∃!{x,y}∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */ - /* P = ¬Q ⊭ ∃!{x,y}∈X.(P(x) ∧ Q(y)) = ∃!{x,y}∈X.(P(x) ∧ ¬P(y)) = ∃!{x,y}∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */ + /* P = ¬Q ⊭ ∃!⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃!⟨x,y⟩∈X.(¬Q(x) ∧ Q(y)) = ∃!⟨x,y⟩∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */ + /* P = ¬Q ⊭ ∃!⟨x,y⟩∈X.(P(x) ∧ Q(y)) = ∃!⟨x,y⟩∈X.(P(x) ∧ ¬P(y)) = ∃!⟨x,y⟩∈X.⊥ = ⊥ ∵ P = ¬Q ⊭ P(x) = ¬Q(y) */ ASSUME(b = libnormalform_one(&dom1, libnormalform_false(), libnormalform_false())); ASSERT_NOTEQUAL(a, b); libnormalform_free(b); diff --git a/libnormalform_to_string.c b/libnormalform_to_string.c index 74aa839..fcf2981 100644 --- a/libnormalform_to_string.c +++ b/libnormalform_to_string.c @@ -65,10 +65,10 @@ add_string(struct string_construction *s, const char *str) */ USE_RESULT NONNULL_INPUT static int -add_number(struct string_construction *s, size_t n) +add_number(struct string_construction *s, size_t num) { char buf[3 * sizeof(size_t)], *str; - int len = sprintf(buf, "%zu", n); + int len = sprintf(buf, "%zu", num); if (len < 0) abort(); if (s->dyn_n == s->dyn_size) { diff --git a/libnormalform_transformation.c b/libnormalform_transformation.c index 3a1218b..82d794d 100644 --- a/libnormalform_transformation.c +++ b/libnormalform_transformation.c @@ -284,28 +284,28 @@ main(void) ASSERT(LEFT(b)->data.trans.input != RIGHT(b)->data.trans.input); libnormalform_free(b); - /* F(Q(q)∀{p,q}:P(p)) illegal construct */ + /* F(Q(q)∀⟨p,q⟩:P(p)) illegal construct */ ASSUME(a = libnormalform_function(&fun1)); ASSUME(b = libnormalform_function(&fun2)); ASSUME(a = libnormalform_all(&dom1, a, b)); errno = 0; ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM); - /* F(Q(q)∃{p,q}:P(p)) illegal construct */ + /* F(Q(q)∃⟨p,q⟩:P(p)) illegal construct */ ASSUME(a = libnormalform_function(&fun1)); ASSUME(b = libnormalform_function(&fun2)); ASSUME(a = libnormalform_any(&dom1, a, b)); errno = 0; ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM); - /* F(Q(q)∃!{p,q}:P(p)) illegal construct */ + /* F(Q(q)∃!⟨p,q⟩:P(p)) illegal construct */ ASSUME(a = libnormalform_function(&fun1)); ASSUME(b = libnormalform_function(&fun2)); ASSUME(a = libnormalform_one(&dom1, a, b)); errno = 0; ASSERT(!libnormalform_transformation(&trans1, a) && errno == EDOM); - /* F(¬(Q(q)∃!{p,q}:P(p))) illegal construct */ + /* F(¬(Q(q)∃!⟨p,q⟩:P(p))) illegal construct */ ASSUME(a = libnormalform_function(&fun1)); ASSUME(b = libnormalform_function(&fun2)); ASSUME(a = libnormalform_one(&dom1, a, b)); diff --git a/libnormalform_xor2.c b/libnormalform_xor2.c index a00c575..447d787 100644 --- a/libnormalform_xor2.c +++ b/libnormalform_xor2.c @@ -3,10 +3,66 @@ #include "common.h" +/** + * Check if two clauses have a term in common or + * a term in common but mutually inverse + * + * Both clauses must be clauses of binary connectives + * + * @param a One of the clauses + * @param b The other clause + * @param common_inv_out Output parameter for whether the common term is mutually inverted + * @param a_common_out Output parameter for `a`'s copy of the common term + * @param a_unique_out Output parameter for `a`'s uncommon term + * @param b_common_out Output parameter for `b`'s copy of the common term + * @param b_unique_out Output parameter for `b`'s uncommon term + * @return Whether the the clauses have a common or inversely common term + */ +static int +has_common(LIBNORMALFORM_SENTENCE *a, LIBNORMALFORM_SENTENCE *b, int *common_inv_out, + LIBNORMALFORM_SENTENCE **a_common_out, LIBNORMALFORM_SENTENCE **a_unique_out, + LIBNORMALFORM_SENTENCE **b_common_out, LIBNORMALFORM_SENTENCE **b_unique_out) +{ + LIBNORMALFORM_SENTENCE *al = LEFT(a); + LIBNORMALFORM_SENTENCE *ar = RIGHT(a); + LIBNORMALFORM_SENTENCE *bl = LEFT(b); + LIBNORMALFORM_SENTENCE *br = RIGHT(b); + + if (al->equals(al, bl, common_inv_out)) { + *a_common_out = al; + *b_common_out = bl; + *a_unique_out = ar; + *b_unique_out = br; + return 1; + } else if (ar->equals(ar, br, common_inv_out)) { + *a_common_out = ar; + *b_common_out = br; + *a_unique_out = al; + *b_unique_out = bl; + return 1; + } else if (al->equals(al, br, common_inv_out)) { + *a_common_out = al; + *b_common_out = br; + *a_unique_out = ar; + *b_unique_out = bl; + return 1; + } else if (ar->equals(ar, bl, common_inv_out)) { + *a_common_out = ar; + *b_common_out = bl; + *a_unique_out = al; + *b_unique_out = br; + return 1; + } + + return 0; +} + + LIBNORMALFORM_SENTENCE * (libnormalform_xor2)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r) { int inv; + LIBNORMALFORM_SENTENCE *t, *not_a, *a, *b, *c; if (!l || !r) { libnormalform_free(l); @@ -49,7 +105,79 @@ LIBNORMALFORM_SENTENCE * /* x ⊕ 0 = 0 ⊕ x = x */ goto return_l; + } else if (l->type == TYPE_OR && r->type == TYPE_OR) { /* TODO test */ + if (!has_common(l, r, &inv, &a, &b, ¬_a, &c) || !inv) + goto asis; + /* (a ∨ b) ⊕ (¬a ∨ c) = + * (a ∨ b ∨ ¬a ∨ c) ∧ ¬((a ∨ b) ∧ (¬a ∨ c)) = + * ¬(a ∨ b) ∨ ¬(¬a ∨ c) */ + return libnormalform_or2(libnormalform_not(l), libnormalform_not(r)); + + } else if (l->type == TYPE_AND && r->type == TYPE_AND) { /* TODO test */ + if (!has_common(l, r, &inv, &a, &b, ¬_a, &c)) + goto asis; + if (!inv) { + /* (a ∧ b) ⊕ (a ∧ c) = + * ((a ∧ b) ∨ (a ∧ c)) ∧ ¬((a ∧ b) ∧ (a ∧ c)) = + * a ∧ (b ∨ c) ∧ ¬(a ∧ b ∧ c) = + * a ∧ (b ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) = + * a ∧ (b ∨ c) ∧ (¬b ∨ ¬c) = + * a ∧ (b ⊕ c) + */ + a = libnormalform_ref(a); + b = libnormalform_ref(b); + c = libnormalform_ref(c); + libnormalform_free(l); + libnormalform_free(r); + return libnormalform_and2(a, libnormalform_xor2(c, b)); + } else { + /* (a ∧ b) ⊕ (¬a ∧ c) = + * ((a ∧ b) ∨ (¬a ∧ c)) ∧ ¬((a ∧ b) ∧ (¬a ∧ c)) = + * ((a ∧ b) ∨ (¬a ∧ c)) ∧ ¬(a ∧ b ∧ ¬a ∧ c) = + * ((a ∧ b) ∨ (¬a ∧ c)) ∧ ¬⊥ = + * (a ∧ b) ∨ (¬a ∧ c) + */ + return libnormalform_or2__(l, r); + } + + } else if (l->type == TYPE_OR && r->type == TYPE_AND) { /* TODO test */ + t = l, l = r, r = t; + goto and_xor_or; + + } else if (l->type == TYPE_AND && r->type == TYPE_OR) { /* TODO test */ + and_xor_or: + if (!has_common(l, r, &inv, &a, &b, ¬_a, &c)) + goto asis; + if (!inv) { + /* (a ∧ b) ⊕ (a ∨ c) = + * ((a ∧ b) ∨ (a ∨ c)) ∧ ¬((a ∧ b) ∧ (a ∨ c)) = + * ((a ∧ b) ∨ a ∨ c) ∧ ¬(a ∧ b ∧ (a ∨ c)) = + * (a ∨ c) ∧ ¬(a ∧ b) = + * ¬(a ∧ b) ∧ (a ∨ c) + */ + return libnormalform_and2__(libnormalform_not(l), r); + } else { + /* (a ∧ b) ⊕ (¬a ∨ c) = + * ((a ∧ b) ∨ (¬a ∨ c)) ∧ ¬((a ∧ b) ∧ (¬a ∨ c)) = + * ((a ∧ b) ∨ ¬a ∨ c) ∧ ¬(a ∧ b ∧ (¬a ∨ c)) = + * ((a ∧ b) ∨ ¬a ∨ c) ∧ ¬(a ∧ b ∧ (⊥ ∨ c)) = + * ((a ∧ b) ∨ ¬a ∨ c) ∧ ¬(a ∧ b ∧ c) = + * ((a ∧ b) ∨ ¬a ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) = + * (b ∨ ¬a ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) = + * (¬a ∨ b ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c) = + * ¬a ∨ ((b ∨ c) ∧ (¬b ∨ ¬c)) = + * ¬a ∨ (b ⊕ c) + */ + not_a = libnormalform_ref(not_a); + b = libnormalform_ref(b); + c = libnormalform_ref(c); + libnormalform_free(l); + libnormalform_free(r); + return libnormalform_or2(not_a, libnormalform_xor2(c, b)); + } + } else { + asis: return libnormalform_xor2__(l, r); } } diff --git a/man3/enum_libnormalform_domain_relationship.3 b/man3/enum_libnormalform_domain_relationship.3 new file mode 120000 index 0000000..d76da20 --- /dev/null +++ b/man3/enum_libnormalform_domain_relationship.3 @@ -0,0 +1 @@ +struct_libnormalform_domain_comparison.3
\ No newline at end of file diff --git a/man3/enum_libnormalform_sentences_relationship.3 b/man3/enum_libnormalform_sentences_relationship.3 new file mode 120000 index 0000000..3b51671 --- /dev/null +++ b/man3/enum_libnormalform_sentences_relationship.3 @@ -0,0 +1 @@ +struct_libnormalform_atom_comparison.3
\ No newline at end of file diff --git a/man3/enum_libnormalform_ternary.3 b/man3/enum_libnormalform_ternary.3 new file mode 120000 index 0000000..0d9b1eb --- /dev/null +++ b/man3/enum_libnormalform_ternary.3 @@ -0,0 +1 @@ +struct_libnormalform_analysers.3
\ No newline at end of file diff --git a/man3/libnormalform_all.3 b/man3/libnormalform_all.3 index 901bba2..207243f 100644 --- a/man3/libnormalform_all.3 +++ b/man3/libnormalform_all.3 @@ -154,9 +154,9 @@ The .BR libnormalform_all () and .BR libnormalform_universally () -functions fails if: +functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_analysers.3 b/man3/libnormalform_analysers.3 new file mode 120000 index 0000000..0d9b1eb --- /dev/null +++ b/man3/libnormalform_analysers.3 @@ -0,0 +1 @@ +struct_libnormalform_analysers.3
\ No newline at end of file diff --git a/man3/libnormalform_and.3 b/man3/libnormalform_and.3 index bb65a74..aeb4fa0 100644 --- a/man3/libnormalform_and.3 +++ b/man3/libnormalform_and.3 @@ -110,9 +110,9 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_any.3 b/man3/libnormalform_any.3 index ac44b0b..57ad55c 100644 --- a/man3/libnormalform_any.3 +++ b/man3/libnormalform_any.3 @@ -221,9 +221,9 @@ The .BR libnormalform_empty (), and .BR libnormalform_nonempty (), -functions fails if: +functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_atom_comparison.3 b/man3/libnormalform_atom_comparison.3 new file mode 120000 index 0000000..3b51671 --- /dev/null +++ b/man3/libnormalform_atom_comparison.3 @@ -0,0 +1 @@ +struct_libnormalform_atom_comparison.3
\ No newline at end of file diff --git a/man3/libnormalform_cdnf.3 b/man3/libnormalform_cdnf.3 new file mode 100644 index 0000000..461e63e --- /dev/null +++ b/man3/libnormalform_cdnf.3 @@ -0,0 +1,134 @@ +.TH LIBNORMALFORM_CDNF 3 LIBNORMALFORM +.SH NAME +libnormalform_cdnf \- Reduce and express in canonical disjunctive normal form + +.SH SYNOPSIS +.nf +#include <libnormalform.h> + +/* See \fBlibnormalform_express\fP(3) for relevant types and constants */ + +struct libnormalform_term * +libnormalform_cdnf(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_cdnf () +function is similar to the +.BR libnormalform_express (3) +function, please refer to +.BR libnormalform_express (3) +for a detailed explanation. There are however +the following differences: +.PP +The result will never contain a +.I LIBNORMALFORM_EXCLUSIVE_DISJUNCTION +clause, instead these are always relax +to disjunctions +.RI ( LIBNORMALFORM_RELAX_XOR ), +or reduced to an equivalent form if the +.I LIBNORMALFORM_REDUCE_XOR +flag is used. +.PP +.I LIBNORMALFORM_CONJUNCTION +and +.I LIBNORMALFORM_DISJUNCTION +clauses in the result can be singleton +clauses. +.PP +The root term is always a +.I LIBNORMALFORM_DISJUNCTION +clause containing only +.I LIBNORMALFORM_CONJUNCTION +clauses, each containing only literals +(boolean variables and boolean-output +functions), input transformations on +literals, and qualifications. Additionally +each conjunctive clause contains a complete +enumerate of all atomic sentences (boolean +variables and boolean-output functions) +and qualifications (universal and existential +qualifiers either be negated or translated to +the other depending on the specified +.IR flags ) +used in any of the conjuctive clauses within +the root disjuntive clause. That is +the returned expression is always +.I this +(or some relaxation) expressed in +canonical disjunctive normal form. +.PP +Each +.RI non- NULL +.I .term.qualifier.antecedent +is expressed in canonical disjunctive normal form. +.PP +Each +.I .term.qualifier.predicate +is expressed in canonical disjunctive normal form. + +.SH RETURN VALUE +Upon successful completion, the +.BR libnormalform_cdnf () +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_cdnf () +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_cdnf () +T} Thread safety MT-Safe race:\fIthis\fP +T{ +.BR libnormalform_cdnf () +T} Async-signal safety AS-Unsafe heap +T{ +.BR libnormalform_cdnf () +T} Async-cancel safety AC-Safe mem, AC-Unsafe heap +.TE + +.SH SEE ALSO +.BR libnormalform (7), +.BR libnormalform_express (3), +.BR libnormalform_dnf (3), +.BR libnormalform_cnf (3) diff --git a/man3/libnormalform_clone.3 b/man3/libnormalform_clone.3 index 0906a44..02cf5ca 100644 --- a/man3/libnormalform_clone.3 +++ b/man3/libnormalform_clone.3 @@ -63,7 +63,7 @@ The .BR libnormalform_clone () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_cnf.3 b/man3/libnormalform_cnf.3 new file mode 100644 index 0000000..c0d7438 --- /dev/null +++ b/man3/libnormalform_cnf.3 @@ -0,0 +1,125 @@ +.TH LIBNORMALFORM_CNF 3 LIBNORMALFORM +.SH NAME +libnormalform_cnf \- Reduce and express in conjunctive normal form + +.SH SYNOPSIS +.nf +#include <libnormalform.h> + +/* See \fBlibnormalform_express\fP(3) for relevant types and constants */ + +struct libnormalform_term * +libnormalform_cnf(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_cnf () +function is similar to the +.BR libnormalform_express (3) +function, please refer to +.BR libnormalform_express (3) +for a detailed explanation. There are however +the following differences: +.PP +The result will never contain a +.I LIBNORMALFORM_EXCLUSIVE_DISJUNCTION +clause, instead these are always relax +to disjunctions +.RI ( LIBNORMALFORM_RELAX_XOR ), +or reduced to an equivalent form if the +.I LIBNORMALFORM_REDUCE_XOR +flag is used. +.PP +.I LIBNORMALFORM_CONJUNCTION +and +.I LIBNORMALFORM_DISJUNCTION +clauses in the result can be singleton +clauses. +.PP +The root term is always a +.I LIBNORMALFORM_CONJUNCTION +clause containing only +.I LIBNORMALFORM_DISJUNCTION +clauses, each containing only literals +(boolean variables and boolean-output +functions), input transformations on +literals, and qualifications. That is +the returned expression is always +.I this +(or some relaxation) expressed in +conjunctive normal form. +.PP +Each +.RI non- NULL +.I .term.qualifier.antecedent +is expressed in conjunctive normal form. +.PP +Each +.I .term.qualifier.predicate +is expressed in conjunctive normal form. + +.SH RETURN VALUE +Upon successful completion, the +.BR libnormalform_cnf () +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_cnf () +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_cnf () +T} Thread safety MT-Safe race:\fIthis\fP +T{ +.BR libnormalform_cnf () +T} Async-signal safety AS-Unsafe heap +T{ +.BR libnormalform_cnf () +T} Async-cancel safety AC-Safe mem, AC-Unsafe heap +.TE + +.SH SEE ALSO +.BR libnormalform (7), +.BR libnormalform_express (3), +.BR libnormalform_dnf (3), +.BR libnormalform_cdnf (3) diff --git a/man3/libnormalform_dnf.3 b/man3/libnormalform_dnf.3 new file mode 100644 index 0000000..825ff1b --- /dev/null +++ b/man3/libnormalform_dnf.3 @@ -0,0 +1,125 @@ +.TH LIBNORMALFORM_DNF 3 LIBNORMALFORM +.SH NAME +libnormalform_dnf \- Reduce and express in disjunctive normal form + +.SH SYNOPSIS +.nf +#include <libnormalform.h> + +/* See \fBlibnormalform_express\fP(3) for relevant types and constants */ + +struct libnormalform_term * +libnormalform_dnf(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_dnf () +function is similar to the +.BR libnormalform_express (3) +function, please refer to +.BR libnormalform_express (3) +for a detailed explanation. There are however +the following differences: +.PP +The result will never contain a +.I LIBNORMALFORM_EXCLUSIVE_DISJUNCTION +clause, instead these are always relax +to disjunctions +.RI ( LIBNORMALFORM_RELAX_XOR ), +or reduced to an equivalent form if the +.I LIBNORMALFORM_REDUCE_XOR +flag is used. +.PP +.I LIBNORMALFORM_CONJUNCTION +and +.I LIBNORMALFORM_DISJUNCTION +clauses in the result can be singleton +clauses. +.PP +The root term is always a +.I LIBNORMALFORM_DISJUNCTION +clause containing only +.I LIBNORMALFORM_CONJUNCTION +clauses, each containing only literals +(boolean variables and boolean-output +functions), input transformations on +literals, and qualifications. That is +the returned expression is always +.I this +(or some relaxation) expressed in +disjunctive normal form. +.PP +Each +.RI non- NULL +.I .term.qualifier.antecedent +is expressed in disjunctive normal form. +.PP +Each +.I .term.qualifier.predicate +is expressed in disjunctive normal form. + +.SH RETURN VALUE +Upon successful completion, the +.BR libnormalform_dnf () +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_dnf () +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_dnf () +T} Thread safety MT-Safe race:\fIthis\fP +T{ +.BR libnormalform_dnf () +T} Async-signal safety AS-Unsafe heap +T{ +.BR libnormalform_dnf () +T} Async-cancel safety AC-Safe mem, AC-Unsafe heap +.TE + +.SH SEE ALSO +.BR libnormalform (7), +.BR libnormalform_express (3), +.BR libnormalform_cnf (3), +.BR libnormalform_cdnf (3) diff --git a/man3/libnormalform_domain_comparison.3 b/man3/libnormalform_domain_comparison.3 new file mode 120000 index 0000000..d76da20 --- /dev/null +++ b/man3/libnormalform_domain_comparison.3 @@ -0,0 +1 @@ +struct_libnormalform_domain_comparison.3
\ No newline at end of file diff --git a/man3/libnormalform_domain_relationship.3 b/man3/libnormalform_domain_relationship.3 new file mode 120000 index 0000000..a243086 --- /dev/null +++ b/man3/libnormalform_domain_relationship.3 @@ -0,0 +1 @@ +enum_libnormalform_domain_relationship.3
\ No newline at end of file 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) diff --git a/man3/libnormalform_false.3 b/man3/libnormalform_false.3 index 83dd97a..54131c4 100644 --- a/man3/libnormalform_false.3 +++ b/man3/libnormalform_false.3 @@ -40,7 +40,7 @@ The .BR libnormalform_false () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. diff --git a/man3/libnormalform_from_string.3 b/man3/libnormalform_from_string.3 index f0bfc98..108c5a7 100644 --- a/man3/libnormalform_from_string.3 +++ b/man3/libnormalform_from_string.3 @@ -111,14 +111,14 @@ The .BR libnormalform_from_string () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .TP -.I EINVAL +.B EINVAL The representation is invalid. .TP -.I EINVAL +.B EINVAL .I end_out is .I NULL @@ -126,35 +126,35 @@ but there are non-whitespace characters in .I s after the detected end of the representation. .TP -.I EDOM +.B EDOM The described sentence contains an empty clause for a connective that does not support empty clauses. .TP -.I EDOM +.B EDOM The described sentence contains a transformation somewhere over a qualifer. .TP -.I ENOENT +.B ENOENT The described sentence contains a boolean variable but .I spec->get_variable was .IR NULL . .TP -.I ENOENT +.B ENOENT The described sentence contains a boolean function but .I spec->get_function was .IR NULL . .TP -.I ENOENT +.B ENOENT The described sentence contains (a domain of interest for a) qualifier but .I spec->get_map was .IR NULL . .TP -.I ENOENT +.B ENOENT The described sentence contains a transformation (a input transformation function) but .I spec->get_transformer diff --git a/man3/libnormalform_function.3 b/man3/libnormalform_function.3 index d89c0e9..87edd46 100644 --- a/man3/libnormalform_function.3 +++ b/man3/libnormalform_function.3 @@ -121,7 +121,7 @@ The .BR libnormalform_function () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. diff --git a/man3/libnormalform_if.3 b/man3/libnormalform_if.3 index 86fde19..02c69dc 100644 --- a/man3/libnormalform_if.3 +++ b/man3/libnormalform_if.3 @@ -111,13 +111,13 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .TP -.I EDOM +.B EDOM The function was not given any subsentences. .PP The diff --git a/man3/libnormalform_imply.3 b/man3/libnormalform_imply.3 index b6e0284..852d965 100644 --- a/man3/libnormalform_imply.3 +++ b/man3/libnormalform_imply.3 @@ -111,9 +111,9 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_nand.3 b/man3/libnormalform_nand.3 index a3604ae..3973dca 100644 --- a/man3/libnormalform_nand.3 +++ b/man3/libnormalform_nand.3 @@ -113,13 +113,13 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .TP -.I EDOM +.B EDOM The function was not given any subsentences. .PP The diff --git a/man3/libnormalform_nif.3 b/man3/libnormalform_nif.3 index 174b9d4..39caec1 100644 --- a/man3/libnormalform_nif.3 +++ b/man3/libnormalform_nif.3 @@ -109,9 +109,9 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_nimply.3 b/man3/libnormalform_nimply.3 index ca7a0e9..c2d3d8e 100644 --- a/man3/libnormalform_nimply.3 +++ b/man3/libnormalform_nimply.3 @@ -109,13 +109,13 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .TP -.I EDOM +.B EDOM The function was not given any subsentences. .PP The diff --git a/man3/libnormalform_nor.3 b/man3/libnormalform_nor.3 index 164e8c5..23eaae2 100644 --- a/man3/libnormalform_nor.3 +++ b/man3/libnormalform_nor.3 @@ -113,13 +113,13 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .TP -.I EDOM +.B EDOM The function was not given any subsentences. .PP The diff --git a/man3/libnormalform_not.3 b/man3/libnormalform_not.3 index 0ebe548..ed6fdca 100644 --- a/man3/libnormalform_not.3 +++ b/man3/libnormalform_not.3 @@ -53,7 +53,7 @@ The .BR libnormalform_not () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_one.3 b/man3/libnormalform_one.3 index bf79161..8aa88a5 100644 --- a/man3/libnormalform_one.3 +++ b/man3/libnormalform_one.3 @@ -192,9 +192,9 @@ The .BR libnormalform_uniquely (), and .BR libnormalform_singleton () -functions fails if: +functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_or.3 b/man3/libnormalform_or.3 index 9d57ee8..c0f58d8 100644 --- a/man3/libnormalform_or.3 +++ b/man3/libnormalform_or.3 @@ -110,9 +110,9 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_ref.3 b/man3/libnormalform_ref.3 index 5592e48..9295f12 100644 --- a/man3/libnormalform_ref.3 +++ b/man3/libnormalform_ref.3 @@ -48,7 +48,7 @@ The .BR libnormalform_ref () function fails if: .TP -.I ENOMEM +.B ENOMEM The reference count of .I x was already maximised (at diff --git a/man3/libnormalform_sentences_relationship.3 b/man3/libnormalform_sentences_relationship.3 new file mode 120000 index 0000000..03be66c --- /dev/null +++ b/man3/libnormalform_sentences_relationship.3 @@ -0,0 +1 @@ +enum_libnormalform_sentences_relationship.3
\ No newline at end of file diff --git a/man3/libnormalform_ternary.3 b/man3/libnormalform_ternary.3 new file mode 120000 index 0000000..96ac9d0 --- /dev/null +++ b/man3/libnormalform_ternary.3 @@ -0,0 +1 @@ +enum_libnormalform_ternary.3
\ No newline at end of file diff --git a/man3/libnormalform_to_string.3 b/man3/libnormalform_to_string.3 index 7008990..2150a10 100644 --- a/man3/libnormalform_to_string.3 +++ b/man3/libnormalform_to_string.3 @@ -62,7 +62,7 @@ The .BR libnormalform_to_string () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to serialise the sentence object. @@ -93,7 +93,7 @@ When a .I LIBNORMALFORM_SENTENCE is created, it is optimised (this includes eliminiation of redundant information and reordering) and reduced to -into fewer types of connetives (it's reducted into negation +into fewer types of connetives (it's reduced into negation normal form, except with XOR allowed, but not necessarily to any canonical form) during construction, so the .BR libnormalform_to_string () diff --git a/man3/libnormalform_transformation.3 b/man3/libnormalform_transformation.3 index 7bb129e..d08ea47 100644 --- a/man3/libnormalform_transformation.3 +++ b/man3/libnormalform_transformation.3 @@ -202,11 +202,11 @@ The .BR libnormalform_transformation () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .TP -.I EDOM +.B EDOM .I sentence contains a qualifier. diff --git a/man3/libnormalform_true.3 b/man3/libnormalform_true.3 index a5da907..77bdf39 100644 --- a/man3/libnormalform_true.3 +++ b/man3/libnormalform_true.3 @@ -40,7 +40,7 @@ The .BR libnormalform_true () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. diff --git a/man3/libnormalform_variable.3 b/man3/libnormalform_variable.3 index ad30a37..dca3d1e 100644 --- a/man3/libnormalform_variable.3 +++ b/man3/libnormalform_variable.3 @@ -96,7 +96,7 @@ The .BR libnormalform_variable () function fails if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. diff --git a/man3/libnormalform_xnor.3 b/man3/libnormalform_xnor.3 index 56a3cab..322becc 100644 --- a/man3/libnormalform_xnor.3 +++ b/man3/libnormalform_xnor.3 @@ -111,9 +111,9 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/libnormalform_xor.3 b/man3/libnormalform_xor.3 index 70e9584..38571b4 100644 --- a/man3/libnormalform_xor.3 +++ b/man3/libnormalform_xor.3 @@ -110,9 +110,9 @@ and set to indicate the error. .SH ERRORS -These functions fails if: +These functions fail if: .TP -.I ENOMEM +.B ENOMEM Insufficient memory was available to create the sentence object. .PP diff --git a/man3/struct_libnormalform_analysers.3 b/man3/struct_libnormalform_analysers.3 new file mode 120000 index 0000000..eae3a15 --- /dev/null +++ b/man3/struct_libnormalform_analysers.3 @@ -0,0 +1 @@ +libnormalform_express.3
\ No newline at end of file diff --git a/man3/struct_libnormalform_atom_comparison.3 b/man3/struct_libnormalform_atom_comparison.3 new file mode 120000 index 0000000..0d9b1eb --- /dev/null +++ b/man3/struct_libnormalform_atom_comparison.3 @@ -0,0 +1 @@ +struct_libnormalform_analysers.3
\ No newline at end of file diff --git a/man3/struct_libnormalform_domain_comparison.3 b/man3/struct_libnormalform_domain_comparison.3 new file mode 120000 index 0000000..0d9b1eb --- /dev/null +++ b/man3/struct_libnormalform_domain_comparison.3 @@ -0,0 +1 @@ +struct_libnormalform_analysers.3
\ No newline at end of file @@ -17,6 +17,16 @@ #include <elfutils/libdwfl.h> +#if defined(__GNUC__) +# pragma GCC diagnostic ignored "-Wpadded" +#endif +#if defined(__clang__) +# pragma clang diagnostic ignored "-Wunsafe-buffer-usage" +# pragma clang diagnostic ignored "-Wcomma" +# pragma clang diagnostic ignored "-Wunsafe-buffer-usage" /* clang is currently exceptionally stupid */ +#endif + + enum alloctype { ALLOCTYPE_REALLOC, ALLOCTYPE_MMAP @@ -150,7 +160,8 @@ fail: static void memcheck_print_backtrace(struct backtrace *backtrace, const char *indent) { - int saved_errno = errno, lineno; + int saved_errno = errno; + int lineno = 0; /* initialised to silence compiler */ char *debuginfo_path = NULL; Dwarf_Addr ip; Dwfl_Callbacks callbacks; @@ -172,6 +183,8 @@ memcheck_print_backtrace(struct backtrace *backtrace, const char *indent) callbacks.find_debuginfo = dwfl_standard_find_debuginfo; callbacks.debuginfo_path = &debuginfo_path; + dwfl = dwfl_begin(&callbacks); + if (dwfl) { if (dwfl_linux_proc_report(dwfl, getpid()) || dwfl_report_end(dwfl, NULL, NULL)) { @@ -211,10 +224,12 @@ memcheck_print_backtrace(struct backtrace *backtrace, const char *indent) #endif -#if defined(__GNUC__) +#if defined(__clang__) +__attribute__((__format__(__printf__, 1, 2))) +#elif defined(__GNUC__) __attribute__((__format__(__gnu_printf__, 1, 2))) #endif -static void +static _Noreturn void memcheck_errorf(const char *fmt, ...) { va_list ap; @@ -610,6 +625,7 @@ memcheck_check_memleaks(void) { struct allocinfo *leak; size_t i, count = 0; + int first = 1; memleak_exclusion = 1; for (i = 0; i < nallocs; i++) { leak = &allocs[i]; @@ -625,6 +641,10 @@ memcheck_check_memleaks(void) leak = &allocs[i]; if (leak->dont_track) continue; + if (first) + first = 0; + else + dprintf(STDERR_FILENO, "\n"); memcheck_print_backtrace(leak->backtrace, "\t"); } #endif |