C++ namespace cleanup (except tests).

libsolidity/formal/BMC.cpp

@@ -23,9 +23,10 @@
 #include <boost/algorithm/string/replace.hpp>
 
 using namespace std;
-using namespace dev;
-using namespace langutil;
-using namespace dev::solidity;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::langutil;
+using namespace solidity::frontend;
 
 BMC::BMC(
 	smt::EncodingContext& _context,

libsolidity/formal/BMC.h

@@ -39,15 +39,15 @@
 #include <string>
 #include <vector>
 
-namespace langutil
+using solidity::util::h256;
+
+namespace solidity::langutil
 {
 class ErrorReporter;
 struct SourceLocation;
 }
 
-namespace dev
-{
-namespace solidity
+namespace solidity::frontend
 {
 
 class BMC: public SMTEncoder
@@ -186,4 +186,3 @@ private:
 };
 
 }
-}

libsolidity/formal/CHC.cpp

@@ -28,14 +28,14 @@
 #include <libsolidity/ast/TypeProvider.h>
 
 using namespace std;
-using namespace dev;
-using namespace langutil;
-using namespace dev::solidity;
+using namespace solidity;
+using namespace solidity::langutil;
+using namespace solidity::frontend;
 
 CHC::CHC(
 	smt::EncodingContext& _context,
 	ErrorReporter& _errorReporter,
-	map<h256, string> const& _smtlib2Responses,
+	map<util::h256, string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	[[maybe_unused]] smt::SMTSolverChoice _enabledSolvers
 ):

libsolidity/formal/CHC.h

@@ -38,9 +38,7 @@
 
 #include <set>
 
-namespace dev
-{
-namespace solidity
+namespace solidity::frontend
 {
 
 class CHC: public SMTEncoder
@@ -49,7 +47,7 @@ public:
 	CHC(
 		smt::EncodingContext& _context,
 		langutil::ErrorReporter& _errorReporter,
-		std::map<h256, std::string> const& _smtlib2Responses,
+		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		smt::SMTSolverChoice _enabledSolvers
 	);
@@ -217,4 +215,3 @@ private:
 };
 
 }
-}

libsolidity/formal/CHCSmtLib2Interface.cpp

@@ -30,9 +30,10 @@
 #include <stdexcept>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-using namespace dev::solidity::smt;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
 
 CHCSmtLib2Interface::CHCSmtLib2Interface(
 	map<h256, string> const& _queryResponses,
@@ -153,7 +154,7 @@ void CHCSmtLib2Interface::write(string _data)
 
 string CHCSmtLib2Interface::querySolver(string const& _input)
 {
-	h256 inputHash = dev::keccak256(_input);
+	util::h256 inputHash = util::keccak256(_input);
 	if (m_queryResponses.count(inputHash))
 		return m_queryResponses.at(inputHash);
 	if (m_smtCallback)

libsolidity/formal/CHCSmtLib2Interface.h

@@ -25,18 +25,14 @@
 
 #include <libsolidity/formal/SMTLib2Interface.h>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 class CHCSmtLib2Interface: public CHCSolverInterface
 {
 public:
 	explicit CHCSmtLib2Interface(
-		std::map<h256, std::string> const& _queryResponses,
+		std::map<util::h256, std::string> const& _queryResponses,
 		ReadCallback::Callback const& _smtCallback
 	);
 
@@ -68,12 +64,10 @@ private:
 	std::string m_accumulatedOutput;
 	std::set<std::string> m_variables;
 
-	std::map<h256, std::string> const& m_queryResponses;
+	std::map<util::h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;
 
 	ReadCallback::Callback m_smtCallback;
 };
 
 }
-}
-}

libsolidity/formal/CHCSolverInterface.h

@@ -23,11 +23,7 @@
 
 #include <libsolidity/formal/SolverInterface.h>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 class CHCSolverInterface
@@ -52,5 +48,3 @@ public:
 };
 
 }
-}
-}

libsolidity/formal/CVC4Interface.cpp

@@ -21,8 +21,9 @@
 #include <libdevcore/CommonIO.h>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity::smt;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::frontend::smt;
 
 CVC4Interface::CVC4Interface():
 	m_solver(&m_context)

libsolidity/formal/CVC4Interface.h

@@ -33,11 +33,7 @@
 #undef _GLIBCXX_PERMIT_BACKWARD_HASH
 #endif
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 class CVC4Interface: public SolverInterface, public boost::noncopyable
@@ -72,5 +68,3 @@ private:
 };
 
 }
-}
-}

libsolidity/formal/EncodingContext.cpp

@@ -20,8 +20,9 @@
 #include <libsolidity/formal/SymbolicTypes.h>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity::smt;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::frontend::smt;
 
 EncodingContext::EncodingContext():
 	m_thisAddress(make_unique<SymbolicAddressVariable>("this", *this))
@@ -51,13 +52,13 @@ void EncodingContext::clear()
 
 /// Variables.
 
-shared_ptr<SymbolicVariable> EncodingContext::variable(solidity::VariableDeclaration const& _varDecl)
+shared_ptr<SymbolicVariable> EncodingContext::variable(frontend::VariableDeclaration const& _varDecl)
 {
 	solAssert(knownVariable(_varDecl), "");
 	return m_variables[&_varDecl];
 }
 
