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