We show how easy it is to hook an SMT (Satisfiability Modulo Theory) solver such as CVC4 or Z3 as a backend to miniKanren, an embedded domain-specific language in Scheme, to create an environment for constraint logic programming. This combination inherits the best of both worlds: the high-level interleaved search and recursive unfolding of miniKanren, and the finely tuned low-level facilities of the underlying solver.

In this talk, we describe the simple implementation and illustrate the technology through interpreters, synthesis, symbolic execution / abstract interpretation, RSA, and music generation.