CODEWITHSUNDEEP
z3
sean
sean

Reputation: 1832

Do Max-SMT benefit from incremental solving?

Do Max-SMT benefit from incremental solving? If yes, does Z3 support it? and how I can use it? Thanks.

Upvotes: 0

Views: 131

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8369

stackoverflow allows incremental questions, but Z3's optimization routines are non-incremental :-) The API exposes push/pop functions, but they are only for convenience. When it comes to solving, Z3 performs pre-processing on the entire set of asserted formulas and then invokes maximization routines. Even if there were no pre-processing, it is possibly an interesting question what it would mean to make core-(and correction set) based max-sat solvers incremental in a useful way.

Upvotes: 1

Related Questions