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

added some new functions to sylvan. isolated new code to make it easier to update sylvan to newer versions later 

Former-commit-id: 6b489993a5
tempestpy_adaptions
dehnert 9 years ago
parent
8eb3720f91
commit
7ea0cb19b3
8 changed files with 643 additions and 380 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. 302
      resources/3rdparty/sylvan/src/sylvan_mtbdd.c
  2. 65
      resources/3rdparty/sylvan/src/sylvan_mtbdd.h
  3. 43
      resources/3rdparty/sylvan/src/sylvan_obj.cpp
  4. 14
      resources/3rdparty/sylvan/src/sylvan_obj.hpp
  5. 464
      resources/3rdparty/sylvan/src/sylvan_storm_custom.c
  6. 95
      resources/3rdparty/sylvan/src/sylvan_storm_custom.h
  7. 20
      src/storage/dd/sylvan/InternalSylvanAdd.cpp
  8. 20
      test/functional/storage/SylvanDdTest.cpp

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

@ -1191,81 +1191,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb)
return mtbdd_invalid;
}
/**
* Binary operation Times (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Integer or Double.
* If either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *pb;
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
// Do not handle Boolean MTBDDs...
mtbddnode_t na = GETNODE(a);
mtbddnode_t nb = GETNODE(b);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
// both uint64_t
if (val_a == 0) return a;
else if (val_b == 0) return b;
else {
MTBDD result;
if (val_a == 1) result = b;
else if (val_b == 1) result = a;
else result = mtbdd_uint64(val_a*val_b);
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nega ^ negb) return mtbdd_negate(result);
else return result;
}
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
if (vval_a == 0.0) return a;
else if (vval_b == 0.0) return b;
else {
MTBDD result;
if (vval_a == 0.0 || vval_b == 1.0) result = a;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
result = mtbdd_double(a / b);
if (nega ^ negb) return mtbdd_negate(result);
else return result;
}
}
else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
// multiply!
uint32_t c = gcd(denom_b, denom_a);
uint32_t d = gcd(nom_a, nom_b);
nom_a /= d;
denom_a /= c;
nom_a *= (denom_b/c);
denom_a *= (nom_b/d);
// compute result
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
MTBDD result = mtbdd_fraction(nom_a, denom_a);
if (nega ^ negb) return mtbdd_negate(result);
else return result;
}
}
return mtbdd_invalid;
}
/**
* Binary operation Minimum (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
@ -1422,188 +1347,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, MTBDD*, pa, MTBDD*, pb)
return mtbdd_invalid;
}
/**
* Binary operation Equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
// both uint64_t
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (val_a == val_b && !(nega ^ negb)) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (vval_a == vval_b && !(nega ^ negb)) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nom_a == nom_b && denom_a == denom_b && !(nega ^ negb)) return mtbdd_true;
return mtbdd_false;
}
}
if (a < b) {
*pa = b;
*pb = a;
}
return mtbdd_invalid;
}
/**
* Binary operation Equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
// both uint64_t
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nega && !negb) return mtbdd_true;
if (!nega && negb) return mtbdd_false;
if (nega && negb && val_a < val_b) return mtbdd_false;
return mtbdd_true;
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
if (nega) vval_a = -vval_a;
int negb = mtbdd_isnegated(b);
if (negb) vval_b = -vval_b;
if (vval_a < vval_b) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nega && !negb) return mtbdd_true;
if (!nega && negb) return mtbdd_false;
return nom_a * denom_b < nom_b * denom_a ? mtbdd_true : mtbdd_false;
}
}
return mtbdd_invalid;
}
/**
* Binary operation Equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
// both uint64_t
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nega && !negb) {
if (val_a != 0) return mtbdd_true;
if (val_b != 0) return mtbdd_true;
return mtbdd_false;
}
if (!nega && negb) {
if (val_b != 0) return mtbdd_false;
if (val_a != 0) return mtbdd_false;
return mtbdd_true;
}
if (nega && negb) {
return val_a >= val_b ? mtbdd_true : mtbdd_false;
}
return val_a <= val_b ? mtbdd_true : mtbdd_false;
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
if (nega) vval_a = -vval_a;
int negb = mtbdd_isnegated(b);
if (negb) vval_b = -vval_b;
if (vval_a <= vval_b) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
nom_a *= denom_b;
nom_b *= denom_a;
if (nega && !negb) {
if (nom_a != 0) return mtbdd_true;
if (nom_b != 0) return mtbdd_true;
return mtbdd_false;
}
if (!nega && negb) {
if (nom_a != 0) return mtbdd_false;
if (nom_b != 0) return mtbdd_false;
return mtbdd_true;
}
if (nega && negb) {
return nom_a >= nom_b ? mtbdd_true : mtbdd_false;
}
return val_a <= val_b ? mtbdd_true : mtbdd_false;
}
}
return mtbdd_invalid;
}
/**
* Compute IF <f> THEN <g> ELSE <h>.
* <f> must be a Boolean MTBDD (or standard BDD).
@ -1712,39 +1455,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue)
return mtbdd_invalid;
}
TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v)
{
/* We only expect "double" terminals, or false */
if (a == mtbdd_false) return mtbdd_false;
if (a == mtbdd_true) return mtbdd_invalid;
// a != constant
mtbddnode_t na = GETNODE(a);
if (mtbddnode_isleaf(na)) {
if (mtbddnode_gettype(na) == 0) {
return mtbdd_getuint64(a) != 0 ? mtbdd_true : mtbdd_false;
} else if (mtbddnode_gettype(na) == 1) {
return mtbdd_getdouble(a) != 0.0 ? mtbdd_true : mtbdd_false;
} else if (mtbddnode_gettype(na) == 2) {
return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false;
}
}
// Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
return v > 0 ? mtbdd_invalid : mtbdd_invalid;
}
TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, a, size_t, v)
{
/* We only expect "double" terminals, or false */
if (a == mtbdd_false) return mtbdd_double(0);
if (a == mtbdd_true) return mtbdd_double(1.0);
// Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
return v > 0 ? mtbdd_invalid : mtbdd_invalid;
}
TASK_IMPL_2(MTBDD, mtbdd_threshold_double, MTBDD, dd, double, d)
{
return mtbdd_uapply(dd, TASK(mtbdd_op_threshold_double), *(size_t*)&d);
@ -1755,16 +1465,6 @@ TASK_IMPL_2(MTBDD, mtbdd_strict_threshold_double, MTBDD, dd, double, d)
return mtbdd_uapply(dd, TASK(mtbdd_op_strict_threshold_double), *(size_t*)&d);
}
TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, dd)
{
return mtbdd_uapply(dd, TASK(mtbdd_op_not_zero), 0);
}
TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd)
{
return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0);
}
/**
* Compare two Double MTBDDs, returns Boolean True if they are equal within some value epsilon
*/
@ -2881,3 +2581,5 @@ mtbdd_map_removeall(MTBDDMAP map, MTBDD variables)
return mtbdd_map_removeall(node_getlow(map, n1), node_gethigh(variables, n2));
}
}
#include "sylvan_storm_custom.c"

