Releases: touist/touist
Releases · touist/touist
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)