Release: 0.8.1

[marcogario]

0.9.0: 2020-04-13 -- PySMT as module

General:

• PySMT as module (PR Define main function for pysmt as module #573): It is now possible to do
  python -m pysmt install

  and

  python -m pysmt shell

  while the tool pystm-install is still available, using the module syntax makes it easier to understand which version of python will be used, in case multiple interpreters co-exist.

• Added functions to obtain the symbols in SMTLIB script (PR Added functions to obtain the symbols in SMTLIB script #583)

• Python 2 is not supported anymore. While it might still work, we will not actively test for it anymore.

Solvers:

• Boolector: Incremental and Unsat cores support (PR Unsat cores from boolector #591, Incremental support for boolector #567). Thanks Makai Mann for providing the patch.

• Picosat: Fixed a bug related to solver reset (PR Incremental support for boolector #567)

• Boolector: Upgrade to 3.2.1

• MathSAT: Upgrade to 5.6.1

• Yices: Upgrade to 2.6.2

Bugfix:

• Collections.abc: fix deprecation warning (PR Collections.abc: fix deprecation in formula.py #574, PR Fix import warning in python 3.7 #562). Thanks to Liana Hadarean and Caleb Donovick.

• PysmtSyntaxError: Fix missing message constructor (PR PysmtSyntaxError: Fix missing message in init #576). Thanks to Liana Hadarean for providing a fix.

• Version: Static version in make_distrib.sh (PR Static Version number in package #575)

• Fix simplifier StrIndexOf capitalization (PR StrIndexof Typo in simplifier.py #563). Thanks to Makai Mann for providing the patch.

• Sort the arguments of Times while simplifying (PR sort the times args while simplifying #561). Thanks to Ahmed Irfan for providing the patch.

• Fix bug in deque pop in smtlib/parser (PR Fix bug in deque pop in smtlib/parser #558). Thanks to Sebastiano Mariani for providing the patch.

• Function names quoted with ' instead of | when seraializing to smt2 (PR Function names quoted with ' instead of | when seraializing to smt2 #584). Thanks Kevin Laeufer for reporting this.

• Fix assertion tracking for boolector (PR Fix assertion tracking for boolector #589). Thanks Makai Mann for providing the patch.

• Handle one-bit shifts in btor (PR Handle one-bit shifts in btor #592) Thanks Makai Mann for providing the patch.

• Fix issue with bv conversion in Yices (PR Fixed issue #596 #597). Thanks to @nano-o for reporting this.

• Fix Mathsat signature for BV_CONCAT (PR Fix mathsat signature for BV_CONCAT #598). Thanks Makai Mann for providing the patch.

• Support n-ary BVConcat (PR Fixed #620 by allowing n-ary BVConcat in the frontend  #621). Thanks to Ridwan Shariffdeen for reporting this.

• Fix a correctness issue when reading from SMT-LIB interface (Issue Correctness bug using an SMTLibSolver #616, No effect setting the 'debug_interaction' option in the SmtLibSolver  #615, PR Fixed issue #616 and #615 #619). Thanks to Sergio Mover for reporting this.

• Clear pending assertions in IncrementalTrackingSolver.assertions (PR add clear pending pop decorator to assertions property of solvers. #627). Thanks to Enrico Magnago for reporting this.

• Various documentation fixes. Thanks to Matthew Fernandez, Guillem Francès, and Gianluca Redondi.

[marcogario]

⚠️ Installation for Btor fails on my Ubuntu. The problem seems to be that the version of btor2tools is not pinned in the Btor config script. Therefore, we are trying to use a newer version of btor2tools that does not accept the -fPIC argument.

I originally wanted to publish this as 0.8.1 and work on 0.8.2 with the new changes since, but now it seems that it is easier to release 0.8.1 with all changes to date since 0.8.0.

Next Steps

• Update release to include master
• Check whether btor now pins btor2tools
  - Yes, since Boolector/boolector@2c1da71#diff-6d813c459ed338cff31aa1235de5fbe5
• Check new versions of solvers
  • Boolector - 3.2.1 https://github.com/Boolector/boolector/releases/tag/3.2.1
    - Needs recent version of cython to work, this is ok for CI, since we pip install cython.
  • Z3 - 4.8.7 https://github.com/Z3Prover/z3/releases
    - `WARNING: unknown parameter 'model_compress'
    - Zero division error on model
  • [x ] MSat - 5.6.1 https://mathsat.fbk.eu/releasenotes.html
  • [ x] Yices - 2.6.2 https://yices.csl.sri.com/release-notes.html
  • [x ] Picosat - 965 No need to upgrade.
  • CVC4 - 1.7 https://github.com/CVC4/CVC4/releases/tag/1.7
    - requires toml
    - Detection of python version might find systems version before current python.
• Update Changelog

[marcogario]

Not released. All changes are now part of 0.9.0 See #635 for details.