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
...

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

Answer 1

这似乎是

的副本

您是想问其他问题吗？如果是请修改问题，如果不是可以删除。

z3py，使用种子给出随机解

z3py, give random solution using seed

python

z3

z3py