z3py，使用种子给出随机解

Question

from z3 import *

a = Int('a')

s = Solver()
s.add(a > 0)
set_option('smt.arith.random_initial_value', True)
set_option('auto_config', False)
set_option('smt.phase_selection', 5)
set_option('smt.random_seed', 1)

while s.check() == sat:
    m = s.model()
    print m[a]
    s.add(a != m[a])

结果是

1
2
3
4
5
...

我怎样才能使随机工作？ 请提供一个使用 z3py 的 Python 示例... 我已经知道如何在 smt 中执行此操作...但是我很难弄清楚如何将 smt 脚本转换为 python。

Answer 1

这似乎与Z3py, random different solution generation 重复

你想问一个不同的问题吗？如果有请修改问题，如果没有可以删除。