#1. Introduction
#1.1. What is TouIST?
TouIST^{1} is a language that allows us to express
propositional
logic [1, 2, 5].
You are provided with two programs: a graphical interface, refered as
touist.jar
(as it is written in Java) and touist
, a commandline
program written in OCaml that compiles and solves TouIST problems
(see 3 for usage).
Propositional logic  TouIST language 

not p  
p and q  
p or q  
p xor q  
p => 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 is . To check the models of this formula using TouIST, you can do
Graphical Java interface  Commandline interface (see 3.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 
#1.2. Check logical consequence
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 () 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 be a set of formulas (called hypotheses or premises) and a
formula (called conclusion). Then
if and only if 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
#1.3. Contribute to this document
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/
).
This reference manual still lacks of a stepbystep tutorial as well as illustrating examples. Feel free to contribute! .
#2. Language reference
#2.1. Structure of a TouIST file
<touistfile> ::= <affect> <touistfile>
 <formula> <touistfile>
 EOF
A TouIST file is a whitespaceseparated^{2} 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 2.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 or b) and (c => a)
#2.2. Variables
First, we describe what a variable is. Then, we detail how to affect variables (with global or local affectations).
#2.2.1. Syntax of a variable
<expr> ::= <int><float><prop><bool><set>
<var> ::= "$" TERM < simplevar
 "$" TERM "(" <commalist(<expr>)> ")" < tuplevar
 Simple variable (“simplevar”)
 A simple variable is of the form
$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.  Tuple variable (can be seen as a predicate)
 A tuple variable is a simple variable followed by a commaseparated list of
indexes in braces, e.g.,
$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.  A tuple variable will always be expanded to a proposition. For example, if
$var=p
and$i=q
, then it will expand top(q,a,4)
 Tuple variables are not (yet) compatible with the setbuilder construct (in 2.6.3). If one of the indexes is a set, the set will stay asis.
Here are some examples of variables:
Simplevar  Tuplevar 

$N  $place($number) 
$time  $action($i,$j) 
$SIZE  
$is_over  
#2.2.2. Global affectation
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
#2.2.3. Local affectation (let
construct)
Sometimes, you want to use the same result in multiple places and you
cannot use a global variable (presented in 2.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
 "let" <commalist(<var>)> "=" <commalist(<expr>)> ":" <formula<T>>
<expr> ::= <int><float><prop><bool><set>
The let
affectation can only be used in formulas (detailed
in 2.7) and cannot be used in expressions (<expr>
, i.e.,
integer, floatingpoint, boolean or set expressions).
Example:
;; This piece of code has no actual purpose
$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
You can also chain multiple variables in a single let
:
let $E,$x,$y = [1..2],3,4: ...
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
#2.3. Propositions
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.
#2.3.1. Tuple proposition containing a 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 2.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)]  
#2.4. Numeric expression
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.
#2.4.1. Integers
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> ")"
#2.4.2. Floats
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> ")"
#2.5. Booleans
The constants are true
and false
. The boolean connectors are ,
, (>=
), (<=
), (==
) and (!=
). The
operators that return a boolean are $P subset $Q
, empty($P)
and
p in $P
:
$P subset $Q  is a subset (or is included in)  
empty($P)  is an empty set  
$i in $P  is an element of the set  
Sets are detailed in 2.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>
 <set> "subset" <set> < TouIST >= 3.4.0
 "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>
#2.6. Sets
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:
#2.6.1. Sets defined by enumeration
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 is denoted by []
.
#2.6.2. Sets defined by a range
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.
#2.6.3. Setbuilder notation
, which the set
of tuple propositions based on the cartesian product of the sets ,
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).
#2.6.4. Operators using sets
Some common set operators are available. Let and denote two sets:
Type  Syntax  Math notation  Description 

<set>  $P inter $Q  intersection  
<set>  $P union $Q  union  
<set>  $P diff $Q  difference  
<set>  powerset($Q)  powerset  
<int>  card($S)  cardinal  
<bool>  empty($P)  set is empty  
<bool>  $e in $P  belongs to  
<bool>  $P subset $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 (2.5).
The priority on operators is:
highest priority  inter 
lowest priority  union , diff 
Up to .
TouIST v3.2.3, the operators inter
, union
, diff
and
subset
were prefix operators (e.g., inter($A,$B)
). From v3.4.0
and later, these prefix operators are deprecated (but still usable).
Instead, we provide more humanfriendly infix operators (e.g.,
$A inter $B
).
Powerset
The powerset($Q)
operator generates all possible subsets such
that . 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
 <set> "inter" <set>
 <set> "union" <set>
 <set> "diff" <set>
 "powerset(" <set> ")"
