In the CS fields I am interested in programming languages, UX, Visualizations & AI. I've spent more than 10 years teaching CS.I love to social dance to swing & blues music.
Lovely series! I have my own crystal-z3 which I am looking forward to mark it as archived if you want to maintain a shard for this!
Two things that I have in my mind regarding z3 in Crystal.
Hopefully we can make the ideas of youtube.com/watch?v=rTOqg-f2rNM possible in Crystal. Having a solver assist the developer in program creating sounds sci-fi to me still.
API related, Crystal does not allow overriding some binary operators ||&&, cause they have typing implications. So there is a limit on how seamlessly the integration can look. But a possible way to solve this is via macros. Somthing like Z3.expr(a && b) could be a macro that translates Crystal syntax to Z3 api without needing && to be an actual call of the typeof(a). This might be useful for the previous point, since a and b could be either actual values or Z3 expressions depending on how the program is invoked.
Lovely series! I have my own crystal-z3 which I am looking forward to mark it as archived if you want to maintain a shard for this!
Two things that I have in my mind regarding z3 in Crystal.
Hopefully we can make the ideas of youtube.com/watch?v=rTOqg-f2rNM possible in Crystal. Having a solver assist the developer in program creating sounds sci-fi to me still.
API related, Crystal does not allow overriding some binary operators
||&&, cause they have typing implications. So there is a limit on how seamlessly the integration can look. But a possible way to solve this is via macros. Somthing likeZ3.expr(a && b)could be a macro that translates Crystal syntax to Z3 api without needing&&to be an actual call of thetypeof(a). This might be useful for the previous point, sinceaandbcould be either actual values or Z3 expressions depending on how the program is invoked.I've taken a look at your version, and wrote a post about how they compare.
My Ruby Z3 gem uses
|&and.itefor booleans as||,&&, and?:are not possible to override. I think I'll need to do the same in Crystal.