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

Merge remote-tracking branch 'origin/sylvanRationalFunctions' into menu_games 

Former-commit-id: 02786f9b10
tempestpy_adaptions
dehnert 9 years ago
parent
56b5b98a2c 68b14b3076
commit
42af59ef5d
20 changed files with 507 additions and 344 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 15
      resources/3rdparty/sylvan/src/storm_function_wrapper.cpp
  2. 3
      resources/3rdparty/sylvan/src/storm_function_wrapper.h
  3. 212
      resources/3rdparty/sylvan/src/sylvan_bdd.c
  4. 87
      resources/3rdparty/sylvan/src/sylvan_bdd_int.h
  5. 6
      resources/3rdparty/sylvan/src/sylvan_bdd_storm.c
  6. 6
      resources/3rdparty/sylvan/src/sylvan_gmp.c
  7. 158
      resources/3rdparty/sylvan/src/sylvan_mtbdd.c
  8. 2
      resources/3rdparty/sylvan/src/sylvan_mtbdd_int.h
  9. 228
      resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
  10. 5
      resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h
  11. 4
      resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp
  12. 4
      resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
  13. 23
      resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
  14. 21
      resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h
  15. 12
      src/storage/dd/Add.cpp
  16. 18
      src/storage/dd/Add.h
  17. 13
      src/storage/dd/cudd/InternalCuddAdd.cpp
  18. 14
      src/storage/dd/cudd/InternalCuddAdd.h
  19. 10
      src/storage/dd/sylvan/InternalSylvanAdd.cpp
  20. 14
      src/storage/dd/sylvan/InternalSylvanAdd.h

15
resources/3rdparty/sylvan/src/storm_function_wrapper.cpp
View File

@ -4,6 +4,7 @@
#include <iostream>
#include <sstream>
#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;
}

3
resources/3rdparty/sylvan/src/storm_function_wrapper.h
View File

@ -3,6 +3,7 @@
#include <stdint.h>
#include <stdio.h>
#include <sylvan.h>
#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

212
resources/3rdparty/sylvan/src/sylvan_bdd.c
View File

@ -30,69 +30,7 @@
#include <sha2.h>
#include <sylvan.h>
#include <sylvan_common.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 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 <sylvan_bdd_int.h>
/**
* 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 <bdd>
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);

87
resources/3rdparty/sylvan/src/sylvan_bdd_int.h
View File

@ -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

6
resources/3rdparty/sylvan/src/sylvan_bdd_storm.c
View File

@ -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);

6
resources/3rdparty/sylvan/src/sylvan_gmp.c
View File

@ -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) {

158
resources/3rdparty/sylvan/src/sylvan_mtbdd.c
View File

@ -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);

2
resources/3rdparty/sylvan/src/sylvan_mtbdd_int.h
View File

@ -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

228
resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
View File

@ -1,3 +1,5 @@
#include <sylvan_bdd_int.h>
/**
* 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;
}
mtbdd_ref(res1);
MTBDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va);
if (res2 == mtbdd_invalid) {
mtbdd_deref(res1);
return mtbdd_invalid;
}
mtbdd_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;
}
mtbdd_deref(res1);
mtbdd_deref(res2);
BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va);
if (res1 == sylvan_invalid) {
return sylvan_invalid;
}
sylvan_ref(res1);
BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va);
if (res2 == sylvan_invalid) {
sylvan_deref(res1);
return sylvan_invalid;
}
sylvan_ref(res2);
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;
}
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;

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

@ -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))

4
resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp
View File

@ -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;

4
resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
View File

@ -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;

23
resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c
View File

@ -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 <a> and <b>, and abstract variables <vars> 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) {

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

@ -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 <a> and <b>, and abstract variables <vars> 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 */

12
src/storage/dd/Add.cpp
View File

