Closed Halbaroth closed 3 months ago
The PR is ready for a second pass. I think we should test the legacy frontend with fpa
on Marvin before merging it.
I rebase this PR on #1117 to remove some polymorphic comparisons again ;)
No regression with the following combinations:
legacy
on ae-format
legacy
on ae-format-fpa
with --enable-theories fpa
dolmen
on ae-format
dolmen
on ae-format-fpa
with --enable-theories fpa
So this PR is ready for I hope a last check ;)
We don't manage correctly incremental type declarations. For instance the following input is accepted by the SMT-LIB standard:
(Notice that we switch the constructors
c1
andc2
in our second declaration of the typet
). AE answersunknown
onnext
but it answersunsat
if we remove the first declaration oft
.This PR fixes the issue for the new frontend only. So we got
unsat
with--frontend dolmen
but we still gotunknown
with--frontend legacy
.The solution consists in using the unique identifiers produced by
Dolmen
for the constructors, destructors and names of ADTs. To reduce as much as possible the amount of modification done in the legacy typechecker, I wrapped Dolmen's identifiers in a new moduleUid
. This module agrees withHstring
if we use the constructorsof_string
orof_hstring
and it uses Dolmen's identifiers if we use the constructorof_dolmen
. Of course, we'll get rid of this module as soon as we remove the legacy frontend.I didn't use a unique identifier for the constructor of builtin enumeration types. This case will be fixed after removing the legacy frontend.
This PR is supposed to be merged before #1093