Added min/max functions on DDs. Added tests for them and ite operation.

Former-commit-id: 8e6df90a38

src/storage/dd/CuddDd.cpp

@@ -25,7 +25,7 @@ namespace storm {
             metaVariableNames.insert(thenDd.getContainedMetaVariableNames().begin(), thenDd.getContainedMetaVariableNames().end());
             metaVariableNames.insert(elseDd.getContainedMetaVariableNames().begin(), elseDd.getContainedMetaVariableNames().end());
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()));
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::operator+(Dd<DdType::CUDD> const& other) const {
@@ -153,6 +153,20 @@ namespace storm {
             return result;
         }
         
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::minimum(Dd<DdType::CUDD> const& other) const {
+            std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+            metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+            
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariableNames);
+        }
+
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::maximum(Dd<DdType::CUDD> const& other) const {
+            std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+            metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+            
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariableNames);
+        }
+
         void Dd<DdType::CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) {
             Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
             

src/storage/dd/CuddDd.h

@@ -210,6 +210,22 @@ namespace storm {
              */
             Dd<DdType::CUDD> greaterOrEqual(Dd<DdType::CUDD> const& other) const;
             
+            /*!
+             * Retrieves the function that maps all evaluations to the minimum of the function values of the two DDs.
+             *
+             * @param other The DD with which to perform the operation.
+             * @return The resulting function represented as a DD.
+             */
+            Dd<DdType::CUDD> minimum(Dd<DdType::CUDD> const& other) const;
+
+            /*!
+             * Retrieves the function that maps all evaluations to the maximum of the function values of the two DDs.
+             *
+             * @param other The DD with which to perform the operation.
+             * @return The resulting function represented as a DD.
+             */
+            Dd<DdType::CUDD> maximum(Dd<DdType::CUDD> const& other) const;
+
             /*!
              * Existentially abstracts from the given meta variables.
              *

test/functional/storage/CuddDdTest.cpp

@@ -178,6 +178,20 @@ TEST(CuddDd, OperatorTest) {
     dd3 = dd1.greaterOrEqual(dd2);
     EXPECT_EQ(5, dd3.getNonZeroCount());
     
+    dd3 = (manager->getEncoding("x", 2)).ite(dd2, dd1);
+    dd4 = dd3.less(dd2);
+    EXPECT_EQ(10, dd4.getNonZeroCount());
+    
+    dd4 = dd3.minimum(dd1);
+    dd4 *= manager->getEncoding("x", 2);
+    dd4.sumAbstract({"x"});
+    EXPECT_EQ(2, dd4.getValue());
+
+    dd4 = dd3.maximum(dd1);
+    dd4 *= manager->getEncoding("x", 2);
+    dd4.sumAbstract({"x"});
+    EXPECT_EQ(5, dd4.getValue());
+
     dd1 = manager->getConstant(0.01);
     dd2 = manager->getConstant(0.01 + 1e-6);
     EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false));