ValidBlockAbstractor.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <functional>
#include <memory>
#include <vector>
 
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/DdType.h"
 
#include "storm-gamebased-ar/abstraction/LocalExpressionInformation.h"
 
#include "storm/solver/SmtSolver.h"
 
namespace storm {
namespace utility {
namespace solver {
class SmtSolverFactory;
}
}  // namespace utility
}  // namespace storm
 
namespace storm::gbar {
namespace abstraction {
 
template<storm::dd::DdType DdType>
class AbstractionInformation;
 
template<storm::dd::DdType DdType>
class ValidBlockAbstractor {
   public:
    ValidBlockAbstractor(AbstractionInformation<DdType>& abstractionInformation,
                         std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory);
 
    storm::dd::Bdd<DdType> const& getValidBlocks();
 
    void refine(std::vector<uint64_t> const& predicates);
 
    void constrain(storm::expressions::Expression const& constraint);
 
   private:
    void recomputeValidBlocks();
 
    void recomputeValidBlocksForPredicateBlock(uint64_t blockIndex);
 
    AbstractionInformation<DdType> const& getAbstractionInformation() const;
 
    storm::dd::Bdd<DdType> getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, uint64_t blockIndex) const;
 
    std::reference_wrapper<AbstractionInformation<DdType> const> abstractionInformation;
 
    LocalExpressionInformation<DdType> localExpressionInformation;
 
    storm::dd::Bdd<DdType> validBlocks;
 
    std::vector<std::unique_ptr<storm::solver::SmtSolver>> smtSolvers;
 
    std::vector<std::vector<std::pair<storm::expressions::Variable, uint64_t>>> relevantVariablesAndPredicates;
 
    std::vector<std::vector<storm::expressions::Variable>> decisionVariables;
 
    std::vector<storm::dd::Bdd<DdType>> validBlocksForPredicateBlocks;
 
    bool checkForRecomputation;
};
 
}  // namespace abstraction
}  // namespace storm::gbar