3#include <boost/algorithm/string.hpp>
4#include <boost/lexical_cast.hpp>
15template<
typename ValueType>
16ValueParser<ValueType>::ParametricData::ParametricData()
18 parser(
std::make_unique<ExpressionParser>(*
manager)),
21 parser->setIdentifierMapping(identifierMapping);
24template<
typename ValueType>
25ValueParser<ValueType>::ParametricData::~ParametricData() =
default;
27template<
typename ValueType>
29 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Parameters are not supported in this build (Have you checked storm-pars?).");
35 data.identifierMapping.emplace(var.
getName(), var);
36 data.parser->setIdentifierMapping(data.identifierMapping);
44 return rationalFunction;
47template<
typename ValueType>
49 return parseNumber<ValueType>(value);
52template<
typename NumberType>
56 STORM_LOG_THROW(
false, storm::exceptions::WrongFormatException,
"Could not parse value '" << value <<
"' into " <<
typeid(NumberType).name() <<
".");
62 if (boost::conversion::try_lexical_convert(value, result)) {
66 storm::RationalNumber rationalResult;
68 result = storm::utility::convertNumber<double>(rationalResult);
77 if (
double pointResult;
parseNumber(value, pointResult)) {
82 std::string intermediate = value;
83 boost::trim(intermediate);
84 carl::BoundType leftBound;
85 carl::BoundType rightBound;
86 if (intermediate.front() ==
'(') {
87 leftBound = carl::BoundType::STRICT;
88 }
else if (intermediate.front() ==
'[') {
89 leftBound = carl::BoundType::WEAK;
93 if (intermediate.back() ==
')') {
94 rightBound = carl::BoundType::STRICT;
95 }
else if (intermediate.back() ==
']') {
96 rightBound = carl::BoundType::WEAK;
100 intermediate = intermediate.substr(1, intermediate.size() - 2);
102 std::vector<std::string> words;
103 boost::split(words, intermediate, boost::is_any_of(
","));
104 if (words.size() != 2) {
107 double leftVal, rightVal;
108 boost::trim(words[0]);
112 boost::trim(words[1]);
120template<
typename NumberType>
122 if constexpr (std::is_same_v<NumberType, double>) {
124 }
else if constexpr (std::is_same_v<NumberType, storm::RationalNumber>) {
125 return carl::try_parse(value, result);
126 }
else if constexpr (std::is_same_v<NumberType, storm::Interval>) {
129 return boost::conversion::try_lexical_convert(value, result);
134template class ValueParser<double>;
135template class ValueParser<storm::RationalNumber>;
136template class ValueParser<storm::RationalFunction>;
137template class ValueParser<storm::Interval>;
139template std::size_t parseNumber<std::size_t>(std::string
const&);
Variable declareRationalVariable(std::string const &name, bool auxiliary=false)
Declares a new rational variable with a name that must not yet exist and its corresponding type.
std::string const & getName() const
Retrieves the name of the variable.
Parser for values according to their ValueType.
#define STORM_LOG_TRACE(message)
#define STORM_LOG_THROW(cond, exception, message)
NumberType parseNumber(std::string const &value)
Parse number from string.
bool parseDouble(std::string const &value, double &result)
bool parseInterval(std::string const &value, storm::Interval &result)
SettingsManager const & manager()
Retrieves the settings manager.
carl::Interval< double > Interval
carl::RationalFunction< Polynomial, true > RationalFunction