From 68b14b307608d82368aa2040f5eb2e8411913ead Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 24 Aug 2016 18:17:13 +0200 Subject: [PATCH] Moved BDD functionality in Sylvan to sylvan_bdd_int.h to allow reuse. Added min/maxExistsRepresentative API to storage/dd/Add. Former-commit-id: 45ff98b35a5d5429f9f862dc408caf07c56391f6 --- .../sylvan/src/storm_function_wrapper.cpp | 15 ++ .../sylvan/src/storm_function_wrapper.h | 3 + resources/3rdparty/sylvan/src/sylvan_bdd.c | 212 ++++++----------- .../3rdparty/sylvan/src/sylvan_bdd_int.h | 87 +++++++ .../3rdparty/sylvan/src/sylvan_bdd_storm.c | 6 +- resources/3rdparty/sylvan/src/sylvan_gmp.c | 6 +- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 158 ++++++------- .../3rdparty/sylvan/src/sylvan_mtbdd_int.h | 2 +- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 220 +++++++++--------- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.h | 5 +- .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 4 +- .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 4 +- .../src/sylvan_storm_rational_function.c | 23 +- .../src/sylvan_storm_rational_function.h | 21 +- src/storage/dd/Add.cpp | 12 + src/storage/dd/Add.h | 18 ++ src/storage/dd/cudd/InternalCuddAdd.cpp | 13 ++ src/storage/dd/cudd/InternalCuddAdd.h | 14 ++ src/storage/dd/sylvan/InternalSylvanAdd.cpp | 10 + src/storage/dd/sylvan/InternalSylvanAdd.h | 14 ++ 20 files changed, 505 insertions(+), 342 deletions(-) create mode 100644 resources/3rdparty/sylvan/src/sylvan_bdd_int.h diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp index 6cd79305e..4c7765781 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp @@ -4,6 +4,7 @@ #include #include #include "src/adapters/CarlAdapter.h" +#include "sylvan_storm_rational_function.h" #undef DEBUG_STORM_FUNCTION_WRAPPER @@ -204,3 +205,17 @@ void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* std::string s = ss.str(); fprintf(out, "%s", s.c_str()); } + +MTBDD storm_rational_function_leaf_parameter_replacement(uint64_t node_value, uint32_t node_type, void* context) { + if (node_type != sylvan_storm_rational_function_get_type()) { + // + } else { + // + } + + (void)node_value; + (void)node_type; + (void)context; + + return mtbdd_invalid; +} diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.h b/resources/3rdparty/sylvan/src/storm_function_wrapper.h index ca5107dcb..0530dc584 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.h +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.h @@ -3,6 +3,7 @@ #include #include +#include #ifdef __cplusplus extern "C" { @@ -30,6 +31,8 @@ void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* int storm_rational_function_is_zero(storm_rational_function_ptr a); +MTBDD storm_rational_function_leaf_parameter_replacement(uint64_t node_value, uint32_t node_type, void* context); + #ifdef __cplusplus } #endif diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd.c b/resources/3rdparty/sylvan/src/sylvan_bdd.c index 6b6b3f74f..281c99bc3 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_bdd.c @@ -30,69 +30,7 @@ #include #include #include - -/** - * Complement handling macros - */ -#define BDD_HASMARK(s) (s&sylvan_complement?1:0) -#define BDD_TOGGLEMARK(s) (s^sylvan_complement) -#define BDD_STRIPMARK(s) (s&~sylvan_complement) -#define BDD_TRANSFERMARK(from, to) (to ^ (from & sylvan_complement)) -// Equal under mark -#define BDD_EQUALM(a, b) ((((a)^(b))&(~sylvan_complement))==0) - -/** - * BDD node structure - */ -typedef struct __attribute__((packed)) bddnode { - uint64_t a, b; -} * bddnode_t; // 16 bytes - -#define GETNODE(bdd) ((bddnode_t)llmsset_index_to_ptr(nodes, bdd&0x000000ffffffffff)) - -static inline int __attribute__((unused)) -bddnode_getcomp(bddnode_t n) -{ - return n->a & 0x8000000000000000 ? 1 : 0; -} - -static inline uint64_t -bddnode_getlow(bddnode_t n) -{ - return n->b & 0x000000ffffffffff; // 40 bits -} - -static inline uint64_t -bddnode_gethigh(bddnode_t n) -{ - return n->a & 0x800000ffffffffff; // 40 bits plus high bit of first -} - -static inline uint32_t -bddnode_getvariable(bddnode_t n) -{ - return (uint32_t)(n->b >> 40); -} - -static inline int -bddnode_getmark(bddnode_t n) -{ - return n->a & 0x2000000000000000 ? 1 : 0; -} - -static inline void -bddnode_setmark(bddnode_t n, int mark) -{ - if (mark) n->a |= 0x2000000000000000; - else n->a &= 0xdfffffffffffffff; -} - -static inline void -bddnode_makenode(bddnode_t n, uint32_t var, uint64_t low, uint64_t high) -{ - n->a = high; - n->b = ((uint64_t)var)<<40 | low; -} +#include /** * Implementation of garbage collection. @@ -104,7 +42,7 @@ VOID_TASK_IMPL_1(sylvan_gc_mark_rec, BDD, bdd) if (bdd == sylvan_false || bdd == sylvan_true) return; if (llmsset_mark(nodes, bdd&0x000000ffffffffff)) { - bddnode_t n = GETNODE(bdd); + bddnode_t n = BDD_GETNODE(bdd); SPAWN(sylvan_gc_mark_rec, bddnode_getlow(n)); CALL(sylvan_gc_mark_rec, bddnode_gethigh(n)); SYNC(sylvan_gc_mark_rec); @@ -348,7 +286,7 @@ sylvan_ithvar(BDDVAR level) BDDVAR sylvan_var(BDD bdd) { - return bddnode_getvariable(GETNODE(bdd)); + return bddnode_getvariable(BDD_GETNODE(bdd)); } static BDD @@ -367,14 +305,14 @@ BDD sylvan_low(BDD bdd) { if (sylvan_isconst(bdd)) return bdd; - return node_low(bdd, GETNODE(bdd)); + return node_low(bdd, BDD_GETNODE(bdd)); } BDD sylvan_high(BDD bdd) { if (sylvan_isconst(bdd)) return bdd; - return node_high(bdd, GETNODE(bdd)); + return node_high(bdd, BDD_GETNODE(bdd)); } /** @@ -401,8 +339,8 @@ TASK_IMPL_3(BDD, sylvan_and, BDD, a, BDD, b, BDDVAR, prev_level) a = t; } - bddnode_t na = GETNODE(a); - bddnode_t nb = GETNODE(b); + bddnode_t na = BDD_GETNODE(a); + bddnode_t nb = BDD_GETNODE(b); BDDVAR va = bddnode_getvariable(na); BDDVAR vb = bddnode_getvariable(nb); @@ -497,8 +435,8 @@ TASK_IMPL_3(BDD, sylvan_xor, BDD, a, BDD, b, BDDVAR, prev_level) b = sylvan_not(b); } - bddnode_t na = GETNODE(a); - bddnode_t nb = GETNODE(b); + bddnode_t na = BDD_GETNODE(a); + bddnode_t nb = BDD_GETNODE(b); BDDVAR va = bddnode_getvariable(na); BDDVAR vb = bddnode_getvariable(nb); @@ -594,9 +532,9 @@ TASK_IMPL_4(BDD, sylvan_ite, BDD, a, BDD, b, BDD, c, BDDVAR, prev_level) mark = 1; } - bddnode_t na = GETNODE(a); - bddnode_t nb = GETNODE(b); - bddnode_t nc = GETNODE(c); + bddnode_t na = BDD_GETNODE(a); + bddnode_t nb = BDD_GETNODE(b); + bddnode_t nc = BDD_GETNODE(c); BDDVAR va = bddnode_getvariable(na); BDDVAR vb = bddnode_getvariable(nb); @@ -699,8 +637,8 @@ TASK_IMPL_3(BDD, sylvan_constrain, BDD, a, BDD, b, BDDVAR, prev_level) sylvan_stats_count(BDD_CONSTRAIN); // a != constant and b != constant - bddnode_t na = GETNODE(a); - bddnode_t nb = GETNODE(b); + bddnode_t na = BDD_GETNODE(a); + bddnode_t nb = BDD_GETNODE(b); BDDVAR va = bddnode_getvariable(na); BDDVAR vb = bddnode_getvariable(nb); @@ -788,8 +726,8 @@ TASK_IMPL_3(BDD, sylvan_restrict, BDD, a, BDD, b, BDDVAR, prev_level) sylvan_stats_count(BDD_RESTRICT); // a != constant and b != constant - bddnode_t na = GETNODE(a); - bddnode_t nb = GETNODE(b); + bddnode_t na = BDD_GETNODE(a); + bddnode_t nb = BDD_GETNODE(b); BDDVAR va = bddnode_getvariable(na); BDDVAR vb = bddnode_getvariable(nb); @@ -850,15 +788,15 @@ TASK_IMPL_3(BDD, sylvan_exists, BDD, a, BDD, variables, BDDVAR, prev_level) if (sylvan_set_isempty(variables)) return a; // a != constant - bddnode_t na = GETNODE(a); + bddnode_t na = BDD_GETNODE(a); BDDVAR level = bddnode_getvariable(na); - bddnode_t nv = GETNODE(variables); + bddnode_t nv = BDD_GETNODE(variables); BDDVAR vv = bddnode_getvariable(nv); while (vv < level) { variables = node_high(variables, nv); if (sylvan_set_isempty(variables)) return a; - nv = GETNODE(variables); + nv = BDD_GETNODE(variables); vv = bddnode_getvariable(nv); } @@ -956,9 +894,9 @@ TASK_IMPL_4(BDD, sylvan_and_exists, BDD, a, BDD, b, BDDSET, v, BDDVAR, prev_leve sylvan_stats_count(BDD_AND_EXISTS); // a != constant - bddnode_t na = GETNODE(a); - bddnode_t nb = GETNODE(b); - bddnode_t nv = GETNODE(v); + bddnode_t na = BDD_GETNODE(a); + bddnode_t nb = BDD_GETNODE(b); + bddnode_t nv = BDD_GETNODE(v); BDDVAR va = bddnode_getvariable(na); BDDVAR vb = bddnode_getvariable(nb); @@ -969,7 +907,7 @@ TASK_IMPL_4(BDD, sylvan_and_exists, BDD, a, BDD, b, BDDSET, v, BDDVAR, prev_leve while (vv < level) { v = node_high(v, nv); // get next variable in conjunction if (sylvan_set_isempty(v)) return sylvan_and(a, b); - nv = GETNODE(v); + nv = BDD_GETNODE(v); vv = bddnode_getvariable(nv); } @@ -1069,8 +1007,8 @@ TASK_IMPL_4(BDD, sylvan_relnext, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve sylvan_stats_count(BDD_RELNEXT); /* Determine top level */ - bddnode_t na = sylvan_isconst(a) ? 0 : GETNODE(a); - bddnode_t nb = sylvan_isconst(b) ? 0 : GETNODE(b); + bddnode_t na = sylvan_isconst(a) ? 0 : BDD_GETNODE(a); + bddnode_t nb = sylvan_isconst(b) ? 0 : BDD_GETNODE(b); BDDVAR va = na ? bddnode_getvariable(na) : 0xffffffff; BDDVAR vb = nb ? bddnode_getvariable(nb) : 0xffffffff; @@ -1082,7 +1020,7 @@ TASK_IMPL_4(BDD, sylvan_relnext, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve if (vars == sylvan_false) { is_s_or_t = 1; } else { - nv = GETNODE(vars); + nv = BDD_GETNODE(vars); for (;;) { /* check if level is s/t */ BDDVAR vv = bddnode_getvariable(nv); @@ -1094,7 +1032,7 @@ TASK_IMPL_4(BDD, sylvan_relnext, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve if (level < vv) break; vars = node_high(vars, nv); // get next in vars if (sylvan_set_isempty(vars)) return a; - nv = GETNODE(vars); + nv = BDD_GETNODE(vars); } } @@ -1131,7 +1069,7 @@ TASK_IMPL_4(BDD, sylvan_relnext, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve BDD b00, b01, b10, b11; if (!sylvan_isconst(b0)) { - bddnode_t nb0 = GETNODE(b0); + bddnode_t nb0 = BDD_GETNODE(b0); if (bddnode_getvariable(nb0) == t) { b00 = node_low(b0, nb0); b01 = node_high(b0, nb0); @@ -1142,7 +1080,7 @@ TASK_IMPL_4(BDD, sylvan_relnext, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve b00 = b01 = b0; } if (!sylvan_isconst(b1)) { - bddnode_t nb1 = GETNODE(b1); + bddnode_t nb1 = BDD_GETNODE(b1); if (bddnode_getvariable(nb1) == t) { b10 = node_low(b1, nb1); b11 = node_high(b1, nb1); @@ -1267,8 +1205,8 @@ TASK_IMPL_4(BDD, sylvan_relprev, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve sylvan_stats_count(BDD_RELPREV); /* Determine top level */ - bddnode_t na = sylvan_isconst(a) ? 0 : GETNODE(a); - bddnode_t nb = sylvan_isconst(b) ? 0 : GETNODE(b); + bddnode_t na = sylvan_isconst(a) ? 0 : BDD_GETNODE(a); + bddnode_t nb = sylvan_isconst(b) ? 0 : BDD_GETNODE(b); BDDVAR va = na ? bddnode_getvariable(na) : 0xffffffff; BDDVAR vb = nb ? bddnode_getvariable(nb) : 0xffffffff; @@ -1280,7 +1218,7 @@ TASK_IMPL_4(BDD, sylvan_relprev, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve if (vars == sylvan_false) { is_s_or_t = 1; } else { - nv = GETNODE(vars); + nv = BDD_GETNODE(vars); for (;;) { /* check if level is s/t */ BDDVAR vv = bddnode_getvariable(nv); @@ -1292,7 +1230,7 @@ TASK_IMPL_4(BDD, sylvan_relprev, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve if (level < vv) break; vars = node_high(vars, nv); // get next in vars if (sylvan_set_isempty(vars)) return b; - nv = GETNODE(vars); + nv = BDD_GETNODE(vars); } } @@ -1329,7 +1267,7 @@ TASK_IMPL_4(BDD, sylvan_relprev, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve BDD a00, a01, a10, a11; if (!sylvan_isconst(a0)) { - bddnode_t na0 = GETNODE(a0); + bddnode_t na0 = BDD_GETNODE(a0); if (bddnode_getvariable(na0) == t) { a00 = node_low(a0, na0); a01 = node_high(a0, na0); @@ -1340,7 +1278,7 @@ TASK_IMPL_4(BDD, sylvan_relprev, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve a00 = a01 = a0; } if (!sylvan_isconst(a1)) { - bddnode_t na1 = GETNODE(a1); + bddnode_t na1 = BDD_GETNODE(a1); if (bddnode_getvariable(na1) == t) { a10 = node_low(a1, na1); a11 = node_high(a1, na1); @@ -1353,7 +1291,7 @@ TASK_IMPL_4(BDD, sylvan_relprev, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve BDD b00, b01, b10, b11; if (!sylvan_isconst(b0)) { - bddnode_t nb0 = GETNODE(b0); + bddnode_t nb0 = BDD_GETNODE(b0); if (bddnode_getvariable(nb0) == t) { b00 = node_low(b0, nb0); b01 = node_high(b0, nb0); @@ -1364,7 +1302,7 @@ TASK_IMPL_4(BDD, sylvan_relprev, BDD, a, BDD, b, BDDSET, vars, BDDVAR, prev_leve b00 = b01 = b0; } if (!sylvan_isconst(b1)) { - bddnode_t nb1 = GETNODE(b1); + bddnode_t nb1 = BDD_GETNODE(b1); if (bddnode_getvariable(nb1) == t) { b10 = node_low(b1, nb1); b11 = node_high(b1, nb1); @@ -1536,7 +1474,7 @@ TASK_IMPL_2(BDD, sylvan_closure, BDD, a, BDDVAR, prev_level) sylvan_stats_count(BDD_CLOSURE); /* Determine top level */ - bddnode_t n = GETNODE(a); + bddnode_t n = BDD_GETNODE(a); BDDVAR level = bddnode_getvariable(n); /* Consult cache */ @@ -1562,7 +1500,7 @@ TASK_IMPL_2(BDD, sylvan_closure, BDD, a, BDDVAR, prev_level) BDD a00, a01, a10, a11; if (!sylvan_isconst(a0)) { - bddnode_t na0 = GETNODE(a0); + bddnode_t na0 = BDD_GETNODE(a0); if (bddnode_getvariable(na0) == t) { a00 = node_low(a0, na0); a01 = node_high(a0, na0); @@ -1573,7 +1511,7 @@ TASK_IMPL_2(BDD, sylvan_closure, BDD, a, BDDVAR, prev_level) a00 = a01 = a0; } if (!sylvan_isconst(a1)) { - bddnode_t na1 = GETNODE(a1); + bddnode_t na1 = BDD_GETNODE(a1); if (bddnode_getvariable(na1) == t) { a10 = node_low(a1, na1); a11 = node_high(a1, na1); @@ -1641,16 +1579,16 @@ TASK_IMPL_3(BDD, sylvan_compose, BDD, a, BDDMAP, map, BDDVAR, prev_level) sylvan_stats_count(BDD_COMPOSE); /* Determine top level */ - bddnode_t n = GETNODE(a); + bddnode_t n = BDD_GETNODE(a); BDDVAR level = bddnode_getvariable(n); /* Skip map */ - bddnode_t map_node = GETNODE(map); + bddnode_t map_node = BDD_GETNODE(map); BDDVAR map_var = bddnode_getvariable(map_node); while (map_var < level) { map = node_low(map, map_node); if (sylvan_map_isempty(map)) return a; - map_node = GETNODE(map); + map_node = BDD_GETNODE(map); map_var = bddnode_getvariable(map_node); } @@ -1690,7 +1628,7 @@ TASK_IMPL_3(BDD, sylvan_compose, BDD, a, BDDMAP, map, BDDVAR, prev_level) uint64_t sylvan_nodecount_do_1(BDD a) { if (sylvan_isconst(a)) return 0; - bddnode_t na = GETNODE(a); + bddnode_t na = BDD_GETNODE(a); if (bddnode_getmark(na)) return 0; bddnode_setmark(na, 1); uint64_t result = 1; @@ -1702,7 +1640,7 @@ uint64_t sylvan_nodecount_do_1(BDD a) void sylvan_nodecount_do_2(BDD a) { if (sylvan_isconst(a)) return; - bddnode_t na = GETNODE(a); + bddnode_t na = BDD_GETNODE(a); if (!bddnode_getmark(na)) return; bddnode_setmark(na, 0); sylvan_nodecount_do_2(bddnode_getlow(na)); @@ -1771,14 +1709,14 @@ TASK_IMPL_3(double, sylvan_satcount, BDD, bdd, BDDSET, variables, BDDVAR, prev_l /* Count variables before var(bdd) */ size_t skipped = 0; BDDVAR var = sylvan_var(bdd); - bddnode_t set_node = GETNODE(variables); + bddnode_t set_node = BDD_GETNODE(variables); BDDVAR set_var = bddnode_getvariable(set_node); while (var != set_var) { skipped++; variables = node_high(variables, set_node); // if this assertion fails, then variables is not the support of assert(!sylvan_set_isempty(variables)); - set_node = GETNODE(variables); + set_node = BDD_GETNODE(variables); set_var = bddnode_getvariable(set_node); } @@ -1816,11 +1754,11 @@ sylvan_sat_one(BDD bdd, BDDSET vars, uint8_t *str) if (sylvan_set_isempty(vars)) return 1; for (;;) { - bddnode_t n_vars = GETNODE(vars); + bddnode_t n_vars = BDD_GETNODE(vars); if (bdd == sylvan_true) { *str = 0; } else { - bddnode_t n_bdd = GETNODE(bdd); + bddnode_t n_bdd = BDD_GETNODE(bdd); if (bddnode_getvariable(n_bdd) != bddnode_getvariable(n_vars)) { *str = 0; } else { @@ -1849,7 +1787,7 @@ sylvan_sat_one_bdd(BDD bdd) if (bdd == sylvan_false) return sylvan_false; if (bdd == sylvan_true) return sylvan_true; - bddnode_t node = GETNODE(bdd); + bddnode_t node = BDD_GETNODE(bdd); BDD low = node_low(bdd, node); BDD high = node_high(bdd, node); @@ -1880,7 +1818,7 @@ sylvan_cube(BDDSET vars, uint8_t *cube) { if (sylvan_set_isempty(vars)) return sylvan_true; - bddnode_t n = GETNODE(vars); + bddnode_t n = BDD_GETNODE(vars); BDDVAR v = bddnode_getvariable(n); vars = node_high(vars, n); @@ -1901,7 +1839,7 @@ TASK_IMPL_3(BDD, sylvan_union_cube, BDD, bdd, BDDSET, vars, uint8_t *, cube) if (bdd == sylvan_false) return sylvan_cube(vars, cube); if (sylvan_set_isempty(vars)) return sylvan_true; - bddnode_t nv = GETNODE(vars); + bddnode_t nv = BDD_GETNODE(vars); for (;;) { if (*cube == 0 || *cube == 1) break; @@ -1909,14 +1847,14 @@ TASK_IMPL_3(BDD, sylvan_union_cube, BDD, bdd, BDDSET, vars, uint8_t *, cube) cube++; vars = node_high(vars, nv); if (sylvan_set_isempty(vars)) return sylvan_true; - nv = GETNODE(vars); + nv = BDD_GETNODE(vars); } sylvan_gc_test(); // missing: SV_CNT_OP - bddnode_t n = GETNODE(bdd); + bddnode_t n = BDD_GETNODE(bdd); BDD result = bdd; BDDVAR v = bddnode_getvariable(nv); BDDVAR n_level = bddnode_getvariable(n); @@ -2138,7 +2076,7 @@ int sylvan_set_in(BDDSET set, BDDVAR level) { while (!sylvan_set_isempty(set)) { - bddnode_t n = GETNODE(set); + bddnode_t n = BDD_GETNODE(set); BDDVAR n_level = bddnode_getvariable(n); if (n_level == level) return 1; if (n_level > level) return 0; // BDDs are ordered @@ -2161,7 +2099,7 @@ sylvan_set_toarray(BDDSET set, BDDVAR *arr) { size_t i = 0; while (!sylvan_set_isempty(set)) { - bddnode_t n = GETNODE(set); + bddnode_t n = BDD_GETNODE(set); arr[i++] = bddnode_getvariable(n); set = node_high(set, n); } @@ -2183,7 +2121,7 @@ sylvan_test_isset(BDDSET set) while (set != sylvan_false) { assert(set != sylvan_true); assert(llmsset_is_marked(nodes, set)); - bddnode_t n = GETNODE(set); + bddnode_t n = BDD_GETNODE(set); assert(node_low(set, n) == sylvan_true); set = node_high(set, n); } @@ -2198,7 +2136,7 @@ sylvan_map_add(BDDMAP map, BDDVAR key, BDD value) { if (sylvan_map_isempty(map)) return sylvan_makenode(key, sylvan_map_empty(), value); - bddnode_t n = GETNODE(map); + bddnode_t n = BDD_GETNODE(map); BDDVAR key_m = bddnode_getvariable(n); if (key_m < key) { @@ -2221,10 +2159,10 @@ sylvan_map_addall(BDDMAP map_1, BDDMAP map_2) if (sylvan_map_isempty(map_1)) return map_2; if (sylvan_map_isempty(map_2)) return map_1; - bddnode_t n_1 = GETNODE(map_1); + bddnode_t n_1 = BDD_GETNODE(map_1); BDDVAR key_1 = bddnode_getvariable(n_1); - bddnode_t n_2 = GETNODE(map_2); + bddnode_t n_2 = BDD_GETNODE(map_2); BDDVAR key_2 = bddnode_getvariable(n_2); BDDMAP result; @@ -2249,7 +2187,7 @@ sylvan_map_remove(BDDMAP map, BDDVAR key) { if (sylvan_map_isempty(map)) return map; - bddnode_t n = GETNODE(map); + bddnode_t n = BDD_GETNODE(map); BDDVAR key_m = bddnode_getvariable(n); if (key_m < key) { @@ -2269,10 +2207,10 @@ sylvan_map_removeall(BDDMAP map, BDDSET toremove) if (sylvan_map_isempty(map)) return map; if (sylvan_set_isempty(toremove)) return map; - bddnode_t n_1 = GETNODE(map); + bddnode_t n_1 = BDD_GETNODE(map); BDDVAR key_1 = bddnode_getvariable(n_1); - bddnode_t n_2 = GETNODE(toremove); + bddnode_t n_2 = BDD_GETNODE(toremove); BDDVAR key_2 = bddnode_getvariable(n_2); if (key_1 < key_2) { @@ -2290,7 +2228,7 @@ int sylvan_map_in(BDDMAP map, BDDVAR key) { while (!sylvan_map_isempty(map)) { - bddnode_t n = GETNODE(map); + bddnode_t n = BDD_GETNODE(map); BDDVAR n_level = bddnode_getvariable(n); if (n_level == key) return 1; if (n_level > key) return 0; // BDDs are ordered @@ -2312,7 +2250,7 @@ BDDMAP sylvan_set_to_map(BDDSET set, BDD value) { if (sylvan_set_isempty(set)) return sylvan_map_empty(); - bddnode_t set_n = GETNODE(set); + bddnode_t set_n = BDD_GETNODE(set); BDD sub = sylvan_set_to_map(node_high(set, set_n), value); BDD result = sylvan_makenode(sub, bddnode_getvariable(set_n), value); return result; @@ -2335,7 +2273,7 @@ TASK_IMPL_1(BDD, sylvan_support, BDD, bdd) return result; } - bddnode_t n = GETNODE(bdd); + bddnode_t n = BDD_GETNODE(bdd); BDD high, low, set; /* compute recursively */ @@ -2359,8 +2297,8 @@ sylvan_unmark_rec(bddnode_t node) { if (bddnode_getmark(node)) { bddnode_setmark(node, 0); - if (!sylvan_isconst(bddnode_getlow(node))) sylvan_unmark_rec(GETNODE(bddnode_getlow(node))); - if (!sylvan_isconst(bddnode_gethigh(node))) sylvan_unmark_rec(GETNODE(bddnode_gethigh(node))); + if (!sylvan_isconst(bddnode_getlow(node))) sylvan_unmark_rec(BDD_GETNODE(bddnode_getlow(node))); + if (!sylvan_isconst(bddnode_gethigh(node))) sylvan_unmark_rec(BDD_GETNODE(bddnode_gethigh(node))); } } @@ -2575,7 +2513,7 @@ static size_t sylvan_serialize_assign_rec(BDD bdd) { if (sylvan_isnode(bdd)) { - bddnode_t n = GETNODE(bdd); + bddnode_t n = BDD_GETNODE(bdd); struct sylvan_ser s, *ss; s.bdd = BDD_STRIPMARK(bdd); @@ -2648,7 +2586,7 @@ sylvan_serialize_totext(FILE *out) while ((s=sylvan_ser_reversed_iter_next(it))) { BDD bdd = s->bdd; - bddnode_t n = GETNODE(bdd); + bddnode_t n = BDD_GETNODE(bdd); fprintf(out, "(%zu,%u,%zu,%zu,%u),", s->assigned, bddnode_getvariable(n), (size_t)bddnode_getlow(n), @@ -2683,7 +2621,7 @@ sylvan_serialize_tofile(FILE *out) index++; assert(s->assigned == index); - bddnode_t n = GETNODE(s->bdd); + bddnode_t n = BDD_GETNODE(s->bdd); struct bddnode node; bddnode_makenode(&node, bddnode_getvariable(n), sylvan_serialize_get(bddnode_getlow(n)), sylvan_serialize_get(bddnode_gethigh(n))); @@ -2738,7 +2676,7 @@ sylvan_sha2_rec(BDD bdd, SHA256_CTX *ctx) return; } - bddnode_t node = GETNODE(bdd); + bddnode_t node = BDD_GETNODE(bdd); if (bddnode_getmark(node) == 0) { bddnode_setmark(node, 1); uint32_t level = bddnode_getvariable(node); @@ -2769,7 +2707,7 @@ sylvan_getsha(BDD bdd, char *target) SHA256_CTX ctx; SHA256_Init(&ctx); sylvan_sha2_rec(bdd, &ctx); - if (bdd != sylvan_true && bdd != sylvan_false) sylvan_unmark_rec(GETNODE(bdd)); + if (bdd != sylvan_true && bdd != sylvan_false) sylvan_unmark_rec(BDD_GETNODE(bdd)); SHA256_End(&ctx, target); } @@ -2790,7 +2728,7 @@ TASK_2(int, sylvan_test_isbdd_rec, BDD, bdd, BDDVAR, parent_var) return result; } - bddnode_t n = GETNODE(bdd); + bddnode_t n = BDD_GETNODE(bdd); BDDVAR var = bddnode_getvariable(n); if (var <= parent_var) { result = 0; @@ -2811,7 +2749,7 @@ TASK_IMPL_1(int, sylvan_test_isbdd, BDD, bdd) assert(llmsset_is_marked(nodes, BDD_STRIPMARK(bdd))); - bddnode_t n = GETNODE(bdd); + bddnode_t n = BDD_GETNODE(bdd); BDDVAR var = bddnode_getvariable(n); SPAWN(sylvan_test_isbdd_rec, node_low(bdd, n), var); int result = CALL(sylvan_test_isbdd_rec, node_high(bdd, n), var); diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_int.h b/resources/3rdparty/sylvan/src/sylvan_bdd_int.h new file mode 100644 index 000000000..1849ba707 --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_int.h @@ -0,0 +1,87 @@ +/* + * Copyright 2011-2015 Formal Methods and Tools, University of Twente + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +/** + * Internals for BDDs + */ + +#ifndef SYLVAN_BDD_INT_H +#define SYLVAN_BDD_INT_H + +/** + * Complement handling macros + */ +#define BDD_HASMARK(s) (s&sylvan_complement?1:0) +#define BDD_TOGGLEMARK(s) (s^sylvan_complement) +#define BDD_STRIPMARK(s) (s&~sylvan_complement) +#define BDD_TRANSFERMARK(from, to) (to ^ (from & sylvan_complement)) +// Equal under mark +#define BDD_EQUALM(a, b) ((((a)^(b))&(~sylvan_complement))==0) + +/** + * BDD node structure + */ +typedef struct __attribute__((packed)) bddnode { + uint64_t a, b; +} * bddnode_t; // 16 bytes + +#define BDD_GETNODE(bdd) ((bddnode_t)llmsset_index_to_ptr(nodes, bdd&0x000000ffffffffff)) + +static inline int __attribute__((unused)) +bddnode_getcomp(bddnode_t n) +{ + return n->a & 0x8000000000000000 ? 1 : 0; +} + +static inline uint64_t +bddnode_getlow(bddnode_t n) +{ + return n->b & 0x000000ffffffffff; // 40 bits +} + +static inline uint64_t +bddnode_gethigh(bddnode_t n) +{ + return n->a & 0x800000ffffffffff; // 40 bits plus high bit of first +} + +static inline uint32_t +bddnode_getvariable(bddnode_t n) +{ + return (uint32_t)(n->b >> 40); +} + +static inline int +bddnode_getmark(bddnode_t n) +{ + return n->a & 0x2000000000000000 ? 1 : 0; +} + +static inline void +bddnode_setmark(bddnode_t n, int mark) +{ + if (mark) n->a |= 0x2000000000000000; + else n->a &= 0xdfffffffffffffff; +} + +static inline void +bddnode_makenode(bddnode_t n, uint32_t var, uint64_t low, uint64_t high) +{ + n->a = high; + n->b = ((uint64_t)var)<<40 | low; +} + +#endif diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c index ff9fddc48..d2c80b8b6 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c @@ -23,7 +23,7 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr } sylvan_ref(res); - BDD res1 = sylvan_ite(sylvan_ithvar(bddnode_getvariable(GETNODE(variables))), sylvan_false, res); + BDD res1 = sylvan_ite(sylvan_ithvar(bddnode_getvariable(BDD_GETNODE(variables))), sylvan_false, res); if (res1 == sylvan_invalid) { sylvan_deref(res); return sylvan_invalid; @@ -39,10 +39,10 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr return a; } /* From now on, f and cube are non-constant. */ - bddnode_t na = GETNODE(a); + bddnode_t na = BDD_GETNODE(a); BDDVAR level = bddnode_getvariable(na); - bddnode_t nv = GETNODE(variables); + bddnode_t nv = BDD_GETNODE(variables); BDDVAR vv = bddnode_getvariable(nv); //printf("a level %i and cube level %i\n", level, vv); diff --git a/resources/3rdparty/sylvan/src/sylvan_gmp.c b/resources/3rdparty/sylvan/src/sylvan_gmp.c index 0437b1be8..5dd05f3ed 100644 --- a/resources/3rdparty/sylvan/src/sylvan_gmp.c +++ b/resources/3rdparty/sylvan/src/sylvan_gmp.c @@ -549,13 +549,13 @@ TASK_IMPL_3(MTBDD, gmp_and_exists, MTBDD, a, MTBDD, b, MTBDD, v) /* Get top variable */ int la = mtbdd_isleaf(a); int lb = mtbdd_isleaf(b); - mtbddnode_t na = la ? 0 : GETNODE(a); - mtbddnode_t nb = lb ? 0 : GETNODE(b); + mtbddnode_t na = la ? 0 : MTBDD_GETNODE(a); + mtbddnode_t nb = lb ? 0 : MTBDD_GETNODE(b); uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); uint32_t var = va < vb ? va : vb; - mtbddnode_t nv = GETNODE(v); + mtbddnode_t nv = MTBDD_GETNODE(v); uint32_t vv = mtbddnode_getvariable(nv); if (vv < var) { diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index ac5a8261f..a603e44ef 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -41,39 +41,39 @@ int mtbdd_isleaf(MTBDD bdd) { if (bdd == mtbdd_true || bdd == mtbdd_false) return 1; - return mtbddnode_isleaf(GETNODE(bdd)); + return mtbddnode_isleaf(MTBDD_GETNODE(bdd)); } // for nodes uint32_t mtbdd_getvar(MTBDD node) { - return mtbddnode_getvariable(GETNODE(node)); + return mtbddnode_getvariable(MTBDD_GETNODE(node)); } MTBDD mtbdd_getlow(MTBDD mtbdd) { - return node_getlow(mtbdd, GETNODE(mtbdd)); + return node_getlow(mtbdd, MTBDD_GETNODE(mtbdd)); } MTBDD mtbdd_gethigh(MTBDD mtbdd) { - return node_gethigh(mtbdd, GETNODE(mtbdd)); + return node_gethigh(mtbdd, MTBDD_GETNODE(mtbdd)); } // for leaves uint32_t mtbdd_gettype(MTBDD leaf) { - return mtbddnode_gettype(GETNODE(leaf)); + return mtbddnode_gettype(MTBDD_GETNODE(leaf)); } uint64_t mtbdd_getvalue(MTBDD leaf) { - return mtbddnode_getvalue(GETNODE(leaf)); + return mtbddnode_getvalue(MTBDD_GETNODE(leaf)); } // for leaf type 0 (integer) @@ -103,7 +103,7 @@ VOID_TASK_IMPL_1(mtbdd_gc_mark_rec, MDD, mtbdd) if (mtbdd == mtbdd_false) return; if (llmsset_mark(nodes, mtbdd&(~mtbdd_complement))) { - mtbddnode_t n = GETNODE(mtbdd); + mtbddnode_t n = MTBDD_GETNODE(mtbdd); if (!mtbddnode_isleaf(n)) { SPAWN(mtbdd_gc_mark_rec, mtbddnode_getlow(n)); CALL(mtbdd_gc_mark_rec, mtbddnode_gethigh(n)); @@ -536,7 +536,7 @@ MTBDD mtbdd_cube(MTBDD variables, uint8_t *cube, MTBDD terminal) { if (variables == mtbdd_true) return terminal; - mtbddnode_t n = GETNODE(variables); + mtbddnode_t n = MTBDD_GETNODE(variables); BDD result; switch (*cube) { @@ -553,7 +553,7 @@ mtbdd_cube(MTBDD variables, uint8_t *cube, MTBDD terminal) case 3: { MTBDD variables2 = node_gethigh(variables, n); - mtbddnode_t n2 = GETNODE(variables2); + mtbddnode_t n2 = MTBDD_GETNODE(variables2); uint32_t var2 = mtbddnode_getvariable(n2); result = mtbdd_cube(node_gethigh(variables2, n2), cube+2, terminal); BDD low = mtbdd_makenode(var2, result, mtbdd_false); @@ -581,10 +581,10 @@ TASK_IMPL_4(MTBDD, mtbdd_union_cube, MTBDD, mtbdd, MTBDD, vars, uint8_t*, cube, sylvan_gc_test(); - mtbddnode_t nv = GETNODE(vars); + mtbddnode_t nv = MTBDD_GETNODE(vars); uint32_t v = mtbddnode_getvariable(nv); - mtbddnode_t na = GETNODE(mtbdd); + mtbddnode_t na = MTBDD_GETNODE(mtbdd); uint32_t va = mtbddnode_getvariable(na); if (va < v) { @@ -682,14 +682,14 @@ TASK_IMPL_3(MTBDD, mtbdd_apply, MTBDD, a, MTBDD, b, mtbdd_apply_op, op) mtbddnode_t na, nb; uint32_t va, vb; if (!la) { - na = GETNODE(a); + na = MTBDD_GETNODE(a); va = mtbddnode_getvariable(na); } else { na = 0; va = 0xffffffff; } if (!lb) { - nb = GETNODE(b); + nb = MTBDD_GETNODE(b); vb = mtbddnode_getvariable(nb); } else { nb = 0; @@ -747,14 +747,14 @@ TASK_IMPL_5(MTBDD, mtbdd_applyp, MTBDD, a, MTBDD, b, size_t, p, mtbdd_applyp_op, mtbddnode_t na, nb; uint32_t va, vb; if (!la) { - na = GETNODE(a); + na = MTBDD_GETNODE(a); va = mtbddnode_getvariable(na); } else { na = 0; va = 0xffffffff; } if (!lb) { - nb = GETNODE(b); + nb = MTBDD_GETNODE(b); vb = mtbddnode_getvariable(nb); } else { nb = 0; @@ -812,7 +812,7 @@ TASK_IMPL_3(MTBDD, mtbdd_uapply, MTBDD, dd, mtbdd_uapply_op, op, size_t, param) } /* Get cofactors */ - mtbddnode_t ndd = GETNODE(dd); + mtbddnode_t ndd = MTBDD_GETNODE(dd); MTBDD ddlow = node_getlow(dd, ndd); MTBDD ddhigh = node_gethigh(dd, ndd); @@ -834,7 +834,7 @@ TASK_2(MTBDD, mtbdd_uop_times_uint, MTBDD, a, size_t, k) if (a == mtbdd_true) return mtbdd_true; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { if (mtbddnode_gettype(na) == 0) { @@ -866,7 +866,7 @@ TASK_2(MTBDD, mtbdd_uop_pow_uint, MTBDD, a, size_t, k) if (a == mtbdd_true) return mtbdd_true; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { if (mtbddnode_gettype(na) == 0) { @@ -933,14 +933,14 @@ TASK_IMPL_3(MTBDD, mtbdd_abstract, MTBDD, a, MTBDD, v, mtbdd_abstract_op, op) sylvan_gc_test(); /* a != constant, v != constant */ - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { /* Count number of variables */ uint64_t k = 0; while (v != mtbdd_true) { k++; - v = node_gethigh(v, GETNODE(v)); + v = node_gethigh(v, MTBDD_GETNODE(v)); } /* Check cache */ @@ -956,7 +956,7 @@ TASK_IMPL_3(MTBDD, mtbdd_abstract, MTBDD, a, MTBDD, v, mtbdd_abstract_op, op) } /* Possibly skip k variables */ - mtbddnode_t nv = GETNODE(v); + mtbddnode_t nv = MTBDD_GETNODE(v); uint32_t var_a = mtbddnode_getvariable(na); uint32_t var_v = mtbddnode_getvariable(nv); uint64_t k = 0; @@ -964,7 +964,7 @@ TASK_IMPL_3(MTBDD, mtbdd_abstract, MTBDD, a, MTBDD, v, mtbdd_abstract_op, op) k++; v = node_gethigh(v, nv); if (v == mtbdd_true) break; - nv = GETNODE(v); + nv = MTBDD_GETNODE(v); var_v = mtbddnode_getvariable(nv); } @@ -1015,8 +1015,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_plus, MTBDD*, pa, MTBDD*, pb) if (a == mtbdd_true) return mtbdd_true; if (b == mtbdd_true) return mtbdd_true; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -1070,8 +1070,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_minus, MTBDD*, pa, MTBDD*, pb) if (a == mtbdd_false) return mtbdd_negate(b); if (b == mtbdd_false) return a; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -1123,8 +1123,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb) if (a == mtbdd_true) return b; if (b == mtbdd_true) return a; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -1179,11 +1179,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_min, MTBDD*, pa, MTBDD*, pb) if (a == b) return a; // Special case where "false" indicates a partial function - if (a == mtbdd_false && b != mtbdd_false && mtbddnode_isleaf(GETNODE(b))) return b; - if (b == mtbdd_false && a != mtbdd_false && mtbddnode_isleaf(GETNODE(a))) return a; + if (a == mtbdd_false && b != mtbdd_false && mtbddnode_isleaf(MTBDD_GETNODE(b))) return b; + if (b == mtbdd_false && a != mtbdd_false && mtbddnode_isleaf(MTBDD_GETNODE(a))) return a; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -1241,8 +1241,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, MTBDD*, pa, MTBDD*, pb) if (b == mtbdd_false) return a; if (a == b) return a; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -1291,7 +1291,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_negate, MTBDD, a, size_t, k) if (a == mtbdd_false) return mtbdd_false; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { if (mtbddnode_gettype(na) == 0) { @@ -1340,9 +1340,9 @@ TASK_IMPL_3(MTBDD, mtbdd_ite, MTBDD, f, MTBDD, g, MTBDD, h) /* Get top variable */ int lg = mtbdd_isleaf(g); int lh = mtbdd_isleaf(h); - mtbddnode_t nf = GETNODE(f); - mtbddnode_t ng = lg ? 0 : GETNODE(g); - mtbddnode_t nh = lh ? 0 : GETNODE(h); + mtbddnode_t nf = MTBDD_GETNODE(f); + mtbddnode_t ng = lg ? 0 : MTBDD_GETNODE(g); + mtbddnode_t nh = lh ? 0 : MTBDD_GETNODE(h); uint32_t vf = mtbddnode_getvariable(nf); uint32_t vg = lg ? 0 : mtbddnode_getvariable(ng); uint32_t vh = lh ? 0 : mtbddnode_getvariable(nh); @@ -1381,7 +1381,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, a, size_t, svalue) if (a == mtbdd_true) return mtbdd_invalid; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { double value = *(double*)&svalue; @@ -1412,7 +1412,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue) if (a == mtbdd_true) return mtbdd_invalid; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { double value = *(double*)&svalue; @@ -1456,8 +1456,8 @@ TASK_4(MTBDD, mtbdd_equal_norm_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, sho if (a == mtbdd_false) return mtbdd_false; if (b == mtbdd_false) return mtbdd_false; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); int la = mtbddnode_isleaf(na); int lb = mtbddnode_isleaf(nb); @@ -1528,8 +1528,8 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, if (a == mtbdd_false) return mtbdd_false; if (b == mtbdd_false) return mtbdd_false; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); int la = mtbddnode_isleaf(na); int lb = mtbddnode_isleaf(nb); @@ -1604,8 +1604,8 @@ TASK_3(MTBDD, mtbdd_leq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) MTBDD result; if (cache_get3(CACHE_MTBDD_LEQ, a, b, 0, &result)) return result; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); int la = mtbddnode_isleaf(na); int lb = mtbddnode_isleaf(nb); @@ -1694,8 +1694,8 @@ TASK_3(MTBDD, mtbdd_less_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) MTBDD result; if (cache_get3(CACHE_MTBDD_LESS, a, b, 0, &result)) return result; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); int la = mtbddnode_isleaf(na); int lb = mtbddnode_isleaf(nb); @@ -1784,8 +1784,8 @@ TASK_3(MTBDD, mtbdd_geq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) MTBDD result; if (cache_get3(CACHE_MTBDD_GEQ, a, b, 0, &result)) return result; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); int la = mtbddnode_isleaf(na); int lb = mtbddnode_isleaf(nb); @@ -1874,8 +1874,8 @@ TASK_3(MTBDD, mtbdd_greater_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) MTBDD result; if (cache_get3(CACHE_MTBDD_GREATER, a, b, 0, &result)) return result; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); int la = mtbddnode_isleaf(na); int lb = mtbddnode_isleaf(nb); @@ -1968,13 +1968,13 @@ TASK_IMPL_3(MTBDD, mtbdd_and_exists, MTBDD, a, MTBDD, b, MTBDD, v) /* Get top variable */ int la = mtbdd_isleaf(a); int lb = mtbdd_isleaf(b); - mtbddnode_t na = la ? 0 : GETNODE(a); - mtbddnode_t nb = lb ? 0 : GETNODE(b); + mtbddnode_t na = la ? 0 : MTBDD_GETNODE(a); + mtbddnode_t nb = lb ? 0 : MTBDD_GETNODE(b); uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); uint32_t var = va < vb ? va : vb; - mtbddnode_t nv = GETNODE(v); + mtbddnode_t nv = MTBDD_GETNODE(v); uint32_t vv = mtbddnode_getvariable(nv); if (vv < var) { @@ -2029,7 +2029,7 @@ TASK_IMPL_1(MTBDD, mtbdd_support, MTBDD, dd) if (cache_get3(CACHE_MTBDD_SUPPORT, dd, 0, 0, &result)) return result; /* Recursive calls */ - mtbddnode_t n = GETNODE(dd); + mtbddnode_t n = MTBDD_GETNODE(dd); mtbdd_refs_spawn(SPAWN(mtbdd_support, node_getlow(dd, n))); MTBDD high = mtbdd_refs_push(CALL(mtbdd_support, node_gethigh(dd, n))); MTBDD low = mtbdd_refs_push(mtbdd_refs_sync(SYNC(mtbdd_support))); @@ -2054,7 +2054,7 @@ TASK_IMPL_2(MTBDD, mtbdd_compose, MTBDD, a, MTBDDMAP, map) if (mtbdd_isleaf(a) || mtbdd_map_isempty(map)) return a; /* Determine top level */ - mtbddnode_t n = GETNODE(a); + mtbddnode_t n = MTBDD_GETNODE(a); uint32_t v = mtbddnode_getvariable(n); /* Find in map */ @@ -2093,7 +2093,7 @@ TASK_IMPL_1(MTBDD, mtbdd_minimum, MTBDD, a) { /* Check terminal case */ if (a == mtbdd_false) return mtbdd_false; - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) return a; /* Maybe perform garbage collection */ @@ -2109,8 +2109,8 @@ TASK_IMPL_1(MTBDD, mtbdd_minimum, MTBDD, a) MTBDD low = SYNC(mtbdd_minimum); /* Determine lowest */ - mtbddnode_t nl = GETNODE(low); - mtbddnode_t nh = GETNODE(high); + mtbddnode_t nl = MTBDD_GETNODE(low); + mtbddnode_t nh = MTBDD_GETNODE(high); if (mtbddnode_gettype(nl) == 0 && mtbddnode_gettype(nh) == 0) { result = mtbdd_getint64(low) < mtbdd_getint64(high) ? low : high; @@ -2146,7 +2146,7 @@ TASK_IMPL_1(MTBDD, mtbdd_maximum, MTBDD, a) { /* Check terminal case */ if (a == mtbdd_false) return mtbdd_false; - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) return a; /* Maybe perform garbage collection */ @@ -2162,8 +2162,8 @@ TASK_IMPL_1(MTBDD, mtbdd_maximum, MTBDD, a) MTBDD low = SYNC(mtbdd_maximum); /* Determine highest */ - mtbddnode_t nl = GETNODE(low); - mtbddnode_t nh = GETNODE(high); + mtbddnode_t nl = MTBDD_GETNODE(low); + mtbddnode_t nh = MTBDD_GETNODE(high); if (mtbddnode_gettype(nl) == 0 && mtbddnode_gettype(nh) == 0) { result = mtbdd_getint64(low) > mtbdd_getint64(high) ? low : high; @@ -2248,7 +2248,7 @@ mtbdd_enum_first(MTBDD dd, MTBDD variables, uint8_t *arr, mtbdd_enum_filter_cb f variables = mtbdd_gethigh(variables); // check if MTBDD is on this variable - mtbddnode_t n = GETNODE(dd); + mtbddnode_t n = MTBDD_GETNODE(dd); if (mtbddnode_getvariable(n) != v) { *arr = 2; return mtbdd_enum_first(dd, variables, arr+1, filter_cb); @@ -2288,7 +2288,7 @@ mtbdd_enum_next(MTBDD dd, MTBDD variables, uint8_t *arr, mtbdd_enum_filter_cb fi if (*arr == 0) { // previous was low - mtbddnode_t n = GETNODE(dd); + mtbddnode_t n = MTBDD_GETNODE(dd); MTBDD res = mtbdd_enum_next(node_getlow(dd, n), variables, arr+1, filter_cb); if (res != mtbdd_false) { return res; @@ -2304,7 +2304,7 @@ mtbdd_enum_next(MTBDD dd, MTBDD variables, uint8_t *arr, mtbdd_enum_filter_cb fi } } else if (*arr == 1) { // previous was high - mtbddnode_t n = GETNODE(dd); + mtbddnode_t n = MTBDD_GETNODE(dd); return mtbdd_enum_next(node_gethigh(dd, n), variables, arr+1, filter_cb); } else { // previous was either @@ -2319,7 +2319,7 @@ mtbdd_enum_next(MTBDD dd, MTBDD variables, uint8_t *arr, mtbdd_enum_filter_cb fi static void mtbdd_unmark_rec(MTBDD mtbdd) { - mtbddnode_t n = GETNODE(mtbdd); + mtbddnode_t n = MTBDD_GETNODE(mtbdd); if (!mtbddnode_getmark(n)) return; mtbddnode_setmark(n, 0); if (mtbddnode_isleaf(n)) return; @@ -2340,7 +2340,7 @@ mtbdd_leafcount_mark(MTBDD mtbdd) if (mtbdd == mtbdd_false) { // do not count true/false leaf return 0; } - mtbddnode_t n = GETNODE(mtbdd); + mtbddnode_t n = MTBDD_GETNODE(mtbdd); if (mtbddnode_getmark(n)) { return 0; } @@ -2368,7 +2368,7 @@ mtbdd_nodecount_mark(MTBDD mtbdd) { if (mtbdd == mtbdd_true) return 0; // do not count true/false leaf if (mtbdd == mtbdd_false) return 0; // do not count true/false leaf - mtbddnode_t n = GETNODE(mtbdd); + mtbddnode_t n = MTBDD_GETNODE(mtbdd); if (mtbddnode_getmark(n)) return 0; mtbddnode_setmark(n, 1); if (mtbddnode_isleaf(n)) return 1; // count leaf as 1 @@ -2399,7 +2399,7 @@ TASK_2(int, mtbdd_test_isvalid_rec, MTBDD, dd, uint32_t, parent_var) if (marked == 0) return 0; // check if leaf - mtbddnode_t n = GETNODE(dd); + mtbddnode_t n = MTBDD_GETNODE(dd); if (mtbddnode_isleaf(n)) return 1; // we're fine // check variable order @@ -2439,7 +2439,7 @@ TASK_IMPL_1(int, mtbdd_test_isvalid, MTBDD, dd) if (marked == 0) return 0; // check if leaf - mtbddnode_t n = GETNODE(dd); + mtbddnode_t n = MTBDD_GETNODE(dd); if (mtbddnode_isleaf(n)) return 1; // we're fine // check recursively @@ -2457,7 +2457,7 @@ TASK_IMPL_1(int, mtbdd_test_isvalid, MTBDD, dd) static void mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb) { - mtbddnode_t n = GETNODE(mtbdd); // also works for mtbdd_false + mtbddnode_t n = MTBDD_GETNODE(mtbdd); // also works for mtbdd_false if (mtbddnode_getmark(n)) return; mtbddnode_setmark(n, 1); @@ -2527,7 +2527,7 @@ int mtbdd_map_contains(MTBDDMAP map, uint32_t key) { while (!mtbdd_map_isempty(map)) { - mtbddnode_t n = GETNODE(map); + mtbddnode_t n = MTBDD_GETNODE(map); uint32_t k = mtbddnode_getvariable(n); if (k == key) return 1; if (k > key) return 0; @@ -2561,7 +2561,7 @@ mtbdd_map_add(MTBDDMAP map, uint32_t key, MTBDD value) { if (mtbdd_map_isempty(map)) return mtbdd_makenode(key, mtbdd_map_empty(), value); - mtbddnode_t n = GETNODE(map); + mtbddnode_t n = MTBDD_GETNODE(map); uint32_t k = mtbddnode_getvariable(n); if (k < key) { @@ -2585,8 +2585,8 @@ mtbdd_map_addall(MTBDDMAP map1, MTBDDMAP map2) if (mtbdd_map_isempty(map1)) return map2; if (mtbdd_map_isempty(map2)) return map1; - mtbddnode_t n1 = GETNODE(map1); - mtbddnode_t n2 = GETNODE(map2); + mtbddnode_t n1 = MTBDD_GETNODE(map1); + mtbddnode_t n2 = MTBDD_GETNODE(map2); uint32_t k1 = mtbddnode_getvariable(n1); uint32_t k2 = mtbddnode_getvariable(n2); @@ -2613,7 +2613,7 @@ mtbdd_map_remove(MTBDDMAP map, uint32_t key) { if (mtbdd_map_isempty(map)) return map; - mtbddnode_t n = GETNODE(map); + mtbddnode_t n = MTBDD_GETNODE(map); uint32_t k = mtbddnode_getvariable(n); if (k < key) { @@ -2635,8 +2635,8 @@ mtbdd_map_removeall(MTBDDMAP map, MTBDD variables) if (mtbdd_map_isempty(map)) return map; if (variables == mtbdd_true) return map; - mtbddnode_t n1 = GETNODE(map); - mtbddnode_t n2 = GETNODE(variables); + mtbddnode_t n1 = MTBDD_GETNODE(map); + mtbddnode_t n2 = MTBDD_GETNODE(variables); uint32_t k1 = mtbddnode_getvariable(n1); uint32_t k2 = mtbddnode_getvariable(n2); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_int.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_int.h index 940250b9a..aff9821bb 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_int.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_int.h @@ -28,7 +28,7 @@ typedef struct __attribute__((packed)) mtbddnode { uint64_t a, b; } * mtbddnode_t; // 16 bytes -#define GETNODE(mtbdd) ((mtbddnode_t)llmsset_index_to_ptr(nodes, mtbdd&0x000000ffffffffff)) +#define MTBDD_GETNODE(mtbdd) ((mtbddnode_t)llmsset_index_to_ptr(nodes, mtbdd&0x000000ffffffffff)) /** * Complement handling macros diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 87e9bb590..7d05d86a1 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -1,3 +1,5 @@ +#include + /** * Generate SHA2 structural hashes. * Hashes are independent of location. @@ -11,7 +13,7 @@ mtbdd_sha2_rec(MTBDD mtbdd, SHA256_CTX *ctx) return; } - mtbddnode_t node = GETNODE(mtbdd); + mtbddnode_t node = MTBDD_GETNODE(mtbdd); if (mtbddnode_isleaf(node)) { uint64_t val = mtbddnode_getvalue(node); SHA256_Update(ctx, (void*)&val, sizeof(uint64_t)); @@ -48,8 +50,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) // Do not handle Boolean MTBDDs... - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -120,8 +122,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb) if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true; if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -174,8 +176,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb) if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true; if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -222,8 +224,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true; if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -269,8 +271,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_pow, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -306,8 +308,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_mod, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -343,8 +345,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_logxy, MTBDD*, pa, MTBDD*, pb) { MTBDD a = *pa, b = *pb; - mtbddnode_t na = GETNODE(a); - mtbddnode_t nb = GETNODE(b); + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) { uint64_t val_a = mtbddnode_getvalue(na); @@ -377,7 +379,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v) if (a == mtbdd_true) return mtbdd_true; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { if (mtbddnode_gettype(na) == 0) { @@ -412,7 +414,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v) if (a == mtbdd_true) return mtbdd_true; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { if (mtbddnode_gettype(na) == 0) { @@ -450,7 +452,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v) if (a == mtbdd_true) return mtbdd_true; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { if (mtbddnode_gettype(na) == 0) { @@ -523,7 +525,7 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars) /* Trivial cases */ if (dd == mtbdd_false) return 0.0; - mtbddnode_t na = GETNODE(dd); + mtbddnode_t na = MTBDD_GETNODE(dd); if (mtbdd_isleaf(dd)) { if (mtbddnode_gettype(na) == 0) { @@ -593,7 +595,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_complement, MTBDD, a, size_t, k) if (a == mtbdd_false) return mtbdd_false; // a != constant - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); if (mtbddnode_isleaf(na)) { if (mtbddnode_gettype(na) == 0) { @@ -626,42 +628,42 @@ TASK_IMPL_2(MTBDD, mtbdd_op_complement, MTBDD, a, size_t, k) (void)k; // unused variable } -TASK_IMPL_3(MTBDD, mtbdd_minExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { - MTBDD zero = mtbdd_false; +TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR, prev_level) { + BDD zero = sylvan_false; /* Maybe perform garbage collection */ sylvan_gc_test(); /* Cube is guaranteed to be a cube at this point. */ if (mtbdd_isleaf(a)) { - if (mtbdd_set_isempty(variables)) { - return a; // FIXME? + if (sylvan_set_isempty(variables)) { + return sylvan_true; // FIXME? } else { return variables; } } - mtbddnode_t na = GETNODE(a); + mtbddnode_t na = MTBDD_GETNODE(a); uint32_t va = mtbddnode_getvariable(na); - mtbddnode_t nv = GETNODE(variables); - uint32_t vv = mtbddnode_getvariable(nv); + bddnode_t nv = BDD_GETNODE(variables); + BDDVAR vv = bddnode_getvariable(nv); /* Abstract a variable that does not appear in a. */ if (va > vv) { - MTBDD _v = mtbdd_set_next(variables); - MTBDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va); - if (res == mtbdd_invalid) { - return mtbdd_invalid; + BDD _v = sylvan_set_next(variables); + BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va); + if (res == sylvan_invalid) { + return sylvan_invalid; } // Fill in the missing variables to make representative unique. - mtbdd_ref(res); - MTBDD res1 = mtbdd_ite(mtbdd_ithvar(vv), zero, res); - if (res1 == mtbdd_invalid) { - mtbdd_deref(res); - return mtbdd_invalid; + sylvan_ref(res); + BDD res1 = sylvan_ite(sylvan_ithvar(vv), zero, res); + if (res1 == sylvan_invalid) { + sylvan_deref(res); + return sylvan_invalid; } - mtbdd_deref(res); + sylvan_deref(res); return res1; } @@ -676,120 +678,120 @@ TASK_IMPL_3(MTBDD, mtbdd_minExistsRepresentative, MTBDD, a, MTBDD, variables, ui /* If the two indices are the same, so are their levels. */ if (va == vv) { - MTBDD _v = mtbdd_set_next(variables); - MTBDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va); - if (res1 == mtbdd_invalid) { - return mtbdd_invalid; + BDD _v = sylvan_set_next(variables); + BDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va); + if (res1 == sylvan_invalid) { + return sylvan_invalid; } - mtbdd_ref(res1); + sylvan_ref(res1); - MTBDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va); - if (res2 == mtbdd_invalid) { - mtbdd_deref(res1); - return mtbdd_invalid; + BDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va); + if (res2 == sylvan_invalid) { + sylvan_deref(res1); + return sylvan_invalid; } - mtbdd_ref(res2); + sylvan_ref(res2); MTBDD left = mtbdd_abstract_min(E, _v); if (left == mtbdd_invalid) { - mtbdd_deref(res1); - mtbdd_deref(res2); - return mtbdd_invalid; + sylvan_deref(res1); + sylvan_deref(res2); + return sylvan_invalid; } mtbdd_ref(left); MTBDD right = mtbdd_abstract_min(T, _v); if (right == mtbdd_invalid) { - mtbdd_deref(res1); - mtbdd_deref(res2); + sylvan_deref(res1); + sylvan_deref(res2); mtbdd_deref(left); - return mtbdd_invalid; + return sylvan_invalid; } mtbdd_ref(right); - MTBDD tmp = mtbdd_less_or_equal_as_bdd(left, right); - if (tmp == mtbdd_invalid) { - mtbdd_deref(res1); - mtbdd_deref(res2); + BDD tmp = mtbdd_less_or_equal_as_bdd(left, right); + if (tmp == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); mtbdd_deref(left); mtbdd_deref(right); - return mtbdd_invalid; + return sylvan_invalid; } - mtbdd_ref(tmp); + sylvan_ref(tmp); mtbdd_deref(left); mtbdd_deref(right); - MTBDD res1Inf = mtbdd_ite(tmp, res1, zero); - if (res1Inf == mtbdd_invalid) { - mtbdd_deref(res1); - mtbdd_deref(res2); - mtbdd_deref(tmp); - return mtbdd_invalid; + BDD res1Inf = sylvan_ite(tmp, res1, zero); + if (res1Inf == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + sylvan_deref(tmp); + return sylvan_invalid; } - mtbdd_ref(res1Inf); - mtbdd_deref(res1); + sylvan_ref(res1Inf); + sylvan_deref(res1); - MTBDD tmp2 = mtbdd_get_complement(tmp); - if (tmp2 == mtbdd_invalid) { - mtbdd_deref(res2); + BDD tmp2 = sylvan_not(tmp); + if (tmp2 == sylvan_invalid) { + sylvan_deref(res2); mtbdd_deref(left); mtbdd_deref(right); - mtbdd_deref(tmp); - return mtbdd_invalid; + sylvan_deref(tmp); + return sylvan_invalid; } - mtbdd_ref(tmp2); - mtbdd_deref(tmp); + sylvan_ref(tmp2); + sylvan_deref(tmp); - MTBDD res2Inf = mtbdd_ite(tmp2, res2, zero); - if (res2Inf == mtbdd_invalid) { - mtbdd_deref(res2); - mtbdd_deref(res1Inf); - mtbdd_deref(tmp2); - return mtbdd_invalid; + BDD res2Inf = sylvan_ite(tmp2, res2, zero); + if (res2Inf == sylvan_invalid) { + sylvan_deref(res2); + sylvan_deref(res1Inf); + sylvan_deref(tmp2); + return sylvan_invalid; } - mtbdd_ref(res2Inf); - mtbdd_deref(res2); - mtbdd_deref(tmp2); + sylvan_ref(res2Inf); + sylvan_deref(res2); + sylvan_deref(tmp2); - MTBDD res = (res1Inf == res2Inf) ? mtbdd_ite(mtbdd_ithvar(va), zero, res1Inf) : mtbdd_ite(mtbdd_ithvar(va), res2Inf, res1Inf); + BDD res = (res1Inf == res2Inf) ? sylvan_ite(sylvan_ithvar(va), zero, res1Inf) : sylvan_ite(sylvan_ithvar(va), res2Inf, res1Inf); - if (res == mtbdd_invalid) { - mtbdd_deref(res1Inf); - mtbdd_deref(res2Inf); - return mtbdd_invalid; + if (res == sylvan_invalid) { + sylvan_deref(res1Inf); + sylvan_deref(res2Inf); + return sylvan_invalid; } - mtbdd_ref(res); - mtbdd_deref(res1Inf); - mtbdd_deref(res2Inf); + sylvan_ref(res); + sylvan_deref(res1Inf); + sylvan_deref(res2Inf); /* TODO: Caching here. */ //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); - mtbdd_deref(res); + sylvan_deref(res); return res; } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ - MTBDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va); - if (res1 == mtbdd_invalid) { - return mtbdd_invalid; + BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va); + if (res1 == sylvan_invalid) { + return sylvan_invalid; } - mtbdd_ref(res1); - MTBDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va); - if (res2 == mtbdd_invalid) { - mtbdd_deref(res1); - return mtbdd_invalid; + sylvan_ref(res1); + BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va); + if (res2 == sylvan_invalid) { + sylvan_deref(res1); + return sylvan_invalid; } - mtbdd_ref(res2); + sylvan_ref(res2); - MTBDD res = (res1 == res2) ? mtbdd_ite(mtbdd_ithvar(va), zero, res1) : mtbdd_ite(mtbdd_ithvar(va), res2, res1); - if (res == mtbdd_invalid) { - mtbdd_deref(res1); - mtbdd_deref(res2); - return mtbdd_invalid; + BDD res = (res1 == res2) ? sylvan_ite(sylvan_ithvar(va), zero, res1) : sylvan_ite(sylvan_ithvar(va), res2, res1); + if (res == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + return sylvan_invalid; } - mtbdd_deref(res1); - mtbdd_deref(res2); + sylvan_deref(res1); + sylvan_deref(res2); /* TODO: Caching here. */ //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); return res; @@ -799,7 +801,7 @@ TASK_IMPL_3(MTBDD, mtbdd_minExistsRepresentative, MTBDD, a, MTBDD, variables, ui (void)prev_level; } -TASK_IMPL_3(MTBDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { +TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { (void)variables; (void)prev_level; return a; diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index d1119438b..0115225e6 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -110,6 +110,7 @@ int mtbdd_isnonzero(MTBDD); #define mtbdd_regular(dd) (dd & ~mtbdd_complement) +#define GETNODE_BDD(bdd) ((bddnode_t)llmsset_index_to_ptr(nodes, bdd&0x000000ffffffffff)) #define mtbdd_set_next(set) (mtbdd_gethigh(set)) #define mtbdd_set_isempty(set) (set == mtbdd_true) @@ -130,12 +131,12 @@ TASK_DECL_2(MTBDD, mtbdd_op_complement, MTBDD, size_t); /** * Just like mtbdd_abstract_min, but instead of abstracting the variables in the given cube, picks a unique representative that realizes the minimal function value. */ -TASK_DECL_3(MTBDD, mtbdd_minExistsRepresentative, MTBDD, MTBDD, uint32_t); +TASK_DECL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, MTBDD, uint32_t); #define mtbdd_minExistsRepresentative(a, vars) (CALL(mtbdd_minExistsRepresentative, a, vars, 0)) /** * Just like mtbdd_abstract_max but instead of abstracting the variables in the given cube, picks a unique representative that realizes the maximal function value. */ -TASK_DECL_3(MTBDD, mtbdd_maxExistsRepresentative, MTBDD, MTBDD, uint32_t); +TASK_DECL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, MTBDD, uint32_t); #define mtbdd_maxExistsRepresentative(a, vars) (CALL(mtbdd_maxExistsRepresentative, a, vars, 0)) diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 87ab6735e..d71aaa232 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -35,12 +35,12 @@ /** * @brief Computes abstraction by minimum */ - Mtbdd AbstractMinRepresentative(const BddSet &variables) const; + Bdd AbstractMinRepresentative(const BddSet &variables) const; /** * @brief Computes abstraction by maximum */ - Mtbdd AbstractMaxRepresentative(const BddSet &variables) const; + Bdd AbstractMaxRepresentative(const BddSet &variables) const; Bdd NotZero() const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 7ef934fbe..570f29626 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -188,14 +188,14 @@ Mtbdd::GetShaHash() const { return std::string(buf); } -Mtbdd +Bdd Mtbdd::AbstractMinRepresentative(const BddSet &variables) const { LACE_ME; return mtbdd_minExistsRepresentative(mtbdd, variables.set.bdd); } -Mtbdd +Bdd Mtbdd::AbstractMaxRepresentative(const BddSet &variables) const { LACE_ME; diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index dd2afab1a..e9334d6ff 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -377,6 +377,23 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p) (void)p; } +/** + * Operation "replace leaves" for one storm::RationalFunction MTBDD + */ +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_replace_leaves, MTBDD, dd, void*, context) +{ + LOG_I("task_impl_2 op_replace") + /* Handle partial functions */ + if (dd == mtbdd_false) return mtbdd_false; + + /* Compute result for leaf */ + if (mtbdd_isleaf(dd)) { + return storm_rational_function_leaf_parameter_replacement(mtbdd_getvalue(dd), mtbdd_gettype(dd), context); + } + + return mtbdd_invalid; +} + /** * Multiply and , and abstract variables using summation. * This is similar to the "and_exists" operation in BDDs. @@ -411,13 +428,13 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b /* Get top variable */ int la = mtbdd_isleaf(a); int lb = mtbdd_isleaf(b); - mtbddnode_t na = la ? 0 : GETNODE(a); - mtbddnode_t nb = lb ? 0 : GETNODE(b); + mtbddnode_t na = la ? 0 : MTBDD_GETNODE(a); + mtbddnode_t nb = lb ? 0 : MTBDD_GETNODE(b); uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); uint32_t var = va < vb ? va : vb; - mtbddnode_t nv = GETNODE(v); + mtbddnode_t nv = MTBDD_GETNODE(v); uint32_t vv = mtbddnode_getvariable(nv); if (vv < var) { diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index 98a2fdffd..b64761955 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -90,7 +90,7 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t) /** * Compute -a */ -#define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0); +#define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0) /** * Multiply and , and abstract variables using summation. @@ -104,6 +104,25 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBD */ #define sylvan_storm_rational_function_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_plus)) +/** + * Functionality regarding the replacement of leaves in MTBDDs. + * + * uint64_t mtbdd_getvalue + * uint32_t mtbdd_gettype + * void* custom context ptr + */ +typedef MTBDD (*mtbddLeaveReplacementFunction)(uint64_t, uint32_t, void*); + +/** + * Operation "replace" for one storm::RationalFunction MTBDD + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_replace_leaves, MTBDD, void*) + +/** + * Compute the MTBDD that arises from a after calling the mtbddLeaveReplacementFunction on each leaf. + */ +#define sylvan_storm_rational_function_replace_leaves(a, func, ctx) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_replace_leaves), ctx) + #ifdef __cplusplus } #endif /* __cplusplus */ diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 0c65233b1..9cd62b49b 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -164,12 +164,24 @@ namespace storm { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); return Add(this->getDdManager(), internalAdd.minAbstract(cube), Dd::subtractMetaVariables(*this, cube)); } + + template + Bdd Add::minAbstractRepresentative(std::set const& metaVariables) const { + Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); + return Bdd(this->getDdManager(), internalAdd.minAbstractRepresentative(cube), this->getContainedMetaVariables()); + } template Add Add::maxAbstract(std::set const& metaVariables) const { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); return Add(this->getDdManager(), internalAdd.maxAbstract(cube), Dd::subtractMetaVariables(*this, cube)); } + + template + Bdd Add::maxAbstractRepresentative(std::set const& metaVariables) const { + Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); + return Bdd(this->getDdManager(), internalAdd.maxAbstractRepresentative(cube), this->getContainedMetaVariables()); + } template bool Add::equalModuloPrecision(Add const& other, double precision, bool relative) const { diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index 67747e0e4..e1482f50f 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -257,12 +257,30 @@ namespace storm { */ Add minAbstract(std::set const& metaVariables) const; + /*! + * Similar to minAbstract, but does not abstract from the variables but rather picks a + * valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a + * valuation (of the other variables) that make the function evaluate to the minimal value. + * + * @param metaVariables The meta variables from which to abstract. + */ + Bdd minAbstractRepresentative(std::set const& metaVariables) const; + /*! * Max-abstracts from the given meta variables. * * @param metaVariables The meta variables from which to abstract. */ Add maxAbstract(std::set const& metaVariables) const; + + /*! + * Similar to maxAbstract, but does not abstract from the variables but rather picks a + * valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a + * valuation (of the other variables) that make the function evaluate to the maximal value. + * + * @param metaVariables The meta variables from which to abstract. + */ + Bdd maxAbstractRepresentative(std::set const& metaVariables) const; /*! * Checks whether the current and the given ADD represent the same function modulo some given precision. diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index d23a2c0e3..6d63c49f3 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -9,6 +9,7 @@ #include "src/utility/constants.h" #include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" namespace storm { namespace dd { @@ -145,11 +146,23 @@ namespace storm { InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->getCuddAdd().MinAbstract(cube.toAdd().getCuddAdd())); } + + template + InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractRepresentative"); + //return InternalAdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); + } template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd().getCuddAdd())); } + + template + InternalBdd InternalAdd::maxAbstractRepresentative(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstractRepresentative"); + //return InternalAdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); + } template bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 9b7bca255..a86a2d654 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -259,6 +259,13 @@ namespace storm { * @param cube The cube from which to abstract. */ InternalAdd minAbstract(InternalBdd const& cube) const; + + /*! + * Min-abstracts from the given cube and returns a representative. + * + * @param cube The cube from which to abstract. + */ + InternalBdd minAbstractRepresentative(InternalBdd const& cube) const; /*! * Max-abstracts from the given cube. @@ -266,6 +273,13 @@ namespace storm { * @param cube The cube from which to abstract. */ InternalAdd maxAbstract(InternalBdd const& cube) const; + + /*! + * Max-abstracts from the given cube and returns a representative. + * + * @param cube The cube from which to abstract. + */ + InternalBdd maxAbstractRepresentative(InternalBdd const& cube) const; /*! * Checks whether the current and the given ADD represent the same function modulo some given precision. diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index af7832945..c3ea30488 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -305,6 +305,11 @@ namespace storm { InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd)); } + + template + InternalBdd InternalAdd::minAbstractRepresentative(InternalBdd const& cube) const { + return InternalBdd(ddManager, this->sylvanMtbdd.AbstractMinRepresentative(cube.sylvanBdd)); + } #ifdef STORM_HAVE_CARL template<> @@ -317,6 +322,11 @@ namespace storm { InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMax(cube.sylvanBdd)); } + + template + InternalBdd InternalAdd::maxAbstractRepresentative(InternalBdd const& cube) const { + return InternalBdd(ddManager, this->sylvanMtbdd.AbstractMaxRepresentative(cube.sylvanBdd)); + } #ifdef STORM_HAVE_CARL template<> diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index b073af6cb..ace237565 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -261,6 +261,13 @@ namespace storm { * @param cube The cube from which to abstract. */ InternalAdd minAbstract(InternalBdd const& cube) const; + + /*! + * Min-abstracts from the given cube and returns a representative. + * + * @param cube The cube from which to abstract. + */ + InternalBdd minAbstractRepresentative(InternalBdd const& cube) const; /*! * Max-abstracts from the given cube. @@ -268,6 +275,13 @@ namespace storm { * @param cube The cube from which to abstract. */ InternalAdd maxAbstract(InternalBdd const& cube) const; + + /*! + * Max-abstracts from the given cube and returns a representative. + * + * @param cube The cube from which to abstract. + */ + InternalBdd maxAbstractRepresentative(InternalBdd const& cube) const; /*! * Checks whether the current and the given ADD represent the same function modulo some given precision.