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

Question

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

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

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

Answer 1

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

取自这里。