Z3:提供解决方案的随机解决方案

Question

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

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

结果总是如此a=101.我在答案中需要一些随机性,它会产生一个范围内的随机数[101,MAXINT).例如得到一个seed=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)