CODEWITHSUNDEEP
z3z3py
R71
R71

Reputation: 4523

how to use z3 to get valid range of a variable

I want to find the range of valid values that a variable can have, given some constraints. Eg,

x = Int('x')
s = Solver()
s.add(x >= 1)
s.add(x < 5+2)

Is there some way that I can get z3 to print 1..6 for this variable?

I tried using the following, but range() applies only to declarations.

print("x.range():", x.range()) # this does not work

Note: 1. This question seems to ask the same, but I did not understand its answers, and I am looking for python answer.

  1. in reply to @Malte: I am not looking for all the answers, I just want to simplify multiple constraints in to a valid range. If constraints on both sides of the variable cannot be merged, then at least only on one side as is mentioned in above mentioned question.

Upvotes: 1

Views: 1870

Answers (2)

alias
alias

Reputation: 30428

This question comes up occasionally, and the answer isn't very trivial, unfortunately. It really depends on what your constraints are and exactly what you are trying to do. See:

Is it possible to get a legit range info when using a SMT constraint with Z3

And

(Sub)optimal way to get a legit range info when using a SMT constraint with Z3

Essentially, the problem is too difficult (and I'd say not even well defined) if you have multiple variables. If you have exactly one variable, you can use the optimizer to some extent, assuming the variable is indeed bounded. In case you have multiple variables, one idea might be to fix all but one to satisfying constants, and compute the range of that last variable based on the constant assignment to the others. But again, it depends on what you're really trying to achieve.

Please take a look at the above two answers and see if it helps you. If not, please show us what you tried: Stack-overflow works the best when you post some code and see how it can be improved/fixed.

Upvotes: 2

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

As a SAT/SMT solver, Z3 "only" needs to find a single model (satisfying assignment) to show that a formula is satisfiable. Finding all models is therefore not directly supported.

The question comes up regularly, though, and the solution is to repeatedly find and then block (assume in negated form) models until no further model can be found. For example, for your snippet of code:

x = Int('x')
s = Solver()
s.add(x >= 1)
s.add(x < 5+2)

result = s.check()

while result == sat:
  m = s.model()
  print("Model: ", m)
  
  v_x = m.eval(x, model_completion=True)

  s.add(x != v_x)
  result = s.check()

print(result, "--> no further models")

Executing the script yields the solution you asked for, albeit in a less concise form:

Model:  [x = 1]
Model:  [x = 2]
Model:  [x = 3]
Model:  [x = 4]
Model:  [x = 5]
Model:  [x = 6]
unsat --> no further models

In general,

  • you would have iterate over all variables (here: just x)
  • model completion is necessary for variables whose value doesn't affect satisfiability; since any value will do, they won't be explicit in the model

Related questions whose answers provide additional details:

Upvotes: 1

Related Questions