Z3Py:随机结果(阶段选择)不是随机的? [英] Z3Py: randomized results (phase-selection) not random?

问题描述

我尝试使用位向量在模型值中获得随机结果，如 de Moura here 然后使用 Z3Py 而不是 SMTLIB.我将他的例子翻译成:

I tried to use bit vectors to get randomized results in model values like suggested by de Moura here but then with Z3Py instead of SMTLIB. I translated his example to:

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 后，执行结果也会相同

However, the result seems to always be the same, i.e. - repetitive checking with s.check() does not alter the result. - even after a restart of the python interactive shell the result of the execution will be the same

添加随机种子的更改不会改变结果:set_option('smt.random_seed', 123)

Adding a change of the random seed did not alter the results: set_option('smt.random_seed', 123)

有人知道为什么不能按预期工作吗?

Does anyone have an idea why is not working as desired?

提前致谢！

卡斯滕

推荐答案

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

This case is simply too simple. It's essentially solved by the preprocessor and never gets to a point where it needs to select a phase, so random phase selection has no effect. Leo's answer to the cited post is now a little bit out of date and Z3 has changed, so it doesn't immediately replicate using the latest unstable version because Z3 chooses to use a different solver. We can still get the random behavior if we force it to use the incremental solver by adding a (push) command though; here's an updated example that is seed dependent:

(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)

这篇关于Z3Py:随机结果(阶段选择)不是随机的?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！