I tried this:
import z3
n,x,y,z = z3.Ints('n x y z')
s = z3.Solver()
s.add(4/n==1/x+1/y+1/z)
s.add(x>0)
s.add(n>0)
s.add(y>0)
s.add(z>0)
s.check()
s.model()
and I get:
[x = 1, n = 2, z = 3, y = 1, div0 = [(1, 1) → 1, (4, 2) → 2, else → 0], mod0 = [(1, 3) → 1, else → 0]]
But 4/2 does not equal 1/1+1/1+1/3.
What am I doing wrong?
You've declared n, x, y, z as integers. So division is done as an integer, giving you 1/1 = 1 and 1/3 = 0; hence satisfying the equality 2=2.
The obvious thing to do is to use Real values for this problem.
Changing the declaration to:
n,x,y,z = z3.Reals('n x y z')
produces:
[z = 1, y = 1, n = 4/3, x = 1]
which does satisfy the equation you posed trivially.
In case you actually do want n, x, y, z to be integers; then you should convert them to reals before you divide, like this:
import z3
n,x,y,z = z3.Ints('n x y z')
s = z3.Solver()
s.add(4/z3.ToReal(n)==1/z3.ToReal(x)+1/z3.ToReal(y)+1/z3.ToReal(z))
s.add(x>0)
s.add(n>0)
s.add(y>0)
s.add(z>0)
print(s.check())
print(s.model())
This prints:
sat
[n = 4, x = 3, z = 3, y = 3]
again satisfying your constraints.