-bool EncodingContext::createVariable(solidity::VariableDeclaration const& _varDecl)
+bool EncodingContext::createVariable(frontend::VariableDeclaration const& _varDecl)
 {
 	solAssert(!knownVariable(_varDecl), "");
 	auto const& type = _varDecl.type();
@@ -66,24 +67,24 @@ bool EncodingContext::createVariable(solidity::VariableDeclaration const& _varDe
 	return result.first;
 }
 
-bool EncodingContext::knownVariable(solidity::VariableDeclaration const& _varDecl)
+bool EncodingContext::knownVariable(frontend::VariableDeclaration const& _varDecl)
 {
 	return m_variables.count(&_varDecl);
 }
 
-void EncodingContext::resetVariable(solidity::VariableDeclaration const& _variable)
+void EncodingContext::resetVariable(frontend::VariableDeclaration const& _variable)
 {
 	newValue(_variable);
 	setUnknownValue(_variable);
 }
 
-void EncodingContext::resetVariables(set<solidity::VariableDeclaration const*> const& _variables)
+void EncodingContext::resetVariables(set<frontend::VariableDeclaration const*> const& _variables)
 {
 	for (auto const* decl: _variables)
 		resetVariable(*decl);
 }
 
-void EncodingContext::resetVariables(function<bool(solidity::VariableDeclaration const&)> const& _filter)
+void EncodingContext::resetVariables(function<bool(frontend::VariableDeclaration const&)> const& _filter)
 {
 	for_each(begin(m_variables), end(m_variables), [&](auto _variable)
 	{
@@ -94,16 +95,16 @@ void EncodingContext::resetVariables(function<bool(solidity::VariableDeclaration
 
 void EncodingContext::resetAllVariables()
 {
-	resetVariables([&](solidity::VariableDeclaration const&) { return true; });
+	resetVariables([&](frontend::VariableDeclaration const&) { return true; });
 }
 
-Expression EncodingContext::newValue(solidity::VariableDeclaration const& _decl)
+Expression EncodingContext::newValue(frontend::VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
 	return m_variables.at(&_decl)->increaseIndex();
 }
 
-void EncodingContext::setZeroValue(solidity::VariableDeclaration const& _decl)
+void EncodingContext::setZeroValue(frontend::VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
 	setZeroValue(*m_variables.at(&_decl));
@@ -114,7 +115,7 @@ void EncodingContext::setZeroValue(SymbolicVariable& _variable)
 	setSymbolicZeroValue(_variable, *this);
 }
 
-void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl)
+void EncodingContext::setUnknownValue(frontend::VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
 	setUnknownValue(*m_variables.at(&_decl));
@@ -127,14 +128,14 @@ void EncodingContext::setUnknownValue(SymbolicVariable& _variable)
 
 /// Expressions
 
-shared_ptr<SymbolicVariable> EncodingContext::expression(solidity::Expression const& _e)
+shared_ptr<SymbolicVariable> EncodingContext::expression(frontend::Expression const& _e)
 {
 	if (!knownExpression(_e))
 		createExpression(_e);
 	return m_expressions.at(&_e);
 }
 
-bool EncodingContext::createExpression(solidity::Expression const& _e, shared_ptr<SymbolicVariable> _symbVar)
+bool EncodingContext::createExpression(frontend::Expression const& _e, shared_ptr<SymbolicVariable> _symbVar)
 {
 	solAssert(_e.annotation().type, "");
 	if (knownExpression(_e))
@@ -155,7 +156,7 @@ bool EncodingContext::createExpression(solidity::Expression const& _e, shared_pt
 	}
 }
 
-bool EncodingContext::knownExpression(solidity::Expression const& _e) const
+bool EncodingContext::knownExpression(frontend::Expression const& _e) const
 {
 	return m_expressions.count(&_e);
 }
@@ -168,7 +169,7 @@ shared_ptr<SymbolicVariable> EncodingContext::globalSymbol(string const& _name)
 	return m_globalContext.at(_name);
 }
 
-bool EncodingContext::createGlobalSymbol(string const& _name, solidity::Expression const& _expr)
+bool EncodingContext::createGlobalSymbol(string const& _name, frontend::Expression const& _expr)
 {
 	solAssert(!knownGlobalSymbol(_name), "");
 	auto result = newSymbolicVariable(*_expr.annotation().type, _name, *this);

libsolidity/formal/EncodingContext.h

@@ -23,11 +23,7 @@
 #include <unordered_map>
 #include <set>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 /**
@@ -67,48 +63,48 @@ public:
 	/// Variables.
 	//@{
 	/// @returns the symbolic representation of a program variable.
-	std::shared_ptr<SymbolicVariable> variable(solidity::VariableDeclaration const& _varDecl);
+	std::shared_ptr<SymbolicVariable> variable(frontend::VariableDeclaration const& _varDecl);
 	/// @returns all symbolic variables.
-	std::unordered_map<solidity::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> const& variables() const { return m_variables; }
+	std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> const& variables() const { return m_variables; }
 
 	/// Creates a symbolic variable and
 	/// @returns true if a variable's type is not supported and is therefore abstract.
-	bool createVariable(solidity::VariableDeclaration const& _varDecl);
+	bool createVariable(frontend::VariableDeclaration const& _varDecl);
 	/// @returns true if variable was created.
-	bool knownVariable(solidity::VariableDeclaration const& _varDecl);
+	bool knownVariable(frontend::VariableDeclaration const& _varDecl);
 
 	/// Resets a specific variable.
-	void resetVariable(solidity::VariableDeclaration const& _variable);
+	void resetVariable(frontend::VariableDeclaration const& _variable);
 	/// Resets a set of variables.
-	void resetVariables(std::set<solidity::VariableDeclaration const*> const& _variables);
+	void resetVariables(std::set<frontend::VariableDeclaration const*> const& _variables);
 	/// Resets variables according to a predicate.
-	void resetVariables(std::function<bool(solidity::VariableDeclaration const&)> const& _filter);
+	void resetVariables(std::function<bool(frontend::VariableDeclaration const&)> const& _filter);
 	///Resets all variables.
 	void resetAllVariables();
 
 	/// Allocates a new index for the declaration, updates the current
 	/// index to this value and returns the expression.
-	Expression newValue(solidity::VariableDeclaration const& _decl);
+	Expression newValue(frontend::VariableDeclaration const& _decl);
 	/// Sets the value of the declaration to zero.
-	void setZeroValue(solidity::VariableDeclaration const& _decl);
+	void setZeroValue(frontend::VariableDeclaration const& _decl);
 	void setZeroValue(SymbolicVariable& _variable);
 	/// Resets the variable to an unknown value (in its range).
-	void setUnknownValue(solidity::VariableDeclaration const& decl);
+	void setUnknownValue(frontend::VariableDeclaration const& decl);
 	void setUnknownValue(SymbolicVariable& _variable);
 	//@}
 
 	/// Expressions.
 	////@{
 	/// @returns the symbolic representation of an AST node expression.
-	std::shared_ptr<SymbolicVariable> expression(solidity::Expression const& _e);
+	std::shared_ptr<SymbolicVariable> expression(frontend::Expression const& _e);
 	/// @returns all symbolic expressions.
-	std::unordered_map<solidity::Expression const*, std::shared_ptr<SymbolicVariable>> const& expressions() const { return m_expressions; }
+	std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> const& expressions() const { return m_expressions; }
 
 	/// Creates the expression (value can be arbitrary).
 	/// @returns true if type is not supported.
-	bool createExpression(solidity::Expression const& _e, std::shared_ptr<SymbolicVariable> _symbExpr = nullptr);
+	bool createExpression(frontend::Expression const& _e, std::shared_ptr<SymbolicVariable> _symbExpr = nullptr);
 	/// Checks if expression was created.
-	bool knownExpression(solidity::Expression const& _e) const;
+	bool knownExpression(frontend::Expression const& _e) const;
 	//@}
 
 	/// Global variables and functions.
@@ -120,7 +116,7 @@ public:
 
 	/// Defines a new global variable or function
 	/// and @returns true if type was abstracted.
-	bool createGlobalSymbol(std::string const& _name, solidity::Expression const& _expr);
+	bool createGlobalSymbol(std::string const& _name, frontend::Expression const& _expr);
 	/// Checks if special variable or function was seen.
 	bool knownGlobalSymbol(std::string const& _var) const;
 	//@}
@@ -158,10 +154,10 @@ private:
 	/// Symbolic expressions.
 	//{@
 	/// Symbolic variables.
-	std::unordered_map<solidity::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
+	std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
 
 	/// Symbolic expressions.
-	std::unordered_map<solidity::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
+	std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
 
 	/// Symbolic representation of global symbols including
 	/// variables and functions.
@@ -188,5 +184,3 @@ private:
 };
 
 }
-}
-}

libsolidity/formal/ModelChecker.cpp

@@ -18,9 +18,10 @@
 #include <libsolidity/formal/ModelChecker.h>
 
 using namespace std;
-using namespace dev;
-using namespace langutil;
-using namespace dev::solidity;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::langutil;
+using namespace solidity::frontend;
 
 ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,

libsolidity/formal/ModelChecker.h

@@ -30,15 +30,13 @@
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/ErrorReporter.h>
 
-namespace langutil
+namespace solidity::langutil
 {
 class ErrorReporter;
 struct SourceLocation;
 }
 
-namespace dev
-{
-namespace solidity
+namespace solidity::frontend
 {
 
 class ModelChecker
@@ -75,4 +73,3 @@ private:
 };
 
 }
-}

libsolidity/formal/SMTEncoder.cpp

@@ -25,9 +25,10 @@
 #include <boost/range/adaptor/reversed.hpp>
 
 using namespace std;
-using namespace dev;
-using namespace langutil;
-using namespace dev::solidity;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::langutil;
+using namespace solidity::frontend;
 
 SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 	m_errorReporter(m_smtErrors),

libsolidity/formal/SMTEncoder.h

@@ -36,15 +36,13 @@
 #include <unordered_map>
 #include <vector>
 
-namespace langutil
+namespace solidity::langutil
 {
 class ErrorReporter;
 struct SourceLocation;
 }
 
-namespace dev
-{
-namespace solidity
+namespace solidity::frontend
 {
 
 class SMTEncoder: public ASTConstVisitor
@@ -274,4 +272,3 @@ protected:
 };
 
 }
-}

