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

Small cleanup

Browse Source
This commit is contained in:
Martin Blicha 2023-08-17 00:26:13 +02:00
parent 1b68b5764d
commit 497ca183b4
4 changed files with 10 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -201,19 +201,19 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
if (m_enabledSolvers.eld) if (m_enabledSolvers.eld)
return "eld"; return "eld";
if (m_enabledSolvers.z3) if (m_enabledSolvers.z3)
return "z3 rlimit=1000000 fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false"; return "z3 -in rlimit=1000000 fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false";
return ""; return "";
}(); }();
std::string z3Input = _input + "(get-model)\n"; std::string z3Input = _input + "(get-model)\n";
auto const& query = boost::starts_with(solverBinary, "z3") ? z3Input : _input; auto const& query = boost::starts_with(solverBinary, "z3") ? z3Input : _input;
auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, query); auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ":" + solverBinary, query);
if (result.success) if (result.success)
{ {
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";
std::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 and boost::starts_with(secondResult.responseOrErrorMessage, "unsat")) if (secondResult.success and boost::starts_with(secondResult.responseOrErrorMessage, "unsat"))
return secondResult.responseOrErrorMessage; return secondResult.responseOrErrorMessage;
} }

6
libsmtutil/SMTLib2Interface.cpp
View File

@ -168,16 +168,16 @@ std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::ve
std::vector<std::string> solverCommands; std::vector<std::string> solverCommands;
if (m_enabledSolvers.z3) if (m_enabledSolvers.z3)
solverCommands.emplace_back("z3 rlimit=1000000"); solverCommands.emplace_back("z3 -in rlimit=1000000");
if (m_enabledSolvers.cvc4) if (m_enabledSolvers.cvc4)
solverCommands.emplace_back("cvc4"); solverCommands.emplace_back("cvc4 --lang smtlib2.6 --output-lang smtlib2.6");
CheckResult lastResult = CheckResult::ERROR; CheckResult lastResult = CheckResult::ERROR;
std::vector<std::string> finalValues; std::vector<std::string> finalValues;
smtAssert(m_smtCallback); smtAssert(m_smtCallback);
for (auto const& s: solverCommands) for (auto const& s: solverCommands)
{ {
auto callBackResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ' ' + s, query); auto callBackResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ":" + s, query);
if (not callBackResult.success) if (not callBackResult.success)
continue; continue;
auto const& response = callBackResult.responseOrErrorMessage; auto const& response = callBackResult.responseOrErrorMessage;

9
libsolidity/interface/SMTSolverCommand.cpp
View File

@ -38,11 +38,11 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
{ {
try try
{ {
auto pos = _kind.find(' '); auto pos = _kind.find(":");
solAssert(pos != std::string::npos);
auto kind = _kind.substr(0, pos); auto kind = _kind.substr(0, pos);
auto solverCommand = _kind.substr(pos + 1); auto solverCommand = _kind.substr(pos + 1);
if (kind != ReadCallback::kindString(ReadCallback::Kind::SMTQuery)) solAssert(kind == ReadCallback::kindString(ReadCallback::Kind::SMTQuery), "SMTQuery callback used as callback kind " + kind);
solAssert(false, "SMTQuery callback used as callback kind " + kind);
std::vector<std::string> commandArgs; std::vector<std::string> commandArgs;
boost::split(commandArgs, solverCommand, boost::is_any_of(" ")); boost::split(commandArgs, solverCommand, boost::is_any_of(" "));
@ -55,9 +55,6 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
commandArgs.erase(commandArgs.begin()); commandArgs.erase(commandArgs.begin());
if (solverBinary == "z3")
commandArgs.insert(commandArgs.begin(), "-in");
boost::process::opstream in; // input to subprocess written to by main process boost::process::opstream in; // input to subprocess written to by main process
boost::process::ipstream out; // output from subprocess read by main process boost::process::ipstream out; // output from subprocess read by main process
boost::process::child solver( boost::process::child solver(

1
libsolidity/interface/SMTSolverCommand.h
View File

@ -29,6 +29,7 @@ public:
SMTSolverCommand() = default; SMTSolverCommand() = default;
/// Calls an SMT solver with the given query. /// Calls an SMT solver with the given query.
/// The whole command line for invoking the solver is part of @p _kind
frontend::ReadCallback::Result solve(std::string const& _kind, std::string const& _query); frontend::ReadCallback::Result solve(std::string const& _kind, std::string const& _query);
frontend::ReadCallback::Callback solver() frontend::ReadCallback::Callback solver()