z3 - 輸送現象の問題をオンラインで Z3Py を使用して解決することに関する質問

Question

トランスポート現象の特定の問題は、次のコードを使用して解決されます。

T_max, T_0, S, R, k, I, k_e, L, R, E, a = Reals('T_max T_0 S R k I k_e L R E a')
k = a*k_e*T_0
I = k_e*E/L
S = (I**2)/k_e
eq = T_0 + S* R**2/(4*k)
print eq
equations = [
T_max == eq,
]
print "Temperature equations:"
print equations
problem = [
R == 2, L == 5000,
T_0 == 20 + 273,
T_max   == 30 + 273, k_e == 1,
a == 2.23*10**(-8), E > 0
]
print "Problem:"
print problem 
print "Solution:"
solve(equations + problem)

このコードをオンラインで使用して取得します

この出力は正しい答えを示しますが、コードには 2 つの問題があります。a) "eq" という名前の式が完全に単純化されていないため、 k_e に任意の値を指定する必要があります。私の質問は次のとおりです: k_e が「eq」から削除されるような方法で式「eq」を単純化するにはどうすればよいですか?

その他の例: チューブの半径を決定するには

コード：

def inte(n,a,b):
return (b**(n+1))/(n+1)-(a**(n+1))/(n+1)
P_0, P_1, L, R, mu, q, C = Reals('P_0 P_1 L R mu q C')
k = (P_0 - P_1)/(2*mu*L)
equations = [0 == -k*inte(1,0,R) +C,
q == 2*3.1416*(-(k/2)*inte(3,0,R) + C*inte(1,0,R))]
print "Fluid equations:"
print equations
problem = [
L == 50.02/100, mu == (4.03*10**(-5)),
P_0 == 4.829*10**5, P_1==0,
q   == 2.997*10**(-3), R >0
]
print "Problem:"
print problem 
print "Solution:"
solve(equations + problem)

出力：

Fluid equations:
[-((P_0 - P_1)/(2·mu·L))·(R2/2 - 0) + C = 0, q =
3927/625·
(-(((P_0 - P_1)/(2·mu·L))/2)·(R4/4 - 0) + C·(R2/2 - 0))]
Problem:
[L = 2501/5000, mu = 403/10000000, P_0 = 482900, P_1 = 0, q = 2997/1000000, R > 0]
Solution:
[R = 0.0007512843?,
q = 2997/1000000,
P_1 = 0,
P_0 = 482900,
mu = 403/10000000,
L = 2501/5000,
C = 3380.3149444289?]