Uninterpreted Sorts

18 views

Skip to first unread message

lykur...@gmail.com

unread,

Sep 1, 2019, 2:42:57 PM9/1/19

to Boolector

Hi everyone,

As Boolector supports the logic QF_UFBV and QF_UFBV provides free sort symbols, I wanted to use such symbols.

I tried to declare such sorts, but when I use for example "(declare-sort A)" as an input for Boolector, I get the output:

" 'declare-sort' not supported if it is not interpreted as a bit-vector "

How can I use uninterpreted sorts in Boolector with SMT-LIB2 inputs?

I am using Boolector version 3.0.1-pre.

Thank you very much for your help and sorry for this question

Mathias Preiner

unread,

Sep 3, 2019, 3:55:52 PM9/3/19

to bool...@googlegroups.com

Hi,

No worries, questions are always welcome!

Unfortunately, you can't use uninterpreted sorts in Boolector, it's not
supported. If you really need them, you can try using CVC4 or Yices.

Cheers,
Mathias

> --
> 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/c03f68ef-9fc9-4155-8cf9-c8f59476f776%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/c03f68ef-9fc9-4155-8cf9-c8f59476f776%40googlegroups.com?utm_medium=email&utm_source=footer>.