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

Question

在微软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)

取自 here .