AbstractEquationSolver.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <chrono>
#include <iostream>
#include <memory>
 
#include "storm/solver/SolutionBounds.h"
#include "storm/solver/SolverStatus.h"
#include "storm/solver/TerminationCondition.h"
#include "storm/utility/ProgressMeasurement.h"
 
namespace storm {
namespace solver {
 
template<typename SolutionType>
class AbstractEquationSolver {
   public:
    AbstractEquationSolver();

    void setShowProgress(bool verbose, uint64_t delay = 5);

    void setTerminationCondition(std::unique_ptr<TerminationCondition<SolutionType>> terminationCondition);

    void resetTerminationCondition();

    bool hasCustomTerminationCondition() const;

    bool terminateNow(std::vector<SolutionType> const& values, SolverGuarantee const& guarantee) const;

    bool hasRelevantValues() const;

    storm::storage::BitVector const& getRelevantValues() const;
    boost::optional<storm::storage::BitVector> const& getOptionalRelevantValues() const;

    void setRelevantValues(storm::storage::BitVector&& valuesOfInterest);

    void setRelevantValues(storm::storage::BitVector const& valuesOfInterest);

    void clearRelevantValues();
 
    enum class BoundType { Global, Local, Any };

    bool hasLowerBound(BoundType const& type = BoundType::Any) const;

    bool hasUpperBound(BoundType const& type = BoundType::Any) const;

    void setLowerBound(SolutionType const& value);

    void setUpperBound(SolutionType const& value);

    void setBounds(SolutionType const& lower, SolutionType const& upper);

    SolutionType const& getLowerBound() const;

    SolutionType const& getLowerBound(uint64_t const& index) const;

    SolutionType getLowerBound(bool convertLocalBounds) const;

    SolutionType const& getUpperBound() const;

    SolutionType const& getUpperBound(uint64_t const& index) const;

    SolutionType getUpperBound(bool convertLocalBounds) const;

    std::vector<SolutionType> const& getLowerBounds() const;

    std::vector<SolutionType> const& getUpperBounds() const;

    void setLowerBounds(std::vector<SolutionType> const& values);

    void setLowerBounds(std::vector<SolutionType>&& values);

    void setUpperBounds(std::vector<SolutionType> const& values);

    void setUpperBounds(std::vector<SolutionType>&& values);

    void setBounds(std::vector<SolutionType> const& lower, std::vector<SolutionType> const& upper);
 
    void setBoundsFromOtherSolver(AbstractEquationSolver<SolutionType> const& other);

    void clearBounds();

    bool hasSolutionLowerBounds() const;
    bool hasSolutionUpperBounds() const;

    bool hasExactSolutionBounds() const;

    std::vector<SolutionType> const& getSolutionLowerBounds() const;
    std::vector<SolutionType> const& getSolutionUpperBounds() const;

    SolutionBounds<SolutionType> const& getSolutionBounds() const;

    bool isShowProgressSet() const;

    uint64_t getShowProgressDelay() const;

    void startMeasureProgress(uint64_t startingIteration = 0) const;

    void showProgressIterative(uint64_t iterations, boost::optional<uint64_t> const& bound = boost::none) const;
 
   protected:
    TerminationCondition<SolutionType> const& getTerminationCondition() const;
    std::unique_ptr<TerminationCondition<SolutionType>> const& getTerminationConditionPointer() const;

    void setSolutionBounds(SolutionBounds<SolutionType> bounds) const;

    void setSolutionBoundsExact(std::vector<SolutionType> const& x) const;

    void finalizeSolutionBounds(std::vector<SolutionType> const& x) const;

    void clearSolutionBounds() const;

    void setSolutionBoundsFromPrecision(std::vector<SolutionType> const& x, SolutionType const& precision, bool relative) const;
 
    void createUpperBoundsVector(std::vector<SolutionType>& upperBoundsVector) const;
    void createUpperBoundsVector(std::unique_ptr<std::vector<SolutionType>>& upperBoundsVector, uint64_t length) const;
    void createLowerBoundsVector(std::vector<SolutionType>& lowerBoundsVector) const;

    void reportStatus(SolverStatus status, boost::optional<uint64_t> const& iterations = boost::none) const;

    SolverStatus updateStatus(SolverStatus status, std::vector<SolutionType> const& x, SolverGuarantee const& guarantee, uint64_t iterations,
                              uint64_t maximalNumberOfIterations) const;

    SolverStatus updateStatus(SolverStatus status, bool earlyTermination, uint64_t iterations, uint64_t maximalNumberOfIterations) const;
 
    // A termination condition to be used (can be unset).
    std::unique_ptr<TerminationCondition<SolutionType>> terminationCondition;
 
    // A bit vector containing the indices of the relevant values if they were set.
    boost::optional<storm::storage::BitVector> relevantValues;
 
    // A lower bound if one was set.
    boost::optional<SolutionType> lowerBound;
 
    // An upper bound if one was set.
    boost::optional<SolutionType> upperBound;
 
    // Lower bounds if they were set.
    boost::optional<std::vector<SolutionType>> lowerBounds;
 
    // Lower bounds if they were set.
    boost::optional<std::vector<SolutionType>> upperBounds;
 
   private:
    // Sound bounds on the solution, if the last call to this solver produced any.
    mutable SolutionBounds<SolutionType> solutionBounds;
 
    // Indicates the progress of this solver.
    mutable boost::optional<storm::utility::ProgressMeasurement> progressMeasurement;
};
 
}  // namespace solver
}  // namespace storm