fix: constraint explosion with logical connectives

[DavePearce]

For reasons which aren't completely clear to me, the following does not compile in any useful timeframe:

(defcolumns (X :i16) (Y :i16) (Z :i16))

(defun (bigun)
    (∨
     (∧ (== X 0) (== Y 1))
     (∧ (== X 1) (== Y 2))
     (∧ (== X 2) (== Y 3))
     (∧ (== X 3) (== Y 4))))

(defconstraint c1 ()
  (if (bigun)
      (== Z 0)))

Of course, we understand there is a potential explosion in the size of generated constraints. But, this seems a little out of whack!

[DavePearce]

Note also that the above can be implemented fairly efficiently like so:

(defconstraint c2a ()
  (if (== X 0)
     (if (== Y 1)
         (== Z 0)))

(defconstraint c2b ()
   (if (== X 1)
     (if (== Y 2)
         (== Z 0)))

(defconstraint c2c ()
   (if (== X 2)
     (if (== Y 3)
         (== Z 0)))

(defconstraint c2d ()
   (if (== X 3)
     (if (== Y 4)
         (== Z 0)))

[DavePearce]

One aspect to consider here is that it is probably not simplifying obvious cases away. For example (x==0) || (x!=0) or (x==0) && (x==1)

[DavePearce]

It is definitely not simplifying cases like this: X!=0 || X!=1 ==> 0.

Overall, when spurious cases are removed, we have a similar number of remaining constraints.