在z3py中使用checksat的等价物是什么？

Question

我一直在努力实现与本文完全相同的目标。 Z3 randomness of generated model values

除此之外，答案是在smt中，如何在python中使用z3py中的check-sat-using？ 有人能帮我把这段代码翻译成python代码吗

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

Answer 1

在SMTLib接口中，check-sat-using是告诉z3使用哪种策略的一种方式。使用z3py时，直接使用策略语言并显式创建解算器。因此，在某种意义上，z3py中没有对应于check-sat-using的调用。相反，你会得到一个完整的战术语言，它更加灵活和强大

有关示例，请参见：http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

还要注意check-sat-using在某种意义上结合了战术和设置，在z3py中，您使用set_param来实现参数设置，并使用战术语言来表达您想要使用的策略

一般来说，不要试图在SMTLib和Z3Python接口之间进行“转换”。虽然两者都可以表示相同的查询，但编程模型不同，尝试“逐个命令”地翻译会导致代码不惯用且难以维护。相反，如果您想使用Z3py，只需了解那里的工作方式，记住它们可能与SMTLib领域有很大的不同。这是一个很好的资源，可以通读以帮助您开始：http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/