File tree Expand file tree Collapse file tree 3 files changed +53
-0
lines changed
packages/touist/touist.3.5.0 Expand file tree Collapse file tree 3 files changed +53
-0
lines changed Original file line number Diff line number Diff line change 1+ The solver for the Touist language
2+
3+ The Touist language is a friendly language for writing propositional
4+ logic (SAT), logic on real and integers (SMT) and quantified boolean
5+ formulas (QBF). This language aims to formalize real-life problems
6+ (e.g., the sudoku can be solved in a few lines). Touist embeds a SAT
7+ solver (minisat) and can be built with optionnal SMT and QBF solvers.
8+ Touist is also able to generate the latex, DIMACS, SMT-LIB and QDIMACS
9+ formats from a touist file.
10+
11+ Optionnal solvers:
12+ - for using Yices2 (--smt --solve), run `opam install yices2`
13+ - for using Quantor (--qbf --solve), run `opam install qbf`
Original file line number Diff line number Diff line change 1+ opam-version: "1.2"
2+ maintainer: "Maël Valais <mael.valais@gmail.com>"
3+ authors: ["Maël Valais <mael.valais@gmail.com>" "Olivier Lezaud"]
4+ homepage: "https://www.irit.fr/touist"
5+ bug-reports: "https://github.com/touist/touist/issues"
6+ license: "MIT"
7+ dev-repo: "https://github.com/touist/touist.git"
8+ build: [
9+ ["jbuilder" "subst"] {pinned}
10+ ["jbuilder" "build" "-p" name "-j" jobs]
11+ ]
12+ install: ["jbuilder" "install"]
13+ build-test: ["jbuilder" "runtest" "-p" name "-j" jobs]
14+ build-doc: ["jbuilder" "build" "@doc" "-j" jobs]
15+ remove: ["jbuilder" "uninstall"]
16+ depends: [
17+ "jbuilder" {build & >= "1.0+beta12"}
18+ "menhir" {>= "20151023"}
19+ "minisat"
20+ "re"
21+ "cmdliner" {>= "0.9.8"}
22+ "ounit" {test}
23+ "odoc" {doc}
24+ ]
25+ depopts: ["qbf" "yices2"]
26+ conflicts: [
27+ "qbf" {< "0.1"}
28+ "yices2" {< "0.0.2"}
29+ ]
30+ available: [ocaml-version >= "4.02.3"]
31+ post-messages: [
32+ "To install more solvers, see 'opam info touist'" {success}
33+ "Built without yices2 (SMT solver)" {success & !yices2:installed}
34+ "Built without qbf (QBF solver)" {success & !qbf:installed}
35+ "Built with yices2 (SMT solver). See 'opam info touist' for license."
36+ {success & yices2:installed}
37+ "Built with qbf (QBF solver)" {success & qbf:installed}
38+ ]
Original file line number Diff line number Diff line change 1+ http: "https://github.com/touist/touist/archive/v3.5.0.tar.gz"
2+ checksum: "c09dd1cda8aff444889d1374636c810b"
You can’t perform that action at this time.
0 commit comments