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, вы можете получить «случайные» решения, закодировав свою проблему в арифметике бит-вектора и выбрав случайный выбор фазы. Вот пример (также имеется here):

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