21 std::string
const& constantDefinitionString) {
22 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
23 std::set<storm::expressions::Variable> definedConstants;
25 if (!constantDefinitionString.empty()) {
28 std::vector<std::string> definitions;
29 boost::split(definitions, constantDefinitionString, boost::is_any_of(
","));
30 for (
auto& definition : definitions) {
31 boost::trim(definition);
34 std::size_t positionOfAssignmentOperator = definition.find(
'=');
35 STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::WrongFormatException,
36 "Illegal constant definition string: syntax error.");
39 std::string constantName = definition.substr(0, positionOfAssignmentOperator);
40 boost::trim(constantName);
41 std::string value = definition.substr(positionOfAssignmentOperator + 1);
45 if (manager.hasVariable(constantName)) {
47 auto const& variable = manager.getVariable(constantName);
48 STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::WrongFormatException,
49 "Illegally trying to define constant '" << constantName <<
"' twice.");
50 definedConstants.insert(variable);
52 if (manager.hasVariable(value)) {
53 auto const& valueVariable = manager.getVariable(value);
55 variable.getType() == valueVariable.getType(), storm::exceptions::WrongFormatException,
56 "Illegally trying to define constant '" << constantName <<
"' by constant '" << valueVariable.getName() <<
" of different type.");
57 constantDefinitions[variable] = valueVariable.getExpression();
58 }
else if (variable.hasBooleanType()) {
59 if (value ==
"true") {
60 constantDefinitions[variable] = manager.boolean(
true);
61 }
else if (value ==
"false") {
62 constantDefinitions[variable] = manager.boolean(
false);
64 throw storm::exceptions::WrongFormatException() <<
"Illegal value for boolean constant: " << value <<
".";
66 }
else if (variable.hasIntegerType()) {
67 int_fast64_t integerValue = std::stoll(value);
68 constantDefinitions[variable] = manager.integer(integerValue);
69 }
else if (variable.hasRationalType()) {
71 storm::RationalNumber rationalValue = storm::utility::convertNumber<storm::RationalNumber>(value);
72 constantDefinitions[variable] = manager.rational(rationalValue);
73 }
catch (std::exception& e) {
75 "Illegal constant definition string '" << constantName <<
"=" << value <<
"': " << e.what());
80 "Illegal constant definition string: unknown undefined constant '" << constantName <<
"'.");
85 return constantDefinitions;