SMT-LIB - Quantifiers

[lykur...@gmail.com]

Hi everyone,

Recently, while I played around with quantifiers, I came across a little problem.
I would be glad, if you could help me.

When I use Boolector with the following SMT-LIB input:

(declare-fun test ((_ BitVec 4)) Bool)
(assert (forall ((x (_ BitVec 4))) (= (test x) true)))
(check-sat)

I get the output:
[btorcore] btor_check_sat: quantifiers with functions not supported yet

I know the input is not particular meaningful, nevertheless I wonder about the output as for other examples,
quantifiers and functions work together. Because of this I would like to know how far the support for quantifiers
goes - is my example only a special case or should I expect this output also for other inputs?  

I am using Boolector version 3.0.1-pre.

Thank you for your help.

[Mathias Preiner]

Hi,

Boolector supports quantifiers for bit-vectors only. There is no support for in uninterpreted functions or arrays yet. In some cases Boolector might be able to eliminate all UFs and/or arrays so that you end up with a pure quantified bit-vector problem, which Boolector can still handle.

HTH,

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/boolector/f71dcdd5-fc14-4b06-a383-d36ed6addb1a%40googlegroups.com.