Conditions in explanations

[adrianleh]

Hi,

I'm currently using explanations on a set of rewrites, of which some are conditional. However, when I get the proof explanation all rewrite steps to rewrite my terms are listed, except the ones that fulfilled the conditions of conditional rewrites. Is it possible to force a condition to include the explanation of the existence of the matched enode into the explanation?

[oflatt]

Unfortunately, egg's explanations system does not support conditional rewrites. We are actively trying to add such support to egglog, but it's turning out to be a tough problem.

If it's possible to change the encoding to include the condition as part of the term, that might be a work around with some effort. You could also include in the term some hints that let whatever you're using with the result reconstruct the proof. Hope this helps.

[adrianleh]

Thanks for the feedback. Could you elaborate a bit on the problem here. In my understanding it seems to me that typically conditions prove the existence of an enode or the equality of two enodes, which the checker could handle? Also is there an updated date on the egglog proof engine?

[oflatt]

Egg's current proof generation algorithm and format doesn't support multiple preconditions- it was built with the assumption of matching a single term.

No solid date on the egglog proof engine, but we are focusing more on it now.

[adrianleh]

I noticed that but it's quite easy to hack in multiple preconditions by creating custom AndConditions that take multiple conditions and ensure they are all met

[oflatt]

That sounds like a great hack, lmk how it goes

[adrianleh]

It’s working successfully, maybe a worthwhile addition to egg; should I open a PR?

…

On Mar 6, 2025, at 13:37, Oliver Flatt ***@***.***> wrote: oflatt left a comment (egraphs-good/egg#350) That sounds like a great hack, lmk how it goes — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you authored the thread. <#350 (comment)> <https://github.com/notifications/unsubscribe-auth/AGKK7HU662BAOMITNFKMKGD2TCPXLAVCNFSM6AAAAABYH52YAOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDOMBUG43TGNRSGA> oflatt left a comment (egraphs-good/egg#350) <#350 (comment)> That sounds like a great hack, lmk how it goes — Reply to this email directly, view it on GitHub <#350 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AGKK7HU662BAOMITNFKMKGD2TCPXLAVCNFSM6AAAAABYH52YAOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDOMBUG43TGNRSGA>. You are receiving this because you authored the thread.

[oflatt]

Sure, open a PR and I'll take a look. Happy to take a look at your code, if we change egg we'd want to consider carefully. I'd like to see how it interacts with the various proof formats and what kinds of conditions are supported.