(Unnecessary use of cardinality): Upper-bound too large for given BitWidth

[tnelson]

E.g.,

******************** testing ./forge-core/examples/booleanLogic.rkt
uncaught exception: "Upper bound too large for given BitWidth; Sig: #(struct:Sig Formula (relation 1 "Formula" (Formula) univ) #f #t #f (Var Not And Or)), Upper-bound: 8, Max-int: 7"

Right now we're always encoding bounds numerically, even when we don't have to.

[tnelson]

Note that Alloy encodes such bounds using some disj ... rather than counting.

[tnelson]

@k-mouline As I review our older issues, I'm wondering: is this causing any trouble for our theory-of-relations translation? Sometimes Forge will produce a cardinality constraint on the size of a sig. Alloy does something smarter: it produces a some disj atom0, atom1, ... constraint that has the same effect.

[tnelson]

This doesn't seem to be a performance gain in general -- negating the above is slow. Worth looking again into what Alloy does, as they are surely not doing something as inefficient as what I just tried.