search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Remove some polymorphic hashtables #1219

Closed Halbaroth closed 2 weeks ago

Halbaroth commented 3 weeks ago

We should not use polymorphic equality on expressions because they may contain recursive terms producing by Dolmen. This PR removes these dangerous hashtables.

Halbaroth commented 2 weeks ago

The purpose of this PR is to ensure that hashing terms will always terminate. I did not try to optimize the model generation. I believe that we hadn't self recursive terms before using Dolmen's terms in Symbols but I might be wrong.