#2.7. Formulas
#2.7.1. Connectors
A formula is a sequence of propositions (that can be variables) and connectors
(not
), (and
), (or
), (xor
),
(=>
) or (<=>
).
<connectors(<formula<T>>)> ::=
 "not" <T>
 <T> "and" <T>
 <T> "or" <T>
 <T> "xor" <T>
 <T> "=>" <T>
 <T> "<=>" <T>
Parenthesis can be used in formulas in order to express priority. The default operator priority is:
highest priority  not 
xor  
and  
or  
=> , <=>  
lowest priority  newlineand (2.7.2) 
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
#2.7.2. Newlineand
As mentioned in a note (first section), in toplevel, a
new line (or any kind of white spaces) separating two formulas will be
translated into a lesserpriority and
. It is expressed in the grammar as:
<formula(<T>)>:
 ...
 <T> ("\n"" ") <T> < newline/whitespace in toplevel is an 'and'
This notation is related to the idea of a set of formulas (premises). For example, a new line would allow to express the separation of these two formulas:
You can write this either with
a
a => b
not c
or
a a => b not c
that are equivalent to
The important thing to notice is that this whitespaceand
has a
lower priority than any other connector.
#2.7.3. Generalized connectors
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> ")"
Bigand and bigor
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… 

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 us 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:




Special cases for quantifier elimination
Here is the list of “limit” cases where bigand
and bigor
will produce
special results:
 In
bigand
, if a set is empty thenTop
is produced  In
bigand
, if thewhen
condition is always false thenTop
is produced  In
bigor
, if a set is empty thenBot
is produced  In
bigor
, if thewhen
condition is always false thenBot
is produced
These behaviors come from the idea of quantification behind the
bigand
and bigor
operators:
Universal quantification  bigand $x in $S: p($x) end  
Existential quantification  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. .
Exact, atmost and atleast
The TouIST language 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 

atmost($k,$P)  
atleast($k,$P)  
exact($k,$P)  
Let be a set of propositions, a proposition and a positive integer. Then:
 represents "at any time, at most propositions must be true"
 represents "at any time, at least propositions must be true"
 represents "at any time, exactly propositions must be true"
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 conjunctions.
The notation .
p([1..20])
is called “setbuilder” and is defined
in 2.6.3. Using this syntax, the formula exact(5,p([1..20])
is equivalent to
Example 1.
exact(2,[a,b,c])
is equivalent to
Special cases for operator elimination
The following table sums up the various “limit” cases that may not be obvious. In this table, is a positive integer and is a set of propositions.
$k  $P  Gives  

exact($k,$P)  Top  
bigand $p in $P: not $p end  
bigand $p in $P: $p end  
atleast($k,$P)  any  Top  
any  bigor $p in $P: $p end  
Bot (subcase of next row)  
Bot  
bigand $p in $P: $p end  
atmost($k,$P)  Top (subcase of next row)  
any  Top  
How to read the table: for example, the row where and
should be read "when using atleast
, all couples
will produce the special case
Top
".
#2.7.4. Propositional logic formulas
The constants (Top
) and (Bot
) allow us 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>)>
#2.8. SMT formulas
The TouIST language also accepts formulas of the Satisfiability Modulo Theory (SMT).
To use the touist
program with SMT formulas, see 3.2.4
Describe the SMT language .
#2.9. QBF formulas
The TouIST language accepts Quantified Boolean Formulas (QBF). 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
) and (forall
):
<formulaqbf> ::=
[...]
 "exists" <commalist(<prop><var>)> [<for>] ":" <formulaqbf>
 "forall" <commalist(<prop><var>)> [<for>] ":" <formulaqbf>
<for> ::= "for" <var> "in" <set>
One quantifier can quantify over multiple propositions. For example:
forall e,d: (exists a,b: a => b) => (e and forall c: e => c)
#2.9.1. Free variables
Any free variable (i.e., not quantified) will be existentially quantified in an innermost way. For example, will become .
#2.9.2. Renaming during the prenex transformation
Using the rules for transforming an arbitrary formula into prenex form requires sometimes some renaming. For example, must be transformed into .
Sometimes, the renaming is not possible. For example, in
, we cannot guess which quantifier the
rightmost 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)
#2.9.3. Multiple exists
or forall
The keyword for
used in exists
or forall
allow us to generate
multiple quantifiers using sets. Imagine that you want to write
You can use one of the two notations:
exists a: exists b: exists c: exists d: phi ;; (1)
exists $p for $p in [a,b,c,d]: phi ;; equivalent to (1)
#2.10. Formal grammar
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>>
 "let" <commalist(<var>)> "=" <commalist(<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
 <set> "inter" <set> < TouIST >= 3.4.0
 <set> "union" <set> < TouIST >= 3.4.0
 <set> "diff" <set> < TouIST >= 3.4.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>)>
 <T> ("\n"" ") <T> < newline/whitespace in toplevel is an 'and'
