From d90350053cdbd33a47da384344d4b1bbc4d42889 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 30 Nov 2019 16:55:56 +0100 Subject: [PATCH] updating documentation. --- CHANGELOG.md | 28 +++++++++++++++++++++++++ README.md | 16 ++++++++------ doc/Developers.md | 53 ++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 88 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1b2ca6e350..44ab6915bc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,33 @@ # JavaSMT ChangeLog +## JavaSMT 3.3.0 + +### Changes in the API: + - FloatingPointManager supports more arithmetic methods, such as `min`, `max`, `abs`, `sqrt`. + +### Improvements and Fixes: + - More consistency checks on bitvector constants + - The Maven release contains the bindings for Princess + - New or updated solver versions: + - Boolector 3.0.0-2019-11-11-g9d06cc0 was added (#174). + - CVC4: 1.8-prerelease-2019-11-30-gae93e65 + - Princess: 2.12-2019-11-20 + - SMTInterpol: 2.5-533-ga4ba1513 + - other solvers were not updated since the last release + +## JavaSMT 3.2.0 + +The biggest change is the integration of the CVC4 SMT solver (CVC4 1.8-prerelease). + +## JavaSMT 3.1.0 + +This is mostly a cleanup release that contains several smaller changes and optimizations. + +We included new solver versions: + +- OptiMathSAT: 1.6.3 +- SMTInterpol: 2.5-515-g2765bdd + ## JavaSMT 3.0.0 ### Changes in the API diff --git a/README.md b/README.md index e1c89ebe1e..2d032b5674 100644 --- a/README.md +++ b/README.md @@ -37,8 +37,10 @@ Currently JavaSMT support several SMT solvers (see [Getting Started](doc/Getting - [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) - [Princess](http://www.philipp.ruemmer.org/princess.shtml) - [Z3](https://github.com/Z3Prover/z3) + - [CVC4](https://cvc4.github.io/) + - [Boolector](https://boolector.github.io/) -The following features are supported: +The following features are supported (depending on the used SMT solver): - Satisfiability checking - Quantifiers and quantifier elimination @@ -46,12 +48,12 @@ The following features are supported: - Incremental solving with push/pop - Multiple independent contexts - Model generation - - Interpolation, including tree and sequential + - Interpolation, including tree and sequential structure - Formula transformation using built-in tactics - Formula introspection using visitors #### Multithreading Support -All solvers support multithreading (MathSAT only since JavaSMT 1.0.1-164-gd14ed28), +Most solvers support multithreading, provided that different threads use different contexts, and _all_ operations on a single context are performed from a single thread. Interruption using [ShutdownNotifier][] may be used to interrupt a @@ -79,7 +81,9 @@ Currently we do not support performing garbage collection for MathSAT5. ## Getting started -Installation is possible via [Maven][Maven repository], [Ivy][Ivy repository], or [manually][Manual Installation]. Please see our [Getting Started Guide](doc/Getting-started.md) +Installation is possible via [Maven][Maven repository], +[Ivy][Ivy repository], or [manually][Manual Installation]. +Please see our [Getting Started Guide](doc/Getting-started.md). #### Usage ``` java @@ -110,8 +114,8 @@ try (SolverContext context = SolverContextFactory.createSolverContext( - Project maintainers: [Karlheinz Friedberger][] and [Philipp Wendler][] - Former project maintainer: [George Karpenkov][] - Initial codebase, many design decisions: [Philipp Wendler][] - - Contributions: [Thomas Stieglmaier][] and others. - + - Contributions: Daniel Baier, [Thomas Stieglmaier][] and several others. + [ConfigurationOptions]: https://sosy-lab.github.io/java-smt/ConfigurationOptions.txt [Manual Installation]: doc/Getting-started.md#manual-installation [ShutdownNotifier]: https://sosy-lab.github.io/java-common-lib/api/org/sosy_lab/common/ShutdownNotifier.html diff --git a/doc/Developers.md b/doc/Developers.md index 47bedbb91b..d5e895d5b8 100644 --- a/doc/Developers.md +++ b/doc/Developers.md @@ -16,7 +16,7 @@ for more information. ## Continuous Integration 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), +compile warnings for both ECJ and javac (for several versions of Java), [SpotBugs](https://github.com/spotbugs/spotbugs) errors,... ## Releasing JavaSMT @@ -57,6 +57,10 @@ For publishing to Maven Central, we use the [Nexus Repository Manager](https://o #### Requirements +Please make sure that all necessary libraries are already released on Maven Central, +before (or at least while) publishing a new version of JavaSMT. +Maven does not check for existing dependencies automatically. + Please make sure that you have a valid user account and configured your local settings accordingly. For example, insert the following content into `~/.m2/settings.xml`: ```xml @@ -87,9 +91,9 @@ The following steps are required: - Run the `stage` ANT target. (There is currently no need to change any label from `SNAPSHOT` to `RELEASE` or vice versa, as written somewhere in the documentation, because we only produce `RELEASE` versions.) - - Login to [Nexus Repository Manager](https://oss.sonatype.org/) + - Login to [Nexus Repository Manager](https://oss.sonatype.org/) and open the [list of staging repositories](https://oss.sonatype.org/#stagingRepositories). - - Run `close` and `release` tasks on your pushed bundle + - Run `close` and `release` tasks on your pushed bundle (see [documentation](http://central.sonatype.org/pages/releasing-the-deployment.html) for details). - After some delay (a few hours or days) the release is automatically synced to Maven Central. @@ -97,6 +101,11 @@ Additional instructions are available at the official [OSSRH][] page. ## Releasing Solvers +Before actually releasing a new version of a solver into the public world, +make sure, it is tested sufficiently. +This is one of the most critical steps in JavaSMT development. + + ### Publishing Z3 We prefer to use the official Z3 binaries, @@ -131,6 +140,43 @@ ant publish-z3 -Dz3.path=$Z3_DIR/build ``` Finally follow the instructions shown in the message at the end. + +### Publishing CVC4 + +We prefer to use our own CVC4 binaries and Java bindings. + +To publish CVC4, checkout the [CVC4 repository](https://github.com/kfriedberger/CVC4). +Then execute the following command in the JavaSMT directory, +where `$CVC4_DIR` is the path to the CVC4 directory +and `$CVC4_VERSION` is the version number: +``` +ant publish-cvc4 -Dcvc4.path=$CVC4_DIR -Dcvc4.customRev=$CVC4_VERSION +``` +Example: +``` +ant publish-cvc4 -Dcvc4.path=../CVC4 -Dcvc4.customRev=1.8-prerelease-2019-10-05 +``` +Finally follow the instructions shown in the message at the end. + + +### Publishing Boolector + +We prefer to use our own Boolector binaries and Java bindings. + +To publish Boolector, checkout the [CVC4 repository](https://github.com/kfriedberger/CVC4). +Then execute the following command in the JavaSMT directory, +where `$BTOR_DIR` is the path to the CVC4 directory +and `$BTOR_VERSION` is the version number: +``` +ant publish-boolector -Dboolector.path=$BTOR_DIR -Dboolector.customRev=$BTOR_VERSION +``` +Example: +``` +ant publish-boolector -Dboolector.path=../boolector -Dboolector.customRev=3.0.0-2019-11-29 +``` +Finally follow the instructions shown in the message at the end. + + ### Publishing (Opti)-MathSAT5 For publishing MathSAT5, you need to use a machine with at least GCC 4.9. @@ -154,6 +200,7 @@ ant publish-optimathsat -Dmathsat.path=$OPTIMATHSAT_PATH -Dgmp.path=$GMP_PATH -D The scripts for publishing Princess and SMTInterpol are available at the root of the [Ivy Repository](https://svn.sosy-lab.org/software/ivy). + ## Writing Solver Backends In order to write a solver backend it is sufficient to provide the