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

Refactor.

Browse Source
This commit is contained in:
chriseth 2022-02-03 11:41:55 +01:00
parent 6bff7a1e91
commit dec67df8d8
2 changed files with 14 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
libsolutil/LP.cpp
View File

@ -394,6 +394,8 @@ void removeColumns(SolvingState& _state, vector<bool> const& _columnsToRemove)
eraseIndices(_state.variableNames, _columnsToRemove); eraseIndices(_state.variableNames, _columnsToRemove);
} }
// TODO move this into a simplifier class
/// Turn constraints of the form ax <= b into an upper bound on x. /// Turn constraints of the form ax <= b into an upper bound on x.
/// @returns false if the system is infeasible. /// @returns false if the system is infeasible.
bool extractDirectConstraints(SolvingState& _state, bool& _changed) bool extractDirectConstraints(SolvingState& _state, bool& _changed)
@ -416,8 +418,8 @@ bool extractDirectConstraints(SolvingState& _state, bool& _changed)
{ {
// 0 <= b or 0 = b // 0 <= b or 0 = b
if ( if (
constraint.data.factors.front() < 0 || constraint.data.front().numerator() < 0 ||
(constraint.equality && constraint.data.factors.front() != 0) (constraint.equality && constraint.data.front())
) )
return false; // Infeasible. return false; // Infeasible.
} }
@ -468,7 +470,7 @@ bool removeFixedVariables(SolvingState& _state, map<string, rational>& _model, b
// substitute variable // substitute variable
for (Constraint& constraint: _state.constraints) for (Constraint& constraint: _state.constraints)
if (constraint.data.factors.at(index) != 0) if (constraint.data[index])
{ {
constraint.data[0] -= constraint.data[index] * lower; constraint.data[0] -= constraint.data[index] * lower;
constraint.data[index] = 0; constraint.data[index] = 0;
@ -601,7 +603,7 @@ struct ProblemSplitter
Constraint splitRow{{}, state.constraints[i].equality}; Constraint splitRow{{}, state.constraints[i].equality};
for (size_t j = 0; j < state.constraints[i].data.size(); j++) for (size_t j = 0; j < state.constraints[i].data.size(); j++)
if (j == 0 || includedColumns[j]) if (j == 0 || includedColumns[j])
splitRow.data.factors.push_back(state.constraints[i].data[j]); splitRow.data.push_back(state.constraints[i].data[j]);
splitOff.constraints.push_back(move(splitRow)); splitOff.constraints.push_back(move(splitRow));
} }
@ -730,7 +732,7 @@ string SolvingState::toString() const
result += result +=
joinHumanReadable(line, " + ") + joinHumanReadable(line, " + ") +
(constraint.equality ? " = " : " <= ") + (constraint.equality ? " = " : " <= ") +
::toString(constraint.data.factors.front()) + ::toString(constraint.data.front()) +
"\n"; "\n";
} }
result += "Bounds:\n"; result += "Bounds:\n";
@ -779,9 +781,8 @@ pair<LPResult, map<string, rational>> LPSolver::check(SolvingState _state)
else else
{ {
LinearExpression objectives; LinearExpression objectives;
objectives.factors = objectives.resize(1);
vector<rational>(1, rational(bigint(0))) + objectives.resize(split.constraints.front().data.size(), rational(bigint(1)));
vector<rational>(split.constraints.front().data.size() - 1, rational(bigint(1)));
tie(lpResult, solution) = simplex(split.constraints, move(objectives)); tie(lpResult, solution) = simplex(split.constraints, move(objectives));
} }
m_cache.emplace(move(orig), make_pair(lpResult, solution)); m_cache.emplace(move(orig), make_pair(lpResult, solution));

6
libsolutil/LinearExpression.h
View File

@ -41,8 +41,9 @@ using rational = boost::rational<bigint>;
* factors[0] + factors[1] * X1 + factors[2] * X2 + ... * factors[0] + factors[1] * X1 + factors[2] * X2 + ...
* The set and order of variables is implied. * The set and order of variables is implied.
*/ */
struct LinearExpression class LinearExpression
{ {
public:
/// Creates the expression "_factor * X_index" /// Creates the expression "_factor * X_index"
static LinearExpression factorForVariable(size_t _index, rational _factor) static LinearExpression factorForVariable(size_t _index, rational _factor)
{ {
@ -74,6 +75,8 @@ struct LinearExpression
auto begin() const { return factors.begin(); } auto begin() const { return factors.begin(); }
auto end() const { return factors.end(); } auto end() const { return factors.end(); }
rational const& front() const { return factors.front(); }
void push_back(rational _value) { factors.push_back(move(_value)); } void push_back(rational _value) { factors.push_back(move(_value)); }
size_t size() const { return factors.size(); } size_t size() const { return factors.size(); }
@ -169,6 +172,7 @@ struct LinearExpression
return _x; return _x;
} }
private:
std::vector<rational> factors; std::vector<rational> factors;
}; };