libsolidity/formal/SMTLib2Interface.cpp

@@ -30,9 +30,10 @@
 #include <stdexcept>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-using namespace dev::solidity::smt;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
 
 SMTLib2Interface::SMTLib2Interface(
 	map<h256, string> const& _queryResponses,
@@ -231,7 +232,7 @@ vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, stri
 
 string SMTLib2Interface::querySolver(string const& _input)
 {
-	h256 inputHash = dev::keccak256(_input);
+	h256 inputHash = keccak256(_input);
 	if (m_queryResponses.count(inputHash))
 		return m_queryResponses.at(inputHash);
 	if (m_smtCallback)

libsolidity/formal/SMTLib2Interface.h

@@ -31,18 +31,14 @@
 #include <string>
 #include <vector>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 class SMTLib2Interface: public SolverInterface, public boost::noncopyable
 {
 public:
 	explicit SMTLib2Interface(
-		std::map<h256, std::string> const& _queryResponses,
+		std::map<util::h256, std::string> const& _queryResponses,
 		ReadCallback::Callback const& _smtCallback
 	);
 
@@ -79,12 +75,10 @@ private:
 	std::vector<std::string> m_accumulatedOutput;
 	std::map<std::string, SortPointer> m_variables;
 
-	std::map<h256, std::string> const& m_queryResponses;
+	std::map<util::h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;
 
 	ReadCallback::Callback m_smtCallback;
 };
 
 }
-}
-}

