diff --git a/resources/3rdparty/sylvan/src/lace.h b/resources/3rdparty/sylvan/src/lace.h index 419cd222a..7933d98d7 100644 --- a/resources/3rdparty/sylvan/src/lace.h +++ b/resources/3rdparty/sylvan/src/lace.h @@ -66,6 +66,7 @@ extern "C" { #define PAD(x,b) ( ( (b) - ((x)%(b)) ) & ((b)-1) ) /* b must be power of 2 */ #define ROUND(x,b) ( (x) + PAD( (x), (b) ) ) +#define MINONE(x) ((x < 1) ? (1) : (x)) /* The size is in bytes. Note that this is without the extra overhead from Lace. The value must be greater than or equal to the maximum size of your tasks. @@ -183,7 +184,7 @@ struct __lace_common_fields_only { TASK_COMMON_FIELDS(_Task) }; typedef struct _Task { TASK_COMMON_FIELDS(_Task); - char p1[PAD(LACE_COMMON_FIELD_SIZE, P_SZ)]; + char p1[MINONE(PAD(LACE_COMMON_FIELD_SIZE, P_SZ))]; char d[LACE_TASKSIZE]; char p2[PAD(ROUND(LACE_COMMON_FIELD_SIZE, P_SZ) + LACE_TASKSIZE, LINE_SIZE)]; } Task; @@ -226,7 +227,7 @@ typedef struct _WorkerP { uint32_t seed; // my random seed (for lace_steal_random) } WorkerP; -#define LACE_TYPEDEF_CB(t, f, ...) typedef t (*f)(WorkerP *, Task *, ##__VA_ARGS__); +#define LACE_TYPEDEF_CB(t, f, ...) typedef t (*f)(WorkerP *, Task *, ##__VA_ARGS__) LACE_TYPEDEF_CB(void, lace_startup_cb, void*); /** @@ -648,7 +649,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head ) if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head+1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -760,7 +762,7 @@ RTYPE NAME##_CALL(WorkerP *w, Task *__dq_head ) static inline __attribute__((always_inline)) \ RTYPE NAME##_WORK(WorkerP *__lace_worker __attribute__((unused)), Task *__lace_dq_head __attribute__((unused)) )\ -#define TASK_0(RTYPE, NAME) TASK_DECL_0(RTYPE, NAME) TASK_IMPL_0(RTYPE, NAME) +#define TASK_0(RTYPE, NAME) TASK_DECL_0(RTYPE, NAME); TASK_IMPL_0(RTYPE, NAME) #define VOID_TASK_DECL_0(NAME) \ \ @@ -798,7 +800,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head ) if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -951,7 +954,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1) if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -1101,7 +1105,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1) if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -1254,7 +1259,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2) if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -1404,7 +1410,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2) if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -1557,7 +1564,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2, AT if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -1707,7 +1715,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2, AT if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -1860,7 +1869,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2, AT if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -2010,7 +2020,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2, AT if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -2163,7 +2174,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2, AT if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -2313,7 +2325,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2, AT if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -2466,7 +2479,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2, AT if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ @@ -2616,7 +2630,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1, ATYPE_2 arg_2, AT if (unlikely(w->allstolen)) { \ if (wt->movesplit) wt->movesplit = 0; \ head = __dq_head - w->dq; \ - ts = (TailSplit){{head,head+1}}; \ + ts.ts.tail = head; \ + ts.ts.split = head + 1; \ wt->ts.v = ts.v; \ compiler_barrier(); \ wt->allstolen = 0; \ diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 38fa6668b..a35fd8398 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -6,7 +6,7 @@ void mtbdd_getsha(MTBDD mtbdd, char *target); // target must be at least 65 byte * If either operand is mtbdd_false (not defined), * then the result is mtbdd_false (i.e. not defined). */ -TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*) #define mtbdd_divide(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_divide)) /** @@ -15,7 +15,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*) #define mtbdd_equals(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_equals)) /** @@ -24,7 +24,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*) #define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less)) /** @@ -33,7 +33,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*) #define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal)) /** @@ -42,7 +42,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_pow, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_pow, MTBDD*, MTBDD*) #define mtbdd_pow(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_pow)) /** @@ -51,7 +51,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_pow, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_mod, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_mod, MTBDD*, MTBDD*) #define mtbdd_mod(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_mod)) /** @@ -60,7 +60,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_mod, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_logxy, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_logxy, MTBDD*, MTBDD*) #define mtbdd_logxy(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_logxy)) /** @@ -101,7 +101,7 @@ TASK_DECL_1(MTBDD, mtbdd_bool_to_int64, MTBDD) /** * Count the number of assignments (minterms) leading to a non-zero */ -TASK_DECL_2(double, mtbdd_non_zero_count, MTBDD, size_t); +TASK_DECL_2(double, mtbdd_non_zero_count, MTBDD, size_t) #define mtbdd_non_zero_count(dd, nvars) CALL(mtbdd_non_zero_count, dd, nvars) // Checks whether the given MTBDD (does represents a zero leaf. diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index f97347690..6cdb142a5 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -34,29 +34,29 @@ MTBDD mtbdd_storm_rational_function(storm_rational_function_t val); /** * Operation "plus" for two storm::RationalFunction MTBDDs */ -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, MTBDD*); -TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, MTBDD, int); +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, MTBDD*) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, MTBDD, int) /** * Operation "minus" for two storm::RationalFunction MTBDDs */ -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, MTBDD*) /** * Operation "times" for two storm::RationalFunction MTBDDs */ -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, MTBDD*); -TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBDD, int); +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, MTBDD*) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBDD, int) /** * Operation "divide" for two storm::RationalFunction MTBDDs */ -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, MTBDD*) /** * Operation "negate" for one storm::RationalFunction MTBDD */ -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t); +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t) /** * Compute a + b