From 92689e42565ca8ad78103838ed9ef5de3c18b7f8 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Fri, 21 Jul 2023 17:14:29 +0200 Subject: [PATCH] Fix code style problems --- libsmtutil/CHCSmtLib2Interface.cpp | 53 +++++++++++++++++------------- libsmtutil/SMTLib2Interface.cpp | 15 ++++----- 2 files changed, 38 insertions(+), 30 deletions(-) diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index f7c3ed286..89be65197 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -22,7 +22,7 @@ #include #include -#include "liblangutil/Common.h" +#include #include @@ -107,7 +107,8 @@ std::tuple CHCSmtLib2Inte // TODO proper parsing if (boost::starts_with(response, "sat")) result = CheckResult::UNSATISFIABLE; - else if (boost::starts_with(response, "unsat")) { + else if (boost::starts_with(response, "unsat")) + { result = CheckResult::SATISFIABLE; 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); 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"; std::string extendedQuery = "(set-option :produce-proofs true)" + _input + "\n(get-proof)"; auto secondResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, extendedQuery); @@ -257,7 +259,8 @@ std::string CHCSmtLib2Interface::SMTLib2Expression::toString() const }, data); } -namespace { +namespace +{ using SMTLib2Expression = CHCSmtLib2Interface::SMTLib2Expression; bool isNumber(std::string const& _expr) { @@ -270,7 +273,7 @@ namespace { bool isAtom(SMTLib2Expression const & expr) { return std::holds_alternative(expr.data); - }; + } std::string const& asAtom(SMTLib2Expression const& expr) { @@ -293,7 +296,8 @@ namespace { SortPointer toSort(SMTLib2Expression const& expr) { - if (isAtom(expr)) { + if (isAtom(expr)) + { auto const& name = asAtom(expr); if (name == "Int") return SortProvider::sintSort; @@ -307,7 +311,8 @@ namespace { return std::make_shared(*it->first); } else { auto const& args = asSubExpressions(expr); - if (asAtom(args[0]) == "Array") { + if (asAtom(args[0]) == "Array") + { assert(args.size() == 3); auto domainSort = toSort(args[1]); auto codomainSort = toSort(args[2]); @@ -316,7 +321,7 @@ namespace { } // FIXME: This is not correct, we need to track sorts properly! // return SortProvider::boolSort; - smtAssert(false, "Unknown sort encountered"); + smtAssert(false, "Unknown sort encountered"); } smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr) @@ -333,13 +338,14 @@ namespace { [&](std::vector const& _subExpr) { SortPointer sort; std::vector arguments; - if (isAtom(_subExpr.front())) { - std::string const &op = std::get(_subExpr.front().data); + if (isAtom(_subExpr.front())) + { + std::string const& op = std::get(_subExpr.front().data); std::set boolOperators{"and", "or", "not", "=", "<", ">", "<=", ">=", "=>"}; for (size_t i = 1; i < _subExpr.size(); i++) arguments.emplace_back(toSMTUtilExpression(_subExpr[i])); 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 { // check for const array 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 // since it might block. m_token = ' '; - return {move(subExpressions)}; + return {std::move(subExpressions)}; } else return {parseToken()}; @@ -506,20 +512,20 @@ namespace { if (isAtom(first) && std::get(first.data) == "let") { assert(!isAtom(subexprs[1])); - auto & bindingExpressions = std::get(subexprs[1].data); + auto& bindingExpressions = std::get(subexprs[1].data); // process new bindings std::vector> newBindings; - for (auto & binding : bindingExpressions) + for (auto& binding: bindingExpressions) { assert(!isAtom(binding)); - auto & bindingPair = std::get(binding.data); + auto& bindingPair = std::get(binding.data); assert(bindingPair.size() == 2); assert(isAtom(bindingPair.at(0))); inlineLetExpressions(bindingPair.at(1), bindings); newBindings.emplace_back(std::get(bindingPair.at(0).data), bindingPair.at(1)); } bindings.pushScope(); - for (auto && [name, expr] : newBindings) + for (auto&& [name, expr] : newBindings) bindings.addBinding(std::move(name), std::move(expr)); newBindings.clear(); @@ -534,7 +540,7 @@ namespace { return; } // not a let expression, just process all arguments - for (auto& subexpr : subexprs) + for (auto& subexpr: subexprs) { inlineLetExpressions(subexpr, bindings); } @@ -632,7 +638,8 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromSMTLib2Expression(SMT return graph; } -CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(const std::string & _proof) { +CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(std::string const& _proof) +{ std::stringstream ss(_proof); std::string answer; ss >> answer; @@ -644,11 +651,13 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(const std::st solAssert(parser.isEOF()); solAssert(!isAtom(all)); auto& commands = std::get(all.data); - for (auto& command : commands) { + for (auto& command: commands) { // std::cout << command.toString() << '\n' << std::endl; - if (!isAtom(command)) { + if (!isAtom(command)) + { auto const& head = std::get(command.data)[0]; - if (isAtom(head) && std::get(head.data) == "proof") { + if (isAtom(head) && std::get(head.data) == "proof") + { // std::cout << "Proof expression!\n" << command.toString() << std::endl; inlineLetExpressions(command); // std::cout << "Cleaned Proof expression!\n" << command.toString() << std::endl; @@ -657,4 +666,4 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromZ3Proof(const std::st } } return {}; -} \ No newline at end of file +} diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index d125890a5..2a7bc0c8b 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -115,7 +115,8 @@ void SMTLib2Interface::addAssertion(Expression const& _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) { CheckResult result; // TODO proper parsing @@ -135,9 +136,9 @@ namespace { // Helpers for querying solvers using SMT callback return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; } - std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end) + std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end) { - std::vector values; + std::vector values; while (_start < _end) { auto valStart = std::find(_start, _end, ' '); @@ -151,7 +152,7 @@ namespace { // Helpers for querying solvers using SMT callback return values; } - std::vector parseValues(std::string const& solverAnswer) + std::vector parseValues(std::string const& solverAnswer) { 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> SMTLib2Interface::check(std::vector const& _expressionsToEvaluate) { - auto query = boost::algorithm::join(m_accumulatedOutput, "\n") + - checkSatAndGetValuesCommand(_expressionsToEvaluate); + auto query = boost::algorithm::join(m_accumulatedOutput, "\n") + checkSatAndGetValuesCommand(_expressionsToEvaluate); std::vector solverCommands; if (m_enabledSolvers.z3) @@ -195,9 +195,8 @@ std::pair> SMTLib2Interface::check(std::ve else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) lastResult = result; } - if (lastResult == CheckResult::ERROR) { + if (lastResult == CheckResult::ERROR) m_unhandledQueries.push_back(query); - } return std::make_pair(lastResult, finalValues); }