libsolidity/formal/SMTPortfolio.cpp

@@ -26,9 +26,10 @@
 #include <libsolidity/formal/SMTLib2Interface.h>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-using namespace dev::solidity::smt;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
 
 SMTPortfolio::SMTPortfolio(
 	map<h256, string> const& _smtlib2Responses,

libsolidity/formal/SMTPortfolio.h

@@ -26,11 +26,7 @@
 #include <map>
 #include <vector>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 /**
@@ -43,7 +39,7 @@ class SMTPortfolio: public SolverInterface, public boost::noncopyable
 {
 public:
 	SMTPortfolio(
-		std::map<h256, std::string> const& _smtlib2Responses,
+		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		SMTSolverChoice _enabledSolvers
 	);
@@ -70,5 +66,3 @@ private:
 };
 
 }
-}
-}

libsolidity/formal/SSAVariable.cpp

@@ -18,7 +18,8 @@
 #include <libsolidity/formal/SSAVariable.h>
 
 using namespace std;
-using namespace dev::solidity::smt;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
 
 SSAVariable::SSAVariable()
 {

libsolidity/formal/SSAVariable.h

@@ -19,11 +19,7 @@
 
 #include <memory>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 /**
@@ -50,5 +46,3 @@ private:
 };
 
 }
-}
-}

libsolidity/formal/SolverInterface.h

@@ -29,11 +29,7 @@
 #include <string>
 #include <vector>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 struct SMTSolverChoice
@@ -145,7 +141,7 @@ struct SortSort: public Sort
 };
 
 // Forward declaration.
-SortPointer smtSort(solidity::Type const& _type);
+SortPointer smtSort(Type const& _type);
 
 /// C++ representation of an SMTLIB2 expression.
 class Expression
@@ -153,7 +149,7 @@ class Expression
 	friend class SolverInterface;
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
-	explicit Expression(solidity::TypePointer _type): Expression(_type->toString(), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
+	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
 	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
 	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
 	Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
@@ -377,5 +373,3 @@ public:
 };
 
 }
-}
-}

libsolidity/formal/SymbolicTypes.cpp

@@ -24,14 +24,10 @@
 
 using namespace std;
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
-SortPointer smtSort(solidity::Type const& _type)
+SortPointer smtSort(frontend::Type const& _type)
 {
 	switch (smtKind(_type.category()))
 	{
@@ -41,7 +37,7 @@ SortPointer smtSort(solidity::Type const& _type)
 		return make_shared<Sort>(Kind::Bool);
 	case Kind::Function:
 	{
-		auto fType = dynamic_cast<solidity::FunctionType const*>(&_type);
+		auto fType = dynamic_cast<frontend::FunctionType const*>(&_type);
 		solAssert(fType, "");
 		vector<SortPointer> parameterSorts = smtSort(fType->parameterTypes());
 		auto returnTypes = fType->returnParameterTypes();
@@ -61,13 +57,13 @@ SortPointer smtSort(solidity::Type const& _type)
 	{
 		if (isMapping(_type.category()))
 		{
-			auto mapType = dynamic_cast<solidity::MappingType const*>(&_type);
+			auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
 			solAssert(mapType, "");
 			return make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
 		}
 		else if (isStringLiteral(_type.category()))
 		{
-			auto stringLitType = dynamic_cast<solidity::StringLiteralType const*>(&_type);
+			auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
 			solAssert(stringLitType, "");
 			auto intSort = make_shared<Sort>(Kind::Int);
 			return make_shared<ArraySort>(intSort, intSort);
@@ -75,7 +71,7 @@ SortPointer smtSort(solidity::Type const& _type)
 		else
 		{
 			solAssert(isArray(_type.category()), "");
-			auto arrayType = dynamic_cast<solidity::ArrayType const*>(&_type);
+			auto arrayType = dynamic_cast<frontend::ArrayType const*>(&_type);
 			solAssert(arrayType, "");
 			return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSortAbstractFunction(*arrayType->baseType()));
 		}
@@ -86,7 +82,7 @@ SortPointer smtSort(solidity::Type const& _type)
 	}
 }
 
-vector<SortPointer> smtSort(vector<solidity::TypePointer> const& _types)
+vector<SortPointer> smtSort(vector<frontend::TypePointer> const& _types)
 {
 	vector<SortPointer> sorts;
 	for (auto const& type: _types)
@@ -94,14 +90,14 @@ vector<SortPointer> smtSort(vector<solidity::TypePointer> const& _types)
 	return sorts;
 }
 
-SortPointer smtSortAbstractFunction(solidity::Type const& _type)
+SortPointer smtSortAbstractFunction(frontend::Type const& _type)
 {
 	if (isFunction(_type.category()))
 		return make_shared<Sort>(Kind::Int);
 	return smtSort(_type);
 }
 
-Kind smtKind(solidity::Type::Category _category)
+Kind smtKind(frontend::Type::Category _category)
 {
 	if (isNumber(_category))
 		return Kind::Int;
@@ -115,7 +111,7 @@ Kind smtKind(solidity::Type::Category _category)
 	return Kind::Int;
 }
 
-bool isSupportedType(solidity::Type::Category _category)
+bool isSupportedType(frontend::Type::Category _category)
 {
 	return isNumber(_category) ||
 		isBool(_category) ||
@@ -124,25 +120,25 @@ bool isSupportedType(solidity::Type::Category _category)
 		isTuple(_category);
 }
 
-bool isSupportedTypeDeclaration(solidity::Type::Category _category)
+bool isSupportedTypeDeclaration(frontend::Type::Category _category)
 {
 	return isSupportedType(_category) ||
 		isFunction(_category);
 }
 
 pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
-	solidity::Type const& _type,
+	frontend::Type const& _type,
 	std::string const& _uniqueName,
 	EncodingContext& _context
 )
 {
 	bool abstract = false;
 	shared_ptr<SymbolicVariable> var;
-	solidity::TypePointer type = &_type;
+	frontend::TypePointer type = &_type;
 	if (!isSupportedTypeDeclaration(_type))
 	{
 		abstract = true;
-		var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), type, _uniqueName, _context);
+		var = make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context);
 	}
 	else if (isBool(_type.category()))
 		var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
