z3 fails with this system of equations

Over the years I keep track of solving technology - and I maintain a blog post about applying them to a specific puzzle - the "crossing ladders".

To get to the point, I accidentally found out about z3, and tried putting it to use in the specific problem. I used the Python bindings, and wrote this:

$ cat  laddersZ3.py
#!/usr/bin/env python
from z3 import *
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
e = Int('e')
f = Int('f')
solve(
    a>0, a<200,
    b>0, b<200,
    c>0, c<200,
    d>0, d<200,
    e>0, e<200,
    f>0, f<200,
    (e+f)**2 + d**2 == 119**2,
    (e+f)**2 + c**2 == 70**2,
    e**2 + 30**2 == a**2,
    f**2 + 30**2 == b**2,
    a*d == 119*30,
    b*c == 70*30,
    a*f - 119*e + a*e == 0,
    b*e - 70*f + b*f == 0,
    d*e == c*f)

Unfortunately, z3 reports...

$ python  laddersZ3.py
failed to solve

The problem does have at least this integer solution: a=34, b=50, c=42, d=105, e=16, f=40.

Am I doing something wrong, or is this kind of system of equations / range constraints beyond what z3 can solve?

Thanks in advance for any help.

UPDATE, 5 years later: Z3 now solves this out of the box.

Solution

You can solve this using Z3 if you encode the integers as reals, which will force Z3 to use the nonlinear real arithmetic solver. See this for more details on the nonlinear integer vs. real arithmetic solvers: How does Z3 handle non-linear integer arithmetic?

Here's your example encoded as reals with the solution (z3py link: http://rise4fun.com/Z3Py/1lxH ):

a,b,c,d,e,f = Reals('a b c d e f')
solve(
a>0, a<200,
b>0, b<200,
c>0, c<200,
d>0, d<200,
e>0, e<200,
f>0, f<200,
(e+f)**2 + d**2 == 119**2,
(e+f)**2 + c**2 == 70**2,
e**2 + 30**2 == a**2,
f**2 + 30**2 == b**2,
a*d == 119*30,
b*c == 70*30,
a*f - 119*e + a*e == 0,
b*e - 70*f + b*f == 0,
d*e == c*f) # yields [a = 34, b = 50, c = 42, d = 105, e = 16, f = 40]

While the result is integer as you noted, and as what Z3 finds, Z3 apparently needs to use the real arithmetic solver to handle it.

Alternatively, you can leave the variables declared as integers and do the following from the suggestion at the referenced post:

t = Then('purify-arith','nlsat')
s = t.solver()
solve_using(s, P)

where P is the conjunction of the constraints (z3py link: http://rise4fun.com/Z3Py/7nqN ).