From 65b1636867ddc5a417afce8fe29ae497e1c172ea Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 24 Mar 2022 00:27:54 +0100
Subject: [PATCH] Share ground state.

---
 libsolutil/LP.cpp | 20 ++++++++++----------
 libsolutil/LP.h   |  5 ++++-
 2 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp
index 70fa94c66..50569f297 100644
--- a/libsolutil/LP.cpp
+++ b/libsolutil/LP.cpp
@@ -798,22 +798,22 @@ LPSolver::LPSolver(bool)
 LPResult LPSolver::setState(SolvingState _state)
 {
 	//cout << "Set state:\n" << _state.toString() << endl;
-	m_state = move(_state);
+	m_state = make_shared<SolvingState>(move(_state));
 	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));
-	m_subProblemsPerConstraint.resize(m_state.constraints.size(), static_cast<size_t>(-1));
-
-	normalizeRowLengths(m_state);
-	auto&& [result, modelOrReasonSet] = SolvingStateSimplifier(m_state).simplify();
+	normalizeRowLengths(*m_state);
+	auto&& [result, modelOrReasonSet] = SolvingStateSimplifier(*m_state).simplify();
 	if (result == LPResult::Infeasible)
 		return result;
+
 	// 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.
 	m_fixedVariables = std::get<decltype(m_fixedVariables)>(modelOrReasonSet);
 
 	//cout << "Splitting..." << endl;
-	ProblemSplitter splitter(m_state);
+	ProblemSplitter splitter(*m_state);
 	while (splitter)
 	{
 		auto&& [variables, constraints] = splitter.next();
@@ -985,13 +985,13 @@ SolvingState LPSolver::stateFromSubProblem(size_t _index) const
 	SubProblem const& problem = *m_subProblems[_index];
 	for (size_t varIndex: problem.variables)
 	{
-		split.variableNames.emplace_back(m_state.variableNames[varIndex]);
-		split.bounds.emplace_back(m_state.bounds[varIndex]);
+		split.variableNames.emplace_back(m_state->variableNames[varIndex]);
+		split.bounds.emplace_back(m_state->bounds[varIndex]);
 	}
 	for (auto&& item: m_subProblemsPerConstraint | ranges::views::enumerate)
 		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};
 			splitRow.data.push_back(constraint.data.get(0));
 			for (size_t varIndex: problem.variables)
diff --git a/libsolutil/LP.h b/libsolutil/LP.h
index 02f067a47..8c144363d 100644
--- a/libsolutil/LP.h
+++ b/libsolutil/LP.h
@@ -192,7 +192,10 @@ private:
 	void addConstraintToSubProblem(size_t _subProblem, Constraint _constraint);
 	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
 	{
 		// TODO now we could actually put the constraints here again.