From dd1092fda254f7bb69abf9887a364ac8a4867929 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 24 Mar 2022 00:08:28 +0100
Subject: [PATCH] Re-add cache.

---
 libsolutil/BooleanLP.cpp |  2 +-
 libsolutil/BooleanLP.h   |  3 +++
 libsolutil/LP.cpp        | 34 +++++++++++++++++++++++++++-------
 libsolutil/LP.h          |  7 ++++++-
 4 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 974d6fd0a..3fd5a22ea 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -243,7 +243,7 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 	// from previous invocations of the boolean solver, we still have to use
 	// a cache.
 	// The current optimization is only for CDCL.
-	lpSolvers.emplace_back(0, LPSolver{});
+	lpSolvers.emplace_back(0, LPSolver{&m_lpCache});
 	if (
 		lpSolvers.back().second.setState(lpState) == LPResult::Infeasible ||
 		lpSolvers.back().second.check().first == LPResult::Infeasible
diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h
index 879431d31..f4dab298f 100644
--- a/libsolutil/BooleanLP.h
+++ b/libsolutil/BooleanLP.h
@@ -122,6 +122,9 @@ private:
 
 	/// Stack of state, to allow for push()/pop().
 	std::vector<State> m_state{{State{}}};
+
+	std::map<SolvingState, LPResult, SolvingState::Compare> m_lpCache;
+
 };
 
 
diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp
index 97544a5ca..70fa94c66 100644
--- a/libsolutil/LP.cpp
+++ b/libsolutil/LP.cpp
@@ -506,7 +506,7 @@ bool Constraint::operator<(Constraint const& _other) const
 		if (rational diff = data.get(i) - _other.data.get(i))
 			return diff < 0;
 
-	return reasons < _other.reasons;
+	return false;
 }
 
 bool Constraint::operator==(Constraint const& _other) const
@@ -518,7 +518,7 @@ bool Constraint::operator==(Constraint const& _other) const
 		if (data.get(i) != _other.data.get(i))
 			return false;
 
-	return reasons == _other.reasons;
+	return true;
 }
 
 bool SolvingState::Compare::operator()(SolvingState const& _a, SolvingState const& _b) const
@@ -912,12 +912,32 @@ pair<LPResult, variant<Model, ReasonSet>> LPSolver::check()
 		}
 		else
 		{
-			LinearExpression objectives;
-			objectives.resize(1);
-			objectives.resize(state.variableNames.size(), rational(bigint(1)));
-			// TODO the model relies on the variable numbering.
-			tie(problem->result, problem->model) = simplex(state.constraints, move(objectives));
+			optional<LPResult> result;
+			if (m_cache)
+			{
+				auto it = m_cache->find(state);
+				if (it != m_cache->end())
+				{
+					//cout << "Cache hit" << endl;
+					result = it->second;
+				}
+			}
+			if (!result)
+			{
+				LinearExpression objectives;
+				objectives.resize(1);
+				objectives.resize(state.variableNames.size(), rational(bigint(1)));
+				// TODO the model relies on the variable numbering.
+				result = LPResult::Unknown;
+				tie(*result, problem->model) = simplex(state.constraints, move(objectives));
+				if (m_cache)
+				{
+					(*m_cache)[state] = *result;
+					//cout << "Cache size " << m_cache->size() << endl;
+				}
+			}
 			problem->dirty = false;
+			problem->result = *result;
 			if (problem->result == LPResult::Infeasible)
 				return {LPResult::Infeasible, reasonSetForSubProblem(*problem)};
 		}
diff --git a/libsolutil/LP.h b/libsolutil/LP.h
index 5e5562ed1..02f067a47 100644
--- a/libsolutil/LP.h
+++ b/libsolutil/LP.h
@@ -80,7 +80,7 @@ struct SolvingState
 
 	struct Compare
 	{
-		explicit Compare(bool _considerVariableNames = true): considerVariableNames(_considerVariableNames) {}
+		explicit Compare(bool _considerVariableNames = false): considerVariableNames(_considerVariableNames) {}
 		bool operator()(SolvingState const& _a, SolvingState const& _b) const;
 		bool considerVariableNames;
 	};
@@ -179,6 +179,9 @@ class LPSolver
 {
 public:
 	explicit LPSolver(bool _supportModels = true);
+	explicit LPSolver(std::map<SolvingState, LPResult, SolvingState::Compare>* _cache):
+		m_cache(_cache) {}
+
 
 	LPResult setState(SolvingState _state);
 	void addConstraint(Constraint _constraint);
@@ -209,6 +212,8 @@ private:
 	std::vector<size_t> m_subProblemsPerConstraint;
 	/// TODO also store the first infeasible subproblem?
 	/// TODO still retain the cache?
+	std::map<SolvingState, LPResult, SolvingState::Compare>* m_cache = nullptr;
+
 };
 
 }