CODEWITHSUNDEEP
z3
Ofer strichman
Ofer strichman

Reputation: 171

get intermediate results from z3opt

solving a large optimization problem with z3, which is not likely to reach optimum in a reasonable amount of time. Any way that I can get intermediate solutions ? perhaps set an internal time-out so it gives me the best solution it found so far ? Thanks, Ofer

Upvotes: 2

Views: 214

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

You can interrupt Z3 from the API directly or by setting a timeout. From the text front-end you can interrupt it (CTRL^C) or set a timeout. It returns a range of upper/lower bound and model of the best bound found so far.

Upvotes: 1

Related Questions