v3.5.2

v3.5.2
  - Language:
    - added list comprehensions (also named 'set builder notation'). Really
      useful for generating sets! Example: [p($i,$j) for $i,$j in [1..2],[a,b]].
  - Command-line
    - it is now possible to display elapsed time (translation time and solve
      time) in --solve and --solver modes. To enable it, use -v/--verbose.

v3.5.1

v3.5.1
  - GUI (fixes):
    - fixed wrong line numbers displayed in error messages in QBF and SMT modes
  - Language:
    - sets and variables (and any other expression) can now be a formula;
      in order for these formulas not be evaluated as a normal boolean
      expression, they must be double quoted (e.g., "a and b => c").
  - Command-line
    - the --verbose flag now takes a number (1 for the lightest verbosity,
      2 and more for more verbosity).
    - with --solver, in order to show stdin/stdout/stderr you now have
      to use -v2 (or --verbose=2). -v only shows the count of literals/clauses.
    - fixed the empty enviroment that was given to the --solver command. Now,
      the solver command is launched using the same env as its parent.

v3.5.0

v3.5.0
  - Command-line
    - touist finally has a proper man page. To open it, use `touist --help'
      or `man touist'.
    - you can now pass arguemnts both using `--flag PARAM' or `--flag=PARAM'.
    - (BREAKING) `--smt' can be used without a logic; by default, QF_LRA is used.
    - (BREAKING) `--debug' renamed to `--verbose'
    - (BREAKING) removed `--debug-cnf' (replaced by `--show=cnf')
    - (BREAKING) removed `--debug-syntax' (replaced by `--verbose')
    - (BREAKING) removed `--latex-full (replaced by `--latex=document)
    - `--show' now takes an optional parameter (can be form, cnf, prenex).
      `--show' keeps the same behaviour but `--debug-cnf' is now `--show=cnf'.
    - `--latex' now takes an optional argument (mathjax or document).
      `--latex' stays the same and refers to `--latex=mathjax', `--latex-full'
      is removed and becomes `--latex=document'.
  - API
    - (BREAKING) Modules renamed (again, sorry!) from `TouistParse'
      to `Touist.Parse'. Function 'SatSolve.Model.pprint' takes 'table' as first
      argument.
    - (internal) use jbuilder instead of oasis, cmdliner instead of Arg.Parse.

v3.4.4 (2017-11-14)

v3.4.4 (2017-11-14)
  - Command-line
    - fix (AGAIN) the --solver option; when parsing the integers of the model,
      it was accepting non-model lines. I hope that will be enough...

v3.4.3 (2017-11-13) (2017-11-13)

v3.4.3 (2017-11-13) (2017-11-13)
  - Command-line
    - fix the option --solver with --sat solvers, once for all.
    - option --solver now supports Minisat output.

v3.4.2

v3.4.2
  - Command-line (new features)
    - the option '--solver CMD' can be used with --debug in order to display
      the stdin, stdout and stderr w.r.t. the external solver.
  - Command-line (fixes)
    - the option '--solver CMD' now uses the same error codes as with
      '--solve'; it expects the external solver to return 10 for SAT and
      20 for UNSAT (as most minisat-inspired solvers do).
    - in --sat mode, the option '--solver CMD' will now work properly instead
      of throwing "assert raised in src/Minisat.ml".

v3.4.1

v3.4.1
  - Command-line (new features)
    - added option '--solver CMD'; combined with --sat or --qbf, touist
      will run CMD feeding the (Q)DIMACS into stdin and expecting a
      DIMACS on stdout; it then prints the model as usual.
    - with --latex, fixed 'subset' that was translated into subset instead
      of subseteq.
    - (internal) drop the 'fileutils' dependency as it was not used anyway.

v3.4.0

v3.4.0
  - TouIST language:
    - 'inter', 'union', 'diff' and 'subset' are now infix operators;
      the prefix versions are still available (but they produce a warning).
  - API:
    - when touist is installed through opam ('opam install touist'), you can
      use it as a library. The API reference is now published on the website.
  - GUI (new features):
    - added the menu button 'Log' that allows to monitor what is happening
      under the hood.
    - the look of the main window has been (kind of) improved with
      less useless blank spaces. Also, the window can be resized smaller
      than before.
    - in the result view, you can now hide all valuations that
      are not true or false. For example, it allows us to hide all
      undefined valuations (denoted by '?') that clutter the results.
    - on macOS, a native application is now available; on Windows, a .exe
      is available (instead of clicking on the .jar). On Linux, a simple
      script launches the jar.
    - 'save' and 'open' now remember the last file opened; the current
      file is displayed in the window title. Also, a friendly warning is now
      displayed when opening or quitting while the current file is unsaved.
    - drag-and-drop enabled on macOS in native TouIST.app (dropping on
      the dock or in the app) and on Windows native TouIST.exe.
    - added links to the manual in 'Help' menu
  - GUI (fixes)
    - fixed 'inter', 'union' and 'subset' that were not properly colored
    - fixed the extremely slow/laggy scrolling of the latex right-panel when
      using the mouse wheel.
    - fixed the 'Solve' button hanging indefinitely in QBF mode
    - fixed the filtering (regex or true/false) of the results on SMT
      and QBF modes.
    - fixed a bug that was preventing the user from filtering when a
      single result was returned.
  - Command-line (new features):
    - in --sat mode, the new option --interactive will enable the
      display of one model at a time by pressing any key (q/n to stop).
    - it is now possible to output QDIMACS using --qbf
    - added --debug-dimacs which displays names instead of numbers in
      DIMACS (--sat) and QDIMACS (--qbf).
  - Command-line (fixes):
    - fixed a bug with --sat --solve where touist was giving a model
      although the formula is UNSAT (it was caused by a misuse of minisat).
    - fixed --latex that failing without --linter
    - (BREAKING) We had not correctly followed the DIMACS specification:
      any comments had to appear before the preamble 'p cnf 4 7'.
      Now, the mapping table (between propositions names and numbers)
      will be given before anything else (with flags --qbf or --sat).

v3.4.0-beta11

v3.4.0-beta11

• command-line: in --sat mode, the new option --interactive will enable
  the display of one model at a time by pressing any key (q/n to stop).
• command-line: it is now possible to output QDIMACS using --qbf

v3.4.0-beta10

v3.4.0-beta10

• fixed a bug with --sat & --solve where touist was giving a model
  although the formula is UNSAT (it was caused by a misuse of minisat)