path: root/common.h

/* 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
#include "libnormalform.h"

#include <ctype.h>
#include <errno.h>
#include <limits.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>


#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")))
# define USE_RESULT __attribute__((__warn_unused_result__))
# define NONNULL_INPUT __attribute__((__nonnull__))
# define SOME_NONNULL_INPUT(...) __attribute__((__nonnull__(__VA_ARGS__)))
#else
# define PURE
# define CONST
# define HIDDEN
# define USE_RESULT
# define NONNULL_INPUT
# define SOME_NONNULL_INPUT(...)
#endif


/**
 * Hash used for tautologies and contradictions
 */
#define TRUE_FALSE_HASH 1U

/**
 * Returns the has for a user provided object
 * 
 * @param  A  The user provided object
 */
#define USER_HASH__(P) ((uintmax_t)(uintptr_t)(P))

/**
 * Hash generator for literals
 * 
 * @param  A  The atomic sentence of the literal
 */
#define LITERAL_HASH(A)\
	_Generic((A),\
		struct libnormalform_variable *: USER_HASH__((A)),\
		struct libnormalform_function *: USER_HASH__((A)))

/**
 * Hash generator for transformations
 * 
 * @param  F:struct libnormalform_transformer *  The transformation function
 * @param  S:LIBNORMALFORM_SENTENCE *            The sentence
 */
#define TRANS_HASH(F, S)\
	_Generic((F), struct libnormalform_transformer *:\
		 (USER_HASH__(F) ^ (S)->hash))

/**
 * Hash generator for conjunctions and disjunctions
 * 
 * @param  L:LIBNORMALFORM_SENTENCE *  The left-hand term
 * @param  R:LIBNORMALFORM_SENTENCE *  The right-hand term
 */
#define AND_OR_HASH(L, R) ((L)->hash + (R)->hash)

/**
 * Hash generator for exclusive disjunctions
 *
 * The reason this is twice of conjunction or disjunction
 * is because a ⊕ b = (a ∨ b) ∧ ¬(a ∧ b) and
 * (a ∨ b) and ¬(a ∧ b) have the same hashes, and if
 * if u = (a ∨ b) and v = ¬(a ∧ b), the hash of
 * u ∧ v is the sum of the hashes of u and v which
 * are both the sum of the hashes of a and b, thus
 * twice the hash of a and b.
 * 
 * @param  L:LIBNORMALFORM_SENTENCE *  The left-hand term
 * @param  R:LIBNORMALFORM_SENTENCE *  The right-hand term
 */
#define XOR_HASH(L, R) (AND_OR_HASH(L, R) * 2)

/**
 * Hash generator for universial and existential qualifiers
 * 
 * @param  D:struct libnormalform_map *  The domain
 * @param  K:LIBNORMALFORM_SENTENCE *    The antecedent (left-hand term)
 * @param  V:LIBNORMALFORM_SENTENCE *    The predicate (right-hand term)
 */
#define ANY_ALL_HASH(D, K, V)\
	_Generic((D), struct libnormalform_map *:\
		(USER_HASH__(D) * 5 + AND_OR_HASH(K, V) * 3))

/**
 * Hash generator for uniqueness qualifiers
 * 
 * @param  D:struct libnormalform_map *  The domain
 * @param  K:LIBNORMALFORM_SENTENCE *    The antecedent (left-hand term)
 * @param  V:LIBNORMALFORM_SENTENCE *    The predicate (right-hand term)
 */
#define ONE_HASH(D, K, V)\
	_Generic((D), struct libnormalform_map *:\
		(USER_HASH__(D) * 5 + AND_OR_HASH(K, V) * 7))


/**
 * Offset for values in `enum type`,
 * used by `libnormalform_free` to distinguish
 * `struct libnormalform_sentence *` for
 * `struct libnormalform_term *`
*/
#define SENTENCE_TYPE_OFFSET 1024


/**
 * Normal forms
 */
enum normal_form {
	NNF,  /**< Negation normal form, optinally with XOR */
	DNF,  /**< Disjunctive normal form */
	CNF   /**< Conjunctive normal form */
};


/**
 * Sentence classification
 */
