package touist
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
On This Page
The solver for the Touist language
Install
dune-project
Dependency
Authors
Maintainers
Sources
v3.5.0.tar.gz
sha256=859a4428ced26ed38615a606138c02ec63541cd34cf94a37b3e35d5bf46d40c4
md5=c09dd1cda8aff444889d1374636c810b
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 Dec 2017
On This Page