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

Use names for the bounds.

Browse Source
This commit is contained in:
chriseth 2022-02-02 14:48:01 +01:00
parent 751f50b6c3
commit 7a250fea42
3 changed files with 38 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
libsolutil/LP.cpp
View File

@ -309,32 +309,33 @@ bool boundsToConstraints(SolvingState& _state)
size_t columns = _state.variableNames.size(); size_t columns = _state.variableNames.size();
// Turn bounds into constraints. // Turn bounds into constraints.
// Bound zero should not exist because the variable zero does not exist.
for (auto const& [index, bounds]: _state.bounds | ranges::views::enumerate | ranges::views::tail) for (auto const& [index, bounds]: _state.bounds | ranges::views::enumerate | ranges::views::tail)
{ {
if (bounds[0] && bounds[1]) if (bounds.lower && bounds.upper)
{ {
if (*bounds[0] > *bounds[1]) if (*bounds.lower > *bounds.upper)
return false; return false;
if (*bounds[0] == *bounds[1]) if (*bounds.lower == *bounds.upper)
{ {
vector<rational> c(columns); vector<rational> c(columns);
c[0] = *bounds[0]; c[0] = *bounds.lower;
c[index] = bigint(1); c[index] = bigint(1);
_state.constraints.emplace_back(Constraint{move(c), true}); _state.constraints.emplace_back(Constraint{move(c), true});
continue; continue;
} }
} }
if (bounds[0] && *bounds[0] > 0) if (bounds.lower && *bounds.lower > 0)
{ {
vector<rational> c(columns); vector<rational> c(columns);
c[0] = -*bounds[0]; c[0] = -*bounds.lower;
c[index] = bigint(-1); c[index] = bigint(-1);
_state.constraints.emplace_back(Constraint{move(c), false}); _state.constraints.emplace_back(Constraint{move(c), false});
} }
if (bounds[1]) if (bounds.upper)
{ {
vector<rational> c(columns); vector<rational> c(columns);
c[0] = *bounds[1]; c[0] = *bounds.upper;
c[index] = bigint(1); c[index] = bigint(1);
_state.constraints.emplace_back(Constraint{move(c), false}); _state.constraints.emplace_back(Constraint{move(c), false});
} }
@ -395,15 +396,15 @@ bool extractDirectConstraints(SolvingState& _state, bool& _changed)
rational bound = constraint.data[0] / factor; rational bound = constraint.data[0] / factor;
if ( if (
(factor >= 0 || constraint.equality) && (factor >= 0 || constraint.equality) &&
(!_state.bounds[varIndex][1] || bound < _state.bounds[varIndex][1]) (!_state.bounds[varIndex].upper || bound < _state.bounds[varIndex].upper)
) )
_state.bounds[varIndex][1] = bound; _state.bounds[varIndex].upper = bound;
if ( if (
(factor <= 0 || constraint.equality) && (factor <= 0 || constraint.equality) &&
(!_state.bounds[varIndex][0] || bound > _state.bounds[varIndex][0]) (!_state.bounds[varIndex].lower || bound > _state.bounds[varIndex].lower)
) )
// Lower bound must be at least zero. // Lower bound must be at least zero.
_state.bounds[varIndex][0] = max(rational{}, bound); _state.bounds[varIndex].lower = max(rational{}, bound);
} }
} }
if (needsRemoval) if (needsRemoval)
@ -419,11 +420,11 @@ bool removeFixedVariables(SolvingState& _state, map<string, rational>& _model, b
// Remove variables that have equal lower and upper bound. // Remove variables that have equal lower and upper bound.
for (auto const& [index, bounds]: _state.bounds | ranges::views::enumerate) for (auto const& [index, bounds]: _state.bounds | ranges::views::enumerate)
{ {
if (!bounds[1] || (!bounds[0] && bounds[1]->numerator() > 0)) if (!bounds.upper || (!bounds.lower && bounds.upper->numerator() > 0))
continue; continue;
// Lower bound must be at least zero. // Lower bound must be at least zero.
rational lower = max(rational{}, bounds[0] ? *bounds[0] : rational{}); rational lower = max(rational{}, bounds.lower ? *bounds.lower : rational{});
rational upper = *bounds[1]; rational upper = *bounds.upper;
if (upper < lower) if (upper < lower)
return false; // Infeasible. return false; // Infeasible.
if (upper != lower) if (upper != lower)
@ -464,12 +465,12 @@ bool removeEmptyColumns(SolvingState& _state, map<string, rational>& _model, boo
{ {
variablesToRemove[i] = true; variablesToRemove[i] = true;
needsRemoval = true; needsRemoval = true;
// TODO actually it is unbounded if _state.bounds.at(i)[1] is nullopt. // TODO actually it is unbounded if _state.bounds.at(i).upper is nullopt.
if (_state.bounds.at(i)[0] || _state.bounds.at(i)[1]) if (_state.bounds.at(i).lower || _state.bounds.at(i).upper)
_model[_state.variableNames.at(i)] = _model[_state.variableNames.at(i)] =
_state.bounds.at(i)[1] ? _state.bounds.at(i).upper ?
*_state.bounds.at(i)[1] : *_state.bounds.at(i).upper :
*_state.bounds.at(i)[0]; *_state.bounds.at(i).lower;
} }
if (needsRemoval) if (needsRemoval)
{ {
@ -702,13 +703,13 @@ string SolvingState::toString() const
result += "Bounds:\n"; result += "Bounds:\n";
for (auto&& [index, bounds]: bounds | ranges::views::enumerate) for (auto&& [index, bounds]: bounds | ranges::views::enumerate)
{ {
if (!bounds[0] && !bounds[1]) if (!bounds.lower && !bounds.upper)
continue; continue;
if (bounds[0]) if (bounds.lower)
result += ::toString(*bounds[0]) + " <= "; result += ::toString(*bounds.lower) + " <= ";
result += variableNames.at(index); result += variableNames.at(index);
if (bounds[1]) if (bounds.upper)
result += " <= " + ::toString(*bounds[1]); result += " <= " + ::toString(*bounds.upper);
result += "\n"; result += "\n";
} }
return result; return result;

13
libsolutil/LP.h
View File

@ -48,11 +48,18 @@ struct Constraint
*/ */
struct SolvingState struct SolvingState
{ {
/// Names of variables, the index zero should be left empty. /// Names of variables, the index zero should be left empty
/// TODO can we change that? /// (because zero corresponds to constants).
std::vector<std::string> variableNames; std::vector<std::string> variableNames;
struct Bounds
{
std::optional<rational> lower;
std::optional<rational> upper;
bool operator<(Bounds const& _other) const { return make_pair(lower, upper) < make_pair(_other.lower, _other.upper); }
bool operator==(Bounds const& _other) const { return make_pair(lower, upper) == make_pair(_other.lower, _other.upper); }
};
/// Lower and upper bounds for variables (in the sense of >= / <=). /// Lower and upper bounds for variables (in the sense of >= / <=).
std::vector<std::array<std::optional<boost::rational<bigint>>, 2>> bounds; std::vector<Bounds> bounds;
std::vector<Constraint> constraints; std::vector<Constraint> constraints;
bool operator<(SolvingState const& _other) const; bool operator<(SolvingState const& _other) const;

4
test/libsolutil/LP.cpp
View File

@ -77,7 +77,7 @@ public:
size_t index = variableIndex(_variable); size_t index = variableIndex(_variable);
if (index >= m_solvingState.bounds.size()) if (index >= m_solvingState.bounds.size())
m_solvingState.bounds.resize(index + 1); m_solvingState.bounds.resize(index + 1);
m_solvingState.bounds.at(index)[0] = _value; m_solvingState.bounds.at(index).lower = _value;
} }
void addUpperBound(string _variable, rational _value) void addUpperBound(string _variable, rational _value)
@ -85,7 +85,7 @@ public:
size_t index = variableIndex(_variable); size_t index = variableIndex(_variable);
if (index >= m_solvingState.bounds.size()) if (index >= m_solvingState.bounds.size())
m_solvingState.bounds.resize(index + 1); m_solvingState.bounds.resize(index + 1);
m_solvingState.bounds.at(index)[1] = _value; m_solvingState.bounds.at(index).upper = _value;
} }
void feasible(vector<pair<string, rational>> const& _solution) void feasible(vector<pair<string, rational>> const& _solution)