Satisfiability modulo theories (SMT) solvers give programmers a useful interface to solve challenging constraints at runtime. SMT solving has been used for a vast variety of different, useful applications, ranging from strengthening Haskell’s type system to verifying network protocols.

Unfortunately, interacting with SMT solvers directly from Haskell requires a great deal of manual effort. Data must be represented in and translated between two forms: that understood by Haskell, and that understood by the SMT solver. As such a translation is often done via printing and parsing text, any notion of type safety is lost. Furthermore, direct translations are rarely sufficient, as it typically takes many iterations on a design in order to get optimal – or even acceptable – performance from an SMT solver on large scale problems. This need for iteration complicates the translation issue: it is easy and frustrating to introduce a runtime bug.

To address these problems, we introduce a new library, G2Q. G2Q includes a quasiquoter that allows solving constraints written in Haskell itself, thus unifying data representation, ensuring correct typing, and simplifying iteration. We describe the API to our library and its backend, which is based on the G2 symbolic execution engine. Finally, we demonstrate the usability of G2Q via four example programs.