started cleaning ADD interface

Former-commit-id: f67fe7cf47

src/builder/DdPrismModelBuilder.cpp

@@ -1033,7 +1033,7 @@ namespace storm {
             
             // If we were asked to treat some states as terminal states, we cut away their transitions now.
             if (options.terminalStates || options.negatedTerminalStates) {
-                storm::dd::Add<Type, ValueType> terminalStatesAdd = generationInfo.manager->template getAddZero<ValueType>();
+                storm::dd::Bdd<Type> terminalStatesBdd = generationInfo.manager->getBddZero();
                 if (options.terminalStates) {
                     storm::expressions::Expression terminalExpression;
                     if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
@@ -1044,7 +1044,7 @@ namespace storm {
                     }
                 
                     STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
-                    terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
+                    terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd();
                 }
                 if (options.negatedTerminalStates) {
                     storm::expressions::Expression nonTerminalExpression;
@@ -1056,10 +1056,10 @@ namespace storm {
                     }
                     
                     STORM_LOG_TRACE("Making the states *not* satisfying " << nonTerminalExpression << " terminal.");
-                    terminalStatesAdd |= !generationInfo.rowExpressionAdapter->translateExpression(nonTerminalExpression);
+                    terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(nonTerminalExpression).toBdd();
                 }
                 
-                transitionMatrix *= !terminalStatesAdd;
+                transitionMatrix *= (!terminalStatesBdd).template toAdd<ValueType>();
             }
             
             // Cut the transitions and rewards to the reachable fragment of the state space.
@@ -1095,7 +1095,10 @@ namespace storm {
                         // For MDPs, however, we need to select an action associated with the self-loop, if we do not
                         // want to attach a lot of self-loops to the deadlock states.
                         storm::dd::Add<Type, ValueType> action = generationInfo.manager->template getAddOne<ValueType>();
-                        std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(), [&action,&generationInfo] (storm::expressions::Variable const& metaVariable) { action *= !generationInfo.manager->template getIdentity<ValueType>(metaVariable); } );
+                        std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(),
+                                      [&action, &generationInfo] (storm::expressions::Variable const& metaVariable) {
+                                          action *= generationInfo.manager->template getIdentity<ValueType>(metaVariable);
+                                      });
                         // Make sure that global variables do not change along the introduced self-loops.
                         for (auto const& var : generationInfo.allGlobalVariables) {
                             action *= generationInfo.variableToIdentityMap.at(var);

src/storage/dd/Add.cpp

@@ -36,10 +36,10 @@ namespace storm {
             return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.ite(thenAdd.internalAdd, elseAdd.internalAdd), metaVariables);
         }
         
-        template<DdType LibraryType, typename ValueType>
-        Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator!() const {
-            return Add<LibraryType, ValueType>(this->getDdManager(), !internalAdd, this->getContainedMetaVariables());
-        }
+//        template<DdType LibraryType, typename ValueType>
+//        Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator!() const {
+//            return Add<LibraryType, ValueType>(this->getDdManager(), !internalAdd, this->getContainedMetaVariables());
+//        }
         
         template<DdType LibraryType, typename ValueType>
         Add<LibraryType, ValueType> Add<LibraryType, ValueType>::operator||(Add<LibraryType, ValueType> const& other) const {

src/storage/dd/Add.h

@@ -81,7 +81,7 @@ namespace storm {
              *
              * @return The resulting ADD.
              */
-            Add<LibraryType, ValueType> operator!() const;
+//            Add<LibraryType, ValueType> operator!() const;
             
             /*!
              * Performs a logical or of the current anBd the given ADD. As a prerequisite, the operand ADDs need to be

test/functional/storage/CuddDdTest.cpp

@@ -113,6 +113,7 @@ TEST(CuddDd, OperatorTest) {
     storm::dd::Add<storm::dd::DdType::CUDD, double> dd1 = manager->template getAddOne<double>();
     storm::dd::Add<storm::dd::DdType::CUDD, double> dd2 = manager->template getAddOne<double>();
     storm::dd::Add<storm::dd::DdType::CUDD, double> dd3 = dd1 + dd2;
+    storm::dd::Bdd<storm::dd::DdType::CUDD> bdd;
     EXPECT_TRUE(dd3 == manager->template getConstant<double>(2));
     
     dd3 += manager->template getAddZero<double>();
@@ -133,14 +134,14 @@ TEST(CuddDd, OperatorTest) {
     dd3 /= manager->template getConstant<double>(2);
     EXPECT_TRUE(dd3.isOne());
     
-    dd3 = !dd3;
-    EXPECT_TRUE(dd3.isZero());
+    bdd = !dd3.toBdd();
+    EXPECT_TRUE(bdd.isZero());
     
-    dd1 = !dd3;
-    EXPECT_TRUE(dd1.isOne());
+    bdd = !bdd;
+    EXPECT_TRUE(bdd.isOne());
 
-    dd3 = dd1 || dd2;
-    EXPECT_TRUE(dd3.isOne());
+    bdd = dd1.toBdd() || dd2.toBdd();
+    EXPECT_TRUE(bdd.isOne());
     
     dd1 = manager->template getIdentity<double>(x.first);
     dd2 = manager->template getConstant<double>(5);