This file contains hints and documentation for developers, i.e., for developing JavaSMT, adding code, integrating or updating SMT solvers, and releasing JavaSMT into a public repository.
The style guide of this project is the Google Java Style: https://google.github.io/styleguide/javaguide.html
We use the auto-formatting tool, hence before committing run ant format-diff
on the staged files in order to format them, or ant format-source in order to
format the entire project.
Additionally, refer to the CPAchecker style guide for more information.
We rely on GitLab-CI for continuous integration, which picks up code style violations, compile warnings for both ECJ and javac (for several versions of Java), SpotBugs errors,...
Currently, releases are pushed to two software repositories, and there is seperate documentation for uploading packages into those repositories:
- Ivy Repository: see Developers-How-to-Release-into-Ivy
- Maven Central: see Developers-How-to-Release-into-Maven.md.
The release version number is derived from the git describe command,
which output is either a git tag (if the release version corresponds exactly
to the tagged commit), or a latest git tag together with a distance measured
in number of commits and a git hash corresponding to the current revision.
A new JavaSMT version is defined by creating a new git tag with a version number.
Git tags should be signed (git tag -s command).
When creating a new version number, populate the CHANGELOG.md file with the
changes which are exposed by the new release.
Semantic versioning guidelines should be followed when defining a new version.
In order to write a solver backend it is sufficient to provide the
implementation for the SolverContext interface.
A new backend does not have to implement all the present methods,
and should throw UnsupportedOperationException for methods it chooses to ignore.
Abstract classes located inside the basicimpl package could be very helpful
for writing new backends.
If the new backend is written inside JavaSMT,
SolverContextFactory and the Solvers enum should be updated
to include the new solver.
The new solver can be added from outside of JavaSMT as well: in that case,
the user might wish to have their own factory which can create
a suitable SolverContext.