Named lemmas in SMT-LIB format

[Halbaroth]

For debugging purposes, it is useful to be able to name lemmas as in the native language. By default, Dolmen names axioms with a string of the form hyp_#number where #number is a counter. It's fine for small files with few axioms but not very convenient for large files.

This PR uses the syntax (! ... :named ...) to be able to rename axioms.

Notice that using this feature has a slight effect on the behaviour of Alt-Ergo, which isn't desirable for a debugging tool. The reason is because Dolmen uses a mechanism of implicit definitions in presence of :named. For instance, the following input file:

(set-logic ALL)
(declare-fun f (Int Int) Int)
(assert (! (forall ((x Int)) (>= (f x x) 0)) :named foo))
(assert (< (f 0 0) 0))
(check-sat)

will produce a pack of definitions:

1. a definition of foo
2. an implicit definition of the underlying axiom

The foo variable will appear in the context and the equality foo = (forall ...) too.

I don't know how to prevent AE from doing that without breaking the get-assignment feature.

[bclement-ocp]

Notice that using this feature are a slight effect on the behaviour of Alt-Ergo, which isn't desirable for a debugging tool. The reason is because Dolmen uses a mechanism of implicit definitions in presence of :named. For instance, the following input file:
[...]
I don't know how to prevent AE from doing that without breaking the get-assignment feature.

This is not a choice Dolmen (or Alt-Ergo) has, this behavior is specified in the SMT-LIB standard (see 4.1.6).

This PR uses the syntax (! ... :named ...) to be able to rename axioms.

I think using :named here sort of makes sense, with this caveat you note that it introduces a variable. We could also have a custom tag (perhaps :lemma, or :debug-name if this is intended purely for debugging purposes).

[bclement-ocp]

Approving I will let you decide if you prefer a custom name instead of reusing :named.

[Halbaroth]

I didn't know we can create custom attribute. It's a better solution because I know exactly where to filter out the extra definition generated by Dolmen.