CODEWITHSUNDEEP
performancez3
Kausik Subramanian
Kausik Subramanian

Reputation: 25

Z3Opt: Finding a sub-optimal model within a time bound?

Does Z3Opt have a functionality to provide a sub-optimal solution for the objective within a certain time bound specified by the user?

Upvotes: 1

Views: 49

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

You can set a timeout or interrupt the opt context. You can then query the opt context for lower and upper bounds of the objective values. You can also query it for the current model and it will return the model for the best possible bound so far.

Upvotes: 1

Related Questions