@@ -155,7 +151,7 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 			return find_if(
 				begin(params),
 				end(params),
-				[&](TypePointer _paramType) { return _paramType->category() == solidity::Type::Category::Function; }
+				[&](TypePointer _paramType) { return _paramType->category() == frontend::Type::Category::Function; }
 			);
 		};
 		if (
@@ -173,7 +169,7 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	else if (isFixedBytes(_type.category()))
 	{
-		auto fixedBytesType = dynamic_cast<solidity::FixedBytesType const*>(type);
+		auto fixedBytesType = dynamic_cast<frontend::FixedBytesType const*>(type);
 		solAssert(fixedBytesType, "");
 		var = make_shared<SymbolicFixedBytesVariable>(type, fixedBytesType->numBytes(), _uniqueName, _context);
 	}
@@ -183,10 +179,10 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _context);
 	else if (isRational(_type.category()))
 	{
-		auto rational = dynamic_cast<solidity::RationalNumberType const*>(&_type);
+		auto rational = dynamic_cast<frontend::RationalNumberType const*>(&_type);
 		solAssert(rational, "");
 		if (rational->isFractional())
-			var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), type, _uniqueName, _context);
+			var = make_shared<SymbolicIntVariable>(frontend::TypeProvider::uint256(), type, _uniqueName, _context);
 		else
 			var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	}
@@ -206,47 +202,47 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 	return make_pair(abstract, var);
 }
 
-bool isSupportedType(solidity::Type const& _type)
+bool isSupportedType(frontend::Type const& _type)
 {
 	return isSupportedType(_type.category());
 }
 
-bool isSupportedTypeDeclaration(solidity::Type const& _type)
+bool isSupportedTypeDeclaration(frontend::Type const& _type)
 {
 	return isSupportedTypeDeclaration(_type.category());
 }
 
-bool isInteger(solidity::Type::Category _category)
+bool isInteger(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Integer;
+	return _category == frontend::Type::Category::Integer;
 }
 
-bool isRational(solidity::Type::Category _category)
+bool isRational(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::RationalNumber;
+	return _category == frontend::Type::Category::RationalNumber;
 }
 
-bool isFixedBytes(solidity::Type::Category _category)
+bool isFixedBytes(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::FixedBytes;
+	return _category == frontend::Type::Category::FixedBytes;
 }
 
-bool isAddress(solidity::Type::Category _category)
+bool isAddress(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Address;
+	return _category == frontend::Type::Category::Address;
 }
 
-bool isContract(solidity::Type::Category _category)
+bool isContract(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Contract;
+	return _category == frontend::Type::Category::Contract;
 }
 
-bool isEnum(solidity::Type::Category _category)
+bool isEnum(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Enum;
+	return _category == frontend::Type::Category::Enum;
 }
 
-bool isNumber(solidity::Type::Category _category)
+bool isNumber(frontend::Type::Category _category)
 {
 	return isInteger(_category) ||
 		isRational(_category) ||
@@ -256,43 +252,43 @@ bool isNumber(solidity::Type::Category _category)
 		isEnum(_category);
 }
 
-bool isBool(solidity::Type::Category _category)
+bool isBool(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Bool;
+	return _category == frontend::Type::Category::Bool;
 }
 
-bool isFunction(solidity::Type::Category _category)
+bool isFunction(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Function;
+	return _category == frontend::Type::Category::Function;
 }
 
-bool isMapping(solidity::Type::Category _category)
+bool isMapping(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Mapping;
+	return _category == frontend::Type::Category::Mapping;
 }
 
-bool isArray(solidity::Type::Category _category)
+bool isArray(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Array ||
-		_category == solidity::Type::Category::StringLiteral;
+	return _category == frontend::Type::Category::Array ||
+		_category == frontend::Type::Category::StringLiteral;
 }
 
-bool isTuple(solidity::Type::Category _category)
+bool isTuple(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::Tuple;
+	return _category == frontend::Type::Category::Tuple;
 }
 
-bool isStringLiteral(solidity::Type::Category _category)
+bool isStringLiteral(frontend::Type::Category _category)
 {
-	return _category == solidity::Type::Category::StringLiteral;
+	return _category == frontend::Type::Category::StringLiteral;
 }
 
-Expression minValue(solidity::IntegerType const& _type)
+Expression minValue(frontend::IntegerType const& _type)
 {
 	return Expression(_type.minValue());
 }
 
-Expression maxValue(solidity::IntegerType const& _type)
+Expression maxValue(frontend::IntegerType const& _type)
 {
 	return Expression(_type.maxValue());
 }
@@ -302,13 +298,13 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c
 	setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
 }
 
-void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context)
+void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
 {
 	solAssert(_type, "");
 	_context.addAssertion(_expr == zeroValue(_type));
 }
 
-Expression zeroValue(solidity::TypePointer const& _type)
+Expression zeroValue(frontend::TypePointer const& _type)
 {
 	solAssert(_type, "");
 	if (isSupportedType(_type->category()))
@@ -336,19 +332,19 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
 	setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context);
 }
 
