Jonathan Lindegaard Starup

icon location Aarhus, Denmark icon location Computer science PhD at Aarhus University

Results 363 comments of Jonathan Lindegaard Starup

fix: splitting the side-condition check in a T-Choose-* rule to increase performance.

I mean that, since your reformulation is equivalent, the solution for the variables in the system will remain equivalent. I'd think that the separation of the constraints could only lead...

fix: splitting the side-condition check in a T-Choose-* rule to increase performance.

I hope I'm not misunderstanding, but if we have three small formulas instead of one of thrice the size, let's say `x ~ f1`, `x ~ f2`, `x ~ f3`,...

fix: splitting the side-condition check in a T-Choose-* rule to increase performance.

The checking should very soon be redundant since we can (and should) change unifySubset from `t1 + a ~ t2` to `t1 - t2 ~ empty` with the new set...