Z3Py:随机结果(阶段选择)不是随机的？

Question

我尝试使用位向量在模型值中获得随机结果，如 de Moura 建议的那样 here但随后使用 Z3Py 而不是 SMTLIB。我把他的例子翻译成:

from z3 import *
s = Solver()
x = BitVec('x', 16)
set_option('auto_config', False)
set_option('smt.phase_selection',5)
s.add(ULT(x,100))
s.check()
s.model()
s.check()
s.model()

然而，结果似乎总是一样的，即- 使用 s.check() 重复检查不会改变结果。- 即使在重新启动 python 交互式 shell 之后，执行的结果也是一样的

添加随机种子的变化并没有改变结果:set_option('smt.random_seed', 123)

有谁知道为什么没有按预期工作？

提前致谢!

卡斯滕

Answer 1

这个案例实在是太简单了。它基本上由预处理器解决，永远不会达到需要选择相位的程度，因此随机相位选择没有效果。 Leo 对所引用帖子的回答现在有点过时并且 Z3 已经更改，因此它不会立即使用最新的不稳定版本进行复制，因为 Z3 选择使用不同的求解器。如果我们通过添加(推送)命令强制它使用增量求解器，我们仍然可以获得随机行为；这是一个依赖于种子的更新示例:

(set-option :auto_config false)
(set-option :smt.phase_selection 5)
(set-option :smt.random_seed 456)
(declare-const x (_ BitVec 16))
(assert (bvult x (_ bv100 16)))
(push)
(check-sat)
(get-model)
;; try again to get a different model
(check-sat)
(get-model)
;; try again to get a different model
(check-sat)
(get-model)