可以将实变量限制在两个范围之间吗？

Question

您可以将实变量限制在两个范围之间吗？

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

此示例为我返回unsat。

Answer 1

在这种情况下，sexpr类的Solver方法是您的朋友！

由于z3py绑定的类型非常弱，您跳了起来。调用Reals返回多个结果，您将这些结果分配给单个元素。也就是说，您的input变量现在是一个包含一个变量的列表。反过来，这会使整个程序变得毫无意义，因为您可以观察到自己：

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

此打印：

(assert true)
(assert false)

为什么？因为您的变量input是一个列表，并且类型提升的怪异规则决定了列表大于或等于-2但小于2。 （这完全是没有意义的，只是绑定的工作方式。没有韵律或理由应该是这种方式。有人可以说它应该进行更多的类型检查并给您一个适当的错误。但是我离题了。）

要解决，只需将您的Reals的呼叫更改为Real：

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

此打印：

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

sat
[input = 0]

这正是您想说的。