Method compoundAssignment

libsolidity/formal/SMTEncoder.cpp:2228–2266

}

smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
{
	static std::map<Token, Token> const compoundToArithmetic{
		{Token::AssignAdd, Token::Add},
		{Token::AssignSub, Token::Sub},
		{Token::AssignMul, Token::Mul},
		{Token::AssignDiv, Token::Div},
		{Token::AssignMod, Token::Mod}
	};
	static std::map<Token, Token> const compoundToBitwise{
		{Token::AssignBitAnd, Token::BitAnd},
		{Token::AssignBitOr, Token::BitOr},
		{Token::AssignBitXor, Token::BitXor},
		{Token::AssignShl, Token::SHL},
		{Token::AssignShr, Token::SHR},
		{Token::AssignSar, Token::SAR}
	};
	Token op = _assignment.assignmentOperator();
	solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), "");

	auto decl = identifierToVariable(_assignment.leftHandSide());

	if (compoundToBitwise.count(op))
		return bitwiseOperation(
			compoundToBitwise.at(op),
			decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
			expr(_assignment.rightHandSide(), _assignment.annotation().type),
			_assignment.annotation().type
		);

	auto values = arithmeticOperation(
		compoundToArithmetic.at(op),
		decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
		expr(_assignment.rightHandSide(), _assignment.annotation().type),
		_assignment.annotation().type,
		_assignment
	);
	return values.first;
}

void SMTEncoder::expressionToTupleAssignment(std::vector<std::shared_ptr<VariableDeclaration>> const& _variables, Expression const& _rhs)
{