more work on sylvan integration

Former-commit-id: 1bd63e5373

resources/3rdparty/sylvan/src/lace.h

@@ -182,7 +182,7 @@ struct __lace_common_fields_only { TASK_COMMON_FIELDS(_Task) };
 #define LACE_COMMON_FIELD_SIZE sizeof(struct __lace_common_fields_only)
 
 typedef struct _Task {
-    TASK_COMMON_FIELDS(_Task);
+    TASK_COMMON_FIELDS(_Task)
     char p1[PAD(LACE_COMMON_FIELD_SIZE, P_SZ)];
     char d[LACE_TASKSIZE];
     char p2[PAD(ROUND(LACE_COMMON_FIELD_SIZE, P_SZ) + LACE_TASKSIZE, LINE_SIZE)];

resources/3rdparty/sylvan/src/sylvan_mtbdd.c

@@ -1263,11 +1263,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
         }
     }
     
-    if (a < b) {
-        *pa = b;
-        *pb = a;
-    }
-    
     return mtbdd_invalid;
 }
 
@@ -1480,6 +1475,135 @@ TASK_IMPL_2(MTBDD, mtbdd_op_equals, 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_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).
@@ -1588,7 +1712,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue)
     return mtbdd_invalid;
 }
 
-TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, a)
+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;
@@ -1607,7 +1731,18 @@ TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, a)
         }
     }
     
-    return mtbdd_invalid;
+    // 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)
@@ -1620,6 +1755,16 @@ 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
  */

resources/3rdparty/sylvan/src/sylvan_mtbdd.h

@@ -258,6 +258,22 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int);
  */
 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
  */
@@ -292,6 +308,9 @@ TASK_DECL_2(MTBDD, mtbdd_op_equals, 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
@@ -340,8 +359,12 @@ 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_1(MTBDD, mtbdd_not_zero, MTBDD)
-#define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd)
+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;
@@ -355,6 +378,12 @@ 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
  * i.e. abs(a-b)<3

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

@@ -443,6 +443,12 @@ Bdd::NodeCount() const
     return sylvan_nodecount(bdd);
 }
 
+Mtbdd
+Bdd::toDoubleMtbdd() const {
+    LACE_ME;
+    return mtbdd_bool_to_double(bdd);
+}
+
 Bdd
 Bdd::bddOne()
 {
@@ -912,6 +918,32 @@ Mtbdd::Equals(const Mtbdd& other) const {
     return mtbdd_equals(mtbdd, other.mtbdd);
 }
 
+Bdd
+Mtbdd::Less(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_less_as_bdd(mtbdd, other.mtbdd);
+}
+
+Bdd
+Mtbdd::LessOrEqual(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd);
+}
+
+double
+Mtbdd::getDoubleMax() const {
+    LACE_ME;
+    MTBDD maxNode = mtbdd_maximum(mtbdd);
+    return mtbdd_getdouble(maxNode);
+}
+
+double
+Mtbdd::getDoubleMin() const {
+    LACE_ME;
+    MTBDD minNode = mtbdd_minimum(mtbdd);
+    return mtbdd_getdouble(minNode);
+}
+
 Mtbdd
 Mtbdd::Support() const
 {

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

@@ -27,6 +27,8 @@ namespace sylvan {
 
 class BddMap;
 
+class Mtbdd;
+    
 class Bdd {
     friend class Sylvan;
     friend class BddMap;
@@ -317,6 +319,8 @@ public:
      */
     size_t NodeCount() const;
 
+    Mtbdd toDoubleMtbdd() const;
+    
 private:
     BDD bdd;
 };
@@ -591,7 +595,15 @@ public:
     Bdd NotZero() const;
     
     Bdd Equals(const Mtbdd& other) const;
+    
+    Bdd Less(const Mtbdd& other) const;
 
+    Bdd LessOrEqual(const Mtbdd& other) const;
+    
+    double getDoubleMax() const;
+
+    double getDoubleMin() 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 {
-            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.NotZero().Ite(thenDd.sylvanMtbdd, elseDd.sylvanMtbdd));
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, sylvan::Mtbdd(static_cast<MTBDD>(this->sylvanMtbdd.NotZero().GetBDD())).Ite(thenDd.sylvanMtbdd, elseDd.sylvanMtbdd));
         }
                 
         template<typename ValueType>
