No warning when no quantifiers are used in quantified logic

[mpreiner]

It would be great if Dolmen warns if no quantifiers are used, but a quantified logic was specified:

For example for

(set-logic BV)
(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))
(assert (= a b))
(check-sat)

Dolmen parses the benchmark without any warning, however, it'd be great if it would inform the user that QF_BV would be sufficient for the logic.

[Gbury]

I'll add that warning (maybe behind a cli flag, but I'm not sure yet).

[hansjoergschurr]

I wonder if this fits into the "find minimal logic" feature. The warning would be emitted on the (set-logic ...) line.

[Gbury]

This would indeed fit into the "minimal logic" feature, considering that dolmen would ultimately warn when a problem is set in a logic that is not the minimal one for the problem. However, the minimal logic detection will likely take some time to be implemented (optimistically, i'd like to do it within about a year, but it's a very optimistic deadline), so the question is really whether it's okay to wait that long to have this warning.

[Gbury]

A first implementation of minimal logic detection is in #211. I'll probably add a warning that can be triggered (and made fatal if wanted) when the input logic of a problem is not minimal.