path: root/common.h

/* See LICENSE file for copyright and license details. */
#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__)
# 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


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


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


#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