added more functions in sylvan

Former-commit-id: f2e0c158a6

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

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
  */

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
 {

resources/3rdparty/sylvan/src/sylvan_obj.hpp

@@ -590,6 +590,8 @@ public:
     
     Bdd NotZero() const;
     
+    Bdd Equals(const Mtbdd& other) const;
+
     /**
      * @brief Computes the support of a Mtbdd.
      */

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>

test/functional/storage/SylvanDdTest.cpp

@@ -114,6 +114,7 @@ TEST(SylvanDd, OperatorTest) {
     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);
 //