cerc-io/solidity
16
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 missing std

Browse Source
This commit is contained in:
Martin Blicha 2023-07-15 14:56:18 +02:00
parent 2195b5e57a
commit 479bb9c3de
2 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -197,7 +197,7 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
{ {
if (m_enabledSolvers.z3 and boost::starts_with(result.responseOrErrorMessage, "unsat")) { if (m_enabledSolvers.z3 and boost::starts_with(result.responseOrErrorMessage, "unsat")) {
solverBinary += " fp.xform.slice=false fp.xform.inline_linear=false fp.xform.inline_eager=false"; solverBinary += " fp.xform.slice=false fp.xform.inline_linear=false fp.xform.inline_eager=false";
string extendedQuery = "(set-option :produce-proofs true)" + _input + "\n(get-proof)"; std::string extendedQuery = "(set-option :produce-proofs true)" + _input + "\n(get-proof)";
auto secondResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, extendedQuery); auto secondResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, extendedQuery);
if (secondResult.success) if (secondResult.success)
return secondResult.responseOrErrorMessage; return secondResult.responseOrErrorMessage;

16
libsmtutil/SMTLib2Interface.cpp
View File

@ -39,7 +39,7 @@ using namespace solidity::frontend;
using namespace solidity::smtutil; using namespace solidity::smtutil;
SMTLib2Interface::SMTLib2Interface( SMTLib2Interface::SMTLib2Interface(
[[maybe_unused]] std::map<h256, string> _queryResponses, [[maybe_unused]] std::map<h256, std::string> _queryResponses,
ReadCallback::Callback _smtCallback, ReadCallback::Callback _smtCallback,
SMTSolverChoice _enabledSolvers, SMTSolverChoice _enabledSolvers,
std::optional<unsigned> _queryTimeout std::optional<unsigned> _queryTimeout
@ -136,23 +136,23 @@ namespace { // Helpers for querying solvers using SMT callback
std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end) std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end)
{ {
std::vector<string> values; std::vector<std::string> values;
while (_start < _end) while (_start < _end)
{ {
auto valStart = find(_start, _end, ' '); auto valStart = std::find(_start, _end, ' ');
if (valStart < _end) if (valStart < _end)
++valStart; ++valStart;
auto valEnd = find(valStart, _end, ')'); auto valEnd = std::find(valStart, _end, ')');
values.emplace_back(valStart, valEnd); values.emplace_back(valStart, valEnd);
_start = find(valEnd, _end, '('); _start = std::find(valEnd, _end, '(');
} }
return values; return values;
} }
std::vector<string> parseValues(string const& solverAnswer) std::vector<std::string> parseValues(std::string const& solverAnswer)
{ {
return parseValues(find(solverAnswer.cbegin(), solverAnswer.cend(), '\n'), solverAnswer.cend()); return parseValues(std::find(solverAnswer.cbegin(), solverAnswer.cend(), '\n'), solverAnswer.cend());
} }
} }
@ -168,7 +168,7 @@ std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::ve
solverCommands.emplace_back("cvc4"); solverCommands.emplace_back("cvc4");
CheckResult lastResult = CheckResult::ERROR; CheckResult lastResult = CheckResult::ERROR;
std::vector<string> finalValues; std::vector<std::string> finalValues;
smtAssert(m_smtCallback); smtAssert(m_smtCallback);
for (auto const& s: solverCommands) for (auto const& s: solverCommands)
{ {