Can you limit a real variable between two bounds?

Question

Can you limit a real variable between two bounds?

    s = Solver()
    input = Reals('input')
    s.add(input >= -2, input <= 2)

This example return unsat for me.

Answer 1

In cases like this, the sexpr method of the Solver class is your friend!

You're tripping up because of the extremely weakly typed nature of the z3py bindings. The call Reals returns multiple results, which you are assigning to a single element. That is, your input variable is now a list containing one variable. This, in turn, makes the whole program meaningless, as you can observe yourself:

from z3 import *
s = Solver()
input = Reals('input')
s.add(input >= -2, input <= 2)
print s.sexpr()

This prints:

(assert true)
(assert false)

Why? Because your variable input is a list, and the bizarre rules of type promotion decided that a list is greater than or equal to -2 but less than 2. (This is totally meaningless, just the way the bindings work. There's no rhyme or reason it should be this way. One can argue it should do more type-checking and give you a proper error. But I digress.)

To solve, simply change your call of Reals to Real:

from z3 import *
s = Solver()
input = Real('input')
s.add(input >= -2, input <= 2)
print s.sexpr()
print s.check()
print s.model()

This prints:

(declare-fun input () Real)
(assert (>= input (- 2.0)))
(assert (<= input 2.0))

sat
[input = 0]

which is exactly what you wanted to say.