/* See LICENSE file for copyright and license details. */ #ifndef LIBNORMALFORM_ALLOW_BAD_WARNINGS # define LIBNORMALFORM_ALLOW_BAD_WARNINGS #endif #include "libnormalform.h" #include #include #include #include #include #include #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 #include #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