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
Unfortunately there isn't a "good" way to model such constraints. Bitvectors go far, assuming you're OK with machine arithmetic (i.e. modular) and your range fits nicely, as previously stated. Here's a previous related discussion: Is there an UnsignedIntSort in Z3?.
To properly support what you want, one would need predicate-subtyping. Theorem provers such as PVS and older versions of Yices (pre SMTLib variants in the 1.X series) supported such fancy types, with varying degrees of automation. If you need to stick to a modern SMT solver, you've no choice but to pepper your code with lots of bound-constraints, unfortunately. It can get pretty ugly pretty quick, of course, since you'd have to check bounds after every operation and define what it means to over/underflow. A proper theorem prover might be a better choice if respecting the bounds is essential.