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.