@ -162,6 +162,12 @@ namespace storm {
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.minAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
}
template<DdType LibraryType, typename ValueType>
Bdd<LibraryType> Add<LibraryType, ValueType>::minAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const {
Bdd<LibraryType> cube = Bdd<LibraryType>::getCube(this->getDdManager(), metaVariables);
return Bdd<LibraryType>(this->getDdManager(), internalAdd.minAbstractRepresentative(cube), this->getContainedMetaVariables());
}
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::minAbstractExcept0(std::set<storm::expressions::Variable> const& metaVariables) const {
Bdd<LibraryType> cube = Bdd<LibraryType>::getCube(this->getDdManager(), metaVariables);
@ -174,6 +180,12 @@ namespace storm {
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.maxAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
}
template<DdType LibraryType, typename ValueType>
Bdd<LibraryType> Add<LibraryType, ValueType>::maxAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const {
Bdd<LibraryType> cube = Bdd<LibraryType>::getCube(this->getDdManager(), metaVariables);
return Bdd<LibraryType>(this->getDdManager(), internalAdd.maxAbstractRepresentative(cube), this->getContainedMetaVariables());
}
template<DdType LibraryType, typename ValueType>
bool Add<LibraryType, ValueType>::equalModuloPrecision(Add<LibraryType, ValueType> const& other, double precision, bool relative) const {
return internalAdd.equalModuloPrecision(other, precision, relative);

18
src/storage/dd/Add.h
View File

@ -264,6 +264,15 @@ namespace storm {
*/
Add<LibraryType, ValueType> minAbstractExcept0(std::set<storm::expressions::Variable> const& metaVariables) const;
/*!
* Similar to <code>minAbstract</code>, 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<LibraryType> minAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const;
/*!
* Max-abstracts from the given meta variables.
*
@ -271,6 +280,15 @@ namespace storm {
*/
Add<LibraryType, ValueType> maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
/*!
* Similar to <code>maxAbstract</code>, 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<LibraryType> maxAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const;
/*!
* Checks whether the current and the given ADD represent the same function modulo some given precision.
*

13
src/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -9,6 +9,7 @@
#include "src/utility/constants.h"
#include "src/utility/macros.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
namespace dd {
@ -146,6 +147,12 @@ namespace storm {
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstract(cube.toAdd<ValueType>().getCuddAdd()));
}
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::minAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractRepresentative");
//return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
}
template<typename ValueType>
InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minAbstractExcept0(InternalBdd<DdType::CUDD> const& cube) const {
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstractExcept0(cube.toAdd<ValueType>().getCuddAdd()));
@ -156,6 +163,12 @@ namespace storm {
return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd<ValueType>().getCuddAdd()));
}
template<typename ValueType>
InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::maxAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstractRepresentative");
//return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
}
template<typename ValueType>
bool InternalAdd<DdType::CUDD, ValueType>::equalModuloPrecision(InternalAdd<DdType::CUDD, ValueType> const& other, double precision, bool relative) const {
if (relative) {

14
src/storage/dd/cudd/InternalCuddAdd.h
View File

@ -267,6 +267,13 @@ namespace storm {
*/
InternalAdd<DdType::CUDD, ValueType> minAbstractExcept0(InternalBdd<DdType::CUDD> const& cube) const;
/*!
* Min-abstracts from the given cube and returns a representative.
*
* @param cube The cube from which to abstract.
*/
InternalBdd<DdType::CUDD> minAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const;
/*!
* Max-abstracts from the given cube.
*
@ -274,6 +281,13 @@ namespace storm {
*/
InternalAdd<DdType::CUDD, ValueType> maxAbstract(InternalBdd<DdType::CUDD> const& cube) const;
/*!
* Max-abstracts from the given cube and returns a representative.
*
* @param cube The cube from which to abstract.
*/
InternalBdd<DdType::CUDD> maxAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const;
/*!
* Checks whether the current and the given ADD represent the same function modulo some given precision.
*

10
src/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -306,6 +306,11 @@ namespace storm {
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd));
}
template<typename ValueType>
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::minAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const {
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.AbstractMinRepresentative(cube.sylvanBdd));
}
#ifdef STORM_HAVE_CARL
template<>
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
@ -330,6 +335,11 @@ namespace storm {
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractMax(cube.sylvanBdd));
}
template<typename ValueType>
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::maxAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const {
return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.AbstractMaxRepresentative(cube.sylvanBdd));
}
#ifdef STORM_HAVE_CARL
template<>
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const {

14
src/storage/dd/sylvan/InternalSylvanAdd.h
View File

@ -269,6 +269,13 @@ namespace storm {
*/
InternalAdd<DdType::Sylvan, ValueType> minAbstractExcept0(InternalBdd<DdType::Sylvan> const& cube) const;
/*!
* Min-abstracts from the given cube and returns a representative.
*
* @param cube The cube from which to abstract.
*/
InternalBdd<DdType::Sylvan> minAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const;
/*!
* Max-abstracts from the given cube.
*
@ -276,6 +283,13 @@ namespace storm {
*/
InternalAdd<DdType::Sylvan, ValueType> maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const;
/*!
* Max-abstracts from the given cube and returns a representative.
*
* @param cube The cube from which to abstract.
*/
InternalBdd<DdType::Sylvan> maxAbstractRepresentative(InternalBdd<DdType::Sylvan> const& cube) const;
/*!
* Checks whether the current and the given ADD represent the same function modulo some given precision.
*
Write Preview
Loading…
Cancel
Save