opam-version: "1.2"

name: "touist"

version: "3.5.2"

maintainer: "Maël Valais <mael.valais@gmail.com>"

authors: [ "Maël Valais <mael.valais@gmail.com>" "Olivier Lezaud" ]

license: "MIT"

homepage: "https://www.irit.fr/touist"

dev-repo: "https://github.com/touist/touist.git"

bug-reports: "https://github.com/touist/touist/issues"

build: [

["dune" "subst"] {dev}

["dune" "build" "-j" jobs "-p" name "@install" "@runtest" {with-test} "@doc" {with-doc}]

]

depends: [

"dune" {build & >= "2.7"}

"menhir" {>= "20151023"}

"minisat"

"re" {>= "1.7.2"}

"cmdliner" {>= "0.9.8"}

"ounit" {with-test}

"odoc" {with-doc}

]

depopts: [

"qbf"

"yices2"

]

conflicts: [

"qbf" {< "0.1"}

"yices2" {< "0.0.2"}

]

available: [ ocaml-version >= "4.08.0" ]

post-messages: [

"To install more solvers, see 'opam info touist'" {success}

"Built without yices2 (SMT solver)" {success & !yices2:installed}

"Built without qbf (QBF solver)" {success & !qbf:installed}

"Built with yices2 (SMT solver). See 'opam info touist' for license." {success & yices2:installed}

"Built with qbf (QBF solver)" {success & qbf:installed}

]

synopsis: "The solver for the Touist language"

description: """

Touist is the compiler for the TouIST language. The TouIST language offers a

friendly syntax 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`

"""