The source of this document is written in madoko, a markdown dialect.
This language has been chosen over Latex for its brevity (Pandoc could
have also been chosen). You can contribute to this document through a
pullrequest or by discussing your thoughts in the issue tracker. To
edit it, you can first take a look at what the madoko editor can do
(with this link, the images and colorizer will not work), or see how to
edit properly in CONTRIBUTETODOCS.md
(located in
docs/
).
Touist is a language that allows to express propositional logic
[1, 2]. You are provided with two programs: a
graphical interface, refered as touist.jar
(as it is written in Java) and
touist
, the commandline compiler and solver (written in Ocaml).
The touist language aims at making the writing of propositional logic as approchable as possible. Propositions and connectors syntaxes are close to what would be written on paper. Here are some examples of formulas:
Propositional logic  touist language 

$\neg p$  not p 
$p \wedge q$  p and q 
$p \vee q$  p or q 
$p \oplus q$  p xor q 
$p \rightarrow q$  p => q 
$p \leftrightarrow q$  p <=> q 
After typing a formula, you can ask touist
to find a valuation (true or
false) of each proposition so that the whole formula is true (such valuation,
also called interpretation, is called model). When a model exists, your
formula is satisfiable. For example, a model of $p \vee q$ is $\{p = true,q =false\}$. To check the models of this formula using touist
, you can do
Graphical Java interface  Commandline interface (see 4.2) 

1. Type p and q  1. Create a file p and q 
2. Press “Solve”  2. Type ./touist solve yourfile 
3. Press “Next” to see other models  3. The first model is displayed 
From a wikipedia example:
Premise 1:  If it's raining then it's cloudy 
Premise 2:  It's raining 
Conclusion:  It's cloudy 
This inference can be written
The infer (or entails) symbol ($\models$) does not belong to the touist
language (we call it “metalanguage”). This means that we have to transform
this notation to an actual propositional formula.
Theorem 1.
Let $H$ be a set of formulas (called hypotheses or premises) and $C$ a
formula (called conclusion). Then
$H \models C$ if and only if $H\cup\{\neg C\}$ is unsatisfiable.
From this theorem, we just have to check that the set of formulas
has no model. We can translate this set to touist
language (comments begin
with two semicolon ";;
"):
raining => cloudy ;; Premise 1
raining ;; Premise 2
not cloudy ;; Conclusion
In touist, the premises are simply formulas separated by a new line. A
new line is semantically equivalent to the .
and
connector: the previous
bit of touist
code could be equivalently written
(raining => cloudy) and raining and not cloudy
<touistfile> ::= <affect> <touistfile>
 <formula> <touistfile>
 EOF
A touist file is a whitespaceseparated^{1} list of affectations
and formulas. Affectations are global and can be interlaced with formulas
as long as they are not nested in formulas (for local variables, you can
use let
, see 3.2.3). Comments begin
with the ";;
" sequence. Two backslashes (\\
) in a formula will
produce a new line in the latex view.
The whitespaceseparated list of formulas is actually going to be
converted to a conjunction; it avoids many intermediate .
and
.
Warning: each formula in this list is going to be put into
parenthesis:
a or b
c => a
will be translated to
(a and b) and (c => a)
First, we describe what a variable is. Then, we detail how to affect variables (with global or local affectations).
<expr> ::= <int><float><prop><bool><set>
<var> ::= "$" TERM < simplevar
 "$" TERM "(" <commalist(<expr>)> ")" < tuplevar
$my_var
. In a formula, a simple
variable is always expected to be a proposition. In an expression, a simple
variable can contain an integer, a floatingpoint, a proposition, a boolean
or a set.
$var($i,a,4)
. The leading variable ($var
)
must always contain a proposition. The nested indexes (e.g., $i
) can be
integers, floats, propositions or booleans.
$var=p
and $i=q
, then it will expand to p(q,a,4)
Here are some examples of variables:
Simplevar  Tuplevar 

