Z3 is kind of my new favorite thing right now. I have a problem that lends itself quite well to constraints-based reasoning, and I need it to be optimized. I'm sure I could have hacked something together using any number of programming languages, but after playing with Z3 for a bit, I realized that this could be easily done in around ~100 lines of an SMT2 file, and probably be considerably faster.
Tools like this make me feel a lot better about all the time I wasted playing with predicate logic.
Same. I’d been circling SMT solvers for a while but a recent HN post on knuckledragger[1] (built on Z3) made me finally take a closer look at Z3 itself. It kind of feels like stealing fire.
If you’re not already familiar with it, have a look at Dafny. It’s an imperative programming language built using Boogie and Z3 that allows extremely interesting compile time assertions.
Would like to know how you us Z3 to evaluate emotional happy Q. Could you apply that to evaluate a piece of content (like thread, feed, comment) and then evaluate the energy of the thing for its happiness quotient value whatever? then you can just Z3 the thread and determine the psychological predicted impact...
Maybe you could then design casula games that provide the positive happy Q vibes.
--
I was in a program from when I was a baby with UCSD that was a life tracking project and they would check in with you every so often to see where you were on that trajectory - and where you were happy in life etc.
Problem is that it was also tied to Morehouse University, MK, Vic Baranco, and a bunch of other Stanford thingy's from the 70s that we all know abou these days.
Nah, the core math for Equation of Happiness is my dad's thing, and it's using a genetic algorithm for its optimization stuff, all I did was port some of his code to Julia and write a basic web frontend. If I had known about Z3's optimization tools when he was writing the book, I might have tried to use it, but I'm not sure how well Z3 would actually work with the differential equation stuff he was doing, since it's not really discrete.
I'm working on something that is trying to utilize Z3 for some financial market stuff that I hack on in my free time.
Tools like this make me feel a lot better about all the time I wasted playing with predicate logic.