Replace polymorphic sets in symbolic execution

[benozol]

Requires comparison for sat_conj

[Niols]

But do we really want sets of states? I don't think that we are eliminating a lot of states by doing so, while we have to compare a lot of things, is this really giving a speedup? I should try to change it to lists and see if that makes a difference.

Also, the comparison for sat_conj might prove quite hard to write. I guess that I'd just fall back on polymorphic comparison…

[Niols]

Also, I was asking about BatSet because I wanted to know why we had Batteries as a dependency. But I don't mind having that dependency, and it is packaged in Debian.

[benozol]

Just using lists may be possible as well! I’d prefer to keep the container abstract in the symbolic execution, but replacing the set with lists is just a question of the Why3 driver.

[Niols]

Yes of course, the container has to be abstract. But we could adapt the Why3 driver. I'll give it a try and run some benchmarks to see if we gain a speedup when removing comparison but keeping duplicates.

[Niols]

I've given it a try on the usual postinst of ocaml-base-nox. I get 1m7s with BatSet and 1m6s with List. I imagine that most of the time is spent in the constraints solving. So no need to bother for now. However, it might be interesting to consider that later, when we'll have a better constraint solver. We'll see.

By the way, why do we need BatSet.choose?

[benozol]

Thanks that’s interesting. Let’s make polymorphic sets the bottleneck!

why do we need BatSet.choose

That’s a leftover and can be removed.

[Niols]

The change we are talking about is just a few lines in src/symbolic/driver.drv, so we can do that whenever we want. However, a few measures on one script might not be enough to see a real difference between BatSet and list, so we might want for the solver to get better. Then, the difference (if there is one) should be more easily noticeable. Le 30 janvier 2019 11:38:53 GMT+01:00, Benedikt Becker <[email protected]> a écrit :

…

Thanks that’s interesting. Let’s make polymorphic sets the bottleneck!> > >why do we need BatSet.choose> > That’s a leftover and can be removed.> > -- > You are receiving this because you were assigned.> Reply to this email directly or view it on GitHub:> #64 (comment)

[Niols]

@benozol Does this issue still make sense? Would you want me to try the whole batch run twice, once on each kind of sets?

[benozol]

Maybe it would make more sense, if we replace the collection type in the symbolic engine and in the OCaml implementation of symbolic utilities (this wasn't the case before IIRC).

(An outdated attempt was made in #102.)

[Niols]

True, because otherwise we need conversions all the time.