<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>)> [<for>] ":" <formulaqbf>
 "forall" <commalist(<prop><var>)> [<for>] ":" <formulaqbf>
<for> ::= "for" <var> "in" <set>
#3. Commandline tool (touist
)
#3.1. Installation
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
By default, .
touist
only comes with a SAT solver. Problems written in
TouIST using the Satisfiability Modulo Theory (SMT) or Quantified
Boolean Formulas (QBF) grammars can also be used (see 3.2.4 and
3.2.5).
#3.2. Usage
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
).
#3.2.1. Return codes
Code  Label  Description 

0  OK  with –solve or –solver, means SAT 
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.
#3.2.2. Usage for propositional logic (SAT mode)
The language accepted for propositional logic is described in
2.7.4. This mode is enabled by
default, but can be optionally expressed using the sat
flag.
Mapping table for DIMACS output
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 before the prelude
line (i.e., p cnf x y
; comments must be before the prelude line in the
DIMACS specification). For example, if you run:
echo 'rain => wet_road rain not wet_road'  touist 
you will get the output:
c wet_road 1 < mapping between DIMACS integers and propositions
c rain 2
p cnf 2 3 < prelude of the DIMACS file
1 2 0
2 0
1 0
You can redirect this mapping table using the table <filename>
flag.
SAT solver
By default, touist
embeds Minisat (see [6]), a SAT solver
written in C++ at the Chalmers University of Technology, Sweden. It is
distributed under the MIT license. To be able to embed it into OCaml,
we use the binding ocamlminisat which relies on a C version of Minisat
(MinisatC1.14.1) for portability concerns.
solve
asks 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 return a single model (and in this case, there is only one single model):
1 a
1 b
Each line corresponds to a valuation, and each valuation should be read
value proposition
. In the example, takes the value 1 (true).
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
**solve interactive
allows the user to display the models one after
the other. Press enter or any other key to continue and q
or n
to stop.
solve limit N
allows to display multiple models. With this 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, with limit 0
which displays an unlimited number of models:
echo a or b  touist  solve limit 0
will display
==== model 0
1 a
0 b
==== model 1
0 a
1 b
==== model 2
1 a
1 b
==== found 3 models, limit is 0 (limit N for more models)
Note that the model counter begins at 0.
solve count
tries to return the count of models instead of
returning the models. This option will only work for small problems: the
number of models explodes when the number of propositions is big.
#3.2.3. Other general options
The following general options must be using in conjunction of smt
, qbf
or sat
(sat
is used by default and can be omitted).
latex
, latexfull
translate the given TouIST code to
. Two options are available:
 with
latex
, only the math formulas are translated and no header/footer is added (e.g.,\begin{document}
). This mode is compatible with any light latex processors (e.g.,mathjax
orjlatexmath
).  with
latexfull
, a proper header is inserted so that the output can directly be given topdflatex
or any other fullyfeatured latex processor. Themathtools
package is necessary for\begin{pmatrix*}
when matching parenthesis span across multiple lines.
show
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
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
disables all outputs except for errors. It also shortens
then evaluation step by bypassing the expansive bigand
, exact
,
powerset
… constructs.
errorformat
allows the user 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
%f: line %l, col %c%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
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/lib/parser.messages
.
debugcnf
(only with sat
or qbf)
) is also a development
option; in SAT and QBF modes, it prints the successive recursive
transformations that produce the CNF formula.
debug
is a development option that displays the status of the
Minisat solver, the call stack in case of unexpected errors and also
displays errors with more AST context ((loc)
for example).
#3.2.4. Usage for Satisfiability Modulo Theory (SMT mode)
The language accepted by the SMT mode is described in 2.8.
By default, touist
is able to translate problems into the
SMTLIB
format with the smt LOGIC
flag. In this mode,
LOGIC
can be any nonwhitespace string of characters (which will be
transformed in uppercase automatically). LOGIC
will simply be used
to fill the correct field in the SMTLIB
file.
SMT solver
TouIST can embed an optional SMT solver, Yices 2.5.2 (see
[4]). It is developed by SRI (Stanford Research Institute,
California) and is written in C. It is free to use for noncommercial
purposes. Its code is licensed under a restrictive noncommercial EULA
which the user must agree before using (see the license). To
enable it, you need to install the OCaml binding yices2
which
embeds the Yices sources:
opam install yices2
If touist
was previously installed, it will be reinstalled to support
the newly installed yices2
.
When using both smt LOGIC
and solve
, the LOGIC
argument must be
one of the logics Yices 2.5.2 supports. Here is a table
with the logics that are can be used through the TouIST language:
LOGIC  Meaning 