enum type {
	TYPE_TRUE = SENTENCE_TYPE_OFFSET,  /**< Tautology */
	TYPE_FALSE,                        /**< Contradiction */
	TYPE_VARIABLE,                     /**< Variable literal */
	TYPE_FUNCTION,                     /**< Function literal */
	TYPE_TRANS,                        /**< Input transformation */
	/* Insert new non-branches (leafs and lines) above */
	TYPE_AND,                          /**< Conjuction */
	TYPE_OR,                           /**< Disjunction */
	TYPE_XOR,                          /**< Exclusive disjunction */
	TYPE_ALL,                          /**< Univerial qualification */
	TYPE_ANY,                          /**< Existential qualification */
	TYPE_ONE,                          /**< Uniqueness qualification */
	TYPE_NOT_ONE                       /**< Negated uniqueness qualification */
	/* Insert new binary branches here */
};


struct atom { /* TODO doc */
	/**
	 * The number of references to the object
	 */
	size_t refcount;
};


/**
 * See `LIBNORMALFORM_SENTENCE`
 */
struct libnormalform_sentence {
	/**
	 * Sentence classification
	 */
	enum type type;

	/**
	 * The number of references to the object
	 */
	size_t refcount;

	/**
	 * Hash of the sentence
	 *
	 * For any two sentences it is preferably that
	 * they have the same hash if and only if they
	 * can be determined to be equivalent or each
	 * other's inverse
	 */
	uintmax_t hash;

	struct atom *atom; /* TODO doc */

	/**
	 * Used by some function for sentence analysis,
	 * in particular to index duplicated subsentence
	 */
	size_t travel_index;

	/**
	 * Used by some function for sentence analysis,
	 * in particular to count duplications
	 */
	size_t travel_count;

	/**
	 * Used by some function recurse over the sentence
	 */
	LIBNORMALFORM_SENTENCE *travel_head;

	/**
	 * Create the inverse of the sentence
	 * 
	 * @param   this  The sentence
	 * @return        The inverse of the sentence, `NULL` on failure
	 * 
	 * @throws  ENOMEM  Insufficient memory available to create the sentence
	 * 
	 * Unlike `libnormalform_not`, this function
	 * will not take ownership if `this`, so
	 * its reference count will not be modified
	 */
	LIBNORMALFORM_SENTENCE *(*inverse)(LIBNORMALFORM_SENTENCE *this);

	/**
	 * Check the equivalence between the sentence and another sentence
	 * 
	 * @param   this     The sentence
	 * @param   other    The the other sentence 
	 * @param   inv_out  Will be set to 0 if the sentences are equivalent,
	 *                   and set to 1 if the sentences are each other's inverse
	 * @return           1 if the functions are equal or each other's inverse,
	 *                   0 otherwise
	 */	
	int (*equals)(LIBNORMALFORM_SENTENCE *this, LIBNORMALFORM_SENTENCE *other, int *inv_out);

	/**
	 * Evaluate the truthness of the sentence
	 * 
	 * @param   this   The sentence
	 * @param   input  See `libnormalform_evaluate`
	 * @return         See `libnormalform_evaluate`
	 */
	int (*evaluate)(LIBNORMALFORM_SENTENCE *this, void *input);

	/**
	 * Type specification information
	 *
	 * Unused if `.type` is `TYPE_TRUE` or `TYPE_FALSE`
	 */
	union {
		/**
		 * Used for literals (that is,
		 * if `.type` is `TYPE_VARIABLE` or `TYPE_FUNCTION`)
		 */
		struct {
			/**
			 * The literal's atomic sentence
			 */
			union {
				struct libnormalform_variable *variable; /**< Use if `.type == TYPE_VARIABLE` */
				struct libnormalform_function *function; /**< Use if `.type == TYPE_FUNCTION` */
			} atom;

			/**
			 * Whether the literal is the inverse of its atomic sentence
			 */
			int inverted;
		} literal;

		/**
		 * Used for input transformations (that is,
		 * if `.type` is `TYPE_TRANS`)
		 */
		struct {
			LIBNORMALFORM_SENTENCE *input;              /**< Input */
			struct libnormalform_transformer *function; /**< Transformation function */
		} trans;

		/**
		 * Used for binary connectives (that is,
		 * if `.type` is `TYPE_AND`, `TYPE_OR`, or `TYPE_XOR`)
		 * 
		 * Traversal code can also use this instead of `.data.qualifer`
		 */
		struct {
			LIBNORMALFORM_SENTENCE *l; /**< Left-hand term */
			LIBNORMALFORM_SENTENCE *r; /**< Right-hand term */
		} binary;