$N  $place($number) 
$time  $action($i,$j) 
$SIZE  
$is_over  
We call “global variables” any variable that is affected in the toplevel formula (meaning that global variables cannot be nested in other formulas) using the following affectation syntax:
<affect> ::= <var> "=" (<expr>) < global affectation
<expr> ::= <int><float><prop><bool><set>
Global variables apply for the whole code, even if the affectation is located before it is first used. This is because all global affectations are evaluated before any formula.
The only case where the order of affectation is important is when you want to use a variable in a global affectation expression. Global affectations are sequentially evaluated, so the order of affectation matters. For example:
$N = 10
$set = [1..$N] ;; $N must be defined before $set
let
construct)Sometimes, you want to use the same result in multiple places and you
cannot use a global variable (presented in 3.2.2) because of
nested formulas. The let
construct lets you create temporary
variables inside formulas:
<letaffect<T>> ::=
 "let" <var> "=" <expr> ":" <formula<T>> < local affectation
<expr> ::= <int><float><prop><bool><set>
The let
affectation can only be used in formulas (detailed
in 3.7) and cannot be used in expressions (<expr>
, i.e.,
integer, floatingpoint, boolean or set expressions).
Example:
;; This piece of code has no actual meaning
$letters = [a,b,c,d,e]
bigand $letter,$number in $letters,[1..card($letters)]:
has($letter,$number) =>
let $without_letter = diff($letters,$letter): ;; keep temorary result
bigand $l1 in $without_letter:
p($letter)
end
end
The scope of a variable affected using .
let
is limited to the formula
that follows the colon (:
). If this formula is followed by a whitespace
and an other formula, the second formula will not be in the variable
scope. Example:
let $v=10: prop($v)
prop($v) ;; error: $v is not in scope anymore
TERM = [_09]*[azAZ][azAZ_09]*
<expr> ::= <int><float><prop><bool><set>
<prop> ::=
 <var>
 TERM
 TERM "(" <commalist(<expr>)> ")"
A simple proposition is a simple word that can contain numbers and the
underscore symbol ("_
"). A tuple proposition (we can it as a
predicate), of the form prop(1,$i,abc)
, must have indexes of type
integer, float, boolean or set.
A tuple proposition that is in an expression and that contains at least one set in its indexes will be expanded to a set of the cartesian product of the set indexes. This feature is called setbuilding and is described in 3.6.3 and only works in expressions (not in formulas).
In the following table, the two rightcolumns show how the propositions are expanded whether they are in an expression or in a formula:
Proposition  is in a formula  is in an expression 

p([a])  p([a])  p(a) 
p([a,b,c])  p([a,b,c])  [p(a),p(b),p(c)] 
p([a,b],[1..2])  p([a,b],[1..2])  [p(a,1),p(b,1) 
p(a,2),p(b,2)]  
The available operations on integers and floats are +
, 
, *
, /
,
$x mod $y
(modulo) and abs($x)
(absolute value). Parenthesis can
be used. The order of priority for the infix operators is:
highest priority  mod 
* ,/  
lowest priority  + , 
Here is the complete rule for numeric operators:
<numoperation(<T>)> ::=
 <T> "+" <T>
 <T> "" <T>
 "" <T>
 <T> "*" <T>
 <T> "/" <T>
<numoperationothers(<T>)> ::=
 <T> "mod" <T>
 "abs(" <T> ")"
Integer and float expressions cannot be mixed. It is necessary to cast
explicitely to the other type when the types are not matching. For
example, the expression .
1+2.0
is invalid and should be written
1+int(2.0)
(gives an integer) or float(1)+2.0
(gives a float).
Some operators are specific to integer or float types:
card([a,b])
returns an integer,
sqrt(3)
returns a float.An integer constant INT
is a number that satisfies the regular expression
[09]+
. Here is the rule for writting correct integer expressions:
<int> ::=
 "(" <int> ")"
 <var>
 INT
 numoperation(<int>)
 numoperationothers(<int>)
 "if" <bool> "then" <int> "else" <int> "end"
 "int(" (<int><float>) ")"
 "card(" <set> ")"
A floatingpoint constant FLOAT
is a number that satisfies the regular
expression [09]+\.[09]+
. The variants 1.
or .1
are not accepted.
Here is the rule for writting correct integer expressions:
<float> ::=
 "(" <float> ")"
 <var>
 FLOAT
 numoperation(<float>)
 numoperationothers(<float>)
 "if" <bool> "then" <float> "else" <float> "end"
 "float(" (<int><float>) ")"
 "sqrt(" <float> ")"
