cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Print reasons.

Browse Source
This commit is contained in:
chriseth 2022-02-17 14:46:46 +01:00
parent 8fbefb9c85
commit 1e1964362c
1 changed files with 19 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
libsolutil/LP.cpp
View File

@ -494,15 +494,26 @@ string toString(rational const& _x)
if (_x.denominator() == 1) if (_x.denominator() == 1)
return ::toString(_x.numerator()); return ::toString(_x.numerator());
else else
return ::toString(_x); return ::toString(_x.numerator()) + "/" + ::toString(_x.denominator());
}
}
namespace
{
string reasonToString(ReasonSet const& _reasons, size_t _minSize)
{
auto reasonsAsStrings = _reasons | ranges::views::transform([](size_t _r) { return to_string(_r); });
string result = "[" + joinHumanReadable(reasonsAsStrings) + "]";
if (result.size() < _minSize)
result.resize(_minSize, ' ');
return result;
} }
} }
string SolvingState::toString() const string SolvingState::toString() const
{ {
size_t const reasonLength = 10;
string result; string result;
// TODO print reasons
for (Constraint const& constraint: constraints) for (Constraint const& constraint: constraints)
{ {
vector<string> line; vector<string> line;
@ -518,6 +529,7 @@ string SolvingState::toString() const
line.emplace_back(mult + variableNames.at(index)); line.emplace_back(mult + variableNames.at(index));
} }
result += result +=
reasonToString(constraint.reasons, reasonLength) +
joinHumanReadable(line, " + ") + joinHumanReadable(line, " + ") +
(constraint.equality ? " = " : " <= ") + (constraint.equality ? " = " : " <= ") +
::toString(constraint.data.front()) + ::toString(constraint.data.front()) +
@ -529,10 +541,12 @@ string SolvingState::toString() const
if (!bounds.lower && !bounds.upper) if (!bounds.lower && !bounds.upper)
continue; continue;
if (bounds.lower) if (bounds.lower)
result += ::toString(*bounds.lower) + " <= "; result +=
reasonToString(bounds.lowerReasons, reasonLength) +
::toString(*bounds.lower) + " <= ";
result += variableNames.at(index); result += variableNames.at(index);
if (bounds.upper) if (bounds.upper)
result += " <= " + ::toString(*bounds.upper); result += " <= "s + ::toString(*bounds.upper) + " " + reasonToString(bounds.upperReasons, 0);
result += "\n"; result += "\n";
} }
return result; return result;