如何在z3或z3py中计算绝对值

Question

我一直在尝试解决一个小问题，这个问题涉及到一些数值的绝对值。在 z3 这个工具里，没有支持 abs() 这个函数。在 Python 里是有这个函数的，但最终我还是得把它传递给 z3py。请问有没有办法让我能从 Python 传递带有绝对值运算符的项到 z3，或者有没有其他的解决办法？下面是一个小例子的代码。

`
x = Int('x')
y = Int('y')

x= abs(2-y)
s=Solver()
s.add(x>0)
s.add(y>0)
s.check()
m=s.model()
print m`

答案应该是 y=1，这个结果是在去掉 abs() 的情况下得到的。有没有办法用绝对值函数 abs() 来解决这个问题？或者有没有办法让我在 Python 中解决这个问题，然后再传递给 z3。我也试过使用 sympy，但没有成功。

Answer 1

绝对值的概念其实很简单。你想知道一个数离零有多远。实现这个的一个方法就是把所有负数的符号变成正号。

if x<0:
    x=-x

Answer 2

你可以把问题转化一下，这样就不需要用到 abs 了。

在你的问题中，'x = abs(2-y), x > 0'，所以就变成了 'abs(2-y) > 0'。绝对值是不会是负数的，所以你只需要关注 'y != 2' 这个条件。

这样你就可以去掉 x 的定义和与 x 相关的限制，只需要加上 'y != 2'，这样问题就变得一样了。

如果你需要 x 的值，可以在 Python 中根据 y 的值再算出来。

Answer 3

这里有一种方法：

x = Int('x')
y = Int('y')

def abs(x):
    return If(x >= 0,x,-x)

s=Solver()
s.add(x == abs(y-2))
s.add(x>0)
s.add(y>0)
s.check()
m=s.model()
print m