Opportunistic `NonZeronessWitness` columns

[OlivierBBB]

Main issue

There are several points (especially in hub scenarii) where one would like to impose nonzeroness of certain columns through a constraint à la

(is-nonzero COL)

where all we want is some dedicated NZW column such taht corset should compile the above down to

(=! (* COL NZW) 1)

There will be times where for other reasons COL already has an inverse column. But at other times it won't. And it's kind of wastefull to introduce the associated inverse column COL_inv $\iff$ (inv COL) which must satisfy 2 degree 3 constraints

( COL_inv * COL - 1) * COL_inv = 0
( COL_inv * COL - 1) * COL     = 0

if we can just opportunistically use one of a fixed number of NZW columns and verify 1 degree 2 constraint

NZW_k * COL = 1

as above.

Implementation

The idea would be to have a reservoir NZW_1, ..., NZW_r of such columns. The number r would be obtained through Corset's analysis of the constraints. The basic idea being: go through the constraints and determine

• how many is-nonzero constraints can simultaneously be active
• how many actually apply to columns where for other reasons we have had to introduce an inverse column (in which case we can simply use this inverse at that point to verify the nonzeroness constraint)
• take the maximum of that over all remaining "not yet covered" constraints in a given module, name it r, and introduce as many NZW columns as necessary.

The next step would then be to opportunistically use these NZW columns to replace the constraints (is-nonzero COL) as indicated above by using k, the index of the "first available NZW column", and replacing it with (=! (* COL NZW_k) 1)

[letypequividelespoubelles]

What would be the difference with (eq! (~ COL) 1) ?