Closed derekelkins closed 2 years ago
Hi @derekelkins, thanks for the report! This is indeed very weird, I'm investigating it now.
This is a great bug find! The problem is that in the explanation generation code, the initial expression is used to populate the beginning of the explanation. While the rest of the explanations code properly caches shared sub-expressions in the same way that RecExpr
does, this initial population does not.
I'll fix it with the next release! Along with the fix will be an algorithm for reducing proof sizes as well.
Thanks for the quick response. Using the pull request branch for the egg
dependency does perform well for me. I can also verify that the PR didn't change the behavior for my use-case.
Running the below with
egg
0.7.1 pegs a CPU core to 100%, takes a long time to complete, and consumes gigabytes of memory. This has 1117 nodes and the rule fires around ~60 times. This is a version of a real expression. I thought the problem might be the depth of the expression (it's probably around a couple hundred layers deep), but my attempts to make an artificial expression didn't seem to cause the problem. I do think the depth is a factor, but something more is going on. If I comment out theexplain_equivalence
, the code executes instantaneously.It's hard to see from the serialized, all the rule applications are independent, i.e. there are no expressions of the form
(Foo (Foo (Constant ?n) ...) ...)
. This could be further reinforced by having the rule produce(Konstant ?n)
.I think this code is reasonable, but if I'm misusing the library in some way or doing something unsupported, let me know.