Open Eh2406 opened 7 months ago
Some obvious thoughts about when it is safe/efficient to call the new simplify
.
A.intersection(B) == empty
but we find that A.simplify().intersection(B.simplify()) != empty
(substitute whatever set property makes this relevant), we should be very careful before fix it by checking (A.simplify().intersection(B.simplify())).simplify() != empty
. (I'm looking at you satisfier code.)I am hoping that we can solve all the real problems using 80/20 solutions like #163. If most of the large VS come from normal patterns that we can identify and merge then we may not need a general solution for identifying all cases where it's safe to simplify.
Some more thoughts:
simplify
in the construction of partial_solution
or relation
. It runs the risk of computing inferences that cannot be proven from incompatibilities. I'm not saying we can't do it, I'm just saying it's risky.simplify
in the satisfier
search. Because those are terms that are constructed tested and thrown away. If we end up simplify
ing in partial_solution
then we probably need to be consistent in satisfier
search. Otherwise we run the risk of partial_solution
telling us were satisfied but satisfier
search not finding a satisfying assignment. So if we utilize simplify
in the construction of partial_solution
, that needs to be saved in such a way that it can be consistently reused in satisfier
search.intersection
is in prior_cause
. Which seems like a perfect fit for simplify
, as long as we are careful about "no versions". Fundamentally, prior_cause
is already simplifying to incompatibilities into one. So simplifying the terms while were at it seems reasonable.
Our implementation of range just gained a new
simplify
method (cc #156). It would not be too hard to make this a method on DependencyProvider and so available to the Solver. Unfortunately, if done naively it breaks important set properties we rely on. What are those properties? Why does it break them? We don't know.Before we can merge a new method to DependencyProvider we need to be able to articulate what properties it must uphold. We also need to figure out where it is safe for us to use the new method.
Hopefully by simplifying internally complex VS's we can solve the performance problems found in #135