嗨，我正在尝试通过非常基本的迭代过程找到具有一些约束的目标函数的最小值。问题是由于浮点问题程序永远不会终止。我需要精确到 15 位十进制数字，我不希望 z3 或 python 探索任何高于该精度的值。以下是代码：我通过Mathematica计算的准确结果是：a=1，b=2，c=3，d=4，e=5，f=6，目标函数对应的最小值是：2.06846* 10^-14。我可以计算出相同的结果吗？
以下是代码：（请复制粘贴运行，因为表达式很长）
from sympy import*
from z3 import*
#working simple optimization example
# Given formula and set of constraints (cons), find the model that minimize the value of X
# using at-most Max iterations.
def abs(X):
return If(X >= 0,x,-x)
def Opti(cons, X, Max):
#set_option(precision=15)
s = Solver()
s.add(cons)
last_model = None
i = 0
while True:
r = s.check()
if r == unsat:
if last_model != None:
return last_model
else:
return unsat
if r == unknown:
raise Z3Exception("failed")
last_model = s.model()
# if last_model[X]<0:
# last_model[X]=-last_model[X]
s.add(X < last_model[X])
i = i + 1
if (i > Max):
raise Z3Exception("Solution not found, maximum number of iterations was reached")
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
e = Int('e')
f = Int('f')
x = Real('x')
y= Real('y')
X = Real('X')
Y = Real('Y')
cons=[ a>0,b>0,c>0,d>0,e>0,f>0, x== (abs((3608946673948233*d)/4503599627370496 + (274464355232027*e)/2251799813685248 - (274464355232027*e**2)/(4*(562949953421312*e + 562949953421312*f - 5536725273124715)) - 1519633732185043491981133247305/1267650600228229401496703205376) + abs((4636666003778669*b)/9007199254740992 + (1118552746194141*c)/2251799813685248 + (29870012493936382538794142709149*b)/(9007199254740992*(9007199254740992*b + 9007199254740992*c - 6442131581095921)) + (7205863971378845991234609198861*c)/(2251799813685248*(9007199254740992*b + 9007199254740992*c - 6442131581095921)) - (4636666003778669*b*(b + c))/(9007199254740992*b + 9007199254740992*c - 6442131581095921) - (4474210984776564*c*(b + c))/(9007199254740992*b + 9007199254740992*c - 6442131581095921)) + abs((274464355232027*e)/2251799813685248 + (1519633732185043491981133247305*e)/(2251799813685248*(562949953421312*e + 562949953421312*f - 5536725273124715)) - (274464355232027*e*(e + f))/(4*(562949953421312*e + 562949953421312*f - 5536725273124715))) + abs((792979490709637*b)/1125899906842624 - (901702497811663*c)/2251799813685248 + (4891864612675574504296157138923*b)/(1125899906842624*(2251799813685248*b + 2251799813685248*c - 6168967381864879)) - (5562573297146236482969456283777*c)/(2251799813685248*(2251799813685248*b + 2251799813685248*c - 6168967381864879)) - (1585958981419274*b*(b + c))/(2251799813685248*b + 2251799813685248*c - 6168967381864879) + (901702497811663*c*(b + c))/(2251799813685248*b + 2251799813685248*c - 6168967381864879)) + abs((8431533077325893*b)/18014398509481984 - (708586604185451*c)/4503599627370496 + (54368167798740930523060826625213*b)/(18014398509481984*(1125899906842624*b + 1125899906842624*c - 6448194806345241)) - (4569104460954436146783095288691*c)/(4503599627370496*(1125899906842624*b + 1125899906842624*c - 6448194806345241)) - (8431533077325893*b*(b + c))/(16*(1125899906842624*b + 1125899906842624*c - 6448194806345241)) + (708586604185451*c*(b + c))/(4*(1125899906842624*b + 1125899906842624*c - 6448194806345241))) + abs((4474210984776564*c**2)/(9007199254740992*b + 9007199254740992*c - 6442131581095921) - (177126692422487*d)/1125899906842624 - (1118552746194141*c)/2251799813685248 + (4636666003778669*b*c)/(9007199254740992*b + 9007199254740992*c - 6442131581095921) + 7205863971378845991234609198861/20282409603651670423947251286016) + abs((2035957719017013*b**2)/(1024*(140737488355328*b + 140737488355328*c - 2249387656040967)) - (2035957719017013*b)/144115188075855872 - (2035957719017013*a)/144115188075855872 + (2939179565022695*b*c)/(64*(140737488355328*b + 140737488355328*c - 2249387656040967)) + 4579658161378192576066497971571/20282409603651670423947251286016) + abs((5056216978909333*b)/36028797018963968 + (3060017963484179*c)/4503599627370496 + (27994884333529598097197586465095*b)/(36028797018963968*(562949953421312*b + 562949953421312*c - 5536725273124715)) + (16942478794638475145271796383985*c)/(4503599627370496*(562949953421312*b + 562949953421312*c - 5536725273124715)) - (5056216978909333*b*(b + c))/(64*(562949953421312*b + 562949953421312*c - 5536725273124715)) - (3060017963484179*c*(b + c))/(8*(562949953421312*b + 562949953421312*c - 5536725273124715))) + abs((2939179565022695*c**2)/(64*(140737488355328*b + 140737488355328*c - 2249387656040967)) - (2230056655377591*d)/2251799813685248 - (2939179565022695*c)/9007199254740992 + (2035957719017013*b*c)/(1024*(140737488355328*b + 140737488355328*c - 2249387656040967)) + 6611354232449908862093204746065/1267650600228229401496703205376) + abs((3860418273669689*e)/9007199254740992 + (24892729062597149834655331100049*e)/(9007199254740992*(1125899906842624*e + 1125899906842624*f - 6448194806345241)) - (3860418273669689*e*(e + f))/(8*(1125899906842624*e + 1125899906842624*f - 6448194806345241))) + abs((4636666003778669*b**2)/(9007199254740992*b + 9007199254740992*c - 6442131581095921) - (4636666003778669*b)/9007199254740992 - (4636666003778669*a)/9007199254740992 + (4474210984776564*b*c)/(9007199254740992*b + 9007199254740992*c - 6442131581095921) + 29870012493936382538794142709149/81129638414606681695789005144064) + abs((8431533077325893*a)/18014398509481984 + (8431533077325893*b)/18014398509481984 - (8431533077325893*b**2)/(16*(1125899906842624*b + 1125899906842624*c - 6448194806345241)) + (708586604185451*b*c)/(4*(1125899906842624*b + 1125899906842624*c - 6448194806345241)) - 54368167798740930523060826625213/20282409603651670423947251286016) + abs((5981047056487669*e)/9007199254740992 + (13453693419063522919576994335923*e)/(9007199254740992*(140737488355328*e + 140737488355328*f - 2249387656040967)) - (5981047056487669*e*(e + f))/(64*(140737488355328*e + 140737488355328*f - 2249387656040967))) + abs((792979490709637*a)/1125899906842624 + (792979490709637*b)/1125899906842624 - (1585958981419274*b**2)/(2251799813685248*b + 2251799813685248*c - 6168967381864879) + (901702497811663*b*c)/(2251799813685248*b + 2251799813685248*c - 6168967381864879) - 4891864612675574504296157138923/2535301200456458802993406410752) + abs((4461181249195911*e)/9007199254740992 + (27520881610876789415202401309769*e)/(9007199254740992*(2251799813685248*e + 2251799813685248*f - 6168967381864879)) - (4461181249195911*e*(e + f))/(4*(2251799813685248*e + 2251799813685248*f - 6168967381864879))) + abs((708586604185451*c)/4503599627370496 + (5277591482040591*d)/9007199254740992 - (708586604185451*c**2)/(4*(1125899906842624*b + 1125899906842624*c - 6448194806345241)) + (8431533077325893*b*c)/(16*(1125899906842624*b + 1125899906842624*c - 6448194806345241)) - 4569104460954436146783095288691/5070602400912917605986812821504) + abs((2035957719017013*b)/144115188075855872 + (2939179565022695*c)/9007199254740992 + (4579658161378192576066497971571*b)/(144115188075855872*(140737488355328*b + 140737488355328*c - 2249387656040967)) + (6611354232449908862093204746065*c)/(9007199254740992*(140737488355328*b + 140737488355328*c - 2249387656040967)) - (2035957719017013*b*(b + c))/(1024*(140737488355328*b + 140737488355328*c - 2249387656040967)) - (2939179565022695*c*(b + c))/(64*(140737488355328*b + 140737488355328*c - 2249387656040967))) + abs((2230056655377591*d)/2251799813685248 + (5981047056487669*e)/9007199254740992 - (5981047056487669*e**2)/(64*(140737488355328*e + 140737488355328*f - 2249387656040967)) - 13453693419063522919576994335923/1267650600228229401496703205376) + abs((854371257949259*d)/9007199254740992 + (4461181249195911*e)/9007199254740992 - (4461181249195911*e**2)/(4*(2251799813685248*e + 2251799813685248*f - 6168967381864879)) - 27520881610876789415202401309769/20282409603651670423947251286016) + abs((854371257949259*d)/9007199254740992 - (901702497811663*c)/2251799813685248 + (901702497811663*c**2)/(2251799813685248*b + 2251799813685248*c - 6168967381864879) - (1585958981419274*b*c)/(2251799813685248*b + 2251799813685248*c - 6168967381864879) + 5562573297146236482969456283777/5070602400912917605986812821504) + abs((3060017963484179*c**2)/(8*(562949953421312*b + 562949953421312*c - 5536725273124715)) - (3608946673948233*d)/4503599627370496 - (3060017963484179*c)/4503599627370496 + (5056216978909333*b*c)/(64*(562949953421312*b + 562949953421312*c - 5536725273124715)) + 16942478794638475145271796383985/2535301200456458802993406410752) + abs((177126692422487*d)/1125899906842624 - (764299361349167*e)/2251799813685248 + (3057197445396668*e**2)/(9007199254740992*e + 9007199254740992*f - 6442131581095921) + 4923717053158911857783000447807/20282409603651670423947251286016) + abs((5277591482040591*d)/9007199254740992 + (3860418273669689*e)/9007199254740992 - (3860418273669689*e**2)/(8*(1125899906842624*e + 1125899906842624*f - 6448194806345241)) - 24892729062597149834655331100049/10141204801825835211973625643008) + abs((5056216978909333*b**2)/(64*(562949953421312*b + 562949953421312*c - 5536725273124715)) - (5056216978909333*b)/36028797018963968 - (5056216978909333*a)/36028797018963968 + (3060017963484179*b*c)/(8*(562949953421312*b + 562949953421312*c - 5536725273124715)) + 27994884333529598097197586465095/20282409603651670423947251286016) + abs((764299361349167*e)/2251799813685248 + (4923717053158911857783000447807*e)/(2251799813685248*(9007199254740992*e + 9007199254740992*f - 6442131581095921)) - (3057197445396668*e*(e + f))/(9007199254740992*e + 9007199254740992*f - 6442131581095921)))]
SOL= Opti(cons,x , 2)
print SOL