Fix code style problems

This commit is contained in:
Martin Blicha 2023-07-21 17:14:29 +02:00
parent 8ea8a1eb99
commit 92689e4256
2 changed files with 38 additions and 30 deletions

View File

@ -22,7 +22,7 @@
#include <libsolutil/StringUtils.h> #include <libsolutil/StringUtils.h>
#include <libsolutil/Visitor.h> #include <libsolutil/Visitor.h>
#include "liblangutil/Common.h" #include <liblangutil/Common.h>
#include <boost/algorithm/string/join.hpp> #include <boost/algorithm/string/join.hpp>
@ -107,7 +107,8 @@ std::tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Inte
// TODO proper parsing // TODO proper parsing
if (boost::starts_with(response, "sat")) if (boost::starts_with(response, "sat"))
result = CheckResult::UNSATISFIABLE; result = CheckResult::UNSATISFIABLE;
else if (boost::starts_with(response, "unsat")) { else if (boost::starts_with(response, "unsat"))
{
result = CheckResult::SATISFIABLE; result = CheckResult::SATISFIABLE;
return {result, Expression(true), graphFromZ3Proof(response)}; return {result, Expression(true), graphFromZ3Proof(response)};
} }
@ -201,7 +202,8 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, _input); auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, _input);
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);
@ -257,7 +259,8 @@ std::string CHCSmtLib2Interface::SMTLib2Expression::toString() const
}, data); }, data);
} }
namespace { namespace
{
using SMTLib2Expression = CHCSmtLib2Interface::SMTLib2Expression; using SMTLib2Expression = CHCSmtLib2Interface::SMTLib2Expression;
bool isNumber(std::string const& _expr) bool isNumber(std::string const& _expr)
{ {
@ -270,7 +273,7 @@ namespace {
bool isAtom(SMTLib2Expression const & expr) bool isAtom(SMTLib2Expression const & expr)
{ {
return std::holds_alternative<std::string>(expr.data); return std::holds_alternative<std::string>(expr.data);
}; }
std::string const& asAtom(SMTLib2Expression const& expr) std::string const& asAtom(SMTLib2Expression const& expr)
{ {
@ -293,7 +296,8 @@ namespace {
SortPointer toSort(SMTLib2Expression const& expr) SortPointer toSort(SMTLib2Expression const& expr)
{ {
if (isAtom(expr)) { if (isAtom(expr))
{
auto const& name = asAtom(expr); auto const& name = asAtom(expr);
if (name == "Int") if (name == "Int")
return SortProvider::sintSort; return SortProvider::sintSort;
@ -307,7 +311,8 @@ namespace {
return std::make_shared<Sort>(*it->first); return std::make_shared<Sort>(*it->first);
} else { } else {
auto const& args = asSubExpressions(expr); auto const& args = asSubExpressions(expr);
if (asAtom(args[0]) == "Array") { if (asAtom(args[0]) == "Array")
{
assert(args.size() == 3); assert(args.size() == 3);
auto domainSort = toSort(args[1]); auto domainSort = toSort(args[1]);
auto codomainSort = toSort(args[2]); auto codomainSort = toSort(args[2]);
@ -316,7 +321,7 @@ namespace {
} }
// FIXME: This is not correct, we need to track sorts properly! // FIXME: This is not correct, we need to track sorts properly!
// return SortProvider::boolSort; // return SortProvider::boolSort;
smtAssert(false, "Unknown sort encountered"); smtAssert(false, "Unknown sort encountered");
} }
smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr) smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr)
@ -333,13 +338,14 @@ namespace {
[&](std::vector<SMTLib2Expression> const& _subExpr) { [&](std::vector<SMTLib2Expression> const& _subExpr) {
SortPointer sort; SortPointer sort;
std::vector<smtutil::Expression> arguments; std::vector<smtutil::Expression> arguments;
if (isAtom(_subExpr.front())) { if (isAtom(_subExpr.front()))
std::string const &op = std::get<std::string>(_subExpr.front().data); {
std::string const& op = std::get<std::string>(_subExpr.front().data);
std::set<std::string> boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", "=>"}; std::set<std::string> boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", "=>"};
for (size_t i = 1; i < _subExpr.size(); i++) for (size_t i = 1; i < _subExpr.size(); i++)
arguments.emplace_back(toSMTUtilExpression(_subExpr[i])); arguments.emplace_back(toSMTUtilExpression(_subExpr[i]));
sort = contains(boolOperators, op) ? SortProvider::boolSort : arguments.back().sort; sort = contains(boolOperators, op) ? SortProvider::boolSort : arguments.back().sort;
return smtutil::Expression(op, move(arguments), move(sort)); return smtutil::Expression(op, std::move(arguments), std::move(sort));
} else { } else {
// check for const array // check for const array
if (_subExpr.size() == 2 and !isAtom(_subExpr[0])) if (_subExpr.size() == 2 and !isAtom(_subExpr[0]))
@ -387,7 +393,7 @@ namespace {
// simulate whitespace because we do not want to read the next token // simulate whitespace because we do not want to read the next token
// since it might block. // since it might block.
m_token = ' '; m_token = ' ';
return {move(subExpressions)}; return {std::move(subExpressions)};
} }
else else
return {parseToken()}; return {parseToken()};
@ -506,20 +512,20 @@ namespace {
if (isAtom(first) && std::get<std::string>(first.data) == "let") if (isAtom(first) && std::get<std::string>(first.data) == "let")
{ {
assert(!isAtom(subexprs[1])); assert(!isAtom(subexprs[1]));
auto & bindingExpressions = std::get<SMTLib2Expression::args_t>(subexprs[1].data); auto& bindingExpressions = std::get<SMTLib2Expression::args_t>(subexprs[1].data);
// process new bindings // process new bindings
std::vector<std::pair<std::string, SMTLib2Expression>> newBindings; std::vector<std::pair<std::string, SMTLib2Expression>> newBindings;
for (auto & binding : bindingExpressions) for (auto& binding: bindingExpressions)
{ {
assert(!isAtom(binding)); assert(!isAtom(binding));
auto & bindingPair = std::get<SMTLib2Expression::args_t>(binding.data); auto& bindingPair = std::get<SMTLib2Expression::args_t>(binding.data);
assert(bindingPair.size() == 2); assert(bindingPair.size() == 2);
assert(isAtom(bindingPair.at(0))); assert(isAtom(bindingPair.at(0)));
inlineLetExpressions(bindingPair.at(1), bindings); inlineLetExpressions(bindingPair.at(1), bindings);
newBindings.emplace_back(std::get<std::string>(bindingPair.at(0).data), bindingPair.at(1)); newBindings.emplace_back(std::get<std::string>(bindingPair.at(0).data), bindingPair.at(1));
} }
bindings.pushScope(); bindings.pushScope();
for (auto && [name, expr] : newBindings) for (auto&& [name, expr] : newBindings)
bindings.addBinding(std::move(name), std::move(expr)); bindings.addBinding(std::move(name), std::move(expr));
newBindings.clear(); newBindings.clear();
@ -534,7 +540,7 @@ namespace {
return; return;
} }
// not a let expression, just process all arguments // not a let expression, just process all arguments
for (auto& subexpr : subexprs) for (auto& subexpr: subexprs)
{ {
inlineLetExpressions(subexpr, bindings); inlineLetExpressions(subexpr, bindings);
} }
@ -632,7 +638,8 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromSMTLib2Expression(SMT
return graph; return graph;
} }
CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(const std::string & _proof) { CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(std::string const& _proof)
{
std::stringstream ss(_proof); std::stringstream ss(_proof);
std::string answer; std::string answer;
ss >> answer; ss >> answer;
@ -644,11 +651,13 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(const std::st
solAssert(parser.isEOF()); solAssert(parser.isEOF());
solAssert(!isAtom(all)); solAssert(!isAtom(all));
auto& commands = std::get<SMTLib2Expression::args_t>(all.data); auto& commands = std::get<SMTLib2Expression::args_t>(all.data);
for (auto& command : commands) { for (auto& command: commands) {
// std::cout << command.toString() << '\n' << std::endl; // std::cout << command.toString() << '\n' << std::endl;
if (!isAtom(command)) { if (!isAtom(command))
{
auto const& head = std::get<SMTLib2Expression::args_t>(command.data)[0]; auto const& head = std::get<SMTLib2Expression::args_t>(command.data)[0];
if (isAtom(head) && std::get<std::string>(head.data) == "proof") { if (isAtom(head) && std::get<std::string>(head.data) == "proof")
{
// std::cout << "Proof expression!\n" << command.toString() << std::endl; // std::cout << "Proof expression!\n" << command.toString() << std::endl;
inlineLetExpressions(command); inlineLetExpressions(command);
// std::cout << "Cleaned Proof expression!\n" << command.toString() << std::endl; // std::cout << "Cleaned Proof expression!\n" << command.toString() << std::endl;
@ -657,4 +666,4 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(const std::st
} }
} }
return {}; return {};
} }

View File

@ -115,7 +115,8 @@ void SMTLib2Interface::addAssertion(Expression const& _expr)
write("(assert " + toSExpr(_expr) + ")"); write("(assert " + toSExpr(_expr) + ")");
} }
namespace { // Helpers for querying solvers using SMT callback namespace // Helpers for querying solvers using SMT callback
{
auto resultFromSolverResponse (std::string const& response) { auto resultFromSolverResponse (std::string const& response) {
CheckResult result; CheckResult result;
// TODO proper parsing // TODO proper parsing
@ -135,9 +136,9 @@ namespace { // Helpers for querying solvers using SMT callback
return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE;
} }
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<std::string> values; std::vector<std::string> values;
while (_start < _end) while (_start < _end)
{ {
auto valStart = std::find(_start, _end, ' '); auto valStart = std::find(_start, _end, ' ');
@ -151,7 +152,7 @@ namespace { // Helpers for querying solvers using SMT callback
return values; return values;
} }
std::vector<std::string> parseValues(std::string const& solverAnswer) std::vector<std::string> parseValues(std::string const& solverAnswer)
{ {
return parseValues(std::find(solverAnswer.cbegin(), solverAnswer.cend(), '\n'), solverAnswer.cend()); return parseValues(std::find(solverAnswer.cbegin(), solverAnswer.cend(), '\n'), solverAnswer.cend());
} }
@ -159,8 +160,7 @@ namespace { // Helpers for querying solvers using SMT callback
std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::vector<Expression> const& _expressionsToEvaluate) std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::vector<Expression> const& _expressionsToEvaluate)
{ {
auto query = boost::algorithm::join(m_accumulatedOutput, "\n") + auto query = boost::algorithm::join(m_accumulatedOutput, "\n") + checkSatAndGetValuesCommand(_expressionsToEvaluate);
checkSatAndGetValuesCommand(_expressionsToEvaluate);
std::vector<std::string> solverCommands; std::vector<std::string> solverCommands;
if (m_enabledSolvers.z3) if (m_enabledSolvers.z3)
@ -195,9 +195,8 @@ std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::ve
else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR)
lastResult = result; lastResult = result;
} }
if (lastResult == CheckResult::ERROR) { if (lastResult == CheckResult::ERROR)
m_unhandledQueries.push_back(query); m_unhandledQueries.push_back(query);
}
return std::make_pair(lastResult, finalValues); return std::make_pair(lastResult, finalValues);
} }