如何从Microsoft Z3获得随机结果？

发布时间：2020-12-14 02:47:20 所属栏目：Windows 来源：网络整理

导读：在Microsoft Z3中,当我们尝试求解公式时,Z3始终以相同的顺序返回结果,此时有两个或更多可满足的解决方案. 是否有可能从Z3获得随机结果,以便对于相同的输入,它将在不同的执行中生成不同的输出序列. 请注意,我使用的是C或C#API.我没有使用smt2lib使用Z3.因此,

在Microsoft Z3中,当我们尝试求解公式时,Z3始终以相同的顺序返回结果,此时有两个或更多可满足的解决方案.

是否有可能从Z3获得随机结果,以便对于相同的输入,它将在不同的执行中生成不同的输出序列.

请注意,我使用的是C或C#API.我没有使用smt2lib使用Z3.因此,如果您可以给我一个可以添加随机化的C或C#API函数示例,它将更有用.

解决方法

(set-option :smt.arith.random_initial_value true)
(declare-const x Int)
(declare-const y Int)
(assert (> (+ x y) 0))
(check-sat-using (using-params qflra :random_seed 1))
(get-model)
(check-sat-using (using-params qflra :random_seed 2))
(get-model)
(check-sat-using (using-params qflra :random_seed 3))
(get-model)

取自here.

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!