-
Notifications
You must be signed in to change notification settings - Fork 16
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Adding FP Library of the SMTLIB #28
Comments
I can confirm that I'm not working on it, so if you have the time and motivation, that's great ! For writing the theory, I would give the following advices:
The fact that builtins are not exported in |
It is for COLIBRI, we have an OCaml to Prolog bridge, so since our previous prolog parser was flaky, using dolmen is more than a bliss. Thanks for the advices @Gbury! |
Good to hear. Is colibri amenable to be re-written in OCaml, or is it too big a stretch? :p |
Not in OCaml too easy, in Why3 it is better 😉 |
Additionally, do you think dolmen should to export the following function (It basically tries and match the type of a term with a bitvector type and if successful extracts the length of the bitvector), or do you think it is simple enough that users can re-implement their variant of it (returning an option, or some other error) ? Lines 2109 to 2112 in bbbe607
|
I think it is not necessary, because I think in most use cases one will match on all the possible builtin at the same time. |
The MR #31 should implement the theory. |
I have some small fixes that I will MR in bulk once when COLIBRI+dolmen works fully. |
I'm proposing to do it, but I prefer to check that someone else is not doing it. I think I will take inspiration from the BV theory which also a family of types indexed by integers, but is there any other advice?
PS: Dolmen is really really great! I still don't understand why builtins are not exported in
Dolmen.Expr
, how should we match the different ids when going through the typed expressions?The text was updated successfully, but these errors were encountered: