[CN] simplify guards in `each` terms in state output

[peterohanley]

I got a program with this term in the Available resources: each(u64 j; (((j < 4u64) && (!(j == 0u64))) && (!(true && (j < 2u64)))) && (!(j == 2u64))) {Block<struct instrumentation_state>(&instrumentation + j * 44u64 /* 0x2c */)}(ii) (same type)

I simplified (((j < 4u64) && (!(j == 0u64))) && (!(true && (j < 2u64)))) && (!(j == 2u64)) to ((j < 4u64) && (j >= 3u64)) manually. This is much easier to read. I might have made a mistake.

Simplifying terms in general might be tricky but at least (!(true && (j < 2u64))) should be amenable to local simplification to (j >= 2u64).

[cp526]

Agreed.

This particular simplification would be easy to add. We might want to see if we can replace CN's (somewhat adhoc) term simplifier with simplification using the SMT solver, which would be much better at it.

[bcpierce00]

This sounds like a useful step!

On Tue, Jun 25, 2024 at 3:34 PM Christopher Pulte @.***> wrote:

Agreed.

This particular simplification would be easy to add. We might want to see if we can replace CN's (somewhat adhoc) term simplifier with simplification using the SMT solver, which would be much better at it.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/351*issuecomment-2189823741__;Iw!!IBzWLUs!UIuWuFQoofyf0UTdSuMGS9_6qTGvu3Ek3GPF-7yEEDQw8OmAKlsf-ugLteDj54INV-Gfuz_8TSy9rGrAwPa6fNuDacwx$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCYWWVPG2NC3R67IZQ3ZJHA3ZAVCNFSM6AAAAABJ4PB3IKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCOBZHAZDGNZUGE__;!!IBzWLUs!UIuWuFQoofyf0UTdSuMGS9_6qTGvu3Ek3GPF-7yEEDQw8OmAKlsf-ugLteDj54INV-Gfuz_8TSy9rGrAwPa6fNgfFJfD$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[yav]

I believe the constraint in this case should just simplify to j = 3. Both CVC5 and Z3 have a simplify command (it's not standard SMTLIB I think, but since it works in both, it's probably OK to use). I tried it on this example, and this is what both of them come up with:

(! (j >= 4)) && (! (j == 0)) && (j >= 2) &&  (! (j == 2))

This is really not much different from the original, it pretty much jsut removed the true &&.

Also translating to the solver makes some things into uninterpreted functions, which probably are less amenable to simplification than if we know the meaning of the terms. So I suspect we'd need some manual simplificaiton anyways, but it'd be interesting if we can also use the solver to help.