Function toSolidityStr

libsolidity/formal/ExpressionFormatter.cpp:141–185

}

std::string toSolidityStr(smtutil::Expression const& _expr)
{
	auto const& op = _expr.name;

	auto const& args = _expr.arguments;
	auto strArgs = util::applyMap(args, [](auto const& _arg) { return toSolidityStr(_arg); });

	// Constant or variable.
	if (args.empty())
		return op;

	if (starts_with(op, "dt_accessor"))
		return formatDatatypeAccessor(_expr, strArgs);

	// Infix operators with format replacements.
	static std::map<std::string, std::string> const infixOps{
		{"and", "&&"},
		{"or", "||"},
		{"implies", "=>"},
		{"=", "="},
		{">", ">"},
		{">=", ">="},
		{"<", "<"},
		{"<=", "<="},
		{"+", "+"},
		{"-", "-"},
		{"*", "*"},
		{"/", "/"},
		{"div", "/"},
		{"mod", "%"}
	};
	// Some of these (and, or, +, *) may have >= 2 arguments from z3.
	if (infixOps.count(op) && args.size() >= 2)
		return formatInfixOp(infixOps.at(op), strArgs);

	static std::set<std::string> const arrayOps{"select", "store", "const_array"};
	if (arrayOps.count(op))
		return formatArrayOp(_expr, strArgs);

	if (args.size() == 1)
		return formatUnaryOp(_expr, strArgs);

	// Other operators such as bv2int, int2bv may end up here.
	return op + "(" + boost::algorithm::join(strArgs, ", ") + ")";
}

namespace
{