The constants are true
and false
. The boolean connectors are $>$,
$<$, $\ge$ (>=
), $\le$ (<=
), $=$ (==
) and $\neq$ (!=
). The
operators that return a boolean are subset($P,$Q)
, empty($P)
and
p in $P
:
subset($P,$Q)  $P \subseteq Q$  $P$ is a subset (or is included in) $Q$ 
empty($P)  $P=\emptyset$  $P$ is an empty set 
$i in $P  $i \in P$  $i$ is an element of the set $P$ 
Sets are detailed in 3.6.
Booleans cannot be mixed with formulas. In a formula, the evaluation (choosing true or false) is not done during the translation from touist to the “solverfriendly” language. Conversely, a boolean expression must be evaluable during the translation. .
Parenthesis can be used in boolean expressions. The priority order for booleans is:
highest priority  == ,!= ,<= ,>= ,< ,> , in 
not  
xor  
and  
or  
lowest priority  => , <=> 
Note that =>
and <=>
associativity is evaluated from right to left.
Here is the full grammar rule for booleans:
<bool> ::= "(" <bool> ")"
 <var>
 "true"
 "false"
 (<int><float><prop><bool>) "in" <set>
 "subset(" <set> "," <set> ")"
 "empty(" <set> ")"
 <equality(<int><float><prop>)>
 <order(<int><float>)>
 <connectors(<bool>)>
<equality(<T>)> ::=
 <T> "!=" <T>
 <T> "==" <T>
<order(<T>)> ::=
 <T> ">" <T>
 <T> "<" <T>
 <T> "<=" <T>
 <T> ">=" <T>
Sets can contain anything (propositions, integers, floats, booleans or even other sets) as long as all elements have the same type. There exists three ways of creating a set:
$\{1,3,8,10\}$ can be written [1,2,3]
. Elements can be integers, floats,
propositions, booleans or sets (or a variable of these five types).
The empty set $\emptyset$ is denoted by []
.
$\{i~~i=1,\dots,10\}$ can be written [1..10]
. Ranges can
be produced with both integer and float limits. For both integer and float
limits, the step is 1 (respectively 1.0). It is not possible to change the step for now.
$\{p(x_1,...,x_n)~~(x_1,...,x_n) \in S_1 \times ... \times S_n \}$, which the set
of tuple propositions based on the cartesian product of the sets $S_1,...,S_n$,
can be written p($S1,$S2,$S3)
. The example p([a,b,c])
will produce
[p(a),p(b),p(c)]
.
You can mix sets, integers, floats, propositions and booleans in indexes:
Proposition  produces the set 

f(1,[a,b],[7..8])  [f(1,a,7),f(1,a,8), 
f(1,b,7),f(1,b,8)]  
Important: the setbuilder feature only works in expressions and does
not work in formulas. In formulas, the proposition f([a,b])
will
simply produce f([a,b])
. This also means that you can debug your sets
by simply putting your set in a tuple proposition.
This notation is inspired from the concept of extension of a predicate (cf. wikipedia).
Some common set operators are available. Let $P$ and $Q$ denote two sets:
Type  Syntax  Math notation  Description 

<set>  inter($P,$Q)  $P \cap Q$  intersection 
<set>  union($P,$Q)  $P \cup Q$  union 
<set>  diff($P,$Q)  $P \setminus Q$  difference 
<set>  powerset($Q)  $\mathcal{P}(Q)$  powerset 
<int>  card($S)  $\vert S \vert$  cardinal 
<bool>  empty($P)  $P=\emptyset$  set is empty 
<bool>  $e in $P  $e \in P$  belongs to 
<bool>  subset($P,$Q)  $P \subseteq Q$  is a subset or equal 
The three last operators of type <bool>
(empty
, in
and subset
)
have also been described in the boolean section (3.5).
The powerset($Q)
operator generates all possible subsets $S$ such
that $S \subseteq Q$. It is defined as
The empty set is included in these subsets. Example:
powerset([1,2])
generates [[],[1],[2],[1,2]]
.
Here is the complete rule for sets:
<set> ::= "(" <set> ")"
 <var>
 "[" <commalist(<int><float><prop><bool>)> "]"
 "[ <int> ".." <int> "]" < step is 1
 "[ <float> ".." <float> "]" < step is 1.0
 "union(" <set> "," <set> ")"
 "inter(" <set> "," <set> ")"
 "diff(" <set> "," <set> ")"
 "powerset(" <set> ")"
