From f163f9b7cefb6feaa8ff448ac81e09f8c25cb57f Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 21 Mar 2022 18:59:48 +0100
Subject: [PATCH] Improving polarity caching to target phases

---
 libsolutil/CDCL.cpp | 6 +++++-
 libsolutil/CDCL.h   | 1 +
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index 633f3758a..58326a88e 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -293,7 +293,6 @@ void CDCL::enqueue(Literal const& _literal, Clause const* _reason)
 	m_levelForVariable[_literal.variable] = currentDecisionLevel();
 	if (_reason) {
 		m_reason[_literal] = _reason;
-		m_assignments_cache[_literal.variable] = _literal.positive;
 	}
 	m_assignmentTrail.push_back(_literal);
 }
@@ -304,6 +303,11 @@ void CDCL::cancelUntil(size_t _backtrackLevel)
 	//cout << "Canceling until " << _backtrackLevel << endl;
 	solAssert(m_assignmentQueuePointer == m_assignmentTrail.size());
 	size_t assignmentsToUndo = m_assignmentTrail.size() - m_decisionPoints.at(_backtrackLevel);
+	if (m_assignmentTrail.size() > m_longest_trail) {
+		m_assignments_cache= m_assignments;
+		m_longest_trail = m_assignmentTrail.size();
+	}
+
 	for (size_t i = 0; i < assignmentsToUndo; i++)
 	{
 		Literal l = m_assignmentTrail.back();
diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h
index 65cae269e..0c1ac1ccf 100644
--- a/libsolutil/CDCL.h
+++ b/libsolutil/CDCL.h
@@ -154,6 +154,7 @@ private:
 	// TODO group those into a class
 
 	std::vector<Literal> m_assignmentTrail;
+	uint64_t m_longest_trail = 0;
 	/// Indices into assignmentTrail where decisions were taken.
 	std::vector<size_t> m_decisionPoints;
 	/// Index into assignmentTrail: All assignments starting there have not yet been propagated.