Z3: Offering random solutions in solving

Question

I tried the following code in http://rise4fun.com/z3/tutorial

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

the result is always a=101. I need some randomness in the answer that it produce a random number in the range [101,MAXINT). for example gets a seed=1000 and offers the a=12344. for seed=2323 offers a=9088765 and ... .

what should i add to this simple code?

Answer 1

The linear arithmetic solver is based on the Simplex algorithm. So, the solutions will not be random. The bit-vector solver is based on SAT, you can get "random" solutions by encoding your problem in bit-vector arithmetic and selecting random phase selection. Here is an example (also available 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)