Developing in pySMT

Licensing

pySMT is distributed under the APACHE License (see LICENSE file). By submitting a contribution, you automatically accept the conditions described in LICENSE. Additionally, we ask you to certify that you have the right to submit such contributions. We adopt the “Developer Certificate of Origin” approach as done by the Linux kernel.

Developer Certificate of Origin Version 1.1

Copyright (C) 2004, 2006 The Linux Foundation and its contributors. 660
York Street, Suite 102, San Francisco, CA 94110 USA

Everyone is permitted to copy and distribute verbatim copies of this
license document, but changing it is not allowed.

Developer’s Certificate of Origin 1.1

By making a contribution to this project, I certify that:

(a) The contribution was created in whole or in part by me and I have
    the right to submit it under the open source license indicated in
    the file; or

(b) The contribution is based upon previous work that, to the best of my
    knowledge, is covered under an appropriate open source license and I
    have the right under that license to submit that work with
    modifications, whether created in whole or in part by me, under the
    same open source license (unless I am permitted to submit under a
    different license), as indicated in the file; or

(c) The contribution was provided directly to me by some other person
    who certified (a), (b) or (c) and I have not modified it.

(d) I understand and agree that this project and the contribution are
    public and that a record of the contribution (including all personal
    information I submit with it, including my sign-off) is maintained
    indefinitely and may be redistributed consistent with this project
    or the open source license(s) involved.

During a Pull-Request you will be asked to edit the CONTRIBUTORS file to add your name and email address. By doing so, you agree to the CLA. You will only have to complete this once, but this applies to all your contributions.

Tests

Running Tests

Tests in pySMT are developed using python’s built-in testing framework unittest. Each TestCase is stored into a separate file, and it should be possible to launch it by calling the file directly, e.g.: $ python test_formula.py.

However, the preferred way is to use pytest, e.g.: $ python -m pytest pysmt/tests/test_formula.py.

There are two utility scripts to simplify the testing of pysmt: run_tests.sh and run_all_tests.sh. They both exploit additional options for pytest, such as timeouts. run_all_tests.sh includes all the tests that are marked as slow, and therefore might take some time to complete.

Finally, tests are run across a wide range of solvers, versions of python and operating systems using Travis CI. This happens automatically when you open a PR. If you want to run this before submitting a PR, create a (free) Travis CI account, fork pySMT, and enable the testing from Travis webinterface.

All tests should pass for a PR to be merged.

Writing Tests

TestCase should inherit from pysmt.test.TestCase. This provides a default SetUp() for running tests in which the global environment is reset after each test is executed. This is necessary to avoid interaction between tests. Moreover, the class provides some additional assertions:

PYSMT_SOLVER

The system environment variable PYSMT_SOLVER controls which solvers are actually available to pySMT. When developing it is common to have multiple solvers installed, but wanting to only test on few of them. For this reason PYSMT_SOLVER can be set to a list of solvers, e.g., PYSMT_SOLVER="msat, z3" will provide access to pySMT only to msat and z3, independently of which other solvers are installed. If the variable is unset or set to all, it does not have any effect.

How to add a new Theory within pySMT

In pySMT we are trying to closely follow the SMT-LIB standard. If the theory you want to add is already part of the standard, than many points below should be easy to answer.

  1. Identify the set of operators that need to be added
    You need to distinguish between operators that are needed to represent the theory, and operators that are syntactic sugar. For example, in pySMT we have less-than and less-than-equal, as basic operators, and define greater-than and greater-than-equal as syntactic sugar.
  2. Identify which solvers support the theory
    For each solver that supports the theory, it is important to identify which sub/super-set of the operators are supported and whether the solver is already integrated in pySMT. The goal of this activity is to identify possible incompatibilities in the way different solvers deal with the theory.
  3. Identify examples in “SMT-LIB” format
    This provides a simple way of looking at how the theory is used, and access to cheap tests.

Once these points are clear, please open an issue on github with the answer to these points and a bit of motivation for the theory. In this way we can discuss possible changes and ideas before you start working on the code.

Code for a new Theory

A good example of theory extension is represented by the BitVector theory. In case of doubt, look at how the BitVector case (bv) has been handled.

