package touist

  1. Overview
  2. Docs
The solver for the Touist language

Install 

dune-project
 Dependency

www.irit.fr Edit opam file Versions (5)

Authors

  1. M
    Maël Valais <mael.valais@gmail.com>
  2. O
    Olivier Lezaud

Maintainers

  1. M
    Maël Valais <mael.valais@gmail.com>

Sources

v3.2.1.tar.gz
sha256=1085e30db117f0fe61bc506531964a6c5c007db9c7b52f166a5d5c9acae357ff
md5=b37b3aaefba542930f0e2b94cd0d79c1

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

Published: 23 Jun 2017

Dependencies (9)

  1. cmdliner < "2.0.0"
  2. ocamlfind build
  3. ocamlbuild build
  4. minisat build & < "0.6"
  5. menhir build & >= "20151023"
  6. fileutils build & >= "0.4.0"
  7. cppo_ocamlbuild build
  8. cppo build & >= "0.9.4"
  9. ocaml >= "4.01.0" & < "5.0.0"

Dev Dependencies (1)

  1. ounit with-test & < "2.2.6"

Used by

None

Conflicts (2)

  1. yices2 < "0.0.2"
  2. qbf < "0.1"