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

Share ground state.

Browse Source
This commit is contained in:
chriseth 2022-03-24 00:27:54 +01:00
parent dd1092fda2
commit 65b1636867
2 changed files with 14 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
libsolutil/LP.cpp
View File

@ -798,22 +798,22 @@ LPSolver::LPSolver(bool)
LPResult LPSolver::setState(SolvingState _state) LPResult LPSolver::setState(SolvingState _state)
{ {
//cout << "Set state:\n" << _state.toString() << endl; //cout << "Set state:\n" << _state.toString() << endl;
m_state = move(_state); m_state = make_shared<SolvingState>(move(_state));
m_subProblems.clear(); m_subProblems.clear();
m_subProblemsPerVariable.resize(m_state->variableNames.size(), static_cast<size_t>(-1));
m_subProblemsPerConstraint.resize(m_state->constraints.size(), static_cast<size_t>(-1));
m_subProblemsPerVariable.resize(m_state.variableNames.size(), static_cast<size_t>(-1)); normalizeRowLengths(*m_state);
m_subProblemsPerConstraint.resize(m_state.constraints.size(), static_cast<size_t>(-1)); auto&& [result, modelOrReasonSet] = SolvingStateSimplifier(*m_state).simplify();
normalizeRowLengths(m_state);
auto&& [result, modelOrReasonSet] = SolvingStateSimplifier(m_state).simplify();
if (result == LPResult::Infeasible) if (result == LPResult::Infeasible)
return result; return result;
// We do not need to store reasons because at this point, we do not have any reasons yet. // We do not need to store reasons because at this point, we do not have any reasons yet.
// We can add this and just need to store the reasons together with the variables. // We can add this and just need to store the reasons together with the variables.
m_fixedVariables = std::get<decltype(m_fixedVariables)>(modelOrReasonSet); m_fixedVariables = std::get<decltype(m_fixedVariables)>(modelOrReasonSet);
//cout << "Splitting..." << endl; //cout << "Splitting..." << endl;
ProblemSplitter splitter(m_state); ProblemSplitter splitter(*m_state);
while (splitter) while (splitter)
{ {
auto&& [variables, constraints] = splitter.next(); auto&& [variables, constraints] = splitter.next();
@ -985,13 +985,13 @@ SolvingState LPSolver::stateFromSubProblem(size_t _index) const
SubProblem const& problem = *m_subProblems[_index]; SubProblem const& problem = *m_subProblems[_index];
for (size_t varIndex: problem.variables) for (size_t varIndex: problem.variables)
{ {
split.variableNames.emplace_back(m_state.variableNames[varIndex]); split.variableNames.emplace_back(m_state->variableNames[varIndex]);
split.bounds.emplace_back(m_state.bounds[varIndex]); split.bounds.emplace_back(m_state->bounds[varIndex]);
} }
for (auto&& item: m_subProblemsPerConstraint | ranges::views::enumerate) for (auto&& item: m_subProblemsPerConstraint | ranges::views::enumerate)
if (item.second == _index) if (item.second == _index)
{ {
Constraint const& constraint = m_state.constraints[item.first]; Constraint const& constraint = m_state->constraints[item.first];
Constraint splitRow{{}, constraint.equality, constraint.reasons}; Constraint splitRow{{}, constraint.equality, constraint.reasons};
splitRow.data.push_back(constraint.data.get(0)); splitRow.data.push_back(constraint.data.get(0));
for (size_t varIndex: problem.variables) for (size_t varIndex: problem.variables)

5
libsolutil/LP.h
View File

@ -192,7 +192,10 @@ private:
void addConstraintToSubProblem(size_t _subProblem, Constraint _constraint); void addConstraintToSubProblem(size_t _subProblem, Constraint _constraint);
void updateSubProblems(); void updateSubProblems();
SolvingState m_state; /// Ground state for CDCL. This is shared by copies of the solver.
/// Only ``setState`` changes the state. Copies will only use
/// ``addConstraint`` which does not change m_state.
std::shared_ptr<SolvingState> m_state;
struct SubProblem struct SubProblem
{ {
// TODO now we could actually put the constraints here again. // TODO now we could actually put the constraints here again.