A formula is a sequence of propositions (that can be variables) and connectors
$\neg p$ (not
), $\wedge$ (and
), $\vee$ (or
), $\oplus$ (xor
),
$\rightarrow$ (=>
) or $\leftrightarrow$ (<=>
).
<connectors(<T>)> ::=
 "not" <T>
 <T> "and" <T>
 <T> "or" <T>
 <T> "xor" <T>
 <T> "=>" <T>
 <T> "<=>" <T>
You can chain multiple variables in .
bigand
or bigor
by giving a
list of variables and sets. This will translate into nested
bigand
/bigor
. You can even use the value of outer variables in
inner set declarations:
bigand $i,$j in [1..3], [1..$i]:
p($i,$j)
end
Generalized connectors bigand
, bigor
, exact
, atmost
and
atleast
are also available for generalizing the formulas using sets. Here
is the rule for these:
<generalizedconnectors(<T>)> ::=
 "bigand" <commalist(<var>)> "in" <commalist(<set>)>
["when" <bool>] ":" <T> "end"
 "bigor" <commalist(<var>)> "in" <commalist(<set>)>
["when" <bool>] ":" <T> "end"
 "exact(" <int> "," <set> ")"
 "atmost(" <int> "," <set> ")"
 "atleast(" <int> "," <set> ")"
When multiple variables and sets are given, the bigand
and bigor
operators will produce the and
/or
sequence for each possible couple of
value of each set (the set of couples is the Cartesian product of the given
sets). For example,
The formula  expands to… 

$\bigwedge\limits_{\substack{i\in \{1,...,2\}\\j \in \{a,b\}}} p_{i,j}$  $p_{1,a} \wedge p_{1,b} \wedge p_{2,a} \wedge p_{2,b}$ 
bigand $i,$j in [1..2],[a,b]:  p(1,a) and p(1,b) 
p($i,$j)  and p(2,a) and p(2,b) 
end  
The when
is optional and allows to apply a condition to each couple of
valued variable.
On the following two examples, the math expression is given on the left and the matching touist code is given on the right:
$\bigwedge\limits_{\substack{i\in [1..n]\\j \in [a,b,c]}} p_{i,j}$ 

$\bigvee\limits_{\substack{v\in [A,B,C]\\x \in [1..9]\\y\in[3..4]\\x \ne y \\ x \ne A\\}} v_{x,y}$ 

Here is the list of “limit” cases where bigand
and bigor
will produce
special results:
bigand
, if a set is empty then Top
is produced
bigand
, if the when
condition is always false then Top
is produced
bigor
, if a set is empty then Bot
is produced
bigor
, if the when
condition is always false then Bot
is
produced
These behaviors come from the idea of quantification behind the
bigand
and bigor
operators:
Universal quantification  $\forall x \in S, p(x)$  bigand $x in $S: p($x) end 
Existential quantification  $\exists x \in S, p(x)$  bigor $x in $S: p($x) end 
The following properties on quantifiers hold:
which helps understand why Top
and Bot
are produced.
Clarify this explanation. .
Touist provides some specialized operators, namely exact
, atmost
and atleast
. In some cases, these operators can drastically lower the
size of some formulas. The syntax of these constructs is:
Math notation  Touist syntax 

