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的副本

您是否要提出其他问题？如果是，请修改问题，否则请删除。