package touist

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

Install

Dune Dependency

Authors

Maintainers

Sources

v3.4.1.tar.gz
sha256=f4ccc2254887a5839c1aebfe1e1f8a85210f0f9c29f7b435b6ee4cef8c572020
md5=7be1923c383605cc48c3fbe0a4ab3593

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 Yices2 (--smt --solve), run opam install yices2
  • for using Quantor (--qbf --solve), run opam install qbf

Published: 09 Nov 2017

Dependencies (7)

  1. ocamlfind build
  2. ocamlbuild build
  3. minisat build & < "0.6"
  4. menhir >= "20151023"
  5. cppo build & >= "0.9.4" & <= "1.5.0"
  6. cppo_ocamlbuild build & >= "1.6.0"
  7. ocaml >= "4.01.0"

Dev Dependencies (1)

  1. ounit with-test

Used by

None

Conflicts (2)

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

Innovation. Community. Security.