diff options
Diffstat (limited to '')
| -rw-r--r-- | common.h | 632 |
1 files changed, 632 insertions, 0 deletions
diff --git a/common.h b/common.h new file mode 100644 index 0000000..68df99c --- /dev/null +++ b/common.h @@ -0,0 +1,632 @@ +/* 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 |