-void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context)
+void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
 {
 	solAssert(_type, "");
 	if (isEnum(_type->category()))
 	{
-		auto enumType = dynamic_cast<solidity::EnumType const*>(_type);
+		auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
 		solAssert(enumType, "");
 		_context.addAssertion(_expr >= 0);
 		_context.addAssertion(_expr < enumType->numberOfMembers());
 	}
 	else if (isInteger(_type->category()))
 	{
-		auto intType = dynamic_cast<solidity::IntegerType const*>(_type);
+		auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
 		solAssert(intType, "");
 		_context.addAssertion(_expr >= minValue(*intType));
 		_context.addAssertion(_expr <= maxValue(*intType));
@@ -356,5 +352,3 @@ void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _typ
 }
 
 }
-}
-}

libsolidity/formal/SymbolicTypes.h

@@ -22,57 +22,51 @@
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/Types.h>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 /// Returns the SMT sort that models the Solidity type _type.
-SortPointer smtSort(solidity::Type const& _type);
-std::vector<SortPointer> smtSort(std::vector<solidity::TypePointer> const& _types);
+SortPointer smtSort(frontend::Type const& _type);
+std::vector<SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
 /// If _type has type Function, abstract it to Integer.
 /// Otherwise return smtSort(_type).
-SortPointer smtSortAbstractFunction(solidity::Type const& _type);
+SortPointer smtSortAbstractFunction(frontend::Type const& _type);
 /// Returns the SMT kind that models the Solidity type type category _category.
-Kind smtKind(solidity::Type::Category _category);
+Kind smtKind(frontend::Type::Category _category);
 
 /// Returns true if type is fully supported (declaration and operations).
-bool isSupportedType(solidity::Type::Category _category);
-bool isSupportedType(solidity::Type const& _type);
+bool isSupportedType(frontend::Type::Category _category);
+bool isSupportedType(frontend::Type const& _type);
 /// Returns true if type is partially supported (declaration).
-bool isSupportedTypeDeclaration(solidity::Type::Category _category);
-bool isSupportedTypeDeclaration(solidity::Type const& _type);
+bool isSupportedTypeDeclaration(frontend::Type::Category _category);
+bool isSupportedTypeDeclaration(frontend::Type const& _type);
 
-bool isInteger(solidity::Type::Category _category);
-bool isRational(solidity::Type::Category _category);
-bool isFixedBytes(solidity::Type::Category _category);
-bool isAddress(solidity::Type::Category _category);
-bool isContract(solidity::Type::Category _category);
-bool isEnum(solidity::Type::Category _category);
-bool isNumber(solidity::Type::Category _category);
-bool isBool(solidity::Type::Category _category);
-bool isFunction(solidity::Type::Category _category);
-bool isMapping(solidity::Type::Category _category);
-bool isArray(solidity::Type::Category _category);
-bool isTuple(solidity::Type::Category _category);
-bool isStringLiteral(solidity::Type::Category _category);
+bool isInteger(frontend::Type::Category _category);
+bool isRational(frontend::Type::Category _category);
+bool isFixedBytes(frontend::Type::Category _category);
+bool isAddress(frontend::Type::Category _category);
+bool isContract(frontend::Type::Category _category);
+bool isEnum(frontend::Type::Category _category);
+bool isNumber(frontend::Type::Category _category);
+bool isBool(frontend::Type::Category _category);
+bool isFunction(frontend::Type::Category _category);
+bool isMapping(frontend::Type::Category _category);
+bool isArray(frontend::Type::Category _category);
+bool isTuple(frontend::Type::Category _category);
+bool isStringLiteral(frontend::Type::Category _category);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,
 /// which is true for unsupported types.
-std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(solidity::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
+std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
 
-Expression minValue(solidity::IntegerType const& _type);
-Expression maxValue(solidity::IntegerType const& _type);
-Expression zeroValue(solidity::TypePointer const& _type);
+Expression minValue(frontend::IntegerType const& _type);
+Expression maxValue(frontend::IntegerType const& _type);
+Expression zeroValue(frontend::TypePointer const& _type);
 
 void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context);
-void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context);
+void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
-void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context);
+void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
 
 }
-}
-}

libsolidity/formal/SymbolicVariables.cpp

@@ -21,12 +21,13 @@
 #include <libsolidity/ast/AST.h>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity::smt;
+using namespace solidity;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
 
 SymbolicVariable::SymbolicVariable(
-	solidity::TypePointer _type,
-	solidity::TypePointer _originalType,
+	TypePointer _type,
+	TypePointer _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -54,7 +55,7 @@ SymbolicVariable::SymbolicVariable(
 	solAssert(m_sort, "");
 }
 
-Expression SymbolicVariable::currentValue(solidity::TypePointer const&) const
+smt::Expression SymbolicVariable::currentValue(frontend::TypePointer const&) const
 {
 	return valueAtIndex(m_ssa->index());
 }
@@ -64,7 +65,7 @@ string SymbolicVariable::currentName() const
 	return uniqueSymbol(m_ssa->index());
 }
 
-Expression SymbolicVariable::valueAtIndex(int _index) const
+smt::Expression SymbolicVariable::valueAtIndex(int _index) const
 {
 	return m_context.newVariable(uniqueSymbol(_index), m_sort);
 }
@@ -79,31 +80,31 @@ string SymbolicVariable::uniqueSymbol(unsigned _index) const
 	return m_uniqueName + "_" + to_string(_index);
 }
 
-Expression SymbolicVariable::resetIndex()
+smt::Expression SymbolicVariable::resetIndex()
 {
 	m_ssa->resetIndex();
 	return currentValue();
 }
 
