Creating random result in Z3

[AnonymousMonkey2021]

Hello, if I have a simple constraint 0<a<1000 Can Z3 provide random results for a?

I've seen a few different ways of doing it. Such as enumerating all the solutions of a. Every new solution is added to the constraints. e.g. a != 1..... Then randomly choose from the list of values. However, this does not work for constraints with infinite solutions.

I've also seen people using random-seed. However, random-seed doesn't seem to randomize results, but just simply providing a random seed for reproducibility purposes.

Is there any built-in ways for Z3 to randomize results such as for constraint a > 10?

[NikolajBjorner]

There isn't a principled way for integers. Z3 solves for integers using dual Simplex, which attempts to find solutions close to the boundary values. For propositional formulas one can set the parameter sat.phase to "random" (and probably play with restart frequency and other goodies). A principled approach works outside of the SAT solvers and involves adding xor constraints that control the parity of a combination of Boolean variables. I think you should try to pursue a principled approach outside of z3, by adding random constraints on the parity of bits in the integers. The i't bit in positive integer a is of course (a div 2^i) mod 2 and if you have a combination of integers and bit-positions you can constrain the sum of these to be even or odd. If the constraints are unsatisfiable you can remove literals from the unsat core.

[AnonymousMonkey2021]

@NikolajBjorner I am sorry for not able to reply to you quicker. Thank you so much for your reply, your answer is exactly what I needed!