你能限制两个边界之间的实变量吗?
s = Solver()
input = Reals('input')
s.add(input >= -2, input <= 2)
这个例子为我返回了 unsat
。
最佳答案
在这种情况下,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]
这正是你想说的。
关于z3 - 你能限制两个边界之间的实变量吗?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/60442674/