如何在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()函数时。有没有办法使用绝对值函数来解决这个问题？或者有没有办法在Python中解决它，然后再传递给z3。我也尝试了sympy，但它没有起作用。

- user3196876

---

也许你可以利用这个事实：|x| > y 等同于 x > y 或 -x < -y，而 |x| < y 等同于 x < y 和 -x > -y（最简单的方法是在数轴上绘制定义域）。 - asmeurer

Answer 1

这里是一种方法：

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

- Nikolaj Bjorner

Answer 2

你可以转化你的问题，这样你就不需要使用abs了。

在你的特定问题中，'x = abs(2-y), x > 0'，所以'abs(2-y) > 0'。绝对值不能为负数，所以你只剩下'y != 2'。

因此，你可以删除x定义和与x相关的限制，只需添加'y != 2' - 这将是一个等价的问题。

如果你需要x的值，只需稍后从Python中的y的值获取即可。

- Sergii Dymchenko

---

我的表达式来自30*30的矩阵，我甚至不知道它们对于哪些y值会变为负数，因此添加一个约束条件以使系统不进入负域，例如(y！=2)，根本不可行。 - user3196876

Answer 3

绝对值的概念非常简单。你想知道距离零点的距离。一种方法是将所有负数项的符号取反。

if x<0:
    x=-x

- Reverend_Dude