-Expression SymbolicVariable::increaseIndex()
+smt::Expression SymbolicVariable::increaseIndex()
 {
 	++(*m_ssa);
 	return currentValue();
 }
 
 SymbolicBoolVariable::SymbolicBoolVariable(
-	solidity::TypePointer _type,
+	frontend::TypePointer _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
 	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
-	solAssert(m_type->category() == solidity::Type::Category::Bool, "");
+	solAssert(m_type->category() == frontend::Type::Category::Bool, "");
 }
 
 SymbolicIntVariable::SymbolicIntVariable(
-	solidity::TypePointer _type,
-	solidity::TypePointer _originalType,
+	frontend::TypePointer _type,
+	frontend::TypePointer _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -121,7 +122,7 @@ SymbolicAddressVariable::SymbolicAddressVariable(
 }
 
 SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
-	solidity::TypePointer _originalType,
+	frontend::TypePointer _originalType,
 	unsigned _numBytes,
 	string _uniqueName,
 	EncodingContext& _context
@@ -131,14 +132,14 @@ SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
 }
 
 SymbolicFunctionVariable::SymbolicFunctionVariable(
-	solidity::TypePointer _type,
+	frontend::TypePointer _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
 	SymbolicVariable(_type, _type, move(_uniqueName), _context),
 	m_declaration(m_context.newVariable(currentName(), m_sort))
 {
-	solAssert(m_type->category() == solidity::Type::Category::Function, "");
+	solAssert(m_type->category() == frontend::Type::Category::Function, "");
 }
 
 SymbolicFunctionVariable::SymbolicFunctionVariable(
@@ -152,33 +153,33 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
 	solAssert(m_sort->kind == Kind::Function, "");
 }
 
-Expression SymbolicFunctionVariable::currentValue(solidity::TypePointer const& _targetType) const
+smt::Expression SymbolicFunctionVariable::currentValue(frontend::TypePointer const& _targetType) const
 {
 	return m_abstract.currentValue(_targetType);
 }
 
-Expression SymbolicFunctionVariable::currentFunctionValue() const
+smt::Expression SymbolicFunctionVariable::currentFunctionValue() const
 {
 	return m_declaration;
 }
 
-Expression SymbolicFunctionVariable::valueAtIndex(int _index) const
+smt::Expression SymbolicFunctionVariable::valueAtIndex(int _index) const
 {
 	return m_abstract.valueAtIndex(_index);
 }
 
-Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const
+smt::Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const
 {
 	return SymbolicVariable::valueAtIndex(_index);
 }
 
-Expression SymbolicFunctionVariable::resetIndex()
+smt::Expression SymbolicFunctionVariable::resetIndex()
 {
 	SymbolicVariable::resetIndex();
 	return m_abstract.resetIndex();
 }
 
-Expression SymbolicFunctionVariable::increaseIndex()
+smt::Expression SymbolicFunctionVariable::increaseIndex()
 {
 	++(*m_ssa);
 	resetDeclaration();
@@ -186,7 +187,7 @@ Expression SymbolicFunctionVariable::increaseIndex()
 	return m_abstract.currentValue();
 }
 
-Expression SymbolicFunctionVariable::operator()(vector<Expression> _arguments) const
+smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _arguments) const
 {
 	return m_declaration(_arguments);
 }
