search

septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Optimise GRASShopper terms #136

Open MattWindsor91 opened 7 years ago

MattWindsor91 commented 7 years ago

As far as I know, the GRASShopper terms are currently bypassing the term optimiser, which is sub-optimal. Not sure whether a quick pass through simp would be enough or if we need to try plumb it back in a bit more.

MattWindsor91 commented 7 years ago

On further look I'm not entirely sure how to proceed with this—the problematic terms are things like P || !P that we aren't currently optimising away at all.

I've started a branch to start adding more expression optimisation but I feel as if this could be a very deep rabbit hole…

septract commented 7 years ago

I don't think this is a high priority unless you can do it easily.

On 1 February 2017 at 16:36, Matt Windsor notifications@github.com wrote:

On further look I'm not entirely sure how to proceed with this—the problematic terms are things like P || !P that we aren't currently optimising away at all.

I've started a branch to start adding more expression optimisation but I feel as if this could be a very deep rabbit hole…

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/septract/starling-tool/issues/136#issuecomment-276707556, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9g1XX9MbwMo0DXnxH8A0p-7RpfnGks5rYLR4gaJpZM4LzyJu .

-- http://www-users.cs.york.ac.uk/~miked/

MattWindsor91 commented 7 years ago

Yeah, I think I'll push what I have and give up =3

septract commented 7 years ago

👍

septract commented 7 years ago

We probably don't want to write our own boolean simplifier, but Z3 has the simplify command built in. If we encoded all the non-Z3 stuff in a formula as distinct uninterpreted symbols, we could pass the encoding to Z3, then reconstruct the simplified formula. Could be a bit of work though and I'm not sure it's worth it.

Stack overflow question on the simplifier: https://stackoverflow.com/questions/14057349/simplification-in-z3