search

Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
79 stars 16 forks source link

No warning when no quantifiers are used in quantified logic #76

Open mpreiner opened 3 years ago

mpreiner commented 3 years ago

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 commented 3 years ago

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

hansjoergschurr commented 3 years ago

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

Gbury commented 3 years ago

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 commented 4 months ago

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.