If with binary condition

[OlivierBBB]

Currently Corset doesn't take advantage of binary-ness of the condition when compiling constraints à la

corset debug "
(defcolumns
  (BIN :binary@prove)
  N
  Z)

(defconstraint example () (if-zero BIN
                                   (vanishes! Z)        ;; zero case
                                   (vanishes! N)))      ;; nonzero case" -xcNeeeeC

produces

=== Constraints ===

example :=
{
 (1 - BIN * C/INV[BIN]) * Z
 BIN * N
}

NORM[BIN] :=
|BIN| == BIN × C/INV[BIN]
BIN×(1 - BIN×C/INV[BIN]) = 0
C/INV[BIN]×(1 - BIN×C/INV[BIN]) = 0

=== Columns ===
  ID                                                                            Name  Type   ×                                              Reg.
   0                                                                             BIN     𝟙   1                                          r0/BINι1
   1                                                                               N     𝔽   1                                            r1/Nι1
   2                                                                               Z     𝔽   1                                            r2/Zι1
   3                                                                      C/INV[BIN]     𝔽   1                                   r3/C/INV[BIN]ι1

=== Computations ===
C/INV[BIN] = (inv BIN)

There are several issues here:

• BIN doesn't require the computation of C/INV[BIN]
• nor should there be NORM[BIN] constraints
• but there should be a binary constraint for BIN

---

Franklin suggested this fix

[DavePearce]

but there should be a binary constraint for BIN

Because it is marked binary@prove ... right?

[DavePearce]

With Franklin's patch we get the following constraints from the example above:

 (1 - BIN) * Z
 BIN * N

But, as I understand it, we should also have a binary constraint as well.

[DavePearce]

See #92 for further discussion around the binary@prove issue.