65
resources/3rdparty/sylvan/src/sylvan_mtbdd.h
View File

@ -223,14 +223,6 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_plus, MTBDD, MTBDD, int);
*/
TASK_DECL_2(MTBDD, mtbdd_op_times, MTBDD*, MTBDD*);
TASK_DECL_3(MTBDD, mtbdd_abstract_op_times, MTBDD, MTBDD, int);
/**
* Binary operation Divide (for MTBDDs of same type)
* Only for MTBDDs where all leaves are Integer or Double.
* If either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*);
/**
* Binary operation Minimum (for MTBDDs of same type)
@ -249,35 +241,6 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_min, MTBDD, MTBDD, int);
*/
TASK_DECL_2(MTBDD, mtbdd_op_max, MTBDD*, MTBDD*);
TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int);
/**
* Binary operation equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*);
/**
* Binary operation Less (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*);
/**
* Binary operation Less (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*);
/**
* Compute a == b
*/
#define mtbdd_equals(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_equals))
/**
* Compute a + b
@ -287,17 +250,12 @@ TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*);
/**
* Compute a - b
*/
#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b))
//#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b))
/**
* Compute a * b
*/
#define mtbdd_times(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_times))
/**
* Compute a / b
*/
#define mtbdd_divide(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_divide))
/**
* Compute min(a, b)
@ -308,9 +266,6 @@ TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*);
* Compute max(a, b)
*/
#define mtbdd_max(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_max))
#define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less))
#define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal))
/**
* Abstract the variables in <v> from <a> by taking the sum of all values
@ -355,16 +310,6 @@ TASK_DECL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, size_t)
* Monad that converts double to a Boolean MTBDD, translate terminals > value to 1 and to 0 otherwise;
*/
TASK_DECL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, size_t)
/**
* Monad that converts double to a Boolean MTBDD, translate terminals != 0 to 1 and to 0 otherwise;
*/
TASK_DECL_2(MTBDD, mtbdd_op_not_zero, MTBDD, size_t)
/**
* Monad that converts Boolean to a Double MTBDD, translate terminals true to 1 and to 0 otherwise;
*/
TASK_DECL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, size_t)
/**
* Convert double to a Boolean MTBDD, translate terminals >= value to 1 and to 0 otherwise;
@ -377,12 +322,6 @@ TASK_DECL_2(MTBDD, mtbdd_threshold_double, MTBDD, double);
*/
TASK_DECL_2(MTBDD, mtbdd_strict_threshold_double, MTBDD, double);
#define mtbdd_strict_threshold_double(dd, value) CALL(mtbdd_strict_threshold_double, dd, value)
TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD)
#define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd)
TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD)
#define mtbdd_bool_to_double(dd) CALL(mtbdd_bool_to_double, dd)
/**
* For two Double MTBDDs, calculate whether they are equal module some value epsilon
@ -612,6 +551,8 @@ mtbdd_refs_sync(MTBDD result)
return result;
}
#include "sylvan_storm_custom.h"
#ifdef __cplusplus
}
#endif /* __cplusplus */

