How to calculate Absolute value in z3 or z3py

Question

I have been trying to solve a small problem which includes absolute value of some terms. In z3 there is no support for abs() function. In python there is, but I eventually i have to pass it to z3py. Is there any way through which I can pass terms with absolute operator to z3 from python or is there any other way around? Following is the code for a small example.

`
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`

The answer should be y=1, which is the case when you remove abs(). Is there any way to solve this problem with absolute value function? abs(). Or is there any way that I can solve it in python and then I can pass it to z3. I tried sympy as well but its not working.

Answer 1

Here is one approach:

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

You can transform your problem so you don't need abs.

In your particular problem 'x = abs(2-y), x > 0', so 'abs(2-y) > 0'. Absolute value can't be negative, and you left with just y != 2.

So you can remove x definition and x-related constraints, and just add 'y != 2' - you'll have an equivalent problem.

If you need value of x, just get it from value of y later in Python.

Answer 3

The idea of absolute value is very simple. You want to know the distance from zero. One way of doing this is to flip on sign of all negative terms.

if x<0:
    x=-x