sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Fixed a few of Sylvans nasty habits. 

Former-commit-id: e965a8f613
tempestpy_adaptions
PBerger 8 years ago
parent
ec3b5d2aac
commit
ca65cecbfd
3 changed files with 47 additions and 32 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 49
      resources/3rdparty/sylvan/src/lace.h
  2. 16
      resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
  3. 14
      resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h

49
resources/3rdparty/sylvan/src/lace.h
View File

@ -66,6 +66,7 @@ extern "C" {
#define PAD(x,b) ( ( (b) - ((x)%(b)) ) & ((b)-1) ) /* b must be power of 2 */ #define PAD(x,b) ( ( (b) - ((x)%(b)) ) & ((b)-1) ) /* b must be power of 2 */
#define ROUND(x,b) ( (x) + PAD( (x), (b) ) ) #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 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. 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 { typedef struct _Task {
TASK_COMMON_FIELDS(_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 d[LACE_TASKSIZE];
char p2[PAD(ROUND(LACE_COMMON_FIELD_SIZE, P_SZ) + LACE_TASKSIZE, LINE_SIZE)]; char p2[PAD(ROUND(LACE_COMMON_FIELD_SIZE, P_SZ) + LACE_TASKSIZE, LINE_SIZE)];
} Task; } Task;
@ -226,7 +227,7 @@ typedef struct _WorkerP {
uint32_t seed; // my random seed (for lace_steal_random) uint32_t seed; // my random seed (for lace_steal_random)
} WorkerP; } 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*); 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head+1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ wt->allstolen = 0; \
@ -760,7 +762,7 @@ RTYPE NAME##_CALL(WorkerP *w, Task *__dq_head )
static inline __attribute__((always_inline)) \ static inline __attribute__((always_inline)) \
RTYPE NAME##_WORK(WorkerP *__lace_worker __attribute__((unused)), Task *__lace_dq_head __attribute__((unused)) )\ 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) \ #define VOID_TASK_DECL_0(NAME) \
\ \
@ -798,7 +800,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head )
if (unlikely(w->allstolen)) { \ if (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ wt->allstolen = 0; \
@ -951,7 +954,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1)
if (unlikely(w->allstolen)) { \ if (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ wt->allstolen = 0; \
@ -1101,7 +1105,8 @@ void NAME##_SPAWN(WorkerP *w, Task *__dq_head , ATYPE_1 arg_1)
if (unlikely(w->allstolen)) { \ if (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ 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 (unlikely(w->allstolen)) { \
if (wt->movesplit) wt->movesplit = 0; \ if (wt->movesplit) wt->movesplit = 0; \
head = __dq_head - w->dq; \ head = __dq_head - w->dq; \
ts = (TailSplit){{head,head+1}}; \
ts.ts.tail = head; \
ts.ts.split = head + 1; \
wt->ts.v = ts.v; \ wt->ts.v = ts.v; \
compiler_barrier(); \ compiler_barrier(); \
wt->allstolen = 0; \ wt->allstolen = 0; \

16
resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
View File

@ -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), * If either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. 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)) #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), * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand. * 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)) #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), * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand. * 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)) #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), * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand. * 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)) #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), * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand. * 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)) #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), * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand. * 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)) #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), * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand. * 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)) #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 * 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) #define mtbdd_non_zero_count(dd, nvars) CALL(mtbdd_non_zero_count, dd, nvars)
// Checks whether the given MTBDD (does represents a zero leaf. // Checks whether the given MTBDD (does represents a zero leaf.

14
resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h
View File

@ -34,29 +34,29 @@ MTBDD mtbdd_storm_rational_function(storm_rational_function_t val);
/** /**
* Operation "plus" for two storm::RationalFunction MTBDDs * 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 * 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 * 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 * 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 * 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 * Compute a + b

Write Preview
Loading…
Cancel
Save