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

Get invariants from eldarica

Browse Source
This commit is contained in:
Martin Blicha 2023-08-17 09:30:52 +02:00
parent d8c1a124e7
commit a4b4e70b67
1 changed files with 13 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -199,7 +199,7 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
smtAssert(m_smtCallback, "Callback must be set!");
std::string solverBinary = [&](){
if (m_enabledSolvers.eld)
return "eld";
return "eld -ssol"; // TODO: Use -scex to get counterexamples, but Eldarica uses different format than Z3
if (m_enabledSolvers.z3)
return "z3 -in rlimit=1000000 fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false";
return "";
@ -217,6 +217,18 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
if (secondResult.success and boost::starts_with(secondResult.responseOrErrorMessage, "unsat"))
return secondResult.responseOrErrorMessage;
}
else if (m_enabledSolvers.eld and boost::starts_with(result.responseOrErrorMessage, "sat"))
{
// Wrap Eldarica model in a pair of parentheses to treat is a single (list) s-expression
// That's the SMTLIB way to print a model (i.e., respond to a get-model command).
auto afterSat = result.responseOrErrorMessage.find('\n');
if (afterSat != std::string::npos) // if there is more than just "sat"
{
result.responseOrErrorMessage.insert(afterSat + 1, "(");
result.responseOrErrorMessage.push_back(')');
return result.responseOrErrorMessage;
}
}
return result.responseOrErrorMessage;
}