Groups keyboard shortcuts have been updated
Dismiss
See shortcuts

Boolector get-unsat-cores

63 views
Skip to first unread message

mmoselhy

unread,
Apr 16, 2020, 6:17:16 PM4/16/20
to Boolector
Hello,

I have a questions. as i didn't find much support for boolector online..

Does it support getting unsat-cores ?  didn't find it in the apis in python neither in C
also tried smt2 with boolector executable and it seems it didnt support (get-unsat-core) .. am I missing something ?


Thanks

Aina Niemetz

unread,
Apr 16, 2020, 6:25:36 PM4/16/20
to bool...@googlegroups.com, mmoselhy
Hi,

I'm wondering if you are aware of Boolector's API documentation at
https://boolector.github.io/docs/index.html.

And no, Boolector does not support (get-unsat-core). However, it
supports to retrieve the set of failed assumptions via the API:
C:
https://boolector.github.io/docs/cboolector_index.html#c.boolector_get_failed_assumptions
You can also check for individual assumptions, if they are unsat:
C: https://boolector.github.io/docs/cboolector_index.html#c.boolector_failed
Python:
https://boolector.github.io/docs/boolector.html#pyboolector.Boolector.Failed

You can use this as a workaround.
And no, we don't support get_failed_assumptions in the Python API yet.
We might in the future.

HTH,
Aina
> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/boolector/01c4ca95-16d5-48d0-b15a-e5932fa4efcc%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/01c4ca95-16d5-48d0-b15a-e5932fa4efcc%40googlegroups.com?utm_medium=email&utm_source=footer>.

signature.asc

sbme...@gmail.com

unread,
Apr 16, 2020, 6:40:23 PM4/16/20
to Boolector
Thank you
Reply all
Reply to author
Forward
0 new messages