RegionConstraintChecker.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <optional>
#include <ostream>
#include <string>
#include <vector>
 
#include "storm-pars/storage/ParameterRegion.h"
#include "storm/analysis/GraphConditions.h"
#include "storm/solver/SmtSolver.h"
#include "storm/storage/expressions/Expression.h"
 
namespace storm::pars::analysis {
 
using RationalFunctionRegion = storm::storage::ParameterRegion<storm::RationalFunction>;
using CoefficientType = RationalFunctionRegion::CoefficientType;

using ConstraintVerdict = storm::solver::SmtSolver::CheckResult;

struct RegionWitness : RationalFunctionRegion::Valuation {
    RegionWitness() = default;
    explicit RegionWitness(RationalFunctionRegion::Valuation valuation) : RationalFunctionRegion::Valuation(std::move(valuation)) {}
};

std::ostream& operator<<(std::ostream& out, RegionWitness const& witness);
 
struct RegionCheckResult {
    ConstraintVerdict verdict = ConstraintVerdict::Unknown;

    std::optional<RegionWitness> witness;

    std::optional<storm::expressions::Expression> violatedConstraint;

    std::vector<storm::expressions::Expression> undecidedConstraints;
 
    bool holdsThroughout() const {
        return verdict == ConstraintVerdict::Sat;
    }
};

class RegionConstraintChecker {
   public:
    explicit RegionConstraintChecker(storm::analysis::ConstraintCollector const& collector);
 
    RegionCheckResult checkWellformedness(RationalFunctionRegion const& region) const;

    RegionCheckResult checkGraphPreservation(RationalFunctionRegion const& region) const;

    bool isWellDefined(RationalFunctionRegion const& region) const;

    bool isGraphPreserving(RationalFunctionRegion const& region) const;

    static RegionCheckResult checkConstraints(storm::analysis::ConstraintCollector::ConstraintSet const& constraints, RationalFunctionRegion const& region,
                                              std::string const& label);
 
   private:
    storm::analysis::ConstraintCollector const& collector;
};
 
}  // namespace storm::pars::analysis