[TG-634] Logical expression building utility

[LAJW]

This PR implements an exprt wrapper for constructing logical expression hierarchies using C++ operators.

Additionally, this PR contains small refactor on one of the most used string functions to show that it's working as intended.

For example, it lets following code:

exprt res_length=plus_exprt( 
  s1.length(), minus_exprt(end_index, start_index));
binary_relation_exprt prem(end_index, ID_gt, start_index); 
implies_exprt a1(prem, equal_exprt(res.length(), res_length));

be expressed this way:

exprt a1 = end_index > start_index >>=
           axt(s1.length()) + end_index - start_index == axt(res.length());

Part 2 of String Refinement overhaul PR

[LAJW]

@reuk @jasigal @romainbrenguier Take a look if you have some spare time on your hands.

[reuk]

Nice and idiomatic 👍

[jasigal]

Looks good :)

[jasigal]

Can we not use ->?

[LAJW]

No, because -> is an unary operator. An alias for (*ptr).<method_name>

[jasigal]

Why do we cast to a string expression? Is this only going to be for the string solver?

[romainbrenguier]

For now it's only used in the string solver, but ultimately this should represent index_of_exprt (taking an array_exprt on the left) this will be unified once the new version of the string solver is merged as strings will be represented by arrays.

[romainbrenguier]

could we also add != for notequal_exprt?

[romainbrenguier]

We may want to use this for index_exprt in case it's not a string_exprt

[LAJW]

I shall wait then until they become one and the same thing.

[jasigal]

Should use axt(binary_relation_exprt(expr_, ID_ge, rhs.expr_))

[jasigal]

Should use axt(binary_relation_exprt(expr_, ID_le, rhs.expr_))

[martin-cs]

We had this code; pretty much exactly. It was called oexpr and in util/oexpr.h. It was deleted by PR #347 : 2db625 as part of a clean up in moving to a new C++ version, having been marked as "old" 346495 .

As I recall, I thought of it and suggested it to Daniel on the basis you could have one piece of code that was both concrete or symbolic depending on the types used (of course you can also achieve this by doing everything symbolically and then constant folding via simply_expr, anyway, I thought I was clever at the time), he implemented it because, why not, it then sat there and wasn't used because it turns out to not be as useful as you'd originally think and then was removed because it wasn't being used.

I guess there are multiple conclusions one could draw from this story and I'll let you pick your own.

[martin-cs]

Over all ... I'm not convinced it gains us that much. A slight reduction in characters in long lines but that is traded against obfuscating what is symbolic and what is literal.

As I said before, I used to think this was a great idea but I've not yet seen a compelling use-case.

[martin-cs]

I would have thought this would be happier in util/ as nothing it does is specific to refinement. Also, maybe we should just resurrect oexpr.

[martin-cs]

Please include in the usual style.

[martin-cs]

Why are these renamed?

[LAJW]

Change too controversial, was attempted before and rejected. Closing.