pySMT 0.6.1: Portfolio and Coverage

[Marco Gario]

pySMT 0.6.1 is out! For this release we have been working hard to improve the quality of the codebase. One way we did this was to start actively tracking the coverage of our tests. This showed that some parts of the code were not being tested properly, highlighted a few bugs, and allowed us to clean-up some tests that were now useful.

The other interesting feature from this release is the support of the Portfolio approach. This makes it possible to execute multiple solvers in parallel, and take the result of the first one that finishes. Using the portfolio with the shortcuts is as simple as calling is_sat(f, portfolio=["msat", "z3"]) .

A lot of other work was done to improve the documentation, mostly spurred by the Hacktoberfest!

Overall, we are thankful to everybody that provided feedback and patches for this release (the full list is in the release notes below).

Let us know what you think!

pySMT Team

--

General:

• Portfolio Solver (PR #284):

  Created Portfolio class that uses multiprocessing to solve the
  problem using multiple solvers. get_value and get_model work after a
  SAT query. Other artifacts (unsat-core, interpolants) are not
  supported.
  Factory.is_* methods have been extended to include portfolio
  key-word, and exported as is_* shortcuts. The syntax becomes:

  is_sat(f, portfolio=["s1", "s2"])
  

• Coverage has been significantly improved, thus giving raise to some
  clean-up of the tests and minor bug fixes. Thanks to Coveralls.io
  for providing free coverage analysis. (PR #353, PR #358, PR #372)

• Introduce PysmtException, from which all exceptions must
  inherit. This also introduces hybrid exceptions that inherit both
  from the Standard Library and from PysmtException (i.e.,
  PysmtValueError). Thanks to Alberto Griggio for
  suggesting this change. (PR #365)

• Windows: Add support for installing Z3. Thanks to Samuele
  Gallerani for contributing this patch. (PR #385)

• Arrays: Improved efficiency of array_value_get (PR #357)

• Documentation: Thanks to the Hacktoberfest for sponsoring these
  activities:

  • Every function in shortcuts.py now has a docstring! Thanks to
    Vijay Raghavan for contributing this patch. (PR #363)

  • Contributing information has been moved to the official
    documentation and prettyfied! Thanks to Jason Taylor Hodge for
    contributing this patch. (PR #339)

  • Add link to Google Group in Readme.md . Thanks to @ankit01ojha for
    contributing this. (PR #345)

• smtlibscript_from_formula(): Allow the user to specify a custom
  logic. Thanks to Alberto Griggio for contributing this
  patch. (PR #360)

Solvers:

• MathSAT: Improve back-conversion performance by using MSAT_TAGS (PR #379)

• MathSAT: Add LIA support for Quantifier Elimination

• Removed: Solver.declare_variable and Solver.set_options (PR #369,
  PR #378)

Bugfix:

• CVC4:

  • Enforce BV Division by 0 to return a known value (0xFF) (PR #351)

  • Force absolute import of CVC4. Thanks to Alexey Ignatiev
    (@2sev) for reporting this issue. (PR #382)

• MathSAT: Thanks to Alberto Griggio for contributing these patches

  • Fix assertions about arity of BV sign/zero extend ops. (PR #350, PR #351)

  • Report the error message generated by MathSAT when raising a
    SolverReturnedUnknownResultError (PR #355)

• Enforce a single call to is_sat in non-incremental mode (PR
  #368). Thanks to @colinmorris for pointing out this issue.

• Clarified Installation section and added example of call to pysmt-install --env. Thanks to Marco Roveri
  (@marcoroveri) for pointing this out.

• SMT-LIB Parser:

  • Minor fixes highlighted by fuzzer (PR #376)

  • Fixed annotations parsing according to SMTLib rules (PR #374)

• pysmt-install: Gracefully fail if GIT is not installed (PR #390)
  Thanks to Alberto Griggio for reporting this.

• Removed dependency from internet connections when checking picosat
  version (PR #386)