2

我尝试使用位向量在模型值中获得随机结果，例如 de Moura 建议的模型值，但随后使用 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)

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

提前致谢！

卡斯滕

4

1 回答 1

3

这个案子简直太简单了。它本质上是由预处理器解决的，并且永远不会到达需要选择相位的地步，因此随机相位选择没有效果。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)
于 2014-06-23T12:29:36.240 回答