In an effort to learn Z3 I tried solving one of my favorite Advent of Code problems (a particularly difficult one, 2018 day 23, part 2) using the Haskell bindings sbv. Spoilers in code ahead... mo...

I've got a type family defined as follows: type family Vec a (n :: Nat) where Vec a Z = a Vec a (S n) = (a, Vec a n) I'd like to assert that the result of applying this type family always fulf...

I wrote an application in Haskell that calls Z3 solver to solve constrains with some complex formulas. Thanks to Haskell I can quickly switch the data type I'm working with. When using SBV's AlgRe...

I'm using SBV (with Z3 backend) in Haskell to create some theory provers. I want to check if forall x and y with given constrains (like x + y = y + x, where + is a "plus operator", not addition) so...