Adding a Theory to the codebase is done by following these steps:

  1. Tests: Add a test file pysmt/test/test_<theory>.py, to demonstrate the use for the theory (e.g., pysmt/test/test_bv.py).
  2. Operators: Add the (basic) operators in pysmt/operators.py, create a constant for each operator, and extend the relevant structures.
  3. Typing: Extend pysmt/typing.py to include the types (sorts) of the new theory.
  4. Walker: Extend pysmt/walkers/generic.py to include one walk_ function for each of the basic operators.
  5. FNode: Extend is_* methods in pysmt/fnode.py:FNode. This makes it possible to check the type of an expression, obtaining additional elements (e.g., width of a bitvector constant).
  6. Typechecker: Extend pysmt/type_checker.py:SimpleTypeChecker to include type-checking rules.
  7. FormulaManager: Create constructor for all operators, including syntactic sugar, in pysmt/formula.py:FormulaManager.

At this point you are able to build expressions in the new theory. This is a good time to start running your tests.

  1. Printers: Extend pysmt/printers.py:HRPrinter to be able to print expressions in the new theory (you might need to do this earlier, if you need to debug your tests output).
  2. Examples: Extend pysmt/test/examples.py with at least one example formula for each new operator defined in FormulaManager. These examples are used in many tests, and will help you identify parts of the system that still need to be extended (e.g., Simplifier).
  3. Theories and Logics: Extend pysmt/logics.py to include the new Theory and possible logics that derive from this Theory. In particular, define logics for each theory combination that makes sense.
  4. SMT-LIB: Extend pysmt/smtlib/parser.py:SmtLibParser and pysmt/smtlib/printers.py to support the new operators.
  5. Shortcuts: All methods that were added in FormulaManager need to be available in pysmt/shortcuts.py.

At this point all pySMT tests should pass. This might require extending other walkers to support the new operators.

  1. Solver: Extend at least one solver to support the Logic. This is done by extending the associated Converter (e.g., pysmt/solvers/msat.py:MSatConverter) and adding at least one logic to its LOGICS field. As a bare-minimum, this will require a way of converting solvers-constants back into pySMT constants (Converter.back()).

Packaging and Distributing PySMT

The setup.py script can be used to create packages. The command

python setup.py bdist --format=gztar

will produce a tar.gz file inside the dist/ directory.

For convenience the script make_distrib.sh is provided, this builds both the binary and source distributions within dist/.

Building Documentation

pySMT uses Sphinx for documentation. To build the documentation you will need Sphinx installed, this can be done via pip.

A Makefile in the docs/ directory allows to build the documentation in many formats. Among them, we usually consider html and latex.

Preparing a Release (Check-List)

In order to make a release, the master branch must pass all tests on the CI (Travis and Appveyor). The release process is broken down into the following steps:

  • Release branch creation
  • Changelog update
  • Version change
  • Package creation and local testing
  • Merge and Tag
  • PyPi update
  • Version Bumping
  • Announcement

Release Branch Creation

As all other activities, the creation of a release requires working on a separate branch. This makes it possible to interrupt, share, and resume the release creation, if bugs are discovered during this process. The branch must be called rc/a.b.c, where a.b.c is the version number of the target release.

Changelog Update (docs/CHANGES.rst)

Use git log to obtain the full list of commits from the latest tag. We use merge commits to structure the Changelog, however, sometimes additional and useful information is described in intermediate commits, and it is thus useful to have them.

The format of the header is <version>: <year> -- <Title>, where version has the format Major.Minor.Patch (e.g., 0.6.1) and year is in ISO format: YYYY-MM-DD (e.g., 2016-11-28). The title should be brief and possible include the highlights of the release.

The body of the changelog should start with the backwards incompatible changes with a prominent header. The other sections (optional if nothing changed) are:

  • General: For new features of pySMT
  • Solvers: For upgrades or improvements to the solvers
  • Theories: For new or improved Theories
  • Bugfix: For all the fixes that do not constitute a new feature

Each item in the lists ends with reference to the Github issue or Pull request. If an item deserves more explanation and it is not associated with an issue or PR, it is acceptable to point to the exact commit id). Items should also acknowledge contributors for submitting patches, opening tickets or simply discussing a problem.

Version change

The variable VERSION in pysmt/__init__.py must be modified to show the correct version number: e.g., VERSION = (0, 6, 1).

Package creation and local testing

The utility script make_distrib.sh to create a distribution package is located in the root directory of the project. This will create various formats.

