let_exprt can now do multiple bindings #4992

kroening · 2019-08-06T21:13:01Z

This matches what the SMT-LIB standard does. It also matches what our own
binding_exprt can do, i.e., let_exprt can be re-written into a lambda
binding plus a function application in the standard way.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 13c457b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122229305

smowton · 2019-08-07T09:02:11Z

src/util/std_expr.h

        where,
        where.type())
  {
  }

+  symbol_value_sequencet &symbol_value_sequence()


So someone retrieving this needs to know it's an alternating sequence of symbol, value, symbol, value? Seems better to either have a sequence of 2-tuples called bindings, or else provide accessors for nth_symbol, nth_value etc. Either of these can also enforce that the symbols are symbol_exprt.

I did consider both options.
Problems of the "accessor" option are that a) you can't easily iterate, and b) it kills the USE_LIST option for performance reasons (but we may want to kill that anyway).
The two-tuple option would be somewhat more memory-consuming, but maybe that's not a genuine issue.

Now with the "sequence of 2-tuples" option.

tautschnig

It doesn't strike me as particularly great design to build something rather fragile just to satisfy a potential, yet unproven future use.

tautschnig · 2019-08-07T10:02:33Z

src/util/std_expr.h

+  {
+  }
+
+  using symbol_value_sequencet = std::vector<exprt>;


I know this isn't the first time/only place we are doing this, but we really shouldn't: this should be exprt::operandst, unless we are very intentionally (but still somewhat questionably) using a subtype that we know has the same memory layout (as was the case for binding_exprt).

I don't see much of an alternative to strengthen typing while still exposing something that can be iterated over.
An option could be to invent a custom range-like setup, which would essentially wrap the underlying iterator. That would eliminate the scary casts at the level of the container.

I'd be happy to look into this, but given that this is a very global problem, I would declare that to be outside of the scope of this PR.

Well, can we at least not make it any worse? I.e., not introduce yet another local definition of what we believe to be the type of exprt::operands()?

Without that, it's not possible to type the symbols.

tautschnig · 2019-08-07T10:07:56Z

src/util/std_expr.h

        where,
        where.type())
  {
  }

+  symbol_value_sequencet &symbol_value_sequence()
+  {
+    return (symbol_value_sequencet &)op0().operands();


I do find these type casts scary. Right now, this one actually is unnecessary. But if in future there were to be a difference then only runtime crashes would tell us.

tautschnig · 2019-08-07T11:36:16Z

src/util/std_expr.h

 {
 public:
-  let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
-    : ternary_exprt(
+  class let_binding_exprt : public binary_exprt


Another question: why is a let_binding_exprt not at all related to a binding_exprt? That seems surprising to me.

This is not trivial: there's only one "where", and not one per binding, whereas the let bindings need an additional "value". Thus, the "is-a" relationship is not easy to establish.

Ack, but then the binding_exprt may need to be reconsidered if it isn't actually as generic as was hoped? Maybe it should just not be called binding_exprt and instead its API should be folded into that of a quantifier_exprt? I would just like to avoid confusion.

I did consider that, but it does fit array_comprehension_exprt. That would then need to be a quantifier (odd) or have it's own API.

Another idea. An option could be that let_exprt gets a binding_exprt as operand!

That would seem nice and consistent with the other uses of binding_exprt!

Ok, will go for it!

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: eba4578).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122360496

This enables let_exprt to use binding_exprt.

This enables let_exprt to do multiple binding, which matches what the SMT-LIB standard does. The new let_exprt can be re-written into a lambda binding plus a function application in the standard way.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 71a20e9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122980484

kroening added the enhancement label Aug 6, 2019

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners August 6, 2019 21:13

kroening force-pushed the let-is-a-binding branch from 8931632 to 13c457b Compare August 7, 2019 06:22

allredj reviewed Aug 7, 2019

View reviewed changes

smowton reviewed Aug 7, 2019

View reviewed changes

tautschnig reviewed Aug 7, 2019

View reviewed changes

kroening force-pushed the let-is-a-binding branch from 13c457b to d5163b7 Compare August 7, 2019 11:02

tautschnig reviewed Aug 7, 2019

View reviewed changes

kroening force-pushed the let-is-a-binding branch 3 times, most recently from cff58cd to eba4578 Compare August 7, 2019 21:46

allredj reviewed Aug 8, 2019

View reviewed changes

kroening mentioned this pull request Aug 13, 2019

prop_conv_solvert: introduce scopes #4510

Merged

5 tasks

Daniel Kroening added 2 commits August 13, 2019 12:08

move binding_exprt to std_expr.h

535aea7

This enables let_exprt to use binding_exprt.

let_exprt now uses binding_exprt

71a20e9

This enables let_exprt to do multiple binding, which matches what the SMT-LIB standard does. The new let_exprt can be re-written into a lambda binding plus a function application in the standard way.

kroening force-pushed the let-is-a-binding branch from eba4578 to 71a20e9 Compare August 13, 2019 11:08

allredj reviewed Aug 13, 2019

View reviewed changes

kroening assigned tautschnig Aug 15, 2019

kroening assigned peterschrammel and pkesseli Oct 10, 2019

peterschrammel approved these changes Oct 10, 2019

View reviewed changes

kroening merged commit 31cd424 into develop Oct 10, 2019

kroening deleted the let-is-a-binding branch October 10, 2019 13:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

let_exprt can now do multiple bindings #4992

let_exprt can now do multiple bindings #4992

kroening commented Aug 6, 2019

allredj left a comment

smowton Aug 7, 2019

kroening Aug 7, 2019

kroening Aug 7, 2019

tautschnig left a comment

tautschnig Aug 7, 2019

kroening Aug 7, 2019

kroening Aug 7, 2019

tautschnig Aug 7, 2019

kroening Aug 7, 2019

tautschnig Aug 7, 2019

tautschnig Aug 7, 2019

kroening Aug 7, 2019

tautschnig Aug 7, 2019

kroening Aug 7, 2019

kroening Aug 7, 2019

tautschnig Aug 7, 2019

kroening Aug 7, 2019

kroening Aug 7, 2019

allredj left a comment

allredj left a comment

let_exprt can now do multiple bindings #4992

let_exprt can now do multiple bindings #4992

Conversation

kroening commented Aug 6, 2019

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment