From 3e36c97367aa27a96ac08241e48842b61565077f Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Mon, 9 May 2022 17:22:38 +0200
Subject: [PATCH] Better assertions for boolean lp.

---
 libsolutil/BooleanLP.cpp | 26 +++++++++++++++++++++++---
 libsolutil/BooleanLP.h   |  2 --
 2 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 9022a94fa..bc1b8367c 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -441,9 +441,9 @@ Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _exp
 
 optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr)
 {
-	if (_expr.arguments.empty() || _expr.name == "*")
-		return parseProduct(_expr);
-	else if (_expr.name == "+" || _expr.name == "-")
+	if (_expr.arguments.empty())
+		return parseFactor(_expr);
+	else if (_expr.name == "+" || (_expr.name == "-" && _expr.arguments.size() == 2))
 	{
 		optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0));
 		optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1));
@@ -451,6 +451,26 @@ optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression c
 			return std::nullopt;
 		return _expr.name == "+" ? *left + *right : *left - *right;
 	}
+	else if (_expr.name == "-" && _expr.arguments.size() == 1)
+	{
+		optional<LinearExpression> arg = parseLinearSum(_expr.arguments.at(0));
+		if (arg)
+			return LinearExpression::constant(0) - *arg;
+		else
+			return std::nullopt;
+	}
+	else if (_expr.name == "*")
+		// This will result in nullopt unless one of them is a constant.
+		return parseLinearSum(_expr.arguments.at(0)) * parseLinearSum(_expr.arguments.at(1));
+	else if (_expr.name == "/")
+	{
+		optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0));
+		optional<LinearExpression> right = parseLinearSum(_expr.arguments.at(1));
+		if (!left || !right || !right->isConstant())
+			return std::nullopt;
+		*left /= right->get(0);
+		return left;
+	}
 	else if (_expr.name == "ite")
 	{
 		Expression result = declareInternalVariable(false);
diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h
index 282ad94ee..7129b0664 100644
--- a/libsolutil/BooleanLP.h
+++ b/libsolutil/BooleanLP.h
@@ -78,8 +78,6 @@ public:
 	std::pair<smtutil::CheckResult, std::vector<std::string>>
 	check(std::vector<smtutil::Expression> const& _expressionsToEvaluate) override;
 
-	std::pair<smtutil::CheckResult, std::map<std::string, boost::rational<bigint>>> check();
-
 	std::string toString() const;
 
 private: