touist

The solver for the Touist language
Description

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 the embeded SMT solver, run opam install yices2 and then do opam reinstall touist
  • for using the embeded QBF solver, run opam install qbf and then do opam reinstall touist
Install
Published
23 Jun 2017
Sources
v3.2.1.tar.gz
md5=b37b3aaefba542930f0e2b94cd0d79c1
Dependencies
ounit
with-test & < "2.2.6"
minisat
build
menhir
build & >= "20151023"
fileutils
build & >= "0.4.0"
cppo
build & >= "0.9.4"
ocaml
>= "4.01.0"
Reverse Dependencies