cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Fix guessing of numbers.

Browse Source
This commit is contained in:
chriseth 2022-06-23 15:18:26 +02:00
parent 27261f6703
commit 4098661b89
2 changed files with 16 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolutil/BooleanLP.cpp
View File

@ -640,7 +640,10 @@ namespace
{ {
bool isNumber(string const& _expr) bool isNumber(string const& _expr)
{ {
return !_expr.empty() && (isDigit(_expr.front()) || _expr.front() == '.'); for (char c: _expr)
if (!isDigit(c) && c != '.')
return false;
return true;
} }
rational parseRational(string const& _atom) rational parseRational(string const& _atom)
{ {

13
tools/solsmt.cpp
View File

@ -129,13 +129,24 @@ string_view command(SMTLib2Expression const& _expr)
return get<string_view>(items.front().data); return get<string_view>(items.front().data);
} }
namespace
{
bool isNumber(string_view const& _expr)
{
for (char c: _expr)
if (!isDigit(c) && c != '.')
return false;
return true;
}
}
smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<string, SortPointer> const& _variableSorts) smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<string, SortPointer> const& _variableSorts)
{ {
return std::visit(GenericVisitor{ return std::visit(GenericVisitor{
[&](string_view const& _atom) { [&](string_view const& _atom) {
if (_atom == "true" || _atom == "false") if (_atom == "true" || _atom == "false")
return Expression(_atom == "true"); return Expression(_atom == "true");
else if (isDigit(_atom.front()) || _atom.front() == '.') else if (isNumber(_atom))
return Expression(string(_atom), {}, SortProvider::realSort); return Expression(string(_atom), {}, SortProvider::realSort);
else else
return Expression(string(_atom), {}, _variableSorts.at(string(_atom))); return Expression(string(_atom), {}, _variableSorts.at(string(_atom)));