@@ -197,7 +198,7 @@ void SymbolicFunctionVariable::resetDeclaration()
 }
 
 SymbolicMappingVariable::SymbolicMappingVariable(
-	solidity::TypePointer _type,
+	frontend::TypePointer _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -207,8 +208,8 @@ SymbolicMappingVariable::SymbolicMappingVariable(
 }
 
 SymbolicArrayVariable::SymbolicArrayVariable(
-	solidity::TypePointer _type,
-	solidity::TypePointer _originalType,
+	frontend::TypePointer _type,
+	frontend::TypePointer _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -217,21 +218,21 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 	solAssert(isArray(m_type->category()), "");
 }
 
-Expression SymbolicArrayVariable::currentValue(solidity::TypePointer const& _targetType) const
+smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
 {
 	if (_targetType)
 		// StringLiterals are encoded as SMT arrays in the generic case,
 		// but they can also be compared/assigned to fixed bytes, in which
 		// case they'd need to be encoded as numbers.
 		if (auto strType = dynamic_cast<StringLiteralType const*>(m_originalType))
-			if (_targetType->category() == solidity::Type::Category::FixedBytes)
-				return smt::Expression(u256(toHex(asBytes(strType->value()), HexPrefix::Add)));
+			if (_targetType->category() == frontend::Type::Category::FixedBytes)
+				return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
 
 	return SymbolicVariable::currentValue(_targetType);
 }
 
 SymbolicEnumVariable::SymbolicEnumVariable(
-	solidity::TypePointer _type,
+	frontend::TypePointer _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -241,7 +242,7 @@ SymbolicEnumVariable::SymbolicEnumVariable(
 }
 
 SymbolicTupleVariable::SymbolicTupleVariable(
-	solidity::TypePointer _type,
+	frontend::TypePointer _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):

libsolidity/formal/SymbolicVariables.h

@@ -23,11 +23,7 @@
 #include <libsolidity/ast/TypeProvider.h>
 #include <memory>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 class EncodingContext;
@@ -40,8 +36,8 @@ class SymbolicVariable
 {
 public:
 	SymbolicVariable(
-		solidity::TypePointer _type,
-		solidity::TypePointer _originalType,
+		frontend::TypePointer _type,
+		frontend::TypePointer _originalType,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -53,7 +49,7 @@ public:
 
 	virtual ~SymbolicVariable() = default;
 
-	virtual Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const;
+	virtual Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const;
 	std::string currentName() const;
 	virtual Expression valueAtIndex(int _index) const;
 	virtual std::string nameAtIndex(int _index) const;
@@ -68,8 +64,8 @@ public:
 	unsigned& index() { return m_ssa->index(); }
 
 	SortPointer const& sort() const { return m_sort; }
-	solidity::TypePointer const& type() const { return m_type; }
-	solidity::TypePointer const& originalType() const { return m_originalType; }
+	frontend::TypePointer const& type() const { return m_type; }
+	frontend::TypePointer const& originalType() const { return m_originalType; }
 
 protected:
 	std::string uniqueSymbol(unsigned _index) const;
@@ -77,9 +73,9 @@ protected:
 	/// SMT sort.
 	SortPointer m_sort;
 	/// Solidity type, used for size and range in number types.
-	solidity::TypePointer m_type;
+	frontend::TypePointer m_type;
 	/// Solidity original type, used for type conversion if necessary.
-	solidity::TypePointer m_originalType;
+	frontend::TypePointer m_originalType;
 	std::string m_uniqueName;
 	EncodingContext& m_context;
 	std::unique_ptr<SSAVariable> m_ssa;
@@ -92,7 +88,7 @@ class SymbolicBoolVariable: public SymbolicVariable
 {
 public:
 	SymbolicBoolVariable(
-		solidity::TypePointer _type,
+		frontend::TypePointer _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -105,8 +101,8 @@ class SymbolicIntVariable: public SymbolicVariable
 {
 public:
 	SymbolicIntVariable(
-		solidity::TypePointer _type,
-		solidity::TypePointer _originalType,
+		frontend::TypePointer _type,
+		frontend::TypePointer _originalType,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -131,7 +127,7 @@ class SymbolicFixedBytesVariable: public SymbolicIntVariable
 {
 public:
 	SymbolicFixedBytesVariable(
-		solidity::TypePointer _originalType,
+		frontend::TypePointer _originalType,
 		unsigned _numBytes,
 		std::string _uniqueName,
 		EncodingContext& _context
@@ -150,7 +146,7 @@ class SymbolicFunctionVariable: public SymbolicVariable
 {
 public:
 	SymbolicFunctionVariable(
-		solidity::TypePointer _type,
+		frontend::TypePointer _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -160,7 +156,7 @@ public:
 		EncodingContext& _context
 	);
 
-	Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const override;
+	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
 
 	// Explicit request the function declaration.
 	Expression currentFunctionValue() const;
@@ -198,7 +194,7 @@ class SymbolicMappingVariable: public SymbolicVariable
 {
 public:
 	SymbolicMappingVariable(
-		solidity::TypePointer _type,
+		frontend::TypePointer _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -211,13 +207,13 @@ class SymbolicArrayVariable: public SymbolicVariable
 {
 public:
 	SymbolicArrayVariable(
-		solidity::TypePointer _type,
-		solidity::TypePointer _originalTtype,
+		frontend::TypePointer _type,
+		frontend::TypePointer _originalTtype,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
 
-	Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const override;
+	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
 };
 
 /**
@@ -227,7 +223,7 @@ class SymbolicEnumVariable: public SymbolicVariable
 {
 public:
 	SymbolicEnumVariable(
-		solidity::TypePointer _type,
+		frontend::TypePointer _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -240,7 +236,7 @@ class SymbolicTupleVariable: public SymbolicVariable
 {
 public:
 	SymbolicTupleVariable(
-		solidity::TypePointer _type,
+		frontend::TypePointer _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -255,5 +251,3 @@ private:
 };
 
 }
-}
-}

libsolidity/formal/VariableUsage.cpp

@@ -23,9 +23,10 @@
 #include <algorithm>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity;
-using namespace dev::solidity::smt;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::frontend;
+using namespace solidity::frontend::smt;
 
 set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<CallableDeclaration const*> const& _outerCallstack)
 {

libsolidity/formal/VariableUsage.h

@@ -22,11 +22,7 @@
 #include <vector>
 #include <set>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 /**
@@ -61,5 +57,3 @@ private:
 };
 
 }
-}
-}

libsolidity/formal/Z3CHCInterface.cpp

@@ -21,8 +21,8 @@
 #include <libdevcore/CommonIO.h>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity::smt;
+using namespace solidity;
+using namespace solidity::frontend::smt;
 
 Z3CHCInterface::Z3CHCInterface():
 	m_z3Interface(make_unique<Z3Interface>()),

libsolidity/formal/Z3CHCInterface.h

@@ -24,11 +24,7 @@
 #include <libsolidity/formal/CHCSolverInterface.h>
 #include <libsolidity/formal/Z3Interface.h>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 class Z3CHCInterface: public CHCSolverInterface
@@ -57,5 +53,3 @@ private:
 };
 
 }
-}
-}

libsolidity/formal/Z3Interface.cpp

@@ -21,8 +21,7 @@
 #include <libdevcore/CommonIO.h>
 
 using namespace std;
-using namespace dev;
-using namespace dev::solidity::smt;
+using namespace solidity::frontend::smt;
 
 Z3Interface::Z3Interface():
 	m_solver(m_context)
@@ -98,7 +97,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 		{
 			z3::model m = m_solver.get_model();
 			for (Expression const& e: _expressionsToEvaluate)
-				values.push_back(toString(m.eval(toZ3Expr(e))));
+				values.push_back(util::toString(m.eval(toZ3Expr(e))));
 		}
 	}
 	catch (z3::exception const&)

libsolidity/formal/Z3Interface.h

@@ -21,11 +21,7 @@
 #include <boost/noncopyable.hpp>
 #include <z3++.h>
 
-namespace dev
-{
-namespace solidity
-{
-namespace smt
+namespace solidity::frontend::smt
 {
 
 class Z3Interface: public SolverInterface, public boost::noncopyable
@@ -70,5 +66,3 @@ private:
 };
 
 }
-}
-}