15 Jul
2010
15 Jul
'10
12:44 p.m.
On Thu, Jul 15, 2010 at 12:42:41AM +0100, Thomas Schilling wrote:
simplifications are possible. To make this efficient, the solver also regularly canonicalises constraints. E.g., function symbols go to the left and constructors to the right.
One minor correction: the canonicalisation of constraints actually has more to do with ensuring that the solving process terminates than it does with efficiency. -Brent