From 690ddb54f1660e4c587b5ed095b48171ad5c15f6 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Mon, 29 Aug 2022 12:14:43 +0200
Subject: [PATCH] Recommended polarity callback.

---
 libsolutil/BooleanLP.cpp     | 23 ++++++++++++++++++++---
 libsolutil/CDCL.cpp          | 28 +++++++++++++++++++---------
 libsolutil/CDCL.h            |  4 +++-
 libsolutil/LPIncremental.cpp |  8 ++++++++
 libsolutil/LPIncremental.h   |  2 ++
 5 files changed, 52 insertions(+), 13 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 09eb5d183..d405b943e 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -109,11 +109,11 @@ void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _s
 
 pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> const&)
 {
-#ifdef DEBUG
+//#ifdef DEBUG
 	cerr << "Solving boolean constraint system" << endl;
 	cerr << toString() << endl;
 	cerr << "--------------" << endl;
-#endif
+//#endif
 
 	if (state().infeasible)
 	{
@@ -156,7 +156,15 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 	// Is it even a problem if the indices overlap?
 	for (auto&& [name, index]: state().variables)
 		if (state().isBooleanVariable.at(index) || isConditionalConstraint(index))
-			resizeAndSet(booleanVariables, index, name);
+		{
+			string innerName = name;
+			if (isConditionalConstraint(index))
+			{
+				innerName = toString(state().conditionalConstraints.at(index));
+				cerr << " - set name to " << innerName << endl;
+			}
+			resizeAndSet(booleanVariables, index, innerName);
+		}
 		else
 			lpSolver.setVariableName(index, name);
 
@@ -224,6 +232,15 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
 #endif
 	};
 
+	auto constraintIndication = [&](size_t _variable)
+	{
+#if LPIncremental
+		lpSolver.recommendedPolarity(_variable);
+#else
+		return std::nullopt;
+#endif
+	};
+
 	auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver, backtrackNotify}.solve();
 	if (!optionalModel)
 	{
diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp
index 70770420f..ef99f732d 100644
--- a/libsolutil/CDCL.cpp
+++ b/libsolutil/CDCL.cpp
@@ -33,10 +33,12 @@ CDCL::CDCL(
 	vector<string> _variables,
 	vector<Clause> const& _clauses,
 	std::function<std::optional<Clause>(size_t, std::map<size_t, bool> const&)> _theorySolver,
-	std::function<void(size_t)> _backtrackNotify
+	std::function<void(size_t)> _backtrackNotify,
+	std::function<std::optional<bool>(size_t)> _constraintIndication
 ):
 	m_theorySolver(_theorySolver),
 	m_backtrackNotify(_backtrackNotify),
+	m_constraintIndication(_constraintIndication),
 	m_variables(move(_variables)),
 	m_order(VarOrderLt(m_activity))
 {
@@ -114,16 +116,24 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
 		{
 			if (auto variable = nextDecisionVariable())
 			{
-// 				cout << "c Level " << currentDecisionLevel() << " - ";
-// 				cout << ((m_assignments.size() * 100) / m_variables.size()) << "% of variables assigned." << endl;
+				cerr << "c Level " << currentDecisionLevel() << " - ";
+				cerr << ((m_assignments.size() * 100) / m_variables.size()) << "% of variables assigned." << endl;
 				m_decisionPoints.emplace_back(m_assignmentTrail.size());
-//				cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl;
+				cerr << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl;
 
-				// Polarity caching below
-				bool positive = false;
-				auto const& found = m_assignments_cache.find(*variable);
-				if (found != m_assignments_cache.end()) positive = found->second;
-				enqueue(Literal{positive, *variable}, nullptr);
+				optional<bool> guess;
+				if (m_constraintIndication)
+					guess = m_constraintIndication(*variable);
+
+				if (!guess)
+				{
+					// Polarity caching below
+					bool positive = false;
+					auto const& found = m_assignments_cache.find(*variable);
+					if (found != m_assignments_cache.end()) positive = found->second;
+					guess = positive;
+				}
+				enqueue(Literal{*guess, *variable}, nullptr);
 			}
 			else
 			{
diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h
index f96fe93a3..b59434fc7 100644
--- a/libsolutil/CDCL.h
+++ b/libsolutil/CDCL.h
@@ -60,7 +60,8 @@ public:
 		std::vector<std::string> _variables,
 		std::vector<Clause> const& _clauses,
 		std::function<std::optional<Clause>(size_t, std::map<size_t, bool> const&)> _theorySolver = {},
-		std::function<void(size_t)> _backtrackNotify = {}
+		std::function<void(size_t)> _backtrackNotify = {},
+		std::function<std::optional<bool>(size_t)> _constraintIndication = {}
 	);
 
 	std::optional<Model> solve();
@@ -105,6 +106,7 @@ private:
 	/// or a conflict clause, i.e. a clauses that is false in the theory with the given assignments.
 	std::function<std::optional<Clause>(size_t, std::map<size_t, bool>)> m_theorySolver;
 	std::function<void(size_t)> m_backtrackNotify;
+	std::function<std::optional<bool>(size_t)> m_constraintIndication;
 
 	std::vector<std::string> m_variables;
 	/// includes the learnt clauses
diff --git a/libsolutil/LPIncremental.cpp b/libsolutil/LPIncremental.cpp
index 6604ba5d2..9dc54b6a8 100644
--- a/libsolutil/LPIncremental.cpp
+++ b/libsolutil/LPIncremental.cpp
@@ -263,7 +263,15 @@ void LPSolver::setVariableName(size_t, string)
 }
 #endif
 
+optional<bool> LPSolver::recommendedPolarity(size_t _reason) const
+{
+	if (!reasonToBounds.count(_reason))
+		return {};
+	return {};
+//	TODO: We cannot actually have a negative polarity for a reason / constraint!
+//	We can recommend not to activate it, though...
 
+}
 
 pair<LPResult, ReasonSet> LPSolver::check()
 {
diff --git a/libsolutil/LPIncremental.h b/libsolutil/LPIncremental.h
index 0216c9a79..e6a7a5471 100644
--- a/libsolutil/LPIncremental.h
+++ b/libsolutil/LPIncremental.h
@@ -167,6 +167,8 @@ public:
 
 	void setVariableName(size_t _variable, std::string _name);
 
+	std::optional<bool> recommendedPolarity(size_t _reason) const;
+
 	std::pair<LPResult, ReasonSet> check();
 
 	std::string toString() const;