z3 - 你能限制两个边界之间的实变量吗？

Question

你能限制两个边界之间的实变量吗？

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

这个例子为我返回了 unsat。

Answer 1

在这种情况下，Solver 类的 sexpr 方法就是您的 friend !

由于 z3py 绑定(bind)的类型极其弱的性质，您被绊倒了。调用 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。 (这完全没有意义，只是绑定(bind)的工作方式。没有押韵或理由应该是这样的。可以说它应该做更多的类型检查并给你一个正确的错误。但我离题了。)

要解决这个问题，只需将 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]

这正是你想说的。