How to perform quantifier elimination using Z3Py and an idea from Taylor in the case of an electrical network

Question

Please consider the following electrical network

the SAT problem for this electrical network is

This problem is solved using Z3Py online using the following code:

r01, r02, r12, r13, r23 = Reals('r01 r02 r12 r13 r23')
i0, i01, i02, i12, i13, i23, i3 = Reals('i0 i01 i02 i12 i13 i23 i3')
u0, u1, u2, u3 = Reals('u0 u1 u2 u3')
r01=1000
r02 = 100
r12 = 300
r13 = 47000
u0 = 0
u3 = 12
s = Solver()
s.add(u1-u0==r01*i01, u2-u0==r02*i02, u2-u1==r12*i12,u3-u1==r13*i13, u3-u2==r23*i23)
s.add(-i0 + i01 + i02 ==0, -i01+i12+i13==0,-i02-i12+i23==0,-i13-i23+i3==0)
s.add(i3==i0)
s.add((u1-u0)*i01<=0.25, (u2-u0)*i02<=0.25, (u2-u1)*i12<=0.25,(u3-u1)*i13<=0.25,  (u3-u2)*i23<=0.25)         
s.add(r23 > 0)
print s
print s.check()
m = s.model()
set_option(rational_to_decimal=True)
print m

and the output is:

sat
[u1 = 1,
r23 = 824.4299674267?,
i02 = 0.0122978723?,
i12 = 0.0007659574?,
u2 = 1.2297872340?,
i23 = 0.0130638297?,
i3 = 0.0132978723?,
i0 = 0.0132978723?,
i01 = 0.001,
i13 = 0.0002340425?]

Finally using Z3Py we solve a linear problem of quantifier elimination:

g = Goal()
g.add(Exists([i0, i01, i02, i12, i13, i23, i3, u1, u2], And(u1-u0==r01*i01, u2-u0==r02*i02, u2-u1==r12*i12,
         u3-u1==r13*i13, u3-u2==r23*i23,-i0 + i01 + i02 ==0, -i01+i12+i13==0,-i02-i12+i23==0,
         -i13-i23+i3==0,i3==i0,r23 > 0, (u1-u0)<=7, (u2-u0)<=7, (u2-u1)<=7,
          (u3-u1)<=7, (u3-u2)<=7 )))
t = Tactic('qe')
print t(g)
print t(g).as_expr()
s1 = Solver()
s1.add(t(g).as_expr())
print s1.check()
m1 = s1.model()
print m1

and the corresponding output is:

[[∃x!5 :
¬(r23 ≤ 0) ∧
0.0107817589?·r23·x!5 + x!5 ≤ 0.1291856677? ∧
-0.0107817589?·r23·x!5 + -1·x!5 ≤ -0.1291856677? ∧
x!5 + 0.0107817589?·r23·x!5 ≤ 0.1291856677? ∧
r23·x!5 ≥ 2.9319148936? ∧
r23·x!5 ≥ 5 ∧
r23·x!5 ≥ -18.0972222222? ∧
r23·x!5 ≤ 5.5446808510? ∧
r23·x!5 ≤ 7]]

∃x!5 :
¬(r23 ≤ 0) ∧
0.0107817589?·r23·x!5 + x!5 ≤ 0.1291856677? ∧
-0.0107817589?·r23·x!5 + -1·x!5 ≤ -0.1291856677? ∧
x!5 + 0.0107817589?·r23·x!5 ≤ 0.1291856677? ∧
r23·x!5 ≥ 2.9319148936? ∧
 r23·x!5 ≥ 5 ∧
r23·x!5 ≥ -18.0972222222? ∧
r23·x!5 ≤ 5.5446808510? ∧
r23·x!5 ≤ 7

sat

[r23 = 68, x!5!54 = 0.0745376635?]

Run this example online here

Please let me know why Z3Py does not perform fully the quantifier elimination in the linear example; and if the original non-linear problem of quantifier elimination could be solved using Z3Py online. Many thanks.

Answer 1

Using Redlog of Reduce is possible to solve the non-linear problem as follows:

Answer 2

Using Redlog of Reduce is possible to solve the linear problem as follows: