Z3解中的奇异变量值

Question

我在Z3中有下面的模型(粘贴http://research.microsoft.com/en-us/um/redmond/projects/z3/代码来尝试它)。网页界面给我一个解决方案，见下文。但是，当我通过.NET对同一个模型进行求解并使用value()获得变量值时，我得到了一个不同的输出，这是我所不理解的。正如你所看到的，我没有得到值，而是得到了表达式。我的问题是:如何在.NET中获得值？为了记录在案，我再次检查了我在.NET中构建的模型是否与这里粘贴的模型相同。我还看到了这篇文章：Post并尝试应用修复(将auto_config设置为false)，但这只会导致求解程序无法计算解决方案。

模型：

    Q311, Q411, Q431, QQ311, QQ411, QQ431, H11, H41 = Reals('Q311 Q411 Q431 QQ311 QQ411 QQ431 H11 H41')
solve(
Q411 + Q311 <= 155,
Q431 - Q311 <= -28.015,
-Q431 - Q411 <= -126.985,
-Q411 - Q311 <= -155,
-Q431 + Q311 <= 28.015,
Q431 + Q411 <= 126.985,
43.015 - H11 - 0.0031 * QQ311 * Q311 <= 0,
H41 - H11 - 0.0031 * QQ411 * Q411 <= 0,
H41 - 43.015 - 0.0031 * QQ431 * Q431 <= 0,
-43.015 + H11 + 0.0031 * QQ311 * Q311 <= 0,
-H41 + H11 + 0.0031 * QQ411 * Q411 <= 0,
-H41 + 43.015 + 0.0031 * QQ431 * Q431 <= 0,
QQ311 - Q311 <= 0,
QQ411 - Q411 <= 0,
QQ431 - Q431 <= 0,
-QQ311 + Q311 <= 0,
-QQ411 + Q411 <= 0,
-QQ431 + Q431 <= 0,
Q311 >= 0,
Q411 >= 0,
Q431 >= 0,
QQ311 >= 0,
QQ411 >= 0,
QQ431 >= 0,
H11 >= 0,
H41 >= 0,
show=True)

网络接口解决方案：

[Q411 = 83.5779688745?,
Q311 = 71.4220311254?,
Q431 = 43.4070311254?,
H11 = 27.2015697567?,
QQ311 = 71.4220311254?,
H41 = 48.8559280884?,
QQ411 = 83.5779688745?,
QQ431 = 43.4070311254?]

.NET解决方案：

Q311: (root-obj (+ (* 40000 (^ x 2)) (* 10158800 x) (- 929606391)) 2)
Q411: (root-obj (+ (* 40000 (^ x 2)) (* (- 22558800) x) 1606007609) 1)
Q431: (root-obj (+ (* 20 (^ x 2)) (* 6200 x) (- 306807)) 2)
QQ431: (root-obj (+ (* 20 (^ x 2)) (* 6200 x) (- 306807)) 2)
H11: (root-obj (+ (* 160000000000000000 (^ x 2)) (* 41281815903200000000 x) (- 1
241318258533436869359)) 2)
QQ311: (root-obj (+ (* 40000 (^ x 2)) (* 10158800 x) (- 929606391)) 2)
H41: (root-obj (+ (* 40000000000 (^ x 2)) (* (- 19162006800000) x) 8407015578762
89) 1)
QQ411: (root-obj (+ (* 40000 (^ x 2)) (* (- 22558800) x) 1606007609) 1)

Answer 1

在阅读了这个post之后，我能够理解输出。

我在上下文的配置中添加了{ "PP_DECIMAL“、"true"}，现在我得到了我预期的十进制值。