From de338e60dee9066ee4035cb58e613aacfef07afb Mon Sep 17 00:00:00 2001
From: Bhargava Shastry <bhargava.shastry@ethereum.org>
Date: Tue, 1 Mar 2022 10:57:11 +0100
Subject: [PATCH] Rebase on rational solver.

---
 test/libsolutil/LP.cpp                        | 28 ++-----------------
 .../lpsolver/FuzzerSolverInterface.cpp        |  6 ++--
 .../ossfuzz/lpsolver/FuzzerSolverInterface.h  |  9 +++---
 3 files changed, 11 insertions(+), 32 deletions(-)

diff --git a/test/libsolutil/LP.cpp b/test/libsolutil/LP.cpp
index 72c461587..9314e4626 100644
--- a/test/libsolutil/LP.cpp
+++ b/test/libsolutil/LP.cpp
@@ -61,14 +61,9 @@ public:
 		{
 			bool equality = static_cast<bool>(c[0]);
 			vector<int> factors(c.begin() + 1, c.end());
-			m_solvingState.constraints.push_back(
-				{
-					linearExpression(factors),
-					equality
-				}
-			);
-		    auto it = find_if(factors.rbegin(), factors.rend(), [](auto const& _i) { return _i != 0; });
-            size_t numVariablesInConstraint = factors.size() - 1 - static_cast<size_t>(distance(factors.rbegin(), it));
+			m_solvingState.constraints.push_back({linearExpression(factors), equality});
+			auto it = find_if(factors.rbegin(), factors.rend(), [](auto const& _i) { return _i != 0; });
+			size_t numVariablesInConstraint = factors.size() - 1 - static_cast<size_t>(distance(factors.rbegin(), it));
 			if (totalNumVariables < numVariablesInConstraint)
 				totalNumVariables = numVariablesInConstraint;
 		}
@@ -150,14 +145,6 @@ public:
 		BOOST_CHECK_MESSAGE(suppliedReason == _reason, "Reasons are different");
 	}
 
-	void sat()
-	{
-		auto [result, model] = m_solver.check(m_solvingState);
-		for (auto const& [var, value]: model)
-			cout << var << " = " << value << endl;
-		BOOST_REQUIRE(result == LPResult::Feasible);
-	}
-
 protected:
 	size_t variableIndex(string const& _name)
 	{
@@ -179,15 +166,6 @@ protected:
 
 BOOST_FIXTURE_TEST_SUITE(LP, LPTestFramework, *boost::unit_test::label("nooptions"))
 
-BOOST_AUTO_TEST_CASE(fuzzer)
-{
-	auto x = variable("x", -6);
-	auto y = variable("y", -6);
-	// expected result: -6x -6y = 8 is unsat since x >= 0 and y >= 0 are implied
-	addEQConstraint(x + y, constant(8));
-	sat();
-}
-
 BOOST_AUTO_TEST_CASE(fuzzer3)
 {
 	addFuzzerInput(
diff --git a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp
index ee69022ef..940a7c149 100644
--- a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp
+++ b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp
@@ -45,7 +45,9 @@ LinearExpression FuzzerSolverInterface::linearExpression(vector<int> _factors)
 
 void FuzzerSolverInterface::addLPConstraint(pair<bool, vector<int>> _constraint)
 {
-	m_lpSolvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first});
+	m_lpSolvingState.constraints.push_back(
+		{linearExpression(move(_constraint.second)), _constraint.first, {}}
+	);
 }
 
 void FuzzerSolverInterface::addLPVariable(string _varName)
@@ -95,7 +97,7 @@ void FuzzerSolverInterface::addZ3Constraints(vector<pair<bool, vector<int>>> _co
 		addZ3Constraint(c);
 }
 
-solution FuzzerSolverInterface::checkLP()
+Solution FuzzerSolverInterface::checkLP()
 {
 	return m_lpSolver.check(m_lpSolvingState);
 }
diff --git a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h
index 6123ccde1..453bd8256 100644
--- a/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h
+++ b/test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h
@@ -28,10 +28,9 @@
 namespace solidity::test::fuzzer::lpsolver
 {
 
-using solution = std::pair<
-    solidity::util::LPResult,
-	std::map<std::string, solidity::util::rational>
->;
+using Model = std::map<std::string, solidity::util::rational>;
+using ReasonSet = std::set<size_t>;
+using Solution = std::pair<solidity::util::LPResult, std::variant<Model, ReasonSet>>;
 
 class FuzzerSolverInterface
 {
@@ -54,7 +53,7 @@ public:
 	solidity::util::LinearExpression linearExpression(std::vector<int> _factors);
 
 	/// Queries LP solver and @returns solution.
-	solution checkLP();
+	Solution checkLP();
 
 	/// Queries Z3 solver and @returns solution.
 	z3::check_result checkZ3();