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 Yices2 (--smt --solve), run
opam install yices2 - for using Quantor (--qbf --solve), run
opam install qbf
| Authors | Maël Valais <mael.valais@gmail.com> and Olivier Lezaud |
|---|---|
| License | MIT |
| Published | |
| Homepage | https://www.irit.fr/touist |
| Issue Tracker | https://github.com/touist/touist/issues |
| Maintainer | Maël Valais <mael.valais@gmail.com> |
| Dependencies |
|
| Optional dependencies | |
| Conflicts | |
| Source [http] | https://github.com/touist/touist/archive/v3.4.1.tar.gz sha256=f4ccc2254887a5839c1aebfe1e1f8a85210f0f9c29f7b435b6ee4cef8c572020 md5=7be1923c383605cc48c3fbe0a4ab3593 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/touist/touist.3.4.1/opam |
No package is dependent