$\leqslant_{x\in P}^k x$  atmost($k,$P) 
$\geqslant_{x\in P}^k x$  atleast($k,$P) 
${<>}_{x\in P}^k x$  exact($k,$P) 
Let $P$ be a set of propositions, $x$ a proposition and $k$ a positive integer. Then:
These operators are extremely expensive in the sense that they produce formulas
with an exponential size. For example, exact(5,p([1..20])
will produce a disjunction of $\binom{20}{5} = 15 504$ conjunctions.
The notation .
p([1..20])
is called “setbuilder” and is defined
in 3.6.3. Using this syntax, the formula exact(5,p([1..20])
is equivalent to
The following table sums up the various “limit” cases that may not be obvious. In this table, $k$ is a positive integer and $P$ is a set of propositions.
$k  $P  Gives  

exact($k,$P)  $k=0$  $P=\emptyset$  Top 
$k=0$  $P\neq\emptyset$  bigand $p in $P: not $p end  
$k>0$  $\vert P\vert=k$  bigand $p in $P: $p end  
atleast($k,$P)  $k=0$  any  Top 
$k=1$  any  bigor $p in $P: $p end  
$k>0$  $\emptyset$  Bot (subcase of next row)  
$k>0$  $\vert P\vert<k$  Bot  
$k>0$  $\vert P\vert=k$  bigand $p in $P: $p end  
atmost($k,$P)  $k=0$  $\emptyset$  Top (subcase of next row) 
$k=0$  any  Top  
How to read the table: for example, the row where $k>0$ and
$\vert P\vert<k$ should be read "when using atleast
, all couples
$(k,P) \in \{(k,P)k>0,\vert P\vert<k\}$ will produce the special case
Top
".
The constants $\top$ (Top
) and $\bot$ (Bot
) allows to express the
“always true” and “always false”. Here is the complete grammar:
<formulasimple> ::=
 "Top"
 "Bot"
 <prop>
 <var>
 <formula(<formulasimple>)>
<formula(<T>)> ::=
 "(" <T> ")"
 "if" <bool> "then" <T> "else" <T> "end"
 <connectors(<T>)>
 <generalizedconnectors(<T>)>
 <letaffect(<T>)>
Touist can also be given Satisfiability Modulo Theory (SMT) formulas and output the SMT2LIBcompliant file.
Describe the SMT language .
Using the qbf
and solve
flags (in touist
) or the QBF selector
(in the graphical interface), you can solve QBF problems with existential
and universal quantifiers over boolean values. This logic is basically
the same as the SAT grammar, except for two new operators:
 "exists" <commalist(<prop><var>)> ":" <formulaqbf>
 "forall" <commalist(<prop><var>)> ":" <formulaqbf>
One quantifier can quantify over multiple propositions. For example:
forall e,d: (exists a,b: a => b) => (e and forall c: e => c)
Any free variable (i.e., not quantified) will be existentially quantified in an innermost way. For example, $\forall a. a and b$ will become $\forall a. \forall b. a and b$.
Using the rules for transforming an arbitraty formula into prenex form requires sometimes some renaming. For example, $(\forall a. a) and a$ must be transformed into $(\forall a_1. a_1 and a)$.
Sometimes, the renaming is not possible. For example, in
$\forall a. (\exists a: a)$, we cannot guess which quantifier the
rightmost $a$ should be bound to. In this case, touist
will give and
error.
Also, the use of the whitespaceasformulaseparator can lead to some misunderstanding. For example, in formula
exists x: x
x => y
the x
in the second line is free whereas the x
in the first line
is bounded. This is because two whitespaceseparated formulas have
different scopes. In fact, the previous formula could be rewritten as
(exists x: x) and (x => y)
The only way to span the scope of a bounded variable across multiple lines
is to continue the formula with a and
instead of using a new line:
exists x: x
and (x => y)
This section presents the grammar formatted in a BNFlike way. Some rules
(a rule begins with "::=
“) are parametrized so that some parts of the
grammar are ”factorized" (the idea of parametrized rules come from the
Menhir parser generator used for generating the touist parser).
This grammar specification is not LR(1) and could not be implemented as such using Menhir; most of the type checking is made after the abstract syntactic tree is produced. The only purpose of the present specification is to give a clear view of what is possible and not possible with this language. .
INT = [09]+
FLOAT = [09]+\.[09]+
TERM = [_09]*[azAZ][azAZ_09]*
<touistfile> ::= <affect> <touistfile>
 <formula> <touistfile>
 EOF
<expr> ::= <int><float><prop><bool><set>
<var> ::= "$" TERM
 "$" TERM "(" <commalist(<expr>)> ")"
<prop> ::=
 <var>
 TERM
 TERM "(" <commalist(<expr>)> ")"
<affect> ::= <var> "=" (<expr>)
<letaffect<T>> ::=
 "let" <var> "=" <expr> ":" <formula<T>>
<equality(<T>)> ::=
 <T> "!=" <T>
 <T> "==" <T>
<order(<T>)> ::=
 <T> ">" <T>
 <T> "<" <T>
 <T> "<=" <T>
 <T> ">=" <T>
<bool> ::= "(" <bool> ")"
 <var>
 "true"
 "false"
 (<expr>) "in" <set>
 "subset(" <set> "," <set> ")"
 "empty(" <set> ")"
 <equality(<int><float><prop>)>
 <order(<int><float>)>
 <connectors(<bool>)>
<numoperation(<T>)> ::=
 <T> "+" <T>
 <T> "" <T>
 "" <T>
 <T> "*" <T>
 <T> "/" <T>
<numoperationothers(<T>)> ::=
 <T> "mod" <T>
 "abs(" <T> ")"
<int> ::=
 "(" <int> ")"
 <var>
 INT
 numoperation(<int>)
 numoperationothers(<int>)
 "if" <bool> "then" <int> "else" <int> "end"
 "int(" (<int><float>) ")"
 "card(" <set> ")"
<float> ::=
 "(" <float> ")"
 <var>
 FLOAT
 numoperation(<float>)
 numoperationothers(<float>)
 "if" <bool> "then" <float> "else" <float> "end"
 "float(" (<int><float>) ")"
 "sqrt(" <float> ")"
<set> ::= "(" <set> ")"
 <var>
 "[" <commalist(<expr>)> "]"
 "[ <int> ".." <int> "]" < step is 1
 "[ <float> ".." <float> "]" < step is 1.0
 "union(" <set> "," <set> ")"
 "inter(" <set> "," <set> ")"
 "diff(" <set> "," <set> ")"
 "powerset(" <set> ")"
