touist

AuthorsMaël Valais <mael.valais@gmail.com> and Olivier Lezaud
LicenseMIT
Homepagehttps://www.irit.fr/touist
Issue Trackerhttps://github.com/touist/touist/issues
MaintainerMaël Valais <mael.valais@gmail.com>
Dependencies
&cppo
|0.9.4
1.0.0
1.0.1
1.1.0
1.1.1
1.1.2
1.2.2
1.3.0
1.3.1
1.3.2
1.4.0
1.4.1
1.5.0
fileutils>= 0.4.0
menhir>= 20151023
minisat
ocamlbuild
ocamlfind
ounit
Optional dependencies
|qbf
yices2
Availableocaml-version >= "4.01.0"
PublishedSep 13, 2017
Source [http] https://github.com/touist/touist/archive/v3.4.0.tar.gz
13920976affe8924b192ccd4e6d5a98b
StatisticsInstalled 3 times last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/touist/touist.3.4.0/opam

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
No package is dependent