I wonder if there is a way to obtain all the results of one constraint problem

[RUOKUNH]

I have the need to sample solution for a constraint problem, but Z3 gives only one solution each time.
I wonder if there is a way to obtain all the results of one constraint problem with limited problem. Or different results each time I run Z3 on the same setting with more than one solution.
For now my method is to add the constraint that "same result is not allowed" to the solver each time I got a new solution, but this will make the solver running process unbearably slow after sampling a lot of results.
Anyone have the idea for enhancing the performance of Z3 on my problem (any tricks or only research ideas), or recommending another tools more suitable for my problem?
THANKS A LOT!

[NikolajBjorner]

There are various papers that describe samplers on top of SAT and even SMT solvers.
Some recent papers from Kuldeep Meel, Mate Soos and others.
In some instances you may be able to use the user propagator (see the examples directory that contains an n-queens example) to block parts of the search space using clauses that are amenable to garbage collection (so the same solution could be revisited). Disabling restarts and forcing backtracking is a way to force the solver to visit more of the solution space systematically (Siboelle Moelle's thesis)