From 68bfbdb2a65dfefc0b6c3f57d223efe2fcb78c5f Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Wed, 1 Jun 2022 17:53:33 +0200
Subject: [PATCH] Support all fractional constants.

---
 libsolutil/BooleanLP.cpp | 42 ++++++++++++++++++++++++++++++++--------
 tools/solsmt.cpp         | 15 ++++----------
 2 files changed, 38 insertions(+), 19 deletions(-)

diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp
index 243eb8c3b..866f4a1c4 100644
--- a/libsolutil/BooleanLP.cpp
+++ b/libsolutil/BooleanLP.cpp
@@ -411,8 +411,6 @@ void BooleanLPSolver::addLetBindings(Expression const& _let, LetBindings& _letBi
 
 optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, LetBindings _letBindings)
 {
-	// TODO constanst true/false?
-
 	if (_expr.name == "let")
 	{
 		addLetBindings(_expr, _letBindings);
@@ -430,6 +428,11 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
 			else
 				varIndex = std::get<size_t>(binding);
 		}
+		else if (_expr.name == "true" || _expr.name == "false")
+		{
+			// TODO handle this better
+			solAssert(false, "True/false literals not implemented");
+		}
 		else
 			varIndex = state().variables.at(_expr.name);
 		solAssert(isBooleanVariable(varIndex));
@@ -594,7 +597,7 @@ optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression c
 		// This will result in nullopt unless one of them is a constant.
 		return parseLinearSum(_expr.arguments.at(0), _letBindings) * parseLinearSum(_expr.arguments.at(1), _letBindings);
 	}
-	else if (_expr.name == "/")
+	else if (_expr.name == "/" || _expr.name == "div")
 	{
 		solAssert(_expr.arguments.size() == 2);
 		optional<LinearExpression> left = parseLinearSum(_expr.arguments.at(0), _letBindings);
@@ -614,19 +617,42 @@ optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression c
 	}
 	else
 	{
-		cerr << _expr.toString() << endl;
-		cerr << "Invalid operator " << _expr.name << endl;
+//		cerr << _expr.toString() << endl;
+//		cerr << "Invalid operator " << _expr.name << endl;
 		return std::nullopt;
 	}
 }
 
+namespace
+{
+bool isNumber(string const& _expr)
+{
+	return !_expr.empty() && (isDigit(_expr.front()) || _expr.front() == '.');
+}
+rational parseRational(string const& _atom)
+{
+	size_t decimal = _atom.find('.');
+	if (decimal == string::npos)
+		return rational(bigint(_atom));
+
+	unsigned shift = static_cast<unsigned>(_atom.size() - decimal - 1);
+	rational r(
+		bigint(string(_atom.substr(0, decimal)) + string(_atom.substr(decimal + 1))),
+		pow(bigint(10), shift)
+	);
+//	cerr << _atom << endl;
+//	cerr << r << endl;
+	return r;
+}
+}
+
 bool BooleanLPSolver::isLiteral(smtutil::Expression const& _expr) const
 {
 	if (!_expr.arguments.empty())
 		return false;
 	solAssert(!_expr.name.empty(), "");
 	return
-		('0' <= _expr.name[0] && _expr.name[0] <= '9') ||
+		isNumber(_expr.name) ||
 		_expr.name == "true" ||
 		_expr.name == "false";
 }
@@ -635,8 +661,8 @@ optional<LinearExpression> BooleanLPSolver::parseFactor(smtutil::Expression cons
 {
 	solAssert(_expr.arguments.empty(), "");
 	solAssert(!_expr.name.empty(), "");
-	if ('0' <= _expr.name[0] && _expr.name[0] <= '9')
-		return LinearExpression::constant(rational(bigint(_expr.name)));
+	if (isNumber(_expr.name))
+		return LinearExpression::constant(parseRational(_expr.name));
 	else if (_expr.name == "true")
 		// TODO do we want to do this?
 		return LinearExpression::constant(1);
diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp
index fe513ec95..c8f72df84 100644
--- a/tools/solsmt.cpp
+++ b/tools/solsmt.cpp
@@ -129,21 +129,14 @@ string_view command(SMTLib2Expression const& _expr)
 	return get<string_view>(items.front().data);
 }
 
-// TODO If we want to return rational here, we need smtutil::Expression to support rationals...
-u256 parseRational(string_view _atom)
-{
-	if (_atom.size() >= 3 && _atom.at(_atom.size() - 1) == '0' && _atom.at(_atom.size() - 2) == '.')
-		return parseRational(_atom.substr(0, _atom.size() - 2));
-	else
-		return u256(_atom);
-}
-
 smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<string, SortPointer> const& _variableSorts)
 {
 	return std::visit(GenericVisitor{
 		[&](string_view const& _atom) {
-			if (isDigit(_atom.front()) || _atom.front() == '.')
-				return Expression(parseRational(_atom).str(), {}, SortProvider::realSort);
+			if (_atom == "true" || _atom == "false")
+				return Expression(_atom == "true");
+			else if (isDigit(_atom.front()) || _atom.front() == '.')
+				return Expression(string(_atom), {}, SortProvider::realSort);
 			else
 				return Expression(string(_atom), {}, _variableSorts.at(string(_atom)));
 		},