The Touist language is a friendly language for writing propositional logic (SAT), logic on real and integers (SMT) and quantified boolean formulas (QBF). This language aims to formalize real-life problems (e.g., the sudoku can be solved in a few lines). Touist embeds a SAT solver (minisat) and can be built with optionnal SMT and QBF solvers. Touist is also able to generate the latex, DIMACS, SMT-LIB and QDIMACS formats from a touist file.

Optionnal solvers:

• for using Yices2 (--smt --solve), run opam install yices2
• for using Quantor (--qbf --solve), run opam install qbf