Remove unused solving state.

libsolutil/LP.cpp

@@ -77,6 +77,7 @@ string toString(rational const& _x)
 		return ::toString(_x.numerator()) + "/" + ::toString(_x.denominator());
 }
 
+/*
 string reasonToString(ReasonSet const& _reasons, size_t _minSize)
 {
 	auto reasonsAsStrings = _reasons | ranges::views::transform([](size_t _r) { return to_string(_r); });
@@ -85,6 +86,7 @@ string reasonToString(ReasonSet const& _reasons, size_t _minSize)
 		result.resize(_minSize, ' ');
 	return result;
 }
+*/
 
 }
 
@@ -131,73 +133,6 @@ string RationalWithDelta::toString() const
 	return result;
 }
 
-bool SolvingState::Compare::operator()(SolvingState const& _a, SolvingState const& _b) const
-{
-	if (!considerVariableNames || _a.variableNames == _b.variableNames)
-	{
-		if (_a.bounds == _b.bounds)
-			return _a.constraints < _b.constraints;
-		else
-			return _a.bounds < _b.bounds;
-	}
-	else
-		return _a.variableNames < _b.variableNames;
-}
-
-set<size_t> SolvingState::reasons() const
-{
-	set<size_t> ret;
-	for (Bounds const& b: bounds)
-		ret += b.lowerReasons + b.upperReasons;
-	return ret;
-}
-
-string SolvingState::toString() const
-{
-	size_t const reasonLength = 10;
-	string result;
-	for (Constraint const& constraint: constraints)
-	{
-		vector<string> line;
-		for (auto&& [index, multiplier]: constraint.data.enumerate())
-			if (index > 0 && multiplier != 0)
-			{
-				string mult =
-					multiplier == -1 ?
-					"-" :
-					multiplier == 1 ?
-					"" :
-					::toString(multiplier) + " ";
-				line.emplace_back(mult + variableNames.at(index));
-			}
-		result +=
-			joinHumanReadable(line, " + ") +
-			(
-				constraint.kind == Constraint::EQUAL ? "  = " :
-				constraint.kind == Constraint::LESS_OR_EQUAL ? " <= " :
-				" <  "
-			) +
-			::toString(constraint.data.front()) +
-			"\n";
-	}
-	result += "Bounds:\n";
-	for (auto&& [index, bounds]: bounds | ranges::views::enumerate)
-	{
-		if (!bounds.lower && !bounds.upper)
-			continue;
-		if (bounds.lower)
-			result +=
-				reasonToString(bounds.lowerReasons, reasonLength) +
-				bounds.lower->toString() + " <= ";
-		result += variableNames.at(index);
-		if (bounds.upper)
-			result += " <= "s + bounds.upper->toString() + " " + reasonToString(bounds.upperReasons, 0);
-		result += "\n";
-	}
-	return result;
-}
-
-
 void LPSolver::addConstraint(Constraint const& _constraint, optional<size_t> _reason)
 {
 	// TODO at this point, we could also determine if it is a fixed variable.

libsolutil/LP.h

@@ -137,50 +137,6 @@ struct RationalWithDelta
 	rational m_delta;
 };
 
-/**
- * State used when solving an LP problem.
- */
-struct SolvingState
-{
-	/// Names of variables. The index zero should be left empty
-	/// because zero corresponds to constants.
-	std::vector<std::string> variableNames;
-	struct Bounds
-	{
-		std::optional<RationalWithDelta> lower;
-		std::optional<RationalWithDelta> upper;
-		bool operator<(Bounds const& _other) const { return make_pair(lower, upper) < make_pair(_other.lower, _other.upper); }
-		bool operator==(Bounds const& _other) const { return make_pair(lower, upper) == make_pair(_other.lower, _other.upper); }
-
-		// TODO this is currently not used
-
-		/// Set of literals the conjunction of which implies the lower bonud.
-		std::set<size_t> lowerReasons;
-		/// Set of literals the conjunction of which implies the upper bonud.
-		std::set<size_t> upperReasons;
-	};
-	/// Lower and upper bounds for variables (in the sense of >= / <=).
-	std::vector<Bounds> bounds;
-	std::vector<Constraint> constraints;
-	// For each bound and constraint, store an index of the literal
-	// that implies it.
-
-	std::set<size_t> reasons() const;
-
-	struct Compare
-	{
-		explicit Compare(bool _considerVariableNames = false): considerVariableNames(_considerVariableNames) {}
-		bool operator()(SolvingState const& _a, SolvingState const& _b) const;
-		bool considerVariableNames;
-	};
-
-	bool operator==(SolvingState const& _other) const noexcept {
-		return bounds == _other.bounds && constraints == _other.constraints;
-	}
-
-	std::string toString() const;
-};
-
 }
 
 template <class T>
@@ -210,18 +166,6 @@ struct std::hash<solidity::util::RationalWithDelta>
 	}
 };
 
-template<>
-struct std::hash<solidity::util::SolvingState::Bounds>
-{
-	std::size_t operator()(solidity::util::SolvingState::Bounds const& _bounds) const noexcept
-	{
-		std::size_t result = 0;
-		hashCombine(result, _bounds.lower);
-		hashCombine(result, _bounds.upper);
-		return result;
-	}
-};
-
 template<>
 struct std::hash<solidity::util::LinearExpression>
 {
@@ -247,18 +191,6 @@ struct std::hash<solidity::util::Constraint>
 	}
 };
 
-template<>
-struct std::hash<solidity::util::SolvingState>
-{
-	std::size_t operator()(solidity::util::SolvingState const& _solvingState) const noexcept
-	{
-		std::size_t result = 0;
-		hashCombineVector(result, _solvingState.bounds);
-		hashCombineVector(result, _solvingState.constraints);
-		return result;
-	}
-};
-
 
 namespace solidity::util
 {

tools/solsmt.cpp

@@ -218,7 +218,7 @@ int main(int argc, char** argv)
 {
 	if (argc != 2)
 	{
-		cout << "Usage: solsmt <smtlib2 fil>" << endl;
+		cout << "Usage: solsmt <smtlib2 file>" << endl;
 		return -1;
 	}