Skip to content

Commit

Permalink
Purge using namespace std in libsmtutil and libsolc
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikola-matic
nikola-matic committed Jul 12, 2023
1 parent 1ac883b commit 62723b7
Show file tree
Hide file tree
Showing 10 changed files with 145 additions and 153 deletions.
43 changes: 21 additions & 22 deletions libsmtutil/CHCSmtLib2Interface.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,20 +31,19 @@
#include <memory>
#include <stdexcept>

using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::frontend;
using namespace solidity::smtutil;

CHCSmtLib2Interface::CHCSmtLib2Interface(
map<h256, string> const& _queryResponses,
std::map<h256, std::string> const& _queryResponses,
ReadCallback::Callback _smtCallback,
SMTSolverChoice _enabledSolvers,
optional<unsigned> _queryTimeout
std::optional<unsigned> _queryTimeout
):
CHCSolverInterface(_queryTimeout),
m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
m_smtlib2(std::make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
m_queryResponses(std::move(_queryResponses)),
m_smtCallback(_smtCallback),
m_enabledSolvers(_enabledSolvers)
Expand All @@ -66,8 +65,8 @@ void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
smtAssert(_expr.sort->kind == Kind::Function);
if (!m_variables.count(_expr.name))
{
auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
string domain = toSmtLibSort(fSort->domain);
auto fSort = std::dynamic_pointer_cast<FunctionSort>(_expr.sort);
std::string domain = toSmtLibSort(fSort->domain);
// Relations are predicates which have implicit codomain Bool.
m_variables.insert(_expr.name);
write(
Expand All @@ -89,10 +88,10 @@ void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*
);
}

tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
std::tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
{
string query = dumpQuery(_block);
string response = querySolver(query);
std::string query = dumpQuery(_block);
std::string response = querySolver(query);

CheckResult result;
// TODO proper parsing
Expand All @@ -108,7 +107,7 @@ tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface
return {result, Expression(true), {}};
}

void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
void CHCSmtLib2Interface::declareVariable(std::string const& _name, SortPointer const& _sort)
{
smtAssert(_sort);
if (_sort->kind == Kind::Function)
Expand All @@ -120,25 +119,25 @@ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const
}
}

string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort)
std::string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort)
{
if (!m_sortNames.count(&_sort))
m_sortNames[&_sort] = m_smtlib2->toSmtLibSort(_sort);
return m_sortNames.at(&_sort);
}

string CHCSmtLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)
std::string CHCSmtLib2Interface::toSmtLibSort(std::vector<SortPointer> const& _sorts)
{
string ssort("(");
std::string ssort("(");
for (auto const& sort: _sorts)
ssort += toSmtLibSort(*sort) + " ";
ssort += ")";
return ssort;
}

string CHCSmtLib2Interface::forall()
std::string CHCSmtLib2Interface::forall()
{
string vars("(");
std::string vars("(");
for (auto const& [name, sort]: m_smtlib2->variables())
{
solAssert(sort, "");
Expand All @@ -149,17 +148,17 @@ string CHCSmtLib2Interface::forall()
return vars;
}

void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
void CHCSmtLib2Interface::declareFunction(std::string const& _name, SortPointer const& _sort)
{
smtAssert(_sort);
smtAssert(_sort->kind == Kind::Function);
// TODO Use domain and codomain as key as well
if (!m_variables.count(_name))
{
auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
auto fSort = std::dynamic_pointer_cast<FunctionSort>(_sort);
smtAssert(fSort->codomain);
string domain = toSmtLibSort(fSort->domain);
string codomain = toSmtLibSort(*fSort->codomain);
std::string domain = toSmtLibSort(fSort->domain);
std::string codomain = toSmtLibSort(*fSort->codomain);
m_variables.insert(_name);
write(
"(declare-fun |" +
Expand All @@ -173,12 +172,12 @@ void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const
}
}

void CHCSmtLib2Interface::write(string _data)
void CHCSmtLib2Interface::write(std::string _data)
{
m_accumulatedOutput += std::move(_data) + "\n";
}

string CHCSmtLib2Interface::querySolver(string const& _input)
std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
{
util::h256 inputHash = util::keccak256(_input);
if (m_queryResponses.count(inputHash))
Expand Down Expand Up @@ -212,7 +211,7 @@ std::string CHCSmtLib2Interface::dumpQuery(Expression const& _expr)
std::string CHCSmtLib2Interface::createHeaderAndDeclarations() {
std::stringstream s;
if (m_queryTimeout)
s << "(set-option :timeout " + to_string(*m_queryTimeout) + ")\n";
s << "(set-option :timeout " + std::to_string(*m_queryTimeout) + ")\n";
s << "(set-logic HORN)" << std::endl;

for (auto const& decl: m_smtlib2->userSorts() | ranges::views::values)
Expand Down
29 changes: 14 additions & 15 deletions libsmtutil/CVC4Interface.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,11 @@

#include <cvc4/util/bitvector.h>

using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::smtutil;

CVC4Interface::CVC4Interface(optional<unsigned> _queryTimeout):
CVC4Interface::CVC4Interface(std::optional<unsigned> _queryTimeout):
SolverInterface(_queryTimeout),
m_solver(&m_context)
{
Expand Down Expand Up @@ -56,7 +55,7 @@ void CVC4Interface::pop()
m_solver.pop();
}

void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort)
void CVC4Interface::declareVariable(std::string const& _name, SortPointer const& _sort)
{
smtAssert(_sort, "");
m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort));
Expand Down Expand Up @@ -86,10 +85,10 @@ void CVC4Interface::addAssertion(Expression const& _expr)
}
}

pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const& _expressionsToEvaluate)
std::pair<CheckResult, std::vector<std::string>> CVC4Interface::check(std::vector<Expression> const& _expressionsToEvaluate)
{
CheckResult result;
vector<string> values;
std::vector<std::string> values;
try
{
switch (m_solver.checkSat().isSat())
Expand Down Expand Up @@ -119,7 +118,7 @@ pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const&
values.clear();
}

return make_pair(result, values);
return std::make_pair(result, values);
}

CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
Expand All @@ -128,13 +127,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
if (_expr.arguments.empty() && m_variables.count(_expr.name))
return m_variables.at(_expr.name);

vector<CVC4::Expr> arguments;
std::vector<CVC4::Expr> arguments;
for (auto const& arg: _expr.arguments)
arguments.push_back(toCVC4Expr(arg));

try
{
string const& n = _expr.name;
std::string const& n = _expr.name;
// Function application
if (!arguments.empty() && m_variables.count(_expr.name))
return m_context.mkExpr(CVC4::kind::APPLY_UF, m_variables.at(n), arguments);
Expand All @@ -145,7 +144,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return m_context.mkConst(true);
else if (n == "false")
return m_context.mkConst(false);
else if (auto sortSort = dynamic_pointer_cast<SortSort>(_expr.sort))
else if (auto sortSort = std::dynamic_pointer_cast<SortSort>(_expr.sort))
return m_context.mkVar(n, cvc4Sort(*sortSort->inner));
else
try
Expand Down Expand Up @@ -224,7 +223,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
}
else if (n == "bv2int")
{
auto intSort = dynamic_pointer_cast<IntSort>(_expr.sort);
auto intSort = std::dynamic_pointer_cast<IntSort>(_expr.sort);
smtAssert(intSort, "");
auto nat = m_context.mkExpr(CVC4::kind::BITVECTOR_TO_NAT, arguments[0]);
if (!intSort->isSigned)
Expand Down Expand Up @@ -254,13 +253,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
else if (n == "const_array")
{
shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
std::shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
smtAssert(sortSort, "");
return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1]));
}
else if (n == "tuple_get")
{
shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.arguments[0].sort);
std::shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.arguments[0].sort);
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
Expand All @@ -270,7 +269,7 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
}
else if (n == "tuple_constructor")
{
shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
std::shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
Expand Down Expand Up @@ -328,9 +327,9 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
return m_context.integerType();
}

vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<SortPointer> const& _sorts)
std::vector<CVC4::Type> CVC4Interface::cvc4Sort(std::vector<SortPointer> const& _sorts)
{
vector<CVC4::Type> cvc4Sorts;
std::vector<CVC4::Type> cvc4Sorts;
for (auto const& _sort: _sorts)
cvc4Sorts.push_back(cvc4Sort(*_sort));
return cvc4Sorts;
Expand Down
Loading

0 comments on commit 62723b7

Please sign in to comment.