你的脚本使用了这个策略
s = Then('simplify','smt').solver()
该策略应用 Z3 简化器，然后执行 Z3 中可用的“通用”SMT 求解器。这个求解器是not完成非线性算术。它基于以下组合：单纯形、区间算术和 Grobner 基础。该模块的一大限制是它无法找到包含无理数的模型/解决方案。将来，我们将用 Z3 中提供的新非线性求解器替换该模块。
对于非线性算术，我们通常建议使用 Z3 中的 nlsat 求解器。这是一个完整的过程，通常对于不可满足和可满足的情况非常有效。您可以在以下位置找到有关 nlsat 的更多信息：本文。
要使用 nlsat，我们必须使用
s = Tactic('qfnra-nlsat').solver()
不幸的是，nlsat 会卡在你的例子中。它会卡住计算子结果求解过程中产生的非常大的多项式..
Z3 还有另一个处理非线性算术的引擎。该引擎将问题简化为 SAT。它仅对具有以下形式解决方案的可满足问题有效a + b sqrt(2) where a and b是有理数。使用该引擎，我们可以在很短的时间内解决您的问题。我将结果附加在帖子的末尾。要使用这个引擎，我们必须使用
s = Then('simplify', 'nla2bv', 'smt').solver()
EDIT此外，战术nla2bv对有理数进行编码a and b作为一对位向量。默认情况下，它使用大小为 4 的位向量。但是，可以使用选项指定该值nlsat_bv_size。这不是全局选项，而是提供给战术的选项nla2bv. Thus, nla2bv只能找到以下形式的解a + b sqrt(2) where a and b可以使用少量的比特进行编码。如果可满足的问题没有这种形式的解决方案，则此策略将失败并返回unknown.
END EDIT
你的例子还表明我们必须改进 nlsat，并使其作为模型/解决方案查找程序更加有效。
当试图表明问题没有解决方案时，当前版本会陷入困境。
我们意识到这些限制，并正在制定新的程序来解决这些问题。
顺便说一句，在 Python 前端，Z3 以十进制形式显示模型/解决方案。然而，一切都是经过精确计算的。以获得解决方案的精确表示。我们可以使用该方法sexpr()。例如，我将你的循环更改为
for d in m.decls():
print "%s = %s = %s" % (d.name(), m[d], m[d].sexpr())
在新循环中，我以十进制表示法和内部精确表示法显示结果。的含义(root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2)是多项式的第二次根2*x^2 + 12x - 7.
EDITZ3提供组合器用于创建不平凡的求解器。在上面的例子中，我们使用了Then执行不同战术的顺序组合。我们也可以使用OrElse尝试不同的策略。和TryFor(t, ms)尝试战术的t for ms毫秒，如果在给定时间内无法解决问题，则失败。这些组合器可用于创建使用不同策略来解决问题的策略。END EDIT
sat
Presenting results
traversing model...
s_2_p_p = 0.5355339059? = (root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2)
s_1_p_p = 0 = 0.0
s_init_p_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
s_2_p = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
s_1_p = 0 = 0.0
s_init_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
epsilon = 0 = 0.0
p_b2_s2_s_sink = 0.9142135623? = (root-obj (+ (* 4 (^ x 2)) (* 4 x) (- 7)) 2)
p_b2_s2_s_target = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
p_b2_s2_s_2 = 0 = 0.0
p_b2_s2_s_1 = 0 = 0.0
p_a2_s2_s_sink = 0 = 0.0
p_a2_s2_s_target = 0.8284271247? = (root-obj (+ (^ x 2) (* 4 x) (- 4)) 2)
p_a2_s2_s_2 = 0.1715728752? = (root-obj (+ (^ x 2) (* (- 6) x) 1) 1)
p_a2_s2_s_1 = 0 = 0.0
sigma_s2_b2 = 1 = 1.0
sigma_s2_a2 = 0 = 0.0
p_b1_s1_s_sink = 1 = 1.0
p_b1_s1_s_target = 0 = 0.0
p_b1_s1_s_2 = 0 = 0.0
p_b1_s1_s_1 = 0 = 0.0
p_a1_s1_s_sink = 1 = 1.0
p_a1_s1_s_target = 0 = 0.0
p_a1_s1_s_2 = 0 = 0.0
p_a1_s1_s_1 = 0 = 0.0
sigma_s1_b1 = 0 = 0.0
sigma_s1_a1 = 1 = 1.0
p_sinit_sink = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
p_sinit_target = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
p_sinit_2 = 0 = 0.0
p_sinit_1 = 0 = 0.0
s_sink = 0 = 0.0
s_target = 1 = 1.0
s_2 = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
s_1 = 0 = 0.0
s_init = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
EDIT您可以使用以下策略解决评论中的问题
s = Then('simplify', 'nlsat').solver()
这种策略将在几秒钟内解决问题，并在帖子末尾给出解决方案。正如我上面所说，nlsat已完成，但可能需要很长时间。
您的问题处于 Z3 当前版本可以自动决定/解决的边缘。我们可以结合不同的策略OrElse and TryFor使其更加稳定。例子：
s = OrElse(TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 1000),
TryFor(Then('simplify', 'nlsat'), 1000),
TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 10000),
Then('simplify', 'nlsat')).solver()
上面的策略尝试了nla2bv接近1秒，然后nlsat1秒，然后nla2bv10秒，最后nlsat没有超时。
我知道这不是一个理想的解决方案，但在下一个非线性算术求解器准备就绪之前，类似的变化可能是有用的解决方法。此外，Z3 还有许多其他策略可用于在我们调用之前简化/预处理问题nlsat.
END EDIT
s_init = 15/32
s_1 = 7/16
s_2 = 1/2
s_target = 1
s_sink = 0
p_sinit_1 = 1/2
p_sinit_2 = 1/4
p_sinit_target = 1/8
p_sinit_sink = 1/8
sigma_s1_a1 = 1/2
sigma_s1_b1 = 1/2
p_a1_s1_s_1 = 1/2
p_a1_s1_s_2 = 1/4
p_a1_s1_s_target = 1/8
p_a1_s1_s_sink = 1/8
p_b1_s1_s_1 = 1/2
p_b1_s1_s_2 = 1/4
p_b1_s1_s_target = 1/16
p_b1_s1_s_sink = 3/16
sigma_s2_a2 = 1/2
sigma_s2_b2 = 1/2
p_a2_s2_s_1 = 1/2
p_a2_s2_s_2 = 1/4
p_a2_s2_s_target = 11/64
p_a2_s2_s_sink = 5/64
p_b2_s2_s_1 = 3/4
p_b2_s2_s_2 = 1/32
p_b2_s2_s_target = 9/64
p_b2_s2_s_sink = 5/64
epsilon = 1/4
s_init_p = 1649/3520
s_1_p = 797/1760
s_2_p = 103/220
s_init_p_p = 1809/3904
s_1_p_p = 813/1952
s_2_p_p = 127/244
EDIT 2您的问题处于 Z3 在合理时间内可以解决的问题的边缘。非线性实数运算是可判定的，但非常昂贵。关于调试/跟踪 Z3 中发生的情况。以下是一些可能性：
我们可以使用以下命令启用详细消息：set_option("verbose", 10)。
该数字是详细级别：0 ==“无消息”，更高的数字==“更多消息”。
编译 Z3 支持跟踪。看这个帖子了解更多信息。
-
使用以下命令创建 Python 程序调用的 Z3 API 的日志open_log("z3.log")。应在任何其他 Z3 API 调用之前调用此命令。然后使用以下命令执行日志z3可执行内部gdb。
因此，您将能够停止执行并找到 Z3 卡在哪里。这nlsat求解器通常会卡在两个不同的地方：
计算子结果（过程psc_chain将在堆栈上），并且
分离具有代数系数的多项式的根（过程isolate_roots将在堆栈上）。
在我们将旧的代数数包替换为new one这样效率要高得多。不幸的是，您的问题似乎陷入了子结果步骤中。
另注：虽然nla2bv对于您的原始基准有效，您的新基准不太可能具有以下形式的解决方案a + b sqrt(2) where a and b是有理数。所以，使用nla2bv只是开销。战术nlsat假设问题出在 CNF 中。因此对于pastebin.com/QRCUQE10，我们必须调用tseitin-cnf在调用之前nlsat。另一种选择是使用“大”策略qfnra-nlsat。它在调用之前调用许多预处理步骤nlsat。然而，其中一些步骤可能会使某些问题更难解决。
结束编辑2