		/**
		 * Used for qualifiers (that is,
		 * if `.type` is `TYPE_ALL`, `TYPE_ANY`, `TYPE_ONE`, `TYPE_NOT_ONE`)
		 */
		struct {
			LIBNORMALFORM_SENTENCE *antecedent; /**< Antecedent */
			LIBNORMALFORM_SENTENCE *predicate;  /**< Predicate */
			struct libnormalform_map *domain;   /**< Domain of interest */
		} qualifier;
	} data;
};

/**
 * Intial values for `struct libnormalform_sentence`
 * that should always be used
 */
#define PROTOTYPE_COMMON\
	.refcount = 1U,\
	.atom = NULL,\
	.travel_index = 0U,\
	.travel_count = 0U


/**
 * 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))

/**
 * Transversal helper macro that return 1
 * if a sentence has two subsentences
 * 
 * @param   S:LIBNORMALFORM_SENTENCE *  The sentence
 * @return  :int                        1 if the sentence has two subsentences, 0 otherwise
 */
#define IS_BRANCH(S) REQ_SENTENCE((S), *, (S)->type >= TYPE_AND)

/**
 * Transversal helper macro that returns
 * the left-hand subsentence (antecedent
 * for qualifiers)
 * 
 * @param   S:LIBNORMALFORM_SENTENCE *  The sentence
 * @return  :LIBNORMALFORM_SENTENCE *   The left subsentence
 */
#define LEFT(S) REQ_SENTENCE((S), *, (S)->data.binary.l)

/**
 * Transversal helper macro that returns
 * the right-hand subsentence (predicate
 * for qualifiers)
 * 
 * @param   S:LIBNORMALFORM_SENTENCE *  The sentence
 * @return  :LIBNORMALFORM_SENTENCE *   The right subsentence
 */
#define RIGHT(S) REQ_SENTENCE((S), *, (S)->data.binary.r)

/**
 * Transversal helper macro that pushes
 * a sentence onto a stack
 * 
 * @param  UNTO:LIBNORMALFORM_SENTENCE **  Reference to the head of the stack
 * @param  S:LIBNORMALFORM_SENTENCE *      The sentence
 */
#define PUSH(UNTO, S)\
	REQ_SENTENCE((UNTO), **,\
	REQ_SENTENCE((S), *,\
		((S)->travel_head = *(UNTO), *(UNTO) = (S), (void) 0)\
	))

/**
 * Transversal helper macro that pops
 * a sentence stack
 * 
 * @param   FROM:LIBNORMALFORM_SENTENCE **  Reference to the head of the stack
 * @param   INTO:LIBNORMALFORM_SENTENCE **  Output parameter for the sentence popped from the stack
 * @return  :int                            1 if a sentences was popped,
 *                                          0 if the stack was empty (*(INTO) will be set to `NULL`)
 */
#define POP(FROM, INTO)\
	REQ_SENTENCE((FROM), **,\
	REQ_SENTENCE((INTO), **,\
		((*(INTO) = *(FROM)) ? (*(FROM) = (*(INTO))->travel_head, 1) : 0)\
	))





/**
 * Create a non-reduced AND expression with two terms
 * 
 * @param   l  The left-hand term; ownership is transfered to the function
 * @param   r  The right-hand term; ownership is transfered to the function
 * @return     The expression (l ∧ r) (may commuted), `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
HIDDEN USE_RESULT NONNULL_INPUT
LIBNORMALFORM_SENTENCE *(libnormalform_and2__)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);

/**
 * Create a non-reduced OR expression with two terms
 * 
 * @param   l  The left-hand term; ownership is transfered to the function
 * @param   r  The right-hand term; ownership is transfered to the function
 * @return     The expression (l ∨ r) (may commuted), `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
HIDDEN USE_RESULT NONNULL_INPUT
LIBNORMALFORM_SENTENCE *(libnormalform_or2__)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);

/**
 * Create a non-reduced XOR expression with two terms
 * 
 * @param   l  The left-hand term; ownership is transfered to the function
 * @param   r  The right-hand term; ownership is transfered to the function
 * @return     The expression (l ⊕ r) (may commuted), `NULL` on failure
 * 
 * @throws  ENOMEM  Insufficient memory available to create the sentence
 * 
 * Ownership is always transfered, even on failure
 * 
 * If `l` or `r` is `NULL`, the function will call
 * `libnormalform_free` on both arguments and return
 * `NULL` (indicating failure) without setting
 * `errno` (expected to already be set in indicate the
 * error that caused one of the terms to be `NULL`)
 */
