From 6f9dd7107d77b2c5e931698bd4064737fe753112 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 1 May 2014 14:14:25 +0200
Subject: [PATCH] Added universal abstraction function to DD layer.

Former-commit-id: 56e5d62b5a780a138ebbfb4276012153d27517e1
---
 src/storage/dd/CuddDd.cpp | 17 +++++++++++++++++
 src/storage/dd/CuddDd.h   |  7 +++++++
 2 files changed, 24 insertions(+)

diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index bbce93902..72abb87bf 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -184,6 +184,23 @@ namespace storm {
             this->cuddAdd = this->cuddAdd.OrAbstract(cubeDd.getCuddAdd());
         }
         
+        void Dd<DdType::CUDD>::universalAbstract(std::set<std::string> const& metaVariableNames) {
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+            
+            for (auto const& metaVariableName : metaVariableNames) {
+                // First check whether the DD contains the meta variable and erase it, if this is the case.
+                if (!this->containsMetaVariable(metaVariableName)) {
+                    throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD.";
+                }
+                this->getContainedMetaVariableNames().erase(metaVariableName);
+                
+                DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName);
+                cubeDd *= metaVariable.getCube();
+            }
+            
+            this->cuddAdd = this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd());
+        }
+        
         void Dd<DdType::CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) {
             Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
             
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 6c7bffd6a..f345c28a2 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -233,6 +233,13 @@ namespace storm {
              */
             void existsAbstract(std::set<std::string> const& metaVariableNames);
             
+            /*!
+             * Universally abstracts from the given meta variables.
+             *
+             * @param metaVariableNames The names of all meta variables from which to abstract.
+             */
+            void universalAbstract(std::set<std::string> const& metaVariableNames);
+            
             /*!
              * Sum-abstracts from the given meta variables.
              *