touistversion

The solver for the Touist language

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
AuthorsMaël Valais <mael.valais@gmail.com> and Olivier Lezaud
LicenseMIT
Published
Homepagehttps://www.irit.fr/touist
Issue Trackerhttps://github.com/touist/touist/issues
MaintainerMaël Valais <mael.valais@gmail.com>
Dependencies
Optional dependencies
Conflicts
Source [http] https://github.com/touist/touist/archive/v3.2.1.tar.gz
sha256=1085e30db117f0fe61bc506531964a6c5c007db9c7b52f166a5d5c9acae357ff
md5=b37b3aaefba542930f0e2b94cd0d79c1
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/touist/touist.3.2.1/opam
No package is dependent