2020-04-21 17:34:44 (GMT)
Sophie said:
Next time, let's create the "time: title" thread as soon as we know these two things!
Is there already an estimate for when the next book club meeting will take place? Does this event have an established frequency?
2020-04-21 17:40:45 (GMT)
I think we're more or less on an every-other-week frequency, so it'd be on april the 30th I believe.
2020-04-21 19:45:10 (GMT)
Simon, if you look at the stream's topics, you'll see that there's no need to "believe". ;)
2020-04-21 19:55:49 (GMT)
who am I, a zulip magician?!
2020-04-27 14:24:8 (GMT)
I didn't think of mentioning that, but my sidekick project is, imho, a neat OCaml implementation of a QF_UF CDCL(T) solver in a few thousands lines of code. It handles formulas, if-then-else, uninterpreted functions, and works pretty ok on smtlib's QF_UF fragment.
Also it's functorized so it can be used in other projects. Anyway it's relatively straightforward but not ridiculous, and the congruence closure is worth a look (with explanations and hooks for theories).
</shameless plug>.