Is it possible to extract the upper and (or) lower bound of some numerical variables in Z3? Suppose there are some constraints on numerical variable x, and the cause of the constraints is that x must be in the interval [x_min, x_max]. Is there a way in Z3 to extract these bounds (x_min and x_max) (in case the solver calculates these values internally), without doing optimization (minimization and maximization).
2 Answers
You could try to increase Z3's verbosity, maybe you can find bounds in the output.
I doubt it, though: since Z3 is ultimately a SAT solver, any numerical solver that (tries to) decide satisfiability could be applied, but deciding satisfiability doesn't necessary require computing (reasonable) numerical bounds.
Out of curiosity: why would you like to avoid optimisation queries?
In general, no.
The minimum/maximum optimal values of a variable x provide the tightest over-approximation of the satisfiable domain interval of x. This requires enumerating all possible Boolean assignments, not just one.
The (Dual) Simplex Algorithm inside the T-Solver for linear arithmetic keeps track of bounds for all arithmetic variables. However, these bounds are only valid for the (possibly partial) Boolean assignment that is currently being constructed by the SAT engine. In early pruning calls, there is no guarantee whatsoever about the significance of these bounds: the corresponding domain for a given variable x may be an under-approximation, an over-approximation or neither (compared to the domain of x wrt. the input formula).
The Theory Combination approach implemented by a SMT solver can also affect the significance of the bounds available inside the LA-Solver. In this regard, I can vouch that Model-Based Theory Combination can be particularly nasty to deal with. With this approach, the SMT Solver may not generate some interface equalities/inequalities when the T-Solvers agree on the Model Value of an interface variable. However, this is counterproductive when one wants to know from the LA-Solver the valid domain of a variable x because it can provide an over-approximated interval even after finding a model of the input formula for a given total Boolean assignment.
Unless the original problem --after preprocessing-- contains terms of the form (x [<|<=|=|=>|>] K), for all possibly interesting values of K, it is hardly likely that the SMT solver generates any valid T-lemma of this form during the search. The main exception is when x is an Int and the LIA-Solver uses splitting on demand. As a consequence, the Boolean stack is not that much helpful to discover bounds either and, even if they were generated, they would only provide an under-approximation of the feasible interval of x (when they are contained in a satisfiable total Boolean assignment).
Related