package touist
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
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)
-
ocamlfind
build -
ocamlbuild
build -
minisat
build & < "0.6" -
menhir
>= "20151023" -
cppo
build & >= "0.9.4" & <= "1.5.0" -
cppo_ocamlbuild
build & >= "1.6.0" -
ocaml
>= "4.01.0"
Dev Dependencies (1)
-
ounit
with-test
Used by
None
On This Page