pySMT 0.5.1: NIRA and Python 3.5
Marco Gario
pySMT 0.5.1 is out!
The highlights for this version are the support for Non-Linear Arithmetic and support for Python 3.5 for all solvers.
You can find the detailed changes at the end of this email.
As usual, you can upgrade via pip ( pip install --upgrade pysmt ) or by downloading the latest version from github ( https://github.com/pysmt/pysmt )
Cheers,
pySMT Team
----
Theories:
-
Non Linear Arithmetic (NRA/NIA): Added support for non-linear, polynomial arithmetic. This thoery is currently supported only by Z3. (PR #282)
New operator POW and DIV
LIRA Solvers not supporting Non-Linear will raise the NonLinearError exception, while solvers not supporting arithmetics will raise a ConvertExpressionError exception (see test_nlira.py:test_unknownresult)
Algebraic solutions (e.g., sqrt(2) are represented using the internal z3 object -- This is bound to change in the future.
General:
Python 3.5: Full support for Python 3.5, all solvers are now tested (and working) on Python 3.5 (PR #287)
-
Improved installed solvers check (install.py)
install.py --check now takes into account the bindings_dir and prints the version of the installed solver
Bindings are installed in different directories depending on the minor version of Python. In this way it is possible to use both Python 2.7 and 3.5.
There is a distinction btw installed solvers and solvers in the PYTHONPATH.
Qelim, Unsat-Core and Interpolants are also visualized (but not checked)
Support for reading compressed SMT-LIB files (.bz2)
Simplified HRPrinter code
Removed six dependency from type_checker (PR #283)
BddSimplifier (pysmt.simplifier.BddSimplifier): Uses BDDs to simplify the boolean structure of an SMT formula. (See test_simplify.py:test_bdd_simplify) (PR #286)
Solvers:
- Yices: New wrapper supporting python 3.5 (https://github.com/pysmt/yicespy)
- Yices: Upgrade to 2.4.2
- SMT-LIB Wrapper: Improved interaction with subprocess (#298)
Bugfix:
Bugfix in Z3Converter.walk_array_value. Thanks to Alberto Griggio for contributing this patch
Bugfix in DL Logic comparison (commit 9e9c8c)