如何从 Microsoft Z3 中获得随机结果? [英] How to get random results from Microsoft Z3?

问题描述

在微软 Z3 中，当我们尝试求解一个公式时，Z3 总是以相同的顺序返回结果，当有两个或多个可满足的解决方案时.

In Microsoft Z3, when we try to solve a formula, Z3 always returns the results in the same sequence, when there are two or more satisfiable solutions.

是否有可能从 Z3 中得到随机结果，使得对于相同的输入，它在不同的执行中会产生不同的输出序列.

Is it possible to get random results from Z3 so that for the same input, it will generate different output sequence in different execution.

请注意，我使用的是 C 或 C# API.我没有使用 smt2lib 使用 Z3.所以如果你能给我一个可以添加随机化的C或C#API函数示例，它会更有用.

Please note that, I am using C or C# API. I am not using Z3 using smt2lib. So if you can give me a C or C# API function example that can add randomization, it will be more useful.

推荐答案

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

取自此处.

这篇关于如何从 Microsoft Z3 中获得随机结果?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！