Optimise GRASShopper terms

[MattWindsor91]

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]

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]

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

…

On 1 February 2017 at 16:36, Matt Windsor ***@***.***> 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 <#136 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9g1XX9MbwMo0DXnxH8A0p-7RpfnGks5rYLR4gaJpZM4LzyJu> .

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

[MattWindsor91]

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

[septract]

👍

[septract]

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