Defining bounded integers in z3

Question

Is there a smart way to define bounded integers in Z3?

For example, lets say I want to define an integer variable "x" that can take values from [1,4]. I can do the following (I am using the Java API)

IntExpr x = ctx.mkIntConst("x");
solver.add(ctx.mkGT(x, ctx.mkInt(0))); // (assert (> x 0))
solver.add(ctx.mkLT(x, ctx.mkInt(5))); // (assert (< x 5))

However, I wonder if there is a smarter way to do this? Something that can automatically put upper/lower bounds on variables upon declaration. I came accross enumerations, but I am not sure if that is the best choice.

Thanks

Answer 1

If they are powers of two, just use bit-vectors. Otherwise there's no easy way to do it (i.e., you are doing it right).