HIDDEN USE_RESULT NONNULL_INPUT
LIBNORMALFORM_SENTENCE *(libnormalform_xor2__)(LIBNORMALFORM_SENTENCE *l, LIBNORMALFORM_SENTENCE *r);

/**
 * Annotate every sentence that appear multiple times
 * with a unique index (counted from 0 up)
 * 
 * @param   this  The sentence that shall be inspected
 *                recursively for annotation
 * @return        The number of annotated sentences
 */
HIDDEN USE_RESULT NONNULL_INPUT
size_t (libnormalform_set_indices_and_counts__)(LIBNORMALFORM_SENTENCE *this);

/**
 * Undo `libnormalform_set_indices_and_counts__`
 * 
 * This is needed because `libnormalform_set_indices_and_counts__`
 * requires some otherwise unused memory to be properly initialised
 * 
 * @param   this  The sentence that shall be recursively restored
 */
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 */
void libnormalform__debug_print__(LIBNORMALFORM_SENTENCE *this, size_t depth_limit);
#endif


#if defined(__GNUC__)
# pragma GCC diagnostic ignored "-Winline"
#endif





#ifdef TEST

#include <sys/resource.h>
#include <unistd.h>

#ifdef CHECK_MEMLEAK
# include "memcheck.h"
# define IF_MEMCHECK(...) __VA_ARGS__
#else
# define IF_MEMCHECK(...)
#endif

#define MEMLIMIT (512UL * 1024UL * 1024UL) /* valgrind requires quite a bit (but not this much) */

