在这个例子中： http://pastebin.com/QyebfD1p Z3和cvc4回归“未知”作为检查SAT的结果。 两者都是不看好的原因非常详细，有没有一种方法，使Z3更详细的关于其执行？
Answer 1:
你的脚本使用战术
s = Then('simplify','smt').solver()
这种战术应用Z3简化器，然后执行一个“通用” SMT在Z3可解算器。 这个求解器是不完整的非线性算法。 它是基于一个组合：单纯，区间运算和Grobner基。 其中该模块的大限制是它不能找到包含无理数款/解决方案。 在未来，我们将更换该模块与Z3提供新的非线性求解器。
对于非线性算法，我们通常建议在Z3提供的nlsat求解。 这是一个完整的过程，通常是对不可满足和满足的情况下很有效。 你可以找到更多关于nlsat在这篇文章 。 要使用nlsat，我们必须使用
s = Tactic('qfnra-nlsat').solver()
不幸的是，nlsat会陷入你的榜样。 它会卡住计算Subresultants解决过程中产生了很大的多项式的..
Z3还有另一个引擎来处理非线性算法。 这台发动机降低了问题饱和 它是仅在具有形式的解决方案可满足的问题的有效a + b sqrt(2)其中a和b是有理数。 使用这个引擎，我们可以在很短时间内量解决您的问题。 我在附后的最终结果。 要使用这个引擎，我们不得不使用
s = Then('simplify', 'nla2bv', 'smt').solver()
EDIT此外，战术nla2bv编码有理数a和b为一对的位向量。 默认情况下，它使用大小4的比特向量。然而，此值可以使用选项来指定nlsat_bv_size 。 这不是一个全球性的选择，但是提供给策略选项nla2bv 。 因此， nla2bv只能找到形式的解决方案a + b sqrt(2)其中a和b可以用一个小数目的位进行编码。 如果满足的问题没有这种形式的解决方案，这种战术将失败，并返回unknown 。 编辑完
你举的例子也表明，我们以提高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 。
编辑 Z3提供组合程序创建非平凡解算器。 在上面的例子中，我们使用Then执行不同的策略的顺序组合。 我们也可以使用OrElse尝试不同的战术。 和TryFor(t, ms)尝试战术t的ms毫秒，如果问题不能在给定的时间内解决故障。 这些组合子可以用于创建用于解决问题的不同的战略战术。 编辑完
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)
编辑您可以通过使用策略解决您的评论的问题
s = Then('simplify', 'nlsat').solver()
这种战术能解决问题的几秒钟，并产生在后的最后解决方案。 正如我前面所说， nlsat完成，但它可能需要很长的时间。 你的问题是什么Z3的当前版本可以决定/自动解决的边缘。 我们可以结合不同的战术OrElse和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秒钟，然后nlsat为1秒，然后nla2bv ，持续10秒，最后nlsat没有超时。
我知道这是不是一个理想的解决方案，但这样的变化可能是有用的解决方法，直到非线性算术下一求解器已准备就绪。 此外，Z3具有可以用于简化/预处理问题，我们调用之前许多其他的战术nlsat 。 编辑完
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
编辑2你的问题是在什么Z3可在合理时间内做了刘海。 非线性真正的算术是可判定的，但非常昂贵。 关于调试/跟踪什么是在Z3回事。 这里有一些可能性：
：我们可以使用下面的命令启用详细消息
set_option("verbose", 10)数目是详细级别：0 ==“没有消息”，并且数字越大==“更多的消息”。与用于支持跟踪编译Z3。 请参阅这篇文章以获取更多信息。
创建日志使用该命令的Python程序调用的API Z3的
open_log("z3.log")该命令应任何其他Z3 API调用之前被调用。 然后执行使用日志z3的可执行文件内gdb。 所以，你将能够停止执行并找到Z3被套牢。 该nlsat求解器通常被卡在两个不同的地方：计算subresultants（程序
psc_chain将在堆栈上），并分离具有代数系数多项式的根（步骤
isolate_roots将在堆栈上）。
问题2将尽快修复，之后我们用替换旧的代数数包新是更有效的。 不幸的是，似乎你的问题会卡在子结式的一步。
另注：虽然nla2bv是有效的原来的基准，它是不太可能的新标准将有形式的溶液a + b sqrt(2)其中a和b是有理数。 因此，使用nla2bv就是多余的。 这个策略nlsat假设是在CNF的问题。 因此，对于pastebin.com/QRCUQE10 ，我们必须调用tseitin-cnf调用之前nlsat 。 另一种选择是用“大”字诀qfnra-nlsat 。 它调用调用之前许多预处理步骤nlsat 。 然而，某些步骤可能使一些问题更难解决。
END EDIT 2
文章来源: Encoding returns “unknown”