After running this script, the package dist/PySMT-a.b.c.tar.gz (where a.b.c are the release number), needs to be uploaded to pypi. Before doing so, however, we test it locally, to make sure that everything works. The most common mistake in this phase is the omission of a file in the package.

To test the package, we create a new hardcopy of the tests of pySMT:

  1. mkdir -p test_pkg/pysmt
  2. cp -a github/pysmt/test test_pkg/pysmt/; cd test_pkg
  3. This should fail: python -m pytest pysmt
  4. pip install --user github/dist/PySMT-a.b.c.tar.gz
  5. python -m pytest pysmt
  6. pip uninstall pysmt

All tests should pass in order to make the release. Note: It is enough to have one solver installed, in order to test the package. The type of issues that might occur during package creation are usually independent of the solver.

Merge and Tag

At this point we have created and tested the release, we can merge the rc/ branch back into master, and tag the release with: git tag -a va.b.c (note the v before the major version number), and finally push the tag to github git push origin va.b.c.

Now on github, it is possible to create the release associated with this tag. The description of the release is the copy-paste of the Changelog. Additionally, we include the wheel file and the tar.gz .

Immediately after tagging, make a commit on master bumping the version. By default we use (a, b, c+1, "dev", 1).

PyPi update

twine upload PySMT-a.b.c.tar.gz

TODO: Figure out how to have shared credentials for pypi. Currently, only marcogario has upload privileges.

Announcement

Performance Tricks

It is our experience that in many cases the performance limitations come from the solvers or from a sub-optimal encoding of the problem, and that pySMT performs well for most use-cases. Nevertheless, sometimes you just want to squeeze a bit more performance from the library, and there are a few things that you might want to try. As always, you should make sure that your code is correct before starting to optimize it.

Disable Assertions

Run the python interpreter with the -O option. Many functions in pySMT have assertions to help you discover problems early on. By using the command line option -O all assertions are disabled

Avoid Infix Notation and shortcuts

Infix notation and shortcuts assume that you are operating on the global environment. The expression a & b needs to:

  1. Resolve the implicit operator (i.e., translate & into And)
  2. Access the global environment
  3. Access the corresponding formula manager
  4. Check if the right-hand-side is already an FNode
  5. Call FormulaManager.And on the two elements.

Using a shortcut is similar in complexity, although you skip step 1 and 4. Therefore, within loop intensive code, make sure that you obtain a reference to the current formula manager or even better to the actual function call that you want to perform: e.g.,

Real = get_env().formula_manager.Real
for x in very_large_set:
    Real(x)

This will save dereferencing those objects over-and-over again.

Disabling Type-Checking

If you really want to squeeze that extra bit of performance, you might consider disabling the type-checker. In pySMT all expressions are checked at creation time in order to guarantee that they are well-formed and well-typed. However, this also means that on very big expressions, you will call many times the type-checker (see discussion in #400). Although, all calls to the type-checker are memoized, the cost of doing so can add up. If you are 100% sure that your expressions will be well-typed, then you can use the following code to create a context that disables temporarily the type-checker. WARNING: If you create an expression that is not well-typed while the type-checker is disabled, there is no way to detect it later on.

class SuspendTypeChecking(object):
    """Context to disable type-checking during formula creation."""

    def __init__(self, env=None):
        if env is None:
            env = get_env()
        self.env = env
        self.mgr = env.formula_manager

    def __enter__(self):
        """Entering a Context: Disable type-checking."""
        self.mgr._do_type_check = lambda x : x
        return self.env

    def __exit__(self, exc_type, exc_val, exc_tb):
        """Exiting the Context: Re-enable type-checking."""
        self.mgr._do_type_check = self.mgr._do_type_check_real

This can be used as follows:

with SuspendTypeChecking():
    r = And(Real(0), Real(1))

PyPy

pySMT is compatible with pypy. Unfortunately, we cannot run most of the solvers due to the way the bindings are created today. However, if are interfacing through the SMT-LIB interface, or are not using a solver, you can run pySMT using pypy. This can drastically improve the performances of code in which most of the time is spent in simple loops. A typical example is parsing, modifying, and dumping an SMT-LIB: this flow can significantly improve by using pypy.

Some work has been done in order to use CFFI to interface more solvers with pypy (see mathsat-cffi repo). If you are interested in this activity, please get in touch.