z3 - Z3：在求解过程中提供随机解

Question

我尝试了以下代码http://rise4fun.com/z3/tutorial

(declare-const a Int)
(assert (> a 100))
(check-sat)
(get-model)

结果总是a=101。我需要一些随机性的答案，它会在 range 中产生一个随机数[101,MAXINT)。例如获取 aseed=1000并提供a=12344. 为seed=2323优惠a=9088765和......

我应该在这个简单的代码中添加什么？

Answer 1

线性算术求解器基于 Simplex 算法。因此，解决方案不会是随机的。位向量求解器基于 SAT，您可以通过在位向量算术中对问题进行编码并选择随机相位选择来获得“随机”解。这是一个示例（也可在此处获得）：

(set-option :auto-config false)
(set-option :phase-selection 5) ;; select random phase selection
(declare-const a (_ BitVec 32))
(assert (bvugt a (_ bv100 32))) ;; a > 100 as a bitvector constraint
(check-sat)
(get-model)
;; try again
(check-sat)
(get-model)
;; try again
(check-sat)
(get-model)