QF_IDL  Integer Difference Logic 
QF_RDL  Real Difference Logic 
QF_LIA  Linear Integer Arithmetic 
QF_LRA  Linear Real Arithmetic 
Note that QF means quantifierfree. Also note that you can solve any SAT problem using any SMT logic solver.
For example:
echo 'x > 3'  touist smt QF_IDL solve 
which will give you the model
4 x
which should be read as takes the value 4.
#3.2.5. Usage for quantified boolean logic (QBF mode)
For now, the QDIMACS
format (which is the equivalent of DIMACS
for
quantified boolean formulas) cannot be printed from a TouIST file.
You can still solve problems using both qbf
and solve
(see below).
QBF solver
touist
can embed an optional QBF solver, Quantor 3.2 (see
[3]). It is developed at the Johannes Kepler University, Austria.
Its source is under a (nonrestrictive) BSD license. To enable the QBF
solver, you must install the OCaml binding qbf
which embeds
the Quantor source:
opam install qbf
Then, we can solve a small example:
echo 'forall x: x or (exists y: y)'  touist qbf solve 
which will give you a partial model:
? x
? y
where ?
means that this value is undefined. To get an actual mode, we
must force the valuations (and doing so, we explore the tree of possible
valuations). touist
and its graphical interface are unable to force these
valuations and explore the tree. As a consequence, they are also unable
to visualize the tree (where each leaf would be a model). For now, the only
way to do it is by hand.
#3.3. Using external solvers from touist
(solver
)
Most SAT and QBF solvers accept the standardized DIMACS (resp.
QDIMACS) as input language. You can give the DIMACS output of touist
directly to the solver and use the mapping table (see 3.2.2.1).
But you can use TouIST to do both the call to the solver as well as the
translation of the resulting DIMACS model back to propositions names, using
the argument solver
:
touist solver "<cmdandarguments>" [debug]
For debugging purposes, you can add debug
to see the stdin/stdout/stderr.
The return code of touist
is the same as with solve
.
The external solvers must use the following Minisat + (Q)DIMACS conventions:
 should accept DIMACS or QDIMACS on standard input;
 should print a model (or a partial model) in DIMACS on standard output; the
model can span on multiple lines, each line begins with v
, V
or nothing (for Minisat compatibility), and each line is optionally ended
with 0.
v 1 2 3 4 0
v 5 6 0
(v
and V
are both supported; 0 is optional);
 should return 10 (as error code) if problem is SAT, 20 if UNSAT.
Tested SAT solvers (brew
is available on linux and mac):

brew install minisat touist test/sat/sudoku.touist solver "minisat /dev/stdin /dev/stdout"

picosat (2015, version 965, SAT Race'15)
brew install touist/touist/picosat touist test/sat/sudoku.touist solver "picosat partial"

glucose (2016, version 4.1, syrup is the parallel version)
brew install touist/touist/glucose touist test/sat/sudoku.touist solver "glucose model" touist test/sat/sudoku.touist solver "glucosesyrup model"
Tested QBF solvers:

caqe (20170719, CAQE qbfeval 2017, binary release without certification). Download the version CAQE qbfeval 2017 (20170719) binary release without certification which will give you
caqemac
:touist test/qbf/allumettes2.touist qbf solver "./caqemac partialassignments"
They also have a Homebrew tap repository but this version does not contain the needed
partialassignments
. 
qute (20170227, fork maelvalais/qute, minisatbased)
brew install touist/touist/qute touist test/qbf/allumettes2.touist qbf solver "qute partialcertificate"

depqbf (20170802, DepQBF 6.03, Minisatbased QCDCL)
brew install depqbf touist test/qbf/allumettes2.touist qbf solver "depqbf qdo nodynamicnenofex"

quantor (20141026, Quantor 3.2). It is not necessary to use this solver externally as it is included with
touist
(see 3.2.5.1).brew install touist/touist/quantor touist test/qbf/allumettes2.touist qbf solver "quantor"

rareqs (2012, v1.1, CEGAR)
brew install touist/touist/rareqs touist test/qbf/allumettes2.touist qbf solver "rareqs"
#4. Technical details
#4.1. One single syntax error per run
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.