search

usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

Dedicated class for unsat cores #754

Closed Tomaqa closed 2 months ago

Tomaqa commented 2 months ago

This allows to do more stuff with unsat cores in the future, or even build a class hierarchy.

Tomaqa commented 2 months ago

I removed const because I was afraid that for example minimal unsat cores may require some non-const operations such as checking unsatisfiability. It can be done with a standalone copy of the solver, but I am not sure if it would be efficient. Do you think keeping it const is important?

blishko commented 2 months ago

In your example, checking unsatisfiability would definitely have to be done in a separate solver. Trying to do that with the same solver would be quite messy. So yes, I think it is important.