SolutionBounds.h

Go to the documentation of this file.

#pragma once
 
#include <algorithm>
#include <cstdint>
#include <optional>
#include <type_traits>
#include <vector>
 
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
 
namespace storm::solver {

template<typename ValueType>
struct SolutionBounds {
    std::optional<std::vector<ValueType>> lower;
    std::optional<std::vector<ValueType>> upper;

    bool hasLower() const {
        return lower.has_value();
    }

    bool hasUpper() const {
        return upper.has_value();
    }

    bool hasAny() const {
        return hasLower() || hasUpper();
    }

    bool encloses(std::vector<ValueType> const& values) const {
        auto const isBoundedBy = [&values](std::optional<std::vector<ValueType>> const& bound, bool fromBelow) {
            if (!bound.has_value()) {
                return true;
            }
            if (bound->size() != values.size()) {
                return false;
            }
            for (uint64_t i = 0; i < values.size(); ++i) {
                if (fromBelow ? (*bound)[i] > values[i] : (*bound)[i] < values[i]) {
                    return false;
                }
            }
            return true;
        };
        return isBoundedBy(lower, true) && isBoundedBy(upper, false);
    }

    bool isExact() const {
        return hasLower() && hasUpper() && *lower == *upper;
    }

    bool isWithinPrecision(std::vector<ValueType> const& values, ValueType const& precision, bool relative) const {
        if (!hasLower() || !hasUpper()) {
            return false;
        }
        STORM_LOG_THROW(lower->size() == values.size() && upper->size() == values.size(), storm::exceptions::InvalidArgumentException,
                        "The given values do not match the size of the bounds.");
        ValueType const zero = storm::utility::zero<ValueType>();
        for (uint64_t i = 0; i < values.size(); ++i) {
            ValueType const& low = (*lower)[i];
            ValueType const& up = (*upper)[i];
            ValueType allowed = precision;
            if (relative) {
                // The enclosed value is at least as far from zero as the bound closer to it, unless the two
                // straddle zero, where only coinciding bounds say anything.
                allowed = (low <= zero && up >= zero) ? zero : precision * std::min(storm::utility::abs<ValueType>(low), storm::utility::abs<ValueType>(up));
            }
            // Negated, so that a distance that is not a number is rejected.
            if (!(values[i] - low <= allowed) || !(up - values[i] <= allowed)) {
                return false;
            }
        }
        return true;
    }

    void setExact(std::vector<ValueType> const& values) {
        lower = values;
        upper = values;
    }

    void invertProbabilityBounds() {
        auto const oneMinus = [](ValueType const& value) { return storm::utility::one<ValueType>() - value; };
        if (hasLower()) {
            std::ranges::transform(*lower, lower->begin(), oneMinus);
        }
        if (hasUpper()) {
            std::ranges::transform(*upper, upper->begin(), oneMinus);
        }
        std::swap(lower, upper);
    }

    template<typename Function>
    auto transform(Function const& function) const {
        SolutionBounds<typename std::invoke_result_t<Function, std::vector<ValueType> const&>::value_type> result;
        if (hasLower()) {
            result.lower = function(*lower);
        }
        if (hasUpper()) {
            result.upper = function(*upper);
        }
        return result;
    }

    void widenTo(std::vector<ValueType> const& values) {
        if (hasLower()) {
            std::ranges::transform(*lower, values, lower->begin(), [](ValueType const& bound, ValueType const& value) { return std::min(bound, value); });
        }
        if (hasUpper()) {
            std::ranges::transform(*upper, values, upper->begin(), [](ValueType const& bound, ValueType const& value) { return std::max(bound, value); });
        }
    }

    void clear() {
        lower = std::nullopt;
        upper = std::nullopt;
    }
};
 
}  // namespace storm::solver