#define SET_LIMIT(WHAT, HOW_MUCH)\
	do {\
		struct rlimit lim;\
		if (getrlimit(WHAT, &lim)) {\
			perror("getrlimit "#WHAT);\
			break;\
		}\
		if ((HOW_MUCH) < lim.rlim_cur)\
			lim.rlim_cur = (HOW_MUCH);\
		lim.rlim_max = lim.rlim_cur;\
		if (setrlimit(WHAT, &lim)) {\
			perror("setrlimit "#WHAT);\
			break;\
		}\
	} while (0)

#define TEST_BEGIN\
	SET_LIMIT(RLIMIT_CORE, 0);\
	SET_LIMIT(RLIMIT_AS, MEMLIMIT);\
	SET_LIMIT(RLIMIT_DATA, MEMLIMIT);\
	SET_LIMIT(RLIMIT_RSS, MEMLIMIT);\
	SET_LIMIT(RLIMIT_STACK, MEMLIMIT);\
	SET_LIMIT(RLIMIT_CPU, TEST_TIMEOUT_SECONDS);\
	alarm(TEST_TIMEOUT_SECONDS);\
	IF_MEMCHECK(memcheck_begin();)\
	do {\
		int exit_value_just_to_remove_warnings_about_this_following_variable_definitions__ = 0

#define TEST_END\
		IF_MEMCHECK(if (!memcheck_check_memleaks()) exit(1);)\
		exit(exit_value_just_to_remove_warnings_about_this_following_variable_definitions__); \
	} while (0)
					       

#define ASSUME(X)\
	do {\
		int assumption_saved_errno__ = errno;\
		errno = 0;\
		if (!(X)) {\
			fprintf(stderr, "Assumption `%s` failed at %s:%i, errno: %s\n", #X, __FILE__, __LINE__, strerror(errno));\
			exit(1);\
		}\
		errno = assumption_saved_errno__;\
	} while (0)

#define ASSERT(X)\
	do {\
		if (!(X)) {\
			fprintf(stderr, "Assertion `%s` failed at %s:%i\n", #X, __FILE__, __LINE__);\
			exit(1);\
		}\
	} while (0)

#define ASSERT_EQUAL(A, B)\
	do {\
		int inv__;\
		LIBNORMALFORM_SENTENCE *a__ = (A);\
		LIBNORMALFORM_SENTENCE *b__ = (B);\
		ASSERT(a__->equals(a__, b__, &inv__) == 1);\
		ASSERT(inv__ == 0);\
	} while (0)

#define ASSERT_INVEQUAL(A, B)\
	do {\
		int inv__;\
		LIBNORMALFORM_SENTENCE *a__ = (A);\
		LIBNORMALFORM_SENTENCE *b__ = (B);\
		ASSERT(a__->equals(a__, b__, &inv__) == 1);\
		ASSERT(inv__ == 1);\
	} while (0)

#define ASSERT_NOTEQUAL(A, B)\
	do {\
		int inv__;\
		LIBNORMALFORM_SENTENCE *a__ = (A);\
		LIBNORMALFORM_SENTENCE *b__ = (B);\
		ASSERT(a__->equals(a__, b__, &inv__) == 0);\
	} while (0)

#define REF libnormalform_ref

#define VALIST(...) __VA_OPT__(__VA_ARGS__,) NULL
#define LIST(...)   ((LIBNORMALFORM_SENTENCE *[]){VALIST(__VA_ARGS__)})
#define COUNT(...)  (sizeof(LIST(__VA_ARGS__)) / sizeof(LIBNORMALFORM_SENTENCE *) - 1U)

#if defined(USE_TWO)
# define USE_CHECKED_VERSION
# undef LIBNORMALFORM_MACRO__
# define LIBNORMALFORM_MACRO__(CONNECTIVE, A, B)\
	libnormalform_##CONNECTIVE##2(A, B)

#elif defined(USE_VARARGS) || defined(USE_VARARGS_MACRO)
# undef LIBNORMALFORM_MACRO__
# define LIBNORMALFORM_MACRO__(CONNECTIVE, ...)\
	(libnormalform_##CONNECTIVE##l(VALIST(__VA_ARGS__)))

#elif defined(USE_CHECKED_VARARGS)
# define USE_CHECKED_VERSION
# undef LIBNORMALFORM_MACRO__
# define LIBNORMALFORM_MACRO__(CONNECTIVE, ...)\
	(libnormalform_##CONNECTIVE##l_checked(COUNT(__VA_ARGS__), VALIST(__VA_ARGS__)))

#elif defined(USE_VALIST)
# undef LIBNORMALFORM_MACRO__
# define LIBNORMALFORM_MACRO__(CONNECTIVE, ...)\
	(vatrampoline(&libnormalform_v##CONNECTIVE, VALIST(__VA_ARGS__)))
USE_RESULT static LIBNORMALFORM_SENTENCE *
vatrampoline(LIBNORMALFORM_SENTENCE *(*f)(LIBNORMALFORM_SENTENCE *, va_list),
             LIBNORMALFORM_SENTENCE *a, ...)
{
	LIBNORMALFORM_SENTENCE *ret;
	va_list args;
	va_start(args, a);
	ret = (*f)(a, args);
	va_end(args);
	return ret;
}

#elif defined(USE_CHECKED_VALIST)
# define USE_CHECKED_VERSION
# undef LIBNORMALFORM_MACRO__
# define LIBNORMALFORM_MACRO__(CONNECTIVE, ...)\
	(vatrampoline(&libnormalform_v##CONNECTIVE##_checked, COUNT(__VA_ARGS__), VALIST(__VA_ARGS__)))
USE_RESULT static LIBNORMALFORM_SENTENCE *
vatrampoline(LIBNORMALFORM_SENTENCE *(*f)(size_t, LIBNORMALFORM_SENTENCE *, va_list),
             size_t n, LIBNORMALFORM_SENTENCE *a, ...)
{
	LIBNORMALFORM_SENTENCE *ret;
	va_list args;
	va_start(args, a);
	ret = (*f)(n, a, args);
	va_end(args);
	return ret;
}

#elif defined(USE_CHECKED)
# define USE_CHECKED_VERSION

#else
# undef LIBNORMALFORM_MACRO__
# define LIBNORMALFORM_MACRO__(CONNECTIVE, ...)\
	(libnormalform_##CONNECTIVE(LIST(__VA_ARGS__)))
#endif

#if !defined(USE_VARARGS_MACRO)
# undef libnormalform_andl
# undef libnormalform_orl
# undef libnormalform_xorl
# undef libnormalform_ifl
# undef libnormalform_implyl
# undef libnormalform_nandl
# undef libnormalform_norl
# undef libnormalform_xnorl
# undef libnormalform_nifl
# undef libnormalform_nimplyl
#endif

#define TO\
DO_TEST /* no indent before, breaking the word TO|DO to hide from grep */ CONST int main(void) {return 0;}

#endif

#endif