[CN] simplify guards in each terms in state output
#351
Comments
|
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. |
|
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: ***@***.***>
|
dc-mak
changed the title
each terms in state outputeach terms in state output
|
I believe the constraint in this case should just simplify to This is really not much different from the original, it pretty much jsut removed the 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. |
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).The text was updated successfully, but these errors were encountered: