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.

travis: set -v in order to understand

travis: fix log truncated

travis: fix log truncated

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.5.0 beta1

v3.5.0 beta1
  - Command-line
    - touist has (finally) a proper man page. To open it, use `touist --help'
    or `man touist'.
    - Command-line arguments can either be used as (for example)
      `--smt QF_LIA' or `--smt=QF_LIA'.
    - (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.

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