43
resources/3rdparty/sylvan/src/sylvan_obj.cpp
View File

@ -944,6 +944,49 @@ Mtbdd::getDoubleMin() const {
return mtbdd_getdouble(minNode);
}
bool
Mtbdd::EqualNorm(const Mtbdd& other, double epsilon) const {
LACE_ME;
return mtbdd_equal_norm_d(mtbdd, other.mtbdd, epsilon);
}
bool
Mtbdd::EqualNormRel(const Mtbdd& other, double epsilon) const {
LACE_ME;
return mtbdd_equal_norm_rel_d(mtbdd, other.mtbdd, epsilon);
}
Mtbdd
Mtbdd::Floor() const {
LACE_ME;
return mtbdd_floor(mtbdd);
}
Mtbdd
Mtbdd::Ceil() const {
LACE_ME;
return mtbdd_ceil(mtbdd);
}
Mtbdd
Mtbdd::Pow(const Mtbdd& other) const {
LACE_ME;
return mtbdd_pow(mtbdd, other.mtbdd);
}
Mtbdd
Mtbdd::Mod(const Mtbdd& other) const {
LACE_ME;
return mtbdd_mod(mtbdd, other.mtbdd);
}
Mtbdd
Mtbdd::Logxy(const Mtbdd& other) const {
LACE_ME;
return mtbdd_logxy(mtbdd, other.mtbdd);
}
Mtbdd
Mtbdd::Support() const
{

14
resources/3rdparty/sylvan/src/sylvan_obj.hpp
View File

@ -604,6 +604,20 @@ public:
double getDoubleMin() const;
bool EqualNorm(const Mtbdd& other, double epsilon) const;
bool EqualNormRel(const Mtbdd& other, double epsilon) const;
Mtbdd Floor() const;
Mtbdd Ceil() const;
Mtbdd Pow(const Mtbdd& other) const;
Mtbdd Mod(const Mtbdd& other) const;
Mtbdd Logxy(const Mtbdd& other) const;
/**
* @brief Computes the support of a Mtbdd.
*/

464
resources/3rdparty/sylvan/src/sylvan_storm_custom.c
View File

@ -0,0 +1,464 @@
/**
* Binary operation Times (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Integer or Double.
* If either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *pb;
if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
// Do not handle Boolean MTBDDs...
mtbddnode_t na = GETNODE(a);
mtbddnode_t nb = GETNODE(b);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
// both uint64_t
if (val_a == 0) return a;
else if (val_b == 0) return b;
else {
MTBDD result;
if (val_a == 1) result = b;
else if (val_b == 1) result = a;
else result = mtbdd_uint64(val_a*val_b);
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nega ^ negb) return mtbdd_negate(result);
else return result;
}
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
if (vval_a == 0.0) return a;
else if (vval_b == 0.0) return b;
else {
MTBDD result;
if (vval_a == 0.0 || vval_b == 1.0) result = a;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
result = mtbdd_double(a / b);
if (nega ^ negb) return mtbdd_negate(result);
else return result;
}
}
else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
// multiply!
uint32_t c = gcd(denom_b, denom_a);
uint32_t d = gcd(nom_a, nom_b);
nom_a /= d;
denom_a /= c;
nom_a *= (denom_b/c);
denom_a *= (nom_b/d);
// compute result
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
MTBDD result = mtbdd_fraction(nom_a, denom_a);
if (nega ^ negb) return mtbdd_negate(result);
else return result;
}
}
return mtbdd_invalid;
}
/**
* Binary operation Equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
// both uint64_t
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (val_a == val_b && !(nega ^ negb)) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (vval_a == vval_b && !(nega ^ negb)) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nom_a == nom_b && denom_a == denom_b && !(nega ^ negb)) return mtbdd_true;
return mtbdd_false;
}
}
if (a < b) {
*pa = b;
*pb = a;
}
return mtbdd_invalid;
}
/**
* Binary operation Equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
// both uint64_t
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nega && !negb) return mtbdd_true;
if (!nega && negb) return mtbdd_false;
if (nega && negb && val_a < val_b) return mtbdd_false;
return mtbdd_true;
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
if (nega) vval_a = -vval_a;
int negb = mtbdd_isnegated(b);
if (negb) vval_b = -vval_b;
if (vval_a < vval_b) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nega && !negb) return mtbdd_true;
if (!nega && negb) return mtbdd_false;
return nom_a * denom_b < nom_b * denom_a ? mtbdd_true : mtbdd_false;
}
}
return mtbdd_invalid;
}
/**
* Binary operation Equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
{
MTBDD a = *pa, b = *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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
// both uint64_t
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
if (nega && !negb) {
if (val_a != 0) return mtbdd_true;
if (val_b != 0) return mtbdd_true;
return mtbdd_false;
}
if (!nega && negb) {
if (val_b != 0) return mtbdd_false;
if (val_a != 0) return mtbdd_false;
return mtbdd_true;
}
if (nega && negb) {
return val_a >= val_b ? mtbdd_true : mtbdd_false;
}
return val_a <= val_b ? mtbdd_true : mtbdd_false;
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
if (nega) vval_a = -vval_a;
int negb = mtbdd_isnegated(b);
if (negb) vval_b = -vval_b;
if (vval_a <= vval_b) return mtbdd_true;
return mtbdd_false;
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
// both fraction
uint64_t nom_a = val_a>>32;
uint64_t nom_b = val_b>>32;
uint64_t denom_a = val_a&0xffffffff;
uint64_t denom_b = val_b&0xffffffff;
int nega = mtbdd_isnegated(a);
int negb = mtbdd_isnegated(b);
nom_a *= denom_b;
nom_b *= denom_a;
if (nega && !negb) {
if (nom_a != 0) return mtbdd_true;
if (nom_b != 0) return mtbdd_true;
return mtbdd_false;
}
if (!nega && negb) {
if (nom_a != 0) return mtbdd_false;
if (nom_b != 0) return mtbdd_false;
return mtbdd_true;
}
if (nega && negb) {
return nom_a >= nom_b ? mtbdd_true : mtbdd_false;
}
return val_a <= val_b ? mtbdd_true : mtbdd_false;
}
}
return mtbdd_invalid;
}
/**
* Binary operation Pow (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
assert(0);
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
if (nega) vval_a = -vval_a;
int negb = mtbdd_isnegated(b);
if (negb) vval_b = -vval_b;
return mtbdd_double(pow(vval_a, vval_b));
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
assert(0);
}
}
return mtbdd_invalid;
}
/**
* Binary operation Mod (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
assert(0);
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
if (nega) vval_a = -vval_a;
int negb = mtbdd_isnegated(b);
if (negb) vval_b = -vval_b;
return mtbdd_double(fmod(vval_a, vval_b));
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
assert(0);
}
}
return mtbdd_invalid;
}
/**
* Binary operation Log (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
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);
if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
uint64_t val_a = mtbddnode_getvalue(na);
uint64_t val_b = mtbddnode_getvalue(nb);
if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
assert(0);
} else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
// both double
double vval_a = *(double*)&val_a;
double vval_b = *(double*)&val_b;
int nega = mtbdd_isnegated(a);
if (nega) vval_a = -vval_a;
int negb = mtbdd_isnegated(b);
if (negb) vval_b = -vval_b;
return mtbdd_double(log(vval_a) / log(vval_b));
} else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
assert(0);
}
}
return mtbdd_invalid;
}
TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v)
{
/* We only expect "double" terminals, or false */
if (a == mtbdd_false) return mtbdd_false;
if (a == mtbdd_true) return mtbdd_true;
// a != constant
mtbddnode_t na = GETNODE(a);
if (mtbddnode_isleaf(na)) {
if (mtbddnode_gettype(na) == 0) {
return mtbdd_getuint64(a) != 0 ? mtbdd_true : mtbdd_false;
} else if (mtbddnode_gettype(na) == 1) {
return mtbdd_getdouble(a) != 0.0 ? mtbdd_true : mtbdd_false;
} else if (mtbddnode_gettype(na) == 2) {
return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false;
}
}
// Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
return v > 0 ? mtbdd_invalid : mtbdd_invalid;
}
TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, dd)
{
return mtbdd_uapply(dd, TASK(mtbdd_op_not_zero), 0);
}
TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v)
{
/* We only expect "double" terminals, or false */
if (a == mtbdd_false) return mtbdd_false;
if (a == mtbdd_true) return mtbdd_true;
// a != constant
mtbddnode_t na = GETNODE(a);
if (mtbddnode_isleaf(na)) {
if (mtbddnode_gettype(na) == 0) {
return a;
} else if (mtbddnode_gettype(na) == 1) {
MTBDD result = mtbdd_double(floor(mtbdd_getdouble(a)));
return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
} else if (mtbddnode_gettype(na) == 2) {
MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a), 1);
return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
}
}
// Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
return v > 0 ? mtbdd_invalid : mtbdd_invalid;
}
TASK_IMPL_1(MTBDD, mtbdd_floor, MTBDD, dd)
{
return mtbdd_uapply(dd, TASK(mtbdd_op_floor), 0);
}
TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v)
{
/* We only expect "double" terminals, or false */
if (a == mtbdd_false) return mtbdd_false;
if (a == mtbdd_true) return mtbdd_true;
// a != constant
mtbddnode_t na = GETNODE(a);
if (mtbddnode_isleaf(na)) {
if (mtbddnode_gettype(na) == 0) {
return a;
} else if (mtbddnode_gettype(na) == 1) {
MTBDD result = mtbdd_double(ceil(mtbdd_getdouble(a)));
return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
} else if (mtbddnode_gettype(na) == 2) {
MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a) + 1, 1);
return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
}
}
// Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
return v > 0 ? mtbdd_invalid : mtbdd_invalid;
}
TASK_IMPL_1(MTBDD, mtbdd_ceil, MTBDD, dd)
{
return mtbdd_uapply(dd, TASK(mtbdd_op_ceil), 0);
}
TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, a, size_t, v)
{
/* We only expect "double" terminals, or false */
if (a == mtbdd_false) return mtbdd_double(0);
if (a == mtbdd_true) return mtbdd_double(1.0);
// Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
return v > 0 ? mtbdd_invalid : mtbdd_invalid;
}
TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd)
{
return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0);
}