<commalist(<T>)> ::= <T>  <T> "," <commalist(<T>)>
<generalizedconnectors(<T>)> ::=
 "bigand" <commalist(<var>)> "in" <commalist(<set>)>
["when" <bool>] ":" <T> "end"
 "bigor" <commalist(<var>)> "in" <commalist(<set>)>
["when" <bool>] ":" <T> "end"
 "exact(" <int> "," <set> ")"
 "atmost(" <int> "," <set> ")"
 "atleast(" <int> "," <set> ")"
<connectors(<T>)> ::=
 "not" <T>
 <T> "and" <T>
 <T> "or" <T>
 <T> "xor" <T>
 <T> "=>" <T>
 <T> "<=>" <T>
<formula(<T>)> ::=
 "\\" <T>  <T> "\\" < newline marker for latex display
 "(" <T> ")"
 "if" <bool> "then" <T> "else" <T> "end"
 <connectors(<T>)>
 <generalizedconnectors(<T>)>
 <letaffect(<T>)>
<formulasimple> ::=
 "Top"
 "Bot"
 <prop>
 <var>
 <formula(<formulasimple>)>
<formulasmt> ::=
 <formula(<formulasmt>)>
 <exprsmt>
<exprsmt> ::=
 "Top"
 "Bot"
 <prop>
 <var>
 <int>
 <float>
 <order>(<exprsmt>)
 <numoperations_standard(<exprsmt>)>
 <equality(<exprsmt>)>
 <in_parenthesis(<exprsmt>)>
<formulaqbf> ::=
 "Top"
 "Bot"
 <prop>
 <var>
 <formula(<formulaqbf>)>
 "exists" <commalist(<prop><var>)> ":" <formulaqbf>
 "forall" <commalist(<prop><var>)> ":" <formulaqbf>
touist
)The main tool that parses and solves the touist programs is written in
Ocaml. It is easily installable (as long as you have installed ocaml
and opam
) with the command
opam install touist
.
touist
can only solve SAT problems (written using propositional logic).
Problems written using the Satisfiability Modulo Theory (SMT) extension
of touist
cannot (yet) be solved, but can still be translated to the
SMT2LIB format which can then be fed to a SMT solver.
Any touist command is of the form:
touist [o OUTPUT] (INPUT  ) [options...]
The flags can be given in any order. You can use the standard input
(stdin
) instead of using an input file by setting the 
argument.
With no o
flag, touist will output to the standard output (stdout
).
Code  Label  Description 

