Get random results from Microsoft Z3 C or C# API

0
votes

We are using Microsoft Z3 C and C# API (I have 2 programs).

In Microsoft Z3, when we try to solve a formula, Z3 always returns the results in the same sequence, when there are two or more satisfiable solutions.

Is it possible to get random results from Z3 so that for the same input, it will generate different output sequence in different execution.

Please note that, I cannot use smt2 code directly. I this issue, people suggested to use "random_seed" and "smt.arith.random_initial_value" parameters.

(set-option :smt.arith.random_initial_value true)
(declare-const x Int)
(declare-const y Int)
(assert (> (+ x y) 0))
(check-sat-using (using-params qflra :random_seed 1))
(get-model)
(check-sat-using (using-params qflra :random_seed 2))
(get-model)
(check-sat-using (using-params qflra :random_seed 3))
(get-model)

This smt2 solution works and I have managed to verify it using rise4fun. But these parameters are not available in Z3 C or C# API.

In C code, we I try to set these parameters using function "Z3_set_param_value", I get warning like this.

WARNING: unknown parameter 'smt.arith.random_initial_value'
WARNING: unknown parameter 'random_seed'

Can anyone guide me how to use these parameters? Also, is there any other way I can get random results from Z3 c-api or C# api code execution?

1
z3

1 Answers

1
votes

Randomized results were never considered, but we can "trick" Z3 into doing a little bit of that by setting options like the random seeds. If you need multiple solutions, but not multiple & random solutions, just assert the negation of the first solution and ask Z3 to solve the problem again, with the added constraint.

Those particular options that are mentioned in the question, can be set via the API as well, but they have to be set on the right objects. As stated in the documentation (header file comments), Z3_set_param_value can only be used for those 10 options mentioned there. Other options have to be set on Z3_params objects which can later be handed over to tactics and solvers, using Z3_params_set_*. If needed, they can also be set by changing the global default value for those options via Z3_global_param_set.