CODEWITHSUNDEEP
z3
mrd abd
mrd abd

Reputation: 858

Z3: Offering random solutions in solving

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?

Upvotes: 9

Views: 1936

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

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)

Upvotes: 4

Related Questions