0  OK  
1  UNKNOWN  
2  CMD_USAGE  something wrong with the commandline arguments 
3  CMD_UNSUPPORTED  
4  TOUIST_SYNTAX  any error of syntax, type or semantic 
5  TOUIST_TIMEOUT  
6  TOUIST_MEMORY  
7  TOUIST_UNKNOWN  
8  SOLVER_UNSAT  the solver did not find any model 
9  SOLVER_UNKNOWN  
10  SOLVER_TIMEOUT  
11  SOLVER_MEMORY  
Note that the SOLVER_UNSAT
is not really an error, but we choose to return
a nonzero return code anyway.
The language accepted for propositional logic is described in
3.7.3. This mode is enabled by
default, but can be optionally expressed using the sat
flag.
With no other argument, touist will simply translate the touist code to
the DIMACS format and then output the mapping table (that maps
each proposition to an integer > 0) in DIMACS comments. You can redirect
this mapping table using the table <filename>
flag.
sat
options:solve
. Ask touist to solve the SAT problem. By default, the first
model is displayed; you can ask for more models using the limit N
option. The models are separated by lines beginning with ====
and for
one model, each line contains a valuation followed by the corresponding
proposition. For example:
echo a and b  touist  solve
will display
==== model 0
1 b
1 a
==== Found 1 models, limit is 1 (limit N for more models)
which corresponds to the valuation $\{a \leftarrow 1, b \leftarrow 1\}$.
Note that the model counter begins at 0. With this format, you can easily
filter the results. For example, the following command will only show the
propositions that are true
:
echo a and b  touist  solve  grep ^1
limit N
. In conjunction with solve
, set the maximum number of
models returned. When N=0, all models are returned.
count
. Instead of returning the models, just return the count of
models. This option will only work for small problems: the number of
models explodes when the number of propositions is big.
Touist embeds a QBF solver, quantor. By default, when installing
touist
through opam, it is not built with it. To enable the QBF solver,
you must install qbf
:
opam install qbf
Then, you can solve any touistwritten QBF problem:
touist qbf solve instance.touist
latex
. Translates the given touist code to $\mbox{\LaTeX}$. The
resulting latex code only require the mathtools
package and is
compatible with Mathjax (JavaScript tool for displaying math in HTML).
This command does not print \begin{document}
nor any
latex headers (\usepackage{}
…).
show
. This option prints the formula generated by the given
touist file. This is useful for debugging and testing that the constructs
bigand
, bigor
, exact
… are correclty evaluated.
showhidden
. This is specific to the SAT mode. When displaying
the DIMACS result, also include the hidden propositions that have been
generated during the CNF expansion by the Tseitin
transformation.
linter
. This option disables all outputs except for errors. It
also shortens then evaluation step by bypassing the expansive bigand
,
exact
, powerset
… constructs.
errorformat
. Allows to format the errors as you wish. This
argument can be useful for plugging touist to another program that needs
to read the errors. The placeholders you can use are:
%f  file name 
%l  line number (start) 
%L  line number (end) 
%c  column number (start) 
%C  column number (end) 
%b  buffer offset (start) 
%B  buffer offset (end) 
%t  error type (warning or error) 
%m  error message 
\n  new line 
By default, the errors and warnings will display with the formatting
%l:%c: %t: %m
. An ending newline (\n
) is automatically added.
wrapwidth N
. Lets you choose the width of the messages (errors,
warnings) given by touist. By default, touist will wrap all messages with
a 76 characters limit. With N set to 0, you can disable the wrapping.
debugsyntax
. This is a development option that adds to the error
and warning messages the state number of the LL(1) automaton. Each state
number that may trigger a syntax error should have a corresponding
message in src/parser.messages
.
debugcnf
. This is also a development option; in SAT mode, it
prints the successive recursive transformations that produce the CNF
formula.
The language accepted by this mode is described in 3.8.
The flag smt LOGIC
enables the SMT mode.
Explain which .
LOGIC
can be given and how to use smt
How
You might have noticed that on every run of touist
, only one error is
shown at a time. Many compilers are able to show multiple errors across
the file (e.g., any C compiler). Some other compilers, like OCaml, only
display one error at a time. This feature is often expected by developers
as a time saver: one single run of the compiler to squash as many
mistakes as possible.
This feature is tightly liked to one particular trait of the grammar of
the language: the semicolon (;
). When an error comes up, the
semicolon will act as a checkpoint to which the parser will try to skip
to. Hoping that this error is only contained in this instruction, the
parser will try to continue after the semicolon.
The touist grammar does not have such an instruction marker; because of that, we are not able to skip to the next instruction.
^{1.}A whitespace is a space, tab or newline. ↩