CODEWITHSUNDEEP
constraintsz3
cschormann
cschormann

Reputation: 11

z3: How to identify conflicts in an unsat model?

In an interactive scenario, user actions cause constraints to be created. These constraints are then evaluated using the Microsoft z3 solver. When all the constraints are good, I can extract the resolved values using (get-model) and all is good.

When user actions result in an over-constrained model (i.e. conflicting constraints), is there a way how to identify which of the input asserts actually cause the conflict that leads to the unsat result? I'd like to use this information to provide UI to users that guides them to choose among conflicting demands they have made in their model.

Upvotes: 0

Views: 294

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

You're looking for unsatisfiable cores, which Z3 supports; see smtc_core for an example.

Upvotes: 2

Related Questions