11namespace abstraction {
13template<storm::dd::DdType DdType>
15 std::shared_ptr<storm::utility::solver::SmtSolverFactory>
const& smtSolverFactory)
16 : abstractionInformation(abstractionInformation),
17 localExpressionInformation(abstractionInformation),
18 validBlocks(abstractionInformation.getDdManager().getBddOne()),
19 checkForRecomputation(false) {
20 uint64_t numberOfBlocks = localExpressionInformation.getNumberOfBlocks();
21 validBlocksForPredicateBlocks.resize(numberOfBlocks, abstractionInformation.
getDdManager().
getBddOne());
22 relevantVariablesAndPredicates.resize(numberOfBlocks);
23 decisionVariables.resize(numberOfBlocks);
25 for (uint64_t i = 0; i < numberOfBlocks; ++i) {
26 smtSolvers.emplace_back(smtSolverFactory->create(abstractionInformation.
getExpressionManager()));
27 for (
auto const& constraint : abstractionInformation.
getConstraints()) {
28 smtSolvers.back()->add(constraint);
33template<storm::dd::DdType DdType>
35 if (checkForRecomputation) {
36 recomputeValidBlocks();
42template<storm::dd::DdType DdType>
44 for (uint64_t i = 0; i < smtSolvers.size(); ++i) {
45 smtSolvers[i]->add(constraint);
49template<storm::dd::DdType DdType>
51 for (
auto const& predicate : predicates) {
52 std::map<uint64_t, uint64_t> mergeInformation = localExpressionInformation.addExpression(predicate);
55 for (
auto const& blockRemapping : mergeInformation) {
56 if (blockRemapping.first == blockRemapping.second) {
60 validBlocksForPredicateBlocks[blockRemapping.second] = validBlocksForPredicateBlocks[blockRemapping.first];
61 smtSolvers[blockRemapping.second] = std::move(smtSolvers[blockRemapping.first]);
62 relevantVariablesAndPredicates[blockRemapping.second] = std::move(relevantVariablesAndPredicates[blockRemapping.first]);
63 decisionVariables[blockRemapping.second] = std::move(decisionVariables[blockRemapping.first]);
65 validBlocksForPredicateBlocks.resize(localExpressionInformation.getNumberOfBlocks());
66 smtSolvers.resize(localExpressionInformation.getNumberOfBlocks());
67 relevantVariablesAndPredicates.resize(localExpressionInformation.getNumberOfBlocks());
68 decisionVariables.resize(localExpressionInformation.getNumberOfBlocks());
70 checkForRecomputation =
true;
73template<storm::dd::DdType DdType>
77 for (uint64_t blockIndex = 0; blockIndex < localExpressionInformation.getNumberOfBlocks(); ++blockIndex) {
78 std::set<uint64_t>
const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex);
81 if (relevantVariablesAndPredicates[blockIndex].size() < predicateBlock.size()) {
82 recomputeValidBlocksForPredicateBlock(blockIndex);
85 newValidBlocks &= validBlocksForPredicateBlocks[blockIndex];
88 validBlocks = newValidBlocks;
91template<storm::dd::DdType DdType>
92void ValidBlockAbstractor<DdType>::recomputeValidBlocksForPredicateBlock(uint64_t blockIndex) {
93 std::set<uint64_t>
const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex);
94 std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newVariables =
95 this->getAbstractionInformation().declareNewVariables(relevantVariablesAndPredicates[blockIndex], predicateBlock);
96 for (
auto const& element : newVariables) {
97 smtSolvers[blockIndex]->add(
storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second)));
98 decisionVariables[blockIndex].push_back(element.first);
101 relevantVariablesAndPredicates[blockIndex].insert(relevantVariablesAndPredicates[blockIndex].end(), newVariables.begin(), newVariables.end());
102 std::sort(relevantVariablesAndPredicates[blockIndex].begin(), relevantVariablesAndPredicates[blockIndex].end(),
103 [](std::pair<storm::expressions::Variable, uint_fast64_t>
const& first, std::pair<storm::expressions::Variable, uint_fast64_t>
const& second) {
104 return first.second < second.second;
109 uint64_t numberOfSolutions = 0;
110 smtSolvers[blockIndex]->allSat(decisionVariables[blockIndex],
112 result |= getSourceStateBdd(model, blockIndex);
117 STORM_LOG_TRACE(
"Computed valid blocks for predicate block " << blockIndex <<
" (" << numberOfSolutions <<
" solutions enumerated).");
119 validBlocksForPredicateBlocks[blockIndex] = result;
122template<storm::dd::DdType DdType>
123AbstractionInformation<DdType>
const& ValidBlockAbstractor<DdType>::getAbstractionInformation()
const {
124 return abstractionInformation.get();
127template<storm::dd::DdType DdType>
130 for (
auto variableIndexPairIt = relevantVariablesAndPredicates[blockIndex].rbegin(),
131 variableIndexPairIte = relevantVariablesAndPredicates[blockIndex].rend();
132 variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) {
133 auto const& variableIndexPair = *variableIndexPairIt;
135 result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
137 result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
145template class ValidBlockAbstractor<storm::dd::DdType::CUDD>;
146template class ValidBlockAbstractor<storm::dd::DdType::Sylvan>;
bool isZero() const
Retrieves whether this DD represents the constant zero function.
DdManager< LibraryType > & getDdManager() const
Retrieves the manager that is responsible for this DD.
Bdd< LibraryType > getBddOne() const
Retrieves a BDD representing the constant one function.
storm::dd::Bdd< DdType > const & getValidBlocks()
void refine(std::vector< uint64_t > const &predicates)
void constrain(storm::expressions::Expression const &constraint)
ValidBlockAbstractor(AbstractionInformation< DdType > &abstractionInformation, std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory)
The base class for all model references.
virtual bool getBooleanValue(storm::expressions::Variable const &variable) const =0
#define STORM_LOG_TRACE(message)
#define STORM_LOG_ASSERT(cond, message)
Expression iff(Expression const &first, Expression const &second)