touist

The solver for the Touist language
README

| Mac, Linux | Windows | Reference manual | Come and discuss! |
|:--------------------:|:-----------------------:|:-----------------------:|:-----------------------:|
| | | | |

Install

  1. TouIST has a java-based graphical interface (which embeds the
    command-line tool). It be downloaded in the releases page and is available
    for Linux, Windows and macOS. Two options are available: the plain jar
    for any platform or the non-signed native version for macOS and
    Windows (see below warning).

    ⚠ WARNING ⚠ On macOS Sierra, the native TouIST.app will show a
    broken message. You must run sudo spctl --master-disable which will
    enable the Open apps from anywhere.

    ⚠ WARNING ⚠ On Windows 10, the native TouIST.exe can't be opened unless
    the Windows Defender SmartScreen feature is disabled. You can still use
    the jar version.

  2. If you only want the command-line program touist, it can be installed
    using either brew (linux/mac)
    or opam.

    Using brew (recommended, provides pre-built binaries):

    brew install touist/touist/touist          # stable version
    brew install touist/touist/touist --HEAD   # git-master version
    

    Using opam (yices2 and qbf are optionnal, you can skip them if
    you don't need the embedded SMT/QBF solvers):

    opam install yices2 qbf touist          # stable version
    opam pin add touist --dev-repo          # git-master version
    

    Now, if we want to know if a ⋀ b ⇒ c is satisfiable:

    echo 'a and b => c' | touist - --solve
    

    The manual (man touist or touist --help) comes very handy, take a look
    at it!

    To build touist from source, see src/HOWTODEBUG.md.

  1. You can also look at the TouIST reference manual
    (pdf version).

  2. Syntax coloring is also available for VSCode (search
    for the touist extension) and for Vim (Vim support is experimental).

Description

TouIST is a user-friendly tool for solving propositional logic problems using
a high-level logic language (known as the bigand format or syntax or
language). This language allows complex expressions like big and, sets...

We can for example solve the problem "Wolf, Sheep, Cabbage", or a sudoku, or
any problem that can be expressed in propositional logic.

The TouIST has been initialized by Frederic Maris and Olivier Gasquet,
associate professors at the Institut de Recherche en Informatique de Toulouse
(IRIT). It is a "second" or "new" version of a previous program,
SAToulouse.

The development is done by a team of five students1 in first year of master's
degree at the Université Toulouse III — Paul Sabatier. This project is a part
of their work at school.

What is Touist made of?

  1. the main program, touist, is written in OCaml and is compiled
    into a native and standalone binary. It does the parsing, the transformations
    (e.g., latex) and embeds one solver per theory (SAT, SMT and QBF) in order
    to solve the problem.

  2. the java-based graphical interface uses Java (>= jre7) and Swing; it embeds
    a copy of the touist binary.

Here is a small figure showing the architecture of the whole thing:

Rebuilding-it

See the ./INSTALL.md file.

Tested architectures

| | GNU/Linux, BSD | Windows | macOS |
| ---------------------- | -------------- | ---------------------- | ----- |
| touist (opam) | yes | yes (mingw32+mingw64) | yes |
| qbf (opam) | yes | yes (minw32 only [^1]) | yes |
| yices2 (opam) [^2] | yes | no | yes |
| yices2 (source) [^2] | yes | yes (mingw32+mingw64) | yes |

[^1]: the qbf package only works on mingw32 because of a slight bug in the
./configure of quantor-3.2. See maelvalais's PR on the ocaml-qbf repo.

[^2]: yices2 needs the gmp library on the system. On linux and macos, opam
will install it for you using the command opam depext conf-gmp.

TouIST API

You can also use the touist library; it is installed using
opam install touist and requires the version 3.4.0 or above.
The API reference is here. For example, in utop:

#require "touist";;
open Touist;;
"a and b and c"
    |> Parse.parse_sat
    |> Eval.eval
    |> Cnf.ast_to_cnf
    |> SatSolve.minisat_clauses_of_cnf
    |> SatSolve.solve_clauses
        ~print:(fun tbl model _ -> SatSolve.Model.pprint tbl model |> print_endline);;

will return

1 c
1 b
1 a
- : SatSolve.ModelSet.t = <abstr>

The API is kind of spread among many modules (which could be gathered in one
single module), sorry for that! We really hope to have some time to
put everything in a nice module well organized.

Bugs and feature requests

You can report bugs by creating a new Github issue. Feature requests can also
be submitted using the issue system.

You can contribute to the project by forking/pull-requesting.

References

  1. Olivier Gasquet, Andreas Herzig, Dominique Longin, Frédéric Maris, and
    Maël Valais. TouIST Again… (Formalisez et Résolvez Facilement Des
    Problèmes Avec Des Solveurs SAT, SMT et QBF).
    In Actes Des 10es
    Journées d’Intelligence Artificielle Fondamentale (IAF 2017). 2017.

  2. Khaled Skander Ben Slimane, Alexis Comte, Olivier Gasquet, Abdelwahab Heba,
    Olivier Lezaud, Frédéric Maris, and Maël Valais La Logique Facile Avec
    TouIST (formalisez et Résolvez Facilement Des Problèmes Du Monde Réel
    )
    . In Actes Des 9es Journées d’Intelligence Artificielle
    Fondamentale (IAF 2015). 2015.

  3. Khaled Skander Ben Slimane, Alexis Comte, Olivier Gasquet, Abdelwahab Heba,
    Olivier Lezaud, Frederic Maris, and Mael Valais. Twist Your Logic with
    TouIST
    . CoRR abs/1507.03663. 2015.

  4. Gasquet O., Schwarzentruber F., Strecker M. Satoulouse: The Computational
    Power of Propositional Logic Shown to Beginners
    . In:
    Blackburn P., van Ditmarsch H., Manzano M., Soler-Toscano F. (eds) Tools
    for Teaching Logic. Lecture Notes in Computer Science, vol 6680. Springer,
    Berlin, Heidelberg. 2011.

Install
Sources
v3.5.0.tar.gz
md5=c09dd1cda8aff444889d1374636c810b
Dependencies
odoc
with-doc
ounit
with-test & < "2.2.6"
cmdliner
>= "0.9.8"
menhir
>= "20151023"
jbuilder
>= "1.0+beta12"
ocaml
>= "4.02.3"
Reverse Dependencies