Tune z3 to try lower numbers first
I have an smt model with several integers, all of which are limited between 0 and N. While it is possible that they will be N or close to N, they will almost always be close to 0. Maybe 80% of the time I need them to be 0.1 or 2 ... something like that.
Also, many integers can be ignored if some of the key integers take a lower value, so it seems to me that if I could tune z3 to start at the lower bound and try smaller models with lower values first, I might improve the time execution.
I tried to understand the options in "z3 -p" but couldn't find a way to tune the solution strategy in a way that suits my requests. Can z3 be configured to try lower numbers first?
source to share
In the context of standard Z3 usage, there is no real solution. I am currently developing optimization functions for Z3, which allows me to create queries to get min / max values. You can do this for several purposes. Unfortunately, getting real options can be quite costly, so it doesn't replace a simple heuristic handle.
source to share