diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index b3c7480e0..1aad4651d 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -133,12 +133,20 @@ namespace storm { // Create a new backtracking point before adding the constraint. smtSolver->push(); - // Then add the constraint. - std::vector result = constraint.toExpression(globalExpressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap); + // Create the constraint. + std::pair, std::unordered_map> result = constraint.toExpression(globalExpressionInformation.getManager()); - for (auto const& expression : result) { + // Then add the constraint. + for (auto const& expression : result.first) { smtSolver->add(expression); } + + // Finally associate the level variables with the predicates. + for (auto const& indexVariablePair : result.second) { + auto predicateIt = ddInformation.bddVariableIndexToPredicateMap.find(indexVariablePair.first); + STORM_LOG_ASSERT(predicateIt != ddInformation.bddVariableIndexToPredicateMap.end(), "Missing predicate for DD variable."); + smtSolver->add(storm::expressions::iff(indexVariablePair.second, predicateIt->second)); + } } template diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 7e767c044..0e64d80a8 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -269,8 +269,8 @@ namespace storm { } template - std::vector Bdd::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map const& indexToExpressionMap) const { - return internalBdd.toExpression(manager, indexToExpressionMap); + std::pair, std::unordered_map> Bdd::toExpression(storm::expressions::ExpressionManager& manager) const { + return internalBdd.toExpression(manager); } template diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index 5d529890d..7b59be347 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -289,11 +289,10 @@ namespace storm { * Translates the function the BDD is representing to a set of expressions that characterize the function. * * @param manager The manager that is used to build the expression and, in particular, create new variables in. - * @param indexToExpressionMap A mapping from indices (of DD variables) to expressions with which they are - * to be replaced. - * @return A list of expressions representing the function of the BDD. + * @return A list of expressions representing the function of the BDD and a mapping of DD variable indices to + * the variables that represent these variables in the expressions. */ - std::vector toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map const& indexToExpressionMap) const; + std::pair, std::unordered_map> toExpression(storm::expressions::ExpressionManager& manager) const; virtual Bdd getSupport() const override; diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 3953c488e..776a5e903 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -416,8 +416,8 @@ namespace storm { } } - std::vector InternalBdd::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map const& indexToExpressionMap) const { - std::vector result; + std::pair, std::unordered_map> InternalBdd::toExpression(storm::expressions::ExpressionManager& manager) const { + std::pair, std::unordered_map> result; // Create (and maintain) a mapping from the DD nodes to a counter that says the how-many-th node (within the // nodes of equal index) the node was. @@ -428,19 +428,19 @@ namespace storm { bool negated = Cudd_Regular(this->getCuddDdNode()) != this->getCuddDdNode(); // Translate from the top node downwards. - storm::expressions::Variable topVariable = this->toExpressionRec(Cudd_Regular(this->getCuddDdNode()), ddManager->getCuddManager(), manager, result, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); + storm::expressions::Variable topVariable = this->toExpressionRec(Cudd_Regular(this->getCuddDdNode()), ddManager->getCuddManager(), manager, result.first, result.second, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); // Create the final expression. if (negated) { - result.push_back(!topVariable); + result.first.push_back(!topVariable); } else { - result.push_back(topVariable); + result.first.push_back(topVariable); } return result; } - storm::expressions::Variable InternalBdd::toExpressionRec(DdNode const* dd, cudd::Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex, std::unordered_map const& indexToExpressionMap) { + storm::expressions::Variable InternalBdd::toExpressionRec(DdNode const* dd, cudd::Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map& indexToVariableMap, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex) { STORM_LOG_ASSERT(dd == Cudd_Regular(dd), "Expected non-negated BDD node."); // First, try to look up the current node if it's not a terminal node. @@ -453,41 +453,47 @@ namespace storm { } // If the node was not yet encountered, we create a variable and associate it with the appropriate expression. - storm::expressions::Variable newVariable = manager.declareFreshBooleanVariable(); + storm::expressions::Variable newNodeVariable = manager.declareFreshBooleanVariable(); // Since we want to reuse the variable whenever possible, we insert the appropriate entries in the hash table. if (!Cudd_IsConstant_const(dd)) { // If we are dealing with a non-terminal node, we count it as a new node with this index. nodeToCounterMap[dd] = nextCounterForIndex[Cudd_NodeReadIndex(dd)]; - countIndexToVariablePair[std::make_pair(nextCounterForIndex[Cudd_NodeReadIndex(dd)], Cudd_NodeReadIndex(dd))] = newVariable; + countIndexToVariablePair[std::make_pair(nextCounterForIndex[Cudd_NodeReadIndex(dd)], Cudd_NodeReadIndex(dd))] = newNodeVariable; ++nextCounterForIndex[Cudd_NodeReadIndex(dd)]; } else { // If it's a terminal node, it is the one leaf and there's no need to keep track of a counter for this level. nodeToCounterMap[dd] = 0; - countIndexToVariablePair[std::make_pair(0, Cudd_NodeReadIndex(dd))] = newVariable; + countIndexToVariablePair[std::make_pair(0, Cudd_NodeReadIndex(dd))] = newNodeVariable; } // In the terminal case, we can only have a one since we are considering non-negated nodes only. if (dd == Cudd_ReadOne(ddManager.getManager())) { // Push the expression that enforces that the new variable is true. - expressions.push_back(storm::expressions::iff(manager.boolean(true), newVariable)); + expressions.push_back(storm::expressions::iff(manager.boolean(true), newNodeVariable)); } else { // In the non-terminal case, we recursively translate the children nodes and then construct and appropriate ite-expression. DdNode const* t = Cudd_T_const(dd); DdNode const* e = Cudd_E_const(dd); DdNode const* T = Cudd_Regular(t); DdNode const* E = Cudd_Regular(e); - storm::expressions::Variable thenVariable = toExpressionRec(T, ddManager, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); - storm::expressions::Variable elseVariable = toExpressionRec(E, ddManager, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); + storm::expressions::Variable thenVariable = toExpressionRec(T, ddManager, manager, expressions, indexToVariableMap, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); + storm::expressions::Variable elseVariable = toExpressionRec(E, ddManager, manager, expressions, indexToVariableMap, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); // Create the appropriate expression. - auto expressionIt = indexToExpressionMap.find(Cudd_NodeReadIndex(dd)); - STORM_LOG_ASSERT(expressionIt != indexToExpressionMap.end(), "Unable to find expression for variable index."); - expressions.push_back(storm::expressions::iff(newVariable, storm::expressions::ite(expressionIt->second, t == T ? thenVariable : !thenVariable, e == E ? elseVariable : !elseVariable))); + auto indexVariable = indexToVariableMap.find(Cudd_NodeReadIndex(dd)); + storm::expressions::Variable levelVariable; + if (indexVariable == indexToVariableMap.end()) { + levelVariable = manager.declareFreshBooleanVariable(); + indexToVariableMap[Cudd_NodeReadIndex(dd)] = levelVariable; + } else { + levelVariable = indexVariable->second; + } + expressions.push_back(storm::expressions::iff(newNodeVariable, storm::expressions::ite(levelVariable, t == T ? thenVariable : !thenVariable, e == E ? elseVariable : !elseVariable))); } // Return the variable for this node. - return newVariable; + return newNodeVariable; } template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 1556235ef..7d70ce848 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -353,11 +353,10 @@ namespace storm { * Translates the function the BDD is representing to a set of expressions that characterize the function. * * @param manager The manager that is used to build the expression and, in particular, create new variables in. - * @param indexToExpressionMap A mapping from indices (of DD variables) to expressions with which they are - * to be replaced. - * @return A list of expressions that is equivalent to the function represented by the BDD. + * @return A list of expressions representing the function of the BDD and a mapping of DD variable indices to + * the variables that represent these variables in the expressions. */ - std::vector toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map const& indexToExpressionMap) const; + std::pair, std::unordered_map> toExpression(storm::expressions::ExpressionManager& manager) const; /*! * Creates an ODD based on the current BDD. @@ -471,6 +470,9 @@ namespace storm { * @param dd The current node of the BDD. * @param ddManager The manager responsible for the BDD. * @param manager The expression manager over which to build the expressions. + * @param expressions The list of expressions to fill during the translation. + * @param indexToVariableMap A mapping of variable indices to expression variables that are associated with + * the respective node level of the BDD. * @param countIndexToVariablePair A mapping of (count, variable index) pairs to a pair of expression variables * such that entry (i, j) is mapped to a variable that represents the i-th node labeled with variable j (counting * from left to right). @@ -478,9 +480,8 @@ namespace storm { * visited with the same variable index as the given node. * @param nextCounterForIndex A vector storing a mapping from variable indices to a counter that indicates * how many nodes with the given variable index have been seen before. - * @param indexToExpressionMap A mapping of variable indices to the expressions they are to be replaced with. */ - static storm::expressions::Variable toExpressionRec(DdNode const* dd, cudd::Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex, std::unordered_map const& indexToExpressionMap); + static storm::expressions::Variable toExpressionRec(DdNode const* dd, cudd::Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map& indexToVariableMap, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex); InternalDdManager const* ddManager; diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 421f6798e..9e9c8c7b3 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -389,8 +389,8 @@ namespace storm { } } - std::vector InternalBdd::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map const& indexToExpressionMap) const { - std::vector result; + std::pair, std::unordered_map> InternalBdd::toExpression(storm::expressions::ExpressionManager& manager) const { + std::pair, std::unordered_map> result; // Create (and maintain) a mapping from the DD nodes to a counter that says the how-many-th node (within the // nodes of equal index) the node was. @@ -401,19 +401,19 @@ namespace storm { bool negated = bdd_isnegated(this->getSylvanBdd().GetBDD()); // Translate from the top node downwards. - storm::expressions::Variable topVariable = this->toExpressionRec(bdd_regular(this->getSylvanBdd().GetBDD()), manager, result, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); + storm::expressions::Variable topVariable = this->toExpressionRec(bdd_regular(this->getSylvanBdd().GetBDD()), manager, result.first, result.second, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); // Create the final expression. if (negated) { - result.push_back(!topVariable); + result.first.push_back(!topVariable); } else { - result.push_back(topVariable); + result.first.push_back(topVariable); } return result; } - storm::expressions::Variable InternalBdd::toExpressionRec(BDD dd, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex, std::unordered_map const& indexToExpressionMap) { + storm::expressions::Variable InternalBdd::toExpressionRec(BDD dd, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map& indexToVariableMap, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex) { STORM_LOG_ASSERT(!bdd_isnegated(dd), "Expected non-negated BDD node."); // First, try to look up the current node if it's not a terminal node. @@ -426,26 +426,26 @@ namespace storm { } // If the node was not yet encountered, we create a variable and associate it with the appropriate expression. - storm::expressions::Variable newVariable = manager.declareFreshBooleanVariable(); + storm::expressions::Variable newNodeVariable = manager.declareFreshBooleanVariable(); // Since we want to reuse the variable whenever possible, we insert the appropriate entries in the hash table. if (!bdd_isterminal(dd)) { // If we are dealing with a non-terminal node, we count it as a new node with this index. nodeToCounterMap[dd] = nextCounterForIndex[sylvan_var(dd)]; - countIndexToVariablePair[std::make_pair(nextCounterForIndex[sylvan_var(dd)], sylvan_var(dd))] = newVariable; + countIndexToVariablePair[std::make_pair(nextCounterForIndex[sylvan_var(dd)], sylvan_var(dd))] = newNodeVariable; ++nextCounterForIndex[sylvan_var(dd)]; } else { // If it's a terminal node, it is the one leaf and there's no need to keep track of a counter for this level. nodeToCounterMap[dd] = 0; - countIndexToVariablePair[std::make_pair(0, sylvan_var(dd))] = newVariable; + countIndexToVariablePair[std::make_pair(0, sylvan_var(dd))] = newNodeVariable; } // In the terminal case, we can only have a one since we are considering non-negated nodes only. if (bdd_isterminal(dd)) { if (dd == sylvan_true) { - expressions.push_back(storm::expressions::iff(manager.boolean(true), newVariable)); + expressions.push_back(storm::expressions::iff(manager.boolean(true), newNodeVariable)); } else { - expressions.push_back(storm::expressions::iff(manager.boolean(false), newVariable)); + expressions.push_back(storm::expressions::iff(manager.boolean(false), newNodeVariable)); } } else { // In the non-terminal case, we recursively translate the children nodes and then construct and appropriate ite-expression. @@ -453,17 +453,24 @@ namespace storm { BDD e = sylvan_low(dd); BDD T = bdd_regular(t); BDD E = bdd_regular(e); - storm::expressions::Variable thenVariable = toExpressionRec(T, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); - storm::expressions::Variable elseVariable = toExpressionRec(E, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap); + storm::expressions::Variable thenVariable = toExpressionRec(T, manager, expressions, indexToVariableMap, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); + storm::expressions::Variable elseVariable = toExpressionRec(E, manager, expressions, indexToVariableMap, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex); // Create the appropriate expression. - auto expressionIt = indexToExpressionMap.find(sylvan_var(dd)); - STORM_LOG_ASSERT(expressionIt != indexToExpressionMap.end(), "Unable to find expression for variable index."); - expressions.push_back(storm::expressions::iff(newVariable, storm::expressions::ite(expressionIt->second, t == T ? thenVariable : !thenVariable, e == E ? elseVariable : !elseVariable))); + // Create the appropriate expression. + auto indexVariable = indexToVariableMap.find(sylvan_var(dd)); + storm::expressions::Variable levelVariable; + if (indexVariable == indexToVariableMap.end()) { + levelVariable = manager.declareFreshBooleanVariable(); + indexToVariableMap[sylvan_var(dd)] = levelVariable; + } else { + levelVariable = indexVariable->second; + } + expressions.push_back(storm::expressions::iff(newNodeVariable, storm::expressions::ite(levelVariable, t == T ? thenVariable : !thenVariable, e == E ? elseVariable : !elseVariable))); } // Return the variable for this node. - return newVariable; + return newNodeVariable; } template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h index d0c781a1b..f99e13c98 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -342,11 +342,10 @@ namespace storm { * Translates the function the BDD is representing to a set of expressions that characterize the function. * * @param manager The manager that is used to build the expression and, in particular, create new variables in. - * @param indexToExpressionMap A mapping from indices (of DD variables) to expressions with which they are - * to be replaced. - * @return A list of expressions representing the function of the BDD. + * @return A list of expressions representing the function of the BDD and a mapping of DD variable indices to + * the variables that represent these variables in the expressions. */ - std::vector toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map const& indexToExpressionMap) const; + std::pair, std::unordered_map> toExpression(storm::expressions::ExpressionManager& manager) const; /*! * Creates an ODD based on the current BDD. @@ -441,6 +440,9 @@ namespace storm { * * @param dd The current node of the BDD. * @param manager The expression manager over which to build the expressions. + * @param expressions The list of expressions to fill during the translation. + * @param indexToVariableMap A mapping of variable indices to expression variables that are associated with + * the respective node level of the BDD. * @param countIndexToVariablePair A mapping of (count, variable index) pairs to a pair of expression variables * such that entry (i, j) is mapped to a variable that represents the i-th node labeled with variable j (counting * from left to right). @@ -448,9 +450,8 @@ namespace storm { * visited with the same variable index as the given node. * @param nextCounterForIndex A vector storing a mapping from variable indices to a counter that indicates * how many nodes with the given variable index have been seen before. - * @param indexToExpressionMap A mapping of variable indices to the expressions they are to be replaced with. */ - static storm::expressions::Variable toExpressionRec(BDD dd, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex, std::unordered_map const& indexToExpressionMap); + static storm::expressions::Variable toExpressionRec(BDD dd, storm::expressions::ExpressionManager& manager, std::vector& expressions, std::unordered_map& indexToVariableMap, std::unordered_map, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map& nodeToCounterMap, std::vector& nextCounterForIndex); /*! * Retrieves the sylvan BDD. diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index beea61e70..695d247e2 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -424,12 +424,5 @@ TEST(CuddDd, BddToExpressionTest) { storm::expressions::Variable c = manager->declareBooleanVariable("c"); storm::expressions::Variable d = manager->declareBooleanVariable("d"); - std::unordered_map indexToExpressionMap; - indexToExpressionMap[0] = c; - indexToExpressionMap[2] = d; - auto result = bdd.toExpression(*manager, indexToExpressionMap); - - for (auto const& expression : result) { - std::cout << expression << std::endl; - } + auto result = bdd.toExpression(*manager); } \ No newline at end of file diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 025ce8227..386501de3 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -426,12 +426,5 @@ TEST(SylvanDd, BddToExpressionTest) { storm::expressions::Variable c = manager->declareBooleanVariable("c"); storm::expressions::Variable d = manager->declareBooleanVariable("d"); - std::unordered_map indexToExpressionMap; - indexToExpressionMap[0] = c; - indexToExpressionMap[2] = d; - auto result = bdd.toExpression(*manager, indexToExpressionMap); - - for (auto const& expression : result) { - std::cout << expression << std::endl; - } + auto result = bdd.toExpression(*manager); } \ No newline at end of file