Z3: providing random solutions in solving

Question

I tried the following code at 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 produces a random number in the range [101,MAXINT) . for example, gets seed=1000 and suggests 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. Thus, decisions 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 choosing a 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)