zhanhaoxiao/touist

TouIST, the IDE & Language for Logic (backed by SAT, SMT and QBF solvers)

TouIST, the language for propositional logic

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:

   touist - --solve <<< "a and b => c"
   

   where - tells touist to expect a formula on stdin and <<< gives the right-hand string to stdin.

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

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

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

4. 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

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.

Footnotes

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. ↩ ↩²