tnelson/Forge

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

Opened this issue · 1 comments

tnelson commented

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 commented

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

  • 👍1