The implementation of FM in ATS/Postiats is largely standard.
One small improvement lies in its handling of an inequality of the
following kind:
2x + 2y >= 1
This inequality is first changed to 2x + 2y >= 2 and then simplified to x +
y >= 1.
The implementation uses linear types to ensure
Hi all,
I've read that ATS uses the Fourier-Mitzkin method to handle
constraints/inequalities but what I've read has been light on details.
Does ATS do anything interesting for integer constraints?
(Also: where in the ATS compiler is the constraint-solving code? I've only
looked a bit but I