@@ -73,7 +73,7 @@ namespace storm {
         
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::equals(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
-            return InternalAdd<DdType::Sylvan, ValueType>(ddManager,  this->sylvanMtbdd.Equals(other.sylvanMtbdd));
+            return InternalBdd<DdType::Sylvan>(ddManager,  this->sylvanMtbdd.Equals(other.sylvanMtbdd));
         }
         
         template<typename ValueType>
@@ -83,12 +83,12 @@ namespace storm {
         
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::less(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.Less(other.sylvanMtbdd));
         }
         
         template<typename ValueType>
         InternalBdd<DdType::Sylvan> InternalAdd<DdType::Sylvan, ValueType>::lessOrEqual(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanMtbdd.LessOrEqual(other.sylvanMtbdd));
         }
         
         template<typename ValueType>
@@ -227,12 +227,12 @@ namespace storm {
         
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getMin() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return static_cast<ValueType>(this-sylvanMtbdd.getDoubleMin());
         }
         
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getMax() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return static_cast<ValueType>(this-sylvanMtbdd.getDoubleMax());
         }
         
         template<typename ValueType>

src/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -147,7 +147,7 @@ namespace storm {
         
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalBdd<DdType::Sylvan>::toAdd() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanBdd.toDoubleMtbdd());
         }
         
         storm::storage::BitVector InternalBdd<DdType::Sylvan>::toVector(storm::dd::Odd const& rowOdd, std::vector<uint_fast64_t> const& ddVariableIndices) const {

test/functional/storage/SylvanDdTest.cpp

@@ -144,36 +144,36 @@ TEST(SylvanDd, OperatorTest) {
     bdd = dd1.toBdd() || dd2.toBdd();
     EXPECT_TRUE(bdd.isOne());
     
-//    dd1 = manager->template getIdentity<double>(x.first);
-//    dd2 = manager->template getConstant<double>(5);
-//    
-//    dd3 = dd1.equals(dd2);
-//    EXPECT_EQ(1ul, dd3.getNonZeroCount());
-//    
-//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd4 = dd1.notEquals(dd2);
-//    EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd());
-//    
-//    dd3 = dd1.less(dd2);
-//    EXPECT_EQ(11ul, dd3.getNonZeroCount());
-//    
-//    dd3 = dd1.lessOrEqual(dd2);
-//    EXPECT_EQ(12ul, dd3.getNonZeroCount());
-//    
-//    dd3 = dd1.greater(dd2);
-//    EXPECT_EQ(4ul, dd3.getNonZeroCount());
-//    
-//    dd3 = dd1.greaterOrEqual(dd2);
-//    EXPECT_EQ(5ul, dd3.getNonZeroCount());
-//    
-//    dd3 = (manager->getEncoding(x.first, 2).template toAdd<double>()).ite(dd2, dd1);
-//    dd4 = dd3.less(dd2);
-//    EXPECT_EQ(10ul, dd4.getNonZeroCount());
-//    
-//    dd4 = dd3.minimum(dd1);
-//    dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
-//    dd4 = dd4.sumAbstract({x.first});
-//    EXPECT_EQ(2, dd4.getValue());
-//    
+    dd1 = manager->template getIdentity<double>(x.first);
+    dd2 = manager->template getConstant<double>(5);
+    
+    bdd = dd1.equals(dd2);
+    EXPECT_EQ(1ul, bdd.getNonZeroCount());
+    
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> bdd2 = dd1.notEquals(dd2);
+    EXPECT_TRUE(bdd2 == !bdd);
+    
+    bdd = dd1.less(dd2);
+    EXPECT_EQ(11ul, bdd.getNonZeroCount());
+    
+    bdd = dd1.lessOrEqual(dd2);
+    EXPECT_EQ(12ul, bdd.getNonZeroCount());
+    
+    bdd = dd1.greater(dd2);
+    EXPECT_EQ(4ul, bdd.getNonZeroCount());
+    
+    bdd = dd1.greaterOrEqual(dd2);
+    EXPECT_EQ(5ul, bdd.getNonZeroCount());
+    
+    dd3 = (manager->getEncoding(x.first, 2).template toAdd<double>()).ite(dd2, dd1);
+    bdd = dd3.less(dd2);
+    EXPECT_EQ(10ul, bdd.getNonZeroCount());
+
+    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd4 = dd3.minimum(dd1);
+    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});