(re)introduced min/maxAbstractRepresentative for ADDs

Former-commit-id: 5a5d269339

resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h

@@ -769,6 +769,8 @@ extern DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cub
 extern DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_addMinAbstract(DdManager * manager, DdNode * f, DdNode * cube);
 extern DdNode * Cudd_addMaxAbstract(DdManager * manager, DdNode * f, DdNode * cube);
+extern DdNode * Cudd_addMinAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube);
+extern DdNode * Cudd_addMaxAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube);
 extern DdNode * Cudd_addApply (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
 extern DdNode * Cudd_addPlus (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addTimes (DdManager *dd, DdNode **f, DdNode **g);

resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c

@@ -310,6 +310,78 @@ Cudd_addMaxAbstract(
     
 } /* end of Cudd_addMaxAbstract */
 
+/**Function********************************************************************
+ 
+ Synopsis    [Just like Cudd_addMinAbstract, but instead of abstracting the
+ variables in the given cube, picks a unique representative that realizes th
+ minimal function value.]
+ 
+ Description [Returns the resulting ADD if successful; NULL otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addMaxAbstractRepresentative]
+ 
+ Note: Added by Christian Dehnert 8/5/14
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addMinAbstractRepresentative(
+                                  DdManager * manager,
+                                  DdNode * f,
+                                  DdNode * cube)
+{
+    DdNode *res;
+    
+    if (addCheckPositiveCube(manager, cube) == 0) {
+        (void) fprintf(manager->err,"Error: Can only abstract cubes");
+        return(NULL);
+    }
+    
+    do {
+        manager->reordered = 0;
+        res = cuddAddMinAbstractRepresentativeRecur(manager, f, cube);
+    } while (manager->reordered == 1);
+    return(res);
+    
+} /* end of Cudd_addMinRepresentative */
+
+/**Function********************************************************************
+ 
+ Synopsis    [Just like Cudd_addMaxAbstract, but instead of abstracting the
+ variables in the given cube, picks a unique representative that realizes th
+ maximal function value.]
+ 
+ Description [Returns the resulting ADD if successful; NULL otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addMinAbstractRepresentative]
+ 
+ Note: Added by Christian Dehnert 8/5/14
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addMaxAbstractRepresentative(
+                                  DdManager * manager,
+                                  DdNode * f,
+                                  DdNode * cube)
+{
+    DdNode *res;
+    
+    if (addCheckPositiveCube(manager, cube) == 0) {
+        (void) fprintf(manager->err,"Error: Can only abstract cubes");
+        return(NULL);
+    }
+    
+    do {
+        manager->reordered = 0;
+        res = cuddAddMaxAbstractRepresentativeRecur(manager, f, cube);
+    } while (manager->reordered == 1);
+    return(res);
+    
+} /* end of Cudd_addMaxRepresentative */
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/
@@ -809,6 +881,374 @@ cuddAddMaxAbstractRecur(
 /* Definition of static functions                                            */
 /*---------------------------------------------------------------------------*/
 
+/**Function********************************************************************
+ 
+ Synopsis    [Performs the recursive step of Cudd_addMinAbstractRepresentative.]
+ 
+ Description [Performs the recursive step of Cudd_addMinAbstractRepresentative.
+ Returns the ADD obtained by picking a representative over the variables in
+ the given cube for all other valuations. Returns the resulting ADD if successful;
+ NULL otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     []
+ 
+ ******************************************************************************/
+DdNode *
+cuddAddMinAbstractRepresentativeRecur(
+                                      DdManager * manager,
+                                      DdNode * f,
+                                      DdNode * cube)
+{
+    DdNode	*T, *E, *res, *res1, *res2, *zero, *one, *res1Inf, *res2Inf, *left, *right, *tmp, *tmp2;
+    
+    zero = DD_ZERO(manager);
+    one = DD_ONE(manager);
+    
+    /* Cube is guaranteed to be a cube at this point. */
+    if (cuddIsConstant(f)) {
+        if (cuddIsConstant(cube)) {
+            return(one);
+        } else {
+            return(cube);
+        }
+    }
+    
+    /* Abstract a variable that does not appear in f. */
+    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
+        res = cuddAddMinAbstractRepresentativeRecur(manager, f, cuddT(cube));
+        if (res == NULL) {
+            return(NULL);
+        }
+        
+        // Fill in the missing variables to make representative unique. Set the "non-used-branch" to infinity, otherwise
+        // this may interfere with the minimum calculation.
+        cuddRef(res);
+        cuddRef(zero);
+        res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
+        if (res1 == NULL) {
+            Cudd_RecursiveDeref(manager,res);
+            Cudd_RecursiveDeref(manager,zero);
+            return(NULL);
+        }
+        Cudd_RecursiveDeref(manager, res);
+        cuddDeref(zero);
+       	return(res1);
+    }
+    
+    if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) {
+        return(res);
+    }
+    
+    
+    E = cuddE(f);
+    T = cuddT(f);
+    
+    /* If the two indices are the same, so are their levels. */
+    if (f->index == cube->index) {
+        res1 = cuddAddMinAbstractRepresentativeRecur(manager, E, cuddT(cube));
+        if (res1 == NULL) {
+            return(NULL);
+        }
+        cuddRef(res1);
+        
+        res2 = cuddAddMinAbstractRepresentativeRecur(manager, T, cuddT(cube));
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager, res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        
+        left = cuddAddMinAbstractRecur(manager, E, cuddT(cube));
+        if (left == NULL) {
+            Cudd_RecursiveDeref(manager, res1);
+            Cudd_RecursiveDeref(manager, res2);
+            return(NULL);
+        }
+        cuddRef(left);
+        right = cuddAddMinAbstractRecur(manager, T, cuddT(cube));
+        if (right == NULL) {
+            Cudd_RecursiveDeref(manager, res1);
+            Cudd_RecursiveDeref(manager, res2);
+            Cudd_RecursiveDeref(manager, left);
+            return(NULL);
+        }
+        cuddRef(right);
+        
+        tmp = cuddAddApplyRecur(manager, Cudd_addLessThanEquals, left, right);
+        if (tmp == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            Cudd_RecursiveDeref(manager,left);
+            Cudd_RecursiveDeref(manager,right);
+            return(NULL);
+        }
+        cuddRef(tmp);
+        
+        Cudd_RecursiveDeref(manager, left);
+        Cudd_RecursiveDeref(manager, right);
+        
+        cuddRef(zero);
+        res1Inf = cuddAddIteRecur(manager, tmp, res1, zero);
+        if (res1Inf == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            Cudd_RecursiveDeref(manager,tmp);
+            cuddDeref(zero);
+            return(NULL);
+        }
+        cuddRef(res1Inf);
+        Cudd_RecursiveDeref(manager,res1);
+        cuddDeref(zero);
+        
+        tmp2 = cuddAddCmplRecur(manager,tmp);
+        if (tmp2 == NULL) {
+            Cudd_RecursiveDeref(manager,res2);
+            Cudd_RecursiveDeref(manager,left);
+            Cudd_RecursiveDeref(manager,right);
+            Cudd_RecursiveDeref(manager,tmp);
+            return(NULL);
+        }
+        cuddRef(tmp2);
+        Cudd_RecursiveDeref(manager,tmp);
+        
+        cuddRef(zero);
+        res2Inf = cuddAddIteRecur(manager, tmp2, res2, zero);
+        if (res2Inf == NULL) {
+            Cudd_RecursiveDeref(manager,res2);
+            Cudd_RecursiveDeref(manager,res1Inf);
+            Cudd_RecursiveDeref(manager,tmp2);
+            cuddDeref(zero);
+            return(NULL);
+        }
+        cuddRef(res2Inf);
+        Cudd_RecursiveDeref(manager,res2);
+        Cudd_RecursiveDeref(manager,tmp2);
+        cuddDeref(zero);
+        
+        res = (res1Inf == res2Inf) ? res1Inf : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1Inf);
+            Cudd_RecursiveDeref(manager,res2Inf);
+            return(NULL);
+        }
+        cuddRef(res);
+        Cudd_RecursiveDeref(manager,res1Inf);
+        Cudd_RecursiveDeref(manager,res2Inf);
+        cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res);
+        cuddDeref(res);
+        return(res);
+    }
+    else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
+        res1 = cuddAddMinAbstractRepresentativeRecur(manager, E, cube);
+        if (res1 == NULL) return(NULL);
+        cuddRef(res1);
+        res2 = cuddAddMinAbstractRepresentativeRecur(manager, T, cube);
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, res2, res1);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            return(NULL);
+        }
+        cuddDeref(res1);
+        cuddDeref(res2);
+        cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res);
+        return(res);
+    }
+    
+} /* end of cuddAddMinAbstractRepresentativeRecur */
+
+/**Function********************************************************************
+ 
+ Synopsis    [Performs the recursive step of Cudd_addMaxAbstractRepresentative.]
+ 
+ Description [Performs the recursive step of Cudd_addMaxAbstractRepresentative.
+ Returns the ADD obtained by picking a representative over the variables in
+ the given cube for all other valuations. Returns the resulting ADD if successful;
+ NULL otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     []
+ 
+ ******************************************************************************/
+DdNode *
+cuddAddMaxAbstractRepresentativeRecur(
+                                      DdManager * manager,
+                                      DdNode * f,
+                                      DdNode * cube)
+{
+    DdNode	*T, *E, *res, *res1, *res2, *zero, *one, *res1Inf, *res2Inf, *left, *right, *tmp, *tmp2;
+    
+    zero = DD_ZERO(manager);
+    one = DD_ONE(manager);
+    
+    /* Cube is guaranteed to be a cube at this point. */
+    if (cuddIsConstant(f)) {
+        if (cuddIsConstant(cube)) {
+            return(one);
+        } else {
+            return(cube);
+        }
+    }
+    
+    /* Abstract a variable that does not appear in f. */
+    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
+        res = cuddAddMaxAbstractRepresentativeRecur(manager, f, cuddT(cube));
+        
+        if (res == NULL) {
+            return(NULL);
+        }
+        
+        // Fill in the missing variables to make representative unique.
+        cuddRef(res);
+        cuddRef(zero);
+        res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
+        if (res1 == NULL) {
+            Cudd_RecursiveDeref(manager, res);
+            Cudd_RecursiveDeref(manager,zero);
+            return(NULL);
+        }
+        Cudd_RecursiveDeref(manager,res);
+        Cudd_RecursiveDeref(manager,zero);
+       	return(res1);
+    }
+    
+    if ((res = cuddCacheLookup2(manager, Cudd_addMaxAbstractRepresentative, f, cube)) != NULL) {
+        return(res);
+    }
+    
+    
+    E = cuddE(f);
+    T = cuddT(f);
+    
+    /* If the two indices are the same, so are their levels. */
+    if (f->index == cube->index) {
+        res1 = cuddAddMaxAbstractRepresentativeRecur(manager, E, cuddT(cube));
+        if (res1 == NULL) {
+            return(NULL);
+        }
+        cuddRef(res1);
+        
+        res2 = cuddAddMaxAbstractRepresentativeRecur(manager, T, cuddT(cube));
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager, res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        
+        left = cuddAddMaxAbstractRecur(manager, E, cuddT(cube));
+        if (left == NULL) {
+            Cudd_RecursiveDeref(manager, res1);
+            Cudd_RecursiveDeref(manager, res2);
+            return(NULL);
+        }
+        cuddRef(left);
+        right = cuddAddMaxAbstractRecur(manager, T, cuddT(cube));
+        if (right == NULL) {
+            Cudd_RecursiveDeref(manager, res1);
+            Cudd_RecursiveDeref(manager, res2);
+            Cudd_RecursiveDeref(manager, left);
+            return(NULL);
+        }
+        cuddRef(right);
+        
+        tmp = cuddAddApplyRecur(manager, Cudd_addGreaterThanEquals, left, right);
+        if (tmp == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            Cudd_RecursiveDeref(manager,left);
+            Cudd_RecursiveDeref(manager,right);
+            return(NULL);
+        }
+        cuddRef(tmp);
+        
+        Cudd_RecursiveDeref(manager, left);
+        Cudd_RecursiveDeref(manager, right);
+        
+        cuddRef(zero);
+        res1Inf = cuddAddIteRecur(manager, tmp, res1, zero);
+        if (res1Inf == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            Cudd_RecursiveDeref(manager,tmp);
+            cuddDeref(zero);
+            return(NULL);
+        }
+        cuddRef(res1Inf);
+        Cudd_RecursiveDeref(manager,res1);
+        cuddDeref(zero);
+        
+        tmp2 = cuddAddCmplRecur(manager,tmp);
+        if (tmp2 == NULL) {
+            Cudd_RecursiveDeref(manager,res2);
+            Cudd_RecursiveDeref(manager,left);
+            Cudd_RecursiveDeref(manager,right);
+            Cudd_RecursiveDeref(manager,tmp);
+            return(NULL);
+        }
+        cuddRef(tmp2);
+        Cudd_RecursiveDeref(manager,tmp);
+        
+        cuddRef(zero);
+        res2Inf = cuddAddIteRecur(manager, tmp2, res2, zero);
+        if (res2Inf == NULL) {
+            Cudd_RecursiveDeref(manager,res2);
+            Cudd_RecursiveDeref(manager,res1Inf);
+            Cudd_RecursiveDeref(manager,tmp2);
+            cuddDeref(zero);
+            return(NULL);
+        }
+        cuddRef(res2Inf);
+        Cudd_RecursiveDeref(manager,res2);
+        Cudd_RecursiveDeref(manager,tmp2);
+        cuddDeref(zero);
+        
+        res = (res1Inf == res2Inf) ? res1Inf : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1Inf);
+            Cudd_RecursiveDeref(manager,res2Inf);
+            return(NULL);
+        }
+        cuddRef(res);
+        Cudd_RecursiveDeref(manager,res1Inf);
+        Cudd_RecursiveDeref(manager,res2Inf);
+        cuddCacheInsert2(manager, Cudd_addMaxAbstractRepresentative, f, cube, res);
+        cuddDeref(res);
+        return(res);
+    }
+    else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
+        res1 = cuddAddMaxAbstractRepresentativeRecur(manager, E, cube);
+        if (res1 == NULL) return(NULL);
+        cuddRef(res1);
+        res2 = cuddAddMaxAbstractRepresentativeRecur(manager, T, cube);
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        res = (res1 == res2) ? res1 : cuddUniqueInter(manager, (int) f->index, res2, res1);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            return(NULL);
+        }
+        cuddDeref(res1);
+        cuddDeref(res2);
+        cuddCacheInsert2(manager, Cudd_addMaxAbstractRepresentative, f, cube, res);
+        return(res);
+    }
+} /* end of cuddAddMaxAbstractRepresentativeRecur */
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
 
 /**Function********************************************************************
 

resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h

@@ -1002,6 +1002,8 @@ extern DdNode * cuddAddUnivAbstractRecur (DdManager *manager, DdNode *f, DdNode
 extern DdNode * cuddAddOrAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddMinAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddMaxAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
+extern DdNode * cuddAddMinAbstractRepresentativeRecur (DdManager *manager, DdNode *f, DdNode *cube);
+extern DdNode * cuddAddMaxAbstractRepresentativeRecur (DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddApplyRecur (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
 extern DdNode * cuddAddMonadicApplyRecur (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
 extern DdNode * cuddAddScalarInverseRecur (DdManager *dd, DdNode *f, DdNode *epsilon);

resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc

@@ -2423,6 +2423,24 @@ ADD::MaxAbstract(const ADD& cube) const
     return ADD(p, result);
 } // ADD::MaxAbstract
 
+ADD
+ADD::MinAbstractRepresentative(const ADD& cube) const
+{
+    DdManager *mgr = checkSameManager(cube);
+    DdNode *result = Cudd_addMinAbstractRepresentative(mgr, node, cube.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+} // ADD::MinRepresentative
+
+ADD
+ADD::MaxAbstractRepresentative(const ADD& cube) const
+{
+    DdManager *mgr = checkSameManager(cube);
+    DdNode *result = Cudd_addMaxAbstractRepresentative(mgr, node, cube.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+} // ADD::MaxRepresentative
+
 ADD
 ADD::Plus(
   const ADD& g) const

resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh

@@ -376,6 +376,8 @@ public:
     ADD OrAbstract(const ADD& cube) const;
     ADD MinAbstract(const ADD& cube) const;
     ADD MaxAbstract(const ADD& cube) const;
+    ADD MinAbstractRepresentative(const ADD& cube) const;
+    ADD MaxAbstractRepresentative(const ADD& cube) const;
     ADD Plus(const ADD& g) const;
     ADD Times(const ADD& g) const;
     ADD Threshold(const ADD& g) const;

src/storage/dd/CuddAdd.cpp

@@ -242,6 +242,38 @@ namespace storm {
             return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().MaxAbstract(cubeDd.toAdd().getCuddAdd()), newMetaVariables);
         }
         
+        Add<DdType::CUDD> Add<DdType::CUDD>::minAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const {
+            Bdd<DdType::CUDD> cubeDd = this->getDdManager()->getBddOne();
+            
+            std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
+            for (auto const& metaVariable : metaVariables) {
+                // First check whether the DD contains the meta variable and erase it, if this is the case.
+                STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD.");
+                newMetaVariables.erase(metaVariable);
+                
+                DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+                cubeDd &= ddMetaVariable.getCube();
+            }
+
+            return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().MinAbstractRepresentative(cubeDd.toAdd().getCuddAdd()), newMetaVariables);
+        }
+        
+        Add<DdType::CUDD> Add<DdType::CUDD>::maxAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const {
+            Bdd<DdType::CUDD> cubeDd = this->getDdManager()->getBddOne();
+            
+            std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
+            for (auto const& metaVariable : metaVariables) {
+                // First check whether the DD contains the meta variable and erase it, if this is the case.
+                STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD.");
+                newMetaVariables.erase(metaVariable);
+                
+                DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+                cubeDd &= ddMetaVariable.getCube();
+            }
+            
+            return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().MaxAbstractRepresentative(cubeDd.toAdd().getCuddAdd()), newMetaVariables);
+        }
+        
         bool Add<DdType::CUDD>::equalModuloPrecision(Add<DdType::CUDD> const& other, double precision, bool relative) const {
             if (relative) {
                 return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision);

src/storage/dd/CuddAdd.h

@@ -309,6 +309,28 @@ namespace storm {
              */
             Add<DdType::CUDD> maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
             
+            /*!
+             * Computes a DD in which each concrete valuation of the meta variables not in the given set is associated
+             * with exactly one valuation of the meta variables in the given set that realizes the minimal function
+             * value (for the valuation of meta variables not in the given set).
+             *
+             * @param metaVariables The set of meta variables for which to pick unique representatives (that achieve the
+             * minimal function value).
+             * @return The resulting DD.
+             */
+            Add<DdType::CUDD> minAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const;
+            
+            /*!
+             * Computes a DD in which each concrete valuation of the meta variables not in the given set is associated
+             * with exactly one valuation of the meta variables in the given set that realizes the maximal function
+             * value (for the valuation of meta variables not in the given set).
+             *
+             * @param metaVariables The set of meta variables for which to pick unique representatives (that achieve the
+             * maximal function value).
+             * @return The resulting DD.
+             */
+            Add<DdType::CUDD> maxAbstractRepresentative(std::set<storm::expressions::Variable> const& metaVariables) const;
+            
             /*!
              * Checks whether the current and the given ADD represent the same function modulo some given precision.
              *