diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
index 26de3cf1b..a02a7877e 100644
--- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
+++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
@@ -1427,6 +1427,59 @@ 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;
+}
+
/**
* Compute IF <f> THEN <g> ELSE <h>.
* <f> must be a Boolean MTBDD (or standard BDD).
diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h
index fb3ec24ac..8053b76c1 100644
--- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h
+++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h
@@ -250,6 +250,19 @@ 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*);
+
+/**
+ * Compute a == b
+ */
+#define mtbdd_equals(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_equals))
+
/**
* Compute a + b
*/
diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp
index da6f7b66b..29e6ec714 100644
--- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp
+++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp
@@ -906,6 +906,12 @@ Mtbdd::NotZero() const
return mtbdd_not_zero(mtbdd);
}
+Bdd
+Mtbdd::Equals(const Mtbdd& other) const {
+ LACE_ME;
+ return mtbdd_equals(mtbdd, other.mtbdd);
+}
+
Mtbdd
Mtbdd::Support() const
{
diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp
index 730e86261..fd47fa662 100644
--- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp
+++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp
@@ -589,6 +589,8 @@ public:
Bdd BddStrictThreshold(double value) const;
Bdd NotZero() const;
+
+ Bdd Equals(const Mtbdd& other) const;
/**
* @brief Computes the support of a Mtbdd.
diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
index ba7d2ec21..363f1927c 100644
--- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
@@ -24,7 +24,7 @@ namespace storm {
template<typename ValueType>
InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::ite(InternalAdd<DdType::Sylvan, ValueType> const& thenDd, InternalAdd<DdType::Sylvan, ValueType> const& elseDd) const {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+ return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.NotZero().Ite(thenDd.sylvanMtbdd, elseDd.sylvanMtbdd));
}
template<typename ValueType>
@@ -73,12 +73,12 @@ namespace storm {
template<typename ValueType>
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::equals(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.Equals(other.sylvanMtbdd));
}
template<typename ValueType>
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::notEquals(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+ return !this->equals(other);
}
template<typename ValueType>
@@ -93,12 +93,12 @@ namespace storm {
template<typename ValueType>
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greater(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+ return !this->lessOrEqual(other);
}
template<typename ValueType>
InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::greaterOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+ return !this->less(other);
}
template<typename ValueType>
diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp
index cd47c66a7..9ec54b2f0 100644
--- a/test/functional/storage/SylvanDdTest.cpp
+++ b/test/functional/storage/SylvanDdTest.cpp
@@ -110,10 +110,11 @@ TEST(SylvanDd, OperatorTest) {
EXPECT_FALSE(manager->template getAddZero<double>() != manager->template getAddZero<double>());
EXPECT_TRUE(manager->template getAddZero<double>() != manager->template getAddOne<double>());
-
+
storm::dd::Add<storm::dd::DdType::Sylvan, double> dd1 = manager->template getAddOne<double>();
storm::dd::Add<storm::dd::DdType::Sylvan, double> dd2 = manager->template getAddOne<double>();
storm::dd::Add<storm::dd::DdType::Sylvan, double> dd3 = dd1 + dd2;
+ storm::dd::Bdd<storm::dd::DdType::Sylvan> bdd;
EXPECT_TRUE(dd3 == manager->template getConstant<double>(2));
dd3 += manager->template getAddZero<double>();
@@ -134,15 +135,15 @@ TEST(SylvanDd, OperatorTest) {
dd3 /= manager->template getConstant<double>(2);
EXPECT_TRUE(dd3.isOne());
-// dd3 = !dd3;
-// EXPECT_TRUE(dd3.isZero());
-//
-// dd1 = !dd3;
-// EXPECT_TRUE(dd1.isOne());
-//
-// dd3 = dd1 || dd2;
-// EXPECT_TRUE(dd3.isOne());
-//
+ bdd = !dd3.toBdd();
+ EXPECT_TRUE(bdd.isZero());
+
+ bdd = !bdd;
+ EXPECT_TRUE(bdd.isOne());
+
+ bdd = dd1.toBdd() || dd2.toBdd();
+ EXPECT_TRUE(bdd.isOne());
+
// dd1 = manager->template getIdentity<double>(x.first);
// dd2 = manager->template getConstant<double>(5);
//