search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.36k stars 1.48k forks source link

max SMT #6640

Closed Elonsolmostafa1 closed 1 year ago

Elonsolmostafa1 commented 1 year ago

I'm working on project for solving constraints and I use Z3 as my solver but I want to get random solution so the approach I took depends on max SMT but Z3 solver that deals with max SMT is quite slow and I want to get solutions as fast as I can. Is there any solution to do that in faster way.

Note: I'm using optimizer class

NikolajBjorner commented 1 year ago

maxsmt for randomization is overkill. You can try repeated calls into z3 blocking subsets of previous solutions using assumption literals or clauses.