#1. Introduction

#1.1. What is TouIST?

TouIST¹ 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 command-line program written in OCaml that compiles and solves TouIST problems (see 3 for usage).

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

#1.2. Check logical consequence

From a wikipedia example:

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.

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 semi-colon ";;"):

raining => cloudy       ;; Premise 1
raining                 ;; Premise 2
not cloudy              ;; Conclusion

(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 pull-request 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 CONTRIBUTE-TO-DOCS.md (located in docs/).

#2. Language reference

#2.1. Structure of a TouIST file

<touist-file> ::= <affect> <touist-file>
                | <formula> <touist-file>
                | EOF

A TouIST file is a whitespace-separated² 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.

a or b
c => a

(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>
    | """<formula-simple>""" <- quoted formula, since TouIST >= 3.5.1
<var> ::= "$" TERM                            <- simple-var
    | "$" TERM "(" <comma-list(<expr>)> ")"   <- tuple-var

Simple variable (“simple-var”)

A simple variable is of the form $my_var. In a formula, a simple variable is always expected to be a proposition or a quoted formula. In an expression, a simple variable can contain an integer, a floating-point, 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 comma-separated 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 or a quoted formula. For example, if $var=p and $i=q, then it will expand to p(q,a,4)

Tuple variables are not (yet) compatible with the set-builder construct (in 2.6.3). If one of the indexes is a set, the set will stay as-is.

Here are some examples of variables:

#2.2.2. Global affectation

We call “global variables” any variable that is affected in the top-level 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>
  | """<formula-simple>""" <-- TouIST >= 3.5.1

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:

<let-affect<T>> ::=
    | "let" <var> "=" <expr> ":" <formula<T>>     <-- local affectation
    | "let" <comma-list(<var>)> "=" <comma-list(<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, floating-point, 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: ...

  let $v=10: prop($v)
  prop($v)    ;; error: $v is not in scope anymore

#2.3. Propositions

TERM = [_0-9]*[a-zA-Z][a-zA-Z_0-9]*
<expr> ::= <int>|<float>|<prop>|<bool>|<set>
<prop> ::=
    | <var>
    | TERM
    | TERM "(" <comma-list(<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 set-building and is described in 2.6.3 and only works in expressions (not in formulas).

In the following table, the two right-columns show how the propositions are expanded whether they are in an expression or in a formula:

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

Here is the complete rule for numeric operators:

<num-operation(<T>)> ::=
    | <T> "+" <T>
    | <T> "-" <T>
    |     "-" <T>
    | <T> "*" <T>
    | <T> "/" <T>
<num-operation-others(<T>)> ::=
    | <T> "mod" <T>
    | "abs(" <T> ")"

#2.4.1. Integers

An integer constant INT is a number that satisfies the regular expression [0-9]+. Here is the rule for writting correct integer expressions:

<int> ::=
    | "(" <int> ")"
    | <var>
    | INT
    | num-operation(<int>)
    | num-operation-others(<int>)
    | "if" <bool> "then" <int> "else" <int> "end"
    | "int(" (<int>|<float>) ")"
    | "card(" <set> ")"

#2.4.2. Floats

A floating-point constant FLOAT is a number that satisfies the regular expression [0-9]+\.[0-9]+. The variants 1. or .1 are not accepted. Here is the rule for writting correct integer expressions:

<float> ::=
    | "(" <float> ")"
    | <var>
    | FLOAT
    | num-operation(<float>)
    | num-operation-others(<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:

Sets are detailed in 2.6.

Parenthesis can be used in boolean expressions. The priority order for booleans is:

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, quoted formulas 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, quoted formulas or sets (or a variable of these six types). The empty set is denoted by []. Examples:

    [1,2,3+1]
    [a,b,p(1,v)]
    [[1,2],[3,4,5]]
    ["a or b", "c => d"]

#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. Set-builder notation (list comprehension)

A set-builder expression is a set defined as , which is the set of expressions based on the cartesian product of the sets . You can use the “list comprehension” (since version 3.5.2) to do that:

[p($i,$j,$k) for $i,$j,$k in $S1,$S2,$S3]

List comprehension allows you to generate sets containing any expression: numbers, propositions and even formulas. In order to use formulas, you must use the quoted notation (see 2.7.7). The when keyword helps filter the generated elements (like in bigand or bigor). Examples:

[$i for $i in [1..100] when $i mod 3 == 0] ;; set of integers
[f($i,$j) for $i,$j in [1..3],[a,b,c]]     ;; set of propositions
[f(1,$p) for $p in [a,b,c,d] when $j != a] ;; set of propositions
["$a and $b" for $a,$b in [r,s],[x,y]]     ;; set of quoted formulas

For simple list comprehension (without when), you can use the condensed syntax: f(1,[a,b],[7..8]) which is equivalent to [f(1,$i,$j) for $i,$j in [a,b],[7..8]].

Important: the set-builder 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:

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:

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>
    | "[" <comma-list(<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:

bigand $i,$j in [1..3], [1..$i]:
    p($i,$j)
end

#2.7.2. Newline-and

As mentioned in a note (first section), in top-level, a new line (or any kind of white spaces) separating two formulas will be translated into a lesser-priority and. It is expressed in the grammar as:

<formula(<T>)>:
  | ...
  | <T> ("\n"|" ") <T>   <- newline/whitespace in top-level 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 whitespace-and 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:

<generalized-connectors(<T>)> ::=
    | "bigand" <comma-list(<var>)> "in" <comma-list(<set>)>
                             ["when" <bool>] ":" <T> "end"
    | "bigor" <comma-list(<var>)> "in" <comma-list(<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 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:

bigand $i,$j in [1..$n],[a,b,c]:
    p($i,$j)
end

bigor $v,$x,$y
      in [A,B,C],[1..9],[3..4]
      when $v!=A and $x!=$y:
    $v($x)
end

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 then Top is produced
• In bigand, if the when condition is always false then Top is produced
• In bigor, if a set is empty then Bot is produced
• In 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:

The following properties on quantifiers hold:

which helps understand why Top and Bot are produced.

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:

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.

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.

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:

<formula-simple> ::=
    | "Top"
    | "Bot"
    | <prop>
    | <var>
    | <formula(<formula-simple>)>

<formula(<T>)> ::=
    | "(" <T> ")"
    | "if" <bool> "then" <T> "else" <T> "end"
    | <connectors(<T>)>
    | <generalized-connectors(<T>)>
    | <let-affect(<T>)>

#2.7.5. 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

#2.7.6. 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):

<formula-qbf> ::=
    [...]
    | "exists" <comma-list(<prop>|<var>)> [<for>] ":" <formula-qbf>
    | "forall" <comma-list(<prop>|<var>)> [<for>] ":" <formula-qbf>

<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)

Free variables

Any free variable (i.e., not quantified) will be existentially quantified in an inner-most way. For example, will become .

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 whitespace-as-formula-separator 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 whitespace-separated formulas have different scopes. In fact, the previous formula could be re-written 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)

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.7.7. Quoted formulas (formulas as expressions)

When you want to use formulas in sets, you must use double quotes "..." to “protect” the formula from being evaluated as a normal expression (available with TouIST >= 3.5.1). For example:

    bigand $f in ["a or b", "c or d", "e"]:
        $f
    end

will give the formula

#2.8. Formal grammar

This section presents the grammar formatted in a BNF-like 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).

INT       = [0-9]+
FLOAT     = [0-9]+\.[0-9]+
TERM      = [_0-9]*[a-zA-Z][a-zA-Z_0-9]*

<touist-file> ::= <affect> <touist-file>
                 | <formula> <touist-file>
                 | EOF

<expr> ::= <int>|<float>|<prop>|<bool>|<set>
    | """<formula-simple>"""  <- Touist >= 3.5.1
<var> ::= "$" TERM
    | "$" TERM "(" <comma-list(<expr>)> ")"

<prop> ::=
    | <var>
    | TERM
    | TERM "(" <comma-list(<expr>)> ")"

<affect> ::= <var> "=" (<expr>)

<let-affect<T>> ::=
    | "let" <var> "=" <expr> ":" <formula<T>>
    | "let" <comma-list(<var>)> "=" <comma-list(<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>)>

<num-operation(<T>)> ::=
    | <T> "+" <T>
    | <T> "-" <T>
    |     "-" <T>
    | <T> "*" <T>
    | <T> "/" <T>

<num-operation-others(<T>)> ::=
    | <T> "mod" <T>
    | "abs(" <T> ")"

<int> ::=
    | "(" <int> ")"
    | <var>
    | INT
    | num-operation(<int>)
    | num-operation-others(<int>)
    | "if" <bool> "then" <int> "else" <int> "end"
    | "int(" (<int>|<float>) ")"
    | "card(" <set> ")"

<float> ::=
    | "(" <float> ")"
    | <var>
    | FLOAT
    | num-operation(<float>)
    | num-operation-others(<float>)
    | "if" <bool> "then" <float> "else" <float> "end"
    | "float(" (<int>|<float>)  ")"
    | "sqrt(" <float> ")"

<set> ::= "(" <set> ")"
    | <var>
    | "[" <comma-list(<expr>)> "]"
    | "[ <int> ".." <int> "]"      <- step is 1
    | "[ <float> ".." <float> "]"  <- step is 1.0
    | "[ <expr> "for" <comma-list(<var>)>
       "in" <comma-list(<set>)> ["when" <bool>] "]"  <- TouIST >= 3.5.2
    | <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> ")"

<comma-list(<T>)> ::= <T> | <T> "," <comma-list(<T>)>

<generalized-connectors(<T>)> ::=
    | "bigand" <comma-list(<var>)> "in" <comma-list(<set>)>
                             ["when" <bool>] ":" <T> "end"
    | "bigor" <comma-list(<var>)> "in" <comma-list(<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>)>
    | <generalized-connectors(<T>)>
    | <let-affect(<T>)>
    | <T> ("\n"|" ") <T>   <- newline/whitespace in top-level is an 'and'

<formula-simple> ::=
    | "Top"
    | "Bot"
    | <prop>
    | <var>
    | <formula(<formula-simple>)>

<formula-smt> ::=
    | <formula(<formula-smt>)>
    | <expr-smt>

<expr-smt> ::=
    | "Top"
    | "Bot"
    | <prop>
    | <var>
    | <int>
    | <float>
    | <order>(<expr-smt>)
    | <num-operations_standard(<expr-smt>)>
    | <equality(<expr-smt>)>
    | <in_parenthesis(<expr-smt>)>

<formula-qbf> ::=
    | "Top"
    | "Bot"
    | <prop>
    | <var>
    | <formula(<formula-qbf>)>
    | "exists" <comma-list(<prop>|<var>)> [<for>] ":" <formula-qbf>
    | "forall" <comma-list(<prop>|<var>)> [<for>] ":" <formula-qbf>

<for> ::= "for" <var> "in" <set>

#3. Command-line 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

#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).

The man page of touist is available through man touist or touist --help. It contains almost everything you need to know its features and arguments.

#3.2.1. Exit status

Note that the UNSAT is not really an error, but we choose to return a non-zero exit status 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 ocaml-minisat which relies on a C version of Minisat (Minisat-C-1.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 translate the given TouIST code to . Two options are available:

• with --latex (synonym of --latex=mathjax, 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 or jlatexmath).
• with --latex=document, a proper header is inserted so that the output can directly be given to pdflatex or any other fully-featured latex processor. The mathtools package is necessary for \begin{pmatrix*} when matching parenthesis span across multiple lines.

--show=AST outputs the AST or translation steps; AST can be - form shows the formula generated by the given TouIST file. This is useful for debugging and testing that the constructs bigand, bigor, exact… are correclty evaluated. - cnf shows the AST after the CNF transformation (warning: huge). - duringcnf shows the recursive translation steps leading to the CNF AST. - prenex and duringprenex are similar to the two previous ones but for prenex transformation (only with --qbf).

--show-hidden 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.

--error-format 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:

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.

--wrap-width 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.

--verbose[=N] or -v[N] (N defaults to 1) prints more information on timing and errors. With no N given (i.e., N=1):

• time spent on translation and solving are displayed (see table 12).
• on syntax error, print more AST context ((loc) for example).
• when an exception is raised, tries to show the stack trace.
• on syntax error, print 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.

With N ≥ 2, --solver=CMD displays the stdin, stdout and stderr of CMD.

#3.2.4. Usage for Satisfiability Modulo Theory (SMT mode)

The language accepted by the SMT mode is described in 2.7.5.

By default, touist is able to translate problems into the SMT-LIB format with the --smt=LOGIC flag. In this mode, LOGIC can be any non-whitespace string of characters (which will be transformed in uppercase automatically). LOGIC will simply be used to fill the correct field in the SMT-LIB 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 non-commercial purposes. Its code is licensed under a restrictive non-commercial 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 re-installed 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:

Note that QF means quantifier-free. 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 (non-restrictive) 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 [--sat|--qbf] --solver="<cmd-and-arguments>" [--verbose]

For debugging purposes, you can add --verbose to see the stdin/stdout/stderr. The exit 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

• should return 10 (as error code) if problem is SAT, 20 if UNSAT.

Tested SAT solvers (brew is available on linux and mac):

• minisat

  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="glucose-syrup -model"

Tested QBF solvers:

• caqe (2017-07-19, CAQE qbfeval 2017, binary release without certification). Download the version CAQE qbfeval 2017 (2017-07-19) binary release without certification which will give you caqe-mac:

  touist test/qbf/allumettes2.touist --qbf --solver="./caqe-mac --partial-assignments"

  They also have a Homebrew tap repository but this version does not contain the needed --partial-assignments.

• qute (2017-02-27, fork maelvalais/qute, minisat-based)

  brew install touist/touist/qute
  touist test/qbf/allumettes2.touist --qbf --solver="qute --partial-certificate"

• depqbf (2017-08-02, DepQBF 6.03, Minisat-based QCDCL)

  brew install depqbf
  touist test/qbf/allumettes2.touist --qbf --solver="depqbf --qdo --no-dynamic-nenofex"

• quantor (2014-10-26, 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 semi-colon (;). When an error comes up, the semi-colon 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 semi-colon.

The TouIST grammar does not have such an instruction marker; because of that, we are not able to skip to the next instruction.