1

z3 returns the number of unsat clauses for a Max-SMT problem together with only one model. I wonder if I can list them all (e.g. using API).

sean
  • 1,632
  • 2
  • 15
  • 34

1 Answers1

0

As mentioned in this question, you can use the generated model to add a constraint to prevent the generated model and run the solver again. In your case however, I believe you will also need to check the number of constraints that are broken, after generating a new model, to ensure that you don't break your optimality constraints.

Community
  • 1
  • 1
dlshriver
  • 156
  • 1
  • 15