1

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.
R71
  • 4,283
  • 7
  • 32
  • 60
  • I don't see how getting Z3 to print the range `[1,6]` of potential values for `x` is different from getting Z3 to print all valid models. Please clarify. Note that the question you linked to appears to differ from yours in that you'd like to find a simple representation for all models, whereas in the linked question, a simplified representation of an initial set of constraints is wanted. – Malte Schwerhoff Aug 12 '20 at 12:44
  • It matters if the range is high. Eg, if the range happens to be [1,10000], I dont want to enumerate all 10k answers to determine its range. – R71 Aug 12 '20 at 12:52
  • In the linked answer, it is simplifying all constraints on one side, ie on >= side. But I was asking for range, which is equivalent to simplifying constraints on both sides. – R71 Aug 12 '20 at 12:53
  • As mentioned in my answer, Z3 does not directly support what you're asking for. Enumerating of all possible answers is the only option you have. Together with filing a feature request (https://github.com/Z3Prover/z3/issues), of course :-) – Malte Schwerhoff Aug 12 '20 at 13:22
  • Thanks for confirming. BTW, the mentioned question has a non-python answer, is there a python equivalent for it? – R71 Aug 12 '20 at 13:23

2 Answers2

2

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.

alias
  • 28,120
  • 2
  • 23
  • 40
1

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:

Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71