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

Add typing extensions, and the bvconv extension #208

Closed Gbury closed 8 months ago

Gbury commented 8 months ago

Should solve #205

This PR adds a notion of typing extensions, which allow to add new builtins for the typechecking. Fomr the point of view of the ocaml API, these do not add much compared to the already existing additional_builtins mechanism. They mainly represent a slightly more structured way to add new builtins. When using the dolmen binary, these extensions can be activated on the command line, using the new --ext option.

Currently, these is only a single extension: the bvconv extension, which adds the bv2nat and int2bv functions, as described in https://github.com/Gbury/dolmen/issues/205#issuecomment-1969393448

Therefore, examples of smtlib2 problems using either bv2nat or int2bv will now be able to typecheck using the following command-line:

dolmen --ext=bvconv problem.smt2
rod-chapman commented 8 months ago

Thanks. Let me know when it's merged.