Construction of with expression in `lowering/byte_operators.cpp` does not match getters in `with_exprt` [rfc]

[thomasspriggs]

This section constructs a with expression containing multiple where/new value pairs -

cbmc/src/solvers/lowering/byte_operators.cpp

Lines 1514 to 1517 in 8bd2617

	if(result.id() != ID_with)
	result = with_exprt{result, std::move(where), std::move(update_value)};
	else
	result.add_to_operands(std::move(where), std::move(update_value));

However the API here only provides access to a single where/new value pair -

cbmc/src/util/std_expr.h

Lines 2444 to 2462 in 8bd2617

	exprt &where()
	{
	return op1();
	}
	const exprt &where() const
	{
	return op1();
	}
	exprt &new_value()
	{
	return op2();
	}
	const exprt &new_value() const
	{
	return op2();
	}

What should be the preferred way to deal with this mismatch?
A. Update the lowering to nest with expressions rather than constructing a single expression with multiple pairs.
B. Update with_exprt to expose the possibility of multiple pairs.
C. Work around the mismatch for the moment using exprt::operands to access the additional pairs.
I am not a huge fan of option C as it leaves the possibility of multiple pairs relatively surprising when referring to with_exprt. Option A seems relatively preferable as it keeps the API simpler, however I have also presented option B in case there are performance reasons for preferring more operands over more deeply nested expressions.

[tautschnig]

I believe "B" is the way to go: the reason "A" isn't the best approach is that it could result in deeply nested expressions when a large array is to be updated in this way.

[thomasspriggs]

I believe "B" is the way to go: the reason "A" isn't the best approach is that it could result in deeply nested expressions when a large array is to be updated in this way.

For context, we came across this issue whilst working on SMT support. The closest array theory equivalent term seems to be the store function - https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml This array theory function only supports a single where/new value pair. So for the purposes of SMT I would expect this to be converted into a deeply nested expression which ever choice we make for the API here.

I appreciate there may be benefits to avoiding deeply nested expressions for SAT support however.

[tautschnig]

Yes, I suppose that nested expression is unavoidable at SMT level at this time.

[tautschnig]

Labelling this "Version 6:" I believe we should reconsider the use of with_exprt altogether, much like the comment at its declaration suggests, or else restructure the operands within the expression such that each operand has two child operands. Else it will be very difficult to assess whether all readers of such expressions correctly process all updates that a with expression seeks to denote.

Any such change will result in (GOTO-) binary incompatibility, and we should postpone that until the major-version bump.