python - 如何计算 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 但它不起作用。

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

Answer 2

你可以改变你的问题，所以你不需要abs.

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

因此，您可以删除 x 定义和与 x 相关的约束，只需添加 'y != 2' - 您将遇到同样的问题。

如果您需要 x 的值，只需稍后在 Python 中从 y 的值中获取它。

Answer 3

绝对值的概念非常简单。你想知道与零的距离。这样做的一种方法是翻转所有否定项的符号。

if x<0:
    x=-x