Can we ask Z3 to maximize the value of arguments to `hypothesis.target()`?

[Zac-HD]

Talking to a friend about using hypothesis+crosshair as an easy-to-use Z3 interface, my main caveat was that we can find counterexamples but not use Z3's optimization power. But if we hacked on this a bit, maybe we could...

Obviously it'd only work for cases where hypothesis.target() is called with a symbolic object, but so long as we let you add a shim to report those cases I think this would work!

[pschanely]

Interesting; IIUC, upon seeing target(), we would materialize the argument to its largest satisfiable value at that point?

Honestly, you wouldn't even need to provide a hook; I could intercept this call in the same way that we intercept everything else.

Shouldn't be hard to add. CrossHair already ships with a not-officially documented search command that can optionally look for inputs that minimizes your function's return value:

% cat example.py

def schedule_jobs(job_assignments: list[int]):
    num_processors = 3
    job_durations = [1, 1, 2, 3, 5, 5, 6, 12]
    if (
            len(job_assignments) == len(job_durations) and
            all(0 <= a             for a in job_assignments) and
            all(a < num_processors for a in job_assignments)
    ):
        duration_per_processor = [
            sum(d for i, d in enumerate(job_durations) if job_assignments[i] == p)
            for p in range(num_processors)
        ]
        return max(duration_per_processor)
    return 9999

% python -m crosshair search example.schedule_jobs --optimization=minimize_int --max_uninteresting_iterations=200
{"job_assignments": [2, 0, 2, 2, 0, 2, 0, 1]}

I'm not using the official optimization though (IIRC, I think it's incompatible with some of the theories that we otherwise need); instead, it just calls the solver repeatedly and performs a binary search for the minimal satisfiable solution.