Second commitHEADmaster

Signed-off-by: Mattias Andrée <m@maandree.se>

1 files changed, 311 insertions, 0 deletions

diff --git a/common.h b/common.h
index 68df99c..7b2eaa9 100644
--- a/common.h
+++ b/common.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