Add sound- operation extraction

[pavpanchekha]

This PR adds a new kind of operator within the egraph: (safe-F x y ... default). The real semantics is that it returns (F x y ...), unless that would crash, in which case it instead returns default. This should be more permissive for rewriting that the current unsound-F approach and should ultimately allow us to solve, say, the quadratic examples again.

https://chatgpt.com/codex/tasks/task_e_68521fa019ec833185e3129d9eeb730e

[pavpanchekha]

Quite odd that this is worse, I had high hopes for this. I looked into some diffs and honestly I have no idea what's going on, besides the basic idea that this PR creates more rewritable expressions so the node limit is exhausted faster.

[pavpanchekha]

Alright, an update on this branch. We now achieve better results than main and also have no more unsound rules. It's worth cleaning up add-sound-with-explanations and removing all the unsound stuff since it's no longer used, and possibly also make egraphs now handle unsoundness with a crash or harsher warning rather than gracefully like now.

[pavpanchekha]

Ok, I think this PR has converged. We now, I believe, are getting results equal to main (no longer better necessarily but not worse) and we also have no more unsound rules, and I've removed all the code I wanted to remove. So I think if nightlies are good this is getting merged.