95
resources/3rdparty/sylvan/src/sylvan_storm_custom.h
View File

@ -0,0 +1,95 @@
/**
* Compute a - b
*/
#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b))
/**
* Binary operation Divide (for MTBDDs of same type)
* Only for MTBDDs where all leaves are Integer or Double.
* If either operand is mtbdd_false (not defined),
* then the result is mtbdd_false (i.e. not defined).
*/
TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*);
#define mtbdd_divide(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_divide))
/**
* Binary operation equals (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*);
#define mtbdd_equals(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_equals))
/**
* Binary operation Less (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*);
#define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less))
/**
* Binary operation Less (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*);
#define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal))
/**
* Binary operation Pow (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Integer, Double or a Fraction.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_pow, MTBDD*, MTBDD*);
#define mtbdd_pow(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_pow))
/**
* Binary operation Mod (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Integer, Double or a Fraction.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_mod, MTBDD*, MTBDD*);
#define mtbdd_mod(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_mod))
/**
* Binary operation Log (for MTBDDs of same type)
* Only for MTBDDs where either all leaves are Double or a Fraction.
* For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
* then the result is the other operand.
*/
TASK_DECL_2(MTBDD, mtbdd_op_logxy, MTBDD*, MTBDD*);
#define mtbdd_logxy(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_logxy))
/**
* Monad that converts double to a Boolean MTBDD, translate terminals != 0 to 1 and to 0 otherwise;
*/
TASK_DECL_2(MTBDD, mtbdd_op_not_zero, MTBDD, size_t)
TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD)
#define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd)
/**
* Monad that floors all values Double and Fraction values.
*/
TASK_DECL_2(MTBDD, mtbdd_op_floor, MTBDD, size_t)
TASK_DECL_1(MTBDD, mtbdd_floor, MTBDD)
#define mtbdd_floor(dd) CALL(mtbdd_floor, dd)
/**
* Monad that ceils all values Double and Fraction values.
*/
TASK_DECL_2(MTBDD, mtbdd_op_ceil, MTBDD, size_t)
TASK_DECL_1(MTBDD, mtbdd_ceil, MTBDD)
#define mtbdd_ceil(dd) CALL(mtbdd_ceil, dd)
/**
* Monad that converts Boolean to a Double MTBDD, translate terminals true to 1 and to 0 otherwise;
*/
TASK_DECL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, size_t)
TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD)
#define mtbdd_bool_to_double(dd) CALL(mtbdd_bool_to_double, dd)

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

@ -103,27 +103,27 @@ namespace storm {
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::pow(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Pow(other.sylvanMtbdd));
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::mod(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Mod(other.sylvanMtbdd));
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::logxy(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Logxy(other.sylvanMtbdd));
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::floor() const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Floor());
}
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::ceil() const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Ceil());
}
template<typename ValueType>
@ -153,7 +153,11 @@ namespace storm {
template<typename ValueType>
bool InternalAdd<DdType::Sylvan, ValueType>::equalModuloPrecision(InternalAdd<DdType::Sylvan, ValueType> const& other, double precision, bool relative) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
if (relative) {
return this->sylvanMtbdd.EqualNormRel(other.sylvanMtbdd, precision);
} else {
return this->sylvanMtbdd.EqualNorm(other.sylvanMtbdd, precision);
}
}
template<typename ValueType>
@ -227,12 +231,12 @@ namespace storm {
template<typename ValueType>
ValueType InternalAdd<DdType::Sylvan, ValueType>::getMin() const {
return static_cast<ValueType>(this-sylvanMtbdd.getDoubleMin());
return static_cast<ValueType>(this->sylvanMtbdd.getDoubleMin());
}
template<typename ValueType>
ValueType InternalAdd<DdType::Sylvan, ValueType>::getMax() const {
return static_cast<ValueType>(this-sylvanMtbdd.getDoubleMax());
return static_cast<ValueType>(this->sylvanMtbdd.getDoubleMax());
}
template<typename ValueType>

20
test/functional/storage/SylvanDdTest.cpp
View File

@ -173,16 +173,16 @@ TEST(SylvanDd, OperatorTest) {
dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
dd4 = dd4.sumAbstract({x.first});
EXPECT_EQ(2, dd4.getValue());
//
// dd4 = dd3.maximum(dd1);
// dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
// dd4 = dd4.sumAbstract({x.first});
// EXPECT_EQ(5, dd4.getValue());
//
// dd1 = manager->template getConstant<double>(0.01);
// dd2 = manager->template getConstant<double>(0.01 + 1e-6);
// EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false));
// EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6));
dd4 = dd3.maximum(dd1);
dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
dd4 = dd4.sumAbstract({x.first});
EXPECT_EQ(5, dd4.getValue());
dd1 = manager->template getConstant<double>(0.01);
dd2 = manager->template getConstant<double>(0.01 + 1e-6);
EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false));
EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6));
}
//TEST(SylvanDd, AbstractionTest) {

Write Preview
Loading…
Cancel
Save