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
80 stars 17 forks source link

Support more Bit-Vector primitives in Alt-Ergo's native language #136

Closed hra687261 closed 1 year ago

Gbury commented 1 year ago

If I understand correctly, this PR adds a new builtin theory for the alt-ergo language, and this new theory coincides with the smtlib's one, is that correct ? This should be safe, considering that alt-ergo's native language currently allows shadowing (at least that's what dolmen implements), but there should be a matching addition to alt-ergo's repo to document that fact.

hra687261 commented 1 year ago

If I understand correctly, this PR adds a new builtin theory for the alt-ergo language, and this new theory coincides with the smtlib's one, is that correct ?

Yes!

but there should be a matching addition to alt-ergo's repo to document that fact.

Yes, it will be added in this PR: https://github